This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )