zmulcl

Description: Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004)

		Ref	Expression
	Assertion	zmulcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		elznn0	$⊢ M \in ℤ \leftrightarrow (M \in ℝ \land (M \in ℕ_{0} \lor - M \in ℕ_{0}))$
2		elznn0	$⊢ N \in ℤ \leftrightarrow (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
3		nn0mulcl	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M \cdot N \in ℕ_{0}$
4	3	orcd	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0})$
5	4	a1i	$⊢ (M \in ℝ \land N \in ℝ) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0}))$
6		remulcl	$⊢ (M \in ℝ \land N \in ℝ) \to M \cdot N \in ℝ$
7	5 6	jctild	$⊢ (M \in ℝ \land N \in ℝ) \to ((M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \cdot N \in ℝ \land (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0})))$
8		nn0mulcl	$⊢ (- M \in ℕ_{0} \land N \in ℕ_{0}) \to -M \cdot N \in ℕ_{0}$
9		recn	$⊢ M \in ℝ \to M \in ℂ$
10		recn	$⊢ N \in ℝ \to N \in ℂ$
11		mulneg1	$⊢ (M \in ℂ \land N \in ℂ) \to -M \cdot N = - M \cdot N$
12	9 10 11	syl2an	$⊢ (M \in ℝ \land N \in ℝ) \to -M \cdot N = - M \cdot N$
13	12	eleq1d	$⊢ (M \in ℝ \land N \in ℝ) \to (-M \cdot N \in ℕ_{0} \leftrightarrow - M \cdot N \in ℕ_{0})$
14	8 13	imbitrid	$⊢ (M \in ℝ \land N \in ℝ) \to ((- M \in ℕ_{0} \land N \in ℕ_{0}) \to - M \cdot N \in ℕ_{0})$
15		olc	$⊢ - M \cdot N \in ℕ_{0} \to (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0})$
16	14 15	syl6	$⊢ (M \in ℝ \land N \in ℝ) \to ((- M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0}))$
17	16 6	jctild	$⊢ (M \in ℝ \land N \in ℝ) \to ((- M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \cdot N \in ℝ \land (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0})))$
18		nn0mulcl	$⊢ (M \in ℕ_{0} \land - N \in ℕ_{0}) \to M -N \in ℕ_{0}$
19		mulneg2	$⊢ (M \in ℂ \land N \in ℂ) \to M -N = - M \cdot N$
20	9 10 19	syl2an	$⊢ (M \in ℝ \land N \in ℝ) \to M -N = - M \cdot N$
21	20	eleq1d	$⊢ (M \in ℝ \land N \in ℝ) \to (M -N \in ℕ_{0} \leftrightarrow - M \cdot N \in ℕ_{0})$
22	18 21	imbitrid	$⊢ (M \in ℝ \land N \in ℝ) \to ((M \in ℕ_{0} \land - N \in ℕ_{0}) \to - M \cdot N \in ℕ_{0})$
23	22 15	syl6	$⊢ (M \in ℝ \land N \in ℝ) \to ((M \in ℕ_{0} \land - N \in ℕ_{0}) \to (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0}))$
24	23 6	jctild	$⊢ (M \in ℝ \land N \in ℝ) \to ((M \in ℕ_{0} \land - N \in ℕ_{0}) \to (M \cdot N \in ℝ \land (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0})))$
25		nn0mulcl	$⊢ (- M \in ℕ_{0} \land - N \in ℕ_{0}) \to -M -N \in ℕ_{0}$
26		mul2neg	$⊢ (M \in ℂ \land N \in ℂ) \to -M -N = M \cdot N$
27	9 10 26	syl2an	$⊢ (M \in ℝ \land N \in ℝ) \to -M -N = M \cdot N$
28	27	eleq1d	$⊢ (M \in ℝ \land N \in ℝ) \to (-M -N \in ℕ_{0} \leftrightarrow M \cdot N \in ℕ_{0})$
29	25 28	imbitrid	$⊢ (M \in ℝ \land N \in ℝ) \to ((- M \in ℕ_{0} \land - N \in ℕ_{0}) \to M \cdot N \in ℕ_{0})$
30		orc	$⊢ M \cdot N \in ℕ_{0} \to (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0})$
31	29 30	syl6	$⊢ (M \in ℝ \land N \in ℝ) \to ((- M \in ℕ_{0} \land - N \in ℕ_{0}) \to (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0}))$
32	31 6	jctild	$⊢ (M \in ℝ \land N \in ℝ) \to ((- M \in ℕ_{0} \land - N \in ℕ_{0}) \to (M \cdot N \in ℝ \land (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0})))$
33	7 17 24 32	ccased	$⊢ (M \in ℝ \land N \in ℝ) \to (((M \in ℕ_{0} \lor - M \in ℕ_{0}) \land (N \in ℕ_{0} \lor - N \in ℕ_{0})) \to (M \cdot N \in ℝ \land (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0})))$
34		elznn0	$⊢ M \cdot N \in ℤ \leftrightarrow (M \cdot N \in ℝ \land (M \cdot N \in ℕ_{0} \lor - M \cdot N \in ℕ_{0}))$
35	33 34	syl6ibr	$⊢ (M \in ℝ \land N \in ℝ) \to (((M \in ℕ_{0} \lor - M \in ℕ_{0}) \land (N \in ℕ_{0} \lor - N \in ℕ_{0})) \to M \cdot N \in ℤ)$
36	35	imp	$⊢ ((M \in ℝ \land N \in ℝ) \land ((M \in ℕ_{0} \lor - M \in ℕ_{0}) \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))) \to M \cdot N \in ℤ$
37	36	an4s	$⊢ ((M \in ℝ \land (M \in ℕ_{0} \lor - M \in ℕ_{0})) \land (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))) \to M \cdot N \in ℤ$
38	1 2 37	syl2anb	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$

Metamath Proof Explorer

Theorem zmulcl

Proof