# 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 ${⊢}\left({X}\in ℙ\wedge {B}\in ℙ\wedge {X}\ne {B}\right)\to {\mathrm{log}}_{{B}}{X}\in \left(ℝ\setminus ℚ\right)$

### Proof

Step Hyp Ref Expression
1 prmuz2 ${⊢}{X}\in ℙ\to {X}\in {ℤ}_{\ge 2}$
2 1 3ad2ant1 ${⊢}\left({X}\in ℙ\wedge {B}\in ℙ\wedge {X}\ne {B}\right)\to {X}\in {ℤ}_{\ge 2}$
3 prmuz2 ${⊢}{B}\in ℙ\to {B}\in {ℤ}_{\ge 2}$
4 3 3ad2ant2 ${⊢}\left({X}\in ℙ\wedge {B}\in ℙ\wedge {X}\ne {B}\right)\to {B}\in {ℤ}_{\ge 2}$
5 prmrp ${⊢}\left({X}\in ℙ\wedge {B}\in ℙ\right)\to \left({X}\mathrm{gcd}{B}=1↔{X}\ne {B}\right)$
6 5 biimp3ar ${⊢}\left({X}\in ℙ\wedge {B}\in ℙ\wedge {X}\ne {B}\right)\to {X}\mathrm{gcd}{B}=1$
7 logbgcd1irr ${⊢}\left({X}\in {ℤ}_{\ge 2}\wedge {B}\in {ℤ}_{\ge 2}\wedge {X}\mathrm{gcd}{B}=1\right)\to {\mathrm{log}}_{{B}}{X}\in \left(ℝ\setminus ℚ\right)$
8 2 4 6 7 syl3anc ${⊢}\left({X}\in ℙ\wedge {B}\in ℙ\wedge {X}\ne {B}\right)\to {\mathrm{log}}_{{B}}{X}\in \left(ℝ\setminus ℚ\right)$