Theorem efle

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

	Ref	Expression
Assertion	efle	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( exp ‘ 𝐴 ) ≤ ( exp ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eflt	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ ( exp ‘ 𝐵 ) < ( exp ‘ 𝐴 ) ) )
2	1	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ ( exp ‘ 𝐵 ) < ( exp ‘ 𝐴 ) ) )
3	2	notbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ¬ 𝐵 < 𝐴 ↔ ¬ ( exp ‘ 𝐵 ) < ( exp ‘ 𝐴 ) ) )
4		lenlt	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
5		reefcl	⊢ ( 𝐴 ∈ ℝ → ( exp ‘ 𝐴 ) ∈ ℝ )
6		reefcl	⊢ ( 𝐵 ∈ ℝ → ( exp ‘ 𝐵 ) ∈ ℝ )
7		lenlt	⊢ ( ( ( exp ‘ 𝐴 ) ∈ ℝ ∧ ( exp ‘ 𝐵 ) ∈ ℝ ) → ( ( exp ‘ 𝐴 ) ≤ ( exp ‘ 𝐵 ) ↔ ¬ ( exp ‘ 𝐵 ) < ( exp ‘ 𝐴 ) ) )
8	5 6 7	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( exp ‘ 𝐴 ) ≤ ( exp ‘ 𝐵 ) ↔ ¬ ( exp ‘ 𝐵 ) < ( exp ‘ 𝐴 ) ) )
9	3 4 8	3bitr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( exp ‘ 𝐴 ) ≤ ( exp ‘ 𝐵 ) ) )