Metamath Proof Explorer


Theorem resubcli

Description: Closure law for subtraction of reals. (Contributed by NM, 17-Jan-1997) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses renegcl.1 A
resubcl.2 B
Assertion resubcli AB

Proof

Step Hyp Ref Expression
1 renegcl.1 A
2 resubcl.2 B
3 1 recni A
4 2 recni B
5 negsub ABA+B=AB
6 3 4 5 mp2an A+B=AB
7 2 renegcli B
8 1 7 readdcli A+B
9 6 8 eqeltrri AB