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

Theorem sqwvfourb 41951
Description: Fourier series 𝐵 coefficients for the square wave function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
sqwvfourb.t 𝑇 = (2 · π)
sqwvfourb.f 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
sqwvfourb.n (𝜑𝑁 ∈ ℕ)
Assertion
Ref Expression
sqwvfourb (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 / π) = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))))
Distinct variable groups:   𝑥,𝑁   𝜑,𝑥
Allowed substitution hints:   𝑇(𝑥)   𝐹(𝑥)

Proof of Theorem sqwvfourb
StepHypRef Expression
1 pire 24747 . . . . . 6 π ∈ ℝ
21renegcli 10748 . . . . 5 -π ∈ ℝ
32a1i 11 . . . 4 (𝜑 → -π ∈ ℝ)
41a1i 11 . . . 4 (𝜑 → π ∈ ℝ)
5 0re 10441 . . . . . 6 0 ∈ ℝ
6 negpilt0 40981 . . . . . . 7 -π < 0
72, 5, 6ltleii 10563 . . . . . 6 -π ≤ 0
8 pipos 24749 . . . . . . 7 0 < π
95, 1, 8ltleii 10563 . . . . . 6 0 ≤ π
102, 1elicc2i 12618 . . . . . 6 (0 ∈ (-π[,]π) ↔ (0 ∈ ℝ ∧ -π ≤ 0 ∧ 0 ≤ π))
115, 7, 9, 10mpbir3an 1321 . . . . 5 0 ∈ (-π[,]π)
1211a1i 11 . . . 4 (𝜑 → 0 ∈ (-π[,]π))
13 elioore 12584 . . . . . . . 8 (𝑥 ∈ (-π(,)π) → 𝑥 ∈ ℝ)
1413adantl 474 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → 𝑥 ∈ ℝ)
15 1re 10439 . . . . . . . 8 1 ∈ ℝ
1615renegcli 10748 . . . . . . . 8 -1 ∈ ℝ
1715, 16ifcli 4396 . . . . . . 7 if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ
18 sqwvfourb.f . . . . . . . 8 𝐹 = (𝑥 ∈ ℝ ↦ if((𝑥 mod 𝑇) < π, 1, -1))
1918fvmpt2 6605 . . . . . . 7 ((𝑥 ∈ ℝ ∧ if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
2014, 17, 19sylancl 577 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)π)) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
2117a1i 11 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℝ)
2221recnd 10468 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)π)) → if((𝑥 mod 𝑇) < π, 1, -1) ∈ ℂ)
2320, 22eqeltrd 2866 . . . . 5 ((𝜑𝑥 ∈ (-π(,)π)) → (𝐹𝑥) ∈ ℂ)
24 sqwvfourb.n . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
2524nncnd 11457 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
2625adantr 473 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → 𝑁 ∈ ℂ)
2714recnd 10468 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)π)) → 𝑥 ∈ ℂ)
2826, 27mulcld 10460 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)π)) → (𝑁 · 𝑥) ∈ ℂ)
2928sincld 15343 . . . . 5 ((𝜑𝑥 ∈ (-π(,)π)) → (sin‘(𝑁 · 𝑥)) ∈ ℂ)
3023, 29mulcld 10460 . . . 4 ((𝜑𝑥 ∈ (-π(,)π)) → ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) ∈ ℂ)
31 elioore 12584 . . . . . . . . . 10 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ ℝ)
3231, 17, 19sylancl 577 . . . . . . . . 9 (𝑥 ∈ (-π(,)0) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
331a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → π ∈ ℝ)
34 sqwvfourb.t . . . . . . . . . . . . . 14 𝑇 = (2 · π)
35 2rp 12209 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
36 pirp 24750 . . . . . . . . . . . . . . 15 π ∈ ℝ+
37 rpmulcl 12229 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ+ ∧ π ∈ ℝ+) → (2 · π) ∈ ℝ+)
3835, 36, 37mp2an 679 . . . . . . . . . . . . . 14 (2 · π) ∈ ℝ+
3934, 38eqeltri 2862 . . . . . . . . . . . . 13 𝑇 ∈ ℝ+
4039a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℝ+)
4131, 40modcld 13058 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → (𝑥 mod 𝑇) ∈ ℝ)
42 picn 24748 . . . . . . . . . . . . . . . . . 18 π ∈ ℂ
43422timesi 11585 . . . . . . . . . . . . . . . . 17 (2 · π) = (π + π)
4434, 43eqtri 2802 . . . . . . . . . . . . . . . 16 𝑇 = (π + π)
4544oveq2i 6987 . . . . . . . . . . . . . . 15 (-π + 𝑇) = (-π + (π + π))
462recni 10454 . . . . . . . . . . . . . . . 16 -π ∈ ℂ
4746, 42, 42addassi 10450 . . . . . . . . . . . . . . 15 ((-π + π) + π) = (-π + (π + π))
4842negidi 10756 . . . . . . . . . . . . . . . . . 18 (π + -π) = 0
4942, 46, 48addcomli 10632 . . . . . . . . . . . . . . . . 17 (-π + π) = 0
5049oveq1i 6986 . . . . . . . . . . . . . . . 16 ((-π + π) + π) = (0 + π)
5142addid2i 10628 . . . . . . . . . . . . . . . 16 (0 + π) = π
5250, 51eqtri 2802 . . . . . . . . . . . . . . 15 ((-π + π) + π) = π
5345, 47, 523eqtr2ri 2809 . . . . . . . . . . . . . 14 π = (-π + 𝑇)
5453a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → π = (-π + 𝑇))
552a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → -π ∈ ℝ)
56 2re 11514 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
5756, 1remulcli 10456 . . . . . . . . . . . . . . . 16 (2 · π) ∈ ℝ
5834, 57eqeltri 2862 . . . . . . . . . . . . . . 15 𝑇 ∈ ℝ
5958a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℝ)
602rexri 10499 . . . . . . . . . . . . . . 15 -π ∈ ℝ*
61 0xr 10487 . . . . . . . . . . . . . . 15 0 ∈ ℝ*
62 ioogtlb 41207 . . . . . . . . . . . . . . 15 ((-π ∈ ℝ* ∧ 0 ∈ ℝ*𝑥 ∈ (-π(,)0)) → -π < 𝑥)
6360, 61, 62mp3an12 1430 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → -π < 𝑥)
6455, 31, 59, 63ltadd1dd 11052 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → (-π + 𝑇) < (𝑥 + 𝑇))
6554, 64eqbrtrd 4951 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → π < (𝑥 + 𝑇))
6658recni 10454 . . . . . . . . . . . . . . . . 17 𝑇 ∈ ℂ
6766mulid2i 10445 . . . . . . . . . . . . . . . 16 (1 · 𝑇) = 𝑇
6867eqcomi 2787 . . . . . . . . . . . . . . 15 𝑇 = (1 · 𝑇)
6968oveq2i 6987 . . . . . . . . . . . . . 14 (𝑥 + 𝑇) = (𝑥 + (1 · 𝑇))
7069oveq1i 6986 . . . . . . . . . . . . 13 ((𝑥 + 𝑇) mod 𝑇) = ((𝑥 + (1 · 𝑇)) mod 𝑇)
7131, 59readdcld 10469 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) ∈ ℝ)
72 0red 10443 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 0 ∈ ℝ)
738a1i 11 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 0 < π)
7472, 33, 71, 73, 65lttrd 10601 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → 0 < (𝑥 + 𝑇))
7572, 71, 74ltled 10588 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 0 ≤ (𝑥 + 𝑇))
76 iooltub 41223 . . . . . . . . . . . . . . . . 17 ((-π ∈ ℝ* ∧ 0 ∈ ℝ*𝑥 ∈ (-π(,)0)) → 𝑥 < 0)
7760, 61, 76mp3an12 1430 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 𝑥 < 0)
7831, 72, 59, 77ltadd1dd 11052 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) < (0 + 𝑇))
7959recnd 10468 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (-π(,)0) → 𝑇 ∈ ℂ)
8079addid2d 10641 . . . . . . . . . . . . . . 15 (𝑥 ∈ (-π(,)0) → (0 + 𝑇) = 𝑇)
8178, 80breqtrd 4955 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) < 𝑇)
82 modid 13079 . . . . . . . . . . . . . 14 ((((𝑥 + 𝑇) ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ (𝑥 + 𝑇) ∧ (𝑥 + 𝑇) < 𝑇)) → ((𝑥 + 𝑇) mod 𝑇) = (𝑥 + 𝑇))
8371, 40, 75, 81, 82syl22anc 826 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → ((𝑥 + 𝑇) mod 𝑇) = (𝑥 + 𝑇))
84 1zzd 11826 . . . . . . . . . . . . . 14 (𝑥 ∈ (-π(,)0) → 1 ∈ ℤ)
85 modcyc 13089 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ∧ 1 ∈ ℤ) → ((𝑥 + (1 · 𝑇)) mod 𝑇) = (𝑥 mod 𝑇))
8631, 40, 84, 85syl3anc 1351 . . . . . . . . . . . . 13 (𝑥 ∈ (-π(,)0) → ((𝑥 + (1 · 𝑇)) mod 𝑇) = (𝑥 mod 𝑇))
8770, 83, 863eqtr3a 2838 . . . . . . . . . . . 12 (𝑥 ∈ (-π(,)0) → (𝑥 + 𝑇) = (𝑥 mod 𝑇))
8865, 87breqtrd 4955 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → π < (𝑥 mod 𝑇))
8933, 41, 88ltnsymd 10589 . . . . . . . . . 10 (𝑥 ∈ (-π(,)0) → ¬ (𝑥 mod 𝑇) < π)
9089iffalsed 4361 . . . . . . . . 9 (𝑥 ∈ (-π(,)0) → if((𝑥 mod 𝑇) < π, 1, -1) = -1)
9132, 90eqtrd 2814 . . . . . . . 8 (𝑥 ∈ (-π(,)0) → (𝐹𝑥) = -1)
9291adantl 474 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)0)) → (𝐹𝑥) = -1)
9392oveq1d 6991 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)0)) → ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) = (-1 · (sin‘(𝑁 · 𝑥))))
9493mpteq2dva 5022 . . . . 5 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) = (𝑥 ∈ (-π(,)0) ↦ (-1 · (sin‘(𝑁 · 𝑥)))))
95 neg1cn 11561 . . . . . . 7 -1 ∈ ℂ
9695a1i 11 . . . . . 6 (𝜑 → -1 ∈ ℂ)
9724nnred 11456 . . . . . . . . 9 (𝜑𝑁 ∈ ℝ)
9897adantr 473 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)0)) → 𝑁 ∈ ℝ)
9931adantl 474 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)0)) → 𝑥 ∈ ℝ)
10098, 99remulcld 10470 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)0)) → (𝑁 · 𝑥) ∈ ℝ)
101100resincld 15356 . . . . . 6 ((𝜑𝑥 ∈ (-π(,)0)) → (sin‘(𝑁 · 𝑥)) ∈ ℝ)
102 ioossicc 12638 . . . . . . . 8 (-π(,)0) ⊆ (-π[,]0)
103102a1i 11 . . . . . . 7 (𝜑 → (-π(,)0) ⊆ (-π[,]0))
104 ioombl 23869 . . . . . . . 8 (-π(,)0) ∈ dom vol
105104a1i 11 . . . . . . 7 (𝜑 → (-π(,)0) ∈ dom vol)
10697adantr 473 . . . . . . . . 9 ((𝜑𝑥 ∈ (-π[,]0)) → 𝑁 ∈ ℝ)
107 iccssre 12634 . . . . . . . . . . . 12 ((-π ∈ ℝ ∧ 0 ∈ ℝ) → (-π[,]0) ⊆ ℝ)
1082, 5, 107mp2an 679 . . . . . . . . . . 11 (-π[,]0) ⊆ ℝ
109108sseli 3854 . . . . . . . . . 10 (𝑥 ∈ (-π[,]0) → 𝑥 ∈ ℝ)
110109adantl 474 . . . . . . . . 9 ((𝜑𝑥 ∈ (-π[,]0)) → 𝑥 ∈ ℝ)
111106, 110remulcld 10470 . . . . . . . 8 ((𝜑𝑥 ∈ (-π[,]0)) → (𝑁 · 𝑥) ∈ ℝ)
112111resincld 15356 . . . . . . 7 ((𝜑𝑥 ∈ (-π[,]0)) → (sin‘(𝑁 · 𝑥)) ∈ ℝ)
113 0red 10443 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
114 sincn 24735 . . . . . . . . . 10 sin ∈ (ℂ–cn→ℂ)
115114a1i 11 . . . . . . . . 9 (𝜑 → sin ∈ (ℂ–cn→ℂ))
116 ax-resscn 10392 . . . . . . . . . . . . 13 ℝ ⊆ ℂ
117108, 116sstri 3867 . . . . . . . . . . . 12 (-π[,]0) ⊆ ℂ
118117a1i 11 . . . . . . . . . . 11 (𝜑 → (-π[,]0) ⊆ ℂ)
119 ssid 3879 . . . . . . . . . . . 12 ℂ ⊆ ℂ
120119a1i 11 . . . . . . . . . . 11 (𝜑 → ℂ ⊆ ℂ)
121118, 25, 120constcncfg 41590 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ 𝑁) ∈ ((-π[,]0)–cn→ℂ))
122118, 120idcncfg 41591 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ 𝑥) ∈ ((-π[,]0)–cn→ℂ))
123121, 122mulcncf 23750 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (𝑁 · 𝑥)) ∈ ((-π[,]0)–cn→ℂ))
124115, 123cncfmpt1f 23224 . . . . . . . 8 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (sin‘(𝑁 · 𝑥))) ∈ ((-π[,]0)–cn→ℂ))
125 cniccibl 24144 . . . . . . . 8 ((-π ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝑥 ∈ (-π[,]0) ↦ (sin‘(𝑁 · 𝑥))) ∈ ((-π[,]0)–cn→ℂ)) → (𝑥 ∈ (-π[,]0) ↦ (sin‘(𝑁 · 𝑥))) ∈ 𝐿1)
1263, 113, 124, 125syl3anc 1351 . . . . . . 7 (𝜑 → (𝑥 ∈ (-π[,]0) ↦ (sin‘(𝑁 · 𝑥))) ∈ 𝐿1)
127103, 105, 112, 126iblss 24108 . . . . . 6 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ (sin‘(𝑁 · 𝑥))) ∈ 𝐿1)
12896, 101, 127iblmulc2 24134 . . . . 5 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ (-1 · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1)
12994, 128eqeltrd 2866 . . . 4 (𝜑 → (𝑥 ∈ (-π(,)0) ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1)
13060a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (0(,)π) → -π ∈ ℝ*)
1311rexri 10499 . . . . . . . . . . . 12 π ∈ ℝ*
132131a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (0(,)π) → π ∈ ℝ*)
133 elioore 12584 . . . . . . . . . . 11 (𝑥 ∈ (0(,)π) → 𝑥 ∈ ℝ)
1342a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → -π ∈ ℝ)
135 0red 10443 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 0 ∈ ℝ)
1366a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → -π < 0)
137 ioogtlb 41207 . . . . . . . . . . . . 13 ((0 ∈ ℝ* ∧ π ∈ ℝ*𝑥 ∈ (0(,)π)) → 0 < 𝑥)
13861, 131, 137mp3an12 1430 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → 0 < 𝑥)
139134, 135, 133, 136, 138lttrd 10601 . . . . . . . . . . 11 (𝑥 ∈ (0(,)π) → -π < 𝑥)
140 iooltub 41223 . . . . . . . . . . . 12 ((0 ∈ ℝ* ∧ π ∈ ℝ*𝑥 ∈ (0(,)π)) → 𝑥 < π)
14161, 131, 140mp3an12 1430 . . . . . . . . . . 11 (𝑥 ∈ (0(,)π) → 𝑥 < π)
142130, 132, 133, 139, 141eliood 41210 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → 𝑥 ∈ (-π(,)π))
143142, 20sylan2 583 . . . . . . . . 9 ((𝜑𝑥 ∈ (0(,)π)) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
14439a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 𝑇 ∈ ℝ+)
145135, 133, 138ltled 10588 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 0 ≤ 𝑥)
1461a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → π ∈ ℝ)
14758a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → 𝑇 ∈ ℝ)
148 2timesgt 40989 . . . . . . . . . . . . . . . . 17 (π ∈ ℝ+ → π < (2 · π))
14936, 148ax-mp 5 . . . . . . . . . . . . . . . 16 π < (2 · π)
150149, 34breqtrri 4956 . . . . . . . . . . . . . . 15 π < 𝑇
151150a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ (0(,)π) → π < 𝑇)
152133, 146, 147, 141, 151lttrd 10601 . . . . . . . . . . . . 13 (𝑥 ∈ (0(,)π) → 𝑥 < 𝑇)
153 modid 13079 . . . . . . . . . . . . 13 (((𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≤ 𝑥𝑥 < 𝑇)) → (𝑥 mod 𝑇) = 𝑥)
154133, 144, 145, 152, 153syl22anc 826 . . . . . . . . . . . 12 (𝑥 ∈ (0(,)π) → (𝑥 mod 𝑇) = 𝑥)
155154, 141eqbrtrd 4951 . . . . . . . . . . 11 (𝑥 ∈ (0(,)π) → (𝑥 mod 𝑇) < π)
156155iftrued 4358 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → if((𝑥 mod 𝑇) < π, 1, -1) = 1)
157156adantl 474 . . . . . . . . 9 ((𝜑𝑥 ∈ (0(,)π)) → if((𝑥 mod 𝑇) < π, 1, -1) = 1)
158143, 157eqtrd 2814 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → (𝐹𝑥) = 1)
159158oveq1d 6991 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)π)) → ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) = (1 · (sin‘(𝑁 · 𝑥))))
160142, 29sylan2 583 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → (sin‘(𝑁 · 𝑥)) ∈ ℂ)
161160mulid2d 10458 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)π)) → (1 · (sin‘(𝑁 · 𝑥))) = (sin‘(𝑁 · 𝑥)))
162159, 161eqtrd 2814 . . . . . 6 ((𝜑𝑥 ∈ (0(,)π)) → ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) = (sin‘(𝑁 · 𝑥)))
163162mpteq2dva 5022 . . . . 5 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) = (𝑥 ∈ (0(,)π) ↦ (sin‘(𝑁 · 𝑥))))
164 ioossicc 12638 . . . . . . 7 (0(,)π) ⊆ (0[,]π)
165164a1i 11 . . . . . 6 (𝜑 → (0(,)π) ⊆ (0[,]π))
166 ioombl 23869 . . . . . . 7 (0(,)π) ∈ dom vol
167166a1i 11 . . . . . 6 (𝜑 → (0(,)π) ∈ dom vol)
16897adantr 473 . . . . . . . 8 ((𝜑𝑥 ∈ (0[,]π)) → 𝑁 ∈ ℝ)
169 iccssre 12634 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ π ∈ ℝ) → (0[,]π) ⊆ ℝ)
1705, 1, 169mp2an 679 . . . . . . . . . 10 (0[,]π) ⊆ ℝ
171170sseli 3854 . . . . . . . . 9 (𝑥 ∈ (0[,]π) → 𝑥 ∈ ℝ)
172171adantl 474 . . . . . . . 8 ((𝜑𝑥 ∈ (0[,]π)) → 𝑥 ∈ ℝ)
173168, 172remulcld 10470 . . . . . . 7 ((𝜑𝑥 ∈ (0[,]π)) → (𝑁 · 𝑥) ∈ ℝ)
174173resincld 15356 . . . . . 6 ((𝜑𝑥 ∈ (0[,]π)) → (sin‘(𝑁 · 𝑥)) ∈ ℝ)
175170, 116sstri 3867 . . . . . . . . . . 11 (0[,]π) ⊆ ℂ
176175a1i 11 . . . . . . . . . 10 (𝜑 → (0[,]π) ⊆ ℂ)
177176, 25, 120constcncfg 41590 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0[,]π) ↦ 𝑁) ∈ ((0[,]π)–cn→ℂ))
178176, 120idcncfg 41591 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0[,]π) ↦ 𝑥) ∈ ((0[,]π)–cn→ℂ))
179177, 178mulcncf 23750 . . . . . . . 8 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (𝑁 · 𝑥)) ∈ ((0[,]π)–cn→ℂ))
180115, 179cncfmpt1f 23224 . . . . . . 7 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (sin‘(𝑁 · 𝑥))) ∈ ((0[,]π)–cn→ℂ))
181 cniccibl 24144 . . . . . . 7 ((0 ∈ ℝ ∧ π ∈ ℝ ∧ (𝑥 ∈ (0[,]π) ↦ (sin‘(𝑁 · 𝑥))) ∈ ((0[,]π)–cn→ℂ)) → (𝑥 ∈ (0[,]π) ↦ (sin‘(𝑁 · 𝑥))) ∈ 𝐿1)
182113, 4, 180, 181syl3anc 1351 . . . . . 6 (𝜑 → (𝑥 ∈ (0[,]π) ↦ (sin‘(𝑁 · 𝑥))) ∈ 𝐿1)
183165, 167, 174, 182iblss 24108 . . . . 5 (𝜑 → (𝑥 ∈ (0(,)π) ↦ (sin‘(𝑁 · 𝑥))) ∈ 𝐿1)
184163, 183eqeltrd 2866 . . . 4 (𝜑 → (𝑥 ∈ (0(,)π) ↦ ((𝐹𝑥) · (sin‘(𝑁 · 𝑥)))) ∈ 𝐿1)
1853, 4, 12, 30, 129, 184itgsplitioo 24141 . . 3 (𝜑 → ∫(-π(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 = (∫(-π(,)0)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥))
186185oveq1d 6991 . 2 (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 / π) = ((∫(-π(,)0)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥) / π))
18791oveq1d 6991 . . . . . . . . 9 (𝑥 ∈ (-π(,)0) → ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) = (-1 · (sin‘(𝑁 · 𝑥))))
188187adantl 474 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)0)) → ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) = (-1 · (sin‘(𝑁 · 𝑥))))
18960a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → -π ∈ ℝ*)
190131a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → π ∈ ℝ*)
19131, 72, 33, 77, 73lttrd 10601 . . . . . . . . . . 11 (𝑥 ∈ (-π(,)0) → 𝑥 < π)
192189, 190, 31, 63, 191eliood 41210 . . . . . . . . . 10 (𝑥 ∈ (-π(,)0) → 𝑥 ∈ (-π(,)π))
193192, 29sylan2 583 . . . . . . . . 9 ((𝜑𝑥 ∈ (-π(,)0)) → (sin‘(𝑁 · 𝑥)) ∈ ℂ)
194193mulm1d 10893 . . . . . . . 8 ((𝜑𝑥 ∈ (-π(,)0)) → (-1 · (sin‘(𝑁 · 𝑥))) = -(sin‘(𝑁 · 𝑥)))
195188, 194eqtrd 2814 . . . . . . 7 ((𝜑𝑥 ∈ (-π(,)0)) → ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) = -(sin‘(𝑁 · 𝑥)))
196195itgeq2dv 24085 . . . . . 6 (𝜑 → ∫(-π(,)0)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 = ∫(-π(,)0)-(sin‘(𝑁 · 𝑥)) d𝑥)
197101, 127itgneg 24107 . . . . . 6 (𝜑 → -∫(-π(,)0)(sin‘(𝑁 · 𝑥)) d𝑥 = ∫(-π(,)0)-(sin‘(𝑁 · 𝑥)) d𝑥)
19824nnne0d 11490 . . . . . . . . . 10 (𝜑𝑁 ≠ 0)
1997a1i 11 . . . . . . . . . 10 (𝜑 → -π ≤ 0)
20025, 198, 3, 113, 199itgsincmulx 41695 . . . . . . . . 9 (𝜑 → ∫(-π(,)0)(sin‘(𝑁 · 𝑥)) d𝑥 = (((cos‘(𝑁 · -π)) − (cos‘(𝑁 · 0))) / 𝑁))
20124nnzd 11899 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℤ)
202 cosknegpi 41586 . . . . . . . . . . . . 13 (𝑁 ∈ ℤ → (cos‘(𝑁 · -π)) = if(2 ∥ 𝑁, 1, -1))
203201, 202syl 17 . . . . . . . . . . . 12 (𝜑 → (cos‘(𝑁 · -π)) = if(2 ∥ 𝑁, 1, -1))
20425mul01d 10639 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 · 0) = 0)
205204fveq2d 6503 . . . . . . . . . . . . 13 (𝜑 → (cos‘(𝑁 · 0)) = (cos‘0))
206 cos0 15363 . . . . . . . . . . . . 13 (cos‘0) = 1
207205, 206syl6eq 2830 . . . . . . . . . . . 12 (𝜑 → (cos‘(𝑁 · 0)) = 1)
208203, 207oveq12d 6994 . . . . . . . . . . 11 (𝜑 → ((cos‘(𝑁 · -π)) − (cos‘(𝑁 · 0))) = (if(2 ∥ 𝑁, 1, -1) − 1))
209 1m1e0 11512 . . . . . . . . . . . . 13 (1 − 1) = 0
210 iftrue 4356 . . . . . . . . . . . . . 14 (2 ∥ 𝑁 → if(2 ∥ 𝑁, 1, -1) = 1)
211210oveq1d 6991 . . . . . . . . . . . . 13 (2 ∥ 𝑁 → (if(2 ∥ 𝑁, 1, -1) − 1) = (1 − 1))
212 iftrue 4356 . . . . . . . . . . . . 13 (2 ∥ 𝑁 → if(2 ∥ 𝑁, 0, -2) = 0)
213209, 211, 2123eqtr4a 2840 . . . . . . . . . . . 12 (2 ∥ 𝑁 → (if(2 ∥ 𝑁, 1, -1) − 1) = if(2 ∥ 𝑁, 0, -2))
214 iffalse 4359 . . . . . . . . . . . . . 14 (¬ 2 ∥ 𝑁 → if(2 ∥ 𝑁, 1, -1) = -1)
215214oveq1d 6991 . . . . . . . . . . . . 13 (¬ 2 ∥ 𝑁 → (if(2 ∥ 𝑁, 1, -1) − 1) = (-1 − 1))
216 ax-1cn 10393 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
217 negdi2 10745 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ 1 ∈ ℂ) → -(1 + 1) = (-1 − 1))
218216, 216, 217mp2an 679 . . . . . . . . . . . . . . 15 -(1 + 1) = (-1 − 1)
219218eqcomi 2787 . . . . . . . . . . . . . 14 (-1 − 1) = -(1 + 1)
220219a1i 11 . . . . . . . . . . . . 13 (¬ 2 ∥ 𝑁 → (-1 − 1) = -(1 + 1))
221 iffalse 4359 . . . . . . . . . . . . . 14 (¬ 2 ∥ 𝑁 → if(2 ∥ 𝑁, 0, -2) = -2)
222 1p1e2 11572 . . . . . . . . . . . . . . 15 (1 + 1) = 2
223222negeqi 10679 . . . . . . . . . . . . . 14 -(1 + 1) = -2
224221, 223syl6reqr 2833 . . . . . . . . . . . . 13 (¬ 2 ∥ 𝑁 → -(1 + 1) = if(2 ∥ 𝑁, 0, -2))
225215, 220, 2243eqtrd 2818 . . . . . . . . . . . 12 (¬ 2 ∥ 𝑁 → (if(2 ∥ 𝑁, 1, -1) − 1) = if(2 ∥ 𝑁, 0, -2))
226213, 225pm2.61i 177 . . . . . . . . . . 11 (if(2 ∥ 𝑁, 1, -1) − 1) = if(2 ∥ 𝑁, 0, -2)
227208, 226syl6eq 2830 . . . . . . . . . 10 (𝜑 → ((cos‘(𝑁 · -π)) − (cos‘(𝑁 · 0))) = if(2 ∥ 𝑁, 0, -2))
228227oveq1d 6991 . . . . . . . . 9 (𝜑 → (((cos‘(𝑁 · -π)) − (cos‘(𝑁 · 0))) / 𝑁) = (if(2 ∥ 𝑁, 0, -2) / 𝑁))
229200, 228eqtrd 2814 . . . . . . . 8 (𝜑 → ∫(-π(,)0)(sin‘(𝑁 · 𝑥)) d𝑥 = (if(2 ∥ 𝑁, 0, -2) / 𝑁))
230229negeqd 10680 . . . . . . 7 (𝜑 → -∫(-π(,)0)(sin‘(𝑁 · 𝑥)) d𝑥 = -(if(2 ∥ 𝑁, 0, -2) / 𝑁))
231 0cn 10431 . . . . . . . . . 10 0 ∈ ℂ
232 2cn 11515 . . . . . . . . . . 11 2 ∈ ℂ
233232negcli 10755 . . . . . . . . . 10 -2 ∈ ℂ
234231, 233ifcli 4396 . . . . . . . . 9 if(2 ∥ 𝑁, 0, -2) ∈ ℂ
235234a1i 11 . . . . . . . 8 (𝜑 → if(2 ∥ 𝑁, 0, -2) ∈ ℂ)
236235, 25, 198divnegd 11230 . . . . . . 7 (𝜑 → -(if(2 ∥ 𝑁, 0, -2) / 𝑁) = (-if(2 ∥ 𝑁, 0, -2) / 𝑁))
237 neg0 10733 . . . . . . . . . . 11 -0 = 0
238212negeqd 10680 . . . . . . . . . . 11 (2 ∥ 𝑁 → -if(2 ∥ 𝑁, 0, -2) = -0)
239 iftrue 4356 . . . . . . . . . . 11 (2 ∥ 𝑁 → if(2 ∥ 𝑁, 0, 2) = 0)
240237, 238, 2393eqtr4a 2840 . . . . . . . . . 10 (2 ∥ 𝑁 → -if(2 ∥ 𝑁, 0, -2) = if(2 ∥ 𝑁, 0, 2))
241232negnegi 10757 . . . . . . . . . . 11 --2 = 2
242221negeqd 10680 . . . . . . . . . . 11 (¬ 2 ∥ 𝑁 → -if(2 ∥ 𝑁, 0, -2) = --2)
243 iffalse 4359 . . . . . . . . . . 11 (¬ 2 ∥ 𝑁 → if(2 ∥ 𝑁, 0, 2) = 2)
244241, 242, 2433eqtr4a 2840 . . . . . . . . . 10 (¬ 2 ∥ 𝑁 → -if(2 ∥ 𝑁, 0, -2) = if(2 ∥ 𝑁, 0, 2))
245240, 244pm2.61i 177 . . . . . . . . 9 -if(2 ∥ 𝑁, 0, -2) = if(2 ∥ 𝑁, 0, 2)
246245oveq1i 6986 . . . . . . . 8 (-if(2 ∥ 𝑁, 0, -2) / 𝑁) = (if(2 ∥ 𝑁, 0, 2) / 𝑁)
247246a1i 11 . . . . . . 7 (𝜑 → (-if(2 ∥ 𝑁, 0, -2) / 𝑁) = (if(2 ∥ 𝑁, 0, 2) / 𝑁))
248230, 236, 2473eqtrd 2818 . . . . . 6 (𝜑 → -∫(-π(,)0)(sin‘(𝑁 · 𝑥)) d𝑥 = (if(2 ∥ 𝑁, 0, 2) / 𝑁))
249196, 197, 2483eqtr2d 2820 . . . . 5 (𝜑 → ∫(-π(,)0)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 = (if(2 ∥ 𝑁, 0, 2) / 𝑁))
250133, 17, 19sylancl 577 . . . . . . . . . . 11 (𝑥 ∈ (0(,)π) → (𝐹𝑥) = if((𝑥 mod 𝑇) < π, 1, -1))
251250, 156eqtrd 2814 . . . . . . . . . 10 (𝑥 ∈ (0(,)π) → (𝐹𝑥) = 1)
252251oveq1d 6991 . . . . . . . . 9 (𝑥 ∈ (0(,)π) → ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) = (1 · (sin‘(𝑁 · 𝑥))))
253252adantl 474 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)π)) → ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) = (1 · (sin‘(𝑁 · 𝑥))))
254253, 161eqtrd 2814 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)π)) → ((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) = (sin‘(𝑁 · 𝑥)))
255254itgeq2dv 24085 . . . . . 6 (𝜑 → ∫(0(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 = ∫(0(,)π)(sin‘(𝑁 · 𝑥)) d𝑥)
2569a1i 11 . . . . . . 7 (𝜑 → 0 ≤ π)
25725, 198, 113, 4, 256itgsincmulx 41695 . . . . . 6 (𝜑 → ∫(0(,)π)(sin‘(𝑁 · 𝑥)) d𝑥 = (((cos‘(𝑁 · 0)) − (cos‘(𝑁 · π))) / 𝑁))
258 coskpi2 41583 . . . . . . . . . 10 (𝑁 ∈ ℤ → (cos‘(𝑁 · π)) = if(2 ∥ 𝑁, 1, -1))
259201, 258syl 17 . . . . . . . . 9 (𝜑 → (cos‘(𝑁 · π)) = if(2 ∥ 𝑁, 1, -1))
260207, 259oveq12d 6994 . . . . . . . 8 (𝜑 → ((cos‘(𝑁 · 0)) − (cos‘(𝑁 · π))) = (1 − if(2 ∥ 𝑁, 1, -1)))
261210oveq2d 6992 . . . . . . . . . 10 (2 ∥ 𝑁 → (1 − if(2 ∥ 𝑁, 1, -1)) = (1 − 1))
262209, 261, 2393eqtr4a 2840 . . . . . . . . 9 (2 ∥ 𝑁 → (1 − if(2 ∥ 𝑁, 1, -1)) = if(2 ∥ 𝑁, 0, 2))
263214oveq2d 6992 . . . . . . . . . 10 (¬ 2 ∥ 𝑁 → (1 − if(2 ∥ 𝑁, 1, -1)) = (1 − -1))
264216, 216subnegi 10766 . . . . . . . . . . 11 (1 − -1) = (1 + 1)
265264a1i 11 . . . . . . . . . 10 (¬ 2 ∥ 𝑁 → (1 − -1) = (1 + 1))
266243, 222syl6reqr 2833 . . . . . . . . . 10 (¬ 2 ∥ 𝑁 → (1 + 1) = if(2 ∥ 𝑁, 0, 2))
267263, 265, 2663eqtrd 2818 . . . . . . . . 9 (¬ 2 ∥ 𝑁 → (1 − if(2 ∥ 𝑁, 1, -1)) = if(2 ∥ 𝑁, 0, 2))
268262, 267pm2.61i 177 . . . . . . . 8 (1 − if(2 ∥ 𝑁, 1, -1)) = if(2 ∥ 𝑁, 0, 2)
269260, 268syl6eq 2830 . . . . . . 7 (𝜑 → ((cos‘(𝑁 · 0)) − (cos‘(𝑁 · π))) = if(2 ∥ 𝑁, 0, 2))
270269oveq1d 6991 . . . . . 6 (𝜑 → (((cos‘(𝑁 · 0)) − (cos‘(𝑁 · π))) / 𝑁) = (if(2 ∥ 𝑁, 0, 2) / 𝑁))
271255, 257, 2703eqtrd 2818 . . . . 5 (𝜑 → ∫(0(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 = (if(2 ∥ 𝑁, 0, 2) / 𝑁))
272249, 271oveq12d 6994 . . . 4 (𝜑 → (∫(-π(,)0)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥) = ((if(2 ∥ 𝑁, 0, 2) / 𝑁) + (if(2 ∥ 𝑁, 0, 2) / 𝑁)))
273231, 232ifcli 4396 . . . . . 6 if(2 ∥ 𝑁, 0, 2) ∈ ℂ
274273a1i 11 . . . . 5 (𝜑 → if(2 ∥ 𝑁, 0, 2) ∈ ℂ)
275274, 274, 25, 198divdird 11255 . . . 4 (𝜑 → ((if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) / 𝑁) = ((if(2 ∥ 𝑁, 0, 2) / 𝑁) + (if(2 ∥ 𝑁, 0, 2) / 𝑁)))
276239, 239oveq12d 6994 . . . . . . . . 9 (2 ∥ 𝑁 → (if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) = (0 + 0))
277 00id 10615 . . . . . . . . 9 (0 + 0) = 0
278276, 277syl6eq 2830 . . . . . . . 8 (2 ∥ 𝑁 → (if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) = 0)
279278oveq1d 6991 . . . . . . 7 (2 ∥ 𝑁 → ((if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) / 𝑁) = (0 / 𝑁))
280279adantl 474 . . . . . 6 ((𝜑 ∧ 2 ∥ 𝑁) → ((if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) / 𝑁) = (0 / 𝑁))
28125, 198div0d 11216 . . . . . . 7 (𝜑 → (0 / 𝑁) = 0)
282281adantr 473 . . . . . 6 ((𝜑 ∧ 2 ∥ 𝑁) → (0 / 𝑁) = 0)
283 iftrue 4356 . . . . . . . 8 (2 ∥ 𝑁 → if(2 ∥ 𝑁, 0, (4 / 𝑁)) = 0)
284283eqcomd 2784 . . . . . . 7 (2 ∥ 𝑁 → 0 = if(2 ∥ 𝑁, 0, (4 / 𝑁)))
285284adantl 474 . . . . . 6 ((𝜑 ∧ 2 ∥ 𝑁) → 0 = if(2 ∥ 𝑁, 0, (4 / 𝑁)))
286280, 282, 2853eqtrd 2818 . . . . 5 ((𝜑 ∧ 2 ∥ 𝑁) → ((if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) / 𝑁) = if(2 ∥ 𝑁, 0, (4 / 𝑁)))
287243, 243oveq12d 6994 . . . . . . . . 9 (¬ 2 ∥ 𝑁 → (if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) = (2 + 2))
288 2p2e4 11582 . . . . . . . . 9 (2 + 2) = 4
289287, 288syl6eq 2830 . . . . . . . 8 (¬ 2 ∥ 𝑁 → (if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) = 4)
290289oveq1d 6991 . . . . . . 7 (¬ 2 ∥ 𝑁 → ((if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) / 𝑁) = (4 / 𝑁))
291 iffalse 4359 . . . . . . 7 (¬ 2 ∥ 𝑁 → if(2 ∥ 𝑁, 0, (4 / 𝑁)) = (4 / 𝑁))
292290, 291eqtr4d 2817 . . . . . 6 (¬ 2 ∥ 𝑁 → ((if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) / 𝑁) = if(2 ∥ 𝑁, 0, (4 / 𝑁)))
293292adantl 474 . . . . 5 ((𝜑 ∧ ¬ 2 ∥ 𝑁) → ((if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) / 𝑁) = if(2 ∥ 𝑁, 0, (4 / 𝑁)))
294286, 293pm2.61dan 800 . . . 4 (𝜑 → ((if(2 ∥ 𝑁, 0, 2) + if(2 ∥ 𝑁, 0, 2)) / 𝑁) = if(2 ∥ 𝑁, 0, (4 / 𝑁)))
295272, 275, 2943eqtr2d 2820 . . 3 (𝜑 → (∫(-π(,)0)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥) = if(2 ∥ 𝑁, 0, (4 / 𝑁)))
296295oveq1d 6991 . 2 (𝜑 → ((∫(-π(,)0)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 + ∫(0(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥) / π) = (if(2 ∥ 𝑁, 0, (4 / 𝑁)) / π))
297283oveq1d 6991 . . . . 5 (2 ∥ 𝑁 → (if(2 ∥ 𝑁, 0, (4 / 𝑁)) / π) = (0 / π))
298297adantl 474 . . . 4 ((𝜑 ∧ 2 ∥ 𝑁) → (if(2 ∥ 𝑁, 0, (4 / 𝑁)) / π) = (0 / π))
2995, 8gtneii 10552 . . . . . 6 π ≠ 0
30042, 299div0i 11175 . . . . 5 (0 / π) = 0
301300a1i 11 . . . 4 ((𝜑 ∧ 2 ∥ 𝑁) → (0 / π) = 0)
302 iftrue 4356 . . . . . 6 (2 ∥ 𝑁 → if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))) = 0)
303302eqcomd 2784 . . . . 5 (2 ∥ 𝑁 → 0 = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))))
304303adantl 474 . . . 4 ((𝜑 ∧ 2 ∥ 𝑁) → 0 = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))))
305298, 301, 3043eqtrd 2818 . . 3 ((𝜑 ∧ 2 ∥ 𝑁) → (if(2 ∥ 𝑁, 0, (4 / 𝑁)) / π) = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))))
306291oveq1d 6991 . . . . 5 (¬ 2 ∥ 𝑁 → (if(2 ∥ 𝑁, 0, (4 / 𝑁)) / π) = ((4 / 𝑁) / π))
307306adantl 474 . . . 4 ((𝜑 ∧ ¬ 2 ∥ 𝑁) → (if(2 ∥ 𝑁, 0, (4 / 𝑁)) / π) = ((4 / 𝑁) / π))
308 4cn 11526 . . . . . . 7 4 ∈ ℂ
309308a1i 11 . . . . . 6 (𝜑 → 4 ∈ ℂ)
31042a1i 11 . . . . . 6 (𝜑 → π ∈ ℂ)
311299a1i 11 . . . . . 6 (𝜑 → π ≠ 0)
312309, 25, 310, 198, 311divdiv1d 11248 . . . . 5 (𝜑 → ((4 / 𝑁) / π) = (4 / (𝑁 · π)))
313312adantr 473 . . . 4 ((𝜑 ∧ ¬ 2 ∥ 𝑁) → ((4 / 𝑁) / π) = (4 / (𝑁 · π)))
314 iffalse 4359 . . . . . 6 (¬ 2 ∥ 𝑁 → if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))) = (4 / (𝑁 · π)))
315314eqcomd 2784 . . . . 5 (¬ 2 ∥ 𝑁 → (4 / (𝑁 · π)) = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))))
316315adantl 474 . . . 4 ((𝜑 ∧ ¬ 2 ∥ 𝑁) → (4 / (𝑁 · π)) = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))))
317307, 313, 3163eqtrd 2818 . . 3 ((𝜑 ∧ ¬ 2 ∥ 𝑁) → (if(2 ∥ 𝑁, 0, (4 / 𝑁)) / π) = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))))
318305, 317pm2.61dan 800 . 2 (𝜑 → (if(2 ∥ 𝑁, 0, (4 / 𝑁)) / π) = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))))
319186, 296, 3183eqtrd 2818 1 (𝜑 → (∫(-π(,)π)((𝐹𝑥) · (sin‘(𝑁 · 𝑥))) d𝑥 / π) = if(2 ∥ 𝑁, 0, (4 / (𝑁 · π))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 387   = wceq 1507  wcel 2050  wne 2967  wss 3829  ifcif 4350   class class class wbr 4929  cmpt 5008  dom cdm 5407  cfv 6188  (class class class)co 6976  cc 10333  cr 10334  0cc0 10335  1c1 10336   + caddc 10338   · cmul 10340  *cxr 10473   < clt 10474  cle 10475  cmin 10670  -cneg 10671   / cdiv 11098  cn 11439  2c2 11495  4c4 11497  cz 11793  +crp 12204  (,)cioo 12554  [,]cicc 12557   mod cmo 13052  sincsin 15277  cosccos 15278  πcpi 15280  cdvds 15467  cnccncf 23187  volcvol 23767  𝐿1cibl 23921  citg 23922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-inf2 8898  ax-cc 9655  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412  ax-pre-sup 10413  ax-addf 10414  ax-mulf 10415
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-pss 3845  df-symdif 4106  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-iin 4795  df-disj 4898  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-se 5367  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-isom 6197  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-of 7227  df-ofr 7228  df-om 7397  df-1st 7501  df-2nd 7502  df-supp 7634  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-1o 7905  df-2o 7906  df-oadd 7909  df-omul 7910  df-er 8089  df-map 8208  df-pm 8209  df-ixp 8260  df-en 8307  df-dom 8308  df-sdom 8309  df-fin 8310  df-fsupp 8629  df-fi 8670  df-sup 8701  df-inf 8702  df-oi 8769  df-dju 9124  df-card 9162  df-acn 9165  df-cda 9388  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-div 11099  df-nn 11440  df-2 11503  df-3 11504  df-4 11505  df-5 11506  df-6 11507  df-7 11508  df-8 11509  df-9 11510  df-n0 11708  df-z 11794  df-dec 11912  df-uz 12059  df-q 12163  df-rp 12205  df-xneg 12324  df-xadd 12325  df-xmul 12326  df-ioo 12558  df-ioc 12559  df-ico 12560  df-icc 12561  df-fz 12709  df-fzo 12850  df-fl 12977  df-mod 13053  df-seq 13185  df-exp 13245  df-fac 13449  df-bc 13478  df-hash 13506  df-shft 14287  df-cj 14319  df-re 14320  df-im 14321  df-sqrt 14455  df-abs 14456  df-limsup 14689  df-clim 14706  df-rlim 14707  df-sum 14904  df-ef 15281  df-sin 15283  df-cos 15284  df-pi 15286  df-dvds 15468  df-struct 16341  df-ndx 16342  df-slot 16343  df-base 16345  df-sets 16346  df-ress 16347  df-plusg 16434  df-mulr 16435  df-starv 16436  df-sca 16437  df-vsca 16438  df-ip 16439  df-tset 16440  df-ple 16441  df-ds 16443  df-unif 16444  df-hom 16445  df-cco 16446  df-rest 16552  df-topn 16553  df-0g 16571  df-gsum 16572  df-topgen 16573  df-pt 16574  df-prds 16577  df-xrs 16631  df-qtop 16636  df-imas 16637  df-xps 16639  df-mre 16715  df-mrc 16716  df-acs 16718  df-mgm 17710  df-sgrp 17752  df-mnd 17763  df-submnd 17804  df-mulg 18012  df-cntz 18218  df-cmn 18668  df-psmet 20239  df-xmet 20240  df-met 20241  df-bl 20242  df-mopn 20243  df-fbas 20244  df-fg 20245  df-cnfld 20248  df-top 21206  df-topon 21223  df-topsp 21245  df-bases 21258  df-cld 21331  df-ntr 21332  df-cls 21333  df-nei 21410  df-lp 21448  df-perf 21449  df-cn 21539  df-cnp 21540  df-haus 21627  df-cmp 21699  df-tx 21874  df-hmeo 22067  df-fil 22158  df-fm 22250  df-flim 22251  df-flf 22252  df-xms 22633  df-ms 22634  df-tms 22635  df-cncf 23189  df-ovol 23768  df-vol 23769  df-mbf 23923  df-itg1 23924  df-itg2 23925  df-ibl 23926  df-itg 23927  df-0p 23974  df-limc 24167  df-dv 24168
This theorem is referenced by:  fouriersw  41953
  Copyright terms: Public domain W3C validator