Theorem zrevaddcl

Description: Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004)

	Ref	Expression
Assertion	zrevaddcl	|- ( N e. ZZ -> ( ( M e. CC /\ ( M + N ) e. ZZ ) <-> M e. ZZ ) )

Proof

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