Theorem logbge0b

Description: The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	logbge0b	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 0 ≤ ( 𝐵 logb 𝑋 ) ↔ 1 ≤ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		relogbval	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
2	1	breq2d	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 0 ≤ ( 𝐵 logb 𝑋 ) ↔ 0 ≤ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ) )
3		relogcl	⊢ ( 𝑋 ∈ ℝ+ → ( log ‘ 𝑋 ) ∈ ℝ )
4	3	adantl	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( log ‘ 𝑋 ) ∈ ℝ )
5		eluz2nn	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℕ )
6	5	nnrpd	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℝ+ )
7		relogcl	⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
8	6 7	syl	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( log ‘ 𝐵 ) ∈ ℝ )
9	8	adantr	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( log ‘ 𝐵 ) ∈ ℝ )
10		eluz2gt1	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐵 )
11		loggt0b	⊢ ( 𝐵 ∈ ℝ+ → ( 0 < ( log ‘ 𝐵 ) ↔ 1 < 𝐵 ) )
12	6 11	syl	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( log ‘ 𝐵 ) ↔ 1 < 𝐵 ) )
13	10 12	mpbird	⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 0 < ( log ‘ 𝐵 ) )
14	13	adantr	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → 0 < ( log ‘ 𝐵 ) )
15		ge0div	⊢ ( ( ( log ‘ 𝑋 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( log ‘ 𝐵 ) ) → ( 0 ≤ ( log ‘ 𝑋 ) ↔ 0 ≤ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ) )
16	4 9 14 15	syl3anc	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 0 ≤ ( log ‘ 𝑋 ) ↔ 0 ≤ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ) )
17		logge0b	⊢ ( 𝑋 ∈ ℝ+ → ( 0 ≤ ( log ‘ 𝑋 ) ↔ 1 ≤ 𝑋 ) )
18	17	adantl	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 0 ≤ ( log ‘ 𝑋 ) ↔ 1 ≤ 𝑋 ) )
19	2 16 18	3bitr2d	⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 0 ≤ ( 𝐵 logb 𝑋 ) ↔ 1 ≤ 𝑋 ) )