Step |
Hyp |
Ref |
Expression |
1 |
|
sqrt2irr0 |
|- ( sqrt ` 2 ) e. ( RR \ QQ ) |
2 |
|
2logb9irr |
|- ( 2 logb 9 ) e. ( RR \ QQ ) |
3 |
|
sqrt2cxp2logb9e3 |
|- ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) = 3 |
4 |
|
3z |
|- 3 e. ZZ |
5 |
|
zq |
|- ( 3 e. ZZ -> 3 e. QQ ) |
6 |
4 5
|
ax-mp |
|- 3 e. QQ |
7 |
3 6
|
eqeltri |
|- ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) e. QQ |
8 |
|
oveq1 |
|- ( a = ( sqrt ` 2 ) -> ( a ^c b ) = ( ( sqrt ` 2 ) ^c b ) ) |
9 |
8
|
eleq1d |
|- ( a = ( sqrt ` 2 ) -> ( ( a ^c b ) e. QQ <-> ( ( sqrt ` 2 ) ^c b ) e. QQ ) ) |
10 |
|
oveq2 |
|- ( b = ( 2 logb 9 ) -> ( ( sqrt ` 2 ) ^c b ) = ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) ) |
11 |
10
|
eleq1d |
|- ( b = ( 2 logb 9 ) -> ( ( ( sqrt ` 2 ) ^c b ) e. QQ <-> ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) e. QQ ) ) |
12 |
9 11
|
rspc2ev |
|- ( ( ( sqrt ` 2 ) e. ( RR \ QQ ) /\ ( 2 logb 9 ) e. ( RR \ QQ ) /\ ( ( sqrt ` 2 ) ^c ( 2 logb 9 ) ) e. QQ ) -> E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ ) |
13 |
1 2 7 12
|
mp3an |
|- E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ |