rplogsumlem1 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > rplogsumlem1		Structured version Unicode version

Theorem rplogsumlem1 22692

Description: Lemma for rplogsum 22735. (Contributed by Mario Carneiro, 2-May-2016.)

**Assertion**
Ref	Expression
rplogsumlem1

Distinct variable group:

Proof of Theorem rplogsumlem1 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 11791	. . 3
2		elfzuz 11445	. . . . . . . 8
3		eluz2b2 10923	. . . . . . . . 9 $/\$
4	3	simplbi 457	. . . . . . . 8
5	2, 4	syl 16	. . . . . . 7
6	5	adantl 463	. . . . . 6 $/\$
7	6	nnrpd 11022	. . . . 5 $/\$
8	7	relogcld 22031	. . . 4 $/\$
9	2	adantl 463	. . . . . 6 $/\$
10		uz2m1nn 10925	. . . . . 6
11	9, 10	syl 16	. . . . 5 $/\$
12	6, 11	nnmulcld 10365	. . . 4 $/\$
13	8, 12	nndivred 10366	. . 3 $/\$
14	1, 13	fsumrecl 13207	. 2
15		2re 10387	. . . . 5
16	11	nnrpd 11022	. . . . . 6 $/\$
17	16	rpsqrcld 12894	. . . . 5 $/\$
18		rerpdivcl 11014	. . . . 5 $/\$
19	15, 17, 18	sylancr 658	. . . 4 $/\$
20	7	rpsqrcld 12894	. . . . 5 $/\$
21		rerpdivcl 11014	. . . . 5 $/\$
22	15, 20, 21	sylancr 658	. . . 4 $/\$
23	19, 22	resubcld 9772	. . 3 $/\$
24	1, 23	fsumrecl 13207	. 2
25	15	a1i 11	. 2
26	17	rpred 11023	. . . . 5 $/\$
27	6	nnred 10333	. . . . . . 7 $/\$
28		peano2rem 9671	. . . . . . . 8
29	27, 28	syl 16	. . . . . . 7 $/\$
30	27, 29	remulcld 9410	. . . . . 6 $/\$
31	30, 23	remulcld 9410	. . . . 5 $/\$
32	6	nncnd 10334	. . . . . . . 8 $/\$
33		ax-1cn 9336	. . . . . . . 8
34		npcan 9615	. . . . . . . 8 $/\$
35	32, 33, 34	sylancl 657	. . . . . . 7 $/\$
36	35	fveq2d 5692	. . . . . 6 $/\$
37	16	rpge0d 11027	. . . . . . 7 $/\$
38		loglesqr 22155	. . . . . . 7 $/\$
39	29, 37, 38	syl2anc 656	. . . . . 6 $/\$
40	36, 39	eqbrtrrd 4311	. . . . 5 $/\$
41	20	rpred 11023	. . . . . . . . . . 11 $/\$
42	41, 26	readdcld 9409	. . . . . . . . . 10 $/\$
43		remulcl 9363	. . . . . . . . . . 11 $/\$
44	41, 15, 43	sylancl 657	. . . . . . . . . 10 $/\$
45	41, 26	resubcld 9772	. . . . . . . . . 10 $/\$
46	27	lem1d 10262	. . . . . . . . . . . 12 $/\$
47	7	rpge0d 11027	. . . . . . . . . . . . 13 $/\$
48	29, 37, 27, 47	sqrled 12909	. . . . . . . . . . . 12 $/\$
49	46, 48	mpbid 210	. . . . . . . . . . 11 $/\$
50	41, 26	subge0d 9925	. . . . . . . . . . 11 $/\$
51	49, 50	mpbird 232	. . . . . . . . . 10 $/\$
52	26, 41, 41, 49	leadd2dd 9950	. . . . . . . . . . 11 $/\$
53	20	rpcnd 11025	. . . . . . . . . . . 12 $/\$
54	53	times2d 10564	. . . . . . . . . . 11 $/\$
55	52, 54	breqtrrd 4315	. . . . . . . . . 10 $/\$
56	42, 44, 45, 51, 55	lemul1ad 10268	. . . . . . . . 9 $/\$
57	32	sqsqrd 12921	. . . . . . . . . . 11 $/\$
58		subcl 9605	. . . . . . . . . . . . 13 $/\$
59	32, 33, 58	sylancl 657	. . . . . . . . . . . 12 $/\$
60	59	sqsqrd 12921	. . . . . . . . . . 11 $/\$
61	57, 60	oveq12d 6108	. . . . . . . . . 10 $/\$
62	17	rpcnd 11025	. . . . . . . . . . 11 $/\$
63		subsq 11969	. . . . . . . . . . 11 $/\$
64	53, 62, 63	syl2anc 656	. . . . . . . . . 10 $/\$
65		nncan 9634	. . . . . . . . . . 11 $/\$
66	32, 33, 65	sylancl 657	. . . . . . . . . 10 $/\$
67	61, 64, 66	3eqtr3d 2481	. . . . . . . . 9 $/\$
68		2cn 10388	. . . . . . . . . . 11
69	68	a1i 11	. . . . . . . . . 10 $/\$
70	45	recnd 9408	. . . . . . . . . 10 $/\$
71	53, 69, 70	mulassd 9405	. . . . . . . . 9 $/\$
72	56, 67, 71	3brtr3d 4318	. . . . . . . 8 $/\$
73		1red 9397	. . . . . . . . 9 $/\$
74		remulcl 9363	. . . . . . . . . . 11 $/\$
75	15, 45, 74	sylancr 658	. . . . . . . . . 10 $/\$
76	41, 75	remulcld 9410	. . . . . . . . 9 $/\$
77	73, 76, 17	lemul1d 11062	. . . . . . . 8 $/\$
78	72, 77	mpbid 210	. . . . . . 7 $/\$
79	62	mulid2d 9400	. . . . . . 7 $/\$
80	75	recnd 9408	. . . . . . . 8 $/\$
81	53, 80, 62	mul32d 9575	. . . . . . 7 $/\$
82	78, 79, 81	3brtr3d 4318	. . . . . 6 $/\$
83		remsqsqr 12742	. . . . . . . . . . 11 $/\$
84	27, 47, 83	syl2anc 656	. . . . . . . . . 10 $/\$
85		remsqsqr 12742	. . . . . . . . . . 11 $/\$
86	29, 37, 85	syl2anc 656	. . . . . . . . . 10 $/\$
87	84, 86	oveq12d 6108	. . . . . . . . 9 $/\$
88	53, 53, 62, 62	mul4d 9577	. . . . . . . . 9 $/\$
89	87, 88	eqtr3d 2475	. . . . . . . 8 $/\$
90	17	rpcnne0d 11032	. . . . . . . . . 10 $/\$ $/\$
91	20	rpcnne0d 11032	. . . . . . . . . 10 $/\$ $/\$
92		divsubdiv 10043	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
93	69, 69, 90, 91, 92	syl22anc 1214	. . . . . . . . 9 $/\$
94	69, 53, 62	subdid 9796	. . . . . . . . . 10 $/\$
95	53, 62	mulcomd 9403	. . . . . . . . . 10 $/\$
96	94, 95	oveq12d 6108	. . . . . . . . 9 $/\$
97	93, 96	eqtr4d 2476	. . . . . . . 8 $/\$
98	89, 97	oveq12d 6108	. . . . . . 7 $/\$
99	53, 62	mulcld 9402	. . . . . . . 8 $/\$
100	20, 17	rpmulcld 11039	. . . . . . . . . 10 $/\$
101	75, 100	rerpdivcld 11050	. . . . . . . . 9 $/\$
102	101	recnd 9408	. . . . . . . 8 $/\$
103	99, 99, 102	mulassd 9405	. . . . . . 7 $/\$
104	100	rpne0d 11028	. . . . . . . . 9 $/\$
105	80, 99, 104	divcan2d 10105	. . . . . . . 8 $/\$
106	105	oveq2d 6106	. . . . . . 7 $/\$
107	98, 103, 106	3eqtrd 2477	. . . . . 6 $/\$
108	82, 107	breqtrrd 4315	. . . . 5 $/\$
109	8, 26, 31, 40, 108	letrd 9524	. . . 4 $/\$
110	12	nngt0d 10361	. . . . 5 $/\$
111		ledivmul 10201	. . . . 5 $/\$ $/\$ $/\$
112	8, 23, 30, 110, 111	syl112anc 1217	. . . 4 $/\$
113	109, 112	mpbird 232	. . 3 $/\$
114	1, 13, 23, 113	fsumle 13258	. 2
115		oveq1 6097	. . . . . . 7
116	115	fveq2d 5692	. . . . . 6
117	116	oveq2d 6106	. . . . 5
118		oveq1 6097	. . . . . . 7
119	118	fveq2d 5692	. . . . . 6
120	119	oveq2d 6106	. . . . 5
121		oveq1 6097	. . . . . . . . . 10
122		2m1e1 10432	. . . . . . . . . 10
123	121, 122	syl6eq 2489	. . . . . . . . 9
124	123	fveq2d 5692	. . . . . . . 8
125		sqr1 12757	. . . . . . . 8
126	124, 125	syl6eq 2489	. . . . . . 7
127	126	oveq2d 6106	. . . . . 6
128	68	div1i 10055	. . . . . 6
129	127, 128	syl6eq 2489	. . . . 5
130		oveq1 6097	. . . . . . 7
131	130	fveq2d 5692	. . . . . 6
132	131	oveq2d 6106	. . . . 5
133		nnz 10664	. . . . 5
134		eluzp1p1 10882	. . . . . . 7
135		nnuz 10892	. . . . . . 7
136	134, 135	eleq2s 2533	. . . . . 6
137		df-2 10376	. . . . . . 7
138	137	fveq2i 5691	. . . . . 6
139	136, 138	syl6eleqr 2532	. . . . 5
140		elfzuz 11445	. . . . . . . . . . 11
141		uz2m1nn 10925	. . . . . . . . . . 11
142	140, 141	syl 16	. . . . . . . . . 10
143	142	adantl 463	. . . . . . . . 9 $/\$
144	143	nnrpd 11022	. . . . . . . 8 $/\$
145	144	rpsqrcld 12894	. . . . . . 7 $/\$
146		rerpdivcl 11014	. . . . . . 7 $/\$
147	15, 145, 146	sylancr 658	. . . . . 6 $/\$
148	147	recnd 9408	. . . . 5 $/\$
149	117, 120, 129, 132, 133, 139, 148	fsumtscop 13263	. . . 4
150		pncan 9612	. . . . . . . . 9 $/\$
151	32, 33, 150	sylancl 657	. . . . . . . 8 $/\$
152	151	fveq2d 5692	. . . . . . 7 $/\$
153	152	oveq2d 6106	. . . . . 6 $/\$
154	153	oveq2d 6106	. . . . 5 $/\$
155	154	sumeq2dv 13176	. . . 4
156		nncn 10326	. . . . . . . 8
157		pncan 9612	. . . . . . . 8 $/\$
158	156, 33, 157	sylancl 657	. . . . . . 7
159	158	fveq2d 5692	. . . . . 6
160	159	oveq2d 6106	. . . . 5
161	160	oveq2d 6106	. . . 4
162	149, 155, 161	3eqtr3d 2481	. . 3
163		2rp 10992	. . . . . 6
164		nnrp 10996	. . . . . . 7
165	164	rpsqrcld 12894	. . . . . 6
166		rpdivcl 11009	. . . . . 6 $/\$
167	163, 165, 166	sylancr 658	. . . . 5
168	167	rpge0d 11027	. . . 4
169	167	rpred 11023	. . . . 5
170		subge02 9851	. . . . 5 $/\$
171	15, 169, 170	sylancr 658	. . . 4
172	168, 171	mpbid 210	. . 3
173	162, 172	eqbrtrd 4309	. 2
174	14, 24, 25, 114, 173	letrd 9524	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1364

wcel 1761

wne 2604 class class class wbr 4289

cfv 5415 (class class class)co 6090

cc 9276

cr 9277

cc0 9278

c1 9279

caddc 9281

cmul 9283

clt 9414

cle 9415

cmin 9591

cdiv 9989

cn 10318

c2 10367

cuz 10857

crp 10987

cfz 11433

cexp 11861

csqr 12718

csu 13159

clog 21965

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-inf2 7843 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356 ax-addf 9357 ax-mulf 9358

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-fal 1370 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-iin 4171 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-se 4676 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-isom 5424 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-of 6319 df-om 6476 df-1st 6576 df-2nd 6577 df-supp 6690 df-recs 6828 df-rdg 6862 df-1o 6916 df-2o 6917 df-oadd 6920 df-er 7097 df-map 7212 df-pm 7213 df-ixp 7260 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-fsupp 7617 df-fi 7657 df-sup 7687 df-oi 7720 df-card 8105 df-cda 8333 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-2 10376 df-3 10377 df-4 10378 df-5 10379 df-6 10380 df-7 10381 df-8 10382 df-9 10383 df-10 10384 df-n0 10576 df-z 10643 df-dec 10752 df-uz 10858 df-q 10950 df-rp 10988 df-xneg 11085 df-xadd 11086 df-xmul 11087 df-ioo 11300 df-ioc 11301 df-ico 11302 df-icc 11303 df-fz 11434 df-fzo 11545 df-fl 11638 df-mod 11705 df-seq 11803 df-exp 11862 df-fac 12048 df-bc 12075 df-hash 12100 df-shft 12552 df-cj 12584 df-re 12585 df-im 12586 df-sqr 12720 df-abs 12721 df-limsup 12945 df-clim 12962 df-rlim 12963 df-sum 13160 df-ef 13349 df-sin 13351 df-cos 13352 df-tan 13353 df-pi 13354 df-struct 14172 df-ndx 14173 df-slot 14174 df-base 14175 df-sets 14176 df-ress 14177 df-plusg 14247 df-mulr 14248 df-starv 14249 df-sca 14250 df-vsca 14251 df-ip 14252 df-tset 14253 df-ple 14254 df-ds 14256 df-unif 14257 df-hom 14258 df-cco 14259 df-rest 14357 df-topn 14358 df-0g 14376 df-gsum 14377 df-topgen 14378 df-pt 14379 df-prds 14382 df-xrs 14436 df-qtop 14441 df-imas 14442 df-xps 14444 df-mre 14520 df-mrc 14521 df-acs 14523 df-mnd 15411 df-submnd 15461 df-mulg 15541 df-cntz 15828 df-cmn 16272 df-psmet 17768 df-xmet 17769 df-met 17770 df-bl 17771 df-mopn 17772 df-fbas 17773 df-fg 17774 df-cnfld 17778 df-top 18462 df-bases 18464 df-topon 18465 df-topsp 18466 df-cld 18582 df-ntr 18583 df-cls 18584 df-nei 18661 df-lp 18699 df-perf 18700 df-cn 18790 df-cnp 18791 df-haus 18878 df-cmp 18949 df-tx 19094 df-hmeo 19287 df-fil 19378 df-fm 19470 df-flim 19471 df-flf 19472 df-xms 19854 df-ms 19855 df-tms 19856 df-cncf 20413 df-limc 21300 df-dv 21301 df-log 21967 df-cxp 21968

This theorem is referenced by: rplogsumlem2 22693

W3C validator