Theorem 2logb9irr

Description: Example for logbgcd1irr . The logarithm of nine to base two is irrational. (Contributed by AV, 29-Dec-2022)

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

Proof

Step	Hyp	Ref	Expression
1		2z	|- 2 e. ZZ
2		9nn	|- 9 e. NN
3	2	nnzi	|- 9 e. ZZ
4		2re	|- 2 e. RR
5		9re	|- 9 e. RR
6		2lt9	|- 2 < 9
7	4 5 6	ltleii	|- 2 <_ 9
8		eluz2	|- ( 9 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 9 e. ZZ /\ 2 <_ 9 ) )
9	1 3 7 8	mpbir3an	|- 9 e. ( ZZ>= ` 2 )
10		uzid	|- ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
11	1 10	ax-mp	|- 2 e. ( ZZ>= ` 2 )
12		sq3	|- ( 3 ^ 2 ) = 9
13	12	eqcomi	|- 9 = ( 3 ^ 2 )
14	13	oveq1i	|- ( 9 gcd 2 ) = ( ( 3 ^ 2 ) gcd 2 )
15		2lt3	|- 2 < 3
16	4 15	gtneii	|- 3 =/= 2
17		3prm	|- 3 e. Prime
18		2prm	|- 2 e. Prime
19		prmrp	|- ( ( 3 e. Prime /\ 2 e. Prime ) -> ( ( 3 gcd 2 ) = 1 <-> 3 =/= 2 ) )
20	17 18 19	mp2an	|- ( ( 3 gcd 2 ) = 1 <-> 3 =/= 2 )
21	16 20	mpbir	|- ( 3 gcd 2 ) = 1
22		3z	|- 3 e. ZZ
23		2nn0	|- 2 e. NN0
24		rpexp1i	|- ( ( 3 e. ZZ /\ 2 e. ZZ /\ 2 e. NN0 ) -> ( ( 3 gcd 2 ) = 1 -> ( ( 3 ^ 2 ) gcd 2 ) = 1 ) )
25	22 1 23 24	mp3an	|- ( ( 3 gcd 2 ) = 1 -> ( ( 3 ^ 2 ) gcd 2 ) = 1 )
26	21 25	ax-mp	|- ( ( 3 ^ 2 ) gcd 2 ) = 1
27	14 26	eqtri	|- ( 9 gcd 2 ) = 1
28		logbgcd1irr	|- ( ( 9 e. ( ZZ>= ` 2 ) /\ 2 e. ( ZZ>= ` 2 ) /\ ( 9 gcd 2 ) = 1 ) -> ( 2 logb 9 ) e. ( RR \ QQ ) )
29	9 11 27 28	mp3an	|- ( 2 logb 9 ) e. ( RR \ QQ )