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