sumnnodd - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sumnnodd		Structured version Visualization version Unicode version

Theorem sumnnodd 39862

Description: A series indexed by

with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
sumnnodd.1
sumnnodd.even0	$/\$ $/\$
sumnnodd.sc

**Assertion**
Ref	Expression
sumnnodd	$/\$

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem sumnnodd Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1843	. . 3
2		nfcv 2764	. . 3
3		nfcv 2764	. . . 4
4		nfcv 2764	. . . 4
5		nfmpt1 4747	. . . 4
6	3, 4, 5	nfseq 12811	. . 3
7		nfmpt1 4747	. . 3
8		nnuz 11723	. . 3
9		1zzd 11408	. . 3
10		seqex 12803	. . . 4
11	10	a1i 11	. . 3
12		sumnnodd.1	. . . . . 6
13	12	ffvelrnda 6359	. . . . 5 $/\$
14	8, 9, 13	serf 12829	. . . 4
15	14	ffvelrnda 6359	. . 3 $/\$
16		sumnnodd.sc	. . 3
17		1nn 11031	. . . . . . 7
18		oveq2 6658	. . . . . . . . 9
19	18	oveq1d 6665	. . . . . . . 8
20		eqid 2622	. . . . . . . 8
21		ovex 6678	. . . . . . . 8
22	19, 20, 21	fvmpt 6282	. . . . . . 7
23	17, 22	ax-mp 5	. . . . . 6
24		2t1e2 11176	. . . . . . 7
25	24	oveq1i 6660	. . . . . 6
26		2m1e1 11135	. . . . . 6
27	23, 25, 26	3eqtri 2648	. . . . 5
28	27, 17	eqeltri 2697	. . . 4
29	28	a1i 11	. . 3
30		2z 11409	. . . . . . . 8
31	30	a1i 11	. . . . . . 7
32		nnz 11399	. . . . . . 7
33	31, 32	zmulcld 11488	. . . . . 6
34	32	peano2zd 11485	. . . . . . . 8
35	31, 34	zmulcld 11488	. . . . . . 7
36		1zzd 11408	. . . . . . 7
37	35, 36	zsubcld 11487	. . . . . 6
38		2re 11090	. . . . . . . . . 10
39	38	a1i 11	. . . . . . . . 9
40		nnre 11027	. . . . . . . . 9
41	39, 40	remulcld 10070	. . . . . . . 8
42	41	lep1d 10955	. . . . . . 7
43		2cnd 11093	. . . . . . . . . . 11
44		nncn 11028	. . . . . . . . . . 11
45		1cnd 10056	. . . . . . . . . . 11
46	43, 44, 45	adddid 10064	. . . . . . . . . 10
47	24	oveq2i 6661	. . . . . . . . . 10
48	46, 47	syl6eq 2672	. . . . . . . . 9
49	48	oveq1d 6665	. . . . . . . 8
50	43, 44	mulcld 10060	. . . . . . . . 9
51	50, 43, 45	addsubassd 10412	. . . . . . . 8
52	26	oveq2i 6661	. . . . . . . . 9
53	52	a1i 11	. . . . . . . 8
54	49, 51, 53	3eqtrrd 2661	. . . . . . 7
55	42, 54	breqtrd 4679	. . . . . 6
56		eluz2 11693	. . . . . 6 $/\$ $/\$
57	33, 37, 55, 56	syl3anbrc 1246	. . . . 5
58		oveq2 6658	. . . . . . . . 9
59	58	oveq1d 6665	. . . . . . . 8
60	59	cbvmptv 4750	. . . . . . 7
61	60	a1i 11	. . . . . 6
62		oveq2 6658	. . . . . . . 8
63	62	oveq1d 6665	. . . . . . 7
64	63	adantl 482	. . . . . 6 $/\$
65		peano2nn 11032	. . . . . 6
66	61, 64, 65, 37	fvmptd 6288	. . . . 5
67	33, 36	zsubcld 11487	. . . . . . . . 9
68	20	fvmpt2 6291	. . . . . . . . 9 $/\$
69	67, 68	mpdan 702	. . . . . . . 8
70	69	oveq1d 6665	. . . . . . 7
71	50, 45	npcand 10396	. . . . . . 7
72	70, 71	eqtrd 2656	. . . . . 6
73	72	fveq2d 6195	. . . . 5
74	57, 66, 73	3eltr4d 2716	. . . 4
75	74	adantl 482	. . 3 $/\$
76		seqex 12803	. . . 4
77	76	a1i 11	. . 3
78		incom 3805	. . . . . . . . . 10 $\$ $\$
79		inss2 3834	. . . . . . . . . . 11
80		ssrin 3838	. . . . . . . . . . 11 $\$ $\$
81	79, 80	ax-mp 5	. . . . . . . . . 10 $\$ $\$
82	78, 81	eqsstri 3635	. . . . . . . . 9 $\$ $\$
83		disjdif 4040	. . . . . . . . 9 $\$
84	82, 83	sseqtri 3637	. . . . . . . 8 $\$
85		ss0 3974	. . . . . . . 8 $\$ $\$
86	84, 85	mp1i 13	. . . . . . 7 $/\$ $\$
87		uncom 3757	. . . . . . . . 9 $\$ $\$
88		inundif 4046	. . . . . . . . 9 $\$
89	87, 88	eqtr2i 2645	. . . . . . . 8 $\$
90	89	a1i 11	. . . . . . 7 $/\$ $\$
91		fzfid 12772	. . . . . . 7 $/\$
92	12	adantr 481	. . . . . . . . 9 $/\$
93		elfznn 12370	. . . . . . . . . 10
94	93	adantl 482	. . . . . . . . 9 $/\$
95	92, 94	ffvelrnd 6360	. . . . . . . 8 $/\$
96	95	adantlr 751	. . . . . . 7 $/\$ $/\$
97	86, 90, 91, 96	fsumsplit 14471	. . . . . 6 $/\$ $\$
98		simpl 473	. . . . . . . . . . . 12 $/\$
99		ssrab2 3687	. . . . . . . . . . . . . 14
100	79	sseli 3599	. . . . . . . . . . . . . 14
101	99, 100	sseldi 3601	. . . . . . . . . . . . 13
102	101	adantl 482	. . . . . . . . . . . 12 $/\$
103		oveq1 6657	. . . . . . . . . . . . . . . 16
104	103	eleq1d 2686	. . . . . . . . . . . . . . 15
105		oveq1 6657	. . . . . . . . . . . . . . . . . 18
106	105	eleq1d 2686	. . . . . . . . . . . . . . . . 17
107	106	elrab 3363	. . . . . . . . . . . . . . . 16 $/\$
108	107	simprbi 480	. . . . . . . . . . . . . . 15
109	104, 108	vtoclga 3272	. . . . . . . . . . . . . 14
110	100, 109	syl 17	. . . . . . . . . . . . 13
111	110	adantl 482	. . . . . . . . . . . 12 $/\$
112		eleq1 2689	. . . . . . . . . . . . . . 15
113	112, 104	3anbi23d 1402	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
114		fveq2 6191	. . . . . . . . . . . . . . 15
115	114	eqeq1d 2624	. . . . . . . . . . . . . 14
116	113, 115	imbi12d 334	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
117		sumnnodd.even0	. . . . . . . . . . . . 13 $/\$ $/\$
118	116, 117	chvarv 2263	. . . . . . . . . . . 12 $/\$ $/\$
119	98, 102, 111, 118	syl3anc 1326	. . . . . . . . . . 11 $/\$
120	119	sumeq2dv 14433	. . . . . . . . . 10
121		fzfid 12772	. . . . . . . . . . . . 13
122		inss1 3833	. . . . . . . . . . . . . 14
123	122	a1i 11	. . . . . . . . . . . . 13
124		ssfi 8180	. . . . . . . . . . . . 13 $/\$
125	121, 123, 124	syl2anc 693	. . . . . . . . . . . 12
126	125	olcd 408	. . . . . . . . . . 11 $\/$
127		sumz 14453	. . . . . . . . . . 11 $\/$
128	126, 127	syl 17	. . . . . . . . . 10
129	120, 128	eqtrd 2656	. . . . . . . . 9
130	129	adantr 481	. . . . . . . 8 $/\$
131	130	oveq2d 6666	. . . . . . 7 $/\$ $\$ $\$
132		fzfi 12771	. . . . . . . . . . . 12
133		difss 3737	. . . . . . . . . . . 12 $\$
134		ssfi 8180	. . . . . . . . . . . 12 $/\$ $\$ $\$
135	132, 133, 134	mp2an 708	. . . . . . . . . . 11 $\$
136	135	a1i 11	. . . . . . . . . 10 $/\$ $\$
137	133	sseli 3599	. . . . . . . . . . . 12 $\$
138	137, 95	sylan2 491	. . . . . . . . . . 11 $/\$ $\$
139	138	adantlr 751	. . . . . . . . . 10 $/\$ $/\$ $\$
140	136, 139	fsumcl 14464	. . . . . . . . 9 $/\$ $\$
141	140	addid1d 10236	. . . . . . . 8 $/\$ $\$ $\$
142		fveq2 6191	. . . . . . . . 9
143	142	cbvsumv 14426	. . . . . . . 8 $\$ $\$
144	141, 143	syl6eq 2672	. . . . . . 7 $/\$ $\$ $\$
145	131, 144	eqtrd 2656	. . . . . 6 $/\$ $\$ $\$
146		fveq2 6191	. . . . . . 7
147		fzfid 12772	. . . . . . 7 $/\$
148		1zzd 11408	. . . . . . . . . . . . . 14 $/\$
149	67	adantr 481	. . . . . . . . . . . . . 14 $/\$
150	30	a1i 11	. . . . . . . . . . . . . . . . 17
151		elfzelz 12342	. . . . . . . . . . . . . . . . 17
152	150, 151	zmulcld 11488	. . . . . . . . . . . . . . . 16
153		1zzd 11408	. . . . . . . . . . . . . . . 16
154	152, 153	zsubcld 11487	. . . . . . . . . . . . . . 15
155	154	adantl 482	. . . . . . . . . . . . . 14 $/\$
156	148, 149, 155	3jca 1242	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
157	25, 26	eqtr2i 2645	. . . . . . . . . . . . . . . 16
158		1re 10039	. . . . . . . . . . . . . . . . . . 19
159	38, 158	remulcli 10054	. . . . . . . . . . . . . . . . . 18
160	159	a1i 11	. . . . . . . . . . . . . . . . 17
161	152	zred 11482	. . . . . . . . . . . . . . . . 17
162		1red 10055	. . . . . . . . . . . . . . . . 17
163	151	zred 11482	. . . . . . . . . . . . . . . . . 18
164	38	a1i 11	. . . . . . . . . . . . . . . . . 18
165		0le2 11111	. . . . . . . . . . . . . . . . . . 19
166	165	a1i 11	. . . . . . . . . . . . . . . . . 18
167		elfzle1 12344	. . . . . . . . . . . . . . . . . 18
168	162, 163, 164, 166, 167	lemul2ad 10964	. . . . . . . . . . . . . . . . 17
169	160, 161, 162, 168	lesub1dd 10643	. . . . . . . . . . . . . . . 16
170	157, 169	syl5eqbr 4688	. . . . . . . . . . . . . . 15
171	170	adantl 482	. . . . . . . . . . . . . 14 $/\$
172	161	adantl 482	. . . . . . . . . . . . . . 15 $/\$
173	41	adantr 481	. . . . . . . . . . . . . . 15 $/\$
174		1red 10055	. . . . . . . . . . . . . . 15 $/\$
175	163	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
176	40	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
177	38	a1i 11	. . . . . . . . . . . . . . . 16 $/\$
178	165	a1i 11	. . . . . . . . . . . . . . . 16 $/\$
179		elfzle2 12345	. . . . . . . . . . . . . . . . 17
180	179	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
181	175, 176, 177, 178, 180	lemul2ad 10964	. . . . . . . . . . . . . . 15 $/\$
182	172, 173, 174, 181	lesub1dd 10643	. . . . . . . . . . . . . 14 $/\$
183	171, 182	jca 554	. . . . . . . . . . . . 13 $/\$ $/\$
184		elfz2 12333	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
185	156, 183, 184	sylanbrc 698	. . . . . . . . . . . 12 $/\$
186	152	zcnd 11483	. . . . . . . . . . . . . . . . . 18
187		1cnd 10056	. . . . . . . . . . . . . . . . . 18
188		2cnd 11093	. . . . . . . . . . . . . . . . . 18
189		2ne0 11113	. . . . . . . . . . . . . . . . . . 19
190	189	a1i 11	. . . . . . . . . . . . . . . . . 18
191	186, 187, 188, 190	divsubdird 10840	. . . . . . . . . . . . . . . . 17
192	151	zcnd 11483	. . . . . . . . . . . . . . . . . . 19
193	192, 188, 190	divcan3d 10806	. . . . . . . . . . . . . . . . . 18
194	193	oveq1d 6665	. . . . . . . . . . . . . . . . 17
195	191, 194	eqtrd 2656	. . . . . . . . . . . . . . . 16
196	151, 153	zsubcld 11487	. . . . . . . . . . . . . . . . . 18
197	164, 190	rereccld 10852	. . . . . . . . . . . . . . . . . . 19
198		halflt1 11250	. . . . . . . . . . . . . . . . . . . 20
199	198	a1i 11	. . . . . . . . . . . . . . . . . . 19
200	197, 162, 163, 199	ltsub2dd 10640	. . . . . . . . . . . . . . . . . 18
201		2rp 11837	. . . . . . . . . . . . . . . . . . . . 21
202		rpreccl 11857	. . . . . . . . . . . . . . . . . . . . 21
203	201, 202	mp1i 13	. . . . . . . . . . . . . . . . . . . 20
204	163, 203	ltsubrpd 11904	. . . . . . . . . . . . . . . . . . 19
205	192, 187	npcand 10396	. . . . . . . . . . . . . . . . . . 19
206	204, 205	breqtrrd 4681	. . . . . . . . . . . . . . . . . 18
207		btwnnz 11453	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
208	196, 200, 206, 207	syl3anc 1326	. . . . . . . . . . . . . . . . 17
209		nnz 11399	. . . . . . . . . . . . . . . . 17
210	208, 209	nsyl 135	. . . . . . . . . . . . . . . 16
211	195, 210	eqneltrd 2720	. . . . . . . . . . . . . . 15
212	211	intnand 962	. . . . . . . . . . . . . 14 $/\$
213		oveq1 6657	. . . . . . . . . . . . . . . 16
214	213	eleq1d 2686	. . . . . . . . . . . . . . 15
215	214	elrab 3363	. . . . . . . . . . . . . 14 $/\$
216	212, 215	sylnibr 319	. . . . . . . . . . . . 13
217	216	adantl 482	. . . . . . . . . . . 12 $/\$
218	185, 217	eldifd 3585	. . . . . . . . . . 11 $/\$ $\$
219		eqid 2622	. . . . . . . . . . 11
220	218, 219	fmptd 6385	. . . . . . . . . 10 $\$
221		eqidd 2623	. . . . . . . . . . . . . . . . . 18
222		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20
223	222	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19
224	223	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
225		id 22	. . . . . . . . . . . . . . . . . 18
226		ovexd 6680	. . . . . . . . . . . . . . . . . 18
227	221, 224, 225, 226	fvmptd 6288	. . . . . . . . . . . . . . . . 17
228	227	eqcomd 2628	. . . . . . . . . . . . . . . 16
229	228	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$
230		simpr 477	. . . . . . . . . . . . . . 15 $/\$ $/\$
231		eqidd 2623	. . . . . . . . . . . . . . . . 17
232		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
233	232	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
234	233	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
235		id 22	. . . . . . . . . . . . . . . . 17
236		ovexd 6680	. . . . . . . . . . . . . . . . 17
237	231, 234, 235, 236	fvmptd 6288	. . . . . . . . . . . . . . . 16
238	237	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ $/\$
239	229, 230, 238	3eqtrd 2660	. . . . . . . . . . . . . 14 $/\$ $/\$
240		2cnd 11093	. . . . . . . . . . . . . . . . . 18
241		elfzelz 12342	. . . . . . . . . . . . . . . . . . 19
242	241	zcnd 11483	. . . . . . . . . . . . . . . . . 18
243	240, 242	mulcld 10060	. . . . . . . . . . . . . . . . 17
244	243	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$
245		2cnd 11093	. . . . . . . . . . . . . . . . . 18
246		elfzelz 12342	. . . . . . . . . . . . . . . . . . 19
247	246	zcnd 11483	. . . . . . . . . . . . . . . . . 18
248	245, 247	mulcld 10060	. . . . . . . . . . . . . . . . 17
249	248	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$
250		1cnd 10056	. . . . . . . . . . . . . . . 16 $/\$ $/\$
251		simpr 477	. . . . . . . . . . . . . . . 16 $/\$ $/\$
252	244, 249, 250, 251	subcan2d 10434	. . . . . . . . . . . . . . 15 $/\$ $/\$
253	242	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$
254	247	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$
255		2cnd 11093	. . . . . . . . . . . . . . . 16 $/\$ $/\$
256	189	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
257		simpr 477	. . . . . . . . . . . . . . . 16 $/\$ $/\$
258	253, 254, 255, 256, 257	mulcanad 10662	. . . . . . . . . . . . . . 15 $/\$ $/\$
259	252, 258	syldan 487	. . . . . . . . . . . . . 14 $/\$ $/\$
260	239, 259	syldan 487	. . . . . . . . . . . . 13 $/\$ $/\$
261	260	adantll 750	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
262	261	ex 450	. . . . . . . . . . 11 $/\$ $/\$
263	262	ralrimivva 2971	. . . . . . . . . 10
264		dff13 6512	. . . . . . . . . 10 $\$ $\$ $/\$
265	220, 263, 264	sylanbrc 698	. . . . . . . . 9 $\$
266		1zzd 11408	. . . . . . . . . . . . . . . 16 $/\$ $\$
267	32	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $\$
268		fzssz 12343	. . . . . . . . . . . . . . . . . . . 20
269	268, 137	sseldi 3601	. . . . . . . . . . . . . . . . . . 19 $\$
270		zeo 11463	. . . . . . . . . . . . . . . . . . 19 $\/$
271	269, 270	syl 17	. . . . . . . . . . . . . . . . . 18 $\$ $\/$
272	271	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\/$
273		eldifn 3733	. . . . . . . . . . . . . . . . . . 19 $\$
274	137, 93	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $\$
275	274	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
276		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
277	275	nnred 11035	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
278	38	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
279	275	nngt0d 11064	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
280		2pos 11112	. . . . . . . . . . . . . . . . . . . . . . 23
281	280	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
282	277, 278, 279, 281	divgt0d 10959	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
283		elnnz 11387	. . . . . . . . . . . . . . . . . . . . 21 $/\$
284	276, 282, 283	sylanbrc 698	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
285		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
286	285	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . 21
287	286	elrab 3363	. . . . . . . . . . . . . . . . . . . 20 $/\$
288	275, 284, 287	sylanbrc 698	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
289	273, 288	mtand 691	. . . . . . . . . . . . . . . . . 18 $\$
290	289	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $\$
291		pm2.53 388	. . . . . . . . . . . . . . . . 17 $\/$
292	272, 290, 291	sylc 65	. . . . . . . . . . . . . . . 16 $/\$ $\$
293	266, 267, 292	3jca 1242	. . . . . . . . . . . . . . 15 $/\$ $\$ $/\$ $/\$
294		1p1e2 11134	. . . . . . . . . . . . . . . . . . . 20
295	294	oveq1i 6660	. . . . . . . . . . . . . . . . . . 19
296		2div2e1 11150	. . . . . . . . . . . . . . . . . . 19
297	295, 296	eqtr2i 2645	. . . . . . . . . . . . . . . . . 18
298		1red 10055	. . . . . . . . . . . . . . . . . . . 20
299	298, 298	readdcld 10069	. . . . . . . . . . . . . . . . . . 19
300	93	nnred 11035	. . . . . . . . . . . . . . . . . . . 20
301	300, 298	readdcld 10069	. . . . . . . . . . . . . . . . . . 19
302	201	a1i 11	. . . . . . . . . . . . . . . . . . 19
303		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20
304	298, 300, 298, 303	leadd1dd 10641	. . . . . . . . . . . . . . . . . . 19
305	299, 301, 302, 304	lediv1dd 11930	. . . . . . . . . . . . . . . . . 18
306	297, 305	syl5eqbr 4688	. . . . . . . . . . . . . . . . 17
307	137, 306	syl 17	. . . . . . . . . . . . . . . 16 $\$
308	307	adantl 482	. . . . . . . . . . . . . . 15 $/\$ $\$
309		elfzel2 12340	. . . . . . . . . . . . . . . . . . . . 21
310	309	zred 11482	. . . . . . . . . . . . . . . . . . . 20
311	310, 298	readdcld 10069	. . . . . . . . . . . . . . . . . . 19
312		elfzle2 12345	. . . . . . . . . . . . . . . . . . . 20
313	300, 310, 298, 312	leadd1dd 10641	. . . . . . . . . . . . . . . . . . 19
314	301, 311, 302, 313	lediv1dd 11930	. . . . . . . . . . . . . . . . . 18
315	314	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
316	50	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
317		1cnd 10056	. . . . . . . . . . . . . . . . . . . 20 $/\$
318	316, 317	npcand 10396	. . . . . . . . . . . . . . . . . . 19 $/\$
319	318	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 $/\$
320	189	a1i 11	. . . . . . . . . . . . . . . . . . . 20
321	44, 43, 320	divcan3d 10806	. . . . . . . . . . . . . . . . . . 19
322	321	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
323	319, 322	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$
324	315, 323	breqtrd 4679	. . . . . . . . . . . . . . . 16 $/\$
325	137, 324	sylan2 491	. . . . . . . . . . . . . . 15 $/\$ $\$
326	293, 308, 325	jca32 558	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $/\$ $/\$ $/\$
327		elfz2 12333	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
328	326, 327	sylibr 224	. . . . . . . . . . . . 13 $/\$ $\$
329	274	nncnd 11036	. . . . . . . . . . . . . . 15 $\$
330		peano2cn 10208	. . . . . . . . . . . . . . . . . 18
331		2cnd 11093	. . . . . . . . . . . . . . . . . 18
332	189	a1i 11	. . . . . . . . . . . . . . . . . 18
333	330, 331, 332	divcan2d 10803	. . . . . . . . . . . . . . . . 17
334	333	oveq1d 6665	. . . . . . . . . . . . . . . 16
335		pncan1 10454	. . . . . . . . . . . . . . . 16
336	334, 335	eqtr2d 2657	. . . . . . . . . . . . . . 15
337	329, 336	syl 17	. . . . . . . . . . . . . 14 $\$
338	337	adantl 482	. . . . . . . . . . . . 13 $/\$ $\$
339		oveq2 6658	. . . . . . . . . . . . . . . 16
340	339	oveq1d 6665	. . . . . . . . . . . . . . 15
341	340	eqeq2d 2632	. . . . . . . . . . . . . 14
342	341	rspcev 3309	. . . . . . . . . . . . 13 $/\$
343	328, 338, 342	syl2anc 693	. . . . . . . . . . . 12 $/\$ $\$
344		eqidd 2623	. . . . . . . . . . . . . . . . 17 $/\$
345		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
346	345	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
347	346	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
348		simpl 473	. . . . . . . . . . . . . . . . 17 $/\$
349		ovexd 6680	. . . . . . . . . . . . . . . . 17 $/\$
350	344, 347, 348, 349	fvmptd 6288	. . . . . . . . . . . . . . . 16 $/\$
351		id 22	. . . . . . . . . . . . . . . . . 18
352	351	eqcomd 2628	. . . . . . . . . . . . . . . . 17
353	352	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
354	350, 353	eqtr2d 2657	. . . . . . . . . . . . . . 15 $/\$
355	354	ex 450	. . . . . . . . . . . . . 14
356	355	adantl 482	. . . . . . . . . . . . 13 $/\$ $\$ $/\$
357	356	reximdva 3017	. . . . . . . . . . . 12 $/\$ $\$
358	343, 357	mpd 15	. . . . . . . . . . 11 $/\$ $\$
359	358	ralrimiva 2966	. . . . . . . . . 10 $\$
360		dffo3 6374	. . . . . . . . . 10 $\$ $\$ $/\$ $\$
361	220, 359, 360	sylanbrc 698	. . . . . . . . 9 $\$
362		df-f1o 5895	. . . . . . . . 9 $\$ $\$ $/\$ $\$
363	265, 361, 362	sylanbrc 698	. . . . . . . 8 $\$
364	363	adantl 482	. . . . . . 7 $/\$ $\$
365		eqidd 2623	. . . . . . . . 9
366		oveq2 6658	. . . . . . . . . . 11
367	366	oveq1d 6665	. . . . . . . . . 10
368	367	adantl 482	. . . . . . . . 9 $/\$
369		id 22	. . . . . . . . 9
370		ovexd 6680	. . . . . . . . 9
371	365, 368, 369, 370	fvmptd 6288	. . . . . . . 8
372	371	adantl 482	. . . . . . 7 $/\$ $/\$
373		eleq1 2689	. . . . . . . . . 10 $\$ $\$
374	373	anbi2d 740	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ $/\$ $\$
375	142	eleq1d 2686	. . . . . . . . 9
376	374, 375	imbi12d 334	. . . . . . . 8 $/\$ $/\$ $\$ $/\$ $/\$ $\$
377	376, 139	chvarv 2263	. . . . . . 7 $/\$ $/\$ $\$
378	146, 147, 364, 372, 377	fsumf1o 14454	. . . . . 6 $/\$ $\$
379	97, 145, 378	3eqtrrd 2661	. . . . 5 $/\$
380		ovex 6678	. . . . . . . . . 10
381	20	fvmpt2 6291	. . . . . . . . . 10 $/\$
382	380, 381	mpan2 707	. . . . . . . . 9
383	382	oveq2d 6666	. . . . . . . 8
384	383	eqcomd 2628	. . . . . . 7
385	384	sumeq1d 14431	. . . . . 6
386	385	adantl 482	. . . . 5 $/\$
387	379, 386	eqtrd 2656	. . . 4 $/\$
388		elfznn 12370	. . . . . . 7
389	388	adantl 482	. . . . . 6 $/\$ $/\$
390	12	adantr 481	. . . . . . . 8 $/\$
391	30	a1i 11	. . . . . . . . . . . 12
392		elfzelz 12342	. . . . . . . . . . . 12
393	391, 392	zmulcld 11488	. . . . . . . . . . 11
394		1zzd 11408	. . . . . . . . . . 11
395	393, 394	zsubcld 11487	. . . . . . . . . 10
396		0red 10041	. . . . . . . . . . 11
397	38	a1i 11	. . . . . . . . . . . . 13
398	24, 397	syl5eqel 2705	. . . . . . . . . . . 12
399		1red 10055	. . . . . . . . . . . 12
400	398, 399	resubcld 10458	. . . . . . . . . . 11
401	395	zred 11482	. . . . . . . . . . 11
402		0lt1 10550	. . . . . . . . . . . 12
403	157	a1i 11	. . . . . . . . . . . 12
404	402, 403	syl5breq 4690	. . . . . . . . . . 11
405	393	zred 11482	. . . . . . . . . . . 12
406	388	nnred 11035	. . . . . . . . . . . . 13
407	165	a1i 11	. . . . . . . . . . . . 13
408		elfzle1 12344	. . . . . . . . . . . . 13
409	399, 406, 397, 407, 408	lemul2ad 10964	. . . . . . . . . . . 12
410	398, 405, 399, 409	lesub1dd 10643	. . . . . . . . . . 11
411	396, 400, 401, 404, 410	ltletrd 10197	. . . . . . . . . 10
412		elnnz 11387	. . . . . . . . . 10 $/\$
413	395, 411, 412	sylanbrc 698	. . . . . . . . 9
414	413	adantl 482	. . . . . . . 8 $/\$
415	390, 414	ffvelrnd 6360	. . . . . . 7 $/\$
416	415	adantlr 751	. . . . . 6 $/\$ $/\$
417	59	fveq2d 6195	. . . . . . . 8
418	417	cbvmptv 4750	. . . . . . 7
419	418	fvmpt2 6291	. . . . . 6 $/\$
420	389, 416, 419	syl2anc 693	. . . . 5 $/\$ $/\$
421		simpr 477	. . . . . 6 $/\$
422	421, 8	syl6eleq 2711	. . . . 5 $/\$
423	420, 422, 416	fsumser 14461	. . . 4 $/\$
424		eqidd 2623	. . . . 5 $/\$ $/\$
425	159	a1i 11	. . . . . . . . . 10
426		1red 10055	. . . . . . . . . 10
427	165	a1i 11	. . . . . . . . . . 11
428		nnge1 11046	. . . . . . . . . . 11
429	426, 40, 39, 427, 428	lemul2ad 10964	. . . . . . . . . 10
430	425, 41, 426, 429	lesub1dd 10643	. . . . . . . . 9
431	157, 430	syl5eqbr 4688	. . . . . . . 8
432		eluz2 11693	. . . . . . . 8 $/\$ $/\$
433	36, 67, 431, 432	syl3anbrc 1246	. . . . . . 7
434	69, 433	eqeltrd 2701	. . . . . 6
435	434	adantl 482	. . . . 5 $/\$
436		simpll 790	. . . . . 6 $/\$ $/\$
437		simpr 477	. . . . . . . 8 $/\$
438	383	adantr 481	. . . . . . . 8 $/\$
439	437, 438	eleqtrd 2703	. . . . . . 7 $/\$
440	439	adantll 750	. . . . . 6 $/\$ $/\$
441	436, 440, 95	syl2anc 693	. . . . 5 $/\$ $/\$
442	424, 435, 441	fsumser 14461	. . . 4 $/\$
443	387, 423, 442	3eqtr3d 2664	. . 3 $/\$
444	1, 2, 6, 7, 8, 9, 11, 15, 16, 29, 75, 77, 443	climsuse 39840	. 2
445		eqidd 2623	. . . 4 $/\$
446	8, 9, 445, 13	isum 14450	. . 3
447		climrel 14223	. . . . . . 7
448	447	releldmi 5362	. . . . . 6
449	16, 448	syl 17	. . . . 5
450		climdm 14285	. . . . 5
451	449, 450	sylib 208	. . . 4
452		climuni 14283	. . . 4 $/\$
453	451, 16, 452	syl2anc 693	. . 3
454	447	a1i 11	. . . . . . . 8
455		releldm 5358	. . . . . . . 8 $/\$
456	454, 444, 455	syl2anc 693	. . . . . . 7
457		climdm 14285	. . . . . . 7
458	456, 457	sylib 208	. . . . . 6
459	418	a1i 11	. . . . . . . 8
460	459	seqeq3d 12809	. . . . . . 7
461	460	fveq2d 6195	. . . . . 6
462	458, 461	breqtrd 4679	. . . . 5
463		climuni 14283	. . . . 5 $/\$
464	444, 462, 463	syl2anc 693	. . . 4
465		eqidd 2623	. . . . . 6 $/\$
466		eqcom 2629	. . . . . . . 8
467		eqcom 2629	. . . . . . . 8
468	417, 466, 467	3imtr3i 280	. . . . . . 7
469	468	adantl 482	. . . . . 6 $/\$ $/\$
470	12	adantr 481	. . . . . . 7 $/\$
471	433, 8	syl6eleqr 2712	. . . . . . . 8
472	471	adantl 482	. . . . . . 7 $/\$
473	470, 472	ffvelrnd 6360	. . . . . 6 $/\$
474	465, 469, 421, 473	fvmptd 6288	. . . . 5 $/\$
475	8, 9, 474, 473	isum 14450	. . . 4
476	464, 475	eqtr4d 2659	. . 3
477	446, 453, 476	3eqtrd 2660	. 2
478	444, 477	jca 554	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915 class class class wbr 4653

cmpt 4729

cdm 5114

wrel 5119

wf 5884

wf1 5885

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cfn 7955

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cle 10075

cmin 10266

cdiv 10684

cn 11020

c2 11070

cz 11377

cuz 11687

crp 11832

cfz 12326

cseq 12801

cli 14215

csu 14416

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417

This theorem is referenced by: fouriersw 40448

W3C validator