Metamath Proof Explorer

Theorem effsumlt

Description: The partial sums of the series expansion of the exponential function at a positive real number are bounded by the value of the function. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses effsumlt.1 
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
effsumlt.2 
|- ( ph -> A e. RR+ )
effsumlt.3 
|- ( ph -> N e. NN0 )
Assertion effsumlt 
|- ( ph -> ( seq 0 ( + , F ) ` N ) < ( exp ` A ) )

Proof

Step Hyp Ref Expression
1 effsumlt.1 
 |-  F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2 effsumlt.2 
 |-  ( ph -> A e. RR+ )
3 effsumlt.3 
 |-  ( ph -> N e. NN0 )
4 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
5 0zd 
 |-  ( ph -> 0 e. ZZ )
6 1 eftval 
 |-  ( k e. NN0 -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
7 6 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
8 2 rpred 
 |-  ( ph -> A e. RR )
9 reeftcl 
 |-  ( ( A e. RR /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. RR )
10 8 9 sylan 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. RR )
11 7 10 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. RR )
12 4 5 11 serfre 
 |-  ( ph -> seq 0 ( + , F ) : NN0 --> RR )
13 12 3 ffvelrnd 
 |-  ( ph -> ( seq 0 ( + , F ) ` N ) e. RR )
14 eqid 
 |-  ( ZZ>= ` ( N + 1 ) ) = ( ZZ>= ` ( N + 1 ) )
15 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
16 3 15 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
17 eqidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) = ( F ` k ) )
18 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
19 rpexpcl 
 |-  ( ( A e. RR+ /\ k e. ZZ ) -> ( A ^ k ) e. RR+ )
20 2 18 19 syl2an 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ^ k ) e. RR+ )
21 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
22 21 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. NN )
23 22 nnrpd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ! ` k ) e. RR+ )
24 20 23 rpdivcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. RR+ )
25 7 24 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. RR+ )
26 8 recnd 
 |-  ( ph -> A e. CC )
27 1 efcllem 
 |-  ( A e. CC -> seq 0 ( + , F ) e. dom ~~> )
28 26 27 syl 
 |-  ( ph -> seq 0 ( + , F ) e. dom ~~> )
29 4 14 16 17 25 28 isumrpcl 
 |-  ( ph -> sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( F ` k ) e. RR+ )
30 13 29 ltaddrpd 
 |-  ( ph -> ( seq 0 ( + , F ) ` N ) < ( ( seq 0 ( + , F ) ` N ) + sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( F ` k ) ) )
31 1 efval2 
 |-  ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( F ` k ) )
32 26 31 syl 
 |-  ( ph -> ( exp ` A ) = sum_ k e. NN0 ( F ` k ) )
33 11 recnd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. CC )
34 4 14 16 17 33 28 isumsplit 
 |-  ( ph -> sum_ k e. NN0 ( F ` k ) = ( sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( F ` k ) ) )
35 3 nn0cnd 
 |-  ( ph -> N e. CC )
36 ax-1cn 
 |-  1 e. CC
37 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
38 35 36 37 sylancl 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
39 38 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N + 1 ) - 1 ) ) = ( 0 ... N ) )
40 39 sumeq1d 
 |-  ( ph -> sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( F ` k ) = sum_ k e. ( 0 ... N ) ( F ` k ) )
41 eqidd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( F ` k ) = ( F ` k ) )
42 3 4 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
43 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
44 43 33 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( F ` k ) e. CC )
45 41 42 44 fsumser 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( F ` k ) = ( seq 0 ( + , F ) ` N ) )
46 40 45 eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( F ` k ) = ( seq 0 ( + , F ) ` N ) )
47 46 oveq1d 
 |-  ( ph -> ( sum_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( F ` k ) + sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( F ` k ) ) = ( ( seq 0 ( + , F ) ` N ) + sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( F ` k ) ) )
48 32 34 47 3eqtrd 
 |-  ( ph -> ( exp ` A ) = ( ( seq 0 ( + , F ) ` N ) + sum_ k e. ( ZZ>= ` ( N + 1 ) ) ( F ` k ) ) )
49 30 48 breqtrrd 
 |-  ( ph -> ( seq 0 ( + , F ) ` N ) < ( exp ` A ) )