Proof of Theorem elfzelfzlble
Step | Hyp | Ref
| Expression |
1 | | elfz2 13102 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤
𝐾 ∧ 𝐾 ≤ 𝑁))) |
2 | | 3simpc 1152 |
. . . . . . . 8
⊢ ((0
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 𝐾
∈ ℤ) → (𝑁
∈ ℤ ∧ 𝐾
∈ ℤ)) |
3 | 2 | adantr 484 |
. . . . . . 7
⊢ (((0
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 𝐾
∈ ℤ) ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) |
4 | 1, 3 | sylbi 220 |
. . . . . 6
⊢ (𝐾 ∈ (0...𝑁) → (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) |
5 | 4 | anim2i 620 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁)) → (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ))) |
6 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝑁 ∈
ℤ) |
7 | 6 | anim2i 620 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ)) |
8 | 7 | ancomd 465 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝑁 ∈ ℤ ∧ 𝑀 ∈
ℤ)) |
9 | | zsubcl 12219 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 − 𝑀) ∈ ℤ) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝑁 − 𝑀) ∈ ℤ) |
11 | 6 | adantl 485 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝑁 ∈
ℤ) |
12 | | simprr 773 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐾 ∈
ℤ) |
13 | 10, 11, 12 | 3jca 1130 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → ((𝑁 − 𝑀) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) |
14 | 5, 13 | syl 17 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁)) → ((𝑁 − 𝑀) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) |
15 | 14 | 3adant3 1134 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑁 < (𝑀 + 𝐾)) → ((𝑁 − 𝑀) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) |
16 | | elfzel2 13110 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ ℤ) |
17 | 16 | zred 12282 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → 𝑁 ∈ ℝ) |
18 | 17 | adantl 485 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁)) → 𝑁 ∈ ℝ) |
19 | | zre 12180 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
20 | 19 | adantr 484 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁)) → 𝑀 ∈ ℝ) |
21 | | elfzelz 13112 |
. . . . . . . 8
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ) |
22 | 21 | zred 12282 |
. . . . . . 7
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℝ) |
23 | 22 | adantl 485 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁)) → 𝐾 ∈ ℝ) |
24 | 18, 20, 23 | 3jca 1130 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ)) |
25 | | simp1 1138 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ) → 𝑁 ∈
ℝ) |
26 | | readdcl 10812 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑀 + 𝐾) ∈ ℝ) |
27 | 26 | 3adant1 1132 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑀 + 𝐾) ∈ ℝ) |
28 | | ltle 10921 |
. . . . . . 7
⊢ ((𝑁 ∈ ℝ ∧ (𝑀 + 𝐾) ∈ ℝ) → (𝑁 < (𝑀 + 𝐾) → 𝑁 ≤ (𝑀 + 𝐾))) |
29 | 25, 27, 28 | syl2anc 587 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑁 < (𝑀 + 𝐾) → 𝑁 ≤ (𝑀 + 𝐾))) |
30 | | lesubadd2 11305 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑁 − 𝑀) ≤ 𝐾 ↔ 𝑁 ≤ (𝑀 + 𝐾))) |
31 | 29, 30 | sylibrd 262 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑁 < (𝑀 + 𝐾) → (𝑁 − 𝑀) ≤ 𝐾)) |
32 | 24, 31 | syl 17 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 < (𝑀 + 𝐾) → (𝑁 − 𝑀) ≤ 𝐾)) |
33 | 32 | 3impia 1119 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑁 < (𝑀 + 𝐾)) → (𝑁 − 𝑀) ≤ 𝐾) |
34 | | elfzle2 13116 |
. . . 4
⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ≤ 𝑁) |
35 | 34 | 3ad2ant2 1136 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑁 < (𝑀 + 𝐾)) → 𝐾 ≤ 𝑁) |
36 | 15, 33, 35 | jca32 519 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑁 < (𝑀 + 𝐾)) → (((𝑁 − 𝑀) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ ((𝑁 − 𝑀) ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
37 | | elfz2 13102 |
. 2
⊢ (𝐾 ∈ ((𝑁 − 𝑀)...𝑁) ↔ (((𝑁 − 𝑀) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ ((𝑁 − 𝑀) ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) |
38 | 36, 37 | sylibr 237 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑁 < (𝑀 + 𝐾)) → 𝐾 ∈ ((𝑁 − 𝑀)...𝑁)) |