Theorem cvgratlem2 7194

Description: Lemma for cvgrat 7198. Using expsubt 6537, restate cvgratlem1 7193 with an absolute index C instead of just an offset from the starting index B.

Hypothesis

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

Assertion

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

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

Proof of Theorem cvgratlem2

Step	Hyp	Ref	Expression
1		nnsubt 5912	. . . . . . . . . . 11 |- ((B e. NN /\ C e. NN) -> (B < C <-> (C - B) e. NN))
2		cvgratlem1.1	. . . . . . . . . . . . . . . . . 18 |- F:NN-->RR
3	2	cvgratlem1 7193	. . . . . . . . . . . . . . . . 17 |- (((C - B) 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 - B))) <_ ((A^(C - B)) x. (F` B)))
4	3	exp45 386	. . . . . . . . . . . . . . . 16 |- ((C - B) 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 - B))) <_ ((A^(C - B)) x. (F` B))))))
5	4	com3r 35	. . . . . . . . . . . . . . 15 |- (B e. NN -> ((C - B) e. NN -> ((A e. RR /\ 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))))))
6	5	imp4d 367	. . . . . . . . . . . . . 14 |- (B e. NN -> (((C - B) e. NN /\ ((A e. RR /\ 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))))
7	6	adantr 389	. . . . . . . . . . . . 13 |- ((B e. NN /\ C e. NN) -> (((C - B) e. NN /\ ((A e. RR /\ 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))))
8		pncan3t 5357	. . . . . . . . . . . . . . . 16 |- ((B e. CC /\ C e. CC) -> (B + (C - B)) = C)
9		nncnt 5886	. . . . . . . . . . . . . . . 16 |- (B e. NN -> B e. CC)
10		nncnt 5886	. . . . . . . . . . . . . . . 16 |- (C e. NN -> C e. CC)
11	8, 9, 10	syl2an 454	. . . . . . . . . . . . . . 15 |- ((B e. NN /\ C e. NN) -> (B + (C - B)) = C)
12	11	fveq2d 3719	. . . . . . . . . . . . . 14 |- ((B e. NN /\ C e. NN) -> (F` (B + (C - B))) = (F` C))
13	12	breq1d 2624	. . . . . . . . . . . . 13 |- ((B e. NN /\ C e. NN) -> ((F` (B + (C - B))) <_ ((A^(C - B)) x. (F` B)) <-> (F` C) <_ ((A^(C - B)) x. (F` B))))
14	7, 13	sylibd 202	. . . . . . . . . . . 12 |- ((B e. NN /\ C e. NN) -> (((C - B) e. NN /\ ((A e. RR /\ 0 < A) /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) -> (F` C) <_ ((A^(C - B)) x. (F` B))))
15	14	exp3a 375	. . . . . . . . . . 11 |- ((B e. NN /\ C e. NN) -> ((C - B) e. NN -> (((A e. RR /\ 0 < A) /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` C) <_ ((A^(C - B)) x. (F` B)))))
16	1, 15	sylbid 203	. . . . . . . . . 10 |- ((B e. NN /\ C e. NN) -> (B < C -> (((A e. RR /\ 0 < A) /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` C) <_ ((A^(C - B)) x. (F` B)))))
17	16	ex 373	. . . . . . . . 9 |- (B e. NN -> (C e. NN -> (B < C -> (((A e. RR /\ 0 < A) /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` C) <_ ((A^(C - B)) x. (F` B))))))
18	17	imp3a 361	. . . . . . . 8 |- (B e. NN -> ((C e. NN /\ B < C) -> (((A e. RR /\ 0 < A) /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` C) <_ ((A^(C - B)) x. (F` B)))))
19	18	exp4a 378	. . . . . . 7 |- (B e. NN -> ((C e. NN /\ B < C) -> ((A e. RR /\ 0 < A) -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> (F` C) <_ ((A^(C - B)) x. (F` B))))))
20	19	com12 11	. . . . . 6 |- ((C e. NN /\ B < C) -> (B e. NN -> ((A e. RR /\ 0 < A) -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> (F` C) <_ ((A^(C - B)) x. (F` B))))))
21	20	com4l 39	. . . . 5 |- (B e. NN -> ((A e. RR /\ 0 < A) -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> ((C e. NN /\ B < C) -> (F` C) <_ ((A^(C - B)) x. (F` B))))))
22	21	com12 11	. . . 4 |- ((A e. RR /\ 0 < A) -> (B e. NN -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> ((C e. NN /\ B < C) -> (F` C) <_ ((A^(C - B)) x. (F` B))))))
23	22	imp42 369	. . 3 |- ((((A e. RR /\ 0 < A) /\ (B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))))) /\ (C e. NN /\ B < C)) -> (F` C) <_ ((A^(C - B)) x. (F` B)))
24		expsubt 6537	. . . . . . . 8 |- (((A e. CC /\ C e. NN0 /\ B e. NN0) /\ (A =/= 0 /\ B <_ C)) -> (A^(C - B)) = ((A^C) / (A^B)))
25		id 59	. . . . . . . . . 10 |- (A e. CC -> A e. CC)
26		nnnn0t 6061	. . . . . . . . . 10 |- (C e. NN -> C e. NN0)
27		nnnn0t 6061	. . . . . . . . . 10 |- (B e. NN -> B e. NN0)
28	25, 26, 27	3anim123i 820	. . . . . . . . 9 |- ((A e. CC /\ C e. NN /\ B e. NN) -> (A e. CC /\ C e. NN0 /\ B e. NN0))
29	28	adantr 389	. . . . . . . 8 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> (A e. CC /\ C e. NN0 /\ B e. NN0))
30		ltlet 5501	. . . . . . . . . . . . 13 |- ((B e. RR /\ C e. RR) -> (B < C -> B <_ C))
31	30	ancoms 436	. . . . . . . . . . . 12 |- ((C e. RR /\ B e. RR) -> (B < C -> B <_ C))
32		nnret 5885	. . . . . . . . . . . 12 |- (C e. NN -> C e. RR)
33		nnret 5885	. . . . . . . . . . . 12 |- (B e. NN -> B e. RR)
34	31, 32, 33	syl2an 454	. . . . . . . . . . 11 |- ((C e. NN /\ B e. NN) -> (B < C -> B <_ C))
35	34	3adant1 796	. . . . . . . . . 10 |- ((A e. CC /\ C e. NN /\ B e. NN) -> (B < C -> B <_ C))
36	35	anim2d 560	. . . . . . . . 9 |- ((A e. CC /\ C e. NN /\ B e. NN) -> ((A =/= 0 /\ B < C) -> (A =/= 0 /\ B <_ C)))
37	36	imp 350	. . . . . . . 8 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> (A =/= 0 /\ B <_ C))
38	24, 29, 37	sylanc 471	. . . . . . 7 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> (A^(C - B)) = ((A^C) / (A^B)))
39		recnt 5293	. . . . . . . . . 10 |- (A e. RR -> A e. CC)
40	39	adantr 389	. . . . . . . . 9 |- ((A e. RR /\ 0 < A) -> A e. CC)
41	40	ad2antrr 404	. . . . . . . 8 |- ((((A e. RR /\ 0 < A) /\ B e. NN) /\ (C e. NN /\ B < C