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

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