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

Metamath Proof Explorer

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 𝑋 ) ∈ ( ℝ ∖ ℚ ) )