HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ef1tllem 7331
Description: Lemma for ef1tlub 7332.
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
StepHypRef Expression
1 0z 6101 . . 3 |- 0 e. ZZ
2 elnn0uz 6381 . . . . 5 |- (k e. NN0 <-> k e. (ZZ>` 0))
3 opreq2 3960 . . . . . . . . . 10 |- (j = k -> (M + j) = (M + k))
43fveq2d 3719 . . . . . . . . 9 |- (j = k -> (!` (M + j)) = (!` (M + k)))
54opreq2d 3967 . . . . . . . 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 3974 . . . . . . . 8 |- (1 / (!` (M + k))) e. V
85, 6, 7fvopab4 3771 . . . . . . 7 |- (k e. NN0 -> (P` k) = (1 / (!` (M + k))))
9 rerecclt 5767 . . . . . . . 8 |- (((!` (M + k)) e. RR /\ (!` (M + k)) =/= 0) -> (1 / (!` (M + k))) e. RR)
10 ef1tllem.5 . . . . . . . . . . . 12 |- M e. NN
1110nnnn0 6062 . . . . . . . . . . 11 |- M e. NN0
12 nn0addclt 6075 . . . . . . . . . . 11 |- ((M e. NN0 /\ k e. NN0) -> (M + k) e. NN0)
1311, 12mpan 694 . . . . . . . . . 10 |- (k e. NN0 -> (M + k) e. NN0)
14 facclt 6885 . . . . . . . . . 10 |- ((M + k) e. NN0 -> (!` (M + k)) e. NN)
1513, 14syl 10 . . . . . . . . 9 |- (k e. NN0 -> (!` (M + k)) e. NN)
16 nnret 5885 . . . . . . . . 9 |- ((!` (M + k)) e. NN -> (!` (M + k)) e. RR)
1715, 16syl 10 . . . . . . . 8 |- (k e. NN0 -> (!` (M + k)) e. RR)
18 nnne0t 5905 . . . . . . . . 9 |- ((!` (M + k)) e. NN -> (!` (M + k)) =/= 0)
1915, 18syl 10 . . . . . . . 8 |- (k e. NN0 -> (!` (M + k)) =/= 0)
209, 17, 19sylanc 471 . . . . . . 7 |- (k e. NN0 -> (1 / (!` (M + k))) e. RR)
218, 20eqeltrd 1545 . . . . . 6 |- (k e. NN0 -> (P` k) e. RR)
22 opreq2 3960 . . . . . . . . 9 |- (j = k -> ((1 / (M + 1))^j) = ((1 / (M + 1))^k))
2322opreq2d 3967 . . . . . . . 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 3974 . . . . . . . 8 |- ((1 / (!` M)) x. ((1 / (M + 1))^k)) e. V
2623, 24, 25fvopab4 3771 . . . . . . 7 |- (k e. NN0 -> (H` k) = ((1 / (!` M)) x. ((1 / (M + 1))^k)))
27 peano2nn 5891 . . . . . . . . . . . . 13 |- (M e. NN -> (M + 1) e. NN)
2810, 27ax-mp 7 . . . . . . . . . . . 12 |- (M + 1) e. NN
2928nncn 5888 . . . . . . . . . . 11 |- (M + 1) e. CC
3028nnne0 5907 . . . . . . . . . . 11 |- (M + 1) =/= 0
31 recexpt 6534 . . . . . . . . . . 11 |- (((M + 1) e. CC /\ k e. NN0 /\ (M + 1) =/= 0) -> ((1 / (M + 1))^k) = (1 / ((M + 1)^k)))
3229, 30, 31mp3an13 905 . . . . . . . . . 10 |- (k e. NN0 -> ((1 / (M + 1))^k) = (1 / ((M + 1)^k)))
3332opreq2d 3967 . . . . . . . . 9 |- (k e. NN0 -> ((1 / (!` M)) x. ((1 / (M + 1))^k)) = ((1 / (!` M)) x. (1 / ((M + 1)^k))))
34 divmuldivt 5744 . . . . . . . . . . 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 6885 . . . . . . . . . . . . . . . . 17 |- (M e. NN0 -> (!` M) e. NN)
3611, 35ax-mp 7 . . . . . . . . . . . . . . . 16 |- (!` M) e. NN
3736nnre 5887 . . . . . . . . . . . . . . 15 |- (!` M) e. RR
3837a1i 8 . . . . . . . . . . . . . 14 |- (k e. NN0 -> (!` M) e. RR)
3938recnd 5295 . . . . . . . . . . . . 13 |- (k e. NN0 -> (!` M) e. CC)
40 ax1cn 5249 . . . . . . . . . . . . 13 |- 1 e. CC
4139, 40jctil 292 . . . . . . . . . . . 12 |- (k e. NN0 -> (1 e. CC /\ (!` M) e. CC))
42 nnexpclt 6516 . . . . . . . . . . . . . . . 16 |- (((M + 1) e. NN /\ k e. NN0) -> ((M + 1)^k) e. NN)
4328, 42mpan 694 . . . . . . . . . . . . . . 15 |- (k e. NN0 -> ((M + 1)^k) e. NN)
44 nnret 5885 . . . . . . . . . . . . . . 15 |- (((M + 1)^k) e. NN -> ((M + 1)^k) e. RR)
4543, 44syl 10 . . . . . . . . . . . . . 14 |- (k e. NN0 -> ((M + 1)^k) e. RR)
4645recnd 5295 . . . . . . . . . . . . 13 |- (k e. NN0 -> ((M + 1)^k) e. CC)
4746, 40jctil 292 . . . . . . . . . . . 12 |- (k e. NN0 -> (1 e. CC /\ ((M + 1)^k) e. CC))
4841, 47jca 288 . . . . . . . . . . 11 |- (k e. NN0 -> ((1 e. CC /\ (!` M) e. CC) /\ (1 e. CC /\ ((M + 1)^k) e. CC)))
49 nnne0t 5905 . . . . . . . . . . . . 13 |- (((M + 1)^k) e. NN -> ((M + 1)^k) =/= 0)
5043, 49syl 10 . . . . . . . . . . . 12 |- (k e. NN0 -> ((M + 1)^k) =/= 0)
5136nnne0 5907 . . . . . . . . . . . 12 |- (!` M) =/= 0
5250, 51jctil 292 . . . . . . . . . . 11 |- (k e. NN0 -> ((!` M) =/= 0 /\ ((M + 1)^k) =/= 0))
5334, 48, 52sylanc 471 . . . . . . . . . 10 |- (k e. NN0 -> ((1 / (!` M)) x. (1 / ((M + 1)^k))) = ((1 x. 1) / ((!` M) x. ((M + 1)^k))))
5440mulid1 5312 . . . . . . . . . . 11 |- (1 x. 1) = 1
5554opreq1i 3962 . . . . . . . . . 10 |- ((1 x. 1) / ((!` M) x. ((M + 1)^k))) = (1 / ((!` M) x. ((M + 1)^k)))
5653, 55syl6eq 1520 . . . . . . . . 9 |- (k e. NN0 -> ((1 / (!` M)) x. (1 / ((M + 1)^k))) = (1 / ((!` M) x. ((M + 1)^k))))
5733, 56eqtrd 1504 . . . . . . . 8 |- (k e. NN0 -> ((1 / (!` M)) x. ((1 / (M + 1))^k)) = (1 / ((!` M) x. ((M + 1)^k))))
58 rerecclt 5767 . . . . . . . . 9 |- ((((!` M) x. ((M + 1)^k)) e. RR /\ ((!` M) x. ((M + 1)^k)) =/= 0) -> (1 / ((!` M) x. ((M + 1)^k))) e. RR)
59 nnmulclt 5897 . . . . . . . . . . 11 |- (((!` M) e. NN /\ ((M + 1)^k) e. NN) -> ((!` M) x. ((M + 1)^k)) e. NN)
6036a1i 8 . . . . . . . . . . 11 |- (k e. NN0 -> (!` M) e. NN)
6159, 60, 43sylanc 471 . . . . . . . . . 10 |- (k e. NN0 -> ((!` M) x. ((M + 1)^k)) e. NN)
62 nnret 5885 . . . . . . . . . 10 |- (((!` M) x. ((M + 1)^k)) e. NN -> ((!` M) x. ((M + 1)^k)) e. RR)
6361, 62syl 10 . . . . . . . . 9 |- (k e. NN0 -> ((!` M) x. ((M + 1)^k)) e. RR)
64 nnne0t 5905 . . . . . . . . . 10 |- (((!` M) x. ((M + 1)^k)) e. NN -> ((!` M) x. ((M + 1)^k)) =/= 0)
6561, 64syl 10 . . . . . . . . 9 |- (k e. NN0 -> ((!` M) x. ((M + 1)^k)) =/= 0)
6658, 63, 65sylanc 471 . . . . . . . 8 |- (k e. NN0 -> (1 / ((!` M) x. ((M + 1)^k))) e. RR)
6757, 66eqeltrd 1545 . . . . . . 7