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 ( 𝐴 ∈ ℚ → ∃ 𝑥 ∈ ℕ ( 𝐴 · 𝑥 ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 elq ( 𝐴 ∈ ℚ ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑦 / 𝑥 ) )
2 rexcom ( ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑦 / 𝑥 ) ↔ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℤ 𝐴 = ( 𝑦 / 𝑥 ) )
3 zcn ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
4 3 adantl ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → 𝑦 ∈ ℂ )
5 nncn ( 𝑥 ∈ ℕ → 𝑥 ∈ ℂ )
6 5 adantr ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → 𝑥 ∈ ℂ )
7 nnne0 ( 𝑥 ∈ ℕ → 𝑥 ≠ 0 )
8 7 adantr ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → 𝑥 ≠ 0 )
9 4 6 8 divcan1d ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑦 / 𝑥 ) · 𝑥 ) = 𝑦 )
10 simpr ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → 𝑦 ∈ ℤ )
11 9 10 eqeltrd ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑦 / 𝑥 ) · 𝑥 ) ∈ ℤ )
12 oveq1 ( 𝐴 = ( 𝑦 / 𝑥 ) → ( 𝐴 · 𝑥 ) = ( ( 𝑦 / 𝑥 ) · 𝑥 ) )
13 12 eleq1d ( 𝐴 = ( 𝑦 / 𝑥 ) → ( ( 𝐴 · 𝑥 ) ∈ ℤ ↔ ( ( 𝑦 / 𝑥 ) · 𝑥 ) ∈ ℤ ) )
14 11 13 syl5ibrcom ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → ( 𝐴 = ( 𝑦 / 𝑥 ) → ( 𝐴 · 𝑥 ) ∈ ℤ ) )
15 14 rexlimdva ( 𝑥 ∈ ℕ → ( ∃ 𝑦 ∈ ℤ 𝐴 = ( 𝑦 / 𝑥 ) → ( 𝐴 · 𝑥 ) ∈ ℤ ) )
16 15 reximia ( ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℤ 𝐴 = ( 𝑦 / 𝑥 ) → ∃ 𝑥 ∈ ℕ ( 𝐴 · 𝑥 ) ∈ ℤ )
17 2 16 sylbi ( ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑦 / 𝑥 ) → ∃ 𝑥 ∈ ℕ ( 𝐴 · 𝑥 ) ∈ ℤ )
18 1 17 sylbi ( 𝐴 ∈ ℚ → ∃ 𝑥 ∈ ℕ ( 𝐴 · 𝑥 ) ∈ ℤ )