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 ∈ ℚ → ∃ 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 ∈ ℤ