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 44544
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 25831 . . . . . 6 Ο€ ∈ ℝ
21renegcli 11469 . . . . 5 -Ο€ ∈ ℝ
32a1i 11 . . . 4 (πœ‘ β†’ -Ο€ ∈ ℝ)
41a1i 11 . . . 4 (πœ‘ β†’ Ο€ ∈ ℝ)
5 0re 11164 . . . . . 6 0 ∈ ℝ
6 negpilt0 43588 . . . . . . 7 -Ο€ < 0
72, 5, 6ltleii 11285 . . . . . 6 -Ο€ ≀ 0
8 pipos 25833 . . . . . . 7 0 < Ο€
95, 1, 8ltleii 11285 . . . . . 6 0 ≀ Ο€
102, 1elicc2i 13337 . . . . . 6 (0 ∈ (-Ο€[,]Ο€) ↔ (0 ∈ ℝ ∧ -Ο€ ≀ 0 ∧ 0 ≀ Ο€))
115, 7, 9, 10mpbir3an 1342 . . . . 5 0 ∈ (-Ο€[,]Ο€)
1211a1i 11 . . . 4 (πœ‘ β†’ 0 ∈ (-Ο€[,]Ο€))
13 elioore 13301 . . . . . . . 8 (π‘₯ ∈ (-Ο€(,)Ο€) β†’ π‘₯ ∈ ℝ)
1413adantl 483 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)Ο€)) β†’ π‘₯ ∈ ℝ)
15 1re 11162 . . . . . . . 8 1 ∈ ℝ
1615renegcli 11469 . . . . . . . 8 -1 ∈ ℝ
1715, 16ifcli 4538 . . . . . . 7 if((π‘₯ mod 𝑇) < Ο€, 1, -1) ∈ ℝ
18 sqwvfourb.f . . . . . . . 8 𝐹 = (π‘₯ ∈ ℝ ↦ if((π‘₯ mod 𝑇) < Ο€, 1, -1))
1918fvmpt2 6964 . . . . . . 7 ((π‘₯ ∈ ℝ ∧ if((π‘₯ mod 𝑇) < Ο€, 1, -1) ∈ ℝ) β†’ (πΉβ€˜π‘₯) = if((π‘₯ mod 𝑇) < Ο€, 1, -1))
2014, 17, 19sylancl 587 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)Ο€)) β†’ (πΉβ€˜π‘₯) = if((π‘₯ mod 𝑇) < Ο€, 1, -1))
2117a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)Ο€)) β†’ if((π‘₯ mod 𝑇) < Ο€, 1, -1) ∈ ℝ)
2221recnd 11190 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)Ο€)) β†’ if((π‘₯ mod 𝑇) < Ο€, 1, -1) ∈ β„‚)
2320, 22eqeltrd 2838 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)Ο€)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
24 sqwvfourb.n . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ β„•)
2524nncnd 12176 . . . . . . . 8 (πœ‘ β†’ 𝑁 ∈ β„‚)
2625adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)Ο€)) β†’ 𝑁 ∈ β„‚)
2714recnd 11190 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)Ο€)) β†’ π‘₯ ∈ β„‚)
2826, 27mulcld 11182 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)Ο€)) β†’ (𝑁 Β· π‘₯) ∈ β„‚)
2928sincld 16019 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)Ο€)) β†’ (sinβ€˜(𝑁 Β· π‘₯)) ∈ β„‚)
3023, 29mulcld 11182 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)Ο€)) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) ∈ β„‚)
31 elioore 13301 . . . . . . . . . 10 (π‘₯ ∈ (-Ο€(,)0) β†’ π‘₯ ∈ ℝ)
3231, 17, 19sylancl 587 . . . . . . . . 9 (π‘₯ ∈ (-Ο€(,)0) β†’ (πΉβ€˜π‘₯) = if((π‘₯ mod 𝑇) < Ο€, 1, -1))
331a1i 11 . . . . . . . . . . 11 (π‘₯ ∈ (-Ο€(,)0) β†’ Ο€ ∈ ℝ)
34 sqwvfourb.t . . . . . . . . . . . . . 14 𝑇 = (2 Β· Ο€)
35 2rp 12927 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
36 pirp 25834 . . . . . . . . . . . . . . 15 Ο€ ∈ ℝ+
37 rpmulcl 12945 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ+ ∧ Ο€ ∈ ℝ+) β†’ (2 Β· Ο€) ∈ ℝ+)
3835, 36, 37mp2an 691 . . . . . . . . . . . . . 14 (2 Β· Ο€) ∈ ℝ+
3934, 38eqeltri 2834 . . . . . . . . . . . . 13 𝑇 ∈ ℝ+
4039a1i 11 . . . . . . . . . . . 12 (π‘₯ ∈ (-Ο€(,)0) β†’ 𝑇 ∈ ℝ+)
4131, 40modcld 13787 . . . . . . . . . . 11 (π‘₯ ∈ (-Ο€(,)0) β†’ (π‘₯ mod 𝑇) ∈ ℝ)
42 picn 25832 . . . . . . . . . . . . . . . . . 18 Ο€ ∈ β„‚
43422timesi 12298 . . . . . . . . . . . . . . . . 17 (2 Β· Ο€) = (Ο€ + Ο€)
4434, 43eqtri 2765 . . . . . . . . . . . . . . . 16 𝑇 = (Ο€ + Ο€)
4544oveq2i 7373 . . . . . . . . . . . . . . 15 (-Ο€ + 𝑇) = (-Ο€ + (Ο€ + Ο€))
462recni 11176 . . . . . . . . . . . . . . . 16 -Ο€ ∈ β„‚
4746, 42, 42addassi 11172 . . . . . . . . . . . . . . 15 ((-Ο€ + Ο€) + Ο€) = (-Ο€ + (Ο€ + Ο€))
4842negidi 11477 . . . . . . . . . . . . . . . . . 18 (Ο€ + -Ο€) = 0
4942, 46, 48addcomli 11354 . . . . . . . . . . . . . . . . 17 (-Ο€ + Ο€) = 0
5049oveq1i 7372 . . . . . . . . . . . . . . . 16 ((-Ο€ + Ο€) + Ο€) = (0 + Ο€)
5142addid2i 11350 . . . . . . . . . . . . . . . 16 (0 + Ο€) = Ο€
5250, 51eqtri 2765 . . . . . . . . . . . . . . 15 ((-Ο€ + Ο€) + Ο€) = Ο€
5345, 47, 523eqtr2ri 2772 . . . . . . . . . . . . . 14 Ο€ = (-Ο€ + 𝑇)
5453a1i 11 . . . . . . . . . . . . 13 (π‘₯ ∈ (-Ο€(,)0) β†’ Ο€ = (-Ο€ + 𝑇))
552a1i 11 . . . . . . . . . . . . . 14 (π‘₯ ∈ (-Ο€(,)0) β†’ -Ο€ ∈ ℝ)
56 2re 12234 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
5756, 1remulcli 11178 . . . . . . . . . . . . . . . 16 (2 Β· Ο€) ∈ ℝ
5834, 57eqeltri 2834 . . . . . . . . . . . . . . 15 𝑇 ∈ ℝ
5958a1i 11 . . . . . . . . . . . . . 14 (π‘₯ ∈ (-Ο€(,)0) β†’ 𝑇 ∈ ℝ)
602rexri 11220 . . . . . . . . . . . . . . 15 -Ο€ ∈ ℝ*
61 0xr 11209 . . . . . . . . . . . . . . 15 0 ∈ ℝ*
62 ioogtlb 43807 . . . . . . . . . . . . . . 15 ((-Ο€ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ -Ο€ < π‘₯)
6360, 61, 62mp3an12 1452 . . . . . . . . . . . . . 14 (π‘₯ ∈ (-Ο€(,)0) β†’ -Ο€ < π‘₯)
6455, 31, 59, 63ltadd1dd 11773 . . . . . . . . . . . . 13 (π‘₯ ∈ (-Ο€(,)0) β†’ (-Ο€ + 𝑇) < (π‘₯ + 𝑇))
6554, 64eqbrtrd 5132 . . . . . . . . . . . 12 (π‘₯ ∈ (-Ο€(,)0) β†’ Ο€ < (π‘₯ + 𝑇))
6658recni 11176 . . . . . . . . . . . . . . . . 17 𝑇 ∈ β„‚
6766mulid2i 11167 . . . . . . . . . . . . . . . 16 (1 Β· 𝑇) = 𝑇
6867eqcomi 2746 . . . . . . . . . . . . . . 15 𝑇 = (1 Β· 𝑇)
6968oveq2i 7373 . . . . . . . . . . . . . 14 (π‘₯ + 𝑇) = (π‘₯ + (1 Β· 𝑇))
7069oveq1i 7372 . . . . . . . . . . . . 13 ((π‘₯ + 𝑇) mod 𝑇) = ((π‘₯ + (1 Β· 𝑇)) mod 𝑇)
7131, 59readdcld 11191 . . . . . . . . . . . . . 14 (π‘₯ ∈ (-Ο€(,)0) β†’ (π‘₯ + 𝑇) ∈ ℝ)
72 0red 11165 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (-Ο€(,)0) β†’ 0 ∈ ℝ)
738a1i 11 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (-Ο€(,)0) β†’ 0 < Ο€)
7472, 33, 71, 73, 65lttrd 11323 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (-Ο€(,)0) β†’ 0 < (π‘₯ + 𝑇))
7572, 71, 74ltled 11310 . . . . . . . . . . . . . 14 (π‘₯ ∈ (-Ο€(,)0) β†’ 0 ≀ (π‘₯ + 𝑇))
76 iooltub 43822 . . . . . . . . . . . . . . . . 17 ((-Ο€ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ π‘₯ < 0)
7760, 61, 76mp3an12 1452 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (-Ο€(,)0) β†’ π‘₯ < 0)
7831, 72, 59, 77ltadd1dd 11773 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (-Ο€(,)0) β†’ (π‘₯ + 𝑇) < (0 + 𝑇))
7959recnd 11190 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (-Ο€(,)0) β†’ 𝑇 ∈ β„‚)
8079addid2d 11363 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (-Ο€(,)0) β†’ (0 + 𝑇) = 𝑇)
8178, 80breqtrd 5136 . . . . . . . . . . . . . 14 (π‘₯ ∈ (-Ο€(,)0) β†’ (π‘₯ + 𝑇) < 𝑇)
82 modid 13808 . . . . . . . . . . . . . 14 ((((π‘₯ + 𝑇) ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≀ (π‘₯ + 𝑇) ∧ (π‘₯ + 𝑇) < 𝑇)) β†’ ((π‘₯ + 𝑇) mod 𝑇) = (π‘₯ + 𝑇))
8371, 40, 75, 81, 82syl22anc 838 . . . . . . . . . . . . 13 (π‘₯ ∈ (-Ο€(,)0) β†’ ((π‘₯ + 𝑇) mod 𝑇) = (π‘₯ + 𝑇))
84 1zzd 12541 . . . . . . . . . . . . . 14 (π‘₯ ∈ (-Ο€(,)0) β†’ 1 ∈ β„€)
85 modcyc 13818 . . . . . . . . . . . . . 14 ((π‘₯ ∈ ℝ ∧ 𝑇 ∈ ℝ+ ∧ 1 ∈ β„€) β†’ ((π‘₯ + (1 Β· 𝑇)) mod 𝑇) = (π‘₯ mod 𝑇))
8631, 40, 84, 85syl3anc 1372 . . . . . . . . . . . . 13 (π‘₯ ∈ (-Ο€(,)0) β†’ ((π‘₯ + (1 Β· 𝑇)) mod 𝑇) = (π‘₯ mod 𝑇))
8770, 83, 863eqtr3a 2801 . . . . . . . . . . . 12 (π‘₯ ∈ (-Ο€(,)0) β†’ (π‘₯ + 𝑇) = (π‘₯ mod 𝑇))
8865, 87breqtrd 5136 . . . . . . . . . . 11 (π‘₯ ∈ (-Ο€(,)0) β†’ Ο€ < (π‘₯ mod 𝑇))
8933, 41, 88ltnsymd 11311 . . . . . . . . . 10 (π‘₯ ∈ (-Ο€(,)0) β†’ Β¬ (π‘₯ mod 𝑇) < Ο€)
9089iffalsed 4502 . . . . . . . . 9 (π‘₯ ∈ (-Ο€(,)0) β†’ if((π‘₯ mod 𝑇) < Ο€, 1, -1) = -1)
9132, 90eqtrd 2777 . . . . . . . 8 (π‘₯ ∈ (-Ο€(,)0) β†’ (πΉβ€˜π‘₯) = -1)
9291adantl 483 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ (πΉβ€˜π‘₯) = -1)
9392oveq1d 7377 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) = (-1 Β· (sinβ€˜(𝑁 Β· π‘₯))))
9493mpteq2dva 5210 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ (-Ο€(,)0) ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯)))) = (π‘₯ ∈ (-Ο€(,)0) ↦ (-1 Β· (sinβ€˜(𝑁 Β· π‘₯)))))
95 neg1cn 12274 . . . . . . 7 -1 ∈ β„‚
9695a1i 11 . . . . . 6 (πœ‘ β†’ -1 ∈ β„‚)
9724nnred 12175 . . . . . . . . 9 (πœ‘ β†’ 𝑁 ∈ ℝ)
9897adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ 𝑁 ∈ ℝ)
9931adantl 483 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ π‘₯ ∈ ℝ)
10098, 99remulcld 11192 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ (𝑁 Β· π‘₯) ∈ ℝ)
101100resincld 16032 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ (sinβ€˜(𝑁 Β· π‘₯)) ∈ ℝ)
102 ioossicc 13357 . . . . . . . 8 (-Ο€(,)0) βŠ† (-Ο€[,]0)
103102a1i 11 . . . . . . 7 (πœ‘ β†’ (-Ο€(,)0) βŠ† (-Ο€[,]0))
104 ioombl 24945 . . . . . . . 8 (-Ο€(,)0) ∈ dom vol
105104a1i 11 . . . . . . 7 (πœ‘ β†’ (-Ο€(,)0) ∈ dom vol)
10697adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]0)) β†’ 𝑁 ∈ ℝ)
107 iccssre 13353 . . . . . . . . . . . 12 ((-Ο€ ∈ ℝ ∧ 0 ∈ ℝ) β†’ (-Ο€[,]0) βŠ† ℝ)
1082, 5, 107mp2an 691 . . . . . . . . . . 11 (-Ο€[,]0) βŠ† ℝ
109108sseli 3945 . . . . . . . . . 10 (π‘₯ ∈ (-Ο€[,]0) β†’ π‘₯ ∈ ℝ)
110109adantl 483 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]0)) β†’ π‘₯ ∈ ℝ)
111106, 110remulcld 11192 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]0)) β†’ (𝑁 Β· π‘₯) ∈ ℝ)
112111resincld 16032 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (-Ο€[,]0)) β†’ (sinβ€˜(𝑁 Β· π‘₯)) ∈ ℝ)
113 0red 11165 . . . . . . . 8 (πœ‘ β†’ 0 ∈ ℝ)
114 sincn 25819 . . . . . . . . . 10 sin ∈ (ℂ–cnβ†’β„‚)
115114a1i 11 . . . . . . . . 9 (πœ‘ β†’ sin ∈ (ℂ–cnβ†’β„‚))
116 ax-resscn 11115 . . . . . . . . . . . . 13 ℝ βŠ† β„‚
117108, 116sstri 3958 . . . . . . . . . . . 12 (-Ο€[,]0) βŠ† β„‚
118117a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (-Ο€[,]0) βŠ† β„‚)
119 ssid 3971 . . . . . . . . . . . 12 β„‚ βŠ† β„‚
120119a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ β„‚ βŠ† β„‚)
121118, 25, 120constcncfg 44187 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ (-Ο€[,]0) ↦ 𝑁) ∈ ((-Ο€[,]0)–cnβ†’β„‚))
122118, 120idcncfg 44188 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ (-Ο€[,]0) ↦ π‘₯) ∈ ((-Ο€[,]0)–cnβ†’β„‚))
123121, 122mulcncf 24826 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (-Ο€[,]0) ↦ (𝑁 Β· π‘₯)) ∈ ((-Ο€[,]0)–cnβ†’β„‚))
124115, 123cncfmpt1f 24293 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ (-Ο€[,]0) ↦ (sinβ€˜(𝑁 Β· π‘₯))) ∈ ((-Ο€[,]0)–cnβ†’β„‚))
125 cniccibl 25221 . . . . . . . 8 ((-Ο€ ∈ ℝ ∧ 0 ∈ ℝ ∧ (π‘₯ ∈ (-Ο€[,]0) ↦ (sinβ€˜(𝑁 Β· π‘₯))) ∈ ((-Ο€[,]0)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (-Ο€[,]0) ↦ (sinβ€˜(𝑁 Β· π‘₯))) ∈ 𝐿1)
1263, 113, 124, 125syl3anc 1372 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (-Ο€[,]0) ↦ (sinβ€˜(𝑁 Β· π‘₯))) ∈ 𝐿1)
127103, 105, 112, 126iblss 25185 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ (-Ο€(,)0) ↦ (sinβ€˜(𝑁 Β· π‘₯))) ∈ 𝐿1)
12896, 101, 127iblmulc2 25211 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ (-Ο€(,)0) ↦ (-1 Β· (sinβ€˜(𝑁 Β· π‘₯)))) ∈ 𝐿1)
12994, 128eqeltrd 2838 . . . 4 (πœ‘ β†’ (π‘₯ ∈ (-Ο€(,)0) ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯)))) ∈ 𝐿1)
13060a1i 11 . . . . . . . . . . 11 (π‘₯ ∈ (0(,)Ο€) β†’ -Ο€ ∈ ℝ*)
1311rexri 11220 . . . . . . . . . . . 12 Ο€ ∈ ℝ*
132131a1i 11 . . . . . . . . . . 11 (π‘₯ ∈ (0(,)Ο€) β†’ Ο€ ∈ ℝ*)
133 elioore 13301 . . . . . . . . . . 11 (π‘₯ ∈ (0(,)Ο€) β†’ π‘₯ ∈ ℝ)
1342a1i 11 . . . . . . . . . . . 12 (π‘₯ ∈ (0(,)Ο€) β†’ -Ο€ ∈ ℝ)
135 0red 11165 . . . . . . . . . . . 12 (π‘₯ ∈ (0(,)Ο€) β†’ 0 ∈ ℝ)
1366a1i 11 . . . . . . . . . . . 12 (π‘₯ ∈ (0(,)Ο€) β†’ -Ο€ < 0)
137 ioogtlb 43807 . . . . . . . . . . . . 13 ((0 ∈ ℝ* ∧ Ο€ ∈ ℝ* ∧ π‘₯ ∈ (0(,)Ο€)) β†’ 0 < π‘₯)
13861, 131, 137mp3an12 1452 . . . . . . . . . . . 12 (π‘₯ ∈ (0(,)Ο€) β†’ 0 < π‘₯)
139134, 135, 133, 136, 138lttrd 11323 . . . . . . . . . . 11 (π‘₯ ∈ (0(,)Ο€) β†’ -Ο€ < π‘₯)
140 iooltub 43822 . . . . . . . . . . . 12 ((0 ∈ ℝ* ∧ Ο€ ∈ ℝ* ∧ π‘₯ ∈ (0(,)Ο€)) β†’ π‘₯ < Ο€)
14161, 131, 140mp3an12 1452 . . . . . . . . . . 11 (π‘₯ ∈ (0(,)Ο€) β†’ π‘₯ < Ο€)
142130, 132, 133, 139, 141eliood 43810 . . . . . . . . . 10 (π‘₯ ∈ (0(,)Ο€) β†’ π‘₯ ∈ (-Ο€(,)Ο€))
143142, 20sylan2 594 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (0(,)Ο€)) β†’ (πΉβ€˜π‘₯) = if((π‘₯ mod 𝑇) < Ο€, 1, -1))
14439a1i 11 . . . . . . . . . . . . 13 (π‘₯ ∈ (0(,)Ο€) β†’ 𝑇 ∈ ℝ+)
145135, 133, 138ltled 11310 . . . . . . . . . . . . 13 (π‘₯ ∈ (0(,)Ο€) β†’ 0 ≀ π‘₯)
1461a1i 11 . . . . . . . . . . . . . 14 (π‘₯ ∈ (0(,)Ο€) β†’ Ο€ ∈ ℝ)
14758a1i 11 . . . . . . . . . . . . . 14 (π‘₯ ∈ (0(,)Ο€) β†’ 𝑇 ∈ ℝ)
148 2timesgt 43596 . . . . . . . . . . . . . . . . 17 (Ο€ ∈ ℝ+ β†’ Ο€ < (2 Β· Ο€))
14936, 148ax-mp 5 . . . . . . . . . . . . . . . 16 Ο€ < (2 Β· Ο€)
150149, 34breqtrri 5137 . . . . . . . . . . . . . . 15 Ο€ < 𝑇
151150a1i 11 . . . . . . . . . . . . . 14 (π‘₯ ∈ (0(,)Ο€) β†’ Ο€ < 𝑇)
152133, 146, 147, 141, 151lttrd 11323 . . . . . . . . . . . . 13 (π‘₯ ∈ (0(,)Ο€) β†’ π‘₯ < 𝑇)
153 modid 13808 . . . . . . . . . . . . 13 (((π‘₯ ∈ ℝ ∧ 𝑇 ∈ ℝ+) ∧ (0 ≀ π‘₯ ∧ π‘₯ < 𝑇)) β†’ (π‘₯ mod 𝑇) = π‘₯)
154133, 144, 145, 152, 153syl22anc 838 . . . . . . . . . . . 12 (π‘₯ ∈ (0(,)Ο€) β†’ (π‘₯ mod 𝑇) = π‘₯)
155154, 141eqbrtrd 5132 . . . . . . . . . . 11 (π‘₯ ∈ (0(,)Ο€) β†’ (π‘₯ mod 𝑇) < Ο€)
156155iftrued 4499 . . . . . . . . . 10 (π‘₯ ∈ (0(,)Ο€) β†’ if((π‘₯ mod 𝑇) < Ο€, 1, -1) = 1)
157156adantl 483 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (0(,)Ο€)) β†’ if((π‘₯ mod 𝑇) < Ο€, 1, -1) = 1)
158143, 157eqtrd 2777 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (0(,)Ο€)) β†’ (πΉβ€˜π‘₯) = 1)
159158oveq1d 7377 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (0(,)Ο€)) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) = (1 Β· (sinβ€˜(𝑁 Β· π‘₯))))
160142, 29sylan2 594 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (0(,)Ο€)) β†’ (sinβ€˜(𝑁 Β· π‘₯)) ∈ β„‚)
161160mulid2d 11180 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (0(,)Ο€)) β†’ (1 Β· (sinβ€˜(𝑁 Β· π‘₯))) = (sinβ€˜(𝑁 Β· π‘₯)))
162159, 161eqtrd 2777 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)Ο€)) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) = (sinβ€˜(𝑁 Β· π‘₯)))
163162mpteq2dva 5210 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ (0(,)Ο€) ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯)))) = (π‘₯ ∈ (0(,)Ο€) ↦ (sinβ€˜(𝑁 Β· π‘₯))))
164 ioossicc 13357 . . . . . . 7 (0(,)Ο€) βŠ† (0[,]Ο€)
165164a1i 11 . . . . . 6 (πœ‘ β†’ (0(,)Ο€) βŠ† (0[,]Ο€))
166 ioombl 24945 . . . . . . 7 (0(,)Ο€) ∈ dom vol
167166a1i 11 . . . . . 6 (πœ‘ β†’ (0(,)Ο€) ∈ dom vol)
16897adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (0[,]Ο€)) β†’ 𝑁 ∈ ℝ)
169 iccssre 13353 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ Ο€ ∈ ℝ) β†’ (0[,]Ο€) βŠ† ℝ)
1705, 1, 169mp2an 691 . . . . . . . . . 10 (0[,]Ο€) βŠ† ℝ
171170sseli 3945 . . . . . . . . 9 (π‘₯ ∈ (0[,]Ο€) β†’ π‘₯ ∈ ℝ)
172171adantl 483 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (0[,]Ο€)) β†’ π‘₯ ∈ ℝ)
173168, 172remulcld 11192 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (0[,]Ο€)) β†’ (𝑁 Β· π‘₯) ∈ ℝ)
174173resincld 16032 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0[,]Ο€)) β†’ (sinβ€˜(𝑁 Β· π‘₯)) ∈ ℝ)
175170, 116sstri 3958 . . . . . . . . . . 11 (0[,]Ο€) βŠ† β„‚
176175a1i 11 . . . . . . . . . 10 (πœ‘ β†’ (0[,]Ο€) βŠ† β„‚)
177176, 25, 120constcncfg 44187 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (0[,]Ο€) ↦ 𝑁) ∈ ((0[,]Ο€)–cnβ†’β„‚))
178176, 120idcncfg 44188 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ (0[,]Ο€) ↦ π‘₯) ∈ ((0[,]Ο€)–cnβ†’β„‚))
179177, 178mulcncf 24826 . . . . . . . 8 (πœ‘ β†’ (π‘₯ ∈ (0[,]Ο€) ↦ (𝑁 Β· π‘₯)) ∈ ((0[,]Ο€)–cnβ†’β„‚))
180115, 179cncfmpt1f 24293 . . . . . . 7 (πœ‘ β†’ (π‘₯ ∈ (0[,]Ο€) ↦ (sinβ€˜(𝑁 Β· π‘₯))) ∈ ((0[,]Ο€)–cnβ†’β„‚))
181 cniccibl 25221 . . . . . . 7 ((0 ∈ ℝ ∧ Ο€ ∈ ℝ ∧ (π‘₯ ∈ (0[,]Ο€) ↦ (sinβ€˜(𝑁 Β· π‘₯))) ∈ ((0[,]Ο€)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (0[,]Ο€) ↦ (sinβ€˜(𝑁 Β· π‘₯))) ∈ 𝐿1)
182113, 4, 180, 181syl3anc 1372 . . . . . 6 (πœ‘ β†’ (π‘₯ ∈ (0[,]Ο€) ↦ (sinβ€˜(𝑁 Β· π‘₯))) ∈ 𝐿1)
183165, 167, 174, 182iblss 25185 . . . . 5 (πœ‘ β†’ (π‘₯ ∈ (0(,)Ο€) ↦ (sinβ€˜(𝑁 Β· π‘₯))) ∈ 𝐿1)
184163, 183eqeltrd 2838 . . . 4 (πœ‘ β†’ (π‘₯ ∈ (0(,)Ο€) ↦ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯)))) ∈ 𝐿1)
1853, 4, 12, 30, 129, 184itgsplitioo 25218 . . 3 (πœ‘ β†’ ∫(-Ο€(,)Ο€)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ = (∫(-Ο€(,)0)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ + ∫(0(,)Ο€)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯))
186185oveq1d 7377 . 2 (πœ‘ β†’ (∫(-Ο€(,)Ο€)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ / Ο€) = ((∫(-Ο€(,)0)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ + ∫(0(,)Ο€)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯) / Ο€))
18791oveq1d 7377 . . . . . . . . 9 (π‘₯ ∈ (-Ο€(,)0) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) = (-1 Β· (sinβ€˜(𝑁 Β· π‘₯))))
188187adantl 483 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) = (-1 Β· (sinβ€˜(𝑁 Β· π‘₯))))
18960a1i 11 . . . . . . . . . . 11 (π‘₯ ∈ (-Ο€(,)0) β†’ -Ο€ ∈ ℝ*)
190131a1i 11 . . . . . . . . . . 11 (π‘₯ ∈ (-Ο€(,)0) β†’ Ο€ ∈ ℝ*)
19131, 72, 33, 77, 73lttrd 11323 . . . . . . . . . . 11 (π‘₯ ∈ (-Ο€(,)0) β†’ π‘₯ < Ο€)
192189, 190, 31, 63, 191eliood 43810 . . . . . . . . . 10 (π‘₯ ∈ (-Ο€(,)0) β†’ π‘₯ ∈ (-Ο€(,)Ο€))
193192, 29sylan2 594 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ (sinβ€˜(𝑁 Β· π‘₯)) ∈ β„‚)
194193mulm1d 11614 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ (-1 Β· (sinβ€˜(𝑁 Β· π‘₯))) = -(sinβ€˜(𝑁 Β· π‘₯)))
195188, 194eqtrd 2777 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (-Ο€(,)0)) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) = -(sinβ€˜(𝑁 Β· π‘₯)))
196195itgeq2dv 25162 . . . . . 6 (πœ‘ β†’ ∫(-Ο€(,)0)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ = ∫(-Ο€(,)0)-(sinβ€˜(𝑁 Β· π‘₯)) dπ‘₯)
197101, 127itgneg 25184 . . . . . 6 (πœ‘ β†’ -∫(-Ο€(,)0)(sinβ€˜(𝑁 Β· π‘₯)) dπ‘₯ = ∫(-Ο€(,)0)-(sinβ€˜(𝑁 Β· π‘₯)) dπ‘₯)
19824nnne0d 12210 . . . . . . . . . 10 (πœ‘ β†’ 𝑁 β‰  0)
1997a1i 11 . . . . . . . . . 10 (πœ‘ β†’ -Ο€ ≀ 0)
20025, 198, 3, 113, 199itgsincmulx 44289 . . . . . . . . 9 (πœ‘ β†’ ∫(-Ο€(,)0)(sinβ€˜(𝑁 Β· π‘₯)) dπ‘₯ = (((cosβ€˜(𝑁 Β· -Ο€)) βˆ’ (cosβ€˜(𝑁 Β· 0))) / 𝑁))
20124nnzd 12533 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ β„€)
202 cosknegpi 44184 . . . . . . . . . . . . 13 (𝑁 ∈ β„€ β†’ (cosβ€˜(𝑁 Β· -Ο€)) = if(2 βˆ₯ 𝑁, 1, -1))
203201, 202syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (cosβ€˜(𝑁 Β· -Ο€)) = if(2 βˆ₯ 𝑁, 1, -1))
20425mul01d 11361 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑁 Β· 0) = 0)
205204fveq2d 6851 . . . . . . . . . . . . 13 (πœ‘ β†’ (cosβ€˜(𝑁 Β· 0)) = (cosβ€˜0))
206 cos0 16039 . . . . . . . . . . . . 13 (cosβ€˜0) = 1
207205, 206eqtrdi 2793 . . . . . . . . . . . 12 (πœ‘ β†’ (cosβ€˜(𝑁 Β· 0)) = 1)
208203, 207oveq12d 7380 . . . . . . . . . . 11 (πœ‘ β†’ ((cosβ€˜(𝑁 Β· -Ο€)) βˆ’ (cosβ€˜(𝑁 Β· 0))) = (if(2 βˆ₯ 𝑁, 1, -1) βˆ’ 1))
209 1m1e0 12232 . . . . . . . . . . . . 13 (1 βˆ’ 1) = 0
210 iftrue 4497 . . . . . . . . . . . . . 14 (2 βˆ₯ 𝑁 β†’ if(2 βˆ₯ 𝑁, 1, -1) = 1)
211210oveq1d 7377 . . . . . . . . . . . . 13 (2 βˆ₯ 𝑁 β†’ (if(2 βˆ₯ 𝑁, 1, -1) βˆ’ 1) = (1 βˆ’ 1))
212 iftrue 4497 . . . . . . . . . . . . 13 (2 βˆ₯ 𝑁 β†’ if(2 βˆ₯ 𝑁, 0, -2) = 0)
213209, 211, 2123eqtr4a 2803 . . . . . . . . . . . 12 (2 βˆ₯ 𝑁 β†’ (if(2 βˆ₯ 𝑁, 1, -1) βˆ’ 1) = if(2 βˆ₯ 𝑁, 0, -2))
214 iffalse 4500 . . . . . . . . . . . . . 14 (Β¬ 2 βˆ₯ 𝑁 β†’ if(2 βˆ₯ 𝑁, 1, -1) = -1)
215214oveq1d 7377 . . . . . . . . . . . . 13 (Β¬ 2 βˆ₯ 𝑁 β†’ (if(2 βˆ₯ 𝑁, 1, -1) βˆ’ 1) = (-1 βˆ’ 1))
216 ax-1cn 11116 . . . . . . . . . . . . . . . 16 1 ∈ β„‚
217 negdi2 11466 . . . . . . . . . . . . . . . 16 ((1 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ -(1 + 1) = (-1 βˆ’ 1))
218216, 216, 217mp2an 691 . . . . . . . . . . . . . . 15 -(1 + 1) = (-1 βˆ’ 1)
219218eqcomi 2746 . . . . . . . . . . . . . 14 (-1 βˆ’ 1) = -(1 + 1)
220219a1i 11 . . . . . . . . . . . . 13 (Β¬ 2 βˆ₯ 𝑁 β†’ (-1 βˆ’ 1) = -(1 + 1))
221 1p1e2 12285 . . . . . . . . . . . . . . 15 (1 + 1) = 2
222221negeqi 11401 . . . . . . . . . . . . . 14 -(1 + 1) = -2
223 iffalse 4500 . . . . . . . . . . . . . 14 (Β¬ 2 βˆ₯ 𝑁 β†’ if(2 βˆ₯ 𝑁, 0, -2) = -2)
224222, 223eqtr4id 2796 . . . . . . . . . . . . 13 (Β¬ 2 βˆ₯ 𝑁 β†’ -(1 + 1) = if(2 βˆ₯ 𝑁, 0, -2))
225215, 220, 2243eqtrd 2781 . . . . . . . . . . . 12 (Β¬ 2 βˆ₯ 𝑁 β†’ (if(2 βˆ₯ 𝑁, 1, -1) βˆ’ 1) = if(2 βˆ₯ 𝑁, 0, -2))
226213, 225pm2.61i 182 . . . . . . . . . . 11 (if(2 βˆ₯ 𝑁, 1, -1) βˆ’ 1) = if(2 βˆ₯ 𝑁, 0, -2)
227208, 226eqtrdi 2793 . . . . . . . . . 10 (πœ‘ β†’ ((cosβ€˜(𝑁 Β· -Ο€)) βˆ’ (cosβ€˜(𝑁 Β· 0))) = if(2 βˆ₯ 𝑁, 0, -2))
228227oveq1d 7377 . . . . . . . . 9 (πœ‘ β†’ (((cosβ€˜(𝑁 Β· -Ο€)) βˆ’ (cosβ€˜(𝑁 Β· 0))) / 𝑁) = (if(2 βˆ₯ 𝑁, 0, -2) / 𝑁))
229200, 228eqtrd 2777 . . . . . . . 8 (πœ‘ β†’ ∫(-Ο€(,)0)(sinβ€˜(𝑁 Β· π‘₯)) dπ‘₯ = (if(2 βˆ₯ 𝑁, 0, -2) / 𝑁))
230229negeqd 11402 . . . . . . 7 (πœ‘ β†’ -∫(-Ο€(,)0)(sinβ€˜(𝑁 Β· π‘₯)) dπ‘₯ = -(if(2 βˆ₯ 𝑁, 0, -2) / 𝑁))
231 0cn 11154 . . . . . . . . . 10 0 ∈ β„‚
232 2cn 12235 . . . . . . . . . . 11 2 ∈ β„‚
233232negcli 11476 . . . . . . . . . 10 -2 ∈ β„‚
234231, 233ifcli 4538 . . . . . . . . 9 if(2 βˆ₯ 𝑁, 0, -2) ∈ β„‚
235234a1i 11 . . . . . . . 8 (πœ‘ β†’ if(2 βˆ₯ 𝑁, 0, -2) ∈ β„‚)
236235, 25, 198divnegd 11951 . . . . . . 7 (πœ‘ β†’ -(if(2 βˆ₯ 𝑁, 0, -2) / 𝑁) = (-if(2 βˆ₯ 𝑁, 0, -2) / 𝑁))
237 neg0 11454 . . . . . . . . . . 11 -0 = 0
238212negeqd 11402 . . . . . . . . . . 11 (2 βˆ₯ 𝑁 β†’ -if(2 βˆ₯ 𝑁, 0, -2) = -0)
239 iftrue 4497 . . . . . . . . . . 11 (2 βˆ₯ 𝑁 β†’ if(2 βˆ₯ 𝑁, 0, 2) = 0)
240237, 238, 2393eqtr4a 2803 . . . . . . . . . 10 (2 βˆ₯ 𝑁 β†’ -if(2 βˆ₯ 𝑁, 0, -2) = if(2 βˆ₯ 𝑁, 0, 2))
241232negnegi 11478 . . . . . . . . . . 11 --2 = 2
242223negeqd 11402 . . . . . . . . . . 11 (Β¬ 2 βˆ₯ 𝑁 β†’ -if(2 βˆ₯ 𝑁, 0, -2) = --2)
243 iffalse 4500 . . . . . . . . . . 11 (Β¬ 2 βˆ₯ 𝑁 β†’ if(2 βˆ₯ 𝑁, 0, 2) = 2)
244241, 242, 2433eqtr4a 2803 . . . . . . . . . 10 (Β¬ 2 βˆ₯ 𝑁 β†’ -if(2 βˆ₯ 𝑁, 0, -2) = if(2 βˆ₯ 𝑁, 0, 2))
245240, 244pm2.61i 182 . . . . . . . . 9 -if(2 βˆ₯ 𝑁, 0, -2) = if(2 βˆ₯ 𝑁, 0, 2)
246245oveq1i 7372 . . . . . . . 8 (-if(2 βˆ₯ 𝑁, 0, -2) / 𝑁) = (if(2 βˆ₯ 𝑁, 0, 2) / 𝑁)
247246a1i 11 . . . . . . 7 (πœ‘ β†’ (-if(2 βˆ₯ 𝑁, 0, -2) / 𝑁) = (if(2 βˆ₯ 𝑁, 0, 2) / 𝑁))
248230, 236, 2473eqtrd 2781 . . . . . 6 (πœ‘ β†’ -∫(-Ο€(,)0)(sinβ€˜(𝑁 Β· π‘₯)) dπ‘₯ = (if(2 βˆ₯ 𝑁, 0, 2) / 𝑁))
249196, 197, 2483eqtr2d 2783 . . . . 5 (πœ‘ β†’ ∫(-Ο€(,)0)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ = (if(2 βˆ₯ 𝑁, 0, 2) / 𝑁))
250133, 17, 19sylancl 587 . . . . . . . . . . 11 (π‘₯ ∈ (0(,)Ο€) β†’ (πΉβ€˜π‘₯) = if((π‘₯ mod 𝑇) < Ο€, 1, -1))
251250, 156eqtrd 2777 . . . . . . . . . 10 (π‘₯ ∈ (0(,)Ο€) β†’ (πΉβ€˜π‘₯) = 1)
252251oveq1d 7377 . . . . . . . . 9 (π‘₯ ∈ (0(,)Ο€) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) = (1 Β· (sinβ€˜(𝑁 Β· π‘₯))))
253252adantl 483 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (0(,)Ο€)) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) = (1 Β· (sinβ€˜(𝑁 Β· π‘₯))))
254253, 161eqtrd 2777 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (0(,)Ο€)) β†’ ((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) = (sinβ€˜(𝑁 Β· π‘₯)))
255254itgeq2dv 25162 . . . . . 6 (πœ‘ β†’ ∫(0(,)Ο€)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ = ∫(0(,)Ο€)(sinβ€˜(𝑁 Β· π‘₯)) dπ‘₯)
2569a1i 11 . . . . . . 7 (πœ‘ β†’ 0 ≀ Ο€)
25725, 198, 113, 4, 256itgsincmulx 44289 . . . . . 6 (πœ‘ β†’ ∫(0(,)Ο€)(sinβ€˜(𝑁 Β· π‘₯)) dπ‘₯ = (((cosβ€˜(𝑁 Β· 0)) βˆ’ (cosβ€˜(𝑁 Β· Ο€))) / 𝑁))
258 coskpi2 44181 . . . . . . . . . 10 (𝑁 ∈ β„€ β†’ (cosβ€˜(𝑁 Β· Ο€)) = if(2 βˆ₯ 𝑁, 1, -1))
259201, 258syl 17 . . . . . . . . 9 (πœ‘ β†’ (cosβ€˜(𝑁 Β· Ο€)) = if(2 βˆ₯ 𝑁, 1, -1))
260207, 259oveq12d 7380 . . . . . . . 8 (πœ‘ β†’ ((cosβ€˜(𝑁 Β· 0)) βˆ’ (cosβ€˜(𝑁 Β· Ο€))) = (1 βˆ’ if(2 βˆ₯ 𝑁, 1, -1)))
261210oveq2d 7378 . . . . . . . . . 10 (2 βˆ₯ 𝑁 β†’ (1 βˆ’ if(2 βˆ₯ 𝑁, 1, -1)) = (1 βˆ’ 1))
262209, 261, 2393eqtr4a 2803 . . . . . . . . 9 (2 βˆ₯ 𝑁 β†’ (1 βˆ’ if(2 βˆ₯ 𝑁, 1, -1)) = if(2 βˆ₯ 𝑁, 0, 2))
263214oveq2d 7378 . . . . . . . . . 10 (Β¬ 2 βˆ₯ 𝑁 β†’ (1 βˆ’ if(2 βˆ₯ 𝑁, 1, -1)) = (1 βˆ’ -1))
264216, 216subnegi 11487 . . . . . . . . . . 11 (1 βˆ’ -1) = (1 + 1)
265264a1i 11 . . . . . . . . . 10 (Β¬ 2 βˆ₯ 𝑁 β†’ (1 βˆ’ -1) = (1 + 1))
266221, 243eqtr4id 2796 . . . . . . . . . 10 (Β¬ 2 βˆ₯ 𝑁 β†’ (1 + 1) = if(2 βˆ₯ 𝑁, 0, 2))
267263, 265, 2663eqtrd 2781 . . . . . . . . 9 (Β¬ 2 βˆ₯ 𝑁 β†’ (1 βˆ’ if(2 βˆ₯ 𝑁, 1, -1)) = if(2 βˆ₯ 𝑁, 0, 2))
268262, 267pm2.61i 182 . . . . . . . 8 (1 βˆ’ if(2 βˆ₯ 𝑁, 1, -1)) = if(2 βˆ₯ 𝑁, 0, 2)
269260, 268eqtrdi 2793 . . . . . . 7 (πœ‘ β†’ ((cosβ€˜(𝑁 Β· 0)) βˆ’ (cosβ€˜(𝑁 Β· Ο€))) = if(2 βˆ₯ 𝑁, 0, 2))
270269oveq1d 7377 . . . . . 6 (πœ‘ β†’ (((cosβ€˜(𝑁 Β· 0)) βˆ’ (cosβ€˜(𝑁 Β· Ο€))) / 𝑁) = (if(2 βˆ₯ 𝑁, 0, 2) / 𝑁))
271255, 257, 2703eqtrd 2781 . . . . 5 (πœ‘ β†’ ∫(0(,)Ο€)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ = (if(2 βˆ₯ 𝑁, 0, 2) / 𝑁))
272249, 271oveq12d 7380 . . . 4 (πœ‘ β†’ (∫(-Ο€(,)0)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ + ∫(0(,)Ο€)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯) = ((if(2 βˆ₯ 𝑁, 0, 2) / 𝑁) + (if(2 βˆ₯ 𝑁, 0, 2) / 𝑁)))
273231, 232ifcli 4538 . . . . . 6 if(2 βˆ₯ 𝑁, 0, 2) ∈ β„‚
274273a1i 11 . . . . 5 (πœ‘ β†’ if(2 βˆ₯ 𝑁, 0, 2) ∈ β„‚)
275274, 274, 25, 198divdird 11976 . . . 4 (πœ‘ β†’ ((if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) / 𝑁) = ((if(2 βˆ₯ 𝑁, 0, 2) / 𝑁) + (if(2 βˆ₯ 𝑁, 0, 2) / 𝑁)))
276239, 239oveq12d 7380 . . . . . . . . 9 (2 βˆ₯ 𝑁 β†’ (if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) = (0 + 0))
277 00id 11337 . . . . . . . . 9 (0 + 0) = 0
278276, 277eqtrdi 2793 . . . . . . . 8 (2 βˆ₯ 𝑁 β†’ (if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) = 0)
279278oveq1d 7377 . . . . . . 7 (2 βˆ₯ 𝑁 β†’ ((if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) / 𝑁) = (0 / 𝑁))
280279adantl 483 . . . . . 6 ((πœ‘ ∧ 2 βˆ₯ 𝑁) β†’ ((if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) / 𝑁) = (0 / 𝑁))
28125, 198div0d 11937 . . . . . . 7 (πœ‘ β†’ (0 / 𝑁) = 0)
282281adantr 482 . . . . . 6 ((πœ‘ ∧ 2 βˆ₯ 𝑁) β†’ (0 / 𝑁) = 0)
283 iftrue 4497 . . . . . . . 8 (2 βˆ₯ 𝑁 β†’ if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)) = 0)
284283eqcomd 2743 . . . . . . 7 (2 βˆ₯ 𝑁 β†’ 0 = if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)))
285284adantl 483 . . . . . 6 ((πœ‘ ∧ 2 βˆ₯ 𝑁) β†’ 0 = if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)))
286280, 282, 2853eqtrd 2781 . . . . 5 ((πœ‘ ∧ 2 βˆ₯ 𝑁) β†’ ((if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) / 𝑁) = if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)))
287243, 243oveq12d 7380 . . . . . . . . 9 (Β¬ 2 βˆ₯ 𝑁 β†’ (if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) = (2 + 2))
288 2p2e4 12295 . . . . . . . . 9 (2 + 2) = 4
289287, 288eqtrdi 2793 . . . . . . . 8 (Β¬ 2 βˆ₯ 𝑁 β†’ (if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) = 4)
290289oveq1d 7377 . . . . . . 7 (Β¬ 2 βˆ₯ 𝑁 β†’ ((if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) / 𝑁) = (4 / 𝑁))
291 iffalse 4500 . . . . . . 7 (Β¬ 2 βˆ₯ 𝑁 β†’ if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)) = (4 / 𝑁))
292290, 291eqtr4d 2780 . . . . . 6 (Β¬ 2 βˆ₯ 𝑁 β†’ ((if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) / 𝑁) = if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)))
293292adantl 483 . . . . 5 ((πœ‘ ∧ Β¬ 2 βˆ₯ 𝑁) β†’ ((if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) / 𝑁) = if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)))
294286, 293pm2.61dan 812 . . . 4 (πœ‘ β†’ ((if(2 βˆ₯ 𝑁, 0, 2) + if(2 βˆ₯ 𝑁, 0, 2)) / 𝑁) = if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)))
295272, 275, 2943eqtr2d 2783 . . 3 (πœ‘ β†’ (∫(-Ο€(,)0)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ + ∫(0(,)Ο€)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯) = if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)))
296295oveq1d 7377 . 2 (πœ‘ β†’ ((∫(-Ο€(,)0)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ + ∫(0(,)Ο€)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯) / Ο€) = (if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)) / Ο€))
297283oveq1d 7377 . . . . 5 (2 βˆ₯ 𝑁 β†’ (if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)) / Ο€) = (0 / Ο€))
298297adantl 483 . . . 4 ((πœ‘ ∧ 2 βˆ₯ 𝑁) β†’ (if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)) / Ο€) = (0 / Ο€))
2995, 8gtneii 11274 . . . . . 6 Ο€ β‰  0
30042, 299div0i 11896 . . . . 5 (0 / Ο€) = 0
301300a1i 11 . . . 4 ((πœ‘ ∧ 2 βˆ₯ 𝑁) β†’ (0 / Ο€) = 0)
302 iftrue 4497 . . . . . 6 (2 βˆ₯ 𝑁 β†’ if(2 βˆ₯ 𝑁, 0, (4 / (𝑁 Β· Ο€))) = 0)
303302eqcomd 2743 . . . . 5 (2 βˆ₯ 𝑁 β†’ 0 = if(2 βˆ₯ 𝑁, 0, (4 / (𝑁 Β· Ο€))))
304303adantl 483 . . . 4 ((πœ‘ ∧ 2 βˆ₯ 𝑁) β†’ 0 = if(2 βˆ₯ 𝑁, 0, (4 / (𝑁 Β· Ο€))))
305298, 301, 3043eqtrd 2781 . . 3 ((πœ‘ ∧ 2 βˆ₯ 𝑁) β†’ (if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)) / Ο€) = if(2 βˆ₯ 𝑁, 0, (4 / (𝑁 Β· Ο€))))
306291oveq1d 7377 . . . . 5 (Β¬ 2 βˆ₯ 𝑁 β†’ (if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)) / Ο€) = ((4 / 𝑁) / Ο€))
307306adantl 483 . . . 4 ((πœ‘ ∧ Β¬ 2 βˆ₯ 𝑁) β†’ (if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)) / Ο€) = ((4 / 𝑁) / Ο€))
308 4cn 12245 . . . . . . 7 4 ∈ β„‚
309308a1i 11 . . . . . 6 (πœ‘ β†’ 4 ∈ β„‚)
31042a1i 11 . . . . . 6 (πœ‘ β†’ Ο€ ∈ β„‚)
311299a1i 11 . . . . . 6 (πœ‘ β†’ Ο€ β‰  0)
312309, 25, 310, 198, 311divdiv1d 11969 . . . . 5 (πœ‘ β†’ ((4 / 𝑁) / Ο€) = (4 / (𝑁 Β· Ο€)))
313312adantr 482 . . . 4 ((πœ‘ ∧ Β¬ 2 βˆ₯ 𝑁) β†’ ((4 / 𝑁) / Ο€) = (4 / (𝑁 Β· Ο€)))
314 iffalse 4500 . . . . . 6 (Β¬ 2 βˆ₯ 𝑁 β†’ if(2 βˆ₯ 𝑁, 0, (4 / (𝑁 Β· Ο€))) = (4 / (𝑁 Β· Ο€)))
315314eqcomd 2743 . . . . 5 (Β¬ 2 βˆ₯ 𝑁 β†’ (4 / (𝑁 Β· Ο€)) = if(2 βˆ₯ 𝑁, 0, (4 / (𝑁 Β· Ο€))))
316315adantl 483 . . . 4 ((πœ‘ ∧ Β¬ 2 βˆ₯ 𝑁) β†’ (4 / (𝑁 Β· Ο€)) = if(2 βˆ₯ 𝑁, 0, (4 / (𝑁 Β· Ο€))))
317307, 313, 3163eqtrd 2781 . . 3 ((πœ‘ ∧ Β¬ 2 βˆ₯ 𝑁) β†’ (if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)) / Ο€) = if(2 βˆ₯ 𝑁, 0, (4 / (𝑁 Β· Ο€))))
318305, 317pm2.61dan 812 . 2 (πœ‘ β†’ (if(2 βˆ₯ 𝑁, 0, (4 / 𝑁)) / Ο€) = if(2 βˆ₯ 𝑁, 0, (4 / (𝑁 Β· Ο€))))
319186, 296, 3183eqtrd 2781 1 (πœ‘ β†’ (∫(-Ο€(,)Ο€)((πΉβ€˜π‘₯) Β· (sinβ€˜(𝑁 Β· π‘₯))) dπ‘₯ / Ο€) = if(2 βˆ₯ 𝑁, 0, (4 / (𝑁 Β· Ο€))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2944   βŠ† wss 3915  ifcif 4491   class class class wbr 5110   ↦ cmpt 5193  dom cdm 5638  β€˜cfv 6501  (class class class)co 7362  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  β„*cxr 11195   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  -cneg 11393   / cdiv 11819  β„•cn 12160  2c2 12215  4c4 12217  β„€cz 12506  β„+crp 12922  (,)cioo 13271  [,]cicc 13274   mod cmo 13781  sincsin 15953  cosccos 15954  Ο€cpi 15956   βˆ₯ cdvds 16143  β€“cnβ†’ccncf 24255  volcvol 24843  πΏ1cibl 24997  βˆ«citg 24998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cc 10378  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-symdif 4207  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-disj 5076  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-ofr 7623  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-omul 8422  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-acn 9885  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-sin 15959  df-cos 15960  df-pi 15962  df-dvds 16144  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-ovol 24844  df-vol 24845  df-mbf 24999  df-itg1 25000  df-itg2 25001  df-ibl 25002  df-itg 25003  df-0p 25050  df-limc 25246  df-dv 25247
This theorem is referenced by:  fouriersw  44546
  Copyright terms: Public domain W3C validator