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