Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem cvgratlem1ALT 7182

Description: Lemma for cvgrat 7190. Establish, by induction, an exponential upper bound for the terms of a real series, given that the ratio of successive terms is less than some positive constant beyond a starting index .

Hypotheses

Ref	Expression
cvgratlem1ALT.1
cvgratlem1ALT.2
cvgratlem1ALT.3
cvgratlem1ALT.4

Assertion

Ref	Expression
cvgratlem1ALT

Distinct variable groups:   ,   ,   ,

---

Proof of Theorem cvgratlem1ALT

Step	Hyp	Ref	Expression
1		cvgratlem1ALT.4	. . 3
2		opreq2 3954	. . . . . . 7
3	2	fveq2d 3713	. . . . . 6
4		opreq2 3954	. . . . . . 7
5	4	opreq1d 3960	. . . . . 6
6	3, 5	breq12d 2621	. . . . 5
7	6	imbi2d 610	. . . 4
8		opreq2 3954	. . . . . . 7
9	8	fveq2d 3713	. . . . . 6
10		opreq2 3954	. . . . . . 7
11	10	opreq1d 3960	. . . . . 6
12	9, 11	breq12d 2621	. . . . 5
13	12	imbi2d 610	. . . 4
14		opreq2 3954	. . . . . . 7
15	14	fveq2d 3713	. . . . . 6
16		opreq2 3954	. . . . . . 7
17	16	opreq1d 3960	. . . . . 6
18	15, 17	breq12d 2621	. . . . 5
19	18	imbi2d 610	. . . 4
20		opreq2 3954	. . . . . . 7
21	20	fveq2d 3713	. . . . . 6
22		opreq2 3954	. . . . . . 7
23	22	opreq1d 3960	. . . . . 6
24	21, 23	breq12d 2621	. . . . 5
25	24	imbi2d 610	. . . 4
26		cvgratlem1ALT.3	. . . . . . . . 9
27	26	nnre 5879	. . . . . . . 8
28	27	leid 5584	. . . . . . 7
29		breq2 2613	. . . . . . . . . 10
30		opreq1 3953	. . . . . . . . . . . 12
31	30	fveq2d 3713	. . . . . . . . . . 11
32		fveq2 3709	. . . . . . . . . . . 12
33	32	opreq2d 3961	. . . . . . . . . . 11
34	31, 33	breq12d 2621	. . . . . . . . . 10
35	29, 34	imbi12d 624	. . . . . . . . 9
36	35	rcla4v 1864	. . . . . . . 8
37	26, 36	ax-mp 7	. . . . . . 7
38	28, 37	mpi 44	. . . . . 6
39		cvgratlem1ALT.2	. . . . . . . . 9
40	39	recn 5286	. . . . . . . 8
41		exp1t 6505	. . . . . . . 8
42	40, 41	ax-mp 7	. . . . . . 7
43	42	opreq1i 3956	. . . . . 6
44	38, 43	syl6breqr 2645	. . . . 5
45	44	adantl 388	. . . 4
46		axlttrn 5476	. . . . . . . . . . . 12
47		nnaddclt 5888	. . . . . . . . . . . . . . 15
48	26, 47	mpan 693	. . . . . . . . . . . . . 14
49		peano2nn 5883	. . . . . . . . . . . . . 14
50	48, 49	syl 10	. . . . . . . . . . . . 13