Theorem logbprmirr

Description: The logarithm of a prime to a different prime base is an irrational number. For example, ( 2 logb 3 ) e. ( RR \ QQ ) (see 2logb3irr ). (Contributed by AV, 31-Dec-2022)

	Ref	Expression
Assertion	logbprmirr	⊢ ( ( 𝑋 ∈ ℙ ∧ 𝐵 ∈ ℙ ∧ 𝑋 ≠ 𝐵 ) → ( 𝐵 logb 𝑋 ) ∈ ( ℝ ∖ ℚ ) )

Proof

Step	Hyp	Ref	Expression
1		prmuz2	⊢ ( 𝑋 ∈ ℙ → 𝑋 ∈ ( ℤ≥ ‘ 2 ) )
2	1	3ad2ant1	⊢ ( ( 𝑋 ∈ ℙ ∧ 𝐵 ∈ ℙ ∧ 𝑋 ≠ 𝐵 ) → 𝑋 ∈ ( ℤ≥ ‘ 2 ) )
3		prmuz2	⊢ ( 𝐵 ∈ ℙ → 𝐵 ∈ ( ℤ≥ ‘ 2 ) )
4	3	3ad2ant2	⊢ ( ( 𝑋 ∈ ℙ ∧ 𝐵 ∈ ℙ ∧ 𝑋 ≠ 𝐵 ) → 𝐵 ∈ ( ℤ≥ ‘ 2 ) )
5		prmrp	⊢ ( ( 𝑋 ∈ ℙ ∧ 𝐵 ∈ ℙ ) → ( ( 𝑋 gcd 𝐵 ) = 1 ↔ 𝑋 ≠ 𝐵 ) )
6	5	biimp3ar	⊢ ( ( 𝑋 ∈ ℙ ∧ 𝐵 ∈ ℙ ∧ 𝑋 ≠ 𝐵 ) → ( 𝑋 gcd 𝐵 ) = 1 )
7		logbgcd1irr	⊢ ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑋 gcd 𝐵 ) = 1 ) → ( 𝐵 logb 𝑋 ) ∈ ( ℝ ∖ ℚ ) )
8	2 4 6 7	syl3anc	⊢ ( ( 𝑋 ∈ ℙ ∧ 𝐵 ∈ ℙ ∧ 𝑋 ≠ 𝐵 ) → ( 𝐵 logb 𝑋 ) ∈ ( ℝ ∖ ℚ ) )