Step |
Hyp |
Ref |
Expression |
1 |
|
elq |
|- ( A e. QQ <-> E. y e. ZZ E. x e. NN A = ( y / x ) ) |
2 |
|
rexcom |
|- ( E. y e. ZZ E. x e. NN A = ( y / x ) <-> E. x e. NN E. y e. ZZ A = ( y / x ) ) |
3 |
|
zcn |
|- ( y e. ZZ -> y e. CC ) |
4 |
3
|
adantl |
|- ( ( x e. NN /\ y e. ZZ ) -> y e. CC ) |
5 |
|
nncn |
|- ( x e. NN -> x e. CC ) |
6 |
5
|
adantr |
|- ( ( x e. NN /\ y e. ZZ ) -> x e. CC ) |
7 |
|
nnne0 |
|- ( x e. NN -> x =/= 0 ) |
8 |
7
|
adantr |
|- ( ( x e. NN /\ y e. ZZ ) -> x =/= 0 ) |
9 |
4 6 8
|
divcan1d |
|- ( ( x e. NN /\ y e. ZZ ) -> ( ( y / x ) x. x ) = y ) |
10 |
|
simpr |
|- ( ( x e. NN /\ y e. ZZ ) -> y e. ZZ ) |
11 |
9 10
|
eqeltrd |
|- ( ( x e. NN /\ y e. ZZ ) -> ( ( y / x ) x. x ) e. ZZ ) |
12 |
|
oveq1 |
|- ( A = ( y / x ) -> ( A x. x ) = ( ( y / x ) x. x ) ) |
13 |
12
|
eleq1d |
|- ( A = ( y / x ) -> ( ( A x. x ) e. ZZ <-> ( ( y / x ) x. x ) e. ZZ ) ) |
14 |
11 13
|
syl5ibrcom |
|- ( ( x e. NN /\ y e. ZZ ) -> ( A = ( y / x ) -> ( A x. x ) e. ZZ ) ) |
15 |
14
|
rexlimdva |
|- ( x e. NN -> ( E. y e. ZZ A = ( y / x ) -> ( A x. x ) e. ZZ ) ) |
16 |
15
|
reximia |
|- ( E. x e. NN E. y e. ZZ A = ( y / x ) -> E. x e. NN ( A x. x ) e. ZZ ) |
17 |
2 16
|
sylbi |
|- ( E. y e. ZZ E. x e. NN A = ( y / x ) -> E. x e. NN ( A x. x ) e. ZZ ) |
18 |
1 17
|
sylbi |
|- ( A e. QQ -> E. x e. NN ( A x. x ) e. ZZ ) |