Proof of Theorem metakunt24
Step | Hyp | Ref
| Expression |
1 | | indir 4176 |
. . . 4
⊢
(((1...(𝐼 −
1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀}))) |
3 | | metakunt24.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
4 | | metakunt24.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ ℕ) |
5 | | metakunt24.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
6 | 3, 4, 5 | metakunt18 39649 |
. . . . . . 7
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) |
7 | 6 | simpld 499 |
. . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)) |
8 | 7 | simp2d 1141 |
. . . . 5
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅) |
9 | 7 | simp3d 1142 |
. . . . 5
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) |
10 | 8, 9 | uneq12d 4065 |
. . . 4
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = (∅ ∪
∅)) |
11 | | unidm 4053 |
. . . . 5
⊢ (∅
∪ ∅) = ∅ |
12 | 11 | a1i 11 |
. . . 4
⊢ (𝜑 → (∅ ∪ ∅) =
∅) |
13 | 10, 12 | eqtrd 2794 |
. . 3
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = ∅) |
14 | 2, 13 | eqtrd 2794 |
. 2
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅) |
15 | | 1zzd 12037 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
16 | 3 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
17 | 3 | nnge1d 11707 |
. . . . 5
⊢ (𝜑 → 1 ≤ 𝑀) |
18 | 3 | nnred 11674 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
19 | 18 | leidd 11229 |
. . . . 5
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
20 | 15, 16, 16, 17, 19 | elfzd 12932 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ (1...𝑀)) |
21 | 20 | fzsplitnd 39535 |
. . 3
⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑀))) |
22 | | oveq1 7150 |
. . . . . . . . . 10
⊢ (𝐼 = 𝑀 → (𝐼 − 1) = (𝑀 − 1)) |
23 | 22 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝐼 = 𝑀 → (1...(𝐼 − 1)) = (1...(𝑀 − 1))) |
24 | | oveq1 7150 |
. . . . . . . . 9
⊢ (𝐼 = 𝑀 → (𝐼...(𝑀 − 1)) = (𝑀...(𝑀 − 1))) |
25 | 23, 24 | uneq12d 4065 |
. . . . . . . 8
⊢ (𝐼 = 𝑀 → ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) = ((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1)))) |
26 | 25 | uneq1d 4063 |
. . . . . . 7
⊢ (𝐼 = 𝑀 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) ∪ (𝑀...𝑀))) |
27 | 26 | adantl 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) ∪ (𝑀...𝑀))) |
28 | 18 | ltm1d 11595 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
29 | 16, 15 | zsubcld 12116 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
30 | | fzn 12957 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)
→ ((𝑀 − 1) <
𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
31 | 16, 29, 30 | syl2anc 588 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) |
32 | 28, 31 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅) |
33 | 32 | adantr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀...(𝑀 − 1)) = ∅) |
34 | 33 | uneq2d 4064 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) = ((1...(𝑀 − 1)) ∪
∅)) |
35 | | un0 4280 |
. . . . . . . . 9
⊢
((1...(𝑀 − 1))
∪ ∅) = (1...(𝑀
− 1)) |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ ∅) = (1...(𝑀 − 1))) |
37 | 34, 36 | eqtrd 2794 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) = (1...(𝑀 − 1))) |
38 | 37 | uneq1d 4063 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) ∪ (𝑀...𝑀)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑀))) |
39 | 27, 38 | eqtrd 2794 |
. . . . 5
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑀))) |
40 | 39 | eqcomd 2765 |
. . . 4
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀))) |
41 | 15 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ∈ ℤ) |
42 | 16 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝑀 ∈ ℤ) |
43 | 42, 41 | zsubcld 12116 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 1) ∈ ℤ) |
44 | 4 | nnzd 12110 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ ℤ) |
45 | 44 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 ∈ ℤ) |
46 | 4 | nnge1d 11707 |
. . . . . . 7
⊢ (𝜑 → 1 ≤ 𝐼) |
47 | 46 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ≤ 𝐼) |
48 | | eqid 2759 |
. . . . . . . . . . 11
⊢ 𝑀 = 𝑀 |
49 | | eqeq1 2763 |
. . . . . . . . . . 11
⊢ (𝑀 = 𝐼 → (𝑀 = 𝑀 ↔ 𝐼 = 𝑀)) |
50 | 48, 49 | mpbii 236 |
. . . . . . . . . 10
⊢ (𝑀 = 𝐼 → 𝐼 = 𝑀) |
51 | 50 | necon3bi 2975 |
. . . . . . . . 9
⊢ (¬
𝐼 = 𝑀 → 𝑀 ≠ 𝐼) |
52 | 51 | adantl 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝑀 ≠ 𝐼) |
53 | 4 | nnred 11674 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ ℝ) |
54 | 53, 18, 5 | leltned 10816 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 < 𝑀 ↔ 𝑀 ≠ 𝐼)) |
55 | 54 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝐼 < 𝑀 ↔ 𝑀 ≠ 𝐼)) |
56 | 52, 55 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 < 𝑀) |
57 | | zltlem1 12059 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1))) |
58 | 44, 16, 57 | syl2anc 588 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1))) |
59 | 58 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1))) |
60 | 56, 59 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 ≤ (𝑀 − 1)) |
61 | 41, 43, 45, 47, 60 | fzsplitnr 39536 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
62 | 61 | uneq1d 4063 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀))) |
63 | 40, 62 | pm2.61dan 813 |
. . 3
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀))) |
64 | | fzsn 12983 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
65 | 16, 64 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) |
66 | 65 | uneq2d 4064 |
. . 3
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀})) |
67 | 21, 63, 66 | 3eqtrd 2798 |
. 2
⊢ (𝜑 → (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀})) |
68 | | uncom 4054 |
. . . . . 6
⊢ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) |
69 | 68 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) |
70 | 69 | uneq1d 4063 |
. . . 4
⊢ (𝜑 → (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀})) |
71 | 65 | uneq2d 4064 |
. . . . . 6
⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀})) |
72 | 71 | eqcomd 2765 |
. . . . 5
⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀}) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀))) |
73 | | fz10 12962 |
. . . . . . . . . . . . . . 15
⊢ (1...0) =
∅ |
74 | 73 | uneq1i 4060 |
. . . . . . . . . . . . . 14
⊢ ((1...0)
∪ (1...(𝑀 − 1)))
= (∅ ∪ (1...(𝑀
− 1))) |
75 | 74 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1...0) ∪ (1...(𝑀 − 1))) = (∅ ∪
(1...(𝑀 −
1)))) |
76 | 75 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...0) ∪ (1...(𝑀 − 1))) = (∅ ∪
(1...(𝑀 −
1)))) |
77 | | uncom 4054 |
. . . . . . . . . . . . . . 15
⊢
((1...(𝑀 − 1))
∪ ∅) = (∅ ∪ (1...(𝑀 − 1))) |
78 | 77 | eqeq1i 2764 |
. . . . . . . . . . . . . 14
⊢
(((1...(𝑀 −
1)) ∪ ∅) = (1...(𝑀 − 1)) ↔ (∅ ∪
(1...(𝑀 − 1))) =
(1...(𝑀 −
1))) |
79 | 78 | imbi2i 340 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ ∅) = (1...(𝑀 − 1))) ↔ ((𝜑 ∧ 𝐼 = 𝑀) → (∅ ∪ (1...(𝑀 − 1))) = (1...(𝑀 − 1)))) |
80 | 36, 79 | mpbi 233 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (∅ ∪ (1...(𝑀 − 1))) = (1...(𝑀 − 1))) |
81 | 76, 80 | eqtrd 2794 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...0) ∪ (1...(𝑀 − 1))) = (1...(𝑀 − 1))) |
82 | 81 | eqcomd 2765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...0) ∪ (1...(𝑀 − 1)))) |
83 | | oveq2 7151 |
. . . . . . . . . . . . . . 15
⊢ (𝐼 = 𝑀 → (𝑀 − 𝐼) = (𝑀 − 𝑀)) |
84 | 83 | adantl 486 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀 − 𝐼) = (𝑀 − 𝑀)) |
85 | 18 | recnd 10692 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℂ) |
86 | 85 | subidd 11008 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 − 𝑀) = 0) |
87 | 86 | adantr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀 − 𝑀) = 0) |
88 | 84, 87 | eqtrd 2794 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀 − 𝐼) = 0) |
89 | 88 | oveq2d 7159 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (1...(𝑀 − 𝐼)) = (1...0)) |
90 | 83 | oveq1d 7158 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 = 𝑀 → ((𝑀 − 𝐼) + 1) = ((𝑀 − 𝑀) + 1)) |
91 | 90 | adantl 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝐼) + 1) = ((𝑀 − 𝑀) + 1)) |
92 | 87 | oveq1d 7158 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝑀) + 1) = (0 + 1)) |
93 | 91, 92 | eqtrd 2794 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝐼) + 1) = (0 + 1)) |
94 | | 1e0p1 12164 |
. . . . . . . . . . . . . 14
⊢ 1 = (0 +
1) |
95 | 93, 94 | eqtr4di 2812 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝐼) + 1) = 1) |
96 | 95 | oveq1d 7158 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((𝑀 − 𝐼) + 1)...(𝑀 − 1)) = (1...(𝑀 − 1))) |
97 | 89, 96 | uneq12d 4065 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) = ((1...0) ∪ (1...(𝑀 − 1)))) |
98 | 97 | eqcomd 2765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...0) ∪ (1...(𝑀 − 1))) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) |
99 | 82, 98 | eqtrd 2794 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) |
100 | 42, 45 | zsubcld 12116 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 𝐼) ∈ ℤ) |
101 | 53 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 ∈ ℝ) |
102 | 18 | adantr 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝑀 ∈ ℝ) |
103 | | 1red 10665 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ∈ ℝ) |
104 | 101, 102,
103, 60 | lesubd 11267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ≤ (𝑀 − 𝐼)) |
105 | 103, 101,
102, 47 | lesub2dd 11280 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 𝐼) ≤ (𝑀 − 1)) |
106 | 41, 43, 100, 104, 105 | elfzd 12932 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 𝐼) ∈ (1...(𝑀 − 1))) |
107 | | fzsplit 12967 |
. . . . . . . . . 10
⊢ ((𝑀 − 𝐼) ∈ (1...(𝑀 − 1)) → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) |
108 | 106, 107 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) |
109 | 99, 108 | pm2.61dan 813 |
. . . . . . . 8
⊢ (𝜑 → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) |
110 | 109 | uneq1d 4063 |
. . . . . . 7
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀))) |
111 | 21, 110 | eqtrd 2794 |
. . . . . 6
⊢ (𝜑 → (1...𝑀) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀))) |
112 | 111 | eqcomd 2765 |
. . . . 5
⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (1...𝑀)) |
113 | 72, 112 | eqtrd 2794 |
. . . 4
⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀}) = (1...𝑀)) |
114 | 70, 113 | eqtrd 2794 |
. . 3
⊢ (𝜑 → (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}) = (1...𝑀)) |
115 | 114 | eqcomd 2765 |
. 2
⊢ (𝜑 → (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀})) |
116 | 14, 67, 115 | 3jca 1126 |
1
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}))) |