qre

Description: A rational number is a real number. (Contributed by NM, 14-Nov-2002)

		Ref	Expression
	Assertion	qre	$⊢ A \in ℚ \to A \in ℝ$

Step	Hyp	Ref	Expression
1		elq	$⊢ A \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y}$
2		zre	$⊢ x \in ℤ \to x \in ℝ$
3		nnre	$⊢ y \in ℕ \to y \in ℝ$
4		nnne0	$⊢ y \in ℕ \to y \neq 0$
5	3 4	jca	$⊢ y \in ℕ \to (y \in ℝ \land y \neq 0)$
6		redivcl	$⊢ (x \in ℝ \land y \in ℝ \land y \neq 0) \to \frac{x}{y} \in ℝ$
7	6	3expb	$⊢ (x \in ℝ \land (y \in ℝ \land y \neq 0)) \to \frac{x}{y} \in ℝ$
8	2 5 7	syl2an	$⊢ (x \in ℤ \land y \in ℕ) \to \frac{x}{y} \in ℝ$
9		eleq1	$⊢ A = \frac{x}{y} \to (A \in ℝ \leftrightarrow \frac{x}{y} \in ℝ)$
10	8 9	syl5ibrcom	$⊢ (x \in ℤ \land y \in ℕ) \to (A = \frac{x}{y} \to A \in ℝ)$
11	10	rexlimivv	$⊢ \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y} \to A \in ℝ$
12	1 11	sylbi	$⊢ A \in ℚ \to A \in ℝ$

Metamath Proof Explorer