Proof of Theorem fzopredsuc
Step | Hyp | Ref
| Expression |
1 | | eluzelz 11573 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
2 | | unidm 3718 |
. . . . . . 7
⊢ ({𝑁} ∪ {𝑁}) = {𝑁} |
3 | 2 | eqcomi 2619 |
. . . . . 6
⊢ {𝑁} = ({𝑁} ∪ {𝑁}) |
4 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑀 = 𝑁 → (𝑀...𝑁) = (𝑁...𝑁)) |
5 | | fzsn 12254 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
6 | 4, 5 | sylan9eqr 2666 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 𝑁) → (𝑀...𝑁) = {𝑁}) |
7 | | sneq 4135 |
. . . . . . . . 9
⊢ (𝑀 = 𝑁 → {𝑀} = {𝑁}) |
8 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑀 = 𝑁 → (𝑀 + 1) = (𝑁 + 1)) |
9 | 8 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑀 = 𝑁 → ((𝑀 + 1)..^𝑁) = ((𝑁 + 1)..^𝑁)) |
10 | 7, 9 | uneq12d 3730 |
. . . . . . . 8
⊢ (𝑀 = 𝑁 → ({𝑀} ∪ ((𝑀 + 1)..^𝑁)) = ({𝑁} ∪ ((𝑁 + 1)..^𝑁))) |
11 | 10 | uneq1d 3728 |
. . . . . . 7
⊢ (𝑀 = 𝑁 → (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}) = (({𝑁} ∪ ((𝑁 + 1)..^𝑁)) ∪ {𝑁})) |
12 | | zre 11258 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
13 | 12 | lep1d 10834 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (𝑁 + 1)) |
14 | | peano2z 11295 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈
ℤ) |
15 | 14 | zred 11358 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈
ℝ) |
16 | 12, 15 | lenltd 10062 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑁 ≤ (𝑁 + 1) ↔ ¬ (𝑁 + 1) < 𝑁)) |
17 | 13, 16 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → ¬
(𝑁 + 1) < 𝑁) |
18 | | fzonlt0 12360 |
. . . . . . . . . . . 12
⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬
(𝑁 + 1) < 𝑁 ↔ ((𝑁 + 1)..^𝑁) = ∅)) |
19 | 14, 18 | mpancom 700 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (¬
(𝑁 + 1) < 𝑁 ↔ ((𝑁 + 1)..^𝑁) = ∅)) |
20 | 17, 19 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → ((𝑁 + 1)..^𝑁) = ∅) |
21 | 20 | uneq2d 3729 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → ({𝑁} ∪ ((𝑁 + 1)..^𝑁)) = ({𝑁} ∪ ∅)) |
22 | | un0 3919 |
. . . . . . . . 9
⊢ ({𝑁} ∪ ∅) = {𝑁} |
23 | 21, 22 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → ({𝑁} ∪ ((𝑁 + 1)..^𝑁)) = {𝑁}) |
24 | 23 | uneq1d 3728 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (({𝑁} ∪ ((𝑁 + 1)..^𝑁)) ∪ {𝑁}) = ({𝑁} ∪ {𝑁})) |
25 | 11, 24 | sylan9eqr 2666 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 𝑁) → (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}) = ({𝑁} ∪ {𝑁})) |
26 | 3, 6, 25 | 3eqtr4a 2670 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 𝑁) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) |
27 | 26 | ex 449 |
. . . 4
⊢ (𝑁 ∈ ℤ → (𝑀 = 𝑁 → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}))) |
28 | 1, 27 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀 = 𝑁 → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}))) |
29 | 28 | com12 32 |
. 2
⊢ (𝑀 = 𝑁 → (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}))) |
30 | | fzisfzounsn 12445 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀..^𝑁) ∪ {𝑁})) |
31 | 30 | adantl 481 |
. . . 4
⊢ ((¬
𝑀 = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝑀...𝑁) = ((𝑀..^𝑁) ∪ {𝑁})) |
32 | | eluz2 11569 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
33 | | simpl1 1057 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ∧ ¬ 𝑀 = 𝑁) → 𝑀 ∈ ℤ) |
34 | | simpl2 1058 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ∧ ¬ 𝑀 = 𝑁) → 𝑁 ∈ ℤ) |
35 | | nesym 2838 |
. . . . . . . . . . . 12
⊢ (𝑁 ≠ 𝑀 ↔ ¬ 𝑀 = 𝑁) |
36 | | zre 11258 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
37 | | ltlen 10017 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀))) |
38 | 36, 12, 37 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀))) |
39 | 38 | biimprd 237 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀) → 𝑀 < 𝑁)) |
40 | 39 | exp4b 630 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ ℤ → (𝑀 ≤ 𝑁 → (𝑁 ≠ 𝑀 → 𝑀 < 𝑁)))) |
41 | 40 | 3imp 1249 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑁 ≠ 𝑀 → 𝑀 < 𝑁)) |
42 | 35, 41 | syl5bir 232 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (¬ 𝑀 = 𝑁 → 𝑀 < 𝑁)) |
43 | 42 | imp 444 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ∧ ¬ 𝑀 = 𝑁) → 𝑀 < 𝑁) |
44 | 33, 34, 43 | 3jca 1235 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ∧ ¬ 𝑀 = 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)) |
45 | 44 | ex 449 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (¬ 𝑀 = 𝑁 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))) |
46 | 32, 45 | sylbi 206 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (¬ 𝑀 = 𝑁 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))) |
47 | 46 | impcom 445 |
. . . . . 6
⊢ ((¬
𝑀 = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)) |
48 | | fzopred 39945 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁))) |
49 | 47, 48 | syl 17 |
. . . . 5
⊢ ((¬
𝑀 = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁))) |
50 | 49 | uneq1d 3728 |
. . . 4
⊢ ((¬
𝑀 = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → ((𝑀..^𝑁) ∪ {𝑁}) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) |
51 | 31, 50 | eqtrd 2644 |
. . 3
⊢ ((¬
𝑀 = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) |
52 | 51 | ex 449 |
. 2
⊢ (¬
𝑀 = 𝑁 → (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}))) |
53 | 29, 52 | pm2.61i 175 |
1
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) |