Proof of Theorem elfzmlbp
Step | Hyp | Ref
| Expression |
1 | | elfz2 9972 |
. . . 4
⊢ (𝐾 ∈ (𝑀...(𝑀 + 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)))) |
2 | | znn0sub 9277 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ≤ 𝐾 ↔ (𝐾 − 𝑀) ∈
ℕ0)) |
3 | 2 | adantr 274 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝐾 ↔ (𝐾 − 𝑀) ∈
ℕ0)) |
4 | 3 | biimpcd 158 |
. . . . . . . . . . . 12
⊢ (𝑀 ≤ 𝐾 → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 − 𝑀) ∈
ℕ0)) |
5 | 4 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 − 𝑀) ∈
ℕ0)) |
6 | 5 | impcom 124 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → (𝐾 − 𝑀) ∈
ℕ0) |
7 | | zre 9216 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
8 | 7 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝑀 ∈
ℝ) |
9 | 8 | adantr 274 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℝ) |
10 | | zre 9216 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
11 | 10 | adantl 275 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝐾 ∈
ℝ) |
12 | 11 | adantr 274 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → 𝐾 ∈
ℝ) |
13 | | zaddcl 9252 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
14 | 13 | adantlr 474 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
15 | 14 | zred 9334 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℝ) |
16 | | letr 8002 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ (𝑀 + 𝑁) ∈ ℝ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → 𝑀 ≤ (𝑀 + 𝑁))) |
17 | 9, 12, 15, 16 | syl3anc 1233 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → 𝑀 ≤ (𝑀 + 𝑁))) |
18 | | zre 9216 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
19 | | addge01 8391 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤
𝑁 ↔ 𝑀 ≤ (𝑀 + 𝑁))) |
20 | 8, 18, 19 | syl2an 287 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (0 ≤
𝑁 ↔ 𝑀 ≤ (𝑀 + 𝑁))) |
21 | | elnn0z 9225 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℤ
∧ 0 ≤ 𝑁)) |
22 | 21 | simplbi2 383 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → (0 ≤
𝑁 → 𝑁 ∈
ℕ0)) |
23 | 22 | adantl 275 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (0 ≤
𝑁 → 𝑁 ∈
ℕ0)) |
24 | 20, 23 | sylbird 169 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ (𝑀 + 𝑁) → 𝑁 ∈
ℕ0)) |
25 | 17, 24 | syld 45 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → 𝑁 ∈
ℕ0)) |
26 | 25 | imp 123 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → 𝑁 ∈
ℕ0) |
27 | | df-3an 975 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈
ℤ)) |
28 | | 3ancoma 980 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ)) |
29 | 27, 28 | bitr3i 185 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ)) |
30 | 10, 7, 18 | 3anim123i 1179 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
31 | 29, 30 | sylbi 120 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
32 | | lesubadd2 8354 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝐾 − 𝑀) ≤ 𝑁 ↔ 𝐾 ≤ (𝑀 + 𝑁))) |
33 | 31, 32 | syl 14 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝐾 − 𝑀) ≤ 𝑁 ↔ 𝐾 ≤ (𝑀 + 𝑁))) |
34 | 33 | biimprcd 159 |
. . . . . . . . . . . 12
⊢ (𝐾 ≤ (𝑀 + 𝑁) → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 − 𝑀) ≤ 𝑁)) |
35 | 34 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 − 𝑀) ≤ 𝑁)) |
36 | 35 | impcom 124 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → (𝐾 − 𝑀) ≤ 𝑁) |
37 | 6, 26, 36 | 3jca 1172 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)) |
38 | 37 | exp31 362 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 ∈ ℤ → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)))) |
39 | 38 | com23 78 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → (𝑁 ∈ ℤ → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)))) |
40 | 39 | 3adant2 1011 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → (𝑁 ∈ ℤ → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)))) |
41 | 40 | imp 123 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → (𝑁 ∈ ℤ → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁))) |
42 | 41 | com12 30 |
. . . 4
⊢ (𝑁 ∈ ℤ → (((𝑀 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁))) |
43 | 1, 42 | syl5bi 151 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (𝑀...(𝑀 + 𝑁)) → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁))) |
44 | 43 | imp 123 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ (𝑀...(𝑀 + 𝑁))) → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)) |
45 | | elfz2nn0 10068 |
. 2
⊢ ((𝐾 − 𝑀) ∈ (0...𝑁) ↔ ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)) |
46 | 44, 45 | sylibr 133 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ (𝑀...(𝑀 + 𝑁))) → (𝐾 − 𝑀) ∈ (0...𝑁)) |