Metamath Proof Explorer

Theorem reef11

Description: The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008) (Revised by Mario Carneiro, 11-Mar-2014)

Ref Expression
Assertion reef11 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( exp ‘ 𝐴 ) = ( exp ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 efle ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( exp ‘ 𝐴 ) ≤ ( exp ‘ 𝐵 ) ) )
2 efle ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 ≤ 𝐴 ↔ ( exp ‘ 𝐵 ) ≤ ( exp ‘ 𝐴 ) ) )
3 2 ancoms ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 ≤ 𝐴 ↔ ( exp ‘ 𝐵 ) ≤ ( exp ‘ 𝐴 ) ) )
4 1 3 anbi12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ↔ ( ( exp ‘ 𝐴 ) ≤ ( exp ‘ 𝐵 ) ∧ ( exp ‘ 𝐵 ) ≤ ( exp ‘ 𝐴 ) ) ) )
5 letri3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) )
6 reefcl ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ 𝐴 ) ∈ ℝ )
7 reefcl ⊢ ( 𝐵 ∈ ℝ → ( exp ‘ 𝐵 ) ∈ ℝ )
8 letri3 ⊢ ( ( ( exp ‘ 𝐴 ) ∈ ℝ ∧ ( exp ‘ 𝐵 ) ∈ ℝ ) → ( ( exp ‘ 𝐴 ) = ( exp ‘ 𝐵 ) ↔ ( ( exp ‘ 𝐴 ) ≤ ( exp ‘ 𝐵 ) ∧ ( exp ‘ 𝐵 ) ≤ ( exp ‘ 𝐴 ) ) ) )
9 6 7 8 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( exp ‘ 𝐴 ) = ( exp ‘ 𝐵 ) ↔ ( ( exp ‘ 𝐴 ) ≤ ( exp ‘ 𝐵 ) ∧ ( exp ‘ 𝐵 ) ≤ ( exp ‘ 𝐴 ) ) ) )
10 4 5 9 3bitr4rd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( exp ‘ 𝐴 ) = ( exp ‘ 𝐵 ) ↔ 𝐴 = 𝐵 ) )