Theorem abspef01tlub 7336

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 3708	. . . . . . . . 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 7321	. . . . . . . . . . 11 |- (((i x. A) e. CC /\ M e. NN) -> sum_k e. (ZZ>` M)(F` k) e. CC)
6		0re 5412	. . . . . . . . . . . . . . . 16 |- 0 e. RR
7		1re 5407	. . . . . . . . . . . . . . . 16 |- 1 e. RR
8		elioc2t 6322	. . . . . . . . . . . . . . . 16 |- ((0 e. RR /\ 1 e. RR) -> (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1)))
9	6, 7, 8	mp2an 695	. . . . . . . . . . . . . . 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 792	. . . . . . . . . . . . 13 |- (A e. (0(,]1) -> A e. RR)
12	11	recnd 5287	. . . . . . . . . . . 12 |- (A e. (0(,]1) -> A e. CC)
13		axicn 5242	. . . . . . . . . . . . 13 |- i e. CC
14		axmulcl 5245	. . . . . . . . . . . . 13 |- ((i e. CC /\ A e. CC) -> (i x. A) e. CC)
15	13, 14	mpan 693	. . . . . . . . . . . 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 6688	. . . . . . . . . 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 1540	. . . . . . 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 3708	. . . . . . . . 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 6689	. . . . . . . . . 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 1540	. . . . . . 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 5287	. . 3 |- ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. CC)
33		absclt 6768	. . 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 6768	. . 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 5246	. . 3 |- (((A^M) e. RR /\ ((M + 1) / ((!` M) x. M)) e. RR) -> ((A^M) x. ((M + 1) / ((!` M) x. M))) e. RR)
38		reexpclt 6512	. . . 4 |- ((A e. RR /\ M e. NN0) -> (A^M) e. RR)
39		nnnn0t 6053	. . . 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 7318	. . . 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 3713	. . . . . 6 |- (P = Re -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) = (abs` (Re` sum_k e. (ZZ>` M)(F` k))))
45	44	breq1d 2619	. . . . 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 6804	. . . . . 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 3713	. . . . . 6 |- (P = Im -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) = (abs` (Im` sum_k e. (ZZ>` M)(F` k))))
50	49	breq1d 2619	. . . . 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 6805	. . . . . 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. (ZZ>