Proof of Theorem fzdifsuc2
Step | Hyp | Ref
| Expression |
1 | | simpr 487 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → 𝑁 = (𝑀 − 1)) |
2 | | zre 11986 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
3 | 2 | ad2antlr 725 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → 𝑀 ∈ ℝ) |
4 | 3 | ltm1d 11572 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → (𝑀 − 1) < 𝑀) |
5 | 1, 4 | eqbrtrd 5088 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → 𝑁 < 𝑀) |
6 | | simplr 767 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → 𝑀 ∈ ℤ) |
7 | | eluzelz 12254 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 − 1)) → 𝑁 ∈ ℤ) |
8 | 7 | ad2antrr 724 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → 𝑁 ∈ ℤ) |
9 | | fzn 12924 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅)) |
10 | 6, 8, 9 | syl2anc 586 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → (𝑁 < 𝑀 ↔ (𝑀...𝑁) = ∅)) |
11 | 5, 10 | mpbid 234 |
. . . 4
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → (𝑀...𝑁) = ∅) |
12 | | difid 4330 |
. . . . . 6
⊢ ({𝑀} ∖ {𝑀}) = ∅ |
13 | 12 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → ({𝑀} ∖ {𝑀}) = ∅) |
14 | 13 | eqcomd 2827 |
. . . 4
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → ∅ = ({𝑀} ∖ {𝑀})) |
15 | | oveq1 7163 |
. . . . . . . . 9
⊢ (𝑁 = (𝑀 − 1) → (𝑁 + 1) = ((𝑀 − 1) + 1)) |
16 | 15 | adantl 484 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → (𝑁 + 1) = ((𝑀 − 1) + 1)) |
17 | 2 | recnd 10669 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
18 | 17 | ad2antlr 725 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → 𝑀 ∈ ℂ) |
19 | | 1cnd 10636 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → 1 ∈
ℂ) |
20 | 18, 19 | npcand 11001 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → ((𝑀 − 1) + 1) = 𝑀) |
21 | 16, 20 | eqtrd 2856 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → (𝑁 + 1) = 𝑀) |
22 | 21 | oveq2d 7172 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → (𝑀...(𝑁 + 1)) = (𝑀...𝑀)) |
23 | | fzsn 12950 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
24 | 23 | ad2antlr 725 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → (𝑀...𝑀) = {𝑀}) |
25 | 22, 24 | eqtr2d 2857 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → {𝑀} = (𝑀...(𝑁 + 1))) |
26 | 21 | eqcomd 2827 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → 𝑀 = (𝑁 + 1)) |
27 | 26 | sneqd 4579 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → {𝑀} = {(𝑁 + 1)}) |
28 | 25, 27 | difeq12d 4100 |
. . . 4
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → ({𝑀} ∖ {𝑀}) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) |
29 | 11, 14, 28 | 3eqtrd 2860 |
. . 3
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ 𝑁 = (𝑀 − 1)) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) |
30 | | simplr 767 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → 𝑀 ∈ ℤ) |
31 | 7 | ad2antrr 724 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → 𝑁 ∈ ℤ) |
32 | 2 | ad2antlr 725 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → 𝑀 ∈ ℝ) |
33 | | 1red 10642 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → 1 ∈
ℝ) |
34 | 32, 33 | resubcld 11068 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → (𝑀 − 1) ∈ ℝ) |
35 | 31 | zred 12088 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → 𝑁 ∈ ℝ) |
36 | | eluzle 12257 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 − 1)) → (𝑀 − 1) ≤ 𝑁) |
37 | 36 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → (𝑀 − 1) ≤ 𝑁) |
38 | | neqne 3024 |
. . . . . . . . 9
⊢ (¬
𝑁 = (𝑀 − 1) → 𝑁 ≠ (𝑀 − 1)) |
39 | 38 | adantl 484 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → 𝑁 ≠ (𝑀 − 1)) |
40 | 34, 35, 37, 39 | leneltd 10794 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → (𝑀 − 1) < 𝑁) |
41 | | zlem1lt 12035 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) |
42 | 30, 31, 41 | syl2anc 586 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → (𝑀 ≤ 𝑁 ↔ (𝑀 − 1) < 𝑁)) |
43 | 40, 42 | mpbird 259 |
. . . . . 6
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → 𝑀 ≤ 𝑁) |
44 | 30, 31, 43 | 3jca 1124 |
. . . . 5
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
45 | | eluz2 12250 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
46 | 44, 45 | sylibr 236 |
. . . 4
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → 𝑁 ∈ (ℤ≥‘𝑀)) |
47 | | fzdifsuc 12968 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) |
48 | 46, 47 | syl 17 |
. . 3
⊢ (((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) ∧ ¬ 𝑁 = (𝑀 − 1)) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) |
49 | 29, 48 | pm2.61dan 811 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ 𝑀 ∈ ℤ) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) |
50 | | eluzel2 12249 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
51 | 50 | con3i 157 |
. . . . . 6
⊢ (¬
𝑀 ∈ ℤ →
¬ 𝑁 ∈
(ℤ≥‘𝑀)) |
52 | | fzn0 12922 |
. . . . . 6
⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀)) |
53 | 51, 52 | sylnibr 331 |
. . . . 5
⊢ (¬
𝑀 ∈ ℤ →
¬ (𝑀...𝑁) ≠ ∅) |
54 | | nne 3020 |
. . . . 5
⊢ (¬
(𝑀...𝑁) ≠ ∅ ↔ (𝑀...𝑁) = ∅) |
55 | 53, 54 | sylib 220 |
. . . 4
⊢ (¬
𝑀 ∈ ℤ →
(𝑀...𝑁) = ∅) |
56 | | eluzel2 12249 |
. . . . . . . . 9
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
57 | 56 | con3i 157 |
. . . . . . . 8
⊢ (¬
𝑀 ∈ ℤ →
¬ (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
58 | | fzn0 12922 |
. . . . . . . 8
⊢ ((𝑀...(𝑁 + 1)) ≠ ∅ ↔ (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
59 | 57, 58 | sylnibr 331 |
. . . . . . 7
⊢ (¬
𝑀 ∈ ℤ →
¬ (𝑀...(𝑁 + 1)) ≠
∅) |
60 | | nne 3020 |
. . . . . . 7
⊢ (¬
(𝑀...(𝑁 + 1)) ≠ ∅ ↔ (𝑀...(𝑁 + 1)) = ∅) |
61 | 59, 60 | sylib 220 |
. . . . . 6
⊢ (¬
𝑀 ∈ ℤ →
(𝑀...(𝑁 + 1)) = ∅) |
62 | 61 | difeq1d 4098 |
. . . . 5
⊢ (¬
𝑀 ∈ ℤ →
((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)}) = (∅ ∖ {(𝑁 + 1)})) |
63 | | 0dif 4355 |
. . . . . 6
⊢ (∅
∖ {(𝑁 + 1)}) =
∅ |
64 | 63 | a1i 11 |
. . . . 5
⊢ (¬
𝑀 ∈ ℤ →
(∅ ∖ {(𝑁 + 1)})
= ∅) |
65 | 62, 64 | eqtr2d 2857 |
. . . 4
⊢ (¬
𝑀 ∈ ℤ →
∅ = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) |
66 | 55, 65 | eqtrd 2856 |
. . 3
⊢ (¬
𝑀 ∈ ℤ →
(𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) |
67 | 66 | adantl 484 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘(𝑀 − 1)) ∧ ¬ 𝑀 ∈ ℤ) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) |
68 | 49, 67 | pm2.61dan 811 |
1
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 − 1)) → (𝑀...𝑁) = ((𝑀...(𝑁 + 1)) ∖ {(𝑁 + 1)})) |