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 3729	. . . . . . . . 9 |- (P = Re -> (P` sum_k e. (ZZ>` M)(F` k)) = (Re` sum_k e. (ZZ>` M)(F` k)))
3	2	adantr 391	. . . . . . . 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 5452	. . . . . . . . . . . . . . . 16 |- 0 e. RR
7		1re 5447	. . . . . . . . . . . . . . . 16 |- 1 e. RR
8		elioc2t 6391	. . . . . . . . . . . . . . . 16 |- ((0 e. RR /\ 1 e. RR) -> (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1)))
9	6, 7, 8	mp2an 699	. . . . . . . . . . . . . . 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 796	. . . . . . . . . . . . 13 |- (A e. (0(,]1) -> A e. RR)
12	11	recnd 5327	. . . . . . . . . . . 12 |- (A e. (0(,]1) -> A e. CC)
13		axicn 5282	. . . . . . . . . . . . 13 |- i e. CC
14		axmulcl 5285	. . . . . . . . . . . . 13 |- ((i e. CC /\ A e. CC) -> (i x. A) e. CC)
15	13, 14	mpan 697	. . . . . . . . . . . 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 450	. . . . . . . . . 10 |- ((A e. (0(,]1) /\ M e. NN) -> sum_k e. (ZZ>` M)(F` k) e. CC)
18		reclt 6758	. . . . . . . . . 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 390	. . . . . . . 8 |- ((P = Re /\ (A e. (0(,]1) /\ M e. NN)) -> (Re` sum_k e. (ZZ>` M)(F` k)) e. RR)
21	3, 20	eqeltrd 1551	. . . . . . 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 3729	. . . . . . . . 9 |- (P = Im -> (P` sum_k e. (ZZ>` M)(F` k)) = (Im` sum_k e. (ZZ>` M)(F` k)))
24	23	adantr 391	. . . . . . . 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 6759	. . . . . . . . . 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 390	. . . . . . . 8 |- ((P = Im /\ (A e. (0(,]1) /\ M e. NN)) -> (Im` sum_k e. (ZZ>` M)(F` k)) e. RR)
28	24, 27	eqeltrd 1551	. . . . . . 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 5327	. . 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 5286	. . 3 |- (((A^M) e. RR /\ ((M + 1) / ((!` M) x. M)) e. RR) -> ((A^M) x. ((M + 1) / ((!` M) x. M))) e. RR)
38		reexpclt 6581	. . . 4 |- ((A e. RR /\ M e. NN0) -> (A^M) e. RR)
39		nnnn0t 6108	. . . 4 |- (M e. NN -> M e. NN0)
40	38, 11, 39	syl2an 456	. . 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 390	. . 3 |- ((A e. (0(,]1) /\ M e. NN) -> ((M + 1) / ((!` M) x. M)) e. RR)
43	37, 40, 42	sylanc 473	. 2 |- ((A e. (0(,]1) /\ M e. NN) -> ((A^M) x. ((M + 1) / ((!` M) x. M))) e. RR)
44	2	fveq2d 3734	. . . . . 6 |- (P = Re -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) = (abs` (Re` sum_k e. (ZZ>` M)(F` k))))
45	44	breq1d 2634	. . . . 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 3734	. . . . . 6 |- (P = Im -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) = (abs` (Im` sum_k e. (ZZ>` M)(F` k))))
50	49	breq1d 2634	. . . . 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. (