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