HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem abspef01tlub 7344
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
StepHypRef Expression
1 abspef01tlub.2 . . . . 5 |- (P = Re \/ P = Im)
2 fveq1 3714 . . . . . . . . 9 |- (P = Re -> (P` sum_k e. (ZZ>` M)(F` k)) = (Re` sum_k e. (ZZ>` M)(F` k)))
32adantr 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)))}
54eftlclt 7329 . . . . . . . . . . 11 |- (((i x. A) e. CC /\ M e. NN) -> sum_k e. (ZZ>` M)(F` k) e. CC)
6 0re 5420 . . . . . . . . . . . . . . . 16 |- 0 e. RR
7 1re 5415 . . . . . . . . . . . . . . . 16 |- 1 e. RR
8 elioc2t 6330 . . . . . . . . . . . . . . . 16 |- ((0 e. RR /\ 1 e. RR) -> (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1)))
96, 7, 8mp2an 696 . . . . . . . . . . . . . . 15 |- (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1))
109biimp 151 . . . . . . . . . . . . . 14 |- (A e. (0(,]1) -> (A e. RR /\ 0 < A /\ A <_ 1))
11103simp1d 793 . . . . . . . . . . . . 13 |- (A e. (0(,]1) -> A e. RR)
1211recnd 5295 . . . . . . . . . . . 12 |- (A e. (0(,]1) -> A e. CC)
13 axicn 5250 . . . . . . . . . . . . 13 |- i e. CC
14 axmulcl 5253 . . . . . . . . . . . . 13 |- ((i e. CC /\ A e. CC) -> (i x. A) e. CC)
1513, 14mpan 694 . . . . . . . . . . . 12 |- (A e. CC -> (i x. A) e. CC)
1612, 15syl 10 . . . . . . . . . . 11 |- (A e. (0(,]1) -> (i x. A) e. CC)
175, 16sylan 448 . . . . . . . . . 10 |- ((A e. (0(,]1) /\ M e. NN) -> sum_k e. (ZZ>` M)(F` k) e. CC)
18 reclt 6696 . . . . . . . . . 10 |- (sum_k e. (ZZ>` M)(F` k) e. CC -> (Re` sum_k e. (ZZ>` M)(F` k)) e. RR)
1917, 18syl 10 . . . . . . . . 9 |- ((A e. (0(,]1) /\ M e. NN) -> (Re` sum_k e. (ZZ>` M)(F` k)) e. RR)
2019adantl 388 . . . . . . . 8 |- ((P = Re /\ (A e. (0(,]1) /\ M e. NN)) -> (Re` sum_k e. (ZZ>` M)(F` k)) e. RR)
213, 20eqeltrd 1545 . . . . . . 7 |- ((P = Re /\ (A e. (0(,]1) /\ M e. NN)) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR)
2221ex 373 . . . . . 6 |- (P = Re -> ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR))
23 fveq1 3714 . . . . . . . . 9 |- (P = Im -> (P` sum_k e. (ZZ>` M)(F` k)) = (Im` sum_k e. (ZZ>` M)(F` k)))
2423adantr 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 6697 . . . . . . . . . 10 |- (sum_k e. (ZZ>` M)(F` k) e. CC -> (Im` sum_k e. (ZZ>` M)(F` k)) e. RR)
2617, 25syl 10 . . . . . . . . 9 |- ((A e. (0(,]1) /\ M e. NN) -> (Im` sum_k e. (ZZ>` M)(F` k)) e. RR)
2726adantl 388 . . . . . . . 8 |- ((P = Im /\ (A e. (0(,]1) /\ M e. NN)) -> (Im` sum_k e. (ZZ>` M)(F` k)) e. RR)
2824, 27eqeltrd 1545 . . . . . . 7 |- ((P = Im /\ (A e. (0(,]1) /\ M e. NN)) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR)
2928ex 373 . . . . . 6 |- (P = Im -> ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR))
3022, 29jaoi 341 . . . . 5 |- ((P = Re \/ P = Im) -> ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR))
311, 30ax-mp 7 . . . 4 |- ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. RR)
3231recnd 5295 . . 3 |- ((A e. (0(,]1) /\ M e. NN) -> (P` sum_k e. (ZZ>` M)(F` k)) e. CC)
33 absclt 6776 . . 3 |- ((P` sum_k e. (ZZ>` M)(F` k)) e. CC -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) e. RR)
3432, 33syl 10 . 2 |- ((A e. (0(,]1) /\ M e. NN) -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) e. RR)
35 absclt 6776 . . 3 |- (sum_k e. (ZZ>` M)(F` k) e. CC -> (abs` sum_k e. (ZZ>` M)(F` k)) e. RR)
3617, 35syl 10 . 2 |- ((A e. (0(,]1) /\ M e. NN) -> (abs` sum_k e. (ZZ>` M)(F` k)) e. RR)
37 axmulrcl 5254 . . 3 |- (((A^M) e. RR /\ ((M + 1) / ((!` M) x. M)) e. RR) -> ((A^M) x. ((M + 1) / ((!` M) x. M))) e. RR)
38 reexpclt 6520 . . . 4 |- ((A e. RR /\ M e. NN0) -> (A^M) e. RR)
39 nnnn0t 6061 . . . 4 |- (M e. NN -> M e. NN0)
4038, 11, 39syl2an 454 . . 3 |- ((A e. (0(,]1) /\ M e. NN) -> (A^M) e. RR)
41 eftlubclt 7326 . . . 4 |- (M e. NN -> ((M + 1) / ((!` M) x. M)) e. RR)
4241adantl 388 . . 3 |- ((A e. (0(,]1) /\ M e. NN) -> ((M + 1) / ((!` M) x. M)) e. RR)
4337, 40, 42sylanc 471 . 2 |- ((A e. (0(,]1) /\ M e. NN) -> ((A^M) x. ((M + 1) / ((!` M) x. M))) e. RR)
442fveq2d 3719 . . . . . 6 |- (P = Re -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) = (abs` (Re` sum_k e. (ZZ>` M)(F` k))))
4544breq1d 2624 . . . . 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 6812 . . . . . 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)))
4717, 46syl 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)))
4845, 47syl5bir 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))))
4923fveq2d 3719 . . . . . 6 |- (P = Im -> (abs` (P` sum_k e. (ZZ>` M)(F` k))) = (abs` (Im` sum_k e. (ZZ>` M)(F` k))))
5049breq1d 2624 . . . . 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 6813 . . . . . 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)))
5217, 51syl 10 . . . . 5 |- ((A e. (0(,]1) /\ M e. NN) -> (abs` (Im` sum_k e. (ZZ>` M)(F` k))) <_ (abs` sum_k e. (ZZ>