Metamath Proof Explorer


Theorem qmulz

Description: If A is rational, then some integer multiple of it is an integer. (Contributed by NM, 7-Nov-2008) (Revised by Mario Carneiro, 22-Jul-2014)

Ref Expression
Assertion qmulz
|- ( A e. QQ -> E. x e. NN ( A x. x ) e. ZZ )

Proof

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 )