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

Metamath Proof Explorer

Theorem qrevaddcl

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

Ref Expression
Assertion qrevaddcl 
|- ( B e. QQ -> ( ( A e. CC /\ ( A + B ) e. QQ ) <-> A e. QQ ) )

Proof

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