Metamath Proof Explorer

Theorem 2logb3irr

Description: Example for logbprmirr . The logarithm of three to base two is irrational. (Contributed by AV, 31-Dec-2022)

Ref Expression
Assertion 2logb3irr 
|- ( 2 logb 3 ) e. ( RR \ QQ )

Proof

Step Hyp Ref Expression
1 3prm 
 |-  3 e. Prime
2 2prm 
 |-  2 e. Prime
3 2re 
 |-  2 e. RR
4 2lt3 
 |-  2 < 3
5 3 4 gtneii 
 |-  3 =/= 2
6 logbprmirr 
 |-  ( ( 3 e. Prime /\ 2 e. Prime /\ 3 =/= 2 ) -> ( 2 logb 3 ) e. ( RR \ QQ ) )
7 1 2 5 6 mp3an 
 |-  ( 2 logb 3 ) e. ( RR \ QQ )