Metamath Proof Explorer


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