| Step | Hyp | Ref
| Expression |
| 1 | | ovexd 7466 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ∈ V) |
| 2 | | ovexd 7466 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ∈ V) |
| 3 | | elfz1 13552 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
| 4 | 3 | biimpd 229 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
| 5 | 4 | 3adant3 1133 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))) |
| 6 | | zaddcl 12657 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ℤ) |
| 7 | 6 | expcom 413 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (𝑘 ∈ ℤ → (𝑘 + 𝐾) ∈ ℤ)) |
| 8 | 7 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → (𝑘 + 𝐾) ∈ ℤ)) |
| 9 | 8 | adantrd 491 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑘 + 𝐾) ∈ ℤ)) |
| 10 | | zre 12617 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
| 11 | | zre 12617 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℝ) |
| 12 | | zre 12617 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
| 13 | | leadd1 11731 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑀 ≤ 𝑘 ↔ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾))) |
| 14 | 10, 11, 12, 13 | syl3an 1161 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ≤ 𝑘 ↔ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾))) |
| 15 | 14 | biimpd 229 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ≤ 𝑘 → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾))) |
| 16 | 15 | adantrd 491 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾))) |
| 17 | 16 | 3com23 1127 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾))) |
| 18 | 17 | 3expia 1122 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾)))) |
| 19 | 18 | impd 410 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾))) |
| 20 | 19 | 3adant2 1132 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑀 + 𝐾) ≤ (𝑘 + 𝐾))) |
| 21 | | zre 12617 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
| 22 | | leadd1 11731 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑘 ≤ 𝑁 ↔ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))) |
| 23 | 11, 21, 12, 22 | syl3an 1161 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ≤ 𝑁 ↔ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))) |
| 24 | 23 | biimpd 229 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ≤ 𝑁 → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))) |
| 25 | 24 | adantld 490 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))) |
| 26 | 25 | 3coml 1128 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))) |
| 27 | 26 | 3expia 1122 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ ℤ → ((𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))) |
| 28 | 27 | impd 410 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))) |
| 29 | 28 | 3adant1 1131 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → (𝑘 + 𝐾) ≤ (𝑁 + 𝐾))) |
| 30 | 9, 20, 29 | 3jcad 1130 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))) |
| 31 | | zaddcl 12657 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ) |
| 32 | 31 | 3adant2 1132 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 𝐾) ∈ ℤ) |
| 33 | | zaddcl 12657 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ) |
| 34 | 33 | 3adant1 1131 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 + 𝐾) ∈ ℤ) |
| 35 | | elfz1 13552 |
. . . . . . . 8
⊢ (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → ((𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))) |
| 36 | 32, 34, 35 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ ((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)))) |
| 37 | 36 | biimprd 248 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (((𝑘 + 𝐾) ∈ ℤ ∧ (𝑀 + 𝐾) ≤ (𝑘 + 𝐾) ∧ (𝑘 + 𝐾) ≤ (𝑁 + 𝐾)) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) |
| 38 | 30, 37 | syldc 48 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) |
| 39 | 38 | 3impb 1115 |
. . . 4
⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) |
| 40 | 39 | com12 32 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) |
| 41 | 5, 40 | syld 47 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 𝐾) ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)))) |
| 42 | | elfz1 13552 |
. . . . 5
⊢ (((𝑀 + 𝐾) ∈ ℤ ∧ (𝑁 + 𝐾) ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)))) |
| 43 | 32, 34, 42 | syl2anc 584 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↔ (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)))) |
| 44 | 43 | biimpd 229 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)))) |
| 45 | | zsubcl 12659 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 − 𝐾) ∈ ℤ) |
| 46 | 45 | expcom 413 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (𝑚 ∈ ℤ → (𝑚 − 𝐾) ∈ ℤ)) |
| 47 | 46 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ℤ → (𝑚 − 𝐾) ∈ ℤ)) |
| 48 | 47 | adantrd 491 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → (𝑚 − 𝐾) ∈ ℤ)) |
| 49 | | zre 12617 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℝ) |
| 50 | | leaddsub 11739 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑚 ∈ ℝ) → ((𝑀 + 𝐾) ≤ 𝑚 ↔ 𝑀 ≤ (𝑚 − 𝐾))) |
| 51 | 10, 12, 49, 50 | syl3an 1161 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑀 + 𝐾) ≤ 𝑚 ↔ 𝑀 ≤ (𝑚 − 𝐾))) |
| 52 | 51 | biimpd 229 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → ((𝑀 + 𝐾) ≤ 𝑚 → 𝑀 ≤ (𝑚 − 𝐾))) |
| 53 | 52 | adantrd 491 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → 𝑀 ≤ (𝑚 − 𝐾))) |
| 54 | 53 | 3expia 1122 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ℤ → (((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → 𝑀 ≤ (𝑚 − 𝐾)))) |
| 55 | 54 | impd 410 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → 𝑀 ≤ (𝑚 − 𝐾))) |
| 56 | 55 | 3adant2 1132 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → 𝑀 ≤ (𝑚 − 𝐾))) |
| 57 | | lesubadd 11735 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑚 − 𝐾) ≤ 𝑁 ↔ 𝑚 ≤ (𝑁 + 𝐾))) |
| 58 | 49, 12, 21, 57 | syl3an 1161 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚 − 𝐾) ≤ 𝑁 ↔ 𝑚 ≤ (𝑁 + 𝐾))) |
| 59 | 58 | biimprd 248 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 ≤ (𝑁 + 𝐾) → (𝑚 − 𝐾) ≤ 𝑁)) |
| 60 | 59 | adantld 490 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → (𝑚 − 𝐾) ≤ 𝑁)) |
| 61 | 60 | 3coml 1128 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → (𝑚 − 𝐾) ≤ 𝑁)) |
| 62 | 61 | 3expia 1122 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 ∈ ℤ → (((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → (𝑚 − 𝐾) ≤ 𝑁))) |
| 63 | 62 | impd 410 |
. . . . . . . . 9
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → (𝑚 − 𝐾) ≤ 𝑁)) |
| 64 | 63 | ancoms 458 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → (𝑚 − 𝐾) ≤ 𝑁)) |
| 65 | 64 | 3adant1 1131 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → (𝑚 − 𝐾) ≤ 𝑁)) |
| 66 | 48, 56, 65 | 3jcad 1130 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → ((𝑚 − 𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚 − 𝐾) ∧ (𝑚 − 𝐾) ≤ 𝑁))) |
| 67 | | elfz1 13552 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑚 − 𝐾) ∈ (𝑀...𝑁) ↔ ((𝑚 − 𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚 − 𝐾) ∧ (𝑚 − 𝐾) ≤ 𝑁))) |
| 68 | 67 | biimprd 248 |
. . . . . . 7
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑚 − 𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚 − 𝐾) ∧ (𝑚 − 𝐾) ≤ 𝑁) → (𝑚 − 𝐾) ∈ (𝑀...𝑁))) |
| 69 | 68 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (((𝑚 − 𝐾) ∈ ℤ ∧ 𝑀 ≤ (𝑚 − 𝐾) ∧ (𝑚 − 𝐾) ≤ 𝑁) → (𝑚 − 𝐾) ∈ (𝑀...𝑁))) |
| 70 | 66, 69 | syldc 48 |
. . . . 5
⊢ ((𝑚 ∈ ℤ ∧ ((𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 − 𝐾) ∈ (𝑀...𝑁))) |
| 71 | 70 | 3impb 1115 |
. . . 4
⊢ ((𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 − 𝐾) ∈ (𝑀...𝑁))) |
| 72 | 71 | com12 32 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾)) → (𝑚 − 𝐾) ∈ (𝑀...𝑁))) |
| 73 | 44, 72 | syld 47 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → (𝑚 − 𝐾) ∈ (𝑀...𝑁))) |
| 74 | 5 | imp 406 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)) |
| 75 | 74 | simp1d 1143 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ ℤ) |
| 76 | 75 | ex 412 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ)) |
| 77 | 44 | imp 406 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → (𝑚 ∈ ℤ ∧ (𝑀 + 𝐾) ≤ 𝑚 ∧ 𝑚 ≤ (𝑁 + 𝐾))) |
| 78 | 77 | simp1d 1143 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → 𝑚 ∈ ℤ) |
| 79 | 78 | ex 412 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) → 𝑚 ∈ ℤ)) |
| 80 | | zcn 12618 |
. . . . . . 7
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
ℂ) |
| 81 | | zcn 12618 |
. . . . . . 7
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
| 82 | | zcn 12618 |
. . . . . . 7
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℂ) |
| 83 | | subadd 11511 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑚 − 𝐾) = 𝑘 ↔ (𝐾 + 𝑘) = 𝑚)) |
| 84 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝑚 − 𝐾) = 𝑘 ↔ 𝑘 = (𝑚 − 𝐾)) |
| 85 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝐾 + 𝑘) = 𝑚 ↔ 𝑚 = (𝐾 + 𝑘)) |
| 86 | 83, 84, 85 | 3bitr3g 313 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝐾 + 𝑘))) |
| 87 | | addcom 11447 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐾 + 𝑘) = (𝑘 + 𝐾)) |
| 88 | 87 | 3adant1 1131 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐾 + 𝑘) = (𝑘 + 𝐾)) |
| 89 | 88 | eqeq2d 2748 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑚 = (𝐾 + 𝑘) ↔ 𝑚 = (𝑘 + 𝐾))) |
| 90 | 86, 89 | bitrd 279 |
. . . . . . 7
⊢ ((𝑚 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾))) |
| 91 | 80, 81, 82, 90 | syl3an 1161 |
. . . . . 6
⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾))) |
| 92 | 91 | 3coml 1128 |
. . . . 5
⊢ ((𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾))) |
| 93 | 92 | 3expib 1123 |
. . . 4
⊢ (𝐾 ∈ ℤ → ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))) |
| 94 | 93 | 3ad2ant3 1136 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))) |
| 95 | 76, 79, 94 | syl2and 608 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑚 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) → (𝑘 = (𝑚 − 𝐾) ↔ 𝑚 = (𝑘 + 𝐾)))) |
| 96 | 1, 2, 41, 73, 95 | en3d 9029 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀...𝑁) ≈ ((𝑀 + 𝐾)...(𝑁 + 𝐾))) |