Proof of Theorem fzopredsuc
Step | Hyp | Ref
| Expression |
1 | | unidm 4130 |
. . . . . 6
⊢ ({𝑁} ∪ {𝑁}) = {𝑁} |
2 | 1 | eqcomi 2832 |
. . . . 5
⊢ {𝑁} = ({𝑁} ∪ {𝑁}) |
3 | | oveq1 7165 |
. . . . . 6
⊢ (𝑀 = 𝑁 → (𝑀...𝑁) = (𝑁...𝑁)) |
4 | | fzsn 12952 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (𝑁...𝑁) = {𝑁}) |
5 | 3, 4 | sylan9eqr 2880 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 𝑁) → (𝑀...𝑁) = {𝑁}) |
6 | | sneq 4579 |
. . . . . . . 8
⊢ (𝑀 = 𝑁 → {𝑀} = {𝑁}) |
7 | | oveq1 7165 |
. . . . . . . . 9
⊢ (𝑀 = 𝑁 → (𝑀 + 1) = (𝑁 + 1)) |
8 | 7 | oveq1d 7173 |
. . . . . . . 8
⊢ (𝑀 = 𝑁 → ((𝑀 + 1)..^𝑁) = ((𝑁 + 1)..^𝑁)) |
9 | 6, 8 | uneq12d 4142 |
. . . . . . 7
⊢ (𝑀 = 𝑁 → ({𝑀} ∪ ((𝑀 + 1)..^𝑁)) = ({𝑁} ∪ ((𝑁 + 1)..^𝑁))) |
10 | 9 | uneq1d 4140 |
. . . . . 6
⊢ (𝑀 = 𝑁 → (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}) = (({𝑁} ∪ ((𝑁 + 1)..^𝑁)) ∪ {𝑁})) |
11 | | zre 11988 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
12 | 11 | lep1d 11573 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (𝑁 + 1)) |
13 | | peano2z 12026 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈
ℤ) |
14 | 13 | zred 12090 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈
ℝ) |
15 | 11, 14 | lenltd 10788 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑁 ≤ (𝑁 + 1) ↔ ¬ (𝑁 + 1) < 𝑁)) |
16 | 12, 15 | mpbid 234 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → ¬
(𝑁 + 1) < 𝑁) |
17 | | fzonlt0 13063 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬
(𝑁 + 1) < 𝑁 ↔ ((𝑁 + 1)..^𝑁) = ∅)) |
18 | 13, 17 | mpancom 686 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → (¬
(𝑁 + 1) < 𝑁 ↔ ((𝑁 + 1)..^𝑁) = ∅)) |
19 | 16, 18 | mpbid 234 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ → ((𝑁 + 1)..^𝑁) = ∅) |
20 | 19 | uneq2d 4141 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → ({𝑁} ∪ ((𝑁 + 1)..^𝑁)) = ({𝑁} ∪ ∅)) |
21 | | un0 4346 |
. . . . . . . 8
⊢ ({𝑁} ∪ ∅) = {𝑁} |
22 | 20, 21 | syl6eq 2874 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → ({𝑁} ∪ ((𝑁 + 1)..^𝑁)) = {𝑁}) |
23 | 22 | uneq1d 4140 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → (({𝑁} ∪ ((𝑁 + 1)..^𝑁)) ∪ {𝑁}) = ({𝑁} ∪ {𝑁})) |
24 | 10, 23 | sylan9eqr 2880 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 𝑁) → (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}) = ({𝑁} ∪ {𝑁})) |
25 | 2, 5, 24 | 3eqtr4a 2884 |
. . . 4
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = 𝑁) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) |
26 | 25 | ex 415 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝑀 = 𝑁 → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}))) |
27 | | eluzelz 12256 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
28 | 26, 27 | syl11 33 |
. 2
⊢ (𝑀 = 𝑁 → (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}))) |
29 | | fzisfzounsn 13152 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀..^𝑁) ∪ {𝑁})) |
30 | 29 | adantl 484 |
. . . 4
⊢ ((¬
𝑀 = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝑀...𝑁) = ((𝑀..^𝑁) ∪ {𝑁})) |
31 | | eluz2 12252 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
32 | | simpl1 1187 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ∧ ¬ 𝑀 = 𝑁) → 𝑀 ∈ ℤ) |
33 | | simpl2 1188 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ∧ ¬ 𝑀 = 𝑁) → 𝑁 ∈ ℤ) |
34 | | nesym 3074 |
. . . . . . . . . . . 12
⊢ (𝑁 ≠ 𝑀 ↔ ¬ 𝑀 = 𝑁) |
35 | | zre 11988 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℝ) |
36 | | ltlen 10743 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀))) |
37 | 35, 11, 36 | syl2an 597 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀))) |
38 | 37 | biimprd 250 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 ≤ 𝑁 ∧ 𝑁 ≠ 𝑀) → 𝑀 < 𝑁)) |
39 | 38 | exp4b 433 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ ℤ → (𝑀 ≤ 𝑁 → (𝑁 ≠ 𝑀 → 𝑀 < 𝑁)))) |
40 | 39 | 3imp 1107 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (𝑁 ≠ 𝑀 → 𝑀 < 𝑁)) |
41 | 34, 40 | syl5bir 245 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (¬ 𝑀 = 𝑁 → 𝑀 < 𝑁)) |
42 | 41 | imp 409 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ∧ ¬ 𝑀 = 𝑁) → 𝑀 < 𝑁) |
43 | 32, 33, 42 | 3jca 1124 |
. . . . . . . . 9
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ∧ ¬ 𝑀 = 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)) |
44 | 43 | ex 415 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → (¬ 𝑀 = 𝑁 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))) |
45 | 31, 44 | sylbi 219 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (¬ 𝑀 = 𝑁 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))) |
46 | 45 | impcom 410 |
. . . . . 6
⊢ ((¬
𝑀 = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁)) |
47 | | fzopred 43529 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁))) |
48 | 46, 47 | syl 17 |
. . . . 5
⊢ ((¬
𝑀 = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁))) |
49 | 48 | uneq1d 4140 |
. . . 4
⊢ ((¬
𝑀 = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → ((𝑀..^𝑁) ∪ {𝑁}) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) |
50 | 30, 49 | eqtrd 2858 |
. . 3
⊢ ((¬
𝑀 = 𝑁 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) |
51 | 50 | ex 415 |
. 2
⊢ (¬
𝑀 = 𝑁 → (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}))) |
52 | 28, 51 | pm2.61i 184 |
1
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) |