fzmul

Description: Membership of a product in a finite interval of integers. (Contributed by Jeff Madsen, 17-Jun-2010)

		Ref	Expression
	Assertion	fzmul	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℕ) \to (J \in (M \dots N) \to K \cdot J \in (K \cdot M \dots K \cdot N))$

Proof

Step	Hyp	Ref	Expression
1		elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (J \in (M \dots N) \leftrightarrow (J \in ℤ \land M \leq J \land J \leq N))$
2	1	3adant3	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℕ) \to (J \in (M \dots N) \leftrightarrow (J \in ℤ \land M \leq J \land J \leq N))$
3		zre	$⊢ M \in ℤ \to M \in ℝ$
4		zre	$⊢ J \in ℤ \to J \in ℝ$
5		nnre	$⊢ K \in ℕ \to K \in ℝ$
6		nngt0	$⊢ K \in ℕ \to 0 < K$
7	5 6	jca	$⊢ K \in ℕ \to (K \in ℝ \land 0 < K)$
8		lemul2	$⊢ (M \in ℝ \land J \in ℝ \land (K \in ℝ \land 0 < K)) \to (M \leq J \leftrightarrow K \cdot M \leq K \cdot J)$
9	3 4 7 8	syl3an	$⊢ (M \in ℤ \land J \in ℤ \land K \in ℕ) \to (M \leq J \leftrightarrow K \cdot M \leq K \cdot J)$
10	9	3expa	$⊢ ((M \in ℤ \land J \in ℤ) \land K \in ℕ) \to (M \leq J \leftrightarrow K \cdot M \leq K \cdot J)$
11	10	biimpd	$⊢ ((M \in ℤ \land J \in ℤ) \land K \in ℕ) \to (M \leq J \to K \cdot M \leq K \cdot J)$
12	11	adantllr	$⊢ (((M \in ℤ \land N \in ℤ) \land J \in ℤ) \land K \in ℕ) \to (M \leq J \to K \cdot M \leq K \cdot J)$
13		zre	$⊢ N \in ℤ \to N \in ℝ$
14		lemul2	$⊢ (J \in ℝ \land N \in ℝ \land (K \in ℝ \land 0 < K)) \to (J \leq N \leftrightarrow K \cdot J \leq K \cdot N)$
15	4 13 7 14	syl3an	$⊢ (J \in ℤ \land N \in ℤ \land K \in ℕ) \to (J \leq N \leftrightarrow K \cdot J \leq K \cdot N)$
16	15	3expa	$⊢ ((J \in ℤ \land N \in ℤ) \land K \in ℕ) \to (J \leq N \leftrightarrow K \cdot J \leq K \cdot N)$
17	16	ancom1s	$⊢ ((N \in ℤ \land J \in ℤ) \land K \in ℕ) \to (J \leq N \leftrightarrow K \cdot J \leq K \cdot N)$
18	17	biimpd	$⊢ ((N \in ℤ \land J \in ℤ) \land K \in ℕ) \to (J \leq N \to K \cdot J \leq K \cdot N)$
19	18	adantlll	$⊢ (((M \in ℤ \land N \in ℤ) \land J \in ℤ) \land K \in ℕ) \to (J \leq N \to K \cdot J \leq K \cdot N)$
20	12 19	anim12d	$⊢ (((M \in ℤ \land N \in ℤ) \land J \in ℤ) \land K \in ℕ) \to ((M \leq J \land J \leq N) \to (K \cdot M \leq K \cdot J \land K \cdot J \leq K \cdot N))$
21		zmulcl	$⊢ (K \in ℤ \land M \in ℤ) \to K \cdot M \in ℤ$
22	21	ex	$⊢ K \in ℤ \to (M \in ℤ \to K \cdot M \in ℤ)$
23		zmulcl	$⊢ (K \in ℤ \land N \in ℤ) \to K \cdot N \in ℤ$
24	23	ex	$⊢ K \in ℤ \to (N \in ℤ \to K \cdot N \in ℤ)$
25		zmulcl	$⊢ (K \in ℤ \land J \in ℤ) \to K \cdot J \in ℤ$
26	25	ex	$⊢ K \in ℤ \to (J \in ℤ \to K \cdot J \in ℤ)$
27	22 24 26	3anim123d	$⊢ K \in ℤ \to ((M \in ℤ \land N \in ℤ \land J \in ℤ) \to (K \cdot M \in ℤ \land K \cdot N \in ℤ \land K \cdot J \in ℤ))$
28		elfz	$⊢ (K \cdot J \in ℤ \land K \cdot M \in ℤ \land K \cdot N \in ℤ) \to (K \cdot J \in (K \cdot M \dots K \cdot N) \leftrightarrow (K \cdot M \leq K \cdot J \land K \cdot J \leq K \cdot N))$
29	28	3coml	$⊢ (K \cdot M \in ℤ \land K \cdot N \in ℤ \land K \cdot J \in ℤ) \to (K \cdot J \in (K \cdot M \dots K \cdot N) \leftrightarrow (K \cdot M \leq K \cdot J \land K \cdot J \leq K \cdot N))$
30	27 29	syl6	$⊢ K \in ℤ \to ((M \in ℤ \land N \in ℤ \land J \in ℤ) \to (K \cdot J \in (K \cdot M \dots K \cdot N) \leftrightarrow (K \cdot M \leq K \cdot J \land K \cdot J \leq K \cdot N)))$
31		nnz	$⊢ K \in ℕ \to K \in ℤ$
32	30 31	syl11	$⊢ (M \in ℤ \land N \in ℤ \land J \in ℤ) \to (K \in ℕ \to (K \cdot J \in (K \cdot M \dots K \cdot N) \leftrightarrow (K \cdot M \leq K \cdot J \land K \cdot J \leq K \cdot N)))$
33	32	3expa	$⊢ ((M \in ℤ \land N \in ℤ) \land J \in ℤ) \to (K \in ℕ \to (K \cdot J \in (K \cdot M \dots K \cdot N) \leftrightarrow (K \cdot M \leq K \cdot J \land K \cdot J \leq K \cdot N)))$
34	33	imp	$⊢ (((M \in ℤ \land N \in ℤ) \land J \in ℤ) \land K \in ℕ) \to (K \cdot J \in (K \cdot M \dots K \cdot N) \leftrightarrow (K \cdot M \leq K \cdot J \land K \cdot J \leq K \cdot N))$
35	20 34	sylibrd	$⊢ (((M \in ℤ \land N \in ℤ) \land J \in ℤ) \land K \in ℕ) \to ((M \leq J \land J \leq N) \to K \cdot J \in (K \cdot M \dots K \cdot N))$
36	35	an32s	$⊢ (((M \in ℤ \land N \in ℤ) \land K \in ℕ) \land J \in ℤ) \to ((M \leq J \land J \leq N) \to K \cdot J \in (K \cdot M \dots K \cdot N))$
37	36	exp4b	$⊢ ((M \in ℤ \land N \in ℤ) \land K \in ℕ) \to (J \in ℤ \to (M \leq J \to (J \leq N \to K \cdot J \in (K \cdot M \dots K \cdot N))))$
38	37	3impd	$⊢ ((M \in ℤ \land N \in ℤ) \land K \in ℕ) \to ((J \in ℤ \land M \leq J \land J \leq N) \to K \cdot J \in (K \cdot M \dots K \cdot N))$
39	38	3impa	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℕ) \to ((J \in ℤ \land M \leq J \land J \leq N) \to K \cdot J \in (K \cdot M \dots K \cdot N))$
40	2 39	sylbid	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℕ) \to (J \in (M \dots N) \to K \cdot J \in (K \cdot M \dots K \cdot N))$

Metamath Proof Explorer

Theorem fzmul

Proof