Theorem abspef01tlub 7395

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 disc projected onto the real or imaginary axis. (Contributed by Paul Chapman, 19-Jan-2008.)

Hypotheses

Ref	Expression
abspef01tlub.1	|- F = {<.j, y>. | (j e. NN0 /\ y = (((i x. A)^j) / (!` j)))}
abspef01tlub.2	|- (P = Re \/ P = Im)

Assertion

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

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

Proof of Theorem abspef01tlub

Step	Hyp	Ref	Expression
1		abspef01tlub.2	. . . . 5 |- (P = Re \/ P = Im)
2		fveq1 3723	. . . . . . . . 9 |- (P = Re -> (P` sum_k e. (ZZ>` M)(F` k)) = (Re` sum_k e. (ZZ>` M)(F` k)))
3	2	adantr 389	. . . . . . . 8 |- ((P = Re /\ (A e. (0(,]1) /\ M e. NN)) -> (P` sum_k e. (ZZ>` M)(F` k)) = (Re` sum_k e. (ZZ>` M)(F` k)))
4		abspef01tlub.1	. . . . . . . . . . . 12 |- F = {<.j, y>. | (j e. NN0 /\ y = (((i x. A)^j) / (!` j)))}
5	4	eftlclt 7379	. . . . . . . . . . 11 |- (((i x. A) e. CC /\ M e. NN) -> sum_k e. (ZZ>` M)(F` k) e. CC)
6		0re 5440	. . . . . . . . . . . . . . . 16 |- 0 e. RR
7		1re 5435	. . . . . . . . . . . . . . . 16 |- 1 e. RR
8		elioc2t 6390	. . . . . . . . . . . . . . . 16 |- ((0 e. RR /\ 1 e. RR) -> (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1)))
9	6, 7, 8	mp2an 697	. . . . . . . . . . . . . . 15 |- (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1))
10	9	biimp 151	. . . . . . . . . . . . . 14 |- (A e. (0(,]1) -> (A e. RR /\ 0 < A /\ A <_ 1))
11	10	3simp1d 794	. . . . . . . . . . . . 13 |- (A e. (0(,]1) -> A e. RR)
12	11	recnd 5315	. . . . . . . . . . . 12 |- (A e. (0(,]1) -> A e. CC)
13		axicn 5270	. . . . . . . . . . . . 13 |- i e. CC
14		axmulcl 5273	. . . . . . . . . . . . 13 |- ((i e. CC /\ A e. CC) -> (i x. A) e. CC)
15	13, 14	mpan 695	. . . . . . . . . . . 12 |- (A e. CC -> (i x. A) e. CC)
16	12, 15	syl 10	. . . . . . . . . . 11 |- (A e. (0(,]1) -> (i x. A) e. CC)
17	5, 16	sylan 448	. . . . . . . . . 10 |- ((A e. (0(,]1) /\ M e. NN) -> sum_k e. (ZZ>` M)(F` k) e. CC)
18		reclt 6757	. . . . . . . . . 10 |- (sum_k e. (ZZ>` M)(F` k) e. CC -> (Re` sum_k e. (ZZ>` M)(F` k)) e. RR)
19	17, 18	syl 10	. . . . . . . . 9 |- ((A e. (0(,]1) /\ M e. NN) -> (Re` sum_k e. (ZZ>` M)(F` k)) e. RR)
20	19	adantl 388	. . . . . . . 8 |- ((P = Re /\ (A e. (0(,]1) /\ M e. NN)) -> (Re` sum_k e. (ZZ>` M)(F` k)) e. RR)
21	3, 20	eqeltrd 1548	. . . . . . 7 |- ((P = Re /\ (A e. (0(,]1) /\ M e. NN)) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR)
22	21	ex 373	. . . . . 6 |- (P = Re -> ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR))
23		fveq1 3723	. . . . . . . . 9 |- (P = Im -> (P` sum_k e. (ZZ>` M)(F` k)) = (Im` sum_k e. (ZZ>` M)(F` k)))
24	23	adantr 389	. . . . . . . 8 |- ((P = Im /\ (A e. (0(,]1) /\ M e. NN)) -> (P` sum_k e. (ZZ>` M)(F` k)) = (Im` sum_k e. (ZZ>` M)(F` k)))
25		imclt 6758	. . . . . . . . . 10 |- (sum_k e. (ZZ>` M)(F` k) e. CC -> (Im` sum_k e. (ZZ>` M)(F` k)) e. RR)
26	17, 25	syl 10	. . . . . . . . 9 |- ((A e. (0(,]1) /\ M e. NN) -> (Im` sum_k e. (ZZ>` M)(F` k)) e. RR)
27	26	adantl 388	. . . . . . . 8 |- ((P = Im /\ (A e. (0(,]1) /\ M e. NN)) -> (Im` sum_k e. (ZZ>` M)(F` k)) e. RR)
28	24, 27	eqeltrd 1548	. . . . . . 7 |- ((P = Im /\ (A e. (0(,]1) /\ M e. NN)) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR)
29	28	ex 373	. . . . . 6 |- (P = Im -> ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR))
30	22, 29	jaoi 341	. . . . 5 |- ((P = Re \/ P = Im) -> ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR))
31	1, 30	ax-mp 7	. . . 4 |- ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR)
32	31	recnd 5315	. . 3 |- ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. CC)
33		absclt 6833	. . 3 |- ((P` sum_k e. (ZZ>` M)(F` k)) e. CC -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) e. RR)
34	32, 33	syl 10	. 2 |- ((A e. (0(,]1) /\ M e. NN) -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) e. RR)
35		absclt 6833	. . 3 |- (sum_k e. (ZZ>` M)(F` k) e. CC -> (abs` sum_k e. (ZZ>` M)(F` k)) e. RR)
36	17, 35	syl 10	. 2 |- ((A e. (0(,]1) /\ M e. NN) -> (abs` sum_k e. (ZZ>` M)(F` k)) e. RR)
37		axmulrcl 5274	. . 3 |- (((A^M) e. RR /\ ((M + 1) / ((!` M) x. M)) e. RR) -> ((A^M) x. ((M + 1) / ((!` M) x. M))) e. RR)
38		reexpclt 6580	. . . 4 |- ((A e. RR /\ M e. NN0) -> (A^M) e. RR)
39		nnnn0t 6106	. . . 4 |- (M e. NN -> M e. NN0)
40	38, 11, 39	syl2an 454	. . 3 |- ((A e. (0(,]1) /\ M e. NN) -> (A^M) e. RR)
41		eftlubclt 7376	. . . 4 |- (M e. NN -> ((M + 1) / ((!` M) x. M)) e. RR)
42	41	adantl 388	. . 3 |- ((A e. (0(,]1) /\ M e. NN) -> ((M + 1) / ((!` M) x. M)) e. RR)
43	37, 40, 42	sylanc 471	. 2 |- ((A e. (0(,]1) /\ M e. NN) -> ((A^M) x. ((M + 1) / ((!` M) x. M))) e. RR)
44	2	fveq2d 3728	. . . . . 6 |- (P = Re -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) = (abs` (Re` sum_k e. (ZZ>` M)(F` k))))
45	44	breq1d 2629	. . . . 5 |- (P = Re -> ((abs` (P` sum_k e. (ZZ>` M)(F` k))) <_ (abs` sum_k e. (ZZ>` M)(F` k)) <-> (abs` (Re` sum_k e. (ZZ>` M)(F` k))) <_ (abs` sum_k e. (ZZ>` M)(F` k))))
46		absrelet 6869	. . . . . 6 |- (sum_k e. (ZZ>` M)(F` k) e. CC -> (abs` (Re` sum_k e. (ZZ>` M)(F` k))) <_ (abs` sum_k e. (ZZ>` M)(F` k)))
47	17, 46	syl 10	. . . . 5 |- ((A e. (0(,]1) /\ M e. NN) -> (abs` (Re` sum_k e. (ZZ>` M)(F` k))) <_ (abs` sum_k e. (ZZ>` M)(F` k)))
48	45, 47	syl5bir 210	. . . 4 |- (P = Re -> ((A e. (0(,]1) /\ M e. NN) -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) <_ (abs` sum_k e. (ZZ>` M)(F` k))))
49	23	fveq2d 3728	. . . . . 6 |- (P = Im -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) = (abs` (Im` sum_k e. (ZZ>` M)(F` k))))
50	49	breq1d 2629	. . . . 5 |- (P = Im -> ((abs` (P` sum_k e. (ZZ>` M)(F` k))) <_ (abs` sum_k e. (ZZ>` M)(F` k)) <-> (abs` (Im` sum_k e. (ZZ>` M)(F` k))) <_ (abs` sum_k e. (ZZ>` M)(F` k))))
51		absimlet 6870	. . . . . 6 |- (sum_k e. (ZZ>` M)(F` k) e. CC -> (abs` (Im` sum_k e. (ZZ>` M)(F` k))) <_ (abs` sum_k e. (ZZ>` M)(F` k)))
52	17, 51	syl 10	. . . . 5 |- ((A e. (0(,]1) /\ M e. NN) -> (abs` (Im` sum_k e. (ZZ>` M)(F` k))) <_ (abs` sum_k e. (