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 ∈ ℤ