Theorem qre

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

	Ref	Expression
Assertion	qre	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		elq	⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
2		zre	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
3		nnre	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
4		nnne0	⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
5	3 4	jca	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℝ ∧ 𝑦 ≠ 0 ) )
6		redivcl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑦 ≠ 0 ) → ( 𝑥 / 𝑦 ) ∈ ℝ )
7	6	3expb	⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑦 ∈ ℝ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 / 𝑦 ) ∈ ℝ )
8	2 5 7	syl2an	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 / 𝑦 ) ∈ ℝ )
9		eleq1	⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ∈ ℝ ↔ ( 𝑥 / 𝑦 ) ∈ ℝ ) )
10	8 9	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → 𝐴 ∈ ℝ ) )
11	10	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) → 𝐴 ∈ ℝ )
12	1 11	sylbi	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℝ )