Proof of Theorem elfzolborelfzop1
| Step | Hyp | Ref
| Expression |
| 1 | | elfzo2 13702 |
. 2
⊢ (𝐾 ∈ (𝑀..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁)) |
| 2 | | eluz2 12884 |
. . . 4
⊢ (𝐾 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾)) |
| 3 | | zre 12617 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
| 4 | | zre 12617 |
. . . . . . 7
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
| 5 | | leloe 11347 |
. . . . . . 7
⊢ ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ) → (𝑀 ≤ 𝐾 ↔ (𝑀 < 𝐾 ∨ 𝑀 = 𝐾))) |
| 6 | 3, 4, 5 | syl2an 596 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ≤ 𝐾 ↔ (𝑀 < 𝐾 ∨ 𝑀 = 𝐾))) |
| 7 | | peano2z 12658 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈
ℤ) |
| 8 | 7 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 + 1) ∈
ℤ) |
| 9 | 8 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) → (𝑀 + 1) ∈ ℤ) |
| 10 | | simprlr 780 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) → 𝐾 ∈ ℤ) |
| 11 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) → 𝑀 < 𝐾) |
| 12 | | zltp1le 12667 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 < 𝐾 ↔ (𝑀 + 1) ≤ 𝐾)) |
| 13 | 12 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) → (𝑀 < 𝐾 ↔ (𝑀 + 1) ≤ 𝐾)) |
| 14 | 11, 13 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) → (𝑀 + 1) ≤ 𝐾) |
| 15 | 9, 10, 14 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ ((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) → ((𝑀 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝐾)) |
| 16 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) ∧ 𝐾 < 𝑁) → ((𝑀 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝐾)) |
| 17 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ (((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) ∧ 𝐾 < 𝑁) → 𝑁 ∈ ℤ) |
| 18 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) ∧ 𝐾 < 𝑁) → 𝐾 < 𝑁) |
| 19 | | elfzo2 13702 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ((𝑀 + 1)..^𝑁) ↔ (𝐾 ∈ (ℤ≥‘(𝑀 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁)) |
| 20 | | eluz2 12884 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈
(ℤ≥‘(𝑀 + 1)) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝐾)) |
| 21 | 20 | 3anbi1i 1158 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝐾) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁)) |
| 22 | 19, 21 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ((𝑀 + 1)..^𝑁) ↔ (((𝑀 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝐾) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁)) |
| 23 | 16, 17, 18, 22 | syl3anbrc 1344 |
. . . . . . . . . . 11
⊢ (((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) ∧ 𝐾 < 𝑁) → 𝐾 ∈ ((𝑀 + 1)..^𝑁)) |
| 24 | 23 | olcd 875 |
. . . . . . . . . 10
⊢ (((𝑀 < 𝐾 ∧ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ)) ∧ 𝐾 < 𝑁) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))) |
| 25 | 24 | exp31 419 |
. . . . . . . . 9
⊢ (𝑀 < 𝐾 → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))))) |
| 26 | | orc 868 |
. . . . . . . . . . 11
⊢ (𝐾 = 𝑀 → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))) |
| 27 | 26 | eqcoms 2745 |
. . . . . . . . . 10
⊢ (𝑀 = 𝐾 → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))) |
| 28 | 27 | 2a1d 26 |
. . . . . . . . 9
⊢ (𝑀 = 𝐾 → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))))) |
| 29 | 25, 28 | jaoi 858 |
. . . . . . . 8
⊢ ((𝑀 < 𝐾 ∨ 𝑀 = 𝐾) → (((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 < 𝑁 → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))))) |
| 30 | 29 | expd 415 |
. . . . . . 7
⊢ ((𝑀 < 𝐾 ∨ 𝑀 = 𝐾) → ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁)))))) |
| 31 | 30 | com12 32 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑀 < 𝐾 ∨ 𝑀 = 𝐾) → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁)))))) |
| 32 | 6, 31 | sylbid 240 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ≤ 𝐾 → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁)))))) |
| 33 | 32 | 3impia 1118 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾) → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))))) |
| 34 | 2, 33 | sylbi 217 |
. . 3
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → (𝑁 ∈ ℤ → (𝐾 < 𝑁 → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))))) |
| 35 | 34 | 3imp 1111 |
. 2
⊢ ((𝐾 ∈
(ℤ≥‘𝑀) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))) |
| 36 | 1, 35 | sylbi 217 |
1
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁))) |