Theorem ef1tllem 7323

Description: Lemma for ef1tlub 7324.

Hypotheses

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

Assertion

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

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

Proof of Theorem ef1tllem

Step	Hyp	Ref	Expression
1		0z 6093	. . 3 |- 0 e. ZZ
2		elnn0uz 6373	. . . . 5 |- (k e. NN0 <-> k e. (ZZ>` 0))
3		opreq2 3954	. . . . . . . . . 10 |- (j = k -> (M + j) = (M + k))
4	3	fveq2d 3713	. . . . . . . . 9 |- (j = k -> (!` (M + j)) = (!` (M + k)))
5	4	opreq2d 3961	. . . . . . . 8 |- (j = k -> (1 / (!` (M + j))) = (1 / (!` (M + k))))
6		ef1tllem.4	. . . . . . . 8 |- P = {<.j, y>. | (j e. NN0 /\ y = (1 / (!` (M + j))))}
7		oprex 3968	. . . . . . . 8 |- (1 / (!` (M + k))) e. V
8	5, 6, 7	fvopab4 3765	. . . . . . 7 |- (k e. NN0 -> (P` k) = (1 / (!` (M + k))))
9		rerecclt 5759	. . . . . . . 8 |- (((!` (M + k)) e. RR /\ (!` (M + k)) =/= 0) -> (1 / (!` (M + k))) e. RR)
10		ef1tllem.5	. . . . . . . . . . . 12 |- M e. NN
11	10	nnnn0 6054	. . . . . . . . . . 11 |- M e. NN0
12		nn0addclt 6067	. . . . . . . . . . 11 |- ((M e. NN0 /\ k e. NN0) -> (M + k) e. NN0)
13	11, 12	mpan 693	. . . . . . . . . 10 |- (k e. NN0 -> (M + k) e. NN0)
14		facclt 6877	. . . . . . . . . 10 |- ((M + k) e. NN0 -> (!` (M + k)) e. NN)
15	13, 14	syl 10	. . . . . . . . 9 |- (k e. NN0 -> (!` (M + k)) e. NN)
16		nnret 5877	. . . . . . . . 9 |- ((!` (M + k)) e. NN -> (!` (M + k)) e. RR)
17	15, 16	syl 10	. . . . . . . 8 |- (k e. NN0 -> (!` (M + k)) e. RR)
18		nnne0t 5897	. . . . . . . . 9 |- ((!` (M + k)) e. NN -> (!` (M + k)) =/= 0)
19	15, 18	syl 10	. . . . . . . 8 |- (k e. NN0 -> (!` (M + k)) =/= 0)
20	9, 17, 19	sylanc 471	. . . . . . 7 |- (k e. NN0 -> (1 / (!` (M + k))) e. RR)
21	8, 20	eqeltrd 1540	. . . . . 6 |- (k e. NN0 -> (P` k) e. RR)
22		opreq2 3954	. . . . . . . . 9 |- (j = k -> ((1 / (M + 1))^j) = ((1 / (M + 1))^k))
23	22	opreq2d 3961	. . . . . . . 8 |- (j = k -> ((1 / (!` M)) x. ((1 / (M + 1))^j)) = ((1 / (!` M)) x. ((1 / (M + 1))^k)))
24		ef1tllem.3	. . . . . . . 8 |- H = {<.j, y>. | (j e. NN0 /\ y = ((1 / (!` M)) x. ((1 / (M + 1))^j)))}
25		oprex 3968	. . . . . . . 8 |- ((1 / (!` M)) x. ((1 / (M + 1))^k)) e. V
26	23, 24, 25	fvopab4 3765	. . . . . . 7 |- (k e. NN0 -> (H` k) = ((1 / (!` M)) x. ((1 / (M + 1))^k)))
27		peano2nn 5883	. . . . . . . . . . . . 13 |- (M e. NN -> (M + 1) e. NN)
28	10, 27	ax-mp 7	. . . . . . . . . . . 12 |- (M + 1) e. NN
29	28	nncn 5880	. . . . . . . . . . 11 |- (M + 1) e. CC
30	28	nnne0 5899	. . . . . . . . . . 11 |- (M + 1) =/= 0
31		recexpt 6526	. . . . . . . . . . 11 |- (((M + 1) e. CC /\ k e. NN0 /\ (M + 1) =/= 0) -> ((1 / (M + 1))^k) = (1 / ((M + 1)^k)))
32	29, 30, 31	mp3an13 904	. . . . . . . . . 10 |- (k e. NN0 -> ((1 / (M + 1))^k) = (1 / ((M + 1)^k)))
33	32	opreq2d 3961	. . . . . . . . 9 |- (k e. NN0 -> ((1 / (!` M)) x. ((1 / (M + 1))^k)) = ((1 / (!` M)) x. (1 / ((M + 1)^k))))
34		divmuldivt 5736	. . . . . . . . . . 11 |- ((((1 e. CC /\ (!` M) e. CC) /\ (1 e. CC /\ ((M + 1)^k) e. CC)) /\ ((!` M) =/= 0 /\ ((M + 1)^k) =/= 0)) -> ((1 / (!` M)) x. (1 / ((M + 1)^k))) = ((1 x. 1) / ((!` M) x. ((M + 1)^k))))
35		facclt 6877	. . . . . . . . . . . . . . . . 17 |- (M e. NN0 -> (!` M) e. NN)
36	11, 35	ax-mp 7	. . . . . . . . . . . . . . . 16 |- (!` M) e. NN
37	36	nnre 5879	. . . . . . . . . . . . . . 15 |- (!` M) e. RR
38	37	a1i 8	. . . . . . . . . . . . . 14 |- (k e. NN0 -> (!` M) e. RR)
39	38	recnd 5287	. . . . . . . . . . . . 13 |- (k e. NN0 -> (!` M) e. CC)
40		ax1cn 5241	. . . . . . . . . . . . 13 |- 1 e. CC
41	39, 40	jctil 292	. . . . . . . . . . . 12 |- (k e. NN0 -> (1 e. CC /\ (!` M) e. CC))
42		nnexpclt 6508	. . . . . . . . . . . . . . . 16 |- (((M + 1) e. NN /\ k e. NN0) -> ((M + 1)^k) e. NN)
43	28, 42	mpan 693	. . . . . . . . . . . . . . 15 |- (k e. NN0 -> ((M + 1)^k) e. NN)
44		nnret 5877	. . . . . . . . . . . . . . 15 |- (((M + 1)^k) e. NN -> ((M + 1)^k) e. RR)
45	43, 44	syl 10	. . . . . . . . . . . . . 14 |- (k e. NN0 -> ((M + 1)^k) e. RR)
46	45	recnd 5287	. . . . . . . . . . . . 13 |- (k e. NN0 -> ((M + 1)^k) e. CC)
47	46, 40	jctil 292	. . . . . . . . . . . 12 |- (k e. NN0 -> (1 e. CC /\ ((M + 1)^k) e. CC))
48	41, 47	jca 288	. . . . . . . . . . 11 |- (k e. NN0 -> ((1 e. CC /\ (!` M) e. CC) /\ (1 e. CC /\ ((M + 1)^k) e. CC)))
49		nnne0t 5897	. . . . . . . . . . . . 13 |- (((M + 1)^k) e. NN -> ((M + 1)^k) =/= 0)
50	43, 49	syl 10	. . . . . . . . . . . 12 |- (k e. NN0 -> ((M + 1)^k) =/= 0)
51	36	nnne0 5899	. . . . . . . . . . . 12 |- (!` M) =/= 0
52	50, 51	jctil 292	. . . . . . . . . . 11 |- (k e. NN0 -> ((!` M) =/= 0 /\ ((M + 1)^k) =/= 0))
53	34, 48, 52	sylanc 471	. . . . . . . . . 10 |- (k e. NN0 -> ((1 / (!` M)) x. (1 / ((M + 1)^k))) = ((1 x. 1) / ((!` M) x. ((M + 1)^k))))
54	40	mulid1 5304	. . . . . . . . . . 11 |- (1 x. 1) = 1
55	54	opreq1i 3956	. . . . . . . . . 10 |- ((1 x. 1) / ((!` M) x. ((M + 1)^k))) = (1 / ((!` M) x. ((M + 1)^k)))
56	53, 55	syl6eq 1515	. . . . . . . . 9 |- (k e. NN0 -> ((1 / (!` M)) x. (1 / ((M + 1)^k))) = (1 / ((!` M) x. ((M + 1)^k))))
57	33, 56	eqtrd 1499	. . . . . . . 8 |- (k e. NN0 -> ((1 / (!` M)) x. ((1 / (M + 1))^k)) = (1 / ((!` M) x. ((M + 1)^k))))
58		rerecclt 5759	. . . . . . . . 9 |- ((((!` M) x. ((M + 1)^k)) e. RR /\ ((!` M) x. ((M + 1)^k)) =/= 0) -> (1 / ((!` M) x. ((M + 1)^k))) e. RR)
59		nnmulclt 5889	. . . . . . . . . . 11 |- (((!` M) e. NN /\ ((M + 1)^k) e. NN) -> ((!` M) x. ((M + 1)^k)) e. NN)
60	36	a1i 8	. . . . . . . . . . 11 |- (k e. NN0 -> (!` M) e. NN)
61	59, 60, 43	sylanc 471	. . . . . . . . . 10 |- (k e. NN0 -> ((!` M) x. ((M + 1)^k)) e. NN)
62		nnret 5877	. . . . . . . . . 10 |- (((!` M) x. ((M + 1)^k)) e. NN -> ((!` M) x. ((M + 1)^k)) e. RR)
63	61, 62	syl 10	. . . . . . . . 9 |- (k e. NN0 -> ((!` M) x. ((M + 1)^k)) e. RR)
64		nnne0t 5897	. . . . . . . . . 10 |- (((!` M) x. ((M + 1)^k)) e. NN -> ((!` M) x. ((M + 1)^k)) =/= 0)
65	61, 64	syl 10	. . . . . . . . 9 |- (k e. NN0 -> ((!` M) x. ((M + 1)^k)) =/= 0)
66	58, 63, 65	sylanc 471	. . . . . . . 8 |- (k e. NN0 -> (1 / ((!` M) x. ((M + 1)^k))) e. RR)
67	57, 66	eqeltrd 1540	. . . . . . 7