rplogsumlem1 - Metamath Proof Explorer

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

Theorem rplogsumlem1 22738

Description: Lemma for rplogsum 22781. (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 11800	. . 3
2		elfzuz 11454	. . . . . . . 8
3		eluz2b2 10932	. . . . . . . . 9 $/\$
4	3	simplbi 460	. . . . . . . 8
5	2, 4	syl 16	. . . . . . 7
6	5	adantl 466	. . . . . 6 $/\$
7	6	nnrpd 11031	. . . . 5 $/\$
8	7	relogcld 22077	. . . 4 $/\$
9	2	adantl 466	. . . . . 6 $/\$
10		uz2m1nn 10934	. . . . . 6
11	9, 10	syl 16	. . . . 5 $/\$
12	6, 11	nnmulcld 10374	. . . 4 $/\$
13	8, 12	nndivred 10375	. . 3 $/\$
14	1, 13	fsumrecl 13216	. 2
15		2re 10396	. . . . 5
16	11	nnrpd 11031	. . . . . 6 $/\$
17	16	rpsqrcld 12903	. . . . 5 $/\$
18		rerpdivcl 11023	. . . . 5 $/\$
19	15, 17, 18	sylancr 663	. . . 4 $/\$
20	7	rpsqrcld 12903	. . . . 5 $/\$
21		rerpdivcl 11023	. . . . 5 $/\$
22	15, 20, 21	sylancr 663	. . . 4 $/\$
23	19, 22	resubcld 9781	. . 3 $/\$
24	1, 23	fsumrecl 13216	. 2
25	15	a1i 11	. 2
26	17	rpred 11032	. . . . 5 $/\$
27	6	nnred 10342	. . . . . . 7 $/\$
28		peano2rem 9680	. . . . . . . 8
29	27, 28	syl 16	. . . . . . 7 $/\$
30	27, 29	remulcld 9419	. . . . . 6 $/\$
31	30, 23	remulcld 9419	. . . . 5 $/\$
32	6	nncnd 10343	. . . . . . . 8 $/\$
33		ax-1cn 9345	. . . . . . . 8
34		npcan 9624	. . . . . . . 8 $/\$
35	32, 33, 34	sylancl 662	. . . . . . 7 $/\$
36	35	fveq2d 5700	. . . . . 6 $/\$
37	16	rpge0d 11036	. . . . . . 7 $/\$
38		loglesqr 22201	. . . . . . 7 $/\$
39	29, 37, 38	syl2anc 661	. . . . . 6 $/\$
40	36, 39	eqbrtrrd 4319	. . . . 5 $/\$
41	20	rpred 11032	. . . . . . . . . . 11 $/\$
42	41, 26	readdcld 9418	. . . . . . . . . 10 $/\$
43		remulcl 9372	. . . . . . . . . . 11 $/\$
44	41, 15, 43	sylancl 662	. . . . . . . . . 10 $/\$
45	41, 26	resubcld 9781	. . . . . . . . . 10 $/\$
46	27	lem1d 10271	. . . . . . . . . . . 12 $/\$
47	7	rpge0d 11036	. . . . . . . . . . . . 13 $/\$
48	29, 37, 27, 47	sqrled 12918	. . . . . . . . . . . 12 $/\$
49	46, 48	mpbid 210	. . . . . . . . . . 11 $/\$
50	41, 26	subge0d 9934	. . . . . . . . . . 11 $/\$
51	49, 50	mpbird 232	. . . . . . . . . 10 $/\$
52	26, 41, 41, 49	leadd2dd 9959	. . . . . . . . . . 11 $/\$
53	20	rpcnd 11034	. . . . . . . . . . . 12 $/\$
54	53	times2d 10573	. . . . . . . . . . 11 $/\$
55	52, 54	breqtrrd 4323	. . . . . . . . . 10 $/\$
56	42, 44, 45, 51, 55	lemul1ad 10277	. . . . . . . . 9 $/\$
57	32	sqsqrd 12930	. . . . . . . . . . 11 $/\$
58		subcl 9614	. . . . . . . . . . . . 13 $/\$
59	32, 33, 58	sylancl 662	. . . . . . . . . . . 12 $/\$
60	59	sqsqrd 12930	. . . . . . . . . . 11 $/\$
61	57, 60	oveq12d 6114	. . . . . . . . . 10 $/\$
62	17	rpcnd 11034	. . . . . . . . . . 11 $/\$
63		subsq 11978	. . . . . . . . . . 11 $/\$
64	53, 62, 63	syl2anc 661	. . . . . . . . . 10 $/\$
65		nncan 9643	. . . . . . . . . . 11 $/\$
66	32, 33, 65	sylancl 662	. . . . . . . . . 10 $/\$
67	61, 64, 66	3eqtr3d 2483	. . . . . . . . 9 $/\$
68		2cn 10397	. . . . . . . . . . 11
69	68	a1i 11	. . . . . . . . . 10 $/\$
70	45	recnd 9417	. . . . . . . . . 10 $/\$
71	53, 69, 70	mulassd 9414	. . . . . . . . 9 $/\$
72	56, 67, 71	3brtr3d 4326	. . . . . . . 8 $/\$
73		1red 9406	. . . . . . . . 9 $/\$
74		remulcl 9372	. . . . . . . . . . 11 $/\$
75	15, 45, 74	sylancr 663	. . . . . . . . . 10 $/\$
76	41, 75	remulcld 9419	. . . . . . . . 9 $/\$
77	73, 76, 17	lemul1d 11071	. . . . . . . 8 $/\$
78	72, 77	mpbid 210	. . . . . . 7 $/\$
79	62	mulid2d 9409	. . . . . . 7 $/\$
80	75	recnd 9417	. . . . . . . 8 $/\$
81	53, 80, 62	mul32d 9584	. . . . . . 7 $/\$
82	78, 79, 81	3brtr3d 4326	. . . . . 6 $/\$
83		remsqsqr 12751	. . . . . . . . . . 11 $/\$
84	27, 47, 83	syl2anc 661	. . . . . . . . . 10 $/\$
85		remsqsqr 12751	. . . . . . . . . . 11 $/\$
86	29, 37, 85	syl2anc 661	. . . . . . . . . 10 $/\$
87	84, 86	oveq12d 6114	. . . . . . . . 9 $/\$
88	53, 53, 62, 62	mul4d 9586	. . . . . . . . 9 $/\$
89	87, 88	eqtr3d 2477	. . . . . . . 8 $/\$
90	17	rpcnne0d 11041	. . . . . . . . . 10 $/\$ $/\$
91	20	rpcnne0d 11041	. . . . . . . . . 10 $/\$ $/\$
92		divsubdiv 10052	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
93	69, 69, 90, 91, 92	syl22anc 1219	. . . . . . . . 9 $/\$
94	69, 53, 62	subdid 9805	. . . . . . . . . 10 $/\$
95	53, 62	mulcomd 9412	. . . . . . . . . 10 $/\$
96	94, 95	oveq12d 6114	. . . . . . . . 9 $/\$
97	93, 96	eqtr4d 2478	. . . . . . . 8 $/\$
98	89, 97	oveq12d 6114	. . . . . . 7 $/\$
99	53, 62	mulcld 9411	. . . . . . . 8 $/\$
100	20, 17	rpmulcld 11048	. . . . . . . . . 10 $/\$
101	75, 100	rerpdivcld 11059	. . . . . . . . 9 $/\$
102	101	recnd 9417	. . . . . . . 8 $/\$
103	99, 99, 102	mulassd 9414	. . . . . . 7 $/\$
104	100	rpne0d 11037	. . . . . . . . 9 $/\$
105	80, 99, 104	divcan2d 10114	. . . . . . . 8 $/\$
106	105	oveq2d 6112	. . . . . . 7 $/\$
107	98, 103, 106	3eqtrd 2479	. . . . . 6 $/\$
108	82, 107	breqtrrd 4323	. . . . 5 $/\$
109	8, 26, 31, 40, 108	letrd 9533	. . . 4 $/\$
110	12	nngt0d 10370	. . . . 5 $/\$
111		ledivmul 10210	. . . . 5 $/\$ $/\$ $/\$
112	8, 23, 30, 110, 111	syl112anc 1222	. . . 4 $/\$
113	109, 112	mpbird 232	. . 3 $/\$
114	1, 13, 23, 113	fsumle 13267	. 2
115		oveq1 6103	. . . . . . 7
116	115	fveq2d 5700	. . . . . 6
117	116	oveq2d 6112	. . . . 5
118		oveq1 6103	. . . . . . 7
119	118	fveq2d 5700	. . . . . 6
120	119	oveq2d 6112	. . . . 5
121		oveq1 6103	. . . . . . . . . 10
122		2m1e1 10441	. . . . . . . . . 10
123	121, 122	syl6eq 2491	. . . . . . . . 9
124	123	fveq2d 5700	. . . . . . . 8
125		sqr1 12766	. . . . . . . 8
126	124, 125	syl6eq 2491	. . . . . . 7
127	126	oveq2d 6112	. . . . . 6
128	68	div1i 10064	. . . . . 6
129	127, 128	syl6eq 2491	. . . . 5
130		oveq1 6103	. . . . . . 7
131	130	fveq2d 5700	. . . . . 6
132	131	oveq2d 6112	. . . . 5
133		nnz 10673	. . . . 5
134		eluzp1p1 10891	. . . . . . 7
135		nnuz 10901	. . . . . . 7
136	134, 135	eleq2s 2535	. . . . . 6
137		df-2 10385	. . . . . . 7
138	137	fveq2i 5699	. . . . . 6
139	136, 138	syl6eleqr 2534	. . . . 5
140		elfzuz 11454	. . . . . . . . . . 11
141		uz2m1nn 10934	. . . . . . . . . . 11
142	140, 141	syl 16	. . . . . . . . . 10
143	142	adantl 466	. . . . . . . . 9 $/\$
144	143	nnrpd 11031	. . . . . . . 8 $/\$
145	144	rpsqrcld 12903	. . . . . . 7 $/\$
146		rerpdivcl 11023	. . . . . . 7 $/\$
147	15, 145, 146	sylancr 663	. . . . . 6 $/\$
148	147	recnd 9417	. . . . 5 $/\$
149	117, 120, 129, 132, 133, 139, 148	fsumtscop 13272	. . . 4
150		pncan 9621	. . . . . . . . 9 $/\$
151	32, 33, 150	sylancl 662	. . . . . . . 8 $/\$
152	151	fveq2d 5700	. . . . . . 7 $/\$
153	152	oveq2d 6112	. . . . . 6 $/\$
154	153	oveq2d 6112	. . . . 5 $/\$
155	154	sumeq2dv 13185	. . . 4
156		nncn 10335	. . . . . . . 8
157		pncan 9621	. . . . . . . 8 $/\$
158	156, 33, 157	sylancl 662	. . . . . . 7
159	158	fveq2d 5700	. . . . . 6
160	159	oveq2d 6112	. . . . 5
161	160	oveq2d 6112	. . . 4
162	149, 155, 161	3eqtr3d 2483	. . 3
163		2rp 11001	. . . . . 6
164		nnrp 11005	. . . . . . 7
165	164	rpsqrcld 12903	. . . . . 6
166		rpdivcl 11018	. . . . . 6 $/\$
167	163, 165, 166	sylancr 663	. . . . 5
168	167	rpge0d 11036	. . . 4
169	167	rpred 11032	. . . . 5
170		subge02 9860	. . . . 5 $/\$
171	15, 169, 170	sylancr 663	. . . 4
172	168, 171	mpbid 210	. . 3
173	162, 172	eqbrtrd 4317	. 2
174	14, 24, 25, 114, 173	letrd 9533	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1369

wcel 1756

wne 2611 class class class wbr 4297

cfv 5423 (class class class)co 6096

cc 9285

cr 9286

cc0 9287

c1 9288

caddc 9290

cmul 9292

clt 9423

cle 9424

cmin 9600

cdiv 9998

cn 10327

c2 10376

cuz 10866

crp 10996

cfz 11442

cexp 11870

csqr 12727

csu 13168

clog 22011

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 ax-addf 9366 ax-mulf 9367

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-iin 4179 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-of 6325 df-om 6482 df-1st 6582 df-2nd 6583 df-supp 6696 df-recs 6837 df-rdg 6871 df-1o 6925 df-2o 6926 df-oadd 6929 df-er 7106 df-map 7221 df-pm 7222 df-ixp 7269 df-en 7316 df-dom 7317 df-sdom 7318 df-fin 7319 df-fsupp 7626 df-fi 7666 df-sup 7696 df-oi 7729 df-card 8114 df-cda 8342 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-4 10387 df-5 10388 df-6 10389 df-7 10390 df-8 10391 df-9 10392 df-10 10393 df-n0 10585 df-z 10652 df-dec 10761 df-uz 10867 df-q 10959 df-rp 10997 df-xneg 11094 df-xadd 11095 df-xmul 11096 df-ioo 11309 df-ioc 11310 df-ico 11311 df-icc 11312 df-fz 11443 df-fzo 11554 df-fl 11647 df-mod 11714 df-seq 11812 df-exp 11871 df-fac 12057 df-bc 12084 df-hash 12109 df-shft 12561 df-cj 12593 df-re 12594 df-im 12595 df-sqr 12729 df-abs 12730 df-limsup 12954 df-clim 12971 df-rlim 12972 df-sum 13169 df-ef 13358 df-sin 13360 df-cos 13361 df-tan 13362 df-pi 13363 df-struct 14181 df-ndx 14182 df-slot 14183 df-base 14184 df-sets 14185 df-ress 14186 df-plusg 14256 df-mulr 14257 df-starv 14258 df-sca 14259 df-vsca 14260 df-ip 14261 df-tset 14262 df-ple 14263 df-ds 14265 df-unif 14266 df-hom 14267 df-cco 14268 df-rest 14366 df-topn 14367 df-0g 14385 df-gsum 14386 df-topgen 14387 df-pt 14388 df-prds 14391 df-xrs 14445 df-qtop 14450 df-imas 14451 df-xps 14453 df-mre 14529 df-mrc 14530 df-acs 14532 df-mnd 15420 df-submnd 15470 df-mulg 15553 df-cntz 15840 df-cmn 16284 df-psmet 17814 df-xmet 17815 df-met 17816 df-bl 17817 df-mopn 17818 df-fbas 17819 df-fg 17820 df-cnfld 17824 df-top 18508 df-bases 18510 df-topon 18511 df-topsp 18512 df-cld 18628 df-ntr 18629 df-cls 18630 df-nei 18707 df-lp 18745 df-perf 18746 df-cn 18836 df-cnp 18837 df-haus 18924 df-cmp 18995 df-tx 19140 df-hmeo 19333 df-fil 19424 df-fm 19516 df-flim 19517 df-flf 19518 df-xms 19900 df-ms 19901 df-tms 19902 df-cncf 20459 df-limc 21346 df-dv 21347 df-log 22013 df-cxp 22014

This theorem is referenced by: rplogsumlem2 22739

W3C validator