Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem georeclim 7175

Description: The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007.)

Hypothesis

Ref	Expression
georeclim.1

Assertion

Ref	Expression
georeclim

Distinct variable group:   ,,

---

Proof of Theorem georeclim

Step	Hyp	Ref	Expression
1		georeclim.1	. . . 4
2	1	geolim 7172	. . 3
3		gt0ne0t 5592	. . . . . 6
4		absclt 6768	. . . . . . 7
5	4	adantr 389	. . . . . 6
6		lt01 5653	. . . . . . . 8
7		0re 5412	. . . . . . . . . 10
8		1re 5407	. . . . . . . . . 10
9		axlttrn 5476	. . . . . . . . . 10
10	7, 8, 9	mp3an12 903	. . . . . . . . 9
11	4, 10	syl 10	. . . . . . . 8
12	6, 11	mpani 696	. . . . . . 7
13	12	imp 350	. . . . . 6
14	3, 5, 13	sylanc 471	. . . . 5
15		abs00t 6788	. . . . . . 7
16	15	necon3bid 1593	. . . . . 6
17	16	adantr 389	. . . . 5
18	14, 17	mpbid 195	. . . 4
19		recclt 5684	. . . 4
20	18, 19	syldan 467	. . 3
21		ax1cn 5241	. . . . . . 7
22		absdivt 6795	. . . . . . 7
23	21, 22	mp3an1 900	. . . . . 6
24	18, 23	syldan 467	. . . . 5
25	7, 8, 6	ltlei 5554	. . . . . . 7
26		absidt 6797	. . . . . . 7
27	8, 25, 26	mp2an 695	. . . . . 6
28	27	opreq1i 3956	. . . . 5
29	24, 28	syl6eq 1515	. . . 4
30		recgt1t 5847	. . . . . . . . 9
31	30, 5, 13	sylanc 471	. . . . . . . 8
32	31	biimpd 153	. . . . . . 7
33	32	ex 373	. . . . . 6
34	33	pm2.43d 65	. . . . 5
35	34	imp 350	. . . 4
36	29, 35	eqbrtrd 2625	. . 3
37	2, 20, 36	sylanc 471	. 2
38		dividt 5722	. . . . . 6
39	18, 38	syldan 467	. . . . 5
40	39	opreq2d 3961	. . . 4
41		divdivdivt 5741	. . . . 5
42		subclt 5339	. . . . . . . 8
43	21	a1i 8	. . . . . . . 8
44	42, 43, 20	sylanc 471	. . . . . . 7
45	44, 21	jctil 292	. . . . . 6
46		pm3.26 319	. . . . . . 7
47	46, 46	jca 288	. . . . . 6
48	45, 47	jca 288	. . . . 5
49		abssubne0t 6820	. . . . . . . 8
50	8, 49	mp3an2 901	. . . . . . 7
51	50, 20, 36	sylanc 471	. . . . . 6
52	51, 18, 18	3jca 817	. . . . 5
53	41, 48, 52	sylanc 471	. . . 4
54		recclt 5684	. . . . . 6
55	54, 44, 51	sylanc 471	. . . . 5
56		div1t 5729	. . . . 5
57	55, 56	syl 10	. . . 4
58	40, 53, 57	3eqtr3rd 1508	. . 3
59		mulid2t 5389	. . . . 5
60	59	adantr 389	. . . 4
61		subdirt 5400	. . . . . 6
62	61, 43, 20, 46	syl3anc 856	. . . . 5
63		recid2t 5699	. . . . . . 7