Proof of Theorem metakunt24
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | indir 4285 | . . . 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 42224 | . . . . . . 7
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) | 
| 7 | 6 | simpld 494 | . . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)) | 
| 8 | 7 | simp2d 1143 | . . . . 5
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅) | 
| 9 | 7 | simp3d 1144 | . . . . 5
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) | 
| 10 | 8, 9 | uneq12d 4168 | . . . 4
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = (∅ ∪
∅)) | 
| 11 |  | unidm 4156 | . . . . 5
⊢ (∅
∪ ∅) = ∅ | 
| 12 | 11 | a1i 11 | . . . 4
⊢ (𝜑 → (∅ ∪ ∅) =
∅) | 
| 13 | 10, 12 | eqtrd 2776 | . . 3
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = ∅) | 
| 14 | 2, 13 | eqtrd 2776 | . 2
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅) | 
| 15 |  | 1zzd 12650 | . . . . 5
⊢ (𝜑 → 1 ∈
ℤ) | 
| 16 | 3 | nnzd 12642 | . . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 17 | 3 | nnge1d 12315 | . . . . 5
⊢ (𝜑 → 1 ≤ 𝑀) | 
| 18 | 3 | nnred 12282 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 19 | 18 | leidd 11830 | . . . . 5
⊢ (𝜑 → 𝑀 ≤ 𝑀) | 
| 20 | 15, 16, 16, 17, 19 | elfzd 13556 | . . . 4
⊢ (𝜑 → 𝑀 ∈ (1...𝑀)) | 
| 21 | 20 | fzsplitnd 41984 | . . 3
⊢ (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑀))) | 
| 22 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝐼 = 𝑀 → (𝐼 − 1) = (𝑀 − 1)) | 
| 23 | 22 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝐼 = 𝑀 → (1...(𝐼 − 1)) = (1...(𝑀 − 1))) | 
| 24 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝐼 = 𝑀 → (𝐼...(𝑀 − 1)) = (𝑀...(𝑀 − 1))) | 
| 25 | 23, 24 | uneq12d 4168 | . . . . . . . 8
⊢ (𝐼 = 𝑀 → ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) = ((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1)))) | 
| 26 | 25 | uneq1d 4166 | . . . . . . 7
⊢ (𝐼 = 𝑀 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) ∪ (𝑀...𝑀))) | 
| 27 | 26 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) ∪ (𝑀...𝑀))) | 
| 28 | 18 | ltm1d 12201 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 1) < 𝑀) | 
| 29 | 16, 15 | zsubcld 12729 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) | 
| 30 |  | fzn 13581 | . . . . . . . . . . . 12
⊢ ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ)
→ ((𝑀 − 1) <
𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) | 
| 31 | 16, 29, 30 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅)) | 
| 32 | 28, 31 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → (𝑀...(𝑀 − 1)) = ∅) | 
| 33 | 32 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀...(𝑀 − 1)) = ∅) | 
| 34 | 33 | uneq2d 4167 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) = ((1...(𝑀 − 1)) ∪
∅)) | 
| 35 |  | un0 4393 | . . . . . . . . 9
⊢
((1...(𝑀 − 1))
∪ ∅) = (1...(𝑀
− 1)) | 
| 36 | 35 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ ∅) = (1...(𝑀 − 1))) | 
| 37 | 34, 36 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) = (1...(𝑀 − 1))) | 
| 38 | 37 | uneq1d 4166 | . . . . . 6
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((1...(𝑀 − 1)) ∪ (𝑀...(𝑀 − 1))) ∪ (𝑀...𝑀)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑀))) | 
| 39 | 27, 38 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑀))) | 
| 40 | 39 | eqcomd 2742 | . . . 4
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀))) | 
| 41 | 15 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ∈ ℤ) | 
| 42 | 16 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝑀 ∈ ℤ) | 
| 43 | 42, 41 | zsubcld 12729 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 1) ∈ ℤ) | 
| 44 | 4 | nnzd 12642 | . . . . . . 7
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 45 | 44 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 ∈ ℤ) | 
| 46 | 4 | nnge1d 12315 | . . . . . . 7
⊢ (𝜑 → 1 ≤ 𝐼) | 
| 47 | 46 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ≤ 𝐼) | 
| 48 |  | eqid 2736 | . . . . . . . . . . 11
⊢ 𝑀 = 𝑀 | 
| 49 |  | eqeq1 2740 | . . . . . . . . . . 11
⊢ (𝑀 = 𝐼 → (𝑀 = 𝑀 ↔ 𝐼 = 𝑀)) | 
| 50 | 48, 49 | mpbii 233 | . . . . . . . . . 10
⊢ (𝑀 = 𝐼 → 𝐼 = 𝑀) | 
| 51 | 50 | necon3bi 2966 | . . . . . . . . 9
⊢ (¬
𝐼 = 𝑀 → 𝑀 ≠ 𝐼) | 
| 52 | 51 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝑀 ≠ 𝐼) | 
| 53 | 4 | nnred 12282 | . . . . . . . . . 10
⊢ (𝜑 → 𝐼 ∈ ℝ) | 
| 54 | 53, 18, 5 | leltned 11415 | . . . . . . . . 9
⊢ (𝜑 → (𝐼 < 𝑀 ↔ 𝑀 ≠ 𝐼)) | 
| 55 | 54 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝐼 < 𝑀 ↔ 𝑀 ≠ 𝐼)) | 
| 56 | 52, 55 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 < 𝑀) | 
| 57 |  | zltlem1 12672 | . . . . . . . . 9
⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1))) | 
| 58 | 44, 16, 57 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1))) | 
| 59 | 58 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝐼 < 𝑀 ↔ 𝐼 ≤ (𝑀 − 1))) | 
| 60 | 56, 59 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 ≤ (𝑀 − 1)) | 
| 61 | 41, 43, 45, 47, 60 | fzsplitnr 41985 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 62 | 61 | uneq1d 4166 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀))) | 
| 63 | 40, 62 | pm2.61dan 812 | . . 3
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀))) | 
| 64 |  | fzsn 13607 | . . . . 5
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) | 
| 65 | 16, 64 | syl 17 | . . . 4
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) | 
| 66 | 65 | uneq2d 4167 | . . 3
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀})) | 
| 67 | 21, 63, 66 | 3eqtrd 2780 | . 2
⊢ (𝜑 → (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀})) | 
| 68 |  | uncom 4157 | . . . . . 6
⊢ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) | 
| 69 | 68 | a1i 11 | . . . . 5
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) | 
| 70 | 69 | uneq1d 4166 | . . . 4
⊢ (𝜑 → (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀})) | 
| 71 | 65 | uneq2d 4167 | . . . . . 6
⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀})) | 
| 72 | 71 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀}) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀))) | 
| 73 |  | fz10 13586 | . . . . . . . . . . . . . . 15
⊢ (1...0) =
∅ | 
| 74 | 73 | uneq1i 4163 | . . . . . . . . . . . . . 14
⊢ ((1...0)
∪ (1...(𝑀 − 1)))
= (∅ ∪ (1...(𝑀
− 1))) | 
| 75 | 74 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((1...0) ∪ (1...(𝑀 − 1))) = (∅ ∪
(1...(𝑀 −
1)))) | 
| 76 | 75 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...0) ∪ (1...(𝑀 − 1))) = (∅ ∪
(1...(𝑀 −
1)))) | 
| 77 |  | uncom 4157 | . . . . . . . . . . . . . . 15
⊢
((1...(𝑀 − 1))
∪ ∅) = (∅ ∪ (1...(𝑀 − 1))) | 
| 78 | 77 | eqeq1i 2741 | . . . . . . . . . . . . . 14
⊢
(((1...(𝑀 −
1)) ∪ ∅) = (1...(𝑀 − 1)) ↔ (∅ ∪
(1...(𝑀 − 1))) =
(1...(𝑀 −
1))) | 
| 79 | 78 | imbi2i 336 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 1)) ∪ ∅) = (1...(𝑀 − 1))) ↔ ((𝜑 ∧ 𝐼 = 𝑀) → (∅ ∪ (1...(𝑀 − 1))) = (1...(𝑀 − 1)))) | 
| 80 | 36, 79 | mpbi 230 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (∅ ∪ (1...(𝑀 − 1))) = (1...(𝑀 − 1))) | 
| 81 | 76, 80 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...0) ∪ (1...(𝑀 − 1))) = (1...(𝑀 − 1))) | 
| 82 | 81 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...0) ∪ (1...(𝑀 − 1)))) | 
| 83 |  | oveq2 7440 | . . . . . . . . . . . . . . 15
⊢ (𝐼 = 𝑀 → (𝑀 − 𝐼) = (𝑀 − 𝑀)) | 
| 84 | 83 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀 − 𝐼) = (𝑀 − 𝑀)) | 
| 85 | 18 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 86 | 85 | subidd 11609 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 − 𝑀) = 0) | 
| 87 | 86 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀 − 𝑀) = 0) | 
| 88 | 84, 87 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (𝑀 − 𝐼) = 0) | 
| 89 | 88 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (1...(𝑀 − 𝐼)) = (1...0)) | 
| 90 | 83 | oveq1d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝐼 = 𝑀 → ((𝑀 − 𝐼) + 1) = ((𝑀 − 𝑀) + 1)) | 
| 91 | 90 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝐼) + 1) = ((𝑀 − 𝑀) + 1)) | 
| 92 | 87 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝑀) + 1) = (0 + 1)) | 
| 93 | 91, 92 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝐼) + 1) = (0 + 1)) | 
| 94 |  | 1e0p1 12777 | . . . . . . . . . . . . . 14
⊢ 1 = (0 +
1) | 
| 95 | 93, 94 | eqtr4di 2794 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((𝑀 − 𝐼) + 1) = 1) | 
| 96 | 95 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (((𝑀 − 𝐼) + 1)...(𝑀 − 1)) = (1...(𝑀 − 1))) | 
| 97 | 89, 96 | uneq12d 4168 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) = ((1...0) ∪ (1...(𝑀 − 1)))) | 
| 98 | 97 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → ((1...0) ∪ (1...(𝑀 − 1))) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) | 
| 99 | 82, 98 | eqtrd 2776 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) | 
| 100 | 42, 45 | zsubcld 12729 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 𝐼) ∈ ℤ) | 
| 101 | 53 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝐼 ∈ ℝ) | 
| 102 | 18 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 𝑀 ∈ ℝ) | 
| 103 |  | 1red 11263 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ∈ ℝ) | 
| 104 | 101, 102,
103, 60 | lesubd 11868 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → 1 ≤ (𝑀 − 𝐼)) | 
| 105 | 103, 101,
102, 47 | lesub2dd 11881 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 𝐼) ≤ (𝑀 − 1)) | 
| 106 | 41, 43, 100, 104, 105 | elfzd 13556 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (𝑀 − 𝐼) ∈ (1...(𝑀 − 1))) | 
| 107 |  | fzsplit 13591 | . . . . . . . . . 10
⊢ ((𝑀 − 𝐼) ∈ (1...(𝑀 − 1)) → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) | 
| 108 | 106, 107 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐼 = 𝑀) → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) | 
| 109 | 99, 108 | pm2.61dan 812 | . . . . . . . 8
⊢ (𝜑 → (1...(𝑀 − 1)) = ((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1)))) | 
| 110 | 109 | uneq1d 4166 | . . . . . . 7
⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (𝑀...𝑀)) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀))) | 
| 111 | 21, 110 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (1...𝑀) = (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀))) | 
| 112 | 111 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ (𝑀...𝑀)) = (1...𝑀)) | 
| 113 | 72, 112 | eqtrd 2776 | . . . 4
⊢ (𝜑 → (((1...(𝑀 − 𝐼)) ∪ (((𝑀 − 𝐼) + 1)...(𝑀 − 1))) ∪ {𝑀}) = (1...𝑀)) | 
| 114 | 70, 113 | eqtrd 2776 | . . 3
⊢ (𝜑 → (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}) = (1...𝑀)) | 
| 115 | 114 | eqcomd 2742 | . 2
⊢ (𝜑 → (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀})) | 
| 116 | 14, 67, 115 | 3jca 1128 | 1
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}))) |