Metamath Proof Explorer


Theorem qrevaddcl

Description: Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion qrevaddcl B A A + B A

Proof

Step Hyp Ref Expression
1 qcn B B
2 pncan A B A + B - B = A
3 1 2 sylan2 A B A + B - B = A
4 3 ancoms B A A + B - B = A
5 4 adantr B A A + B A + B - B = A
6 qsubcl A + B B A + B - B
7 6 ancoms B A + B A + B - B
8 7 adantlr B A A + B A + B - B
9 5 8 eqeltrrd B A A + B A
10 9 ex B A A + B A
11 qaddcl A B A + B
12 11 expcom B A A + B
13 12 adantr B A A A + B
14 10 13 impbid B A A + B A
15 14 pm5.32da B A A + B A A
16 qcn A A
17 16 pm4.71ri A A A
18 15 17 bitr4di B A A + B A