Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem geolimilem 7170

Description: Lemma for geolimi 7171.

Hypotheses

Ref	Expression
geoser.1
geoser.2
geolimilem.3
geolimilem.4
geolimilem.5

Assertion

Ref	Expression
geolimilem

Distinct variable groups:   ,,,   ,   ,

---

Proof of Theorem geolimilem

Step	Hyp	Ref	Expression
1		ax1cn 5241	. . . . . . . . . . 11
2		geoser.2	. . . . . . . . . . 11
3	1, 2	subcl 5338	. . . . . . . . . 10
4		1re 5407	. . . . . . . . . . 11
5		geolimilem.3	. . . . . . . . . . 11
6		abssubne0t 6820	. . . . . . . . . . 11
7	2, 4, 5, 6	mp3an 913	. . . . . . . . . 10
8	3, 7	reccl 5682	. . . . . . . . 9
9	8	negcl 5341	. . . . . . . 8
10	9, 2	mulcl 5293	. . . . . . 7
11		nnnn0t 6053	. . . . . . . . . 10
12		opreq2 3954	. . . . . . . . . . 11
13		geoser.1	. . . . . . . . . . 11
14		oprex 3968	. . . . . . . . . . 11
15	12, 13, 14	fvopab4 3765	. . . . . . . . . 10
16	11, 15	syl 10	. . . . . . . . 9
17	16	rgen 1690	. . . . . . . 8
18		nn0ex 6052	. . . . . . . . . 10
19	18, 13	fopabex2 3598	. . . . . . . . 9
20	19	expcnv 7168	. . . . . . . 8
21	2, 17, 5, 20	mp3an 913	. . . . . . 7
22	10, 21	pm3.2i 285	. . . . . 6
23		0z 6093	. . . . . . 7
24		elnn0uz 6373	. . . . . . . . 9
25		expclt 6513	. . . . . . . . . . . . 13
26	2, 25	mpan 693	. . . . . . . . . . . 12
27	13, 26	fopab 3812	. . . . . . . . . . 11
28	27	ffvelrni 3800	. . . . . . . . . 10
29		geolimilem.5	. . . . . . . . . . 11
30	2	negcl 5341	. . . . . . . . . . . . . 14
31		div23t 5705	. . . . . . . . . . . . . . 15
32	7, 31	mpan2 694	. . . . . . . . . . . . . 14
33	30, 3, 32	mp3an13 904	. . . . . . . . . . . . 13
34	28, 33	syl 10	. . . . . . . . . . . 12
35		mulneg1t 5423	. . . . . . . . . . . . . . 15
36	2, 35	mpan 693	. . . . . . . . . . . . . 14
37	28, 36	syl 10	. . . . . . . . . . . . 13
38	37	opreq1d 3960	. . . . . . . . . . . 12
39		mulneg12t 5425	. . . . . . . . . . . . . . . . 17
40	8, 2, 39	mp2an 695	. . . . . . . . . . . . . . . 16
41		divrec2t 5703	. . . . . . . . . . . . . . . . 17
42	30, 3, 7, 41	mp3an 913	. . . . . . . . . . . . . . . 16
43	40, 42	eqtr4 1490	. . . . . . . . . . . . . . 15
44	43	opreq1i 3956	. . . . . . . . . . . . . 14
45	44	eqcomi 1471	. . . . . . . . . . . . 13
46	45	a1i 8	. . . . . . . . . . . 12
47	34, 38, 46	3eqtr3d 1507	. . . . . . . . . . 11
48	29, 47	eqtrd 1499	. . . . . . . . . 10
49	28, 48	jca 288	. . . . . . . . 9
50	24, 49	sylbir 201	. . . . . . . 8
51	50	rgen 1690	. . . . . . 7
52	23, 51	pm3.2i 285	. . . . . 6
53		geolimilem.4	. . . . . . . 8
54		fnex 3593	. . . . . . . 8
55	53, 18, 54	mp2an 695	. . . . . . 7
56	23	elisseti 1809	. . . . . . 7
57	19, 55, 56	climmulc2 7065	. . . . . 6
58	22, 52, 57	mp2an 695	. . . . 5
59	10	mul01 5403	. . . . 5
60	58, 59	breqtr 2628	. . . 4
61	60, 8	pm3.2i 285	. . 3
62		axmulcl 5245	. . . . . . . . . . . 12
63	2, 62	mpan 693	. . . . . . . . . . 11
64	28, 63	syl 10	. . . . . . . . . 10
65		negclt 5340	. . . . . . . . . 10
66	64, 65	syl 10	. . . . . . . . 9
67		divclt 5681	. . . . . . . . . 10
68	3, 7, 67	mp3an23 905	. . . . . . . . 9
69	66, 68	syl 10	. . . . . . . 8
70	29, 69	eqeltrd 1540	. . . . . . 7
71		expclt 6513	. . . . . . . . . . . . . . 15
72	2, 71	mpan 693	. . . . . . . . . . . . . 14
73		axmulcom 5248	. . . . . . . . . . . . . . 15