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 x A x

Proof

Step Hyp Ref Expression
1 elq A y x A = y x
2 rexcom y x A = y x x y A = y x
3 zcn y y
4 3 adantl x y y
5 nncn x x
6 5 adantr x y x
7 nnne0 x x 0
8 7 adantr x y x 0
9 4 6 8 divcan1d x y y x x = y
10 simpr x y y
11 9 10 eqeltrd x y y x x
12 oveq1 A = y x A x = y x x
13 12 eleq1d A = y x A x y x x
14 11 13 syl5ibrcom x y A = y x A x
15 14 rexlimdva x y A = y x A x
16 15 reximia x y A = y x x A x
17 2 16 sylbi y x A = y x x A x
18 1 17 sylbi A x A x