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 )