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 ( 𝑁 ∈ ℤ → ( ( 𝑀 ∈ ℂ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) ↔ 𝑀 ∈ ℤ ) )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2 pncan ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
3 1 2 sylan2 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
4 3 ancoms ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
5 4 adantr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℂ ) ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) = 𝑀 )
6 zsubcl ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) ∈ ℤ )
7 6 ancoms ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) ∈ ℤ )
8 7 adantlr ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℂ ) ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → ( ( 𝑀 + 𝑁 ) − 𝑁 ) ∈ ℤ )
9 5 8 eqeltrrd ⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℂ ) ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) → 𝑀 ∈ ℤ )
10 9 ex ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) ∈ ℤ → 𝑀 ∈ ℤ ) )
11 zaddcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
12 11 expcom ⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ℤ → ( 𝑀 + 𝑁 ) ∈ ℤ ) )
13 12 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℂ ) → ( 𝑀 ∈ ℤ → ( 𝑀 + 𝑁 ) ∈ ℤ ) )
14 10 13 impbid ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑀 + 𝑁 ) ∈ ℤ ↔ 𝑀 ∈ ℤ ) )
15 14 pm5.32da ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑀 ∈ ℂ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) ↔ ( 𝑀 ∈ ℂ ∧ 𝑀 ∈ ℤ ) ) )
16 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
17 16 pm4.71ri ⊢ ( 𝑀 ∈ ℤ ↔ ( 𝑀 ∈ ℂ ∧ 𝑀 ∈ ℤ ) )
18 15 17 bitr4di ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑀 ∈ ℂ ∧ ( 𝑀 + 𝑁 ) ∈ ℤ ) ↔ 𝑀 ∈ ℤ ) )