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 e. Prime /\ B e. Prime /\ X =/= B ) -> ( B logb X ) e. ( RR \ QQ ) )

Proof

Step Hyp Ref Expression
1 prmuz2 
 |-  ( X e. Prime -> X e. ( ZZ>= ` 2 ) )
2 1 3ad2ant1 
 |-  ( ( X e. Prime /\ B e. Prime /\ X =/= B ) -> X e. ( ZZ>= ` 2 ) )
3 prmuz2 
 |-  ( B e. Prime -> B e. ( ZZ>= ` 2 ) )
4 3 3ad2ant2 
 |-  ( ( X e. Prime /\ B e. Prime /\ X =/= B ) -> B e. ( ZZ>= ` 2 ) )
5 prmrp 
 |-  ( ( X e. Prime /\ B e. Prime ) -> ( ( X gcd B ) = 1 <-> X =/= B ) )
6 5 biimp3ar 
 |-  ( ( X e. Prime /\ B e. Prime /\ X =/= B ) -> ( X gcd B ) = 1 )
7 logbgcd1irr 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) /\ ( X gcd B ) = 1 ) -> ( B logb X ) e. ( RR \ QQ ) )
8 2 4 6 7 syl3anc 
 |-  ( ( X e. Prime /\ B e. Prime /\ X =/= B ) -> ( B logb X ) e. ( RR \ QQ ) )