Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem21 Structured version   Visualization version   GIF version

Theorem fourierdlem21 45516
Description: The coefficients of the fourier series are integrable and reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem21.f (𝜑𝐹:ℝ⟶ℝ)
fourierdlem21.c 𝐶 = (-π(,)π)
fourierdlem21.fibl (𝜑 → (𝐹𝐶) ∈ 𝐿1)
fourierdlem21.b 𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem21.n (𝜑𝑁 ∈ ℕ)
Assertion
Ref Expression
fourierdlem21 (𝜑 → (((𝐵𝑁) ∈ ℝ ∧ (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 ∈ ℝ))
Distinct variable groups:   𝐶,𝑛,𝑥   𝑛,𝐹,𝑥   𝑛,𝑁,𝑥   𝜑,𝑛,𝑥
Allowed substitution hints:   𝐵(𝑥,𝑛)

Proof of Theorem fourierdlem21
Dummy variables 𝑏 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnnn0 12509 . . . . . 6 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
2 fourierdlem21.f . . . . . . . . . . 11 (𝜑𝐹:ℝ⟶ℝ)
32adantr 480 . . . . . . . . . 10 ((𝜑𝑥𝐶) → 𝐹:ℝ⟶ℝ)
4 ioossre 13417 . . . . . . . . . . . 12 (-π(,)π) ⊆ ℝ
5 id 22 . . . . . . . . . . . . 13 (𝑥𝐶𝑥𝐶)
6 fourierdlem21.c . . . . . . . . . . . . 13 𝐶 = (-π(,)π)
75, 6eleqtrdi 2839 . . . . . . . . . . . 12 (𝑥𝐶𝑥 ∈ (-π(,)π))
84, 7sselid 3978 . . . . . . . . . . 11 (𝑥𝐶𝑥 ∈ ℝ)
98adantl 481 . . . . . . . . . 10 ((𝜑𝑥𝐶) → 𝑥 ∈ ℝ)
103, 9ffvelcdmd 7095 . . . . . . . . 9 ((𝜑𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
1110adantlr 714 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℝ)
12 nn0re 12511 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
1312adantr 480 . . . . . . . . . . 11 ((𝑛 ∈ ℕ0𝑥𝐶) → 𝑛 ∈ ℝ)
148adantl 481 . . . . . . . . . . 11 ((𝑛 ∈ ℕ0𝑥𝐶) → 𝑥 ∈ ℝ)
1513, 14remulcld 11274 . . . . . . . . . 10 ((𝑛 ∈ ℕ0𝑥𝐶) → (𝑛 · 𝑥) ∈ ℝ)
1615resincld 16119 . . . . . . . . 9 ((𝑛 ∈ ℕ0𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
1716adantll 713 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℝ)
1811, 17remulcld 11274 . . . . . . 7 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) ∈ ℝ)
19 ioombl 25493 . . . . . . . . . . . 12 (-π(,)π) ∈ dom vol
206, 19eqeltri 2825 . . . . . . . . . . 11 𝐶 ∈ dom vol
2120a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → 𝐶 ∈ dom vol)
22 eqidd 2729 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
23 eqidd 2729 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥)))
2421, 17, 11, 22, 23offval2 7705 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) = (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))))
2517recnd 11272 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (sin‘(𝑛 · 𝑥)) ∈ ℂ)
2611recnd 11272 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → (𝐹𝑥) ∈ ℂ)
2725, 26mulcomd 11265 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑥𝐶) → ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥)) = ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))))
2827mpteq2dva 5248 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((sin‘(𝑛 · 𝑥)) · (𝐹𝑥))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))))
2924, 28eqtr2d 2769 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))))
30 sincn 26380 . . . . . . . . . . . 12 sin ∈ (ℂ–cn→ℂ)
3130a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → sin ∈ (ℂ–cn→ℂ))
326, 4eqsstri 4014 . . . . . . . . . . . . . . . 16 𝐶 ⊆ ℝ
33 ax-resscn 11195 . . . . . . . . . . . . . . . 16 ℝ ⊆ ℂ
3432, 33sstri 3989 . . . . . . . . . . . . . . 15 𝐶 ⊆ ℂ
3534a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0𝐶 ⊆ ℂ)
3612recnd 11272 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
37 ssid 4002 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
3837a1i 11 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 → ℂ ⊆ ℂ)
3935, 36, 38constcncfg 45260 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 → (𝑥𝐶𝑛) ∈ (𝐶cn→ℂ))
4035, 38idcncfg 45261 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 → (𝑥𝐶𝑥) ∈ (𝐶cn→ℂ))
4139, 40mulcncf 25373 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0 → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
4241adantl 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝑛 · 𝑥)) ∈ (𝐶cn→ℂ))
4331, 42cncfmpt1f 24833 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ))
44 cnmbf 25587 . . . . . . . . . 10 ((𝐶 ∈ dom vol ∧ (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ (𝐶cn→ℂ)) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
4520, 43, 44sylancr 586 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn)
462feqmptd 6967 . . . . . . . . . . . . 13 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
4746reseq1d 5984 . . . . . . . . . . . 12 (𝜑 → (𝐹𝐶) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶))
48 resmpt 6041 . . . . . . . . . . . . 13 (𝐶 ⊆ ℝ → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
4932, 48mp1i 13 . . . . . . . . . . . 12 (𝜑 → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) ↾ 𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
5047, 49eqtr2d 2769 . . . . . . . . . . 11 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) = (𝐹𝐶))
51 fourierdlem21.fibl . . . . . . . . . . 11 (𝜑 → (𝐹𝐶) ∈ 𝐿1)
5250, 51eqeltrd 2829 . . . . . . . . . 10 (𝜑 → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
5352adantr 480 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1)
54 1re 11244 . . . . . . . . . . 11 1 ∈ ℝ
55 simpr 484 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
56 nfv 1910 . . . . . . . . . . . . . . . . 17 𝑥 𝑛 ∈ ℕ0
57 nfmpt1 5256 . . . . . . . . . . . . . . . . . . 19 𝑥(𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))
5857nfdm 5953 . . . . . . . . . . . . . . . . . 18 𝑥dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))
5958nfcri 2886 . . . . . . . . . . . . . . . . 17 𝑥 𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))
6056, 59nfan 1895 . . . . . . . . . . . . . . . 16 𝑥(𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
6116ex 412 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0 → (𝑥𝐶 → (sin‘(𝑛 · 𝑥)) ∈ ℝ))
6261adantr 480 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (𝑥𝐶 → (sin‘(𝑛 · 𝑥)) ∈ ℝ))
6360, 62ralrimi 3251 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → ∀𝑥𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ)
64 dmmptg 6246 . . . . . . . . . . . . . . 15 (∀𝑥𝐶 (sin‘(𝑛 · 𝑥)) ∈ ℝ → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
6563, 64syl 17 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = 𝐶)
6655, 65eleqtrd 2831 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → 𝑦𝐶)
67 eqidd 2729 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ0𝑦𝐶) → (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) = (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))))
68 oveq2 7428 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝑛 · 𝑥) = (𝑛 · 𝑦))
6968fveq2d 6901 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
7069adantl 481 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ0𝑦𝐶) ∧ 𝑥 = 𝑦) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑛 · 𝑦)))
71 simpr 484 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑦𝐶)
7212adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑛 ∈ ℝ)
7332, 71sselid 3978 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ0𝑦𝐶) → 𝑦 ∈ ℝ)
7472, 73remulcld 11274 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℕ0𝑦𝐶) → (𝑛 · 𝑦) ∈ ℝ)
7574resincld 16119 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ0𝑦𝐶) → (sin‘(𝑛 · 𝑦)) ∈ ℝ)
7667, 70, 71, 75fvmptd 7012 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℕ0𝑦𝐶) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦) = (sin‘(𝑛 · 𝑦)))
7776fveq2d 6901 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) = (abs‘(sin‘(𝑛 · 𝑦))))
78 abssinbd 44677 . . . . . . . . . . . . . . 15 ((𝑛 · 𝑦) ∈ ℝ → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
7974, 78syl 17 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘(sin‘(𝑛 · 𝑦))) ≤ 1)
8077, 79eqbrtrd 5170 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ0𝑦𝐶) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
8166, 80syldan 590 . . . . . . . . . . . 12 ((𝑛 ∈ ℕ0𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))) → (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
8281ralrimiva 3143 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1)
83 breq2 5152 . . . . . . . . . . . . 13 (𝑏 = 1 → ((abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ (abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
8483ralbidv 3174 . . . . . . . . . . . 12 (𝑏 = 1 → (∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏 ↔ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1))
8584rspcev 3609 . . . . . . . . . . 11 ((1 ∈ ℝ ∧ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 1) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
8654, 82, 85sylancr 586 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
8786adantl 481 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏)
88 bddmulibl 25767 . . . . . . . . 9 (((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∈ MblFn ∧ (𝑥𝐶 ↦ (𝐹𝑥)) ∈ 𝐿1 ∧ ∃𝑏 ∈ ℝ ∀𝑦 ∈ dom (𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))(abs‘((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥)))‘𝑦)) ≤ 𝑏) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
8945, 53, 87, 88syl3anc 1369 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → ((𝑥𝐶 ↦ (sin‘(𝑛 · 𝑥))) ∘f · (𝑥𝐶 ↦ (𝐹𝑥))) ∈ 𝐿1)
9029, 89eqeltrd 2829 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1)
9118, 90itgrecl 25726 . . . . . 6 ((𝜑𝑛 ∈ ℕ0) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
921, 91sylan2 592 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ)
93 pire 26392 . . . . . 6 π ∈ ℝ
9493a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → π ∈ ℝ)
95 0re 11246 . . . . . . 7 0 ∈ ℝ
96 pipos 26394 . . . . . . 7 0 < π
9795, 96gtneii 11356 . . . . . 6 π ≠ 0
9897a1i 11 . . . . 5 ((𝜑𝑛 ∈ ℕ) → π ≠ 0)
9992, 94, 98redivcld 12072 . . . 4 ((𝜑𝑛 ∈ ℕ) → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) ∈ ℝ)
100 fourierdlem21.b . . . 4 𝐵 = (𝑛 ∈ ℕ ↦ (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
10199, 100fmptd 7124 . . 3 (𝜑𝐵:ℕ⟶ℝ)
102 fourierdlem21.n . . 3 (𝜑𝑁 ∈ ℕ)
103101, 102ffvelcdmd 7095 . 2 (𝜑 → (𝐵𝑁) ∈ ℝ)
104102nnnn0d 12562 . . 3 (𝜑𝑁 ∈ ℕ0)
105 eleq1 2817 . . . . . . 7 (𝑛 = 𝑁 → (𝑛 ∈ ℕ0𝑁 ∈ ℕ0))
106105anbi2d 629 . . . . . 6 (𝑛 = 𝑁 → ((𝜑𝑛 ∈ ℕ0) ↔ (𝜑𝑁 ∈ ℕ0)))
107 simpl 482 . . . . . . . . . . 11 ((𝑛 = 𝑁𝑥𝐶) → 𝑛 = 𝑁)
108107oveq1d 7435 . . . . . . . . . 10 ((𝑛 = 𝑁𝑥𝐶) → (𝑛 · 𝑥) = (𝑁 · 𝑥))
109108fveq2d 6901 . . . . . . . . 9 ((𝑛 = 𝑁𝑥𝐶) → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑁 · 𝑥)))
110109oveq2d 7436 . . . . . . . 8 ((𝑛 = 𝑁𝑥𝐶) → ((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) = ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))))
111110mpteq2dva 5248 . . . . . . 7 (𝑛 = 𝑁 → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) = (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))))
112111eleq1d 2814 . . . . . 6 (𝑛 = 𝑁 → ((𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1 ↔ (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1))
113106, 112imbi12d 344 . . . . 5 (𝑛 = 𝑁 → (((𝜑𝑛 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑛 · 𝑥)))) ∈ 𝐿1) ↔ ((𝜑𝑁 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1)))
114113, 90vtoclg 3540 . . . 4 (𝑁 ∈ ℕ0 → ((𝜑𝑁 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1))
115114anabsi7 670 . . 3 ((𝜑𝑁 ∈ ℕ0) → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1)
116104, 115mpdan 686 . 2 (𝜑 → (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1)
117102ancli 548 . . 3 (𝜑 → (𝜑𝑁 ∈ ℕ))
118 eleq1 2817 . . . . . 6 (𝑛 = 𝑁 → (𝑛 ∈ ℕ ↔ 𝑁 ∈ ℕ))
119118anbi2d 629 . . . . 5 (𝑛 = 𝑁 → ((𝜑𝑛 ∈ ℕ) ↔ (𝜑𝑁 ∈ ℕ)))
120110itgeq2dv 25710 . . . . . 6 (𝑛 = 𝑁 → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 = ∫𝐶((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥)
121120eleq1d 2814 . . . . 5 (𝑛 = 𝑁 → (∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ ↔ ∫𝐶((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 ∈ ℝ))
122119, 121imbi12d 344 . . . 4 (𝑛 = 𝑁 → (((𝜑𝑛 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 ∈ ℝ) ↔ ((𝜑𝑁 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 ∈ ℝ)))
123122, 92vtoclg 3540 . . 3 (𝑁 ∈ ℕ → ((𝜑𝑁 ∈ ℕ) → ∫𝐶((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 ∈ ℝ))
124102, 117, 123sylc 65 . 2 (𝜑 → ∫𝐶((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 ∈ ℝ)
125103, 116, 124jca31 514 1 (𝜑 → (((𝐵𝑁) ∈ ℝ ∧ (𝑥𝐶 ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1) ∧ ∫𝐶((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 ∈ ℝ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1534  wcel 2099  wne 2937  wral 3058  wrex 3067  wss 3947   class class class wbr 5148  cmpt 5231  dom cdm 5678  cres 5680  wf 6544  cfv 6548  (class class class)co 7420  f cof 7683  cc 11136  cr 11137  0cc0 11138  1c1 11139   · cmul 11143  cle 11279  -cneg 11475   / cdiv 11901  cn 12242  0cn0 12502  (,)cioo 13356  abscabs 15213  sincsin 16039  πcpi 16042  cnccncf 24795  volcvol 25391  MblFncmbf 25542  𝐿1cibl 25545  citg 25546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-inf2 9664  ax-cc 10458  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-pre-sup 11216  ax-addf 11217
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-isom 6557  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7685  df-ofr 7686  df-om 7871  df-1st 7993  df-2nd 7994  df-supp 8166  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-1o 8486  df-2o 8487  df-oadd 8490  df-omul 8491  df-er 8724  df-map 8846  df-pm 8847  df-ixp 8916  df-en 8964  df-dom 8965  df-sdom 8966  df-fin 8967  df-fsupp 9386  df-fi 9434  df-sup 9465  df-inf 9466  df-oi 9533  df-dju 9924  df-card 9962  df-acn 9965  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243  df-2 12305  df-3 12306  df-4 12307  df-5 12308  df-6 12309  df-7 12310  df-8 12311  df-9 12312  df-n0 12503  df-z 12589  df-dec 12708  df-uz 12853  df-q 12963  df-rp 13007  df-xneg 13124  df-xadd 13125  df-xmul 13126  df-ioo 13360  df-ioc 13361  df-ico 13362  df-icc 13363  df-fz 13517  df-fzo 13660  df-fl 13789  df-mod 13867  df-seq 13999  df-exp 14059  df-fac 14265  df-bc 14294  df-hash 14322  df-shft 15046  df-cj 15078  df-re 15079  df-im 15080  df-sqrt 15214  df-abs 15215  df-limsup 15447  df-clim 15464  df-rlim 15465  df-sum 15665  df-ef 16043  df-sin 16045  df-cos 16046  df-pi 16048  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17180  df-ress 17209  df-plusg 17245  df-mulr 17246  df-starv 17247  df-sca 17248  df-vsca 17249  df-ip 17250  df-tset 17251  df-ple 17252  df-ds 17254  df-unif 17255  df-hom 17256  df-cco 17257  df-rest 17403  df-topn 17404  df-0g 17422  df-gsum 17423  df-topgen 17424  df-pt 17425  df-prds 17428  df-xrs 17483  df-qtop 17488  df-imas 17489  df-xps 17491  df-mre 17565  df-mrc 17566  df-acs 17568  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-submnd 18740  df-mulg 19023  df-cntz 19267  df-cmn 19736  df-psmet 21270  df-xmet 21271  df-met 21272  df-bl 21273  df-mopn 21274  df-fbas 21275  df-fg 21276  df-cnfld 21279  df-top 22795  df-topon 22812  df-topsp 22834  df-bases 22848  df-cld 22922  df-ntr 22923  df-cls 22924  df-nei 23001  df-lp 23039  df-perf 23040  df-cn 23130  df-cnp 23131  df-haus 23218  df-cmp 23290  df-tx 23465  df-hmeo 23658  df-fil 23749  df-fm 23841  df-flim 23842  df-flf 23843  df-xms 24225  df-ms 24226  df-tms 24227  df-cncf 24797  df-ovol 25392  df-vol 25393  df-mbf 25547  df-itg1 25548  df-itg2 25549  df-ibl 25550  df-itg 25551  df-0p 25598  df-limc 25794  df-dv 25795
This theorem is referenced by:  fourierdlem83  45577  fourierdlem112  45606
  Copyright terms: Public domain W3C validator
OSZAR »