This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℝ )