# Metamath Proof Explorer

## Theorem qre

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

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

### Proof

Step Hyp Ref Expression
1 elq ${⊢}{A}\in ℚ↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{A}=\frac{{x}}{{y}}$
2 zre ${⊢}{x}\in ℤ\to {x}\in ℝ$
3 nnre ${⊢}{y}\in ℕ\to {y}\in ℝ$
4 nnne0 ${⊢}{y}\in ℕ\to {y}\ne 0$
5 3 4 jca ${⊢}{y}\in ℕ\to \left({y}\in ℝ\wedge {y}\ne 0\right)$
6 redivcl ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\wedge {y}\ne 0\right)\to \frac{{x}}{{y}}\in ℝ$
7 6 3expb ${⊢}\left({x}\in ℝ\wedge \left({y}\in ℝ\wedge {y}\ne 0\right)\right)\to \frac{{x}}{{y}}\in ℝ$
8 2 5 7 syl2an ${⊢}\left({x}\in ℤ\wedge {y}\in ℕ\right)\to \frac{{x}}{{y}}\in ℝ$
9 eleq1 ${⊢}{A}=\frac{{x}}{{y}}\to \left({A}\in ℝ↔\frac{{x}}{{y}}\in ℝ\right)$
10 8 9 syl5ibrcom ${⊢}\left({x}\in ℤ\wedge {y}\in ℕ\right)\to \left({A}=\frac{{x}}{{y}}\to {A}\in ℝ\right)$
11 10 rexlimivv ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{A}=\frac{{x}}{{y}}\to {A}\in ℝ$
12 1 11 sylbi ${⊢}{A}\in ℚ\to {A}\in ℝ$