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

Theorem sqwvfoura 44459
Description: Fourier coefficients for the square wave function. Since the square function is an odd function, there is no contribution from the 𝐴 coefficients. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
sqwvfoura.t 𝑇 = (2 · π)
sqwvfoura.f 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
sqwvfoura.n (𝜑𝑁 ∈ ℕ0)
Assertion
Ref Expression
sqwvfoura (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = 0)
Distinct variable groups:   𝑥,𝑁   𝜑,𝑥
Allowed substitution hints:   𝑇(𝑥)   𝐹(𝑥)

Proof of Theorem sqwvfoura
StepHypRef Expression
1 pire 25815 . . . . . 6 π ∈ ℝ
21renegcli 11462 . . . . 5 -π ∈ ℝ
32a1i 11 . . . 4 (𝜑 → -π ∈ ℝ)
41a1i 11 . . . 4 (𝜑 → π ∈ ℝ)
5 0re 11157 . . . . . 6 0 ∈ ℝ
6 negpilt0 43504 . . . . . . 7 -π < 0
72, 5, 6ltleii 11278 . . . . . 6 -π ≤ 0
8 pipos 25817 . . . . . . 7 0 < π
95, 1, 8ltleii 11278 . . . . . 6 0 ≤ π
102, 1elicc2i 13330 . . . . . 6 (0 ∈ (-π[,]π) ↔ (0 ∈ ℝ ∧ -π ≤ 0 ∧ 0 ≤ π))
115, 7, 9, 10mpbir3an 1341 . . . . 5 0 ∈ (-π[,]π)
1211a1i 11 . . . 4 (𝜑 → 0 ∈ (-π[,]π))
13 1red 11156 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 1 ∈ ℝ)
1413renegcld 11582 . . . . . . . . . . 11 (𝑥 ∈ ℝ → -1 ∈ ℝ)
1513, 14ifcld 4532 . . . . . . . . . 10 (𝑥 ∈ ℝ → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
1615adantl 482 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ) → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
17 sqwvfoura.f . . . . . . . . 9 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
1816, 17fmptd 7062 . . . . . . . 8 (𝜑𝐹:ℝ⟶ℝ)
1918adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → 𝐹:ℝ⟶ℝ)
20 elioore 13294 . . . . . . . 8 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℝ)
2120adantl 482 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → 𝑥 ∈ ℝ)
2219, 21ffvelcdmd 7036 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)π)) → (𝐹𝑥) ∈ ℝ)
23 sqwvfoura.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
2423nn0red 12474 . . . . . . . . 9 (𝜑𝑁 ∈ ℝ)
2524adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)π)) → 𝑁 ∈ ℝ)
2625, 21remulcld 11185 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → (𝑁 · 𝑥) ∈ ℝ)
2726recoscld 16026 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
2822, 27remulcld 11185 . . . . 5 ((𝜑𝑥 ∈ (-π(,)π)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) ∈ ℝ)
2928recnd 11183 . . . 4 ((𝜑𝑥 ∈ (-π(,)π)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) ∈ ℂ)
30 elioore 13294 . . . . . . . . . 10 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ ℝ)
3117fvmpt2 6959 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
3230, 15, 31syl2anc2 585 . . . . . . . . 9 (𝑥 ∈ (-π(,)0) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
331a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → π ∈ ℝ)
34 sqwvfoura.t . . . . . . . . . . . . . 14 𝑇 = (2 · π)
35 2rp 12920 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
36 pirp 25818 . . . . . . . . . . . . . . 15 π ∈ ℝ+
37 rpmulcl 12938 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ+ ∧ π ∈ ℝ+) → (2 · π) ∈ ℝ+)
3835, 36, 37mp2an 690 . . . . . . . . . . . . . 14 (2 · π) ∈ ℝ+
3934, 38eqeltri 2834 . . . . . . . . . . . . 13 𝑇 ∈ ℝ+
4039a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℝ+)
4130, 40modcld 13780 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → (𝑥 mod 𝑇) ∈ ℝ)
42 picn 25816 . . . . . . . . . . . . . . . . 17 π ∈ ℂ
43422timesi 12291 . . . . . . . . . . . . . . . 16 (2 · π) = (π + π)
4434, 43eqtri 2764 . . . . . . . . . . . . . . 15 𝑇 = (π + π)
4544oveq2i 7368 . . . . . . . . . . . . . 14 (-π + 𝑇) = (-π + (π + π))
462recni 11169 . . . . . . . . . . . . . . 15 -π ∈ ℂ
4746, 42, 42addassi 11165 . . . . . . . . . . . . . 14 ((-π + π) + π) = (-π + (π + π))
4842negidi 11470 . . . . . . . . . . . . . . . . 17 (π + -π) = 0
4942, 46, 48addcomli 11347 . . . . . . . . . . . . . . . 16 (-π + π) = 0
5049oveq1i 7367 . . . . . . . . . . . . . . 15 ((-π + π) + π) = (0 + π)
5142addid2i 11343 . . . . . . . . . . . . . . 15 (0 + π) = π
5250, 51eqtri 2764 . . . . . . . . . . . . . 14 ((-π + π) + π) = π
5345, 47, 523eqtr2ri 2771 . . . . . . . . . . . . 13 π = (-π + 𝑇)
542a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → -π ∈ ℝ)
55 2re 12227 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
5655, 1remulcli 11171 . . . . . . . . . . . . . . . 16 (2 · π) ∈ ℝ
5734, 56eqeltri 2834 . . . . . . . . . . . . . . 15 𝑇 ∈ ℝ
5857a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℝ)
592rexri 11213 . . . . . . . . . . . . . . . 16 -π ∈ ℝ*
6059a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → -π ∈ ℝ*)
61 0red 11158 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 0 ∈ ℝ)
6261rexrd 11205 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 0 ∈ ℝ*)
63 id 22 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ (-π(,)0))
64 ioogtlb 43723 . . . . . . . . . . . . . . 15 ((-π ∈ ℝ* ∧ 0 ∈ ℝ*𝑥 ∈ (-π(,)0)) → -π < 𝑥)
6560, 62, 63, 64syl3anc 1371 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → -π < 𝑥)
6654, 30, 58, 65ltadd1dd 11766 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → (-π + 𝑇) < (𝑥 + 𝑇))
6753, 66eqbrtrid 5140 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → π < (𝑥 + 𝑇))
6857recni 11169 . . . . . . . . . . . . . . . . 17 𝑇 ∈ ℂ
6968mulid2i 11160 . . . . . . . . . . . . . . . 16 (1 · 𝑇) = 𝑇
7069eqcomi 2745 . . . . . . . . . . . . . . 15 𝑇 = (1 · 𝑇)
7170oveq2i 7368 . . . . . . . . . . . . . 14 (𝑥 + 𝑇) = (𝑥 + (1 · 𝑇))
7271oveq1i 7367 . . . . . . . . . . . . 13 ((𝑥 + 𝑇) mod 𝑇) = ((𝑥 + (1 · 𝑇)) mod 𝑇)
7330, 58readdcld 11184 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) ∈ ℝ)
748a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 0 < π)
7561, 33, 73, 74, 67lttrd 11316 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 0 < (𝑥 + 𝑇))
7661, 73, 75ltled 11303 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 0 ≤ (𝑥 + 𝑇))
77 iooltub 43738 . . . . . . . . . . . . . . . . 17 ((-π ∈ ℝ* ∧ 0 ∈ ℝ*𝑥 ∈ (-π(,)0)) → 𝑥 < 0)
7860, 62, 63, 77syl3anc 1371 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 𝑥 < 0)
7930, 61, 58, 78ltadd1dd 11766 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) < (0 + 𝑇))
8068a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℂ)
8180addid2d 11356 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → (0 + 𝑇) = 𝑇)
8279, 81breqtrd 5131 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) < 𝑇)
83 modid 13801 . . . . . . . . . . . . . 14 ((((𝑥 + 𝑇) ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ (𝑥 + 𝑇) ∧ (𝑥 + 𝑇) < 𝑇)) → ((𝑥 + 𝑇) mod 𝑇) = (𝑥 + 𝑇))
8473, 40, 76, 82, 83syl22anc 837 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → ((𝑥 + 𝑇) mod 𝑇) = (𝑥 + 𝑇))
85 1zzd 12534 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 1 ∈ ℤ)
86 modcyc 13811 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((𝑥 + (1 · 𝑇)) mod 𝑇) = (𝑥 mod 𝑇))
8730, 40, 85, 86syl3anc 1371 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → ((𝑥 + (1 · 𝑇)) mod 𝑇) = (𝑥 mod 𝑇))
8872, 84, 873eqtr3a 2800 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) = (𝑥 mod 𝑇))
8967, 88breqtrd 5131 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → π < (𝑥 mod 𝑇))
9033, 41, 89ltnsymd 11304 . . . . . . . . . 10 (𝑥 ∈ (-π(,)0) → ¬ (𝑥 mod 𝑇) < π)
9190iffalsed 4497 . . . . . . . . 9 (𝑥 ∈ (-π(,)0) → if((𝑥 mod 𝑇) < π, 1, -1) = -1)
9232, 91eqtrd 2776 . . . . . . . 8 (𝑥 ∈ (-π(,)0) → (𝐹𝑥) = -1)
9392oveq1d 7372 . . . . . . 7 (𝑥 ∈ (-π(,)0) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (-1 · (cos‘(𝑁 · 𝑥))))
9493adantl 482 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)0)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (-1 · (cos‘(𝑁 · 𝑥))))
9594mpteq2dva 5205 . . . . 5 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) = (𝑥 ∈ (-π(,)0) ↦ (-1 · (cos‘(𝑁 · 𝑥)))))
96 1cnd 11150 . . . . . . 7 (𝜑 → 1 ∈ ℂ)
9796negcld 11499 . . . . . 6 (𝜑 → -1 ∈ ℂ)
9824adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)0)) → 𝑁 ∈ ℝ)
9930adantl 482 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)0)) → 𝑥 ∈ ℝ)
10098, 99remulcld 11185 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)0)) → (𝑁 · 𝑥) ∈ ℝ)
101100recoscld 16026 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
102 ioossicc 13350 . . . . . . . 8 (-π(,)0) ⊆ (-π[,]0)
103102a1i 11 . . . . . . 7 (𝜑 → (-π(,)0) ⊆ (-π[,]0))
104 ioombl 24929 . . . . . . . 8 (-π(,)0) ∈ dom vol
105104a1i 11 . . . . . . 7 (𝜑 → (-π(,)0) ∈ dom vol)
10624adantr 481 . . . . . . . . 9 ((𝜑𝑥 ∈ (-π[,]0)) → 𝑁 ∈ ℝ)
107 iccssre 13346 . . . . . . . . . . . 12 ((-π ∈ ℝ ∧ 0 ∈ ℝ) → (-π[,]0) ⊆ ℝ)
1082, 5, 107mp2an 690 . . . . . . . . . . 11 (-π[,]0) ⊆ ℝ
109108sseli 3940 . . . . . . . . . 10 (𝑥 ∈ (-π[,]0) → 𝑥 ∈ ℝ)
110109adantl 482 . . . . . . . . 9 ((𝜑𝑥 ∈ (-π[,]0)) → 𝑥 ∈ ℝ)
111106, 110remulcld 11185 . . . . . . . 8 ((𝜑𝑥 ∈ (-π[,]0)) → (𝑁 · 𝑥) ∈ ℝ)
112111recoscld 16026 . . . . . . 7 ((𝜑𝑥 ∈ (-π[,]0)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
113 0red 11158 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
114 coscn 25804 . . . . . . . . . 10 cos ∈ (ℂ–cn→ℂ)
115114a1i 11 . . . . . . . . 9 (𝜑 → cos ∈ (ℂ–cn→ℂ))
116 ax-resscn 11108 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
117108, 116sstri 3953 . . . . . . . . . . . 12 (-π[,]0) ⊆ ℂ
118117a1i 11 . . . . . . . . . . 11 (𝜑 → (-π[,]0) ⊆ ℂ)
11924recnd 11183 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
120 ssid 3966 . . . . . . . . . . . 12 ℂ ⊆ ℂ
121120a1i 11 . . . . . . . . . . 11 (𝜑 → ℂ ⊆ ℂ)
122118, 119, 121constcncfg 44103 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ 𝑁) ∈ ((-π[,]0)–cn→ℂ))
123118, 121idcncfg 44104 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ 𝑥) ∈ ((-π[,]0)–cn→ℂ))
124122, 123mulcncf 24810 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (𝑁 · 𝑥)) ∈ ((-π[,]0)–cn→ℂ))
125115, 124cncfmpt1f 24277 . . . . . . . 8 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((-π[,]0)–cn→ℂ))
126 cniccibl 25205 . . . . . . . 8 ((-π ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((-π[,]0)–cn→ℂ)) → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
1273, 113, 125, 126syl3anc 1371 . . . . . . 7 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
128103, 105, 112, 127iblss 25169 . . . . . 6 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
12997, 101, 128iblmulc2 25195 . . . . 5 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ (-1 · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
13095, 129eqeltrd 2838 . . . 4 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
131 elioore 13294 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℝ)
132131, 15, 31syl2anc2 585 . . . . . . . . 9 (𝑥 ∈ (0(,)π) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
13339a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 𝑇 ∈ ℝ+)
134 0red 11158 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 0 ∈ ℝ)
135134rexrd 11205 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → 0 ∈ ℝ*)
1361rexri 11213 . . . . . . . . . . . . . . 15 π ∈ ℝ*
137136a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → π ∈ ℝ*)
138 id 22 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → 𝑥 ∈ (0(,)π))
139 ioogtlb 43723 . . . . . . . . . . . . . 14 ((0 ∈ ℝ* ∧ π ∈ ℝ*𝑥 ∈ (0(,)π)) → 0 < 𝑥)
140135, 137, 138, 139syl3anc 1371 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 0 < 𝑥)
141134, 131, 140ltled 11303 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 0 ≤ 𝑥)
1421a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → π ∈ ℝ)
14357a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 𝑇 ∈ ℝ)
144 iooltub 43738 . . . . . . . . . . . . . 14 ((0 ∈ ℝ* ∧ π ∈ ℝ*𝑥 ∈ (0(,)π)) → 𝑥 < π)
145135, 137, 138, 144syl3anc 1371 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 𝑥 < π)
146 2timesgt 43512 . . . . . . . . . . . . . . . 16 (π ∈ ℝ+ → π < (2 · π))
14736, 146ax-mp 5 . . . . . . . . . . . . . . 15 π < (2 · π)
148147, 34breqtrri 5132 . . . . . . . . . . . . . 14 π < 𝑇
149148a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → π < 𝑇)
150131, 142, 143, 145, 149lttrd 11316 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 𝑥 < 𝑇)
151 modid 13801 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ 𝑥𝑥 < 𝑇)) → (𝑥 mod 𝑇) = 𝑥)
152131, 133, 141, 150, 151syl22anc 837 . . . . . . . . . . 11 (𝑥 ∈ (0(,)π) → (𝑥 mod 𝑇) = 𝑥)
153152, 145eqbrtrd 5127 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → (𝑥 mod 𝑇) < π)
154153iftrued 4494 . . . . . . . . 9 (𝑥 ∈ (0(,)π) → if((𝑥 mod 𝑇) < π, 1, -1) = 1)
155132, 154eqtrd 2776 . . . . . . . 8 (𝑥 ∈ (0(,)π) → (𝐹𝑥) = 1)
156155oveq1d 7372 . . . . . . 7 (𝑥 ∈ (0(,)π) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (1 · (cos‘(𝑁 · 𝑥))))
157156adantl 482 . . . . . 6 ((𝜑𝑥 ∈ (0(,)π)) → ((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) = (1 · (cos‘(𝑁 · 𝑥))))
158157mpteq2dva 5205 . . . . 5 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) = (𝑥 ∈ (0(,)π) ↦ (1 · (cos‘(𝑁 · 𝑥)))))
15924adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → 𝑁 ∈ ℝ)
160131adantl 482 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → 𝑥 ∈ ℝ)
161159, 160remulcld 11185 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) ∈ ℝ)
162161recoscld 16026 . . . . . 6 ((𝜑𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
163 ioossicc 13350 . . . . . . . 8 (0(,)π) ⊆ (0[,]π)
164163a1i 11 . . . . . . 7 (𝜑 → (0(,)π) ⊆ (0[,]π))
165 ioombl 24929 . . . . . . . 8 (0(,)π) ∈ dom vol
166165a1i 11 . . . . . . 7 (𝜑 → (0(,)π) ∈ dom vol)
16724adantr 481 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]π)) → 𝑁 ∈ ℝ)
168 iccssre 13346 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆ ℝ)
1695, 1, 168mp2an 690 . . . . . . . . . . 11 (0[,]π) ⊆ ℝ
170169sseli 3940 . . . . . . . . . 10 (𝑥 ∈ (0[,]π) → 𝑥 ∈ ℝ)
171170adantl 482 . . . . . . . . 9 ((𝜑𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℝ)
172167, 171remulcld 11185 . . . . . . . 8 ((𝜑𝑥 ∈ (0[,]π)) → (𝑁 · 𝑥) ∈ ℝ)
173172recoscld 16026 . . . . . . 7 ((𝜑𝑥 ∈ (0[,]π)) → (cos‘(𝑁 · 𝑥)) ∈ ℝ)
174169, 116sstri 3953 . . . . . . . . . . . 12 (0[,]π) ⊆ ℂ
175174a1i 11 . . . . . . . . . . 11 (𝜑 → (0[,]π) ⊆ ℂ)
176175, 119, 121constcncfg 44103 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0[,]π) ↦ 𝑁) ∈ ((0[,]π)–cn→ℂ))
177175, 121idcncfg 44104 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0[,]π) ↦ 𝑥) ∈ ((0[,]π)–cn→ℂ))
178176, 177mulcncf 24810 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝑁 · 𝑥)) ∈ ((0[,]π)–cn→ℂ))
179115, 178cncfmpt1f 24277 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((0[,]π)–cn→ℂ))
180 cniccibl 25205 . . . . . . . 8 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
181113, 4, 179, 180syl3anc 1371 . . . . . . 7 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
182164, 166, 173, 181iblss 25169 . . . . . 6 (𝜑 → (𝑥 ∈ (0(,)π) ↦ (cos‘(𝑁 · 𝑥))) ∈ 𝐿1)
18396, 162, 182iblmulc2 25195 . . . . 5 (𝜑 → (𝑥 ∈ (0(,)π) ↦ (1 · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
184158, 183eqeltrd 2838 . . . 4 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝐹𝑥) · (cos‘(𝑁 · 𝑥)))) ∈ 𝐿1)
1853, 4, 12, 29, 130, 184itgsplitioo 25202 . . 3 (𝜑 → ∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = (∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥))
186185oveq1d 7372 . 2 (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = ((∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) / π))
18794itgeq2dv 25146 . . . . 5 (𝜑 → ∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = ∫(-π(,)0)(-1 · (cos‘(𝑁 · 𝑥))) d𝑥)
18897, 101, 128itgmulc2 25198 . . . . 5 (𝜑 → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(-π(,)0)(-1 · (cos‘(𝑁 · 𝑥))) d𝑥)
189 oveq1 7364 . . . . . . . . . . . . . 14 (𝑁 = 0 → (𝑁 · 𝑥) = (0 · 𝑥))
190 ioosscn 13326 . . . . . . . . . . . . . . . 16 (-π(,)0) ⊆ ℂ
191190sseli 3940 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ ℂ)
192191mul02d 11353 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (0 · 𝑥) = 0)
193189, 192sylan9eq 2796 . . . . . . . . . . . . 13 ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (𝑁 · 𝑥) = 0)
194193fveq2d 6846 . . . . . . . . . . . 12 ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = (cos‘0))
195 cos0 16032 . . . . . . . . . . . 12 (cos‘0) = 1
196194, 195eqtrdi 2792 . . . . . . . . . . 11 ((𝑁 = 0 ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = 1)
197196adantll 712 . . . . . . . . . 10 (((𝜑𝑁 = 0) ∧ 𝑥 ∈ (-π(,)0)) → (cos‘(𝑁 · 𝑥)) = 1)
198197itgeq2dv 25146 . . . . . . . . 9 ((𝜑𝑁 = 0) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = ∫(-π(,)0)1 d𝑥)
199 ioovolcl 24934 . . . . . . . . . . . . 13 ((-π ∈ ℝ ∧ 0 ∈ ℝ) → (vol‘(-π(,)0)) ∈ ℝ)
2002, 5, 199mp2an 690 . . . . . . . . . . . 12 (vol‘(-π(,)0)) ∈ ℝ
201200a1i 11 . . . . . . . . . . 11 (𝜑 → (vol‘(-π(,)0)) ∈ ℝ)
202 itgconst 25183 . . . . . . . . . . 11 (((-π(,)0) ∈ dom vol ∧ (vol‘(-π(,)0)) ∈ ℝ ∧ 1 ∈ ℂ) → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
203105, 201, 96, 202syl3anc 1371 . . . . . . . . . 10 (𝜑 → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
204203adantr 481 . . . . . . . . 9 ((𝜑𝑁 = 0) → ∫(-π(,)0)1 d𝑥 = (1 · (vol‘(-π(,)0))))
205 volioo 24933 . . . . . . . . . . . . . . 15 ((-π ∈ ℝ ∧ 0 ∈ ℝ ∧ -π ≤ 0) → (vol‘(-π(,)0)) = (0 − -π))
2062, 5, 7, 205mp3an 1461 . . . . . . . . . . . . . 14 (vol‘(-π(,)0)) = (0 − -π)
207 0cn 11147 . . . . . . . . . . . . . . 15 0 ∈ ℂ
208207, 42subnegi 11480 . . . . . . . . . . . . . 14 (0 − -π) = (0 + π)
209206, 208, 513eqtri 2768 . . . . . . . . . . . . 13 (vol‘(-π(,)0)) = π
210209a1i 11 . . . . . . . . . . . 12 (𝜑 → (vol‘(-π(,)0)) = π)
211210oveq2d 7373 . . . . . . . . . . 11 (𝜑 → (1 · (vol‘(-π(,)0))) = (1 · π))
21242a1i 11 . . . . . . . . . . . 12 (𝜑 → π ∈ ℂ)
213212mulid2d 11173 . . . . . . . . . . 11 (𝜑 → (1 · π) = π)
214211, 213eqtrd 2776 . . . . . . . . . 10 (𝜑 → (1 · (vol‘(-π(,)0))) = π)
215214adantr 481 . . . . . . . . 9 ((𝜑𝑁 = 0) → (1 · (vol‘(-π(,)0))) = π)
216198, 204, 2153eqtrd 2780 . . . . . . . 8 ((𝜑𝑁 = 0) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = π)
217216oveq2d 7373 . . . . . . 7 ((𝜑𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = (-1 · π))
21842mulm1i 11600 . . . . . . . 8 (-1 · π) = -π
219218a1i 11 . . . . . . 7 ((𝜑𝑁 = 0) → (-1 · π) = -π)
220 iftrue 4492 . . . . . . . . 9 (𝑁 = 0 → if(𝑁 = 0, -π, 0) = -π)
221220eqcomd 2742 . . . . . . . 8 (𝑁 = 0 → -π = if(𝑁 = 0, -π, 0))
222221adantl 482 . . . . . . 7 ((𝜑𝑁 = 0) → -π = if(𝑁 = 0, -π, 0))
223217, 219, 2223eqtrd 2780 . . . . . 6 ((𝜑𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
22424adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑁 = 0) → 𝑁 ∈ ℝ)
22523nn0ge0d 12476 . . . . . . . . 9 (𝜑 → 0 ≤ 𝑁)
226225adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑁 = 0) → 0 ≤ 𝑁)
227 neqne 2951 . . . . . . . . 9 𝑁 = 0 → 𝑁 ≠ 0)
228227adantl 482 . . . . . . . 8 ((𝜑 ∧ ¬ 𝑁 = 0) → 𝑁 ≠ 0)
229224, 226, 228ne0gt0d 11292 . . . . . . 7 ((𝜑 ∧ ¬ 𝑁 = 0) → 0 < 𝑁)
230 1cnd 11150 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → 1 ∈ ℂ)
231230negcld 11499 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → -1 ∈ ℂ)
232231mul01d 11354 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → (-1 · 0) = 0)
233119adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → 𝑁 ∈ ℂ)
2342a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → -π ∈ ℝ)
235 0red 11158 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → 0 ∈ ℝ)
2367a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → -π ≤ 0)
237 simpr 485 . . . . . . . . . . . 12 ((𝜑 ∧ 0 < 𝑁) → 0 < 𝑁)
238237gt0ne0d 11719 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → 𝑁 ≠ 0)
239233, 234, 235, 236, 238itgcoscmulx 44200 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = (((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) / 𝑁))
240119mul01d 11354 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 · 0) = 0)
241240fveq2d 6846 . . . . . . . . . . . . . . 15 (𝜑 → (sin‘(𝑁 · 0)) = (sin‘0))
242 sin0 16031 . . . . . . . . . . . . . . 15 (sin‘0) = 0
243241, 242eqtrdi 2792 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑁 · 0)) = 0)
244119, 212mulneg2d 11609 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 · -π) = -(𝑁 · π))
245244fveq2d 6846 . . . . . . . . . . . . . . 15 (𝜑 → (sin‘(𝑁 · -π)) = (sin‘-(𝑁 · π)))
246119, 212mulcld 11175 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 · π) ∈ ℂ)
247 sinneg 16028 . . . . . . . . . . . . . . . 16 ((𝑁 · π) ∈ ℂ → (sin‘-(𝑁 · π)) = -(sin‘(𝑁 · π)))
248246, 247syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (sin‘-(𝑁 · π)) = -(sin‘(𝑁 · π)))
249245, 248eqtrd 2776 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑁 · -π)) = -(sin‘(𝑁 · π)))
250243, 249oveq12d 7375 . . . . . . . . . . . . 13 (𝜑 → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (0 − -(sin‘(𝑁 · π))))
251 0cnd 11148 . . . . . . . . . . . . . 14 (𝜑 → 0 ∈ ℂ)
252246sincld 16012 . . . . . . . . . . . . . 14 (𝜑 → (sin‘(𝑁 · π)) ∈ ℂ)
253251, 252subnegd 11519 . . . . . . . . . . . . 13 (𝜑 → (0 − -(sin‘(𝑁 · π))) = (0 + (sin‘(𝑁 · π))))
254252addid2d 11356 . . . . . . . . . . . . 13 (𝜑 → (0 + (sin‘(𝑁 · π))) = (sin‘(𝑁 · π)))
255250, 253, 2543eqtrd 2780 . . . . . . . . . . . 12 (𝜑 → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (sin‘(𝑁 · π)))
256255adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) = (sin‘(𝑁 · π)))
257256oveq1d 7372 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · 0)) − (sin‘(𝑁 · -π))) / 𝑁) = ((sin‘(𝑁 · π)) / 𝑁))
25823nn0zd 12525 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
259 sinkpi 25878 . . . . . . . . . . . . . 14 (𝑁 ∈ ℤ → (sin‘(𝑁 · π)) = 0)
260258, 259syl 17 . . . . . . . . . . . . 13 (𝜑 → (sin‘(𝑁 · π)) = 0)
261260oveq1d 7372 . . . . . . . . . . . 12 (𝜑 → ((sin‘(𝑁 · π)) / 𝑁) = (0 / 𝑁))
262261adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · π)) / 𝑁) = (0 / 𝑁))
263233, 238div0d 11930 . . . . . . . . . . 11 ((𝜑 ∧ 0 < 𝑁) → (0 / 𝑁) = 0)
264262, 263eqtrd 2776 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → ((sin‘(𝑁 · π)) / 𝑁) = 0)
265239, 257, 2643eqtrd 2780 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥 = 0)
266265oveq2d 7373 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = (-1 · 0))
267238neneqd 2948 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → ¬ 𝑁 = 0)
268267iffalsed 4497 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → if(𝑁 = 0, -π, 0) = 0)
269232, 266, 2683eqtr4d 2786 . . . . . . 7 ((𝜑 ∧ 0 < 𝑁) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
270229, 269syldan 591 . . . . . 6 ((𝜑 ∧ ¬ 𝑁 = 0) → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
271223, 270pm2.61dan 811 . . . . 5 (𝜑 → (-1 · ∫(-π(,)0)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, -π, 0))
272187, 188, 2713eqtr2d 2782 . . . 4 (𝜑 → ∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, -π, 0))
273157itgeq2dv 25146 . . . . 5 (𝜑 → ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = ∫(0(,)π)(1 · (cos‘(𝑁 · 𝑥))) d𝑥)
27496, 162, 182itgmulc2 25198 . . . . 5 (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(0(,)π)(1 · (cos‘(𝑁 · 𝑥))) d𝑥)
275162, 182itgcl 25148 . . . . . . 7 (𝜑 → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 ∈ ℂ)
276275mulid2d 11173 . . . . . 6 (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥)
277 simpl 483 . . . . . . . . . . . . . 14 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → 𝑁 = 0)
278277oveq1d 7372 . . . . . . . . . . . . 13 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) = (0 · 𝑥))
279131recnd 11183 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℂ)
280279adantl 482 . . . . . . . . . . . . . 14 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → 𝑥 ∈ ℂ)
281280mul02d 11353 . . . . . . . . . . . . 13 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (0 · 𝑥) = 0)
282278, 281eqtrd 2776 . . . . . . . . . . . 12 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (𝑁 · 𝑥) = 0)
283282fveq2d 6846 . . . . . . . . . . 11 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = (cos‘0))
284283, 195eqtrdi 2792 . . . . . . . . . 10 ((𝑁 = 0 ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = 1)
285284adantll 712 . . . . . . . . 9 (((𝜑𝑁 = 0) ∧ 𝑥 ∈ (0(,)π)) → (cos‘(𝑁 · 𝑥)) = 1)
286285itgeq2dv 25146 . . . . . . . 8 ((𝜑𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = ∫(0(,)π)1 d𝑥)
287 ioovolcl 24934 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ π ∈ ℝ) → (vol‘(0(,)π)) ∈ ℝ)
2885, 1, 287mp2an 690 . . . . . . . . . 10 (vol‘(0(,)π)) ∈ ℝ
289 ax-1cn 11109 . . . . . . . . . 10 1 ∈ ℂ
290 itgconst 25183 . . . . . . . . . 10 (((0(,)π) ∈ dom vol ∧ (vol‘(0(,)π)) ∈ ℝ ∧ 1 ∈ ℂ) → ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π))))
291165, 288, 289, 290mp3an 1461 . . . . . . . . 9 ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π)))
292291a1i 11 . . . . . . . 8 ((𝜑𝑁 = 0) → ∫(0(,)π)1 d𝑥 = (1 · (vol‘(0(,)π))))
29342mulid2i 11160 . . . . . . . . . 10 (1 · π) = π
294 volioo 24933 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ 0 ≤ π) → (vol‘(0(,)π)) = (π − 0))
2955, 1, 9, 294mp3an 1461 . . . . . . . . . . . . 13 (vol‘(0(,)π)) = (π − 0)
29642subid1i 11473 . . . . . . . . . . . . 13 (π − 0) = π
297295, 296eqtri 2764 . . . . . . . . . . . 12 (vol‘(0(,)π)) = π
298297oveq2i 7368 . . . . . . . . . . 11 (1 · (vol‘(0(,)π))) = (1 · π)
299298a1i 11 . . . . . . . . . 10 (𝑁 = 0 → (1 · (vol‘(0(,)π))) = (1 · π))
300 iftrue 4492 . . . . . . . . . 10 (𝑁 = 0 → if(𝑁 = 0, π, 0) = π)
301293, 299, 3003eqtr4a 2802 . . . . . . . . 9 (𝑁 = 0 → (1 · (vol‘(0(,)π))) = if(𝑁 = 0, π, 0))
302301adantl 482 . . . . . . . 8 ((𝜑𝑁 = 0) → (1 · (vol‘(0(,)π))) = if(𝑁 = 0, π, 0))
303286, 292, 3023eqtrd 2780 . . . . . . 7 ((𝜑𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
304260, 243oveq12d 7375 . . . . . . . . . . . . 13 (𝜑 → ((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) = (0 − 0))
305251subidd 11500 . . . . . . . . . . . . 13 (𝜑 → (0 − 0) = 0)
306304, 305eqtrd 2776 . . . . . . . . . . . 12 (𝜑 → ((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) = 0)
307306oveq1d 7372 . . . . . . . . . . 11 (𝜑 → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = (0 / 𝑁))
308307adantr 481 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = (0 / 𝑁))
309308, 263eqtrd 2776 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁) = 0)
3101a1i 11 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → π ∈ ℝ)
3119a1i 11 . . . . . . . . . 10 ((𝜑 ∧ 0 < 𝑁) → 0 ≤ π)
312233, 235, 310, 311, 238itgcoscmulx 44200 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = (((sin‘(𝑁 · π)) − (sin‘(𝑁 · 0))) / 𝑁))
313267iffalsed 4497 . . . . . . . . 9 ((𝜑 ∧ 0 < 𝑁) → if(𝑁 = 0, π, 0) = 0)
314309, 312, 3133eqtr4d 2786 . . . . . . . 8 ((𝜑 ∧ 0 < 𝑁) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
315229, 314syldan 591 . . . . . . 7 ((𝜑 ∧ ¬ 𝑁 = 0) → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
316303, 315pm2.61dan 811 . . . . . 6 (𝜑 → ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥 = if(𝑁 = 0, π, 0))
317276, 316eqtrd 2776 . . . . 5 (𝜑 → (1 · ∫(0(,)π)(cos‘(𝑁 · 𝑥)) d𝑥) = if(𝑁 = 0, π, 0))
318273, 274, 3173eqtr2d 2782 . . . 4 (𝜑 → ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 = if(𝑁 = 0, π, 0))
319272, 318oveq12d 7375 . . 3 (𝜑 → (∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) = (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)))
320319oveq1d 7372 . 2 (𝜑 → ((∫(-π(,)0)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥) / π) = ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π))
321220, 300oveq12d 7375 . . . . . . 7 (𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = (-π + π))
322321, 49eqtrdi 2792 . . . . . 6 (𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0)
323 iffalse 4495 . . . . . . . 8 𝑁 = 0 → if(𝑁 = 0, -π, 0) = 0)
324 iffalse 4495 . . . . . . . 8 𝑁 = 0 → if(𝑁 = 0, π, 0) = 0)
325323, 324oveq12d 7375 . . . . . . 7 𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = (0 + 0))
326 00id 11330 . . . . . . 7 (0 + 0) = 0
327325, 326eqtrdi 2792 . . . . . 6 𝑁 = 0 → (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0)
328322, 327pm2.61i 182 . . . . 5 (if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) = 0
329328oveq1i 7367 . . . 4 ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = (0 / π)
3305, 8gtneii 11267 . . . . 5 π ≠ 0
33142, 330div0i 11889 . . . 4 (0 / π) = 0
332329, 331eqtri 2764 . . 3 ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = 0
333332a1i 11 . 2 (𝜑 → ((if(𝑁 = 0, -π, 0) + if(𝑁 = 0, π, 0)) / π) = 0)
334186, 320, 3333eqtrd 2780 1 (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (cos‘(𝑁 · 𝑥))) d𝑥 / π) = 0)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1541  wcel 2106  wne 2943  wss 3910  ifcif 4486   class class class wbr 5105  cmpt 5188  dom cdm 5633  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  *cxr 11188   < clt 11189  cle 11190  cmin 11385  -cneg 11386   / cdiv 11812  2c2 12208  0cn0 12413  cz 12499  +crp 12915  (,)cioo 13264  [,]cicc 13267   mod cmo 13774  sincsin 15946  cosccos 15947  πcpi 15949  cnccncf 24239  volcvol 24827  𝐿1cibl 24981  citg 24982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cc 10371  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-symdif 4202  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-ofr 7618  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-omul 8417  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-dju 9837  df-card 9875  df-acn 9878  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-ef 15950  df-sin 15952  df-cos 15953  df-pi 15955  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-ovol 24828  df-vol 24829  df-mbf 24983  df-itg1 24984  df-itg2 24985  df-ibl 24986  df-itg 24987  df-0p 25034  df-limc 25230  df-dv 25231
This theorem is referenced by:  fouriersw  44462
  Copyright terms: Public domain W3C validator