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