Metamath Proof Explorer


Theorem zrevaddcl

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

Ref Expression
Assertion zrevaddcl N M M + N M

Proof

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