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

Metamath Proof Explorer

Theorem qsubcl

Description: Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion qsubcl ⊢ A ∈ ℚ ∧ B ∈ ℚ → A − B ∈ ℚ

Proof

Step Hyp Ref Expression
1 qcn ⊢ A ∈ ℚ → A ∈ ℂ
2 qcn ⊢ B ∈ ℚ → B ∈ ℂ
3 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
4 1 2 3 syl2an ⊢ A ∈ ℚ ∧ B ∈ ℚ → A + − B = A − B
5 qnegcl ⊢ B ∈ ℚ → − B ∈ ℚ
6 qaddcl ⊢ A ∈ ℚ ∧ − B ∈ ℚ → A + − B ∈ ℚ
7 5 6 sylan2 ⊢ A ∈ ℚ ∧ B ∈ ℚ → A + − B ∈ ℚ
8 4 7 eqeltrrd ⊢ A ∈ ℚ ∧ B ∈ ℚ → A − B ∈ ℚ