Metamath Proof Explorer


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