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 ) ∈ ( ℝ ∖ ℚ )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		9nn	⊢ 9 ∈ ℕ
3	2	nnzi	⊢ 9 ∈ ℤ
4		2re	⊢ 2 ∈ ℝ
5		9re	⊢ 9 ∈ ℝ
6		2lt9	⊢ 2 < 9
7	4 5 6	ltleii	⊢ 2 ≤ 9
8		eluz2	⊢ ( 9 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 9 ∈ ℤ ∧ 2 ≤ 9 ) )
9	1 3 7 8	mpbir3an	⊢ 9 ∈ ( ℤ≥ ‘ 2 )
10		uzid	⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
11	1 10	ax-mp	⊢ 2 ∈ ( ℤ≥ ‘ 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 ∈ ℙ
18		2prm	⊢ 2 ∈ ℙ
19		prmrp	⊢ ( ( 3 ∈ ℙ ∧ 2 ∈ ℙ ) → ( ( 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 ∈ ℤ
23		2nn0	⊢ 2 ∈ ℕ0
24		rpexp1i	⊢ ( ( 3 ∈ ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℕ0 ) → ( ( 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 ∈ ( ℤ≥ ‘ 2 ) ∧ 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 9 gcd 2 ) = 1 ) → ( 2 logb 9 ) ∈ ( ℝ ∖ ℚ ) )
29	9 11 27 28	mp3an	⊢ ( 2 logb 9 ) ∈ ( ℝ ∖ ℚ )