HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem cvgratlem1 7455
Description: Lemma for cvgrati 7460. 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
StepHypRef Expression
1 opreq2 4027 . . . . . . 7 |- (y = 1 -> (B + y) = (B + 1))
21fveq2d 3839 . . . . . 6 |- (y = 1 -> (F` (B + y)) = (F` (B + 1)))
3 opreq2 4027 . . . . . . 7 |- (y = 1 -> (A^y) = (A^1))
43opreq1d 4033 . . . . . 6 |- (y = 1 -> ((A^y) x. (F` B)) = ((A^1) x. (F` B)))
52, 4breq12d 2704 . . . . 5 |- (y = 1 -> ((F` (B + y)) < ((A^y) x. (F` B)) <-> (F` (B + 1)) < ((A^1) x. (F` B))))
65imbi2d 615 . . . 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 4027 . . . . . . 7 |- (y = z -> (B + y) = (B + z))
87fveq2d 3839 . . . . . 6 |- (y = z -> (F` (B + y)) = (F` (B + z)))
9 opreq2 4027 . . . . . . 7 |- (y = z -> (A^y) = (A^z))
109opreq1d 4033 . . . . . 6 |- (y = z -> ((A^y) x. (F` B)) = ((A^z) x. (F` B)))
118, 10breq12d 2704 . . . . 5 |- (y = z -> ((F` (B + y)) < ((A^y) x. (F` B)) <-> (F` (B + z)) < ((A^z) x. (F` B))))
1211imbi2d 615 . . . 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 4027 . . . . . . 7 |- (y = (z + 1) -> (B + y) = (B + (z + 1)))
1413fveq2d 3839 . . . . . 6 |- (y = (z + 1) -> (F` (B + y)) = (F` (B + (z + 1))))
15 opreq2 4027 . . . . . . 7 |- (y = (z + 1) -> (A^y) = (A^(z + 1)))
1615opreq1d 4033 . . . . . 6 |- (y = (z + 1) -> ((A^y) x. (F` B)) = ((A^(z + 1)) x. (F` B)))
1714, 16breq12d 2704 . . . . 5 |- (y = (z + 1) -> ((F` (B + y)) < ((A^y) x. (F` B)) <-> (F` (B + (z + 1))) < ((A^(z + 1)) x. (F` B))))
1817imbi2d 615 . . . 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 4027 . . . . . . 7 |- (y = C -> (B + y) = (B + C))
2019fveq2d 3839 . . . . . 6 |- (y = C -> (F` (B + y)) = (F` (B + C)))
21 opreq2 4027 . . . . . . 7 |- (y = C -> (A^y) = (A^C))
2221opreq1d 4033 . . . . . 6 |- (y = C -> ((A^y) x. (F` B)) = ((A^C) x. (F` B)))
2320, 22breq12d 2704 . . . . 5 |- (y = C -> ((F` (B + y)) < ((A^y) x. (F` B)) <-> (F` (B + C)) < ((A^C) x. (F` B))))
2423imbi2d 615 . . . 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 nnre 6074 . . . . . . . . 9 |- (B e. NN -> B e. RR)
26 leid 5685 . . . . . . . . 9 |- (B e. RR -> B <_ B)
2725, 26syl 10 . . . . . . . 8 |- (B e. NN -> B <_ B)
28 breq2 2696 . . . . . . . . . 10 |- (x = B -> (B <_ x <-> B <_ B))
29 opreq1 4026 . . . . . . . . . . . 12 |- (x = B -> (x + 1) = (B + 1))
3029fveq2d 3839 . . . . . . . . . . 11 |- (x = B -> (F` (x + 1)) = (F` (B + 1)))
31 fveq2 3835 . . . . . . . . . . . 12 |- (x = B -> (F` x) = (F` B))
3231opreq2d 4034 . . . . . . . . . . 11 |- (x = B -> (A x. (F` x)) = (A x. (F` B)))
3330, 32breq12d 2704 . . . . . . . . . 10 |- (x = B -> ((F` (x + 1)) < (A x. (F` x)) <-> (F` (B + 1)) < (A x. (F` B))))
3428, 33imbi12d 629 . . . . . . . . 9 |- (x = B -> ((B <_ x -> (F` (x + 1)) < (A x. (F` x))) <-> (B <_ B -> (F` (B + 1)) < (A x. (F` B)))))
3534rcla4v 1919 . . . . . . . 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)))))
3627, 35mpid 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))))
3736imp 348 . . . . . 6 |- ((B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (F` (B + 1)) < (A x. (F` B)))
3837adantl 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 recn 5467 . . . . . . . . 9 |- (A e. RR -> A e. CC)
40 exp1 6768 . . . . . . . . 9 |- (A e. CC -> (A^1) = A)
4139, 40syl 10 . . . . . . . 8 |- (A e. RR -> (A^1) = A)
4241adantr 389 . . . . . . 7 |- ((A e. RR /\ 0 < A) -> (A^1) = A)
4342opreq1d 4033 . . . . . 6 |- ((A e. RR /\ 0 < A) -> ((A^1) x. (F` B)) = (A x. (F` B)))
4443adantr 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)))
4538, 44breqtrrd 2714 . . . 4 |- (((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)))
46 axlttrn 5658 . . . . . . . . . . . . . . 15 |- (((F` ((B + z) + 1)) e. RR /\ (A x. (F` (B + z))) e. RR /\ (A x. ((A^z) x. (F` B))) e. RR) -> (((F` ((B + z) + 1)) < (A x. (F` (B + z))) /\ (A x. (F` (B + z))) < (A x. ((A^z) x. (F` B)))) -> (F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B)))))
47 nnaddcl 6085 . . . . . . . . . . . . . . . . . . 19 |- ((B e. NN /\ z e. NN) -> (B + z) e. NN)
4847ancoms 438 . . . . . . . . . . . . . . . . . 18 |- ((z e. NN /\ B e. NN) -> (B + z) e. NN)
49 peano2nn 6080 . . . . . . . . . . . . . . . . . 18 |- ((B + z) e. NN -> ((B + z) + 1) e. NN)
5048, 49syl 10 . . . . . . . . . . . . . . . . 17 |- ((z e. NN /\ B e. NN) -> ((B + z) + 1) e. NN)
51 cvgratlem1.1 . . . . . . . . . . . . . . . . . 18 |- F:NN-->RR
5251ffvelrni 3929 . . . . . . . . . . . . . . . . 17 |- (((B + z) + 1) e. NN -> (F` ((B + z) + 1)) e. RR)
5350, 52syl 10 . . . . . . . . . . . . . . . 16 |- ((z e. NN /\ B e. NN) -> (F` ((B + z) + 1)) e. RR)
5453adantll 392 . . . . . . . . . . . . . . 15 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> (F` ((B + z) + 1)) e. RR)
55 remulcl 5458 . . . . . . . . . . . . . . . . 17 |- ((A e. RR /\ (F` (B + z)) e. RR) -> (A x. (F` (B + z))) e. RR)
5651ffvelrni 3929 . . . . . . . . . . . . . . . . . 18 |- ((B + z) e. NN -> (F` (B + z)) e. RR)
5748, 56syl 10 . . . . . . . . . . . . . . . . 17 |- ((z e. NN /\ B e. NN) -> (F` (B + z)) e. RR)
5855, 57sylan2 453 . . . . . . . . . . . . . . . 16 |- ((A e. RR /\ (z e. NN /\ B e. NN)) -> (A x. (F` (B + z))) e. RR)
5958anassrs 443 . . . . . . . . . . . . . . 15 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> (A x. (F` (B + z))) e. RR)
60 remulcl 5458 . . . . . . . . . . . . . . . 16 |- ((A e. RR /\ ((A^z) x. (F` B)) e. RR) -> (A x. ((A^z) x. (F` B))) e. RR)
61 simpll 412 . . . . . . . . . . . . . . . 16 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> A e. RR)
62 remulcl 5458 . . . . . . . . . . . . . . . . 17 |- (((A^z) e. RR /\ (F` B) e. RR) -> ((A^z) x. (F` B)) e. RR)
63 reexpcl 6775 . . . . . . . . . . . . . . . . . 18 |- ((A e. RR /\ z e. NN0) -> (A^z) e. RR)
64 nnnn0 6274 . . . . . . . . . . . . . . . . . 18 |- (z e. NN -> z e. NN0)
6563, 64sylan2 453 . . . . . . . . . . . . . . . . 17 |- ((A e. RR /\ z e. NN) -> (A^z) e. RR)
6651ffvelrni 3929 . . . . . . . . . . . . . . . . 17 |- (B e. NN -> (F` B) e. RR)
6762, 65, 66syl2an 456 . . . . . . . . . . . . . . . 16 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> ((A^z) x. (F` B)) e. RR)
6860, 61, 67sylanc 473 . . . . . . . . . . . . . . 15 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> (A x. ((A^z) x. (F` B))) e. RR)
6946, 54, 59, 68syl3anc 864 . . . . . . . . . . . . . 14 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> (((F` ((B + z) + 1)) < (A x. (F` (B + z))) /\ (A x. (F` (B + z))) < (A x. ((A^z) x. (F` B)))) -> (F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B)))))
70 nn0addge1 6298 . . . . . . . . . . . . . . . . . 18 |- ((B e. RR /\ z e. NN0) -> B <_ (B + z))
7170, 25, 64syl2an 456 . . . . . . . . . . . . . . . . 17 |- ((B e. NN /\ z e. NN) -> B <_ (B + z))
72 breq2 2696 . . . . . . . . . . . . . . . . . . . 20 |- (x = (B + z) -> (B <_ x <-> B <_ (B + z)))
73 opreq1 4026 . . . . . . . . . . . . . . . . . . . . . 22 |- (x = (B + z) -> (x + 1) = ((B + z) + 1))
7473fveq2d 3839 . . . . . . . . . . . . . . . . . . . . 21 |- (x = (B + z) -> (F` (x + 1)) = (F` ((B + z) + 1)))
75 fveq2 3835 . . . . . . . . . . . . . . . . . . . . . 22 |- (x = (B + z) -> (F` x) = (F` (B + z)))
7675opreq2d 4034 . . . . . . . . . . . . . . . . . . . . 21 |- (x = (B + z) -> (A x. (F` x)) = (A x. (F` (B + z))))
7774, 76breq12d 2704 . . . . . . . . . . . . . . . . . . . 20 |- (x = (B + z) -> ((F` (x + 1)) < (A x. (F` x)) <-> (F` ((B + z) + 1)) < (A x. (F` (B + z)))))
7872, 77imbi12d 629 . . . . . . . . . . . . . . . . . . 19 |- (x = (B + z) -> ((B <_ x -> (F` (x + 1)) < (A x. (F` x))) <-> (B <_ (B + z) -> (F` ((B + z) + 1)) < (A x. (F` (B + z))))))
7978rcla4v 1919 . . . . . . . . . . . . . . . . . 18 |- ((B + z) e. NN -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> (B <_ (B + z) -> (F` ((B + z) + 1)) < (A x. (F` (B + z))))))
8047, 79syl 10 . . . . . . . . . . . . . . . . 17 |- ((B e. NN /\ z e. NN) -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> (B <_ (B + z) -> (F` ((B + z) + 1)) < (A x. (F` (B + z))))))
8171, 80mpid 47 . . . . . . . . . . . . . . . 16 |- ((B e. NN /\ z e. NN) -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> (F` ((B + z) + 1)) < (A x. (F` (B + z)))))
8281ancoms 438 . . . . . . . . . . . . . . 15 |- ((z e. NN /\ B e. NN) -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> (F` ((B + z) + 1)) < (A x. (F` (B + z)))))
8382adantll 392 . . . . . . . . . . . . . 14 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> (F` ((B + z) + 1)) < (A x. (F` (B + z)))))
84 ltmul2OLD 5972 . . . . . . . . . . . . . . . . . 18 |- ((((F` (B + z)) e. RR /\ ((A^z) x. (F` B)) e. RR /\ A e. RR) /\ 0 < A) -> ((F` (B + z)) < ((A^z) x. (F` B)) <-> (A x. (F` (B + z))) < (A x. ((A^z) x. (F` B)))))
8584biimpd 151 . . . . . . . . . . . . . . . . 17 |- ((((F` (B + z)) e. RR /\ ((A^z) x. (F` B)) e. RR /\ A e. RR) /\ 0 < A) -> ((F` (B + z)) < ((A^z) x. (F` B)) -> (A x. (F` (B + z))) < (A x. ((A^z) x. (F` B)))))
8685ex 371 . . . . . . . . . . . . . . . 16 |- (((F` (B + z)) e. RR /\ ((A^z) x. (F` B)) e. RR /\ A e. RR) -> (0 < A -> ((F` (B + z)) < ((A^z) x. (F` B)) -> (A x. (F` (B + z))) < (A x. ((A^z) x. (F` B))))))
8748adantll 392 . . . . . . . . . . . . . . . . 17 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> (B + z) e. NN)
8887, 56syl 10 . . . . . . . . . . . . . . . 16 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> (F` (B + z)) e. RR)
8986, 88, 67, 61syl3anc 864 . . . . . . . . . . . . . . 15 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> (0 < A -> ((F` (B + z)) < ((A^z) x. (F` B)) -> (A x. (F` (B + z))) < (A x. ((A^z) x. (F` B))))))
9089imp3a 359 . . . . . . . . . . . . . 14 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> ((0 < A /\ (F` (B + z)) < ((A^z) x. (F` B))) -> (A x. (F` (B + z))) < (A x. ((A^z) x. (F` B)))))
9169, 83, 90syl2and 461 . . . . . . . . . . . . 13 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> ((A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) /\ (0 < A /\ (F` (B + z)) < ((A^z) x. (F` B)))) -> (F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B)))))
9291exp4d 381 . . . . . . . . . . . 12 |- (((A e. RR /\ z e. NN) /\ B e. NN) -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> (0 < A -> ((F` (B + z)) < ((A^z) x. (F` B)) -> (F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B)))))))
9392exp31 376 . . . . . . . . . . 11 |- (A e. RR -> (z e. NN -> (B e. NN -> (A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x))) -> (0 < A -> ((F` (B + z)) < ((A^z) x. (F` B)) -> (F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B)))))))))
9493imp4a 362 . . . . . . . . . 10 |- (A e. RR -> (z e. NN -> ((B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (0 < A -> ((F` (B + z)) < ((A^z) x. (F` B)) -> (F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B))))))))
9594com12 11 . . . . . . . . 9 |- (z e. NN -> (A e. RR -> ((B e. NN /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) -> (0 < A -> ((F` (B + z)) < ((A^z) x. (F` B)) -> (F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B))))))))
9695com34 36 . . . . . . . 8 |- (z 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 + z)) < ((A^z) x. (F` B)) -> (F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B))))))))
9796imp44 369 . . . . . . 7 |- ((z 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 + z)) < ((A^z) x. (F` B)) -> (F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B)))))
98 ax1cn 5423 . . . . . . . . . . . . . . . 16 |- 1 e. CC
99 addass 5461 . . . . . . . . . . . . . . . 16 |- ((B e. CC /\ z e. CC /\ 1 e. CC) -> ((B + z) + 1) = (B + (z + 1)))
10098, 99mp3an3 911 . . . . . . . . . . . . . . 15 |- ((B e. CC /\ z e. CC) -> ((B + z) + 1) = (B + (z + 1)))
101 nncn 6075 . . . . . . . . . . . . . . 15 |- (B e. NN -> B e. CC)
102 nncn 6075 . . . . . . . . . . . . . . 15 |- (z e. NN -> z e. CC)
103100, 101, 102syl2an 456 . . . . . . . . . . . . . 14 |- ((B e. NN /\ z e. NN) -> ((B + z) + 1) = (B + (z + 1)))
104103fveq2d 3839 . . . . . . . . . . . . 13 |- ((B e. NN /\ z e. NN) -> (F` ((B + z) + 1)) = (F` (B + (z + 1))))
105104adantll 392 . . . . . . . . . . . 12 |- (((A e. CC /\ B e. NN) /\ z e. NN) -> (F` ((B + z) + 1)) = (F` (B + (z + 1))))
106 expp1 6769 . . . . . . . . . . . . . . . . 17 |- ((A e. CC /\ z e. NN0) -> (A^(z + 1)) = ((A^z) x. A))
107106, 64sylan2 453 . . . . . . . . . . . . . . . 16 |- ((A e. CC /\ z e. NN) -> (A^(z + 1)) = ((A^z) x. A))
108 mulcom 5460 . . . . . . . . . . . . . . . . 17 |- (((A^z) e. CC /\ A e. CC) -> ((A^z) x. A) = (A x. (A^z)))
109 expcl 6776 . . . . . . . . . . . . . . . . . 18 |- ((A e. CC /\ z e. NN0) -> (A^z) e. CC)
110109, 64sylan2 453 . . . . . . . . . . . . . . . . 17 |- ((A e. CC /\ z e. NN) -> (A^z) e. CC)
111 pm3.26 317 . . . . . . . . . . . . . . . . 17 |- ((A e. CC /\ z e. NN) -> A e. CC)
112108, 110, 111sylanc 473 . . . . . . . . . . . . . . . 16 |- ((A e. CC /\ z e. NN) -> ((A^z) x. A) = (A x. (A^z)))
113107, 112eqtrd 1550 . . . . . . . . . . . . . . 15 |- ((A e. CC /\ z e. NN) -> (A^(z + 1)) = (A x. (A^z)))
114113adantlr 393 . . . . . . . . . . . . . 14 |- (((A e. CC /\ B e. NN) /\ z e. NN) -> (A^(z + 1)) = (A x. (A^z)))
115114opreq1d 4033 . . . . . . . . . . . . 13 |- (((A e. CC /\ B e. NN) /\ z e. NN) -> ((A^(z + 1)) x. (F` B)) = ((A x. (A^z)) x. (F` B)))
116 mulass 5462 . . . . . . . . . . . . . . . 16 |- ((A e. CC /\ (A^z) e. CC /\ (F` B) e. CC) -> ((A x. (A^z)) x. (F` B)) = (A x. ((A^z) x. (F` B))))
1171163expa 839 . . . . . . . . . . . . . . 15 |- (((A e. CC /\ (A^z) e. CC) /\ (F` B) e. CC) -> ((A x. (A^z)) x. (F` B)) = (A x. ((A^z) x. (F` B))))
118111, 110jca 286 . . . . . . . . . . . . . . 15 |- ((A e. CC /\ z e. NN) -> (A e. CC /\ (A^z) e. CC))
11966recnd 5469 . . . . . . . . . . . . . . 15 |- (B e. NN -> (F` B) e. CC)
120117, 118, 119syl2an 456 . . . . . . . . . . . . . 14 |- (((A e. CC /\ z e. NN) /\ B e. NN) -> ((A x. (A^z)) x. (F` B)) = (A x. ((A^z) x. (F` B))))
121120an1rs 492 . . . . . . . . . . . . 13 |- (((A e. CC /\ B e. NN) /\ z e. NN) -> ((A x. (A^z)) x. (F` B)) = (A x. ((A^z) x. (F` B))))
122115, 121eqtr2d 1551 . . . . . . . . . . . 12 |- (((A e. CC /\ B e. NN) /\ z e. NN) -> (A x. ((A^z) x. (F` B))) = ((A^(z + 1)) x. (F` B)))
123105, 122breq12d 2704 . . . . . . . . . . 11 |- (((A e. CC /\ B e. NN) /\ z e. NN) -> ((F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B))) <-> (F` (B + (z + 1))) < ((A^(z + 1)) x. (F` B))))
124123, 39sylanl1 462 . . . . . . . . . 10 |- (((A e. RR /\ B e. NN) /\ z e. NN) -> ((F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B))) <-> (F` (B + (z + 1))) < ((A^(z + 1)) x. (F` B))))
125124ancoms 438 . . . . . . . . 9 |- ((z e. NN /\ (A e. RR /\ B e. NN)) -> ((F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B))) <-> (F` (B + (z + 1))) < ((A^(z + 1)) x. (F` B))))
126125adantrlr 401 . . . . . . . 8 |- ((z e. NN /\ ((A e. RR /\ 0 < A) /\ B e. NN)) -> ((F` ((B + z) + 1)) < (A x. ((A^z) x. (F` B))) <-> (F` (B + (z + 1))) < ((A^(z + 1)) x. (F` B))))
127126adantrrr 403 . . . . . . 7 |- ((z 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 + z) + 1)) < (A x. ((A^z) x. (F` B))) <-> (F` (B + (z + 1))) < ((A^(z + 1)) x. (F` B))))
12897, 127sylibd 200 . . . . . 6 |- ((z 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 + z)) < ((A^z) x. (F` B)) -> (F` (B + (z + 1))) < ((A^(z + 1)) x. (F` B))))
129128ex 371 . . . . 5 |- (z 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 + z)) < ((A^z) x. (F` B)) -> (F` (B + (z + 1))) < ((A^(z + 1)) x. (F` B)))))
130129a2d 13 . . . 4 |- (z 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 + z)) < ((A^z) 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)))))
1316, 12, 18, 24, 45, 130nnind 6082 . . 3 |- (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))))
132131imp 348 . 2 |- ((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)))
133 ltle 5674 . . . . 5 |- (((F` (B + C)) e. RR /\ ((A^C) x. (F` B)) e. RR) -> ((F` (B + C)) < ((A^C) x. (F` B)) -> (F` (B + C)) <_ ((A^C) x. (F` B))))
134 nnaddcl 6085 . . . . . . . 8 |- ((B e. NN /\ C e. NN) -> (B + C) e. NN)
135134ancoms 438 . . . . . . 7 |- ((C e. NN /\ B e. NN) -> (B + C) e. NN)
13651ffvelrni 3929 . . . . . . 7 |- ((B + C) e. NN -> (F` (B + C)) e. RR)
137135, 136syl 10 . . . . . 6 |- ((C e. NN /\ B e. NN) -> (F` (B + C)) e. RR)
138137adantrl 394 . . . . 5 |- ((C e. NN /\ (A e. RR /\ B e. NN)) -> (F` (B + C)) e. RR)
139 remulcl 5458 . . . . . . 7 |- (((A^C) e. RR /\ (F` B) e. RR) -> ((A^C) x. (F` B)) e. RR)
140 reexpcl 6775 . . . . . . . . 9 |- ((A e. RR /\ C e. NN0) -> (A^C) e. RR)
141 nnnn0 6274 . . . . . . . . 9 |- (C e. NN -> C e. NN0)
142140, 141sylan2 453 . . . . . . . 8 |- ((A e. RR /\ C e. NN) -> (A^C) e. RR)
143142ancoms 438 . . . . . . 7 |- ((C e. NN /\ A e. RR) -> (A^C) e. RR)
144139, 143, 66syl2an 456 . . . . . 6 |- (((C e. NN /\ A e. RR) /\ B e. NN) -> ((A^C) x. (F` B)) e. RR)
145144anasss 442 . . . . 5 |- ((C e. NN /\ (A e. RR /\ B e. NN)) -> ((A^C) x. (F` B)) e. RR)
146133, 138, 145sylanc 473 . . . 4 |- ((C e. NN /\ (A e. RR /\ B e. NN)) -> ((F` (B + C)) < ((A^C) x. (F` B)) -> (F` (B + C)) <_ ((A^C) x. (F` B))))
147146adantrlr 401 . . 3 |- ((C e. NN /\ ((A e. RR /\ 0 < A) /\ B e. NN)) -> ((F` (B + C)) < ((A^C) x. (F` B)) -> (F` (B + C)) <_ ((A^C) x. (F` B))))
148147adantrrr 403 . 2 |- ((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)) -> (F` (B + C)) <_ ((A^C) x. (F` B))))
149132, 148mpd 26 1 |- ((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)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   /\ w3a 781   = wceq 992   e. wcel 994  A.wral 1691   class class class wbr 2692  -->wf 3259  ` cfv 3263  (class class class)co 4021  CCcc 5386  RRcr 5387  0cc0 5388  1c1 5389   + caddc 5391   x. cmul 5393   <_ cle 5449  NNcn 5450  NN0cn0 5451   < clt 5640  ^cexp 6763
This theorem is referenced by:  cvgratlem2 7456
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089  ax-inf2 4770
This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-nel 1631  df-ral 1695  df-rex 1696  df-reu 1697  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-int 2601  df-iun 2635  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-opr 4023  df-oprab 4024  df-1st 4140  df-2nd 4141  df-rdg 4233  df-1o 4269  df-oadd 4271  df-omul 4272  df-er 4401  df-ec 4403  df-qs 4406  df-en 4509  df-dom 4510  df-sdom 4511  df-ni 5154  df-pli 5155  df-mi 5156  df-lti 5157  df-plpq 5189  df-mpq 5190  df-enq 5191  df-nq 5192  df-plq 5193  df-mq 5194  df-rq 5195  df-ltq 5196  df-1q 5197  df-np 5240  df-1p 5241  df-plp 5242  df-mp 5243  df-ltp 5244  df-plpr 5318  df-mpr 5319  df-enr 5320  df-nr 5321  df-plr 5322  df-mr 5323  df-ltr 5324  df-0r 5325  df-1r 5326  df-m1r 5327  df-c 5394  df-0 5395  df-1 5396  df-i 5397  df-r 5398  df-plus 5399  df-mul 5400  df-lt 5401  df-sub 5510  df-neg 5512  df-pnf 5641  df-mnf 5642  df-xr 5643  df-ltxr 5644  df-le 5645  df-n 6070  df-n0 6268  df-z 6304  df-seq1 6673  df-exp 6764
Copyright terms: Public domain