Theorem fzmul

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

	Ref	Expression
Assertion	fzmul	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfz1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) )
2	1	3adant3	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) ) )
3		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
4		zre	⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ )
5		nnre	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ )
6		nngt0	⊢ ( 𝐾 ∈ ℕ → 0 < 𝐾 )
7	5 6	jca	⊢ ( 𝐾 ∈ ℕ → ( 𝐾 ∈ ℝ ∧ 0 < 𝐾 ) )
8		lemul2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ ( 𝐾 ∈ ℝ ∧ 0 < 𝐾 ) ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ) )
9	3 4 7 8	syl3an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℕ ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ) )
10	9	3expa	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( 𝑀 ≤ 𝐽 ↔ ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ) )
11	10	biimpd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( 𝑀 ≤ 𝐽 → ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ) )
12	11	adantllr	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐽 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( 𝑀 ≤ 𝐽 → ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ) )
13		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
14		lemul2	⊢ ( ( 𝐽 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝐾 ∈ ℝ ∧ 0 < 𝐾 ) ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) )
15	4 13 7 14	syl3an	⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) )
16	15	3expa	⊢ ( ( ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) )
17	16	ancom1s	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( 𝐽 ≤ 𝑁 ↔ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) )
18	17	biimpd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( 𝐽 ≤ 𝑁 → ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) )
19	18	adantlll	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐽 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( 𝐽 ≤ 𝑁 → ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) )
20	12 19	anim12d	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐽 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( ( 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) → ( ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ∧ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) ) )
21		zmulcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 · 𝑀 ) ∈ ℤ )
22	21	ex	⊢ ( 𝐾 ∈ ℤ → ( 𝑀 ∈ ℤ → ( 𝐾 · 𝑀 ) ∈ ℤ ) )
23		zmulcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
24	23	ex	⊢ ( 𝐾 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 𝐾 · 𝑁 ) ∈ ℤ ) )
25		zmulcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐾 · 𝐽 ) ∈ ℤ )
26	25	ex	⊢ ( 𝐾 ∈ ℤ → ( 𝐽 ∈ ℤ → ( 𝐾 · 𝐽 ) ∈ ℤ ) )
27	22 24 26	3anim123d	⊢ ( 𝐾 ∈ ℤ → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ∧ ( 𝐾 · 𝐽 ) ∈ ℤ ) ) )
28		elfz	⊢ ( ( ( 𝐾 · 𝐽 ) ∈ ℤ ∧ ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) → ( ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ↔ ( ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ∧ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) ) )
29	28	3coml	⊢ ( ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ∧ ( 𝐾 · 𝐽 ) ∈ ℤ ) → ( ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ↔ ( ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ∧ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) ) )
30	27 29	syl6	⊢ ( 𝐾 ∈ ℤ → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ↔ ( ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ∧ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) ) ) )
31		nnz	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
32	30 31	syl11	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐾 ∈ ℕ → ( ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ↔ ( ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ∧ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) ) ) )
33	32	3expa	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐽 ∈ ℤ ) → ( 𝐾 ∈ ℕ → ( ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ↔ ( ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ∧ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) ) ) )
34	33	imp	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐽 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ↔ ( ( 𝐾 · 𝑀 ) ≤ ( 𝐾 · 𝐽 ) ∧ ( 𝐾 · 𝐽 ) ≤ ( 𝐾 · 𝑁 ) ) ) )
35	20 34	sylibrd	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐽 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( ( 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) → ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ) )
36	35	an32s	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) ∧ 𝐽 ∈ ℤ ) → ( ( 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) → ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ) )
37	36	exp4b	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( 𝐽 ∈ ℤ → ( 𝑀 ≤ 𝐽 → ( 𝐽 ≤ 𝑁 → ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ) ) ) )
38	37	3impd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℕ ) → ( ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) → ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ) )
39	38	3impa	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ ) → ( ( 𝐽 ∈ ℤ ∧ 𝑀 ≤ 𝐽 ∧ 𝐽 ≤ 𝑁 ) → ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ) )
40	2 39	sylbid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ) )