zrevaddcl

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

		Ref	Expression
	Assertion	zrevaddcl	$⊢ N \in ℤ \to ((M \in ℂ \land M + N \in ℤ) \leftrightarrow M \in ℤ)$

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

Metamath Proof Explorer