Theorem ef01tllem2 7384

Description: Lemma for ef01tlub 7386.

Hypotheses

Ref	Expression
ef1tllem.1	|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
ef01tllem2.2	|- G = {<.j, y>. | (j e. NN0 /\ y = ((A^(j - M)) / (!` j)))}
ef01tllem2.3	|- H = {<.j, y>. | (j e. NN0 /\ y = ((1^j) / (!` j)))}
ef01tllem2.4	|- M e. NN
ef01tllem2.5	|- A e. (0(,]1)

Assertion

Ref	Expression
ef01tllem2	|- sum_k e. (ZZ>` M)(F` k) <_ ((A^M) x. ((M + 1) / ((!` M) x. M)))

Distinct variable groups:   A,j,k,y   k,F   k,G   k,H   j,M,k,y

Proof of Theorem ef01tllem2

Step	Hyp	Ref	Expression
1		ef1tllem.1	. . . . . 6 |- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
2		ef01tllem2.2	. . . . . 6 |- G = {<.j, y>. | (j e. NN0 /\ y = ((A^(j - M)) / (!` j)))}
3		ef01tllem2.4	. . . . . 6 |- M e. NN
4		ef01tllem2.5	. . . . . . . 8 |- A e. (0(,]1)
5		0re 5440	. . . . . . . . 9 |- 0 e. RR
6		1re 5435	. . . . . . . . 9 |- 1 e. RR
7		elioc2t 6390	. . . . . . . . 9 |- ((0 e. RR /\ 1 e. RR) -> (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1)))
8	5, 6, 7	mp2an 697	. . . . . . . 8 |- (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1))
9	4, 8	mpbi 189	. . . . . . 7 |- (A e. RR /\ 0 < A /\ A <_ 1)
10	9	3simp1i 791	. . . . . 6 |- A e. RR
11	9	3simp2i 792	. . . . . . 7 |- 0 < A
12	10, 11	gt0ne0i 5617	. . . . . 6 |- A =/= 0
13	1, 2, 3, 10, 12	ef01tllem1 7383	. . . . 5 |- (<.M, + >. seq G) ~~> (sum_k e. (ZZ>` M)(F` k) / (A^M))
14		nnzt 6153	. . . . . . 7 |- (M e. NN -> M e. ZZ)
15	3, 14	ax-mp 7	. . . . . 6 |- M e. ZZ
16		ax1cn 5269	. . . . . . 7 |- 1 e. CC
17		ef01tllem2.3	. . . . . . . 8 |- H = {<.j, y>. | (j e. NN0 /\ y = ((1^j) / (!` j)))}
18	17	eftlext 7378	. . . . . . 7 |- ((1 e. CC /\ M e. NN) -> E.x(<.M, + >. seq H) ~~> x)
19	16, 3, 18	mp2an 697	. . . . . 6 |- E.x(<.M, + >. seq H) ~~> x
20		nn0ex 6105	. . . . . . . 8 |- NN0 e. V
21	20, 17	fopabex2 3612	. . . . . . 7 |- H e. V
22	21	isumclim2t 7199	. . . . . 6 |- ((M e. ZZ /\ E.x(<.M, + >. seq H) ~~> x) -> (<.M, + >. seq H) ~~> sum_k e. (ZZ>` M)(H` k))
23	15, 19, 22	mp2an 697	. . . . 5 |- (<.M, + >. seq H) ~~> sum_k e. (ZZ>` M)(H` k)
24	13, 23	pm3.2i 285	. . . 4 |- ((<.M, + >. seq G) ~~> (sum_k e. (ZZ>` M)(F` k) / (A^M)) /\ (<.M, + >. seq H) ~~> sum_k e. (ZZ>` M)(H` k))
25	3	nnnn0 6107	. . . . . . . . . . . 12 |- M e. NN0
26		elnn0uz 6441	. . . . . . . . . . . 12 |- (M e. NN0 <-> M e. (ZZ>` 0))
27	25, 26	mpbi 189	. . . . . . . . . . 11 |- M e. (ZZ>` 0)
28		uztrn 6428	. . . . . . . . . . 11 |- ((k e. (ZZ>` M) /\ M e. (ZZ>` 0)) -> k e. (ZZ>` 0))
29	27, 28	mpan2 696	. . . . . . . . . 10 |- (k e. (ZZ>` M) -> k e. (ZZ>` 0))
30		elnn0uz 6441	. . . . . . . . . 10 |- (k e. NN0 <-> k e. (ZZ>` 0))
31	29, 30	sylibr 200	. . . . . . . . 9 |- (k e. (ZZ>` M) -> k e. NN0)
32		opreq1 3968	. . . . . . . . . . . 12 |- (j = k -> (j - M) = (k - M))
33	32	opreq2d 3976	. . . . . . . . . . 11 |- (j = k -> (A^(j - M)) = (A^(k - M)))
34		fveq2 3724	. . . . . . . . . . 11 |- (j = k -> (!` j) = (!` k))
35	33, 34	opreq12d 3978	. . . . . . . . . 10 |- (j = k -> ((A^(j - M)) / (!` j)) = ((A^(k - M)) / (!` k)))
36		oprex 3983	. . . . . . . . . 10 |- ((A^(k - M)) / (!` k)) e. V
37	35, 2, 36	fvopab4 3780	. . . . . . . . 9 |- (k e. NN0 -> (G` k) = ((A^(k - M)) / (!` k)))
38	31, 37	syl 10	. . . . . . . 8 |- (k e. (ZZ>` M) -> (G` k) = ((A^(k - M)) / (!` k)))
39		redivclt 5800	. . . . . . . . 9 |- (((A^(k - M)) e. RR /\ (!` k) e. RR /\ (!` k) =/= 0) -> ((A^(k - M)) / (!` k)) e. RR)
40		nn0sub2t 6162	. . . . . . . . . . . 12 |- ((M e. NN0 /\ k e. NN0 /\ M <_ k) -> (k - M) e. NN0)
41	25, 40	mp3an1 903	. . . . . . . . . . 11 |- ((k e. NN0 /\ M <_ k) -> (k - M) e. NN0)
42		eluzle 6425	. . . . . . . . . . 11 |- (k e. (ZZ>` M) -> M <_ k)
43	41, 31, 42	sylanc 471	. . . . . . . . . 10 |- (k e. (ZZ>` M) -> (k - M) e. NN0)
44		reexpclt 6580	. . . . . . . . . . 11 |- ((A e. RR /\ (k - M) e. NN0) -> (A^(k - M)) e. RR)
45	10, 44	mpan 695	. . . . . . . . . 10 |- ((k - M) e. NN0 -> (A^(k - M)) e. RR)
46	43, 45	syl 10	. . . . . . . . 9 |- (k e. (ZZ>` M) -> (A^(k - M)) e. RR)
47		facclt 6940	. . . . . . . . . . 11 |- (k e. NN0 -> (!` k) e. NN)
48		nnret 5929	. . . . . . . . . . 11 |- ((!` k) e. NN -> (!` k) e. RR)
49	47, 48	syl 10	. . . . . . . . . 10 |- (k e. NN0 -> (!` k) e. RR)
50	31, 49	syl 10	. . . . . . . . 9 |- (k e. (ZZ>` M) -> (!` k) e. RR)
51		nnne0t 5949	. . . . . . . . . . 11 |- ((!` k) e. NN -> (!` k) =/= 0)
52	47, 51	syl 10	. . . . . . . . . 10 |- (k e. NN0 -> (!` k) =/= 0)
53	31, 52	syl 10	. . . . . . . . 9 |- (k e. (ZZ>` M) -> (!` k) =/= 0)
54	39, 46, 50, 53	syl3anc 858	. . . . . . . 8 |- (k e. (ZZ>` M) -> ((A^(k - M)) / (!` k)) e. RR)
55	38, 54	eqeltrd 1548	. . . . . . 7 |- (k e. (ZZ>` M) -> (G` k) e. RR)
56	17	eftval 7316	. . . . . . . . . 10 |- (k e. NN0 -> (H` k) = ((1^k) / (!` k)))
57		1expt 6584	. . . . . . . . . . 11 |- (k e. NN0 -> (1^k) = 1)
58	57	opreq1d 3975	. . . . . . . . . 10 |- (k e. NN0 -> ((1^k) / (!` k)) = (1 / (!` k)))
59	56, 58	eqtrd 1507	. . . . . . . . 9 |- (k e. NN0 -> (H` k) = (1 / (!` k)))
60	31, 59	syl 10	. . . . . . . 8 |- (k e. (ZZ>` M) -> (H` k) = (1 / (!` k)))
61		rerecclt 5803	. . . . . . . . 9 |- (((!` k) e. RR /\ (!` k) =/= 0) -> (1 / (!` k)) e. RR)
62	61, 50, 53	sylanc 471	. . . . . . . 8 |- (k e. (ZZ>` M) -> (1 / (!` k)) e. RR)
63	60, 62	eqeltrd 1548	. . . . . . 7 |- (k e. (ZZ>` M) -> (H` k) e. RR)
64	5, 10, 11	ltlei 5581	. . . . . . . . . . . 12 |- 0 <_ A
65	9	3simp3i 793	. . . . . . . . . . . 12 |- A <_ 1
66	10, 64, 65	3pm3.2i 818	. . . . . . . . . . 11 |- (A e. RR /\ 0 <_ A /\ A <_ 1)
67		exple1t 6607	. . . . . . . . . . 11 |- (((A e. RR /\ 0 <_ A /\ A <_ 1) /\ (k - M) e. NN0) -> (A^(k - M)) <_ 1)
68	66, 67	mpan 695	. . . . . . . . . 10 |- ((k - M) e. NN0 -> (A^(k - M)) <_ 1)
69	43, 68	syl 10	. . . . . . . . 9 |- (k e. (ZZ>` M) -> (A^(k - M)) <_ 1)
70		lediv1tOLD 5852	. . . . . . . . . 10 |- ((((A^(k - M)) e. RR /\ 1 e. RR /\ (!` k) e. RR) /\ 0 < (!` k)) -> ((A^(k - M)) <_ 1 <-> ((A^(k - M)) / (!` k)) <_ (1 / (!` k))))
71	6	a1i 8	. . . . . . . . . . 11 |- (k e. (ZZ>` M) -> 1 e. RR)
72	46, 71, 50	3jca 819	. . . . . . . . . 10 |- (k e. (ZZ>` M) -> ((A^(k - M)) e. RR /\ 1 e. RR /\ (!` k) e. RR))
73		nngt0t 5946	. . . . . . . . . . 11 |- ((!` k) e. NN -> 0 < (!` k))
74	31, 47, 73	3syl 20	. . . . . . . . . 10 |- (k e. (ZZ>` M) -> 0 < (!` k))
75	70, 72, 74	sylanc 471	. . . . . . . . 9 |- (k e. (ZZ>` M) -> ((A^(k - M)) <_ 1 <-> ((A^(k - M)) / (!` k)) <_ (1 / (!` k))))
76	69, 75	mpbid 195	. . . . . . . 8 |- (k e. (ZZ>` M) -> ((A^(k - M)) / (!` k)) <_ (1 / (!` k)))
77	76, 38, 60	3brtr4d 2645	. . . . . . 7 |- (k e. (ZZ>` M) -> (G` k) <_ (H` k))
78	55, 63, 77	3jca 819	. . . . . 6 |- (k e. (ZZ>` M) -> ((G` k) e. RR /\ (H` k) e. RR /\ (G` k) <_ (H` k)))
79	78	rgen 1698	. . . . 5 |- A.k e. (ZZ>` M)((G` k) e. RR /\ (H` k) e. RR /\ (G` k) <_ (H` k))
80	15, 79	pm3.2i 285	. . . 4 |- (M e. ZZ /\ A.k e. (ZZ>` M)((G` k) e.