This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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