Theorem ef01tlub 7335

Description: An upper bound on the infinite tail of the series expansion of the exponential function on the positive reals less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.)

Hypothesis

Ref	Expression
ef1tllem.1	|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}

Assertion

Ref	Expression
ef01tlub	|- ((A e. (0(,]1) /\ M e. NN) -> sum_k e. (ZZ>` M)(F` k) <_ ((A^M) x. ((M + 1) / ((!` M) x. M))))

Distinct variable groups:   A,j,k,y   j,M,k,y

Proof of Theorem ef01tlub

Step	Hyp	Ref	Expression
1		opreq1 3959	. . . . . . . . . 10 |- (A = if(A e. (0(,]1), A, 1) -> (A^j) = (if(A e. (0(,]1), A, 1)^j))
2	1	opreq1d 3966	. . . . . . . . 9 |- (A = if(A e. (0(,]1), A, 1) -> ((A^j) / (!` j)) = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))
3	2	eqeq2d 1483	. . . . . . . 8 |- (A = if(A e. (0(,]1), A, 1) -> (y = ((A^j) / (!` j)) <-> y = ((if(A e. (0(,]1), A, 1)^j) / (!` j))))
4	3	anbi2d 615	. . . . . . 7 |- (A = if(A e. (0(,]1), A, 1) -> ((j e. NN0 /\ y = ((A^j) / (!` j))) <-> (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))))
5	4	opabbidv 2665	. . . . . 6 |- (A = if(A e. (0(,]1), A, 1) -> {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} = {<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))})
6		ef1tllem.1	. . . . . 6 |- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
7	5, 6	syl5eq 1516	. . . . 5 |- (A = if(A e. (0(,]1), A, 1) -> F = {<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))})
8	7	fveq1d 3717	. . . 4 |- (A = if(A e. (0(,]1), A, 1) -> (F` k) = ({<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))}` k))
9	8	sumeq2sdv 6939	. . 3 |- (A = if(A e. (0(,]1), A, 1) -> sum_k e. (ZZ>` M)(F` k) = sum_k e. (ZZ>` M)({<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))}` k))
10		opreq1 3959	. . . 4 |- (A = if(A e. (0(,]1), A, 1) -> (A^M) = (if(A e. (0(,]1), A, 1)^M))
11	10	opreq1d 3966	. . 3 |- (A = if(A e. (0(,]1), A, 1) -> ((A^M) x. ((M + 1) / ((!` M) x. M))) = ((if(A e. (0(,]1), A, 1)^M) x. ((M + 1) / ((!` M) x. M))))
12	9, 11	breq12d 2626	. 2 |- (A = if(A e. (0(,]1), A, 1) -> (sum_k e. (ZZ>` M)(F` k) <_ ((A^M) x. ((M + 1) / ((!` M) x. M))) <-> sum_k e. (ZZ>` M)({<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))}` k) <_ ((if(A e. (0(,]1), A, 1)^M) x. ((M + 1) / ((!` M) x. M)))))
13		fveq2 3715	. . . 4 |- (M = if(M e. NN, M, 1) -> (ZZ>` M) = (ZZ>` if(M e. NN, M, 1)))
14	13	sumeq1d 6936	. . 3 |- (M = if(M e. NN, M, 1) -> sum_k e. (ZZ>` M)({<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))}` k) = sum_k e. (ZZ>` if(M e. NN, M, 1))({<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))}` k))
15		opreq2 3960	. . . 4 |- (M = if(M e. NN, M, 1) -> (if(A e. (0(,]1), A, 1)^M) = (if(A e. (0(,]1), A, 1)^if(M e. NN, M, 1)))
16		opreq1 3959	. . . . 5 |- (M = if(M e. NN, M, 1) -> (M + 1) = (if(M e. NN, M, 1) + 1))
17		fveq2 3715	. . . . . 6 |- (M = if(M e. NN, M, 1) -> (!` M) = (!` if(M e. NN, M, 1)))
18		id 59	. . . . . 6 |- (M = if(M e. NN, M, 1) -> M = if(M e. NN, M, 1))
19	17, 18	opreq12d 3969	. . . . 5 |- (M = if(M e. NN, M, 1) -> ((!` M) x. M) = ((!` if(M e. NN, M, 1)) x. if(M e. NN, M, 1)))
20	16, 19	opreq12d 3969	. . . 4 |- (M = if(M e. NN, M, 1) -> ((M + 1) / ((!` M) x. M)) = ((if(M e. NN, M, 1) + 1) / ((!` if(M e. NN, M, 1)) x. if(M e. NN, M, 1))))
21	15, 20	opreq12d 3969	. . 3 |- (M = if(M e. NN, M, 1) -> ((if(A e. (0(,]1), A, 1)^M) x. ((M + 1) / ((!` M) x. M))) = ((if(A e. (0(,]1), A, 1)^if(M e. NN, M, 1)) x. ((if(M e. NN, M, 1) + 1) / ((!` if(M e. NN, M, 1)) x. if(M e. NN, M, 1)))))
22	14, 21	breq12d 2626	. 2 |- (M = if(M e. NN, M, 1) -> (sum_k e. (ZZ>` M)({<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))}` k) <_ ((if(A e. (0(,]1), A, 1)^M) x. ((M + 1) / ((!` M) x. M))) <-> sum_k e. (ZZ>` if(M e. NN, M, 1))({<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))}` k) <_ ((if(A e. (0(,]1), A, 1)^if(M e. NN, M, 1)) x. ((if(M e. NN, M, 1) + 1) / ((!` if(M e. NN, M, 1)) x. if(M e. NN, M, 1))))))
23		eqid 1473	. . 3 |- {<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))} = {<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^j) / (!` j)))}
24		eqid 1473	. . 3 |- {<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^(j - if(M e. NN, M, 1))) / (!` j)))} = {<.j, y>. | (j e. NN0 /\ y = ((if(A e. (0(,]1), A, 1)^(j - if(M e. NN, M, 1))) / (!` j)))}
25		eqid 1473	. . 3 |- {<.j, y>. | (j e. NN0 /\ y = ((1^j) / (!` j)))} = {<.j, y>. | (j e. NN0 /\ y = ((1^j) / (!` j)))}
26		1nn 5890	. . . 4 |- 1 e. NN
27	26	elimel 2390	. . 3 |- if(M e. NN, M, 1) e. NN
28		1re 5415	. . . . 5 |- 1 e. RR
29		lt01 5661	. . . . 5 |- 0 < 1
30	28	leid 5592	. . . . 5 |- 1 <_ 1
31		0re 5420	. . . . . . 7 |- 0 e. RR
32		elioc2t 6330	. . . . . . 7 |- ((0 e. RR /\ 1 e. RR) -> (1 e. (0(,]1) <-> (1 e. RR /\ 0 < 1 /\ 1 <_ 1)))
33	31, 28, 32	mp2an 696	. . . . . 6 |- (1 e. (0(,]1) <-> (1 e. RR /\ 0 < 1 /\ 1 <_ 1))
34	33	biimpr 152	. . . . 5 |- ((1 e. RR /\ 0 < 1 /\