Proof of Theorem elfzmlbp
| Step | Hyp | Ref
| Expression |
| 1 | | elfz2 13554 |
. . . 4
⊢ (𝐾 ∈ (𝑀...(𝑀 + 𝑁)) ↔ ((𝑀 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)))) |
| 2 | | znn0sub 12664 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ≤ 𝐾 ↔ (𝐾 − 𝑀) ∈
ℕ0)) |
| 3 | 2 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝐾 ↔ (𝐾 − 𝑀) ∈
ℕ0)) |
| 4 | 3 | biimpcd 249 |
. . . . . . . . . . . 12
⊢ (𝑀 ≤ 𝐾 → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 − 𝑀) ∈
ℕ0)) |
| 5 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 − 𝑀) ∈
ℕ0)) |
| 6 | 5 | impcom 407 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → (𝐾 − 𝑀) ∈
ℕ0) |
| 7 | | zre 12617 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
| 8 | 7 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝑀 ∈
ℝ) |
| 9 | 8 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℝ) |
| 10 | | zre 12617 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
| 11 | 10 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝐾 ∈
ℝ) |
| 12 | 11 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → 𝐾 ∈
ℝ) |
| 13 | | zaddcl 12657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
| 14 | 13 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ) |
| 15 | 14 | zred 12722 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℝ) |
| 16 | | letr 11355 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ (𝑀 + 𝑁) ∈ ℝ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → 𝑀 ≤ (𝑀 + 𝑁))) |
| 17 | 9, 12, 15, 16 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → 𝑀 ≤ (𝑀 + 𝑁))) |
| 18 | | zre 12617 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
| 19 | | addge01 11773 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 ≤
𝑁 ↔ 𝑀 ≤ (𝑀 + 𝑁))) |
| 20 | 8, 18, 19 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (0 ≤
𝑁 ↔ 𝑀 ≤ (𝑀 + 𝑁))) |
| 21 | | elnn0z 12626 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℤ
∧ 0 ≤ 𝑁)) |
| 22 | 21 | simplbi2 500 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → (0 ≤
𝑁 → 𝑁 ∈
ℕ0)) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (0 ≤
𝑁 → 𝑁 ∈
ℕ0)) |
| 24 | 20, 23 | sylbird 260 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ (𝑀 + 𝑁) → 𝑁 ∈
ℕ0)) |
| 25 | 17, 24 | syld 47 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → 𝑁 ∈
ℕ0)) |
| 26 | 25 | imp 406 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → 𝑁 ∈
ℕ0) |
| 27 | | df-3an 1089 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈
ℤ)) |
| 28 | | 3ancoma 1098 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ)) |
| 29 | 27, 28 | bitr3i 277 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) ↔ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈
ℤ)) |
| 30 | 10, 7, 18 | 3anim123i 1152 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
| 31 | 29, 30 | sylbi 217 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
| 32 | | lesubadd2 11736 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝐾 − 𝑀) ≤ 𝑁 ↔ 𝐾 ≤ (𝑀 + 𝑁))) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → ((𝐾 − 𝑀) ≤ 𝑁 ↔ 𝐾 ≤ (𝑀 + 𝑁))) |
| 34 | 33 | biimprcd 250 |
. . . . . . . . . . . 12
⊢ (𝐾 ≤ (𝑀 + 𝑁) → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 − 𝑀) ≤ 𝑁)) |
| 35 | 34 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 − 𝑀) ≤ 𝑁)) |
| 36 | 35 | impcom 407 |
. . . . . . . . . 10
⊢ ((((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → (𝐾 − 𝑀) ≤ 𝑁) |
| 37 | 6, 26, 36 | 3jca 1129 |
. . . . . . . . 9
⊢ ((((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)) |
| 38 | 37 | exp31 419 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 ∈ ℤ → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)))) |
| 39 | 38 | com23 86 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → (𝑁 ∈ ℤ → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)))) |
| 40 | 39 | 3adant2 1132 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁)) → (𝑁 ∈ ℤ → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)))) |
| 41 | 40 | imp 406 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → (𝑁 ∈ ℤ → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁))) |
| 42 | 41 | com12 32 |
. . . 4
⊢ (𝑁 ∈ ℤ → (((𝑀 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ (𝑀 + 𝑁))) → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁))) |
| 43 | 1, 42 | biimtrid 242 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝐾 ∈ (𝑀...(𝑀 + 𝑁)) → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁))) |
| 44 | 43 | imp 406 |
. 2
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ (𝑀...(𝑀 + 𝑁))) → ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)) |
| 45 | | elfz2nn0 13658 |
. 2
⊢ ((𝐾 − 𝑀) ∈ (0...𝑁) ↔ ((𝐾 − 𝑀) ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ (𝐾 − 𝑀) ≤ 𝑁)) |
| 46 | 44, 45 | sylibr 234 |
1
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ (𝑀...(𝑀 + 𝑁))) → (𝐾 − 𝑀) ∈ (0...𝑁)) |