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 ) )