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

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