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 ) )