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 ⊢ X ∈ ℙ ∧ B ∈ ℙ ∧ X ≠ B → log B X ∈ ℝ ∖ ℚ

Proof

Step Hyp Ref Expression
1 prmuz2 ⊢ X ∈ ℙ → X ∈ ℤ ≥ 2
2 1 3ad2ant1 ⊢ X ∈ ℙ ∧ B ∈ ℙ ∧ X ≠ B → X ∈ ℤ ≥ 2
3 prmuz2 ⊢ B ∈ ℙ → B ∈ ℤ ≥ 2
4 3 3ad2ant2 ⊢ X ∈ ℙ ∧ B ∈ ℙ ∧ X ≠ B → B ∈ ℤ ≥ 2
5 prmrp ⊢ X ∈ ℙ ∧ B ∈ ℙ → X gcd B = 1 ↔ X ≠ B
6 5 biimp3ar ⊢ X ∈ ℙ ∧ B ∈ ℙ ∧ X ≠ B → X gcd B = 1
7 logbgcd1irr ⊢ X ∈ ℤ ≥ 2 ∧ B ∈ ℤ ≥ 2 ∧ X gcd B = 1 → log B X ∈ ℝ ∖ ℚ
8 2 4 6 7 syl3anc ⊢ X ∈ ℙ ∧ B ∈ ℙ ∧ X ≠ B → log B X ∈ ℝ ∖ ℚ