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 < 𝐴 ) )