Metamath Proof Explorer


Theorem qsubcl

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

Ref Expression
Assertion qsubcl ABAB

Proof

Step Hyp Ref Expression
1 qcn AA
2 qcn BB
3 negsub ABA+B=AB
4 1 2 3 syl2an ABA+B=AB
5 qnegcl BB
6 qaddcl ABA+B
7 5 6 sylan2 ABA+B
8 4 7 eqeltrrd ABAB