| Step |
Hyp |
Ref |
Expression |
| 1 |
|
2z |
|- 2 e. ZZ |
| 2 |
|
9nn |
|- 9 e. NN |
| 3 |
2
|
nnzi |
|- 9 e. ZZ |
| 4 |
|
2re |
|- 2 e. RR |
| 5 |
|
9re |
|- 9 e. RR |
| 6 |
|
2lt9 |
|- 2 < 9 |
| 7 |
4 5 6
|
ltleii |
|- 2 <_ 9 |
| 8 |
|
eluz2 |
|- ( 9 e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ 9 e. ZZ /\ 2 <_ 9 ) ) |
| 9 |
1 3 7 8
|
mpbir3an |
|- 9 e. ( ZZ>= ` 2 ) |
| 10 |
|
uzid |
|- ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) ) |
| 11 |
1 10
|
ax-mp |
|- 2 e. ( ZZ>= ` 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 e. Prime |
| 18 |
|
2prm |
|- 2 e. Prime |
| 19 |
|
prmrp |
|- ( ( 3 e. Prime /\ 2 e. Prime ) -> ( ( 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 e. ZZ |
| 23 |
|
2nn0 |
|- 2 e. NN0 |
| 24 |
|
rpexp1i |
|- ( ( 3 e. ZZ /\ 2 e. ZZ /\ 2 e. NN0 ) -> ( ( 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 e. ( ZZ>= ` 2 ) /\ 2 e. ( ZZ>= ` 2 ) /\ ( 9 gcd 2 ) = 1 ) -> ( 2 logb 9 ) e. ( RR \ QQ ) ) |
| 29 |
9 11 27 28
|
mp3an |
|- ( 2 logb 9 ) e. ( RR \ QQ ) |