rplogsumlem1 - Metamath Proof Explorer

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

Theorem rplogsumlem1 23397

Description: Lemma for rplogsum 23440. (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 12047	. . 3
2		elfzuz 11680	. . . . . . . 8
3		eluz2b2 11150	. . . . . . . . 9 $/\$
4	3	simplbi 460	. . . . . . . 8
5	2, 4	syl 16	. . . . . . 7
6	5	adantl 466	. . . . . 6 $/\$
7	6	nnrpd 11251	. . . . 5 $/\$
8	7	relogcld 22736	. . . 4 $/\$
9	2	adantl 466	. . . . . 6 $/\$
10		uz2m1nn 11152	. . . . . 6
11	9, 10	syl 16	. . . . 5 $/\$
12	6, 11	nnmulcld 10579	. . . 4 $/\$
13	8, 12	nndivred 10580	. . 3 $/\$
14	1, 13	fsumrecl 13515	. 2
15		2re 10601	. . . . 5
16	11	nnrpd 11251	. . . . . 6 $/\$
17	16	rpsqrtcld 13202	. . . . 5 $/\$
18		rerpdivcl 11243	. . . . 5 $/\$
19	15, 17, 18	sylancr 663	. . . 4 $/\$
20	7	rpsqrtcld 13202	. . . . 5 $/\$
21		rerpdivcl 11243	. . . . 5 $/\$
22	15, 20, 21	sylancr 663	. . . 4 $/\$
23	19, 22	resubcld 9983	. . 3 $/\$
24	1, 23	fsumrecl 13515	. 2
25	15	a1i 11	. 2
26	17	rpred 11252	. . . . 5 $/\$
27	6	nnred 10547	. . . . . . 7 $/\$
28		peano2rem 9882	. . . . . . . 8
29	27, 28	syl 16	. . . . . . 7 $/\$
30	27, 29	remulcld 9620	. . . . . 6 $/\$
31	30, 23	remulcld 9620	. . . . 5 $/\$
32	6	nncnd 10548	. . . . . . . 8 $/\$
33		ax-1cn 9546	. . . . . . . 8
34		npcan 9825	. . . . . . . 8 $/\$
35	32, 33, 34	sylancl 662	. . . . . . 7 $/\$
36	35	fveq2d 5868	. . . . . 6 $/\$
37	16	rpge0d 11256	. . . . . . 7 $/\$
38		loglesqrt 22860	. . . . . . 7 $/\$
39	29, 37, 38	syl2anc 661	. . . . . 6 $/\$
40	36, 39	eqbrtrrd 4469	. . . . 5 $/\$
41	20	rpred 11252	. . . . . . . . . . 11 $/\$
42	41, 26	readdcld 9619	. . . . . . . . . 10 $/\$
43		remulcl 9573	. . . . . . . . . . 11 $/\$
44	41, 15, 43	sylancl 662	. . . . . . . . . 10 $/\$
45	41, 26	resubcld 9983	. . . . . . . . . 10 $/\$
46	27	lem1d 10475	. . . . . . . . . . . 12 $/\$
47	7	rpge0d 11256	. . . . . . . . . . . . 13 $/\$
48	29, 37, 27, 47	sqrtled 13217	. . . . . . . . . . . 12 $/\$
49	46, 48	mpbid 210	. . . . . . . . . . 11 $/\$
50	41, 26	subge0d 10138	. . . . . . . . . . 11 $/\$
51	49, 50	mpbird 232	. . . . . . . . . 10 $/\$
52	26, 41, 41, 49	leadd2dd 10163	. . . . . . . . . . 11 $/\$
53	20	rpcnd 11254	. . . . . . . . . . . 12 $/\$
54	53	times2d 10778	. . . . . . . . . . 11 $/\$
55	52, 54	breqtrrd 4473	. . . . . . . . . 10 $/\$
56	42, 44, 45, 51, 55	lemul1ad 10481	. . . . . . . . 9 $/\$
57	32	sqsqrtd 13229	. . . . . . . . . . 11 $/\$
58		subcl 9815	. . . . . . . . . . . . 13 $/\$
59	32, 33, 58	sylancl 662	. . . . . . . . . . . 12 $/\$
60	59	sqsqrtd 13229	. . . . . . . . . . 11 $/\$
61	57, 60	oveq12d 6300	. . . . . . . . . 10 $/\$
62	17	rpcnd 11254	. . . . . . . . . . 11 $/\$
63		subsq 12239	. . . . . . . . . . 11 $/\$
64	53, 62, 63	syl2anc 661	. . . . . . . . . 10 $/\$
65		nncan 9844	. . . . . . . . . . 11 $/\$
66	32, 33, 65	sylancl 662	. . . . . . . . . 10 $/\$
67	61, 64, 66	3eqtr3d 2516	. . . . . . . . 9 $/\$
68		2cn 10602	. . . . . . . . . . 11
69	68	a1i 11	. . . . . . . . . 10 $/\$
70	45	recnd 9618	. . . . . . . . . 10 $/\$
71	53, 69, 70	mulassd 9615	. . . . . . . . 9 $/\$
72	56, 67, 71	3brtr3d 4476	. . . . . . . 8 $/\$
73		1red 9607	. . . . . . . . 9 $/\$
74		remulcl 9573	. . . . . . . . . . 11 $/\$
75	15, 45, 74	sylancr 663	. . . . . . . . . 10 $/\$
76	41, 75	remulcld 9620	. . . . . . . . 9 $/\$
77	73, 76, 17	lemul1d 11291	. . . . . . . 8 $/\$
78	72, 77	mpbid 210	. . . . . . 7 $/\$
79	62	mulid2d 9610	. . . . . . 7 $/\$
80	75	recnd 9618	. . . . . . . 8 $/\$
81	53, 80, 62	mul32d 9785	. . . . . . 7 $/\$
82	78, 79, 81	3brtr3d 4476	. . . . . 6 $/\$
83		remsqsqrt 13049	. . . . . . . . . . 11 $/\$
84	27, 47, 83	syl2anc 661	. . . . . . . . . 10 $/\$
85		remsqsqrt 13049	. . . . . . . . . . 11 $/\$
86	29, 37, 85	syl2anc 661	. . . . . . . . . 10 $/\$
87	84, 86	oveq12d 6300	. . . . . . . . 9 $/\$
88	53, 53, 62, 62	mul4d 9787	. . . . . . . . 9 $/\$
89	87, 88	eqtr3d 2510	. . . . . . . 8 $/\$
90	17	rpcnne0d 11261	. . . . . . . . . 10 $/\$ $/\$
91	20	rpcnne0d 11261	. . . . . . . . . 10 $/\$ $/\$
92		divsubdiv 10256	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
93	69, 69, 90, 91, 92	syl22anc 1229	. . . . . . . . 9 $/\$
94	69, 53, 62	subdid 10008	. . . . . . . . . 10 $/\$
95	53, 62	mulcomd 9613	. . . . . . . . . 10 $/\$
96	94, 95	oveq12d 6300	. . . . . . . . 9 $/\$
97	93, 96	eqtr4d 2511	. . . . . . . 8 $/\$
98	89, 97	oveq12d 6300	. . . . . . 7 $/\$
99	53, 62	mulcld 9612	. . . . . . . 8 $/\$
100	20, 17	rpmulcld 11268	. . . . . . . . . 10 $/\$
101	75, 100	rerpdivcld 11279	. . . . . . . . 9 $/\$
102	101	recnd 9618	. . . . . . . 8 $/\$
103	99, 99, 102	mulassd 9615	. . . . . . 7 $/\$
104	100	rpne0d 11257	. . . . . . . . 9 $/\$
105	80, 99, 104	divcan2d 10318	. . . . . . . 8 $/\$
106	105	oveq2d 6298	. . . . . . 7 $/\$
107	98, 103, 106	3eqtrd 2512	. . . . . 6 $/\$
108	82, 107	breqtrrd 4473	. . . . 5 $/\$
109	8, 26, 31, 40, 108	letrd 9734	. . . 4 $/\$
110	12	nngt0d 10575	. . . . 5 $/\$
111		ledivmul 10414	. . . . 5 $/\$ $/\$ $/\$
112	8, 23, 30, 110, 111	syl112anc 1232	. . . 4 $/\$
113	109, 112	mpbird 232	. . 3 $/\$
114	1, 13, 23, 113	fsumle 13572	. 2
115		oveq1 6289	. . . . . . 7
116	115	fveq2d 5868	. . . . . 6
117	116	oveq2d 6298	. . . . 5
118		oveq1 6289	. . . . . . 7
119	118	fveq2d 5868	. . . . . 6
120	119	oveq2d 6298	. . . . 5
121		oveq1 6289	. . . . . . . . . 10
122		2m1e1 10646	. . . . . . . . . 10
123	121, 122	syl6eq 2524	. . . . . . . . 9
124	123	fveq2d 5868	. . . . . . . 8
125		sqrt1 13064	. . . . . . . 8
126	124, 125	syl6eq 2524	. . . . . . 7
127	126	oveq2d 6298	. . . . . 6
128	68	div1i 10268	. . . . . 6
129	127, 128	syl6eq 2524	. . . . 5
130		oveq1 6289	. . . . . . 7
131	130	fveq2d 5868	. . . . . 6
132	131	oveq2d 6298	. . . . 5
133		nnz 10882	. . . . 5
134		eluzp1p1 11103	. . . . . . 7
135		nnuz 11113	. . . . . . 7
136	134, 135	eleq2s 2575	. . . . . 6
137		df-2 10590	. . . . . . 7
138	137	fveq2i 5867	. . . . . 6
139	136, 138	syl6eleqr 2566	. . . . 5
140		elfzuz 11680	. . . . . . . . . . 11
141		uz2m1nn 11152	. . . . . . . . . . 11
142	140, 141	syl 16	. . . . . . . . . 10
143	142	adantl 466	. . . . . . . . 9 $/\$
144	143	nnrpd 11251	. . . . . . . 8 $/\$
145	144	rpsqrtcld 13202	. . . . . . 7 $/\$
146		rerpdivcl 11243	. . . . . . 7 $/\$
147	15, 145, 146	sylancr 663	. . . . . 6 $/\$
148	147	recnd 9618	. . . . 5 $/\$
149	117, 120, 129, 132, 133, 139, 148	telfsum 13577	. . . 4
150		pncan 9822	. . . . . . . . 9 $/\$
151	32, 33, 150	sylancl 662	. . . . . . . 8 $/\$
152	151	fveq2d 5868	. . . . . . 7 $/\$
153	152	oveq2d 6298	. . . . . 6 $/\$
154	153	oveq2d 6298	. . . . 5 $/\$
155	154	sumeq2dv 13484	. . . 4
156		nncn 10540	. . . . . . . 8
157		pncan 9822	. . . . . . . 8 $/\$
158	156, 33, 157	sylancl 662	. . . . . . 7
159	158	fveq2d 5868	. . . . . 6
160	159	oveq2d 6298	. . . . 5
161	160	oveq2d 6298	. . . 4
162	149, 155, 161	3eqtr3d 2516	. . 3
163		2rp 11221	. . . . . 6
164		nnrp 11225	. . . . . . 7
165	164	rpsqrtcld 13202	. . . . . 6
166		rpdivcl 11238	. . . . . 6 $/\$
167	163, 165, 166	sylancr 663	. . . . 5
168	167	rpge0d 11256	. . . 4
169	167	rpred 11252	. . . . 5
170		subge02 10064	. . . . 5 $/\$
171	15, 169, 170	sylancr 663	. . . 4
172	168, 171	mpbid 210	. . 3
173	162, 172	eqbrtrd 4467	. 2
174	14, 24, 25, 114, 173	letrd 9734	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1379

wcel 1767

wne 2662 class class class wbr 4447

cfv 5586 (class class class)co 6282

cc 9486

cr 9487

cc0 9488

c1 9489

caddc 9491

cmul 9493

clt 9624

cle 9625

cmin 9801

cdiv 10202

cn 10532

c2 10581

cuz 11078

crp 11216

cfz 11668

cexp 12130

csqrt 13025

csu 13467

clog 22670

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 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566 ax-addf 9567 ax-mulf 9568

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 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-iin 4328 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-of 6522 df-om 6679 df-1st 6781 df-2nd 6782 df-supp 6899 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-map 7419 df-pm 7420 df-ixp 7467 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-fsupp 7826 df-fi 7867 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-4 10592 df-5 10593 df-6 10594 df-7 10595 df-8 10596 df-9 10597 df-10 10598 df-n0 10792 df-z 10861 df-dec 10973 df-uz 11079 df-q 11179 df-rp 11217 df-xneg 11314 df-xadd 11315 df-xmul 11316 df-ioo 11529 df-ioc 11530 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-fl 11893 df-mod 11961 df-seq 12072 df-exp 12131 df-fac 12318 df-bc 12345 df-hash 12370 df-shft 12859 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-limsup 13253 df-clim 13270 df-rlim 13271 df-sum 13468 df-ef 13661 df-sin 13663 df-cos 13664 df-tan 13665 df-pi 13666 df-struct 14488 df-ndx 14489 df-slot 14490 df-base 14491 df-sets 14492 df-ress 14493 df-plusg 14564 df-mulr 14565 df-starv 14566 df-sca 14567 df-vsca 14568 df-ip 14569 df-tset 14570 df-ple 14571 df-ds 14573 df-unif 14574 df-hom 14575 df-cco 14576 df-rest 14674 df-topn 14675 df-0g 14693 df-gsum 14694 df-topgen 14695 df-pt 14696 df-prds 14699 df-xrs 14753 df-qtop 14758 df-imas 14759 df-xps 14761 df-mre 14837 df-mrc 14838 df-acs 14840 df-mnd 15728 df-submnd 15778 df-mulg 15861 df-cntz 16150 df-cmn 16596 df-psmet 18182 df-xmet 18183 df-met 18184 df-bl 18185 df-mopn 18186 df-fbas 18187 df-fg 18188 df-cnfld 18192 df-top 19166 df-bases 19168 df-topon 19169 df-topsp 19170 df-cld 19286 df-ntr 19287 df-cls 19288 df-nei 19365 df-lp 19403 df-perf 19404 df-cn 19494 df-cnp 19495 df-haus 19582 df-cmp 19653 df-tx 19798 df-hmeo 19991 df-fil 20082 df-fm 20174 df-flim 20175 df-flf 20176 df-xms 20558 df-ms 20559 df-tms 20560 df-cncf 21117 df-limc 22005 df-dv 22006 df-log 22672 df-cxp 22673

This theorem is referenced by: rplogsumlem2 23398

W3C validator