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