# Metamath Proof Explorer

## Theorem reglogleb

Description: General logarithm preserves <_ . (Contributed by Stefan O'Rear, 19-Oct-2014) (New usage is discouraged.) Use logbleb instead.

Ref Expression
Assertion reglogleb ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({C}\in {ℝ}^{+}\wedge 1<{C}\right)\right)\to \left({A}\le {B}↔\frac{\mathrm{log}{A}}{\mathrm{log}{C}}\le \frac{\mathrm{log}{B}}{\mathrm{log}{C}}\right)$

### Proof

Step Hyp Ref Expression
1 logleb ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left({A}\le {B}↔\mathrm{log}{A}\le \mathrm{log}{B}\right)$
2 1 adantr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({C}\in {ℝ}^{+}\wedge 1<{C}\right)\right)\to \left({A}\le {B}↔\mathrm{log}{A}\le \mathrm{log}{B}\right)$
3 relogcl ${⊢}{A}\in {ℝ}^{+}\to \mathrm{log}{A}\in ℝ$
4 3 ad2antrr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({C}\in {ℝ}^{+}\wedge 1<{C}\right)\right)\to \mathrm{log}{A}\in ℝ$
5 relogcl ${⊢}{B}\in {ℝ}^{+}\to \mathrm{log}{B}\in ℝ$
6 5 ad2antlr ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({C}\in {ℝ}^{+}\wedge 1<{C}\right)\right)\to \mathrm{log}{B}\in ℝ$
7 relogcl ${⊢}{C}\in {ℝ}^{+}\to \mathrm{log}{C}\in ℝ$
8 7 ad2antrl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({C}\in {ℝ}^{+}\wedge 1<{C}\right)\right)\to \mathrm{log}{C}\in ℝ$
9 log1 ${⊢}\mathrm{log}1=0$
10 1rp ${⊢}1\in {ℝ}^{+}$
11 logltb ${⊢}\left(1\in {ℝ}^{+}\wedge {C}\in {ℝ}^{+}\right)\to \left(1<{C}↔\mathrm{log}1<\mathrm{log}{C}\right)$
12 10 11 mpan ${⊢}{C}\in {ℝ}^{+}\to \left(1<{C}↔\mathrm{log}1<\mathrm{log}{C}\right)$
13 12 biimpa ${⊢}\left({C}\in {ℝ}^{+}\wedge 1<{C}\right)\to \mathrm{log}1<\mathrm{log}{C}$
14 9 13 eqbrtrrid ${⊢}\left({C}\in {ℝ}^{+}\wedge 1<{C}\right)\to 0<\mathrm{log}{C}$
15 14 adantl ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({C}\in {ℝ}^{+}\wedge 1<{C}\right)\right)\to 0<\mathrm{log}{C}$
16 lediv1 ${⊢}\left(\mathrm{log}{A}\in ℝ\wedge \mathrm{log}{B}\in ℝ\wedge \left(\mathrm{log}{C}\in ℝ\wedge 0<\mathrm{log}{C}\right)\right)\to \left(\mathrm{log}{A}\le \mathrm{log}{B}↔\frac{\mathrm{log}{A}}{\mathrm{log}{C}}\le \frac{\mathrm{log}{B}}{\mathrm{log}{C}}\right)$
17 4 6 8 15 16 syl112anc ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({C}\in {ℝ}^{+}\wedge 1<{C}\right)\right)\to \left(\mathrm{log}{A}\le \mathrm{log}{B}↔\frac{\mathrm{log}{A}}{\mathrm{log}{C}}\le \frac{\mathrm{log}{B}}{\mathrm{log}{C}}\right)$
18 2 17 bitrd ${⊢}\left(\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\wedge \left({C}\in {ℝ}^{+}\wedge 1<{C}\right)\right)\to \left({A}\le {B}↔\frac{\mathrm{log}{A}}{\mathrm{log}{C}}\le \frac{\mathrm{log}{B}}{\mathrm{log}{C}}\right)$