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