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

Metamath Proof Explorer

Theorem logbgt0b

Description: The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022)

Ref Expression
Assertion logbgt0b ( ( 𝐴 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → ( 0 < ( 𝐵 logb 𝐴 ) ↔ 1 < 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rpcn ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
2 1 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → 𝐵 ∈ ℂ )
3 rpne0 ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
4 3 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → 𝐵 ≠ 0 )
5 1red ⊢ ( 𝐵 ∈ ℝ+ → 1 ∈ ℝ )
6 ltne ⊢ ( ( 1 ∈ ℝ ∧ 1 < 𝐵 ) → 𝐵 ≠ 1 )
7 5 6 sylan ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → 𝐵 ≠ 1 )
8 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
9 2 4 7 8 syl3anbrc ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
10 rpcndif0 ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ( ℂ ∖ { 0 } ) )
11 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) )
12 9 10 11 syl2anr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → ( 𝐵 logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) )
13 12 breq2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → ( 0 < ( 𝐵 logb 𝐴 ) ↔ 0 < ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) ) )
14 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
15 14 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
16 relogcl ⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
17 16 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → ( log ‘ 𝐵 ) ∈ ℝ )
18 17 adantl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → ( log ‘ 𝐵 ) ∈ ℝ )
19 loggt0b ⊢ ( 𝐵 ∈ ℝ+ → ( 0 < ( log ‘ 𝐵 ) ↔ 1 < 𝐵 ) )
20 19 biimpar ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) → 0 < ( log ‘ 𝐵 ) )
21 20 adantl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → 0 < ( log ‘ 𝐵 ) )
22 gt0div ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( log ‘ 𝐵 ) ) → ( 0 < ( log ‘ 𝐴 ) ↔ 0 < ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) ) )
23 15 18 21 22 syl3anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → ( 0 < ( log ‘ 𝐴 ) ↔ 0 < ( ( log ‘ 𝐴 ) / ( log ‘ 𝐵 ) ) ) )
24 loggt0b ⊢ ( 𝐴 ∈ ℝ+ → ( 0 < ( log ‘ 𝐴 ) ↔ 1 < 𝐴 ) )
25 24 adantr ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → ( 0 < ( log ‘ 𝐴 ) ↔ 1 < 𝐴 ) )
26 13 23 25 3bitr2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 𝐵 ∈ ℝ+ ∧ 1 < 𝐵 ) ) → ( 0 < ( 𝐵 logb 𝐴 ) ↔ 1 < 𝐴 ) )