sqwvfourb

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

	Ref	Expression
Hypotheses	sqwvfourb.t	\|- T = ( 2 x. _pi )
	sqwvfourb.f	\|- F = ( x e. RR \|-> if ( ( x mod T ) < _pi , 1 , -u 1 ) )
	sqwvfourb.n	\|- ( ph -> N e. NN )
Assertion	sqwvfourb	\|- ( ph -> ( S. ( -u _pi (,) _pi ) ( ( F ` x ) x. ( sin ` ( N x. x ) ) ) _d x / _pi ) = if ( 2 \|\| N , 0 , ( 4 / ( N x. _pi ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem sqwvfourb

Proof