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 A beyond a starting index B.

Hypotheses

Ref	Expression
cvgratlem1ALT.1	|- F:NN-->RR
cvgratlem1ALT.2	|- A e. RR
cvgratlem1ALT.3	|- B e. NN
cvgratlem1ALT.4	|- C e. NN

Assertion

Ref	Expression
cvgratlem1ALT	|- ((0 < A /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` (B + C)) <_ ((A^C) x. (F` B)))

Distinct variable groups:   x,A   x,B   x,F

Proof of Theorem cvgratlem1ALT

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