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 ⊢ A ∈ ℝ ∧ B ∈ ℝ → e A = e B ↔ A = B

Proof

Step Hyp Ref Expression
1 efle ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ e A ≤ e B
2 efle ⊢ B ∈ ℝ ∧ A ∈ ℝ → B ≤ A ↔ e B ≤ e A
3 2 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ≤ A ↔ e B ≤ e A
4 1 3 anbi12d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ∧ B ≤ A ↔ e A ≤ e B ∧ e B ≤ e A
5 letri3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = B ↔ A ≤ B ∧ B ≤ A
6 reefcl ⊢ A ∈ ℝ → e A ∈ ℝ
7 reefcl ⊢ B ∈ ℝ → e B ∈ ℝ
8 letri3 ⊢ e A ∈ ℝ ∧ e B ∈ ℝ → e A = e B ↔ e A ≤ e B ∧ e B ≤ e A
9 6 7 8 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → e A = e B ↔ e A ≤ e B ∧ e B ≤ e A
10 4 5 9 3bitr4rd ⊢ A ∈ ℝ ∧ B ∈ ℝ → e A = e B ↔ A = B