Metamath Proof Explorer

Theorem 2logb9irrALT

Description: Alternate proof of 2logb9irr : The logarithm of nine to base two is irrational. (Contributed by AV, 31-Dec-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 2logb9irrALT 
|- ( 2 logb 9 ) e. ( RR \ QQ )

Proof

Step Hyp Ref Expression
1 sq3 
 |-  ( 3 ^ 2 ) = 9
2 1 eqcomi 
 |-  9 = ( 3 ^ 2 )
3 2 oveq2i 
 |-  ( 2 logb 9 ) = ( 2 logb ( 3 ^ 2 ) )
4 2cn 
 |-  2 e. CC
5 2ne0 
 |-  2 =/= 0
6 1ne2 
 |-  1 =/= 2
7 6 necomi 
 |-  2 =/= 1
8 eldifpr 
 |-  ( 2 e. ( CC \ { 0 , 1 } ) <-> ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) )
9 4 5 7 8 mpbir3an 
 |-  2 e. ( CC \ { 0 , 1 } )
10 3rp 
 |-  3 e. RR+
11 2z 
 |-  2 e. ZZ
12 relogbzexp 
 |-  ( ( 2 e. ( CC \ { 0 , 1 } ) /\ 3 e. RR+ /\ 2 e. ZZ ) -> ( 2 logb ( 3 ^ 2 ) ) = ( 2 x. ( 2 logb 3 ) ) )
13 9 10 11 12 mp3an 
 |-  ( 2 logb ( 3 ^ 2 ) ) = ( 2 x. ( 2 logb 3 ) )
14 3 13 eqtri 
 |-  ( 2 logb 9 ) = ( 2 x. ( 2 logb 3 ) )
15 3cn 
 |-  3 e. CC
16 3ne0 
 |-  3 =/= 0
17 eldifsn 
 |-  ( 3 e. ( CC \ { 0 } ) <-> ( 3 e. CC /\ 3 =/= 0 ) )
18 15 16 17 mpbir2an 
 |-  3 e. ( CC \ { 0 } )
19 logbcl 
 |-  ( ( 2 e. ( CC \ { 0 , 1 } ) /\ 3 e. ( CC \ { 0 } ) ) -> ( 2 logb 3 ) e. CC )
20 9 18 19 mp2an 
 |-  ( 2 logb 3 ) e. CC
21 4 20 mulcomi 
 |-  ( 2 x. ( 2 logb 3 ) ) = ( ( 2 logb 3 ) x. 2 )
22 2logb3irr 
 |-  ( 2 logb 3 ) e. ( RR \ QQ )
23 zq 
 |-  ( 2 e. ZZ -> 2 e. QQ )
24 11 23 ax-mp 
 |-  2 e. QQ
25 irrmul 
 |-  ( ( ( 2 logb 3 ) e. ( RR \ QQ ) /\ 2 e. QQ /\ 2 =/= 0 ) -> ( ( 2 logb 3 ) x. 2 ) e. ( RR \ QQ ) )
26 22 24 5 25 mp3an 
 |-  ( ( 2 logb 3 ) x. 2 ) e. ( RR \ QQ )
27 21 26 eqeltri 
 |-  ( 2 x. ( 2 logb 3 ) ) e. ( RR \ QQ )
28 14 27 eqeltri 
 |-  ( 2 logb 9 ) e. ( RR \ QQ )