Proof of Theorem fzm1
Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑁 = 𝑀 → (𝑁...𝑁) = (𝑀...𝑁)) |
2 | 1 | eleq2d 2673 |
. . . . . 6
⊢ (𝑁 = 𝑀 → (𝐾 ∈ (𝑁...𝑁) ↔ 𝐾 ∈ (𝑀...𝑁))) |
3 | | elfz1eq 12223 |
. . . . . 6
⊢ (𝐾 ∈ (𝑁...𝑁) → 𝐾 = 𝑁) |
4 | 2, 3 | syl6bir 243 |
. . . . 5
⊢ (𝑁 = 𝑀 → (𝐾 ∈ (𝑀...𝑁) → 𝐾 = 𝑁)) |
5 | | olc 398 |
. . . . 5
⊢ (𝐾 = 𝑁 → (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁)) |
6 | 4, 5 | syl6 34 |
. . . 4
⊢ (𝑁 = 𝑀 → (𝐾 ∈ (𝑀...𝑁) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |
7 | 6 | adantl 481 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...𝑁) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |
8 | | noel 3878 |
. . . . . 6
⊢ ¬
𝐾 ∈
∅ |
9 | | eluzelz 11573 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
10 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 𝑁 ∈ ℤ) |
11 | 10 | zred 11358 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 𝑁 ∈ ℝ) |
12 | 11 | ltm1d 10835 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑁 − 1) < 𝑁) |
13 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑁 = 𝑀 → ((𝑁 − 1) < 𝑁 ↔ (𝑁 − 1) < 𝑀)) |
14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ((𝑁 − 1) < 𝑁 ↔ (𝑁 − 1) < 𝑀)) |
15 | 12, 14 | mpbid 221 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑁 − 1) < 𝑀) |
16 | | eluzel2 11568 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
17 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 𝑀 ∈ ℤ) |
18 | | 1zzd 11285 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → 1 ∈ ℤ) |
19 | 10, 18 | zsubcld 11363 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑁 − 1) ∈ ℤ) |
20 | | fzn 12228 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ)
→ ((𝑁 − 1) <
𝑀 ↔ (𝑀...(𝑁 − 1)) = ∅)) |
21 | 17, 19, 20 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ((𝑁 − 1) < 𝑀 ↔ (𝑀...(𝑁 − 1)) = ∅)) |
22 | 15, 21 | mpbid 221 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝑀...(𝑁 − 1)) = ∅) |
23 | 22 | eleq2d 2673 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...(𝑁 − 1)) ↔ 𝐾 ∈ ∅)) |
24 | 8, 23 | mtbiri 316 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ¬ 𝐾 ∈ (𝑀...(𝑁 − 1))) |
25 | 24 | pm2.21d 117 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...(𝑁 − 1)) → 𝐾 ∈ (𝑀...𝑁))) |
26 | | eluzfz2 12220 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁)) |
27 | 26 | ad2antrr 758 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) ∧ 𝐾 = 𝑁) → 𝑁 ∈ (𝑀...𝑁)) |
28 | | eleq1 2676 |
. . . . . . 7
⊢ (𝐾 = 𝑁 → (𝐾 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁))) |
29 | 28 | adantl 481 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) ∧ 𝐾 = 𝑁) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝑁 ∈ (𝑀...𝑁))) |
30 | 27, 29 | mpbird 246 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) ∧ 𝐾 = 𝑁) → 𝐾 ∈ (𝑀...𝑁)) |
31 | 30 | ex 449 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 = 𝑁 → 𝐾 ∈ (𝑀...𝑁))) |
32 | 25, 31 | jaod 394 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → ((𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁) → 𝐾 ∈ (𝑀...𝑁))) |
33 | 7, 32 | impbid 201 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ 𝑁 = 𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |
34 | | elfzp1 12261 |
. . . 4
⊢ ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...((𝑁 − 1) + 1)) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = ((𝑁 − 1) + 1)))) |
35 | 34 | adantl 481 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝐾 ∈ (𝑀...((𝑁 − 1) + 1)) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = ((𝑁 − 1) + 1)))) |
36 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → 𝑁 ∈ ℤ) |
37 | 36 | zcnd 11359 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → 𝑁 ∈ ℂ) |
38 | | npcan1 10334 |
. . . . . 6
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
39 | 37, 38 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → ((𝑁 − 1) + 1) = 𝑁) |
40 | 39 | oveq2d 6565 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝑀...((𝑁 − 1) + 1)) = (𝑀...𝑁)) |
41 | 40 | eleq2d 2673 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝐾 ∈ (𝑀...((𝑁 − 1) + 1)) ↔ 𝐾 ∈ (𝑀...𝑁))) |
42 | 39 | eqeq2d 2620 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝐾 = ((𝑁 − 1) + 1) ↔ 𝐾 = 𝑁)) |
43 | 42 | orbi2d 734 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → ((𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = ((𝑁 − 1) + 1)) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |
44 | 35, 41, 43 | 3bitr3d 297 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘𝑀) ∧ (𝑁 − 1) ∈
(ℤ≥‘𝑀)) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |
45 | | uzm1 11594 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 = 𝑀 ∨ (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
46 | 33, 44, 45 | mpjaodan 823 |
1
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (𝑀...(𝑁 − 1)) ∨ 𝐾 = 𝑁))) |