Metamath Proof Explorer


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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℕ ) → ( 𝐽 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 · 𝐽 ) ∈ ( ( 𝐾 · 𝑀 ) ... ( 𝐾 · 𝑁 ) ) ) )