Theorem cvgratlem5 7254

Description: Lemma for cvgrat 7255. A complex infinite series F meeting the ratio test criterion converges. We show that the partial sums of F are smaller than the partial sums of a geometric series (which converges by geolimi 7236), so by the comparison test cvgcmp3cet 7190, F also converges.

Hypotheses

Ref	Expression
cvgrat.1	|- F:NN-->CC
cvgratlem5.2	|- G = {<.z, w>. | (z e. NN /\ w = (A^z))}

Assertion

Ref	Expression
cvgratlem5	|- (((A e. RR /\ A < 1) /\ (B e. NN /\ A.x e. NN (B <_ x -> (abs` (F` (x + 1))) < (A x. (abs` (F` x)))))) -> E.y( + seq1 F) ~~> y)

Distinct variable groups:   x,y,z,w,A   x,B,y   x,F,y   y,G

Proof of Theorem cvgratlem5

Step	Hyp	Ref	Expression
1		oprex 3983	. . 3 |- (A / (1 - A)) e. V
2	1	cvgcmp3cet 7190	. 2 |- ((B e. NN /\ (((G:NN-->RR /\ A.v e. NN 0 <_ (G` v)) /\ ( + seq1 G) ~~> (A / (1 - A))) /\ ((((abs` (F` B)) / (A^B)) e. RR /\ 0 <_ ((abs` (F` B)) / (A^B))) /\ (F:NN-->CC /\ A.v e. NN (B < v -> (abs` (F` v)) <_ (((abs` (F` B)) / (A^B)) x. (G` v))))))) -> E.y( + seq1 F) ~~> y)
3		simprl 414	. 2 |- (((A e. RR /\ A < 1) /\ (B e. NN /\ A.x e. NN (B <_ x -> (abs` (F` (x + 1))) < (A x. (abs` (F` x)))))) -> B e. NN)
4		cvgrat.1	. . . . 5 |- F:NN-->CC
5	4	cvgratlem4 7253	. . . 4 |- ((A e. RR /\ (B e. NN /\ A.x e. NN (B <_ x -> (abs` (F` (x + 1))) < (A x. (abs` (F` x)))))) -> 0 < A)
6	5	adantlr 393	. . 3 |- (((A e. RR /\ A < 1) /\ (B e. NN /\ A.x e. NN (B <_ x -> (abs` (F` (x + 1))) < (A x. (abs` (F` x)))))) -> 0 < A)
7		0re 5440	. . . . . . . . . . . 12 |- 0 e. RR
8		ltlet 5520	. . . . . . . . . . . 12 |- ((0 e. RR /\ A e. RR) -> (0 < A -> 0 <_ A))
9	7, 8	mpan 695	. . . . . . . . . . 11 |- (A e. RR -> (0 < A -> 0 <_ A))
10	9	imp 350	. . . . . . . . . 10 |- ((A e. RR /\ 0 < A) -> 0 <_ A)
11	10	adantlr 393	. . . . . . . . 9 |- (((A e. RR /\ A < 1) /\ 0 < A) -> 0 <_ A)
12		reexpclt 6580	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ z e. NN0) -> (A^z) e. RR)
13		nnnn0t 6106	. . . . . . . . . . . . . . . 16 |- (z e. NN -> z e. NN0)
14	12, 13	sylan2 451	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ z e. NN) -> (A^z) e. RR)
15	14	r19.21aiva 1714	. . . . . . . . . . . . . 14 |- (A e. RR -> A.z e. NN (A^z) e. RR)
16		cvgratlem5.2	. . . . . . . . . . . . . . 15 |- G = {<.z, w>. | (z e. NN /\ w = (A^z))}
17	16	fopab2 3823	. . . . . . . . . . . . . 14 |- (A.z e. NN (A^z) e. RR <-> G:NN-->RR)
18	15, 17	sylib 198	. . . . . . . . . . . . 13 |- (A e. RR -> G:NN-->RR)
19	18	adantr 389	. . . . . . . . . . . 12 |- ((A e. RR /\ 0 <_ A) -> G:NN-->RR)
20		expge0t 6591	. . . . . . . . . . . . . . . . 17 |- ((A e. RR /\ v e. NN0 /\ 0 <_ A) -> 0 <_ (A^v))
21		nnnn0t 6106	. . . . . . . . . . . . . . . . 17 |- (v e. NN -> v e. NN0)
22	20, 21	syl3an2 860	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ v e. NN /\ 0 <_ A) -> 0 <_ (A^v))
23	22	3expa 833	. . . . . . . . . . . . . . 15 |- (((A e. RR /\ v e. NN) /\ 0 <_ A) -> 0 <_ (A^v))
24	23	an1rs 489	. . . . . . . . . . . . . 14 |- (((A e. RR /\ 0 <_ A) /\ v e. NN) -> 0 <_ (A^v))
25		opreq2 3969	. . . . . . . . . . . . . . . 16 |- (z = v -> (A^z) = (A^v))
26		oprex 3983	. . . . . . . . . . . . . . . 16 |- (A^v) e. V
27	25, 16, 26	fvopab4 3780	. . . . . . . . . . . . . . 15 |- (v e. NN -> (G` v) = (A^v))
28	27	adantl 388	. . . . . . . . . . . . . 14 |- (((A e. RR /\ 0 <_ A) /\ v e. NN) -> (G` v) = (A^v))
29	24, 28	breqtrrd 2641	. . . . . . . . . . . . 13 |- (((A e. RR /\ 0 <_ A) /\ v e. NN) -> 0 <_ (G` v))
30	29	r19.21aiva 1714	. . . . . . . . . . . 12 |- ((A e. RR /\ 0 <_ A) -> A.v e. NN 0 <_ (G` v))
31	19, 30	jca 288	. . . . . . . . . . 11 |- ((A e. RR /\ 0 <_ A) -> (G:NN-->RR /\ A.v e. NN 0 <_ (G` v)))
32	31	adantlr 393	. . . . . . . . . 10 |- (((A e. RR /\ A < 1) /\ 0 <_ A) -> (G:NN-->RR /\ A.v e. NN 0 <_ (G` v)))
33	16	geolim1 7239	. . . . . . . . . . 11 |- ((A e. CC /\ (abs` A) < 1) -> ( + seq1 G) ~~> (A / (1 - A)))
34		recnt 5313	. . . . . . . . . . . 12 |- (A e. RR -> A e. CC)
35	34	ad2antrr 404	. . . . . . . . . . 11 |- (((A e. RR /\ A < 1) /\ 0 <_ A) -> A e. CC)
36		absidt 6862	. . . . . . . . . . . . 13 |- ((A e. RR /\ 0 <_ A) -> (abs` A) = A)
37	36	adantlr 393	. . . . . . . . . . . 12 |- (((A e. RR /\ A < 1) /\ 0 <_ A) -> (abs` A) = A)
38		simplr 413	. . . . . . . . . . . 12 |- (((A e. RR /\ A < 1) /\ 0 <_ A) -> A < 1)
39	37, 38	eqbrtrd 2635	. . . . . . . . . . 11 |- (((A e. RR /\ A < 1) /\ 0 <_ A) -> (abs` A) < 1)
40	33, 35, 39	sylanc 471	. . . . . . . . . 10 |- (((A e. RR /\ A < 1) /\ 0 <_ A) -> ( + seq1 G) ~~> (A / (1 - A)))
41	32, 40	jca 288	. . . . . . . . 9 |- (((A e. RR /\ A < 1) /\ 0 <_ A) -> ((G:NN-->RR /\ A.v e. NN 0 <_ (G` v)) /\ ( + seq1 G) ~~> (A / (1 - A))))
42	11, 41	syldan 467	. . . . . . . 8 |- (((A e. RR /\ A < 1) /\ 0 < A) -> ((G:NN-->RR /\ A.v e. NN 0 <_ (G` v)) /\ ( + seq1 G) ~~> (A / (1 - A))))
43	42	adantr 389	. . . . . . 7 |- ((((A e. RR /\ A < 1) /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (abs` (F` (x + 1))) < (A x. (abs` (F` x)))))) -> ((G:NN-->RR /\ A.v e. NN 0 <_ (G` v)) /\ ( + seq1 G) ~~> (A / (1 - A))))
44		redivclt 5800	. . . . . . . . . . . . . 14 |- (((abs` (F` B)) e. RR /\ (A^B) e. RR /\ (A^B) =/= 0) -> ((abs` (F` B)) / (A^B)) e. RR)
45	4	ffvelrni 3815	. . . . . . . . . . . . . . . 16 |- (B e. NN -> (F` B) e. CC)
46		absclt 6833	. . . . . . . . . . . . . . . 16 |- ((F` B) e. CC -> (abs` (F` B)) e. RR)
47	45, 46	syl 10	. . . . . . . . . . . . . . 15 |- (B e. NN -> (abs` (F` B)) e. RR)
48	47	3ad2ant2 801	. . . . . . . . . . . . . 14 |- ((A e. RR /\ B e. NN /\ 0 < A) -> (abs` (F` B)) e. RR)
49		reexpclt 6580	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ B e. NN0) -> (A^B) e. RR)
50		nnnn0t 6106	. . . . . . . . . . . . . . . 16 |- (B e. NN -> B e. NN0)
51	49, 50	sylan2 451	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ B e. NN) -> (A^B) e. RR)
52	51	3adant3 799	. . . . . . . . . . . . . 14 |- ((A e. RR /\ B e. NN /\ 0 < A) -> (A^B) e. RR)
53		gt0ne0t 5618	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ 0 < A) -> A =/= 0)
54	53	3adant2 798	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ B e. NN /\ 0 < A) -> A =/= 0)
55		expne0t 6586	. . . . . . . . . . . . . . . . 17 |- ((A e. CC /\ B e. NN) -> ((A^B) =/= 0 <-> A =/= 0))
56	55, 34	sylan 448	. . . . . . . . . . . . . . . 16 |- ((A e. RR /\ B e. NN) -> ((A^B) =/= 0 <-> A =/= 0))
57	56	3adant3 799	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ B e. NN /\ 0 < A) -> ((A^B) =/= 0 <-> A =/= 0))
58	54, 57	mpbird 196	. . . . . . . . . . . . . 14 |- ((A e. RR /\ B e. NN /\ 0 < A) -> (A^B) =/= 0)
59	44, 48, 52, 58	syl3anc 858	. . . . . . . . . . . . 13 |- ((A e. RR /\ B e. NN /\ 0 < A) -> ((abs` (F` B)) / (A^B)) e. RR)
60		divge0t 5856	. . . . . . . . . . . . . 14 |- ((((abs` (F` B)) e. RR /\ 0 <_ (abs` (F` B))) /\ ((A^B) e. RR /\ 0 < (A^B))) -> 0 <_ ((abs` (F` B)) / (A^B)))
61		absge0t 6854	. . . . . . . . . . . . . . . 16 |- ((F` B) e. CC -> 0 <_ (abs` (F` B)))
62	45, 61	syl 10	. . . . . . . . . . . . . . 15 |- (B e. NN -> 0 <_ (abs` (F` B)))
63	62	3ad2ant2 801	. . . . . . . . . . . . . 14 |- ((A e. RR /\ B e. NN /\ 0 < A) -> 0 <_ (abs` (F` B)))
64		expgt0t 6589	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ B e. NN0 /\ 0 < A) -> 0 < (A^B))
65	64, 50	syl3an2 860	. . . . . . . . . . . . . 14 |- ((A e. RR /\ B e. NN /\ 0 <