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	⊢ ( 𝐴 ∈ ℝ → 0 < ( exp ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		reefcl	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ 𝐴 ) ∈ ℝ )
2		rehalfcl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℝ )
3	2	reefcld	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
4	3	sqge0d	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( ( exp ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
5	2	recnd	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℂ )
6		2z	⊢ 2 ∈ ℤ
7		efexp	⊢ ( ( ( 𝐴 / 2 ) ∈ ℂ ∧ 2 ∈ ℤ ) → ( exp ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( ( exp ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
8	5 6 7	sylancl	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( ( exp ‘ ( 𝐴 / 2 ) ) ↑ 2 ) )
9		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
10		2cn	⊢ 2 ∈ ℂ
11		2ne0	⊢ 2 ≠ 0
12		divcan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
13	10 11 12	mp3an23	⊢ ( 𝐴 ∈ ℂ → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
14	9 13	syl	⊢ ( 𝐴 ∈ ℝ → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
15	14	fveq2d	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( exp ‘ 𝐴 ) )
16	8 15	eqtr3d	⊢ ( 𝐴 ∈ ℝ → ( ( exp ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = ( exp ‘ 𝐴 ) )
17	4 16	breqtrd	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( exp ‘ 𝐴 ) )
18		efne0	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ≠ 0 )
19	9 18	syl	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ 𝐴 ) ≠ 0 )
20	1 17 19	ne0gt0d	⊢ ( 𝐴 ∈ ℝ → 0 < ( exp ‘ 𝐴 ) )