This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efgt0

Description: The exponential of a real number is greater than 0. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Assertion efgt0 
|- ( A e. RR -> 0 < ( exp ` A ) )

Proof

Step Hyp Ref Expression
1 reefcl 
 |-  ( A e. RR -> ( exp ` A ) e. RR )
2 rehalfcl 
 |-  ( A e. RR -> ( A / 2 ) e. RR )
3 2 reefcld 
 |-  ( A e. RR -> ( exp ` ( A / 2 ) ) e. RR )
4 3 sqge0d 
 |-  ( A e. RR -> 0 <_ ( ( exp ` ( A / 2 ) ) ^ 2 ) )
5 2 recnd 
 |-  ( A e. RR -> ( A / 2 ) e. CC )
6 2z 
 |-  2 e. ZZ
7 efexp 
 |-  ( ( ( A / 2 ) e. CC /\ 2 e. ZZ ) -> ( exp ` ( 2 x. ( A / 2 ) ) ) = ( ( exp ` ( A / 2 ) ) ^ 2 ) )
8 5 6 7 sylancl 
 |-  ( A e. RR -> ( exp ` ( 2 x. ( A / 2 ) ) ) = ( ( exp ` ( A / 2 ) ) ^ 2 ) )
9 recn 
 |-  ( A e. RR -> A e. CC )
10 2cn 
 |-  2 e. CC
11 2ne0 
 |-  2 =/= 0
12 divcan2 
 |-  ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( A / 2 ) ) = A )
13 10 11 12 mp3an23 
 |-  ( A e. CC -> ( 2 x. ( A / 2 ) ) = A )
14 9 13 syl 
 |-  ( A e. RR -> ( 2 x. ( A / 2 ) ) = A )
15 14 fveq2d 
 |-  ( A e. RR -> ( exp ` ( 2 x. ( A / 2 ) ) ) = ( exp ` A ) )
16 8 15 eqtr3d 
 |-  ( A e. RR -> ( ( exp ` ( A / 2 ) ) ^ 2 ) = ( exp ` A ) )
17 4 16 breqtrd 
 |-  ( A e. RR -> 0 <_ ( exp ` A ) )
18 efne0 
 |-  ( A e. CC -> ( exp ` A ) =/= 0 )
19 9 18 syl 
 |-  ( A e. RR -> ( exp ` A ) =/= 0 )
20 1 17 19 ne0gt0d 
 |-  ( A e. RR -> 0 < ( exp ` A ) )