Proof of Theorem fzm1
| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → (𝑁...𝑁) = (𝑀...𝑁)) |
| 2 | 1 | eleq2d 2827 |
. . . . . 6
⊢ (𝑁 = 𝑀 → (𝐾 ∈ (𝑁...𝑁) ↔ 𝐾 ∈ (𝑀...𝑁))) |
| 3 | | elfz1eq 13575 |
. . . . . 6
⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁) |
| 4 | 2, 3 | biimtrrdi 254 |
. . . . 5
⊢ (𝑁 = 𝑀 → (𝐾 ∈ (𝑀...𝑁) → 𝐾 = 𝑁)) |
| 5 | | olc 869 |
. . . . 5
⊢ (𝐾 = 𝑁 → (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)) |
| 6 | 4, 5 | syl6 35 |
. . . 4
⊢ (𝑁 = 𝑀 → (𝐾 ∈ (𝑀...𝑁) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |
| 7 | 6 | adantl 481 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...𝑁) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |
| 8 | | noel 4338 |
. . . . . 6
⊢ ¬
𝐾 ∈
∅ |
| 9 | | eluzelz 12888 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
| 10 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 𝑁 ∈ ℤ) |
| 11 | 10 | zred 12722 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 𝑁 ∈ ℝ) |
| 12 | 11 | ltm1d 12200 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑁 − 1) < 𝑁) |
| 13 | | breq2 5147 |
. . . . . . . . . 10
⊢ (𝑁 = 𝑀 → ((𝑁 − 1) < 𝑁 ↔ (𝑁 − 1) < 𝑀)) |
| 14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ((𝑁 − 1) < 𝑁 ↔ (𝑁 − 1) < 𝑀)) |
| 15 | 12, 14 | mpbid 232 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑁 − 1) < 𝑀) |
| 16 | | eluzel2 12883 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
| 17 | | 1zzd 12648 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 1 ∈ ℤ) |
| 18 | 10, 17 | zsubcld 12727 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑁 − 1) ∈ ℤ) |
| 19 | | fzn 13580 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ)
→ ((𝑁 − 1) <
𝑀 ↔ (𝑀...(𝑁 − 1)) = ∅)) |
| 20 | 16, 18, 19 | syl2an2r 685 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ((𝑁 − 1) < 𝑀 ↔ (𝑀...(𝑁 − 1)) = ∅)) |
| 21 | 15, 20 | mpbid 232 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑀...(𝑁 − 1)) = ∅) |
| 22 | 21 | eleq2d 2827 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ 𝐾 ∈ ∅)) |
| 23 | 8, 22 | mtbiri 327 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ¬ 𝐾 ∈ (𝑀...(𝑁 − 1))) |
| 24 | 23 | pm2.21d 121 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...(𝑁 − 1)) → 𝐾 ∈ (𝑀...𝑁))) |
| 25 | | eluzfz2 13572 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
| 26 | 25 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) ∧ 𝐾 = 𝑁) → 𝑁 ∈ (𝑀...𝑁)) |
| 27 | | eleq1 2829 |
. . . . . . 7
⊢ (𝐾 = 𝑁 → (𝐾 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁))) |
| 28 | 27 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) ∧ 𝐾 = 𝑁) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁))) |
| 29 | 26, 28 | mpbird 257 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) ∧ 𝐾 = 𝑁) → 𝐾 ∈ (𝑀...𝑁)) |
| 30 | 29 | ex 412 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 = 𝑁 → 𝐾 ∈ (𝑀...𝑁))) |
| 31 | 24, 30 | jaod 860 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ((𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁) → 𝐾 ∈ (𝑀...𝑁))) |
| 32 | 7, 31 | impbid 212 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |
| 33 | | elfzp1 13614 |
. . . 4
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...((𝑁 − 1) + 1)) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = ((𝑁 − 1) + 1)))) |
| 34 | 33 | adantl 481 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝐾 ∈ (𝑀...((𝑁 − 1) + 1)) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = ((𝑁 − 1) + 1)))) |
| 35 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → 𝑁 ∈ ℤ) |
| 36 | 35 | zcnd 12723 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → 𝑁 ∈ ℂ) |
| 37 | | npcan1 11688 |
. . . . . 6
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
| 38 | 36, 37 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → ((𝑁 − 1) + 1) = 𝑁) |
| 39 | 38 | oveq2d 7447 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝑀...((𝑁 − 1) + 1)) = (𝑀...𝑁)) |
| 40 | 39 | eleq2d 2827 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝐾 ∈ (𝑀...((𝑁 − 1) + 1)) ↔ 𝐾 ∈ (𝑀...𝑁))) |
| 41 | 38 | eqeq2d 2748 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝐾 = ((𝑁 − 1) + 1) ↔ 𝐾 = 𝑁)) |
| 42 | 41 | orbi2d 916 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → ((𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = ((𝑁 − 1) + 1)) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |
| 43 | 34, 40, 42 | 3bitr3d 309 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |
| 44 | | uzm1 12916 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
| 45 | 32, 43, 44 | mpjaodan 961 |
1
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |