HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem cvgratlem2 7251
Description: Lemma for cvgrat 7255. Using expsubt 6599, restate cvgratlem1 7250 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
StepHypRef Expression
1 nnsubt 5959 . . . . . . . . . 10 |- ((B e. NN /\ C e. NN) -> (B < C <-> (C - B) e. NN))
2 cvgratlem1.1 . . . . . . . . . . . . . . . . 17 |- F:NN-->RR
32cvgratlem1 7250 . . . . . . . . . . . . . . . 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)))
43exp45 388 . . . . . . . . . . . . . . 15 |- ((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))))))
54com3r 35 . . . . . . . . . . . . . 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))))))
65imp4d 367 . . . . . . . . . . . . 13 |- (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))))
76adantr 391 . . . . . . . . . . . 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` (B + (C - B))) <_ ((A^(C - B)) x. (F` B))))
8 pncan3t 5389 . . . . . . . . . . . . . . 15 |- ((B e. CC /\ C e. CC) -> (B + (C - B)) = C)
9 nncnt 5932 . . . . . . . . . . . . . . 15 |- (B e. NN -> B e. CC)
10 nncnt 5932 . . . . . . . . . . . . . . 15 |- (C e. NN -> C e. CC)
118, 9, 10syl2an 456 . . . . . . . . . . . . . 14 |- ((B e. NN /\ C e. NN) -> (B + (C - B)) = C)
1211fveq2d 3734 . . . . . . . . . . . . 13 |- ((B e. NN /\ C e. NN) -> (F` (B + (C - B))) = (F` C))
1312breq1d 2634 . . . . . . . . . . . 12 |- ((B e. NN /\ C e. NN) -> ((F` (B + (C - B))) <_ ((A^(C - B)) x. (F` B)) <-> (F` C) <_ ((A^(C - B)) x. (F` B))))
147, 13sylibd 202 . . . . . . . . . . 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))))
1514exp3a 376 . . . . . . . . . 10 |- ((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)))))
161, 15sylbid 203 . . . . . . . . 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)))))
1716expimpd 375 . . . . . . . 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)))))
1817exp4a 380 . . . . . . 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))))))
1918com12 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))))))
2019com4l 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))))))
2120com12 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))))))
2221imp42 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)))
23 expsubt 6599 . . . . . . . 8 |- (((A e. CC /\ C e. NN0 /\ B e. NN0) /\ (A =/= 0 /\ B <_ C)) -> (A^(C - B)) = ((A^C) / (A^B)))
24 id 59 . . . . . . . . . 10 |- (A e. CC -> A e. CC)
25 nnnn0t 6108 . . . . . . . . . 10 |- (C e. NN -> C e. NN0)
26 nnnn0t 6108 . . . . . . . . . 10 |- (B e. NN -> B e. NN0)
2724, 25, 263anim123i 823 . . . . . . . . 9 |- ((A e. CC /\ C e. NN /\ B e. NN) -> (A e. CC /\ C e. NN0 /\ B e. NN0))
2827adantr 391 . . . . . . . 8 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> (A e. CC /\ C e. NN0 /\ B e. NN0))
29 ltlet 5532 . . . . . . . . . . . . 13 |- ((B e. RR /\ C e. RR) -> (B < C -> B <_ C))
3029ancoms 438 . . . . . . . . . . . 12 |- ((C e. RR /\ B e. RR) -> (B < C -> B <_ C))
31 nnret 5931 . . . . . . . . . . . 12 |- (C e. NN -> C e. RR)
32 nnret 5931 . . . . . . . . . . . 12 |- (B e. NN -> B e. RR)
3330, 31, 32syl2an 456 . . . . . . . . . . 11 |- ((C e. NN /\ B e. NN) -> (B < C -> B <_ C))
34333adant1 799 . . . . . . . . . 10 |- ((A e. CC /\ C e. NN /\ B e. NN) -> (B < C -> B <_ C))
3534anim2d 563 . . . . . . . . 9 |- ((A e. CC /\ C e. NN /\ B e. NN) -> ((A =/= 0 /\ B < C) -> (A =/= 0 /\ B <_ C)))
3635imp 350 . . . . . . . 8 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> (A =/= 0 /\ B <_ C))
3723, 28, 36sylanc 473 . . . . . . 7 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> (A^(C - B)) = ((A^C) / (A^B)))
38 recnt 5325 . . . . . . . . . 10 |- (A e. RR -> A e. CC)
3938adantr 391 . . . . . . . . 9 |- ((A e. RR /\ 0 < A) -> A e. CC)
4039ad2antrr 406 . . . . . . . 8 |- ((((A e. RR /\ 0 < A) /\ B e. NN) /\ (C e. NN /\ B < C)) -> A e. CC)
41 simprl 416 . . . . . . . 8 |- ((((A e. RR /\ 0 < A) /\ B e. NN) /\ (C e. NN /\ B < C)) -> C e. NN)
42 simplr 415 . . . . . . . 8 |- ((((A e. RR /\ 0 < A) /\ B e. NN) /\ (C e. NN /\ B < C)) -> B e. NN)
4340, 41, 423jca 821 . . . . . . 7 |- (