Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  qre GIF version

Theorem qre 8657
 Description: A rational number is a real number. (Contributed by NM, 14-Nov-2002.)
Assertion
Ref Expression
qre (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)

Proof of Theorem qre
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elq 8654 . 2 (𝐴 ∈ ℚ ↔ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦))
2 zre 8306 . . . . 5 (𝑥 ∈ ℤ → 𝑥 ∈ ℝ)
3 nnre 7997 . . . . . 6 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
4 nnap0 8019 . . . . . 6 (𝑦 ∈ ℕ → 𝑦 # 0)
53, 4jca 294 . . . . 5 (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 𝑦 # 0))
6 redivclap 7782 . . . . . 6 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑦 # 0) → (𝑥 / 𝑦) ∈ ℝ)
763expb 1116 . . . . 5 ((𝑥 ∈ ℝ ∧ (𝑦 ∈ ℝ ∧ 𝑦 # 0)) → (𝑥 / 𝑦) ∈ ℝ)
82, 5, 7syl2an 277 . . . 4 ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝑥 / 𝑦) ∈ ℝ)
9 eleq1 2116 . . . 4 (𝐴 = (𝑥 / 𝑦) → (𝐴 ∈ ℝ ↔ (𝑥 / 𝑦) ∈ ℝ))
108, 9syl5ibrcom 150 . . 3 ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ) → (𝐴 = (𝑥 / 𝑦) → 𝐴 ∈ ℝ))
1110rexlimivv 2455 . 2 (∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ 𝐴 = (𝑥 / 𝑦) → 𝐴 ∈ ℝ)
121, 11sylbi 118 1 (𝐴 ∈ ℚ → 𝐴 ∈ ℝ)