Metamath Proof Explorer

Theorem logleb

Description: Natural logarithm preserves <_ . (Contributed by Stefan O'Rear, 19-Sep-2014)

Ref Expression
Assertion logleb ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 logltb ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( 𝐵 < 𝐴 ↔ ( log ‘ 𝐵 ) < ( log ‘ 𝐴 ) ) )
2 1 ancoms ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 < 𝐴 ↔ ( log ‘ 𝐵 ) < ( log ‘ 𝐴 ) ) )
3 2 notbid ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ¬ 𝐵 < 𝐴 ↔ ¬ ( log ‘ 𝐵 ) < ( log ‘ 𝐴 ) ) )
4 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
5 rpre ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
6 lenlt ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
7 4 5 6 syl2an ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
8 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
9 relogcl ⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
10 lenlt ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ↔ ¬ ( log ‘ 𝐵 ) < ( log ‘ 𝐴 ) ) )
11 8 9 10 syl2an ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ↔ ¬ ( log ‘ 𝐵 ) < ( log ‘ 𝐴 ) ) )
12 3 7 11 3bitr4d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ) )