This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efle

Description: The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014)

Ref Expression
Assertion efle ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ e A ≤ e B

Proof

Step Hyp Ref Expression
1 eflt ⊢ B ∈ ℝ ∧ A ∈ ℝ → B < A ↔ e B < e A
2 1 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B < A ↔ e B < e A
3 2 notbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → ¬ B < A ↔ ¬ e B < e A
4 lenlt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ ¬ B < A
5 reefcl ⊢ A ∈ ℝ → e A ∈ ℝ
6 reefcl ⊢ B ∈ ℝ → e B ∈ ℝ
7 lenlt ⊢ e A ∈ ℝ ∧ e B ∈ ℝ → e A ≤ e B ↔ ¬ e B < e A
8 5 6 7 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → e A ≤ e B ↔ ¬ e B < e A
9 3 4 8 3bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ e A ≤ e B