Theorem absef01tlub 7329

Description: An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the punctured closed unit disk. (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
absef01tlub	|- ((A e. CC /\ (abs` A) e. (0(,]1) /\ M e. NN) -> (abs` sum_k e. (ZZ>` M)(F` k)) <_ (((abs` A)^M) x. ((M + 1) / ((!` M) x. M))))

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

Proof of Theorem absef01tlub

Step	Hyp	Ref	Expression
1		opreq1 3953	. . . . . . . . . . . 12 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> (A^j) = (if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j))
2	1	opreq1d 3960	. . . . . . . . . . 11 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> ((A^j) / (!` j)) = ((if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))
3	2	eqeq2d 1478	. . . . . . . . . 10 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> (y = ((A^j) / (!` j)) <-> y = ((if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j))))
4	3	anbi2d 614	. . . . . . . . 9 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> ((j e. NN0 /\ y = ((A^j) / (!` j))) <-> (j e. NN0 /\ y = ((if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))))
5	4	opabbidv 2660	. . . . . . . 8 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))} = {<.j, y>. | (j e. NN0 /\ y = ((if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))})
6		ef1tllem.1	. . . . . . . 8 |- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}
7	5, 6	syl5eq 1511	. . . . . . 7 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> F = {<.j, y>. | (j e. NN0 /\ y = ((if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))})
8	7	fveq1d 3711	. . . . . 6 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> (F` k) = ({<.j, y>. | (j e. NN0 /\ y = ((if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))}` k))
9	8	sumeq2sdv 6931	. . . . 5 |- (A = if((A e. CC /\ (abs` 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. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))}` k))
10	9	fveq2d 3713	. . . 4 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> (abs` sum_k e. (ZZ>` M)(F` k)) = (abs` sum_k e. (ZZ>` M)({<.j, y>. | (j e. NN0 /\ y = ((if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))}` k)))
11		fveq2 3709	. . . . . 6 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> (abs` A) = (abs` if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)))
12	11	opreq1d 3960	. . . . 5 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> ((abs` A)^M) = ((abs` if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1))^M))
13	12	opreq1d 3960	. . . 4 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> (((abs` A)^M) x. ((M + 1) / ((!` M) x. M))) = (((abs` if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1))^M) x. ((M + 1) / ((!` M) x. M))))
14	10, 13	breq12d 2621	. . 3 |- (A = if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1) -> ((abs` sum_k e. (ZZ>` M)(F` k)) <_ (((abs` A)^M) x. ((M + 1) / ((!` M) x. M))) <-> (abs` sum_k e. (ZZ>` M)({<.j, y>. | (j e. NN0 /\ y = ((if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))}` k)) <_ (((abs` if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1))^M) x. ((M + 1) / ((!` M) x. M)))))
15		fveq2 3709	. . . . . 6 |- (M = if(M e. NN, M, 1) -> (ZZ>` M) = (ZZ>` if(M e. NN, M, 1)))
16	15	sumeq1d 6928	. . . . 5 |- (M = if(M e. NN, M, 1) -> sum_k e. (ZZ>` M)({<.j, y>. | (j e. NN0 /\ y = ((if((A e. CC /\ (abs` 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. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))}` k))
17	16	fveq2d 3713	. . . 4 |- (M = if(M e. NN, M, 1) -> (abs` sum_k e. (ZZ>` M)({<.j, y>. | (j e. NN0 /\ y = ((if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))}` k)) = (abs` sum_k e. (ZZ>` if(M e. NN, M, 1))({<.j, y>. | (j e. NN0 /\ y = ((if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1)^j) / (!` j)))}` k)))
18		opreq2 3954	. . . . 5 |- (M = if(M e. NN, M, 1) -> ((abs` if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1))^M) = ((abs` if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1))^if(M e. NN, M, 1)))
19		opreq1 3953	. . . . . 6 |- (M = if(M e. NN, M, 1) -> (M + 1) = (if(M e. NN, M, 1) + 1))
20		fveq2 3709	. . . . . . 7 |- (M = if(M e. NN, M, 1) -> (!` M) = (!` if(M e. NN, M, 1)))
21		id 59	. . . . . . 7 |- (M = if(M e. NN, M, 1) -> M = if(M e. NN, M, 1))
22	20, 21	opreq12d 3963	. . . . . 6 |- (M = if(M e. NN, M, 1) -> ((!` M) x. M) = ((!` if(M e. NN, M, 1)) x. if(M e. NN, M, 1)))
23	19, 22	opreq12d 3963	. . . . 5 |- (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))))
24	18, 23	opreq12d 3963	. . . 4 |- (M = if(M e. NN, M, 1) -> (((abs` if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1))^M) x. ((M + 1) / ((!` M) x. M))) = (((abs` if((A e. CC /\ (abs` A) e. (0(,]1)), A, 1))^if(M e. NN, M, 1)