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