Theorem cvgratlem1 7185

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.

Hypothesis

Ref	Expression
cvgratlem1.1	|- F:NN-->RR

Assertion

Ref	Expression
cvgratlem1	|- ((C e. NN /\ ((A e. RR /\ 0 < A) /\ (B e. NN /\ 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 cvgratlem1

Step	Hyp	Ref	Expression
1		opreq2 3954	. . . . . . 7 |- (y = 1 -> (B + y) = (B + 1))
2	1	fveq2d 3713	. . . . . 6 |- (y = 1 -> (F` (B + y)) = (F` (B + 1)))
3		opreq2 3954	. . . . . . 7 |- (y = 1 -> (A^y) = (A^1))
4	3	opreq1d 3960	. . . . . 6 |- (y = 1 -> ((A^y) x. (F` B)) = ((A^1) x. (F` B)))
5	2, 4	breq12d 2621	. . . . 5 |- (y = 1 -> ((F` (B + y)) < ((A^y) x. (F` B)) <-> (F` (B + 1)) < ((A^1) x. (F` B))))
6	5	imbi2d 610	. . . 4 |- (y = 1 -> ((((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> (F` (B + y)) < ((A^y) x. (F` B))) <-> (((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> (F` (B + 1)) < ((A^1) x. (F` B)))))
7		opreq2 3954	. . . . . . 7 |- (y = z -> (B + y) = (B + z))
8	7	fveq2d 3713	. . . . . 6 |- (y = z -> (F` (B + y)) = (F` (B + z)))
9		opreq2 3954	. . . . . . 7 |- (y = z -> (A^y) = (A^z))
10	9	opreq1d 3960	. . . . . 6 |- (y = z -> ((A^y) x. (F` B)) = ((A^z) x. (F` B)))
11	8, 10	breq12d 2621	. . . . 5 |- (y = z -> ((F` (B + y)) < ((A^y) x. (F` B)) <-> (F` (B + z)) < ((A^z) x. (F` B))))
12	11	imbi2d 610	. . . 4 |- (y = z -> ((((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> (F` (B + y)) < ((A^y) x. (F` B))) <-> (((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> (F` (B + z)) < ((A^z) x. (F` B)))))
13		opreq2 3954	. . . . . . 7 |- (y = (z + 1) -> (B + y) = (B + (z + 1)))
14	13	fveq2d 3713	. . . . . 6 |- (y = (z + 1) -> (F` (B + y)) = (F` (B + (z + 1))))
15		opreq2 3954	. . . . . . 7 |- (y = (z + 1) -> (A^y) = (A^(z + 1)))
16	15	opreq1d 3960	. . . . . 6 |- (y = (z + 1) -> ((A^y) x. (F` B)) = ((A^(z + 1)) x. (F` B)))
17	14, 16	breq12d 2621	. . . . 5 |- (y = (z + 1) -> ((F` (B + y)) < ((A^y) x. (F` B)) <-> (F` (B + (z + 1))) < ((A^(z + 1)) x. (F` B))))
18	17	imbi2d 610	. . . 4 |- (y = (z + 1) -> ((((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> (F` (B + y)) < ((A^y) x. (F` B))) <-> (((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> (F` (B + (z + 1))) < ((A^(z + 1)) x. (F` B)))))
19		opreq2 3954	. . . . . . 7 |- (y = C -> (B + y) = (B + C))
20	19	fveq2d 3713	. . . . . 6 |- (y = C -> (F` (B + y)) = (F` (B + C)))
21		opreq2 3954	. . . . . . 7 |- (y = C -> (A^y) = (A^C))
22	21	opreq1d 3960	. . . . . 6 |- (y = C -> ((A^y) x. (F` B)) = ((A^C) x. (F` B)))
23	20, 22	breq12d 2621	. . . . 5 |- (y = C -> ((F` (B + y)) < ((A^y) x. (F` B)) <-> (F` (B + C)) < ((A^C) x. (F` B))))
24	23	imbi2d 610	. . . 4 |- (y = C -> ((((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> (F` (B + y)) < ((A^y) x. (F` B))) <-> (((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> (F` (B + C)) < ((A^C) x. (F` B)))))
25		nnret 5877	. . . . . . . . 9 |- (B e. NN -> B e. RR)
26		leidt 5504	. . . . . . . . 9 |- (B e. RR -> B <_ B)
27	25, 26	syl 10	. . . . . . . 8 |- (B e. NN -> B <_ B)
28		breq2 2613	. . . . . . . . . 10 |- (x = B -> (B <_ x <-> B <_ B))
29		opreq1 3953	. . . . . . . . . . . 12 |- (x = B -> (x + 1) = (B + 1))
30	29	fveq2d 3713	. . . . . . . . . . 11 |- (x = B -> (F` (x + 1)) = (F` (B + 1)))
31		fveq2 3709	. . . . . . . . . . . 12 |- (x = B -> (F` x) = (F` B))
32	31	opreq2d 3961	. . . . . . . . . . 11 |- (x = B -> (A x. (F` x)) = (A x. (F` B)))
33	30, 32	breq12d 2621	. . . . . . . . . 10 |- (x = B -> ((F` (x + 1)) < (A x. (F` x)) <-> (F` (B + 1)) < (A x. (F` B))))
34	28, 33	imbi12d 624	. . . . . . . . 9 |- (x = B -> ((B <_ x -> (F` (x + 1)) < (A x. (F` x))) <-> (B <_ B -> (F` (B + 1)) < (A x. (F` B)))))
35	34	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)))))
36	27, 35	mpid 47	. . . . . . 7 |- (B e. NN -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> (F` (B + 1)) < (A x. (F` B))))
37	36	imp 350	. . . . . 6 |- ((B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` (B + 1)) < (A x. (F` B)))
38	37	adantl 388	. . . . 5 |- (((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> (F` (B + 1)) < (A x. (F` B)))
39		recnt 5285	. . . . . . . . 9 |- (A e. RR -> A e. CC)
40		exp1t 6505	. . . . . . . . 9 |- (A e. CC -> (A^1) = A)
41	39, 40	syl 10	. . . . . . . 8 |- (A e. RR -> (A^1) = A)
42	41	adantr 389	. . . . . . 7 |- ((A e. RR /\ 0 < A) -> (A^1) = A)
43	42	opreq1d 3960	. . . . . 6 |- ((A e. RR /\ 0 < A) -> ((A^1) x. (F` B)) = (A x. (F` B)))
44	43	adantr 389	. . . . 5 |- (((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> ((A^1) x. (F` B)) = (A x. (F` B)))
45	38, 44	breqtrrd 2631	. . . 4 |- (((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F