Theorem cvgratlem2ALT 9026

Description: Lemma for cvgrati 9033. Using expsub 8341, restate cvgratlem1ALT 9025 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	nnsubi 7575	. . . . 5 |- (B < C <-> (C - B) e. NN)
4		opreq2 5026	. . . . . . . . . 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 4808	. . . . . . . . 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 5026	. . . . . . . . . 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 5032	. . . . . . . . 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 3552	. . . . . . . 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 380	. . . . . . 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 7552	. . . . . . . . 9 |- 1 e. NN
13	12	elimel 3251	. . . . . . . 8 |- if((C - B) e. NN, (C - B), 1) e. NN
14	10, 11, 1, 13	cvgratlem1ALT 9025	. . . . . . 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 3240	. . . . . 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	nncni 7550	. . . . . . . . 9 |- B e. CC
17	2	nncni 7550	. . . . . . . . 9 |- C e. CC
18	16, 17	pncan3i 7133	. . . . . . . 8 |- (B + (C - B)) = C
19	18	fveq2i 4807	. . . . . . 7 |- (F` (B + (C - B))) = (F` C)
20	19	breq1i 3546	. . . . . 6 |- ((F` (B + (C - B))) <_ ((A^(C - B)) x. (F` B)) <-> (F` C) <_ ((A^(C - B)) x. (F` B)))
21	15, 20	syl6ib 282	. . . . 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 237	. . . 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 490	. . 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	gt0ne0i 7239	. . . . . . 7 |- (0 < A -> A =/= 0)
25	11	recni 6920	. . . . . . . . 9 |- A e. CC
26	25, 2, 1	3pm3.2i 1326	. . . . . . . 8 |- (A e. CC /\ C e. NN /\ B e. NN)
27		simpr 538	. . . . . . . . . . . 12 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ A =/= 0) -> A =/= 0)
28	27, 25	jctil 597	. . . . . . . . . . 11 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ A =/= 0) -> (A e. CC /\ A =/= 0))
29		nnnn0 7767	. . . . . . . . . . . . 13 |- (C e. NN -> C e. NN0)
30	29	3ad2ant2 1170	. . . . . . . . . . . 12 |- ((A e. CC /\ C e. NN /\ B e. NN) -> C e. NN0)
31	30	adantr 543	. . . . . . . . . . 11 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ A =/= 0) -> C e. NN0)
32		nnnn0 7767	. . . . . . . . . . . . 13 |- (B e. NN -> B e. NN0)
33	32	3ad2ant3 1171	. . . . . . . . . . . 12 |- ((A e. CC /\ C e. NN /\ B e. NN) -> B e. NN0)
34	33	adantr 543	. . . . . . . . . . 11 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ A =/= 0) -> B e. NN0)
35	28, 31, 34	3jca 1328	. . . . . . . . . 10 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ A =/= 0) -> ((A e. CC /\ A =/= 0) /\ C e. NN0 /\ B e. NN0))
36	35	adantrr 838	. . . . . . . . 9 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> ((A e. CC /\ A =/= 0) /\ C e. NN0 /\ B e. NN0))
37		nnre 7547	. . . . . . . . . . . . . 14 |- (B e. NN -> B e. RR)
38		nnre 7547	. . . . . . . . . . . . . 14 |- (C e. NN -> C e. RR)
39		ltle 6981	. . . . . . . . . . . . . 14 |- ((B e. RR /\ C e. RR) -> (B < C -> B <_ C))
40	37, 38, 39	syl2an 699	. . . . . . . . . . . . 13 |- ((B e. NN /\ C e. NN) -> (B < C -> B <_ C))
41	40	ancoms 512	. . . . . . . . . . . 12 |- ((C e. NN /\ B e. NN) -> (B < C -> B <_ C))
42	41	imp 489	. . . . . . . . . . 11 |- (((C e. NN /\ B e. NN) /\ B < C) -> B <_ C)
43	42	3adantl1 1304	. . . . . . . . . 10 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ B < C) -> B <_ C)
44	43	adantrl 836	. . . . . . . . 9 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> B <_ C)
45		expsub 8341	. . . . . . . . 9 |- ((((A e. CC /\ A =/= 0) /\ C e. NN0 /\ B e. NN0) /\ B <_ C) -> (A^(C - B)) = ((A^C) / (A^B)))
46	36, 44, 45	syl11anc 755	. . . . . . . 8 |- (((A e. CC /\ C e. NN /\ B e. NN) /\ (A =/= 0 /\ B < C)) -> (A^(C - B)) = ((A^C) / (A^B)))
47	26, 46	mpan 773	. . . . . . 7 |- ((A =/= 0 /\ B < C) -> (A^(C - B)) = ((A^C) / (A^B)))
48	24, 47	sylan 693	. . . . . 6 |- ((0 < A /\ B < C) -> (A^(C - B)) = ((A^C) / (A^B)))
49	48	opreq1d 5032	. . . . 5 |- ((0 < A /\ B < C) -> ((A^(C - B)) x. (F` B)) = (((A^C) / (A^B)) x. (F` B)))
50		reexpcl 8323	. . . . . . . . . 10 |- ((A e. RR /\ B e. NN0) -> (A^B) e. RR)
51	32, 50	sylan2 696	. . . . . . . . 9 |- ((A e. RR /\ B e. NN) -> (A^B) e. RR)
52	11, 1, 51	mp2an 777	. . . . . . . 8 |- (A^B) e. RR
53	52	recni 6920	. . . . . . 7 |- (A^B) e. CC
54		expgt0 8331	. . . . . . . . . 10 |- ((A e. RR /\ B e. NN0 /\ 0 < A) -> 0 < (A^B))
55	32, 54	syl3an2 1411	. . . . . . . . 9 |- ((A e. RR /\ B e. NN /\ 0 < A) -> 0 < (A^B))
56	11, 1, 55	mp3an12 1484	. . . . . . . 8 |- (0 < A -> 0 < (A^B))
57	52	gt0ne0i 7239	. . . . . . . 8 |- (0 < (A^B) -> (A^B) =/= 0)
58	56, 57	syl 13	. . . . . . 7 |- (0 < A -> (A^B) =/= 0)
59	10	ffvelrni 4917	. . . . . . . . . 10 |- (B e. NN -> (F` B) e. RR)
60	1, 59	ax-mp 7	. . . . . . . . 9 |- (F` B) e. RR
61	60	recni 6920	. . . . . . . 8 |- (F` B) e. CC
62		expcl 8324	. . . . . . . . . 10 |- ((A e. CC /\ C e. NN0) -> (A^C) e. CC)
63	29, 62	sylan2 696	. . . . . . . . 9 |- ((A e. CC /\ C e. NN) -> (A^C) e. CC)
64	25, 2, 63	mp2an 777	. . . . . . . 8 |- (A^C) e. CC
65		div13 7359	. . . . . . . 8 |- (((F` B) e. CC /\ ((A^B) e. CC /\ (A^B) =/= 0) /\ (A^C) e. CC) -> (((F` B) / (A^B)) x. (A^C)) = (((A^C) / (A^B)) x. (F` B)))
66	61, 64, 65	mp3an13 1485	. . . . . . 7 |- (((A^B) e. CC /\ (A^B) =/= 0) -> (((F` B) / (A^B)) x. (A^C)) = (((A^C) / (A^B)) x. (F` B)))
67	53, 58, 66	sylancr 758	. . . . . 6 |- (0 < A -> (((F` B) / (A^B)) x. (A^C)) = (((A^C) / (A^B)) x. (F` B)))
68	67	adantr 543	. . . . 5 |- ((0 < A /\ B < C) -> (((F` B) / (A^B)) x. (A^C)) = (((A^C) / (A^B)) x. (F` B)))
69	49, 68	eqtr4d 2205	. . . 4 |- ((0 < A /\ B < C) -> ((A^(C - B)) x. (F` B)) = (((F` B) / (A^B)) x. (A^C)))
70	69	adantlr 834	. . 3 |- (((0 < A /\ A.x e. NN (B <_ x -> (F` (x + 1)) < (A x. (F` x)))) /\ B < C) -> ((A^(C - B)) x. (F` B)) = (((F` B) / (A^B)) x. (A^C)))
71	23, 70	breqtrd 3563	. 2 |- (((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)))
72	71	ex 494	1 |- ((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))))

Syntax hints:   -> wi 3   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617   =/= wne 2295  A.wral 2385  ifcif 3212   class class class wbr 3539  -->wf 4159  ` cfv 4163  (class class class)co 5020  CCcc 6827  RRcr 6828  0cc0 6829  1c1 6830   + caddc 6832   x. cmul 6834   <_ cle 6943   < clt 6947   - cmin 7091   / cdiv 7093  NNcn 7094  NN0cn0 7095  ^cexp 8311

This theorem is referenced by:  cvgratlem3ALT 9027

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-cnex 6885  ax-resscn 6886  ax-1cn 6887  ax-icn 6888  ax-addcl 6889  ax-addrcl 6890  ax-mulcl 6891  ax-mulrcl 6892  ax-mulcom 6893  ax-addass 6894  ax-mulass 6895  ax-distr 6896  ax-i2m1 6897  ax-1ne0 6898  ax-1rid 6899  ax-rnegex 6900  ax-rrecex 6901  ax-cnre 6902  ax-pre-lttri 6903  ax-pre-lttrn 6904  ax-pre-ltadd 6905  ax-pre-mulgt0 6906  ax-mulopr 6909

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-nel 2298  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-opr 5022  df-oprab 5023  df-mpt 5138  df-1st 5166  df-2nd 5167  df-iota 5259  df-rdg 5344  df-er 5519  df-en 5631  df-dom 5632  df-sdom 5633  df-undef 5769  df-riota 5773  df-pnf 6948  df-mnf 6949  df-xr 6950  df-ltxr 6951  df-le 6952  df-sub 7111  df-neg 7113  df-div 7325  df-n 7543  df-n0 7761  df-z 7798  df-seq1 8210  df-exp 8312

Copyright terms: Public domain