Theorem cvgratlem2ALT 7200

Description: Lemma for cvgrat 7207. Using expsubt 6543, restate cvgratlem1ALT 7199 with an absolute index C instead of just an offset from the 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
cvgratlem2ALT	|- ((0 < A /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (B < C -> (F` C) <_ (((F` B) / (A^B)) x. (A^C))))

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

Proof of Theorem cvgratlem2ALT

Step	Hyp	Ref	Expression
1		cvgratlem1ALT.3	. . . . . 6 |- B e. NN
2		cvgratlem1ALT.4	. . . . . 6 |- C e. NN
3	1, 2	nnsub 5913	. . . . 5 |- (B < C <-> (C - B) e. NN)
4		opreq2 3964	. . . . . . . . . 10 |- ((C - B) = if((C - B) e. NN, (C - B), 1) -> (B + (C - B)) = (B + if((C - B) e. NN, (C - B), 1)))
5	4	fveq2d 3723	. . . . . . . . 9 |- ((C - B) = if((C - B) e. NN, (C - B), 1) -> (F` (B + (C - B))) = (F` (B + if((C - B) e. NN, (C - B), 1))))
6		opreq2 3964	. . . . . . . . . 10 |- ((C - B) = if((C - B) e. NN, (C - B), 1) -> (A^(C - B)) = (A^if((C - B) e. NN, (C - B), 1)))
7	6	opreq1d 3970	. . . . . . . . 9 |- ((C - B) = if((C - B) e. NN, (C - B), 1) -> ((A^(C - B)) x. (F` B)) = ((A^if((C - B) e. NN, (C - B), 1)) x. (F` B)))
8	5, 7	breq12d 2627	. . . . . . . 8 |- ((C - B) = if((C - B) e. NN, (C - B), 1) -> ((F` (B + (C - B))) <_ ((A^(C - B)) x. (F` B)) <-> (F` (B + if((C - B) e. NN, (C - B), 1))) <_ ((A^if((C - B) e. NN, (C - B), 1)) x. (F` B))))
9	8	imbi2d 611	. . . . . . 7 |- ((C - B) = if((C - B) e. NN, (C - B), 1) -> (((0 < A /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` (B + (C - B))) <_ ((A^(C - B)) x. (F` B))) <-> ((0 < A /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` (B + if((C - B) e. NN, (C - B), 1))) <_ ((A^if((C - B) e. NN, (C - B), 1)) x. (F` B)))))
10		cvgratlem1ALT.1	. . . . . . . 8 |- F:NN-->RR
11		cvgratlem1ALT.2	. . . . . . . 8 |- A e. RR
12		1nn 5892	. . . . . . . . 9 |- 1 e. NN
13	12	elimel 2391	. . . . . . . 8 |- if((C - B) e. NN, (C - B), 1) e. NN
14	10, 11, 1, 13	cvgratlem1ALT 7199	. . . . . . 7 |- ((0 < A /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` (B + if((C - B) e. NN, (C - B), 1))) <_ ((A^if((C - B) e. NN, (C - B), 1)) x. (F` B)))
15	9, 14	dedth 2380	. . . . . 6 |- ((C - B) e. NN -> ((0 < A /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` (B + (C - B))) <_ ((A^(C - B)) x. (F` B))))
16	1	nncn 5890	. . . . . . . . 9 |- B e. CC
17	2	nncn 5890	. . . . . . . . 9 |- C e. CC
18	16, 17	pncan3 5361	. . . . . . . 8 |- (B + (C - B)) = C
19	18	fveq2i 3722	. . . . . . 7 |- (F` (B + (C - B))) = (F` C)
20	19	breq1i 2622	. . . . . 6 |- ((F` (B + (C - B))) <_ ((A^(C - B)) x. (F` B)) <-> (F` C) <_ ((A^(C - B)) x. (F` B)))
21	15, 20	syl6ib 212	. . . . 5 |- ((C - B) e. NN -> ((0 < A /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` C) <_ ((A^(C - B)) x. (F` B))))
22	3, 21	sylbi 199	. . . 4 |- (B < C -> ((0 < A /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` C) <_ ((A^(C - B)) x. (F` B))))
23	22	impcom 351	. . 3 |- (((0 < A /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) /\ B < C) -> (F` C) <_ ((A^(C - B)) x. (F` B)))
24	11	recn 5297	. . . . . . . . 9 |- A e. CC
25	24, 2, 1	3pm3.2i 817	. . . . . . . 8 |- (A e. CC /\ C e. NN /\ B e. NN)
26		expsubt 6543	. . . . . . . . 9 |- (((A e. CC /\ C e. NN0 /\ B e. NN0) /\ (A =/= 0 /\ B <_ C)) -> (A^(C - B)) = ((A^C) / (A^B)))
27		id 59	. . . . . . . . . . 11 |- (A e. CC -> A e. CC)
28		nnnn0t 6063	. . . . . . . . . . 11 |- (C e. NN -> C e. NN0)
29		nnnn0t 6063	. . . . . . . . . . 11 |- (B e. NN -> B e. NN0)
30	27, 28, 29	3anim123i 820	. . . . . . . . . 10 |- ((A e. CC /\ C e. NN /\ B e. NN) -> (A e. CC /\ C e. NN0 /\ B e. NN0))
31	30	adantr 389	. . . . . . . . 9 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> (A e. CC /\ C e. NN0 /\ B e. NN0))
32		ltlet 5503	. . . . . . . . . . . . . 14 |- ((B e. RR /\ C e. RR) -> (B < C -> B <_ C))
33		nnret 5887	. . . . . . . . . . . . . 14 |- (B e. NN -> B e. RR)
34		nnret 5887	. . . . . . . . . . . . . 14 |- (C e. NN -> C e. RR)
35	32, 33, 34	syl2an 454	. . . . . . . . . . . . 13 |- ((B e. NN /\ C e. NN) -> (B < C -> B <_ C))
36	35	ancoms 436	. . . . . . . . . . . 12 |- ((C e. NN /\ B e. NN) -> (B < C -> B <_ C))
37	36	3adant1 796	. . . . . . . . . . 11 |- ((A e. CC /\ C e. NN /\ B e. NN) -> (B < C -> B <_ C))
38	37	anim2d 560	. . . . . . . . . 10 |- ((A e. CC /\ C e. NN /\ B e. NN) -> ((A =/= 0 /\ B < C) -> (A =/= 0 /\ B <_ C)))
39	38	imp 350	. . . . . . . . 9 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> (A =/= 0 /\ B <_ C))
40	26, 31, 39	sylanc 471	. . . . . . . 8 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> (A^(C - B)) = ((A^C) / (A^B)))
41	25, 40	mpan 694	. . . . . . 7 |- ((A =/= 0 /\ B < C) -> (A^(C - B)) = ((A^C) / (A^B)))
42	11	gt0ne0 5595	. . . . . . 7 |- (0 < A -> A =/= 0)
43	41, 42	sylan 448	. . . . . 6 |- ((0 < A /\ B < C) -> (A^(C - B)) = ((A^C) / (A^B)))
44	43	opreq1d 3970	. . . . 5 |- ((0 < A /\ B < C) -> ((A^(C - B)) x. (F` B)) = (((A^C) / (A^B)) x. (F` B)))
45		expgt0t 6534	. . . . . . . . 9 |- ((A e. RR /\ B e. NN0 /\ 0 < A) -> 0 < (A^B))
46	45, 29	syl3an2 859	. . . . . . . 8 |- ((A e. RR /\ B e. NN /\ 0 < A) -> 0 < (A^B))
47	11, 1, 46	mp3an12 905	. . . . . . 7 |- (0 < A -> 0 < (A^B))
48		reexpclt 6525	. . . . . . . . . 10 |- ((A e. RR /\ B e. NN0) -> (A^B) e. RR)
49	48, 29	sylan2 451	. . . . . . . . 9 |- ((A e. RR /\ B e. NN) -> (A^B) e. RR)
50	11, 1, 49	mp2an 696	. . . . . . . 8 |- (A^B) e. RR
51	50	gt0ne0 5595	. . . . . . 7 |- (0 < (A^B) -> (A^B) =/= 0)
52	10	ffvelrni 3810	. . . . . . . . . . 11 |- (B e. NN -> (F` B) e. RR)
53	1, 52	ax-mp 7	. . . . . . . . . 10 |- (F` B) e. RR
54	53	recn 5297	. . . . . . . . 9 |- (F` B) e. CC
55	50	recn 5297	. . . . . . . . 9 |- (A^B) e. CC
56		expclt 6526	. . . . . . . . . . 11 |- ((A e. CC /\ C e. NN0) -> (A^C) e. CC)
57	56, 28	sylan2 451	. . . . . . . . . 10 |- ((A e. CC /\ C e. NN) -> (A^C) e. CC)
58	24, 2, 57	mp2an 696	. . . . . . . . 9 |- (A^C) e. CC
59	54, 55, 58	3pm3.2i 817	. . . . . . . 8 |- ((F` B) e. CC /\ (A^B) e. CC /\ (A^C) e. CC)
60		div13t 5716	. . . . . . . 8 |- ((((F` B)