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 \in ℚ \to \exists x \in ℕ A x \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		elq	$⊢ A \in ℚ \leftrightarrow \exists y \in ℤ \exists x \in ℕ A = \frac{y}{x}$
2		rexcom	$⊢ \exists y \in ℤ \exists x \in ℕ A = \frac{y}{x} \leftrightarrow \exists x \in ℕ \exists y \in ℤ A = \frac{y}{x}$
3		zcn	$⊢ y \in ℤ \to y \in ℂ$
4	3	adantl	$⊢ (x \in ℕ \land y \in ℤ) \to y \in ℂ$
5		nncn	$⊢ x \in ℕ \to x \in ℂ$
6	5	adantr	$⊢ (x \in ℕ \land y \in ℤ) \to x \in ℂ$
7		nnne0	$⊢ x \in ℕ \to x \neq 0$
8	7	adantr	$⊢ (x \in ℕ \land y \in ℤ) \to x \neq 0$
9	4 6 8	divcan1d	$⊢ (x \in ℕ \land y \in ℤ) \to (\frac{y}{x}) x = y$
10		simpr	$⊢ (x \in ℕ \land y \in ℤ) \to y \in ℤ$
11	9 10	eqeltrd	$⊢ (x \in ℕ \land y \in ℤ) \to (\frac{y}{x}) x \in ℤ$
12		oveq1	$⊢ A = \frac{y}{x} \to A x = (\frac{y}{x}) x$
13	12	eleq1d	$⊢ A = \frac{y}{x} \to (A x \in ℤ \leftrightarrow (\frac{y}{x}) x \in ℤ)$
14	11 13	syl5ibrcom	$⊢ (x \in ℕ \land y \in ℤ) \to (A = \frac{y}{x} \to A x \in ℤ)$
15	14	rexlimdva	$⊢ x \in ℕ \to (\exists y \in ℤ A = \frac{y}{x} \to A x \in ℤ)$
16	15	reximia	$⊢ \exists x \in ℕ \exists y \in ℤ A = \frac{y}{x} \to \exists x \in ℕ A x \in ℤ$
17	2 16	sylbi	$⊢ \exists y \in ℤ \exists x \in ℕ A = \frac{y}{x} \to \exists x \in ℕ A x \in ℤ$
18	1 17	sylbi	$⊢ A \in ℚ \to \exists x \in ℕ A x \in ℤ$