Metamath Proof Explorer

Theorem eftabs

Description: The absolute value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 23-Nov-2007)

Ref Expression
Assertion eftabs 
|- ( ( A e. CC /\ K e. NN0 ) -> ( abs ` ( ( A ^ K ) / ( ! ` K ) ) ) = ( ( ( abs ` A ) ^ K ) / ( ! ` K ) ) )

Proof

Step Hyp Ref Expression
1 expcl 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( A ^ K ) e. CC )
2 faccl 
 |-  ( K e. NN0 -> ( ! ` K ) e. NN )
3 2 adantl 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( ! ` K ) e. NN )
4 3 nncnd 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( ! ` K ) e. CC )
5 facne0 
 |-  ( K e. NN0 -> ( ! ` K ) =/= 0 )
6 5 adantl 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( ! ` K ) =/= 0 )
7 1 4 6 absdivd 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( abs ` ( ( A ^ K ) / ( ! ` K ) ) ) = ( ( abs ` ( A ^ K ) ) / ( abs ` ( ! ` K ) ) ) )
8 absexp 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( abs ` ( A ^ K ) ) = ( ( abs ` A ) ^ K ) )
9 3 nnred 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( ! ` K ) e. RR )
10 3 nnnn0d 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( ! ` K ) e. NN0 )
11 10 nn0ge0d 
 |-  ( ( A e. CC /\ K e. NN0 ) -> 0 <_ ( ! ` K ) )
12 9 11 absidd 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( abs ` ( ! ` K ) ) = ( ! ` K ) )
13 8 12 oveq12d 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( ( abs ` ( A ^ K ) ) / ( abs ` ( ! ` K ) ) ) = ( ( ( abs ` A ) ^ K ) / ( ! ` K ) ) )
14 7 13 eqtrd 
 |-  ( ( A e. CC /\ K e. NN0 ) -> ( abs ` ( ( A ^ K ) / ( ! ` K ) ) ) = ( ( ( abs ` A ) ^ K ) / ( ! ` K ) ) )