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 ⊢ log 2 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 → log 2 9 ∈ ℝ ∖ ℚ
29 9 11 27 28 mp3an ⊢ log 2 9 ∈ ℝ ∖ ℚ