Metamath Proof Explorer

Theorem sqwvfoura

Description: Fourier coefficients for the square wave function. Since the square function is an odd function, there is no contribution from the A coefficients. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 sqwvfoura.t ⊢ 𝑇 = ( 2 · π )
2 sqwvfoura.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
3 sqwvfoura.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
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 1red ⊢ ( 𝑥 ∈ ℝ → 1 ∈ ℝ )
17 16 renegcld ⊢ ( 𝑥 ∈ ℝ → - 1 ∈ ℝ )
18 16 17 ifcld ⊢ ( 𝑥 ∈ ℝ → if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) ∈ ℝ )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) ∈ ℝ )
20 19 2 fmptd ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → 𝐹 : ℝ ⟶ ℝ )
22 elioore ⊢ ( 𝑥 ∈ ( - π (,) π ) → 𝑥 ∈ ℝ )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → 𝑥 ∈ ℝ )
24 21 23 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
25 3 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → 𝑁 ∈ ℝ )
27 26 23 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( 𝑁 · 𝑥 ) ∈ ℝ )
28 27 recoscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) ∈ ℝ )
29 24 28 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ℝ )
30 29 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) π ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ℂ )
31 elioore ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑥 ∈ ℝ )
32 2 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) = if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
33 31 18 32 syl2anc2 ⊢ ( 𝑥 ∈ ( - π (,) 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 31 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 5 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → - π ∈ ℝ )
55 2re ⊢ 2 ∈ ℝ
56 55 4 remulcli ⊢ ( 2 · π ) ∈ ℝ
57 1 56 eqeltri ⊢ 𝑇 ∈ ℝ
58 57 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑇 ∈ ℝ )
59 5 rexri ⊢ - π ∈ ℝ*
60 59 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → - π ∈ ℝ* )
61 0red ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 0 ∈ ℝ )
62 61 rexrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 0 ∈ ℝ* )
63 id ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑥 ∈ ( - π (,) 0 ) )
64 ioogtlb ⊢ ( ( - π ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑥 ∈ ( - π (,) 0 ) ) → - π < 𝑥 )
65 60 62 63 64 syl3anc ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → - π < 𝑥 )
66 54 31 58 65 ltadd1dd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( - π + 𝑇 ) < ( 𝑥 + 𝑇 ) )
67 53 66 eqbrtrid ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → π < ( 𝑥 + 𝑇 ) )
68 57 recni ⊢ 𝑇 ∈ ℂ
69 68 mullidi ⊢ ( 1 · 𝑇 ) = 𝑇
70 69 eqcomi ⊢ 𝑇 = ( 1 · 𝑇 )
71 70 oveq2i ⊢ ( 𝑥 + 𝑇 ) = ( 𝑥 + ( 1 · 𝑇 ) )
72 71 oveq1i ⊢ ( ( 𝑥 + 𝑇 ) mod 𝑇 ) = ( ( 𝑥 + ( 1 · 𝑇 ) ) mod 𝑇 )
73 31 58 readdcld ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝑥 + 𝑇 ) ∈ ℝ )
74 11 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 0 < π )
75 61 34 73 74 67 lttrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 0 < ( 𝑥 + 𝑇 ) )
76 61 73 75 ltled ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 0 ≤ ( 𝑥 + 𝑇 ) )
77 iooltub ⊢ ( ( - π ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝑥 ∈ ( - π (,) 0 ) ) → 𝑥 < 0 )
78 60 62 63 77 syl3anc ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑥 < 0 )
79 31 61 58 78 ltadd1dd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝑥 + 𝑇 ) < ( 0 + 𝑇 ) )
80 68 a1i ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑇 ∈ ℂ )
81 80 addlidd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 0 + 𝑇 ) = 𝑇 )
82 79 81 breqtrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝑥 + 𝑇 ) < 𝑇 )
83 modid ⊢ ( ( ( ( 𝑥 + 𝑇 ) ∈ ℝ ∧ 𝑇 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑥 + 𝑇 ) ∧ ( 𝑥 + 𝑇 ) < 𝑇 ) ) → ( ( 𝑥 + 𝑇 ) mod 𝑇 ) = ( 𝑥 + 𝑇 ) )
84 73 40 76 82 83 syl22anc ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( ( 𝑥 + 𝑇 ) mod 𝑇 ) = ( 𝑥 + 𝑇 ) )
85 1zzd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 1 ∈ ℤ )
86 modcyc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ∧ 1 ∈ ℤ ) → ( ( 𝑥 + ( 1 · 𝑇 ) ) mod 𝑇 ) = ( 𝑥 mod 𝑇 ) )
87 31 40 85 86 syl3anc ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( ( 𝑥 + ( 1 · 𝑇 ) ) mod 𝑇 ) = ( 𝑥 mod 𝑇 ) )
88 72 84 87 3eqtr3a ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝑥 + 𝑇 ) = ( 𝑥 mod 𝑇 ) )
89 67 88 breqtrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → π < ( 𝑥 mod 𝑇 ) )
90 34 41 89 ltnsymd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ¬ ( 𝑥 mod 𝑇 ) < π )
91 90 iffalsed ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) = - 1 )
92 33 91 eqtrd ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 𝐹 ‘ 𝑥 ) = - 1 )
93 92 oveq1d ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) = ( - 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) )
94 93 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) = ( - 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) )
95 94 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π (,) 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ( - π (,) 0 ) ↦ ( - 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ) )
96 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
97 96 negcld ⊢ ( 𝜑 → - 1 ∈ ℂ )
98 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → 𝑁 ∈ ℝ )
99 31 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → 𝑥 ∈ ℝ )
100 98 99 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( 𝑁 · 𝑥 ) ∈ ℝ )
101 100 recoscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) ∈ ℝ )
102 ioossicc ⊢ ( - π (,) 0 ) ⊆ ( - π [,] 0 )
103 102 a1i ⊢ ( 𝜑 → ( - π (,) 0 ) ⊆ ( - π [,] 0 ) )
104 ioombl ⊢ ( - π (,) 0 ) ∈ dom vol
105 104 a1i ⊢ ( 𝜑 → ( - π (,) 0 ) ∈ dom vol )
106 25 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 recoscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] 0 ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) ∈ ℝ )
113 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
114 coscn ⊢ cos ∈ ( ℂ –cn→ ℂ )
115 114 a1i ⊢ ( 𝜑 → cos ∈ ( ℂ –cn→ ℂ ) )
116 ax-resscn ⊢ ℝ ⊆ ℂ
117 108 116 sstri ⊢ ( - π [,] 0 ) ⊆ ℂ
118 117 a1i ⊢ ( 𝜑 → ( - π [,] 0 ) ⊆ ℂ )
119 25 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
120 ssid ⊢ ℂ ⊆ ℂ
121 120 a1i ⊢ ( 𝜑 → ℂ ⊆ ℂ )
122 118 119 121 constcncfg ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] 0 ) ↦ 𝑁 ) ∈ ( ( - π [,] 0 ) –cn→ ℂ ) )
123 118 121 idcncfg ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] 0 ) ↦ 𝑥 ) ∈ ( ( - π [,] 0 ) –cn→ ℂ ) )
124 122 123 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] 0 ) ↦ ( 𝑁 · 𝑥 ) ) ∈ ( ( - π [,] 0 ) –cn→ ℂ ) )
125 115 124 cncfmpt1f ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] 0 ) ↦ ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ( ( - π [,] 0 ) –cn→ ℂ ) )
126 cniccibl ⊢ ( ( - π ∈ ℝ ∧ 0 ∈ ℝ ∧ ( 𝑥 ∈ ( - π [,] 0 ) ↦ ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ( ( - π [,] 0 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( - π [,] 0 ) ↦ ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
127 6 113 125 126 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π [,] 0 ) ↦ ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
128 103 105 112 127 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π (,) 0 ) ↦ ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
129 97 101 128 iblmulc2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π (,) 0 ) ↦ ( - 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 )
130 95 129 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( - π (,) 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 )
131 elioore ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 ∈ ℝ )
132 131 18 32 syl2anc2 ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( 𝐹 ‘ 𝑥 ) = if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) )
133 39 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑇 ∈ ℝ+ )
134 0red ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 0 ∈ ℝ )
135 134 rexrd ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 0 ∈ ℝ* )
136 4 rexri ⊢ π ∈ ℝ*
137 136 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → π ∈ ℝ* )
138 id ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 ∈ ( 0 (,) π ) )
139 ioogtlb ⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑥 ∈ ( 0 (,) π ) ) → 0 < 𝑥 )
140 135 137 138 139 syl3anc ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 0 < 𝑥 )
141 134 131 140 ltled ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 0 ≤ 𝑥 )
142 4 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → π ∈ ℝ )
143 57 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑇 ∈ ℝ )
144 iooltub ⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝑥 ∈ ( 0 (,) π ) ) → 𝑥 < π )
145 135 137 138 144 syl3anc ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 < π )
146 2timesgt ⊢ ( π ∈ ℝ+ → π < ( 2 · π ) )
147 36 146 ax-mp ⊢ π < ( 2 · π )
148 147 1 breqtrri ⊢ π < 𝑇
149 148 a1i ⊢ ( 𝑥 ∈ ( 0 (,) π ) → π < 𝑇 )
150 131 142 143 145 149 lttrd ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 < 𝑇 )
151 modid ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑇 ∈ ℝ+ ) ∧ ( 0 ≤ 𝑥 ∧ 𝑥 < 𝑇 ) ) → ( 𝑥 mod 𝑇 ) = 𝑥 )
152 131 133 141 150 151 syl22anc ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( 𝑥 mod 𝑇 ) = 𝑥 )
153 152 145 eqbrtrd ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( 𝑥 mod 𝑇 ) < π )
154 153 iftrued ⊢ ( 𝑥 ∈ ( 0 (,) π ) → if ( ( 𝑥 mod 𝑇 ) < π , 1 , - 1 ) = 1 )
155 132 154 eqtrd ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( 𝐹 ‘ 𝑥 ) = 1 )
156 155 oveq1d ⊢ ( 𝑥 ∈ ( 0 (,) π ) → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) = ( 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) )
157 156 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) = ( 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) )
158 157 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 0 (,) π ) ↦ ( 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ) )
159 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → 𝑁 ∈ ℝ )
160 131 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → 𝑥 ∈ ℝ )
161 159 160 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( 𝑁 · 𝑥 ) ∈ ℝ )
162 161 recoscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) ∈ ℝ )
163 ioossicc ⊢ ( 0 (,) π ) ⊆ ( 0 [,] π )
164 163 a1i ⊢ ( 𝜑 → ( 0 (,) π ) ⊆ ( 0 [,] π ) )
165 ioombl ⊢ ( 0 (,) π ) ∈ dom vol
166 165 a1i ⊢ ( 𝜑 → ( 0 (,) π ) ∈ dom vol )
167 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] π ) ) → 𝑁 ∈ ℝ )
168 iccssre ⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ) → ( 0 [,] π ) ⊆ ℝ )
169 8 4 168 mp2an ⊢ ( 0 [,] π ) ⊆ ℝ
170 169 sseli ⊢ ( 𝑥 ∈ ( 0 [,] π ) → 𝑥 ∈ ℝ )
171 170 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] π ) ) → 𝑥 ∈ ℝ )
172 167 171 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] π ) ) → ( 𝑁 · 𝑥 ) ∈ ℝ )
173 172 recoscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] π ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) ∈ ℝ )
174 169 116 sstri ⊢ ( 0 [,] π ) ⊆ ℂ
175 174 a1i ⊢ ( 𝜑 → ( 0 [,] π ) ⊆ ℂ )
176 175 119 121 constcncfg ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] π ) ↦ 𝑁 ) ∈ ( ( 0 [,] π ) –cn→ ℂ ) )
177 175 121 idcncfg ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] π ) ↦ 𝑥 ) ∈ ( ( 0 [,] π ) –cn→ ℂ ) )
178 176 177 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] π ) ↦ ( 𝑁 · 𝑥 ) ) ∈ ( ( 0 [,] π ) –cn→ ℂ ) )
179 115 178 cncfmpt1f ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] π ) ↦ ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ( ( 0 [,] π ) –cn→ ℂ ) )
180 cniccibl ⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ∧ ( 𝑥 ∈ ( 0 [,] π ) ↦ ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ ( ( 0 [,] π ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 0 [,] π ) ↦ ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
181 113 7 179 180 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] π ) ↦ ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
182 164 166 173 181 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ∈ 𝐿1 )
183 96 162 182 iblmulc2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 )
184 158 183 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) π ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) ) ∈ 𝐿1 )
185 6 7 15 30 130 184 itgsplitioo ⊢ ( 𝜑 → ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 = ( ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 + ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ) )
186 185 oveq1d ⊢ ( 𝜑 → ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 / π ) = ( ( ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 + ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ) / π ) )
187 94 itgeq2dv ⊢ ( 𝜑 → ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 = ∫ ( - π (,) 0 ) ( - 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 )
188 97 101 128 itgmulc2 ⊢ ( 𝜑 → ( - 1 · ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ) = ∫ ( - π (,) 0 ) ( - 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 )
189 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 · 𝑥 ) = ( 0 · 𝑥 ) )
190 ioosscn ⊢ ( - π (,) 0 ) ⊆ ℂ
191 190 sseli ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → 𝑥 ∈ ℂ )
192 191 mul02d ⊢ ( 𝑥 ∈ ( - π (,) 0 ) → ( 0 · 𝑥 ) = 0 )
193 189 192 sylan9eq ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( 𝑁 · 𝑥 ) = 0 )
194 193 fveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) = ( cos ‘ 0 ) )
195 cos0 ⊢ ( cos ‘ 0 ) = 1
196 194 195 eqtrdi ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) = 1 )
197 196 adantll ⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ) ∧ 𝑥 ∈ ( - π (,) 0 ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) = 1 )
198 197 itgeq2dv ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = ∫ ( - π (,) 0 ) 1 d 𝑥 )
199 ioovolcl ⊢ ( ( - π ∈ ℝ ∧ 0 ∈ ℝ ) → ( vol ‘ ( - π (,) 0 ) ) ∈ ℝ )
200 5 8 199 mp2an ⊢ ( vol ‘ ( - π (,) 0 ) ) ∈ ℝ
201 200 a1i ⊢ ( 𝜑 → ( vol ‘ ( - π (,) 0 ) ) ∈ ℝ )
202 itgconst ⊢ ( ( ( - π (,) 0 ) ∈ dom vol ∧ ( vol ‘ ( - π (,) 0 ) ) ∈ ℝ ∧ 1 ∈ ℂ ) → ∫ ( - π (,) 0 ) 1 d 𝑥 = ( 1 · ( vol ‘ ( - π (,) 0 ) ) ) )
203 105 201 96 202 syl3anc ⊢ ( 𝜑 → ∫ ( - π (,) 0 ) 1 d 𝑥 = ( 1 · ( vol ‘ ( - π (,) 0 ) ) ) )
204 203 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ∫ ( - π (,) 0 ) 1 d 𝑥 = ( 1 · ( vol ‘ ( - π (,) 0 ) ) ) )
205 volioo ⊢ ( ( - π ∈ ℝ ∧ 0 ∈ ℝ ∧ - π ≤ 0 ) → ( vol ‘ ( - π (,) 0 ) ) = ( 0 − - π ) )
206 5 8 10 205 mp3an ⊢ ( vol ‘ ( - π (,) 0 ) ) = ( 0 − - π )
207 0cn ⊢ 0 ∈ ℂ
208 207 42 subnegi ⊢ ( 0 − - π ) = ( 0 + π )
209 206 208 51 3eqtri ⊢ ( vol ‘ ( - π (,) 0 ) ) = π
210 209 a1i ⊢ ( 𝜑 → ( vol ‘ ( - π (,) 0 ) ) = π )
211 210 oveq2d ⊢ ( 𝜑 → ( 1 · ( vol ‘ ( - π (,) 0 ) ) ) = ( 1 · π ) )
212 42 a1i ⊢ ( 𝜑 → π ∈ ℂ )
213 212 mullidd ⊢ ( 𝜑 → ( 1 · π ) = π )
214 211 213 eqtrd ⊢ ( 𝜑 → ( 1 · ( vol ‘ ( - π (,) 0 ) ) ) = π )
215 214 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 1 · ( vol ‘ ( - π (,) 0 ) ) ) = π )
216 198 204 215 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = π )
217 216 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( - 1 · ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ) = ( - 1 · π ) )
218 42 mulm1i ⊢ ( - 1 · π ) = - π
219 218 a1i ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( - 1 · π ) = - π )
220 iftrue ⊢ ( 𝑁 = 0 → if ( 𝑁 = 0 , - π , 0 ) = - π )
221 220 eqcomd ⊢ ( 𝑁 = 0 → - π = if ( 𝑁 = 0 , - π , 0 ) )
222 221 adantl ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → - π = if ( 𝑁 = 0 , - π , 0 ) )
223 217 219 222 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( - 1 · ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ) = if ( 𝑁 = 0 , - π , 0 ) )
224 25 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) → 𝑁 ∈ ℝ )
225 3 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
226 225 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) → 0 ≤ 𝑁 )
227 neqne ⊢ ( ¬ 𝑁 = 0 → 𝑁 ≠ 0 )
228 227 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) → 𝑁 ≠ 0 )
229 224 226 228 ne0gt0d ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) → 0 < 𝑁 )
230 1cnd ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 1 ∈ ℂ )
231 230 negcld ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → - 1 ∈ ℂ )
232 231 mul01d ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( - 1 · 0 ) = 0 )
233 119 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑁 ∈ ℂ )
234 5 a1i ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → - π ∈ ℝ )
235 0red ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 0 ∈ ℝ )
236 10 a1i ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → - π ≤ 0 )
237 simpr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 0 < 𝑁 )
238 237 gt0ne0d ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 𝑁 ≠ 0 )
239 233 234 235 236 238 itgcoscmulx ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = ( ( ( sin ‘ ( 𝑁 · 0 ) ) − ( sin ‘ ( 𝑁 · - π ) ) ) / 𝑁 ) )
240 119 mul01d ⊢ ( 𝜑 → ( 𝑁 · 0 ) = 0 )
241 240 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( 𝑁 · 0 ) ) = ( sin ‘ 0 ) )
242 sin0 ⊢ ( sin ‘ 0 ) = 0
243 241 242 eqtrdi ⊢ ( 𝜑 → ( sin ‘ ( 𝑁 · 0 ) ) = 0 )
244 119 212 mulneg2d ⊢ ( 𝜑 → ( 𝑁 · - π ) = - ( 𝑁 · π ) )
245 244 fveq2d ⊢ ( 𝜑 → ( sin ‘ ( 𝑁 · - π ) ) = ( sin ‘ - ( 𝑁 · π ) ) )
246 119 212 mulcld ⊢ ( 𝜑 → ( 𝑁 · π ) ∈ ℂ )
247 sinneg ⊢ ( ( 𝑁 · π ) ∈ ℂ → ( sin ‘ - ( 𝑁 · π ) ) = - ( sin ‘ ( 𝑁 · π ) ) )
248 246 247 syl ⊢ ( 𝜑 → ( sin ‘ - ( 𝑁 · π ) ) = - ( sin ‘ ( 𝑁 · π ) ) )
249 245 248 eqtrd ⊢ ( 𝜑 → ( sin ‘ ( 𝑁 · - π ) ) = - ( sin ‘ ( 𝑁 · π ) ) )
250 243 249 oveq12d ⊢ ( 𝜑 → ( ( sin ‘ ( 𝑁 · 0 ) ) − ( sin ‘ ( 𝑁 · - π ) ) ) = ( 0 − - ( sin ‘ ( 𝑁 · π ) ) ) )
251 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
252 246 sincld ⊢ ( 𝜑 → ( sin ‘ ( 𝑁 · π ) ) ∈ ℂ )
253 251 252 subnegd ⊢ ( 𝜑 → ( 0 − - ( sin ‘ ( 𝑁 · π ) ) ) = ( 0 + ( sin ‘ ( 𝑁 · π ) ) ) )
254 252 addlidd ⊢ ( 𝜑 → ( 0 + ( sin ‘ ( 𝑁 · π ) ) ) = ( sin ‘ ( 𝑁 · π ) ) )
255 250 253 254 3eqtrd ⊢ ( 𝜑 → ( ( sin ‘ ( 𝑁 · 0 ) ) − ( sin ‘ ( 𝑁 · - π ) ) ) = ( sin ‘ ( 𝑁 · π ) ) )
256 255 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( ( sin ‘ ( 𝑁 · 0 ) ) − ( sin ‘ ( 𝑁 · - π ) ) ) = ( sin ‘ ( 𝑁 · π ) ) )
257 256 oveq1d ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( ( ( sin ‘ ( 𝑁 · 0 ) ) − ( sin ‘ ( 𝑁 · - π ) ) ) / 𝑁 ) = ( ( sin ‘ ( 𝑁 · π ) ) / 𝑁 ) )
258 3 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
259 sinkpi ⊢ ( 𝑁 ∈ ℤ → ( sin ‘ ( 𝑁 · π ) ) = 0 )
260 258 259 syl ⊢ ( 𝜑 → ( sin ‘ ( 𝑁 · π ) ) = 0 )
261 260 oveq1d ⊢ ( 𝜑 → ( ( sin ‘ ( 𝑁 · π ) ) / 𝑁 ) = ( 0 / 𝑁 ) )
262 261 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( ( sin ‘ ( 𝑁 · π ) ) / 𝑁 ) = ( 0 / 𝑁 ) )
263 233 238 div0d ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( 0 / 𝑁 ) = 0 )
264 262 263 eqtrd ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( ( sin ‘ ( 𝑁 · π ) ) / 𝑁 ) = 0 )
265 239 257 264 3eqtrd ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = 0 )
266 265 oveq2d ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( - 1 · ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ) = ( - 1 · 0 ) )
267 238 neneqd ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ¬ 𝑁 = 0 )
268 267 iffalsed ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → if ( 𝑁 = 0 , - π , 0 ) = 0 )
269 232 266 268 3eqtr4d ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( - 1 · ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ) = if ( 𝑁 = 0 , - π , 0 ) )
270 229 269 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) → ( - 1 · ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ) = if ( 𝑁 = 0 , - π , 0 ) )
271 223 270 pm2.61dan ⊢ ( 𝜑 → ( - 1 · ∫ ( - π (,) 0 ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ) = if ( 𝑁 = 0 , - π , 0 ) )
272 187 188 271 3eqtr2d ⊢ ( 𝜑 → ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 = if ( 𝑁 = 0 , - π , 0 ) )
273 157 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 = ∫ ( 0 (,) π ) ( 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 )
274 96 162 182 itgmulc2 ⊢ ( 𝜑 → ( 1 · ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ) = ∫ ( 0 (,) π ) ( 1 · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 )
275 162 182 itgcl ⊢ ( 𝜑 → ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ∈ ℂ )
276 275 mullidd ⊢ ( 𝜑 → ( 1 · ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ) = ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 )
277 simpl ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → 𝑁 = 0 )
278 277 oveq1d ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( 𝑁 · 𝑥 ) = ( 0 · 𝑥 ) )
279 131 recnd ⊢ ( 𝑥 ∈ ( 0 (,) π ) → 𝑥 ∈ ℂ )
280 279 adantl ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → 𝑥 ∈ ℂ )
281 280 mul02d ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( 0 · 𝑥 ) = 0 )
282 278 281 eqtrd ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( 𝑁 · 𝑥 ) = 0 )
283 282 fveq2d ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) = ( cos ‘ 0 ) )
284 283 195 eqtrdi ⊢ ( ( 𝑁 = 0 ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) = 1 )
285 284 adantll ⊢ ( ( ( 𝜑 ∧ 𝑁 = 0 ) ∧ 𝑥 ∈ ( 0 (,) π ) ) → ( cos ‘ ( 𝑁 · 𝑥 ) ) = 1 )
286 285 itgeq2dv ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = ∫ ( 0 (,) π ) 1 d 𝑥 )
287 ioovolcl ⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ) → ( vol ‘ ( 0 (,) π ) ) ∈ ℝ )
288 8 4 287 mp2an ⊢ ( vol ‘ ( 0 (,) π ) ) ∈ ℝ
289 ax-1cn ⊢ 1 ∈ ℂ
290 itgconst ⊢ ( ( ( 0 (,) π ) ∈ dom vol ∧ ( vol ‘ ( 0 (,) π ) ) ∈ ℝ ∧ 1 ∈ ℂ ) → ∫ ( 0 (,) π ) 1 d 𝑥 = ( 1 · ( vol ‘ ( 0 (,) π ) ) ) )
291 165 288 289 290 mp3an ⊢ ∫ ( 0 (,) π ) 1 d 𝑥 = ( 1 · ( vol ‘ ( 0 (,) π ) ) )
292 291 a1i ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ∫ ( 0 (,) π ) 1 d 𝑥 = ( 1 · ( vol ‘ ( 0 (,) π ) ) ) )
293 42 mullidi ⊢ ( 1 · π ) = π
294 volioo ⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ∧ 0 ≤ π ) → ( vol ‘ ( 0 (,) π ) ) = ( π − 0 ) )
295 8 4 12 294 mp3an ⊢ ( vol ‘ ( 0 (,) π ) ) = ( π − 0 )
296 42 subid1i ⊢ ( π − 0 ) = π
297 295 296 eqtri ⊢ ( vol ‘ ( 0 (,) π ) ) = π
298 297 oveq2i ⊢ ( 1 · ( vol ‘ ( 0 (,) π ) ) ) = ( 1 · π )
299 298 a1i ⊢ ( 𝑁 = 0 → ( 1 · ( vol ‘ ( 0 (,) π ) ) ) = ( 1 · π ) )
300 iftrue ⊢ ( 𝑁 = 0 → if ( 𝑁 = 0 , π , 0 ) = π )
301 293 299 300 3eqtr4a ⊢ ( 𝑁 = 0 → ( 1 · ( vol ‘ ( 0 (,) π ) ) ) = if ( 𝑁 = 0 , π , 0 ) )
302 301 adantl ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ( 1 · ( vol ‘ ( 0 (,) π ) ) ) = if ( 𝑁 = 0 , π , 0 ) )
303 286 292 302 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = if ( 𝑁 = 0 , π , 0 ) )
304 260 243 oveq12d ⊢ ( 𝜑 → ( ( sin ‘ ( 𝑁 · π ) ) − ( sin ‘ ( 𝑁 · 0 ) ) ) = ( 0 − 0 ) )
305 251 subidd ⊢ ( 𝜑 → ( 0 − 0 ) = 0 )
306 304 305 eqtrd ⊢ ( 𝜑 → ( ( sin ‘ ( 𝑁 · π ) ) − ( sin ‘ ( 𝑁 · 0 ) ) ) = 0 )
307 306 oveq1d ⊢ ( 𝜑 → ( ( ( sin ‘ ( 𝑁 · π ) ) − ( sin ‘ ( 𝑁 · 0 ) ) ) / 𝑁 ) = ( 0 / 𝑁 ) )
308 307 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( ( ( sin ‘ ( 𝑁 · π ) ) − ( sin ‘ ( 𝑁 · 0 ) ) ) / 𝑁 ) = ( 0 / 𝑁 ) )
309 308 263 eqtrd ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ( ( ( sin ‘ ( 𝑁 · π ) ) − ( sin ‘ ( 𝑁 · 0 ) ) ) / 𝑁 ) = 0 )
310 4 a1i ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → π ∈ ℝ )
311 12 a1i ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → 0 ≤ π )
312 233 235 310 311 238 itgcoscmulx ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = ( ( ( sin ‘ ( 𝑁 · π ) ) − ( sin ‘ ( 𝑁 · 0 ) ) ) / 𝑁 ) )
313 267 iffalsed ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → if ( 𝑁 = 0 , π , 0 ) = 0 )
314 309 312 313 3eqtr4d ⊢ ( ( 𝜑 ∧ 0 < 𝑁 ) → ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = if ( 𝑁 = 0 , π , 0 ) )
315 229 314 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝑁 = 0 ) → ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = if ( 𝑁 = 0 , π , 0 ) )
316 303 315 pm2.61dan ⊢ ( 𝜑 → ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 = if ( 𝑁 = 0 , π , 0 ) )
317 276 316 eqtrd ⊢ ( 𝜑 → ( 1 · ∫ ( 0 (,) π ) ( cos ‘ ( 𝑁 · 𝑥 ) ) d 𝑥 ) = if ( 𝑁 = 0 , π , 0 ) )
318 273 274 317 3eqtr2d ⊢ ( 𝜑 → ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 = if ( 𝑁 = 0 , π , 0 ) )
319 272 318 oveq12d ⊢ ( 𝜑 → ( ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 + ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ) = ( if ( 𝑁 = 0 , - π , 0 ) + if ( 𝑁 = 0 , π , 0 ) ) )
320 319 oveq1d ⊢ ( 𝜑 → ( ( ∫ ( - π (,) 0 ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 + ∫ ( 0 (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 ) / π ) = ( ( if ( 𝑁 = 0 , - π , 0 ) + if ( 𝑁 = 0 , π , 0 ) ) / π ) )
321 220 300 oveq12d ⊢ ( 𝑁 = 0 → ( if ( 𝑁 = 0 , - π , 0 ) + if ( 𝑁 = 0 , π , 0 ) ) = ( - π + π ) )
322 321 49 eqtrdi ⊢ ( 𝑁 = 0 → ( if ( 𝑁 = 0 , - π , 0 ) + if ( 𝑁 = 0 , π , 0 ) ) = 0 )
323 iffalse ⊢ ( ¬ 𝑁 = 0 → if ( 𝑁 = 0 , - π , 0 ) = 0 )
324 iffalse ⊢ ( ¬ 𝑁 = 0 → if ( 𝑁 = 0 , π , 0 ) = 0 )
325 323 324 oveq12d ⊢ ( ¬ 𝑁 = 0 → ( if ( 𝑁 = 0 , - π , 0 ) + if ( 𝑁 = 0 , π , 0 ) ) = ( 0 + 0 ) )
326 00id ⊢ ( 0 + 0 ) = 0
327 325 326 eqtrdi ⊢ ( ¬ 𝑁 = 0 → ( if ( 𝑁 = 0 , - π , 0 ) + if ( 𝑁 = 0 , π , 0 ) ) = 0 )
328 322 327 pm2.61i ⊢ ( if ( 𝑁 = 0 , - π , 0 ) + if ( 𝑁 = 0 , π , 0 ) ) = 0
329 328 oveq1i ⊢ ( ( if ( 𝑁 = 0 , - π , 0 ) + if ( 𝑁 = 0 , π , 0 ) ) / π ) = ( 0 / π )
330 8 11 gtneii ⊢ π ≠ 0
331 42 330 div0i ⊢ ( 0 / π ) = 0
332 329 331 eqtri ⊢ ( ( if ( 𝑁 = 0 , - π , 0 ) + if ( 𝑁 = 0 , π , 0 ) ) / π ) = 0
333 332 a1i ⊢ ( 𝜑 → ( ( if ( 𝑁 = 0 , - π , 0 ) + if ( 𝑁 = 0 , π , 0 ) ) / π ) = 0 )
334 186 320 333 3eqtrd ⊢ ( 𝜑 → ( ∫ ( - π (,) π ) ( ( 𝐹 ‘ 𝑥 ) · ( cos ‘ ( 𝑁 · 𝑥 ) ) ) d 𝑥 / π ) = 0 )