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 28124

Description: Lemma for eulerpart 28146. (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 28123	. . . . 5
4	3	ffvelrni 6031	. . . 4
5		nndiffz1 27419	. . . . 5 $\$
6	5	eleq2d 2537	. . . 4 $\$
7	4, 6	syl 16	. . 3 $\$
8	7	pm5.32i 637	. 2 $/\$ $\$ $/\$
9		simpr 461	. . . . . 6 $/\$ $\$ $\$
10		eldif 3491	. . . . . 6 $\$ $/\$
11	9, 10	sylib 196	. . . . 5 $/\$ $\$ $/\$
12	11	simpld 459	. . . 4 $/\$ $\$
13	1, 2	eulerpartlemelr 28121	. . . . . 6 $/\$
14	13	simpld 459	. . . . 5
15	14	ffvelrnda 6032	. . . 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 11129	. . . . . . . . . 10
22	20, 21	syl6eleq 2565	. . . . . . . . 9 $/\$
23		simpr 461	. . . . . . . . . 10 $/\$
24	23	nn0zd 10976	. . . . . . . . 9 $/\$
25		elfz5 11692	. . . . . . . . 9 $/\$
26	22, 24, 25	syl2anc 661	. . . . . . . 8 $/\$
27	26	notbid 294	. . . . . . 7 $/\$
28	23	nn0red 10865	. . . . . . . 8 $/\$
29	20	nnred 10563	. . . . . . . 8 $/\$
30	28, 29	ltnled 9743	. . . . . . 7 $/\$
31	27, 30	bitr4d 256	. . . . . 6 $/\$
32	31	biimpa 484	. . . . 5 $/\$ $/\$
33	12, 18, 19, 32	syl21anc 1227	. . . 4 $/\$ $\$
34		fveq2 5872	. . . . . . . . . . . 12
35		id 22	. . . . . . . . . . . 12
36	34, 35	oveq12d 6313	. . . . . . . . . . 11
37	36	cbvsumv 13498	. . . . . . . . . 10
38	1, 2	eulerpartlemsv1 28120	. . . . . . . . . . 11
39	38	eqcomd 2475	. . . . . . . . . 10
40	37, 39	syl5eqr 2522	. . . . . . . . 9
41		breq2 4457	. . . . . . . . . . . . 13
42		fveq2 5872	. . . . . . . . . . . . . 14
43	42	breq2d 4465	. . . . . . . . . . . . 13
44	41, 43	anbi12d 710	. . . . . . . . . . . 12 $/\$ $/\$
45	44	cbvrexv 3094	. . . . . . . . . . 11 $/\$ $/\$
46	4	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$
47	46	nn0red 10865	. . . . . . . . . . . . 13 $/\$ $/\$
48	4	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
49	48	nn0red 10865	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
50		simpr 461	. . . . . . . . . . . . . . . . . . . 20 $/\$
51	50	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
52	51	nnred 10563	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
53		1z 10906	. . . . . . . . . . . . . . . . . . . . 21
54	53	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
55	14	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
56		simpr 461	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
57		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
58		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
59	58	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
60	59, 58	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
61		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
62		ffvelrn 6030	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
63	61	nnnn0d 10864	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
64	62, 63	nn0mulcld 10869	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
65	57, 60, 61, 64	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . 21 $/\$
66	55, 56, 65	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
67	14	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
68	67	ffvelrnda 6032	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
69	56	nnnn0d 10864	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
70	68, 69	nn0mulcld 10869	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
71	70	nn0red 10865	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
72		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . 25
73		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25
74	72, 73	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . 24
75	74	cbvmptv 4544	. . . . . . . . . . . . . . . . . . . . . . 23
76	70, 75	fmptd 6056	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
77		nn0sscn 10812	. . . . . . . . . . . . . . . . . . . . . 22
78		fss 5745	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
79	76, 77, 78	sylancl 662	. . . . . . . . . . . . . . . . . . . . 21 $/\$
80		nnex 10554	. . . . . . . . . . . . . . . . . . . . . . . 24
81		0nn0 10822	. . . . . . . . . . . . . . . . . . . . . . . 24
82		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
83	82	ffs2 27374	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ supp $\$
84	80, 81, 83	mp3an12 1314	. . . . . . . . . . . . . . . . . . . . . . 23 supp $\$
85	79, 84	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ supp $\$
86		frnnn0supp 10861	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2555	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ supp
92	80	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
93	81	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
94		ffn 5737	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		simp3 998	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
96	95	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
97		simp2 997	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
98	97	nncnd 10564	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
99	98	mul02d 9789	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
100	96, 99	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
101	75, 92, 93, 94, 100	suppss3 27373	. . . . . . . . . . . . . . . . . . . . . . . 24 supp supp
102	67, 101	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ supp supp
103		ssfi 7752	. . . . . . . . . . . . . . . . . . . . . . 23 supp $/\$ supp supp supp
104	91, 102, 103	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ supp
105	85, 104	eqeltrrd 2556	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$
106	21, 54, 79, 105	fsumcvg4 27757	. . . . . . . . . . . . . . . . . . . 20 $/\$
107	21, 54, 66, 71, 106	isumrecl 13560	. . . . . . . . . . . . . . . . . . 19 $/\$
108	107	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
109		simprl 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
110	14	ffvelrnda 6032	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
111	110	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
112	111	nn0red 10865	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
113	112, 52	remulcld 9636	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
114	51	nnnn0d 10864	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
115		nn0ge0 10833	. . . . . . . . . . . . . . . . . . . . 21
116	114, 115	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
117		simprr 756	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
118		elnnnn0b 10852	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
119		nnge1 10574	. . . . . . . . . . . . . . . . . . . . . 22
120	118, 119	sylbir 213	. . . . . . . . . . . . . . . . . . . . 21 $/\$
121	111, 117, 120	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
122	52, 112, 116, 121	lemulge12d 10496	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
123	110	nn0cnd 10866	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
124	50	nncnd 10564	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
125	123, 124	mulcld 9628	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
126		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24
127	42, 126	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . 23
128	127	sumsn 13543	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
129	50, 125, 128	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$
130		snfi 7608	. . . . . . . . . . . . . . . . . . . . . . 23
131	130	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
132	50	snssd 4178	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
133	70	nn0ge0d 10867	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
134	21, 54, 131, 132, 66, 71, 133, 106	isumless 13637	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	129, 134	eqbrtrrd 4475	. . . . . . . . . . . . . . . . . . . 20 $/\$
136	135	adantr 465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
137	52, 113, 108, 122, 136	letrd 9750	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
138	49, 52, 108, 109, 137	ltletrd 9753	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
139	138	ex 434	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140	139	rexlimdva 2959	. . . . . . . . . . . . . . 15 $/\$
141	140	imp 429	. . . . . . . . . . . . . 14 $/\$ $/\$
142	127	cbvsumv 13498	. . . . . . . . . . . . . 14
143	141, 142	syl6breq 4492	. . . . . . . . . . . . 13 $/\$ $/\$
144		ltne 9693	. . . . . . . . . . . . . 14 $/\$
145	142	neeq1i 2752	. . . . . . . . . . . . . 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 2682	. . . . . . . . 9 $/\$
151	40, 150	mpd 15	. . . . . . . 8 $/\$
152		ralnex 2913	. . . . . . . 8 $/\$ $/\$
153	151, 152	sylibr 212	. . . . . . 7 $/\$
154		imnan 422	. . . . . . . 8 $/\$
155	154	ralbii 2898	. . . . . . 7 $/\$
156	153, 155	sylibr 212	. . . . . 6
157	156	r19.21bi 2836	. . . . 5 $/\$
158	157	imp 429	. . . 4 $/\$ $/\$
159	17, 12, 33, 158	syl21anc 1227	. . 3 $/\$ $\$
160		nn0re 10816	. . . . . 6
161		0re 9608	. . . . . . 7
162	161	a1i 11	. . . . . 6
163	160, 162	lenltd 9742	. . . . 5
164		nn0le0eq0 10836	. . . . 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 973

wceq 1379

wcel 1767

cab 2452

wne 2662

wral 2817

wrex 2818

cvv 3118 $\$ cdif 3478

cin 3480

wss 3481

csn 4033 class class class wbr 4453

cmpt 4511

ccnv 5004

cima 5008

wf 5590

cfv 5594 (class class class)co 6295 supp csupp 6913

cmap 7432

cfn 7528

cc 9502

cr 9503

cc0 9504

c1 9505

caddc 9507

cmul 9509

clt 9640

cle 9641

cn 10548

cn0 10807

cz 10876

cuz 11094

cfz 11684

csu 13488

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4564 ax-sep 4574 ax-nul 4582 ax-pow 4631 ax-pr 4692 ax-un 6587 ax-inf2 8070 ax-cnex 9560 ax-resscn 9561 ax-1cn 9562 ax-icn 9563 ax-addcl 9564 ax-addrcl 9565 ax-mulcl 9566 ax-mulrcl 9567 ax-mulcom 9568 ax-addass 9569 ax-mulass 9570 ax-distr 9571 ax-i2m1 9572 ax-1ne0 9573 ax-1rid 9574 ax-rnegex 9575 ax-rrecex 9576 ax-cnre 9577 ax-pre-lttri 9578 ax-pre-lttrn 9579 ax-pre-ltadd 9580 ax-pre-mulgt0 9581 ax-pre-sup 9582

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2822 df-rex 2823 df-reu 2824 df-rmo 2825 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-pss 3497 df-nul 3791 df-if 3946 df-pw 4018 df-sn 4034 df-pr 4036 df-tp 4038 df-op 4040 df-uni 4252 df-int 4289 df-iun 4333 df-br 4454 df-opab 4512 df-mpt 4513 df-tr 4547 df-eprel 4797 df-id 4801 df-po 4806 df-so 4807 df-fr 4844 df-se 4845 df-we 4846 df-ord 4887 df-on 4888 df-lim 4889 df-suc 4890 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6256 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6696 df-1st 6795 df-2nd 6796 df-supp 6914 df-recs 7054 df-rdg 7088 df-1o 7142 df-oadd 7146 df-er 7323 df-map 7434 df-pm 7435 df-en 7529 df-dom 7530 df-sdom 7531 df-fin 7532 df-sup 7913 df-oi 7947 df-card 8332 df-pnf 9642 df-mnf 9643 df-xr 9644 df-ltxr 9645 df-le 9646 df-sub 9819 df-neg 9820 df-div 10219 df-nn 10549 df-2 10606 df-3 10607 df-n0 10808 df-z 10877 df-uz 11095 df-rp 11233 df-fz 11685 df-fzo 11805 df-fl 11909 df-seq 12088 df-exp 12147 df-hash 12386 df-cj 12912 df-re 12913 df-im 12914 df-sqrt 13048 df-abs 13049 df-clim 13291 df-rlim 13292 df-sum 13489

This theorem is referenced by: eulerpartlemsv3 28125 eulerpartlemgc 28126

W3C validator