This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sqwvfourb

Description: Fourier series B coefficients for the square wave function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses sqwvfourb.t ⊢ 𝑇 = ( 2 · π )
sqwvfourb.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
sqwvfourb.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion sqwvfourb ( 𝜑 → ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 / π ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) )

Proof

Step Hyp Ref Expression
1 sqwvfourb.t ⊢ 𝑇 = ( 2 · π )
2 sqwvfourb.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
3 sqwvfourb.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 pire ⊢ π ∈ ℝ
5 4 renegcli ⊢ - π ∈ ℝ
6 5 a1i ⊢ ( 𝜑 → - π ∈ ℝ )
7 4 a1i ⊢ ( 𝜑 → π ∈ ℝ )
8 0re ⊢ 0 ∈ ℝ
9 negpilt0 ⊢ - π < 0
10 5 8 9 ltleii ⊢ - π ≤ 0
11 pipos ⊢ 0 < π
12 8 4 11 ltleii ⊢ 0 ≤ π
13 5 4 elicc2i ⊢ ( 0 ∈ ( - π [,] π ) ↔ ( 0 ∈ ℝ ∧ - π ≤ 0 ∧ 0 ≤ π ) )
14 8 10 12 13 mpbir3an ⊢ 0 ∈ ( - π [,] π )
15 14 a1i ⊢ ( 𝜑 → 0 ∈ ( - π [,] π ) )
16 elioore ⊢ ( 𝑥 ∈ ( - π (,) π ) → 𝑥 ∈ ℝ )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → 𝑥 ∈ ℝ )
18 1re ⊢ 1 ∈ ℝ
19 18 renegcli ⊢ - 1 ∈ ℝ
20 18 19 ifcli ⊢ if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) ∈ ℝ
21 2 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
22 17 20 21 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( 𝐹 ‘ 𝑥 ) = if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
23 20 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) ∈ ℝ )
24 23 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) ∈ ℂ )
25 22 24 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
26 3 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → 𝑁 ∈ ℂ )
28 17 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → 𝑥 ∈ ℂ )
29 27 28 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( 𝑁 · 𝑥 ) ∈ ℂ )
30 29 sincld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( sin ‘ ( 𝑁 · 𝑥 ) ) ∈ ℂ )
31 25 30 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ℂ )
32 elioore ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑥 ∈ ℝ )
33 32 20 21 sylancl ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝐹 ‘ 𝑥 ) = if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
34 4 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → π ∈ ℝ )
35 2rp ⊢ 2 ∈ ℝ+
36 pirp ⊢ π ∈ ℝ+
37 rpmulcl ⊢ ( ( 2 ∈ ℝ+ ∧ π ∈ ℝ+ ) → ( 2 · π ) ∈ ℝ+ )
38 35 36 37 mp2an ⊢ ( 2 · π ) ∈ ℝ+
39 1 38 eqeltri ⊢ 𝑇 ∈ ℝ+
40 39 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑇 ∈ ℝ+ )
41 32 40 modcld ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝑥 mod 𝑇 ) ∈ ℝ )
42 picn ⊢ π ∈ ℂ
43 42 2timesi ⊢ ( 2 · π ) = ( π + π )
44 1 43 eqtri ⊢ 𝑇 = ( π + π )
45 44 oveq2i ⊢ ( - π + 𝑇 ) = ( - π + ( π + π ) )
46 5 recni ⊢ - π ∈ ℂ
47 46 42 42 addassi ⊢ ( ( - π + π ) + π ) = ( - π + ( π + π ) )
48 42 negidi ⊢ ( π + - π ) = 0
49 42 46 48 addcomli ⊢ ( - π + π ) = 0
50 49 oveq1i ⊢ ( ( - π + π ) + π ) = ( 0 + π )
51 42 addlidi ⊢ ( 0 + π ) = π
52 50 51 eqtri ⊢ ( ( - π + π ) + π ) = π
53 45 47 52 3eqtr2ri ⊢ π = ( - π + 𝑇 )
54 53 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → π = ( - π + 𝑇 ) )
55 5 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → - π ∈ ℝ )
56 2re ⊢ 2 ∈ ℝ
57 56 4 remulcli ⊢ ( 2 · π ) ∈ ℝ
58 1 57 eqeltri ⊢ 𝑇 ∈ ℝ
59 58 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑇 ∈ ℝ )
60 5 rexri ⊢ - π ∈ ℝ*
61 0xr ⊢ 0 ∈ ℝ*
62 ioogtlb ⊢ ( ( - π ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑥 ∈ ( - π (,) 0 ) ) → - π < 𝑥 )
63 60 61 62 mp3an12 ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → - π < 𝑥 )
64 55 32 59 63 ltadd1dd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( - π + 𝑇 ) < ( 𝑥 + 𝑇 ) )
65 54 64 eqbrtrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → π < ( 𝑥 + 𝑇 ) )
66 58 recni ⊢ 𝑇 ∈ ℂ
67 66 mullidi ⊢ ( 1 · 𝑇 ) = 𝑇
68 67 eqcomi ⊢ 𝑇 = ( 1 · 𝑇 )
69 68 oveq2i ⊢ ( 𝑥 + 𝑇 ) = ( 𝑥 + ( 1 · 𝑇 ) )
70 69 oveq1i ⊢ ( ( 𝑥 + 𝑇 ) mod 𝑇 ) = ( ( 𝑥 + ( 1 · 𝑇 ) ) mod 𝑇 )
71 32 59 readdcld ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝑥 + 𝑇 ) ∈ ℝ )
72 0red ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 0 ∈ ℝ )
73 11 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 0 < π )
74 72 34 71 73 65 lttrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 0 < ( 𝑥 + 𝑇 ) )
75 72 71 74 ltled ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 0 ≤ ( 𝑥 + 𝑇 ) )
76 iooltub ⊢ ( ( - π ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑥 ∈ ( - π (,) 0 ) ) → 𝑥 < 0 )
77 60 61 76 mp3an12 ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑥 < 0 )
78 32 72 59 77 ltadd1dd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝑥 + 𝑇 ) < ( 0 + 𝑇 ) )
79 59 recnd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑇 ∈ ℂ )
80 79 addlidd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 0 + 𝑇 ) = 𝑇 )
81 78 80 breqtrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝑥 + 𝑇 ) < 𝑇 )
82 modid ⊢ ( ( ( ( 𝑥 + 𝑇 ) ∈ ℝ ∧ 𝑇 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑥 + 𝑇 ) ∧ ( 𝑥 + 𝑇 ) < 𝑇 ) ) → ( ( 𝑥 + 𝑇 ) mod 𝑇 ) = ( 𝑥 + 𝑇 ) )
83 71 40 75 81 82 syl22anc ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( ( 𝑥 + 𝑇 ) mod 𝑇 ) = ( 𝑥 + 𝑇 ) )
84 1zzd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 1 ∈ ℤ )
85 modcyc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ∧ 1 ∈ ℤ ) → ( ( 𝑥 + ( 1 · 𝑇 ) ) mod 𝑇 ) = ( 𝑥 mod 𝑇 ) )
86 32 40 84 85 syl3anc ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( ( 𝑥 + ( 1 · 𝑇 ) ) mod 𝑇 ) = ( 𝑥 mod 𝑇 ) )
87 70 83 86 3eqtr3a ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝑥 + 𝑇 ) = ( 𝑥 mod 𝑇 ) )
88 65 87 breqtrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → π < ( 𝑥 mod 𝑇 ) )
89 34 41 88 ltnsymd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ¬ ( 𝑥 mod 𝑇 ) < π )
90 89 iffalsed ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) = - 1 )
91 33 90 eqtrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝐹 ‘ 𝑥 ) = - 1 )
92 91 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( 𝐹 ‘ 𝑥 ) = - 1 )
93 92 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = ( - 1 · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) )
94 93 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π (,) 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ( - π (,) 0 ) ↦ ( - 1 · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) )
95 neg1cn ⊢ - 1 ∈ ℂ
96 95 a1i ⊢ ( 𝜑 → - 1 ∈ ℂ )
97 3 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → 𝑁 ∈ ℝ )
99 32 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → 𝑥 ∈ ℝ )
100 98 99 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( 𝑁 · 𝑥 ) ∈ ℝ )
101 100 resincld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( sin ‘ ( 𝑁 · 𝑥 ) ) ∈ ℝ )
102 ioossicc ⊢ ( - π (,) 0 ) ⊆ ( - π [,] 0 )
103 102 a1i ⊢ ( 𝜑 → ( - π (,) 0 ) ⊆ ( - π [,] 0 ) )
104 ioombl ⊢ ( - π (,) 0 ) ∈ dom vol
105 104 a1i ⊢ ( 𝜑 → ( - π (,) 0 ) ∈ dom vol )
106 97 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] 0 ) ) → 𝑁 ∈ ℝ )
107 iccssre ⊢ ( ( - π ∈ ℝ ∧ 0 ∈ ℝ ) → ( - π [,] 0 ) ⊆ ℝ )
108 5 8 107 mp2an ⊢ ( - π [,] 0 ) ⊆ ℝ
109 108 sseli ⊢ ( 𝑥 ∈ ( - π [,] 0 ) → 𝑥 ∈ ℝ )
110 109 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] 0 ) ) → 𝑥 ∈ ℝ )
111 106 110 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] 0 ) ) → ( 𝑁 · 𝑥 ) ∈ ℝ )
112 111 resincld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] 0 ) ) → ( sin ‘ ( 𝑁 · 𝑥 ) ) ∈ ℝ )
113 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
114 sincn ⊢ sin ∈ ( ℂ –cn→ ℂ )
115 114 a1i ⊢ ( 𝜑 → sin ∈ ( ℂ –cn→ ℂ ) )
116 ax-resscn ⊢ ℝ ⊆ ℂ
117 108 116 sstri ⊢ ( - π [,] 0 ) ⊆ ℂ
118 117 a1i ⊢ ( 𝜑 → ( - π [,] 0 ) ⊆ ℂ )
119 ssid ⊢ ℂ ⊆ ℂ
120 119 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
121 118 26 120 constcncfg ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] 0 ) ↦ 𝑁 ) ∈ ( ( - π [,] 0 ) –cn→ ℂ ) )
122 118 120 idcncfg ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] 0 ) ↦ 𝑥 ) ∈ ( ( - π [,] 0 ) –cn→ ℂ ) )
123 121 122 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] 0 ) ↦ ( 𝑁 · 𝑥 ) ) ∈ ( ( - π [,] 0 ) –cn→ ℂ ) )
124 115 123 cncfmpt1f ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] 0 ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ( ( - π [,] 0 ) –cn→ ℂ ) )
125 cniccibl ⊢ ( ( - π ∈ ℝ ∧ 0 ∈ ℝ ∧ ( 𝑥 ∈ ( - π [,] 0 ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ( ( - π [,] 0 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( - π [,] 0 ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
126 6 113 124 125 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] 0 ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
127 103 105 112 126 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π (,) 0 ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
128 96 101 127 iblmulc2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π (,) 0 ) ↦ ( - 1 · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 )
129 94 128 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π (,) 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 )
130 60 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → - π ∈ ℝ* )
131 4 rexri ⊢ π ∈ ℝ*
132 131 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → π ∈ ℝ* )
133 elioore ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 ∈ ℝ )
134 5 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → - π ∈ ℝ )
135 0red ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 0 ∈ ℝ )
136 9 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → - π < 0 )
137 ioogtlb ⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑥 ∈ ( 0 (,) π ) ) → 0 < 𝑥 )
138 61 131 137 mp3an12 ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 0 < 𝑥 )
139 134 135 133 136 138 lttrd ⊢ ( 𝑥 ∈ ( 0 (,) π ) → - π < 𝑥 )
140 iooltub ⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑥 ∈ ( 0 (,) π ) ) → 𝑥 < π )
141 61 131 140 mp3an12 ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 < π )
142 130 132 133 139 141 eliood ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 ∈ ( - π (,) π ) )
143 142 22 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( 𝐹 ‘ 𝑥 ) = if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
144 39 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑇 ∈ ℝ+ )
145 135 133 138 ltled ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 0 ≤ 𝑥 )
146 4 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → π ∈ ℝ )
147 58 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑇 ∈ ℝ )
148 2timesgt ⊢ ( π ∈ ℝ+ → π < ( 2 · π ) )
149 36 148 ax-mp ⊢ π < ( 2 · π )
150 149 1 breqtrri ⊢ π < 𝑇
151 150 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → π < 𝑇 )
152 133 146 147 141 151 lttrd ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 < 𝑇 )
153 modid ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 < 𝑇 ) ) → ( 𝑥 mod 𝑇 ) = 𝑥 )
154 133 144 145 152 153 syl22anc ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( 𝑥 mod 𝑇 ) = 𝑥 )
155 154 141 eqbrtrd ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( 𝑥 mod 𝑇 ) < π )
156 155 iftrued ⊢ ( 𝑥 ∈ ( 0 (,) π ) → if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) = 1 )
157 156 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) = 1 )
158 143 157 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( 𝐹 ‘ 𝑥 ) = 1 )
159 158 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = ( 1 · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) )
160 142 30 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( sin ‘ ( 𝑁 · 𝑥 ) ) ∈ ℂ )
161 160 mullidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( 1 · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = ( sin ‘ ( 𝑁 · 𝑥 ) ) )
162 159 161 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = ( sin ‘ ( 𝑁 · 𝑥 ) ) )
163 162 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 0 (,) π ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) )
164 ioossicc ⊢ ( 0 (,) π ) ⊆ ( 0 [,] π )
165 164 a1i ⊢ ( 𝜑 → ( 0 (,) π ) ⊆ ( 0 [,] π ) )
166 ioombl ⊢ ( 0 (,) π ) ∈ dom vol
167 166 a1i ⊢ ( 𝜑 → ( 0 (,) π ) ∈ dom vol )
168 97 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] π ) ) → 𝑁 ∈ ℝ )
169 iccssre ⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ) → ( 0 [,] π ) ⊆ ℝ )
170 8 4 169 mp2an ⊢ ( 0 [,] π ) ⊆ ℝ
171 170 sseli ⊢ ( 𝑥 ∈ ( 0 [,] π ) → 𝑥 ∈ ℝ )
172 171 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] π ) ) → 𝑥 ∈ ℝ )
173 168 172 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] π ) ) → ( 𝑁 · 𝑥 ) ∈ ℝ )
174 173 resincld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] π ) ) → ( sin ‘ ( 𝑁 · 𝑥 ) ) ∈ ℝ )
175 170 116 sstri ⊢ ( 0 [,] π ) ⊆ ℂ
176 175 a1i ⊢ ( 𝜑 → ( 0 [,] π ) ⊆ ℂ )
177 176 26 120 constcncfg ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] π ) ↦ 𝑁 ) ∈ ( ( 0 [,] π ) –cn→ ℂ ) )
178 176 120 idcncfg ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] π ) ↦ 𝑥 ) ∈ ( ( 0 [,] π ) –cn→ ℂ ) )
179 177 178 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] π ) ↦ ( 𝑁 · 𝑥 ) ) ∈ ( ( 0 [,] π ) –cn→ ℂ ) )
180 115 179 cncfmpt1f ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] π ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ( ( 0 [,] π ) –cn→ ℂ ) )
181 cniccibl ⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ∧ ( 𝑥 ∈ ( 0 [,] π ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ( ( 0 [,] π ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 0 [,] π ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
182 113 7 180 181 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] π ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
183 165 167 174 182 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
184 163 183 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 )
185 6 7 15 31 129 184 itgsplitioo ⊢ ( 𝜑 → ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 = ( ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 + ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ) )
186 185 oveq1d ⊢ ( 𝜑 → ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 / π ) = ( ( ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 + ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ) / π ) )
187 91 oveq1d ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = ( - 1 · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) )
188 187 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = ( - 1 · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) )
189 60 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → - π ∈ ℝ* )
190 131 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → π ∈ ℝ* )
191 32 72 34 77 73 lttrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑥 < π )
192 189 190 32 63 191 eliood ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑥 ∈ ( - π (,) π ) )
193 192 30 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( sin ‘ ( 𝑁 · 𝑥 ) ) ∈ ℂ )
194 193 mulm1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( - 1 · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = - ( sin ‘ ( 𝑁 · 𝑥 ) ) )
195 188 194 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = - ( sin ‘ ( 𝑁 · 𝑥 ) ) )
196 195 itgeq2dv ⊢ ( 𝜑 → ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 = ∫ ( - π (,) 0 ) - ( sin ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 )
197 101 127 itgneg ⊢ ( 𝜑 → - ∫ ( - π (,) 0 ) ( sin ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = ∫ ( - π (,) 0 ) - ( sin ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 )
198 3 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
199 10 a1i ⊢ ( 𝜑 → - π ≤ 0 )
200 26 198 6 113 199 itgsincmulx ⊢ ( 𝜑 → ∫ ( - π (,) 0 ) ( sin ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = ( ( ( cos ‘ ( 𝑁 · - π ) ) − ( cos ‘ ( 𝑁 · 0 ) ) ) / 𝑁 ) )
201 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
202 cosknegpi ⊢ ( 𝑁 ∈ ℤ → ( cos ‘ ( 𝑁 · - π ) ) = if ( 2 ∥ 𝑁 , 1 , - 1 ) )
203 201 202 syl ⊢ ( 𝜑 → ( cos ‘ ( 𝑁 · - π ) ) = if ( 2 ∥ 𝑁 , 1 , - 1 ) )
204 26 mul01d ⊢ ( 𝜑 → ( 𝑁 · 0 ) = 0 )
205 204 fveq2d ⊢ ( 𝜑 → ( cos ‘ ( 𝑁 · 0 ) ) = ( cos ‘ 0 ) )
206 cos0 ⊢ ( cos ‘ 0 ) = 1
207 205 206 eqtrdi ⊢ ( 𝜑 → ( cos ‘ ( 𝑁 · 0 ) ) = 1 )
208 203 207 oveq12d ⊢ ( 𝜑 → ( ( cos ‘ ( 𝑁 · - π ) ) − ( cos ‘ ( 𝑁 · 0 ) ) ) = ( if ( 2 ∥ 𝑁 , 1 , - 1 ) − 1 ) )
209 1m1e0 ⊢ ( 1 − 1 ) = 0
210 iftrue ⊢ ( 2 ∥ 𝑁 → if ( 2 ∥ 𝑁 , 1 , - 1 ) = 1 )
211 210 oveq1d ⊢ ( 2 ∥ 𝑁 → ( if ( 2 ∥ 𝑁 , 1 , - 1 ) − 1 ) = ( 1 − 1 ) )
212 iftrue ⊢ ( 2 ∥ 𝑁 → if ( 2 ∥ 𝑁 , 0 , - 2 ) = 0 )
213 209 211 212 3eqtr4a ⊢ ( 2 ∥ 𝑁 → ( if ( 2 ∥ 𝑁 , 1 , - 1 ) − 1 ) = if ( 2 ∥ 𝑁 , 0 , - 2 ) )
214 iffalse ⊢ ( ¬ 2 ∥ 𝑁 → if ( 2 ∥ 𝑁 , 1 , - 1 ) = - 1 )
215 214 oveq1d ⊢ ( ¬ 2 ∥ 𝑁 → ( if ( 2 ∥ 𝑁 , 1 , - 1 ) − 1 ) = ( - 1 − 1 ) )
216 ax-1cn ⊢ 1 ∈ ℂ
217 negdi2 ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( 1 + 1 ) = ( - 1 − 1 ) )
218 216 216 217 mp2an ⊢ - ( 1 + 1 ) = ( - 1 − 1 )
219 218 eqcomi ⊢ ( - 1 − 1 ) = - ( 1 + 1 )
220 219 a1i ⊢ ( ¬ 2 ∥ 𝑁 → ( - 1 − 1 ) = - ( 1 + 1 ) )
221 1p1e2 ⊢ ( 1 + 1 ) = 2
222 221 negeqi ⊢ - ( 1 + 1 ) = - 2
223 iffalse ⊢ ( ¬ 2 ∥ 𝑁 → if ( 2 ∥ 𝑁 , 0 , - 2 ) = - 2 )
224 222 223 eqtr4id ⊢ ( ¬ 2 ∥ 𝑁 → - ( 1 + 1 ) = if ( 2 ∥ 𝑁 , 0 , - 2 ) )
225 215 220 224 3eqtrd ⊢ ( ¬ 2 ∥ 𝑁 → ( if ( 2 ∥ 𝑁 , 1 , - 1 ) − 1 ) = if ( 2 ∥ 𝑁 , 0 , - 2 ) )
226 213 225 pm2.61i ⊢ ( if ( 2 ∥ 𝑁 , 1 , - 1 ) − 1 ) = if ( 2 ∥ 𝑁 , 0 , - 2 )
227 208 226 eqtrdi ⊢ ( 𝜑 → ( ( cos ‘ ( 𝑁 · - π ) ) − ( cos ‘ ( 𝑁 · 0 ) ) ) = if ( 2 ∥ 𝑁 , 0 , - 2 ) )
228 227 oveq1d ⊢ ( 𝜑 → ( ( ( cos ‘ ( 𝑁 · - π ) ) − ( cos ‘ ( 𝑁 · 0 ) ) ) / 𝑁 ) = ( if ( 2 ∥ 𝑁 , 0 , - 2 ) / 𝑁 ) )
229 200 228 eqtrd ⊢ ( 𝜑 → ∫ ( - π (,) 0 ) ( sin ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = ( if ( 2 ∥ 𝑁 , 0 , - 2 ) / 𝑁 ) )
230 229 negeqd ⊢ ( 𝜑 → - ∫ ( - π (,) 0 ) ( sin ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = - ( if ( 2 ∥ 𝑁 , 0 , - 2 ) / 𝑁 ) )
231 0cn ⊢ 0 ∈ ℂ
232 2cn ⊢ 2 ∈ ℂ
233 232 negcli ⊢ - 2 ∈ ℂ
234 231 233 ifcli ⊢ if ( 2 ∥ 𝑁 , 0 , - 2 ) ∈ ℂ
235 234 a1i ⊢ ( 𝜑 → if ( 2 ∥ 𝑁 , 0 , - 2 ) ∈ ℂ )
236 235 26 198 divnegd ⊢ ( 𝜑 → - ( if ( 2 ∥ 𝑁 , 0 , - 2 ) / 𝑁 ) = ( - if ( 2 ∥ 𝑁 , 0 , - 2 ) / 𝑁 ) )
237 neg0 ⊢ - 0 = 0
238 212 negeqd ⊢ ( 2 ∥ 𝑁 → - if ( 2 ∥ 𝑁 , 0 , - 2 ) = - 0 )
239 iftrue ⊢ ( 2 ∥ 𝑁 → if ( 2 ∥ 𝑁 , 0 , 2 ) = 0 )
240 237 238 239 3eqtr4a ⊢ ( 2 ∥ 𝑁 → - if ( 2 ∥ 𝑁 , 0 , - 2 ) = if ( 2 ∥ 𝑁 , 0 , 2 ) )
241 232 negnegi ⊢ - - 2 = 2
242 223 negeqd ⊢ ( ¬ 2 ∥ 𝑁 → - if ( 2 ∥ 𝑁 , 0 , - 2 ) = - - 2 )
243 iffalse ⊢ ( ¬ 2 ∥ 𝑁 → if ( 2 ∥ 𝑁 , 0 , 2 ) = 2 )
244 241 242 243 3eqtr4a ⊢ ( ¬ 2 ∥ 𝑁 → - if ( 2 ∥ 𝑁 , 0 , - 2 ) = if ( 2 ∥ 𝑁 , 0 , 2 ) )
245 240 244 pm2.61i ⊢ - if ( 2 ∥ 𝑁 , 0 , - 2 ) = if ( 2 ∥ 𝑁 , 0 , 2 )
246 245 oveq1i ⊢ ( - if ( 2 ∥ 𝑁 , 0 , - 2 ) / 𝑁 ) = ( if ( 2 ∥ 𝑁 , 0 , 2 ) / 𝑁 )
247 246 a1i ⊢ ( 𝜑 → ( - if ( 2 ∥ 𝑁 , 0 , - 2 ) / 𝑁 ) = ( if ( 2 ∥ 𝑁 , 0 , 2 ) / 𝑁 ) )
248 230 236 247 3eqtrd ⊢ ( 𝜑 → - ∫ ( - π (,) 0 ) ( sin ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = ( if ( 2 ∥ 𝑁 , 0 , 2 ) / 𝑁 ) )
249 196 197 248 3eqtr2d ⊢ ( 𝜑 → ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 = ( if ( 2 ∥ 𝑁 , 0 , 2 ) / 𝑁 ) )
250 133 20 21 sylancl ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( 𝐹 ‘ 𝑥 ) = if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
251 250 156 eqtrd ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( 𝐹 ‘ 𝑥 ) = 1 )
252 251 oveq1d ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = ( 1 · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) )
253 252 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = ( 1 · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) )
254 253 161 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) = ( sin ‘ ( 𝑁 · 𝑥 ) ) )
255 254 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 = ∫ ( 0 (,) π ) ( sin ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 )
256 12 a1i ⊢ ( 𝜑 → 0 ≤ π )
257 26 198 113 7 256 itgsincmulx ⊢ ( 𝜑 → ∫ ( 0 (,) π ) ( sin ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = ( ( ( cos ‘ ( 𝑁 · 0 ) ) − ( cos ‘ ( 𝑁 · π ) ) ) / 𝑁 ) )
258 coskpi2 ⊢ ( 𝑁 ∈ ℤ → ( cos ‘ ( 𝑁 · π ) ) = if ( 2 ∥ 𝑁 , 1 , - 1 ) )
259 201 258 syl ⊢ ( 𝜑 → ( cos ‘ ( 𝑁 · π ) ) = if ( 2 ∥ 𝑁 , 1 , - 1 ) )
260 207 259 oveq12d ⊢ ( 𝜑 → ( ( cos ‘ ( 𝑁 · 0 ) ) − ( cos ‘ ( 𝑁 · π ) ) ) = ( 1 − if ( 2 ∥ 𝑁 , 1 , - 1 ) ) )
261 210 oveq2d ⊢ ( 2 ∥ 𝑁 → ( 1 − if ( 2 ∥ 𝑁 , 1 , - 1 ) ) = ( 1 − 1 ) )
262 209 261 239 3eqtr4a ⊢ ( 2 ∥ 𝑁 → ( 1 − if ( 2 ∥ 𝑁 , 1 , - 1 ) ) = if ( 2 ∥ 𝑁 , 0 , 2 ) )
263 214 oveq2d ⊢ ( ¬ 2 ∥ 𝑁 → ( 1 − if ( 2 ∥ 𝑁 , 1 , - 1 ) ) = ( 1 − - 1 ) )
264 216 216 subnegi ⊢ ( 1 − - 1 ) = ( 1 + 1 )
265 264 a1i ⊢ ( ¬ 2 ∥ 𝑁 → ( 1 − - 1 ) = ( 1 + 1 ) )
266 221 243 eqtr4id ⊢ ( ¬ 2 ∥ 𝑁 → ( 1 + 1 ) = if ( 2 ∥ 𝑁 , 0 , 2 ) )
267 263 265 266 3eqtrd ⊢ ( ¬ 2 ∥ 𝑁 → ( 1 − if ( 2 ∥ 𝑁 , 1 , - 1 ) ) = if ( 2 ∥ 𝑁 , 0 , 2 ) )
268 262 267 pm2.61i ⊢ ( 1 − if ( 2 ∥ 𝑁 , 1 , - 1 ) ) = if ( 2 ∥ 𝑁 , 0 , 2 )
269 260 268 eqtrdi ⊢ ( 𝜑 → ( ( cos ‘ ( 𝑁 · 0 ) ) − ( cos ‘ ( 𝑁 · π ) ) ) = if ( 2 ∥ 𝑁 , 0 , 2 ) )
270 269 oveq1d ⊢ ( 𝜑 → ( ( ( cos ‘ ( 𝑁 · 0 ) ) − ( cos ‘ ( 𝑁 · π ) ) ) / 𝑁 ) = ( if ( 2 ∥ 𝑁 , 0 , 2 ) / 𝑁 ) )
271 255 257 270 3eqtrd ⊢ ( 𝜑 → ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 = ( if ( 2 ∥ 𝑁 , 0 , 2 ) / 𝑁 ) )
272 249 271 oveq12d ⊢ ( 𝜑 → ( ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 + ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ) = ( ( if ( 2 ∥ 𝑁 , 0 , 2 ) / 𝑁 ) + ( if ( 2 ∥ 𝑁 , 0 , 2 ) / 𝑁 ) ) )
273 231 232 ifcli ⊢ if ( 2 ∥ 𝑁 , 0 , 2 ) ∈ ℂ
274 273 a1i ⊢ ( 𝜑 → if ( 2 ∥ 𝑁 , 0 , 2 ) ∈ ℂ )
275 274 274 26 198 divdird ⊢ ( 𝜑 → ( ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) / 𝑁 ) = ( ( if ( 2 ∥ 𝑁 , 0 , 2 ) / 𝑁 ) + ( if ( 2 ∥ 𝑁 , 0 , 2 ) / 𝑁 ) ) )
276 239 239 oveq12d ⊢ ( 2 ∥ 𝑁 → ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) = ( 0 + 0 ) )
277 00id ⊢ ( 0 + 0 ) = 0
278 276 277 eqtrdi ⊢ ( 2 ∥ 𝑁 → ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) = 0 )
279 278 oveq1d ⊢ ( 2 ∥ 𝑁 → ( ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) / 𝑁 ) = ( 0 / 𝑁 ) )
280 279 adantl ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) / 𝑁 ) = ( 0 / 𝑁 ) )
281 26 198 div0d ⊢ ( 𝜑 → ( 0 / 𝑁 ) = 0 )
282 281 adantr ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( 0 / 𝑁 ) = 0 )
283 iftrue ⊢ ( 2 ∥ 𝑁 → if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) = 0 )
284 283 eqcomd ⊢ ( 2 ∥ 𝑁 → 0 = if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) )
285 284 adantl ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → 0 = if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) )
286 280 282 285 3eqtrd ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) / 𝑁 ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) )
287 243 243 oveq12d ⊢ ( ¬ 2 ∥ 𝑁 → ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) = ( 2 + 2 ) )
288 2p2e4 ⊢ ( 2 + 2 ) = 4
289 287 288 eqtrdi ⊢ ( ¬ 2 ∥ 𝑁 → ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) = 4 )
290 289 oveq1d ⊢ ( ¬ 2 ∥ 𝑁 → ( ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) / 𝑁 ) = ( 4 / 𝑁 ) )
291 iffalse ⊢ ( ¬ 2 ∥ 𝑁 → if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) = ( 4 / 𝑁 ) )
292 290 291 eqtr4d ⊢ ( ¬ 2 ∥ 𝑁 → ( ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) / 𝑁 ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) )
293 292 adantl ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) / 𝑁 ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) )
294 286 293 pm2.61dan ⊢ ( 𝜑 → ( ( if ( 2 ∥ 𝑁 , 0 , 2 ) + if ( 2 ∥ 𝑁 , 0 , 2 ) ) / 𝑁 ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) )
295 272 275 294 3eqtr2d ⊢ ( 𝜑 → ( ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 + ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) )
296 295 oveq1d ⊢ ( 𝜑 → ( ( ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 + ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ) / π ) = ( if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) / π ) )
297 283 oveq1d ⊢ ( 2 ∥ 𝑁 → ( if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) / π ) = ( 0 / π ) )
298 297 adantl ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) / π ) = ( 0 / π ) )
299 8 11 gtneii ⊢ π ≠ 0
300 42 299 div0i ⊢ ( 0 / π ) = 0
301 300 a1i ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( 0 / π ) = 0 )
302 iftrue ⊢ ( 2 ∥ 𝑁 → if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) = 0 )
303 302 eqcomd ⊢ ( 2 ∥ 𝑁 → 0 = if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) )
304 303 adantl ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → 0 = if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) )
305 298 301 304 3eqtrd ⊢ ( ( 𝜑 ∧ 2 ∥ 𝑁 ) → ( if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) / π ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) )
306 291 oveq1d ⊢ ( ¬ 2 ∥ 𝑁 → ( if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) / π ) = ( ( 4 / 𝑁 ) / π ) )
307 306 adantl ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) / π ) = ( ( 4 / 𝑁 ) / π ) )
308 4cn ⊢ 4 ∈ ℂ
309 308 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
310 42 a1i ⊢ ( 𝜑 → π ∈ ℂ )
311 299 a1i ⊢ ( 𝜑 → π ≠ 0 )
312 309 26 310 198 311 divdiv1d ⊢ ( 𝜑 → ( ( 4 / 𝑁 ) / π ) = ( 4 / ( 𝑁 · π ) ) )
313 312 adantr ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( ( 4 / 𝑁 ) / π ) = ( 4 / ( 𝑁 · π ) ) )
314 iffalse ⊢ ( ¬ 2 ∥ 𝑁 → if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) = ( 4 / ( 𝑁 · π ) ) )
315 314 eqcomd ⊢ ( ¬ 2 ∥ 𝑁 → ( 4 / ( 𝑁 · π ) ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) )
316 315 adantl ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( 4 / ( 𝑁 · π ) ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) )
317 307 313 316 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 2 ∥ 𝑁 ) → ( if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) / π ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) )
318 305 317 pm2.61dan ⊢ ( 𝜑 → ( if ( 2 ∥ 𝑁 , 0 , ( 4 / 𝑁 ) ) / π ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) )
319 186 296 318 3eqtrd ⊢ ( 𝜑 → ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( sin ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 / π ) = if ( 2 ∥ 𝑁 , 0 , ( 4 / ( 𝑁 · π ) ) ) )