eulerpartlems - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > eulerpartlems		Structured version Unicode version

Theorem eulerpartlems 26748

Description: Lemma for eulerpart 26770. (Contributed by Thierry Arnoux, 6-Aug-2018.) (Revised by Thierry Arnoux, 1-Sep-2019.)

**Hypotheses**
Ref	Expression
eulerpartlems.r
eulerpartlems.s

**Assertion**
Ref	Expression
eulerpartlems	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem eulerpartlems Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eulerpartlems.r	. . . . . 6
2		eulerpartlems.s	. . . . . 6
3	1, 2	eulerpartlemsf 26747	. . . . 5
4	3	ffvelrni 5847	. . . 4
5		nndiffz1 26080	. . . . 5 $\$
6	5	eleq2d 2510	. . . 4 $\$
7	4, 6	syl 16	. . 3 $\$
8	7	pm5.32i 637	. 2 $/\$ $\$ $/\$
9		simpr 461	. . . . . 6 $/\$ $\$ $\$
10		eldif 3343	. . . . . 6 $\$ $/\$
11	9, 10	sylib 196	. . . . 5 $/\$ $\$ $/\$
12	11	simpld 459	. . . 4 $/\$ $\$
13	1, 2	eulerpartlemelr 26745	. . . . . 6 $/\$
14	13	simpld 459	. . . . 5
15	14	ffvelrnda 5848	. . . 4 $/\$
16	12, 15	syldan 470	. . 3 $/\$ $\$
17		simpl 457	. . . 4 $/\$ $\$
18	4	adantr 465	. . . . 5 $/\$ $\$
19	11	simprd 463	. . . . 5 $/\$ $\$
20		simpl 457	. . . . . . . . . 10 $/\$
21		nnuz 10901	. . . . . . . . . 10
22	20, 21	syl6eleq 2533	. . . . . . . . 9 $/\$
23		simpr 461	. . . . . . . . . 10 $/\$
24	23	nn0zd 10750	. . . . . . . . 9 $/\$
25		elfz5 11450	. . . . . . . . 9 $/\$
26	22, 24, 25	syl2anc 661	. . . . . . . 8 $/\$
27	26	notbid 294	. . . . . . 7 $/\$
28	23	nn0red 10642	. . . . . . . 8 $/\$
29	20	nnred 10342	. . . . . . . 8 $/\$
30	28, 29	ltnled 9526	. . . . . . 7 $/\$
31	27, 30	bitr4d 256	. . . . . 6 $/\$
32	31	biimpa 484	. . . . 5 $/\$ $/\$
33	12, 18, 19, 32	syl21anc 1217	. . . 4 $/\$ $\$
34		fveq2 5696	. . . . . . . . . . . 12
35		id 22	. . . . . . . . . . . 12
36	34, 35	oveq12d 6114	. . . . . . . . . . 11
37	36	cbvsumv 13178	. . . . . . . . . 10
38	1, 2	eulerpartlemsv1 26744	. . . . . . . . . . 11
39	38	eqcomd 2448	. . . . . . . . . 10
40	37, 39	syl5eqr 2489	. . . . . . . . 9
41		breq2 4301	. . . . . . . . . . . . 13
42		fveq2 5696	. . . . . . . . . . . . . 14
43	42	breq2d 4309	. . . . . . . . . . . . 13
44	41, 43	anbi12d 710	. . . . . . . . . . . 12 $/\$ $/\$
45	44	cbvrexv 2953	. . . . . . . . . . 11 $/\$ $/\$
46	4	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$
47	46	nn0red 10642	. . . . . . . . . . . . 13 $/\$ $/\$
48	4	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
49	48	nn0red 10642	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
50		simpr 461	. . . . . . . . . . . . . . . . . . . 20 $/\$
51	50	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
52	51	nnred 10342	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
53		1z 10681	. . . . . . . . . . . . . . . . . . . . 21
54	53	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
55	14	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
56		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
57		eqidd 2444	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
58		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
59	58	fveq2d 5700	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
60	59, 58	oveq12d 6114	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
61		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
62		ffvelrn 5846	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
63	61	nnnn0d 10641	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
64	62, 63	nn0mulcld 10646	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
65	57, 60, 61, 64	fvmptd 5784	. . . . . . . . . . . . . . . . . . . . 21 $/\$
66	55, 56, 65	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
67	14	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
68	67	ffvelrnda 5848	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
69	56	nnnn0d 10641	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
70	68, 69	nn0mulcld 10646	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
71	70	nn0red 10642	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
72		fveq2 5696	. . . . . . . . . . . . . . . . . . . . . . . . 25
73		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25
74	72, 73	oveq12d 6114	. . . . . . . . . . . . . . . . . . . . . . . 24
75	74	cbvmptv 4388	. . . . . . . . . . . . . . . . . . . . . . 23
76	70, 75	fmptd 5872	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
77		nn0sscn 10589	. . . . . . . . . . . . . . . . . . . . . 22
78		fss 5572	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
79	76, 77, 78	sylancl 662	. . . . . . . . . . . . . . . . . . . . 21 $/\$
80		nnex 10333	. . . . . . . . . . . . . . . . . . . . . . . 24
81		0nn0 10599	. . . . . . . . . . . . . . . . . . . . . . . 24
82		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
83	82	ffs2 26033	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ supp $\$
84	80, 81, 83	mp3an12 1304	. . . . . . . . . . . . . . . . . . . . . . 23 supp $\$
85	79, 84	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ supp $\$
86		frnnn0supp 10638	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ supp
87	80, 86	mpan 670	. . . . . . . . . . . . . . . . . . . . . . . . 25 supp
88	67, 87	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ supp
89	13	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	89	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
91	88, 90	eqeltrd 2517	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ supp
92	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
93	81	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
94		ffn 5564	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		simp3 990	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
96	95	oveq1d 6111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
97		simp2 989	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
98	97	nncnd 10343	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
99	98	mul02d 9572	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
100	96, 99	eqtrd 2475	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
101	75, 92, 93, 94, 100	suppss3 26032	. . . . . . . . . . . . . . . . . . . . . . . 24 supp supp
102	67, 101	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ supp supp
103		ssfi 7538	. . . . . . . . . . . . . . . . . . . . . . 23 supp $/\$ supp supp supp
104	91, 102, 103	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ supp
105	85, 104	eqeltrrd 2518	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$
106	21, 54, 79, 105	fsumcvg4 26385	. . . . . . . . . . . . . . . . . . . 20 $/\$
107	21, 54, 66, 71, 106	isumrecl 13237	. . . . . . . . . . . . . . . . . . 19 $/\$
108	107	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
109		simprl 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
110	14	ffvelrnda 5848	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
111	110	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
112	111	nn0red 10642	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
113	112, 52	remulcld 9419	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
114	51	nnnn0d 10641	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
115		nn0ge0 10610	. . . . . . . . . . . . . . . . . . . . 21
116	114, 115	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
117		simprr 756	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
118		elnnnn0b 10629	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
119		nnge1 10353	. . . . . . . . . . . . . . . . . . . . . 22
120	118, 119	sylbir 213	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	111, 117, 120	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
122	52, 112, 116, 121	lemulge12d 10276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
123	110	nn0cnd 10643	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
124	50	nncnd 10343	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
125	123, 124	mulcld 9411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
126		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24
127	42, 126	oveq12d 6114	. . . . . . . . . . . . . . . . . . . . . . 23
128	127	sumsn 13222	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
129	50, 125, 128	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$
130		snfi 7395	. . . . . . . . . . . . . . . . . . . . . . 23
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
132	50	snssd 4023	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
133	70	nn0ge0d 10644	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
134	21, 54, 131, 132, 66, 71, 133, 106	isumless 13313	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	129, 134	eqbrtrrd 4319	. . . . . . . . . . . . . . . . . . . 20 $/\$
136	135	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	52, 113, 108, 122, 136	letrd 9533	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
138	49, 52, 108, 109, 137	ltletrd 9536	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
139	138	ex 434	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140	139	rexlimdva 2846	. . . . . . . . . . . . . . 15 $/\$
141	140	imp 429	. . . . . . . . . . . . . 14 $/\$ $/\$
142	127	cbvsumv 13178	. . . . . . . . . . . . . 14
143	141, 142	syl6breq 4336	. . . . . . . . . . . . 13 $/\$ $/\$
144		ltne 9476	. . . . . . . . . . . . . 14 $/\$
145	142	neeq1i 2623	. . . . . . . . . . . . . 14
146	144, 145	sylibr 212	. . . . . . . . . . . . 13 $/\$
147	47, 143, 146	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
148	147	ex 434	. . . . . . . . . . 11 $/\$
149	45, 148	syl5bi 217	. . . . . . . . . 10 $/\$
150	149	necon2bd 2665	. . . . . . . . 9 $/\$
151	40, 150	mpd 15	. . . . . . . 8 $/\$
152		ralnex 2730	. . . . . . . 8 $/\$ $/\$
153	151, 152	sylibr 212	. . . . . . 7 $/\$
154		imnan 422	. . . . . . . 8 $/\$
155	154	ralbii 2744	. . . . . . 7 $/\$
156	153, 155	sylibr 212	. . . . . 6
157	156	r19.21bi 2819	. . . . 5 $/\$
158	157	imp 429	. . . 4 $/\$ $/\$
159	17, 12, 33, 158	syl21anc 1217	. . 3 $/\$ $\$
160		nn0re 10593	. . . . . 6
161		0re 9391	. . . . . . 7
162	161	a1i 11	. . . . . 6
163	160, 162	lenltd 9525	. . . . 5
164		nn0le0eq0 10613	. . . . 5
165	163, 164	bitr3d 255	. . . 4
166	165	biimpa 484	. . 3 $/\$
167	16, 159, 166	syl2anc 661	. 2 $/\$ $\$
168	8, 167	sylbir 213	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

cab 2429

wne 2611

wral 2720

wrex 2721

cvv 2977 $\$ cdif 3330

cin 3332

wss 3333

csn 3882 class class class wbr 4297

cmpt 4355

ccnv 4844

cima 4848

wf 5419

cfv 5423 (class class class)co 6096 supp csupp 6695

cmap 7219

cfn 7315

cc 9285

cr 9286

cc0 9287

c1 9288

caddc 9290

cmul 9292

clt 9423

cle 9424

cn 10327

cn0 10584

cz 10651

cuz 10866

cfz 11442

csu 13168

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4408 ax-sep 4418 ax-nul 4426 ax-pow 4475 ax-pr 4536 ax-un 6377 ax-inf2 7852 ax-cnex 9343 ax-resscn 9344 ax-1cn 9345 ax-icn 9346 ax-addcl 9347 ax-addrcl 9348 ax-mulcl 9349 ax-mulrcl 9350 ax-mulcom 9351 ax-addass 9352 ax-mulass 9353 ax-distr 9354 ax-i2m1 9355 ax-1ne0 9356 ax-1rid 9357 ax-rnegex 9358 ax-rrecex 9359 ax-cnre 9360 ax-pre-lttri 9361 ax-pre-lttrn 9362 ax-pre-ltadd 9363 ax-pre-mulgt0 9364 ax-pre-sup 9365

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2573 df-ne 2613 df-nel 2614 df-ral 2725 df-rex 2726 df-reu 2727 df-rmo 2728 df-rab 2729 df-v 2979 df-sbc 3192 df-csb 3294 df-dif 3336 df-un 3338 df-in 3340 df-ss 3347 df-pss 3349 df-nul 3643 df-if 3797 df-pw 3867 df-sn 3883 df-pr 3885 df-tp 3887 df-op 3889 df-uni 4097 df-int 4134 df-iun 4178 df-br 4298 df-opab 4356 df-mpt 4357 df-tr 4391 df-eprel 4637 df-id 4641 df-po 4646 df-so 4647 df-fr 4684 df-se 4685 df-we 4686 df-ord 4727 df-on 4728 df-lim 4729 df-suc 4730 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5386 df-fun 5425 df-fn 5426 df-f 5427 df-f1 5428 df-fo 5429 df-f1o 5430 df-fv 5431 df-isom 5432 df-riota 6057 df-ov 6099 df-oprab 6100 df-mpt2 6101 df-om 6482 df-1st 6582 df-2nd 6583 df-supp 6696 df-recs 6837 df-rdg 6871 df-1o 6925 df-oadd 6929 df-er 7106 df-map 7221 df-pm 7222 df-en 7316 df-dom 7317 df-sdom 7318 df-fin 7319 df-sup 7696 df-oi 7729 df-card 8114 df-pnf 9425 df-mnf 9426 df-xr 9427 df-ltxr 9428 df-le 9429 df-sub 9602 df-neg 9603 df-div 9999 df-nn 10328 df-2 10385 df-3 10386 df-n0 10585 df-z 10652 df-uz 10867 df-rp 10997 df-fz 11443 df-fzo 11554 df-fl 11647 df-seq 11812 df-exp 11871 df-hash 12109 df-cj 12593 df-re 12594 df-im 12595 df-sqr 12729 df-abs 12730 df-clim 12971 df-rlim 12972 df-sum 13169

This theorem is referenced by: eulerpartlemsv3 26749 eulerpartlemgc 26750

W3C validator