Metamath Proof Explorer

Theorem metakunt24

Description: Technical condition such that metakunt17 holds. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses metakunt24.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt24.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt24.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
Assertion metakunt24 ( 𝜑 → ( ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ∅ ∧ ( 1 ... 𝑀 ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) ∧ ( 1 ... 𝑀 ) = ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∪ ( 1 ... ( 𝑀 − 𝐼 ) ) ) ∪ { 𝑀 } ) ) )

Proof

Step Hyp Ref Expression
1 metakunt24.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt24.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt24.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 indir ⊢ ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) )
5 4 a1i ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) ) )
6 1 2 3 metakunt18 ⊢ ( 𝜑 → ( ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) ∧ ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ∅ ∧ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∩ { 𝑀 } ) = ∅ ) ) )
7 6 simpld ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ∅ ∧ ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ ∧ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ ) )
8 7 simp2d ⊢ ( 𝜑 → ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
9 7 simp3d ⊢ ( 𝜑 → ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) = ∅ )
10 8 9 uneq12d ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) ) = ( ∅ ∪ ∅ ) )
11 unidm ⊢ ( ∅ ∪ ∅ ) = ∅
12 11 a1i ⊢ ( 𝜑 → ( ∅ ∪ ∅ ) = ∅ )
13 10 12 eqtrd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∩ { 𝑀 } ) ∪ ( ( 𝐼 ... ( 𝑀 − 1 ) ) ∩ { 𝑀 } ) ) = ∅ )
14 5 13 eqtrd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ∅ )
15 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
16 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
17 1 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑀 )
18 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
19 18 leidd ⊢ ( 𝜑 → 𝑀 ≤ 𝑀 )
20 15 16 16 17 19 elfzd ⊢ ( 𝜑 → 𝑀 ∈ ( 1 ... 𝑀 ) )
21 20 fzsplitnd ⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
22 oveq1 ⊢ ( 𝐼 = 𝑀 → ( 𝐼 − 1 ) = ( 𝑀 − 1 ) )
23 22 oveq2d ⊢ ( 𝐼 = 𝑀 → ( 1 ... ( 𝐼 − 1 ) ) = ( 1 ... ( 𝑀 − 1 ) ) )
24 oveq1 ⊢ ( 𝐼 = 𝑀 → ( 𝐼 ... ( 𝑀 − 1 ) ) = ( 𝑀 ... ( 𝑀 − 1 ) ) )
25 23 24 uneq12d ⊢ ( 𝐼 = 𝑀 → ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... ( 𝑀 − 1 ) ) ) )
26 25 uneq1d ⊢ ( 𝐼 = 𝑀 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
28 18 ltm1d ⊢ ( 𝜑 → ( 𝑀 − 1 ) < 𝑀 )
29 16 15 zsubcld ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℤ )
30 fzn ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 − 1 ) ∈ ℤ ) → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ ) )
31 16 29 30 syl2anc ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ ) )
32 28 31 mpbid ⊢ ( 𝜑 → ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ )
34 33 uneq2d ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... ( 𝑀 − 1 ) ) ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ∅ ) )
35 un0 ⊢ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ∅ ) = ( 1 ... ( 𝑀 − 1 ) )
36 35 a1i ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ∅ ) = ( 1 ... ( 𝑀 − 1 ) ) )
37 34 36 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... ( 𝑀 − 1 ) ) ) = ( 1 ... ( 𝑀 − 1 ) ) )
38 37 uneq1d ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
39 27 38 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
40 39 eqcomd ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
41 15 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 1 ∈ ℤ )
42 16 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 𝑀 ∈ ℤ )
43 42 41 zsubcld ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → ( 𝑀 − 1 ) ∈ ℤ )
44 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
45 44 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 𝐼 ∈ ℤ )
46 2 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐼 )
47 46 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 1 ≤ 𝐼 )
48 eqid ⊢ 𝑀 = 𝑀
49 eqeq1 ⊢ ( 𝑀 = 𝐼 → ( 𝑀 = 𝑀 ↔ 𝐼 = 𝑀 ) )
50 48 49 mpbii ⊢ ( 𝑀 = 𝐼 → 𝐼 = 𝑀 )
51 50 necon3bi ⊢ ( ¬ 𝐼 = 𝑀 → 𝑀 ≠ 𝐼 )
52 51 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 𝑀 ≠ 𝐼 )
53 2 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
54 53 18 3 leltned ⊢ ( 𝜑 → ( 𝐼 < 𝑀 ↔ 𝑀 ≠ 𝐼 ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → ( 𝐼 < 𝑀 ↔ 𝑀 ≠ 𝐼 ) )
56 52 55 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 𝐼 < 𝑀 )
57 zltlem1 ⊢ ( ( 𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐼 < 𝑀 ↔ 𝐼 ≤ ( 𝑀 − 1 ) ) )
58 44 16 57 syl2anc ⊢ ( 𝜑 → ( 𝐼 < 𝑀 ↔ 𝐼 ≤ ( 𝑀 − 1 ) ) )
59 58 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → ( 𝐼 < 𝑀 ↔ 𝐼 ≤ ( 𝑀 − 1 ) ) )
60 56 59 mpbid ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 𝐼 ≤ ( 𝑀 − 1 ) )
61 41 43 45 47 60 fzsplitnr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → ( 1 ... ( 𝑀 − 1 ) ) = ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) )
62 61 uneq1d ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
63 40 62 pm2.61dan ⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
64 fzsn ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
65 16 64 syl ⊢ ( 𝜑 → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
66 65 uneq2d ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) )
67 21 63 66 3eqtrd ⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) )
68 uncom ⊢ ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∪ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) )
69 68 a1i ⊢ ( 𝜑 → ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∪ ( 1 ... ( 𝑀 − 𝐼 ) ) ) = ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) )
70 69 uneq1d ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∪ ( 1 ... ( 𝑀 − 𝐼 ) ) ) ∪ { 𝑀 } ) = ( ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) )
71 65 uneq2d ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) )
72 71 eqcomd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) = ( ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
73 fz10 ⊢ ( 1 ... 0 ) = ∅
74 73 uneq1i ⊢ ( ( 1 ... 0 ) ∪ ( 1 ... ( 𝑀 − 1 ) ) ) = ( ∅ ∪ ( 1 ... ( 𝑀 − 1 ) ) )
75 74 a1i ⊢ ( 𝜑 → ( ( 1 ... 0 ) ∪ ( 1 ... ( 𝑀 − 1 ) ) ) = ( ∅ ∪ ( 1 ... ( 𝑀 − 1 ) ) ) )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 1 ... 0 ) ∪ ( 1 ... ( 𝑀 − 1 ) ) ) = ( ∅ ∪ ( 1 ... ( 𝑀 − 1 ) ) ) )
77 uncom ⊢ ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ∅ ) = ( ∅ ∪ ( 1 ... ( 𝑀 − 1 ) ) )
78 77 eqeq1i ⊢ ( ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ∅ ) = ( 1 ... ( 𝑀 − 1 ) ) ↔ ( ∅ ∪ ( 1 ... ( 𝑀 − 1 ) ) ) = ( 1 ... ( 𝑀 − 1 ) ) )
79 78 imbi2i ⊢ ( ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ∅ ) = ( 1 ... ( 𝑀 − 1 ) ) ) ↔ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ∅ ∪ ( 1 ... ( 𝑀 − 1 ) ) ) = ( 1 ... ( 𝑀 − 1 ) ) ) )
80 36 79 mpbi ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ∅ ∪ ( 1 ... ( 𝑀 − 1 ) ) ) = ( 1 ... ( 𝑀 − 1 ) ) )
81 76 80 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 1 ... 0 ) ∪ ( 1 ... ( 𝑀 − 1 ) ) ) = ( 1 ... ( 𝑀 − 1 ) ) )
82 81 eqcomd ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( 1 ... ( 𝑀 − 1 ) ) = ( ( 1 ... 0 ) ∪ ( 1 ... ( 𝑀 − 1 ) ) ) )
83 oveq2 ⊢ ( 𝐼 = 𝑀 → ( 𝑀 − 𝐼 ) = ( 𝑀 − 𝑀 ) )
84 83 adantl ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( 𝑀 − 𝐼 ) = ( 𝑀 − 𝑀 ) )
85 18 recnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
86 85 subidd ⊢ ( 𝜑 → ( 𝑀 − 𝑀 ) = 0 )
87 86 adantr ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( 𝑀 − 𝑀 ) = 0 )
88 84 87 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( 𝑀 − 𝐼 ) = 0 )
89 88 oveq2d ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( 1 ... ( 𝑀 − 𝐼 ) ) = ( 1 ... 0 ) )
90 83 oveq1d ⊢ ( 𝐼 = 𝑀 → ( ( 𝑀 − 𝐼 ) + 1 ) = ( ( 𝑀 − 𝑀 ) + 1 ) )
91 90 adantl ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 𝑀 − 𝐼 ) + 1 ) = ( ( 𝑀 − 𝑀 ) + 1 ) )
92 87 oveq1d ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 𝑀 − 𝑀 ) + 1 ) = ( 0 + 1 ) )
93 91 92 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 𝑀 − 𝐼 ) + 1 ) = ( 0 + 1 ) )
94 1e0p1 ⊢ 1 = ( 0 + 1 )
95 93 94 eqtr4di ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 𝑀 − 𝐼 ) + 1 ) = 1 )
96 95 oveq1d ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) = ( 1 ... ( 𝑀 − 1 ) ) )
97 89 96 uneq12d ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) = ( ( 1 ... 0 ) ∪ ( 1 ... ( 𝑀 − 1 ) ) ) )
98 97 eqcomd ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( ( 1 ... 0 ) ∪ ( 1 ... ( 𝑀 − 1 ) ) ) = ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) )
99 82 98 eqtrd ⊢ ( ( 𝜑 ∧ 𝐼 = 𝑀 ) → ( 1 ... ( 𝑀 − 1 ) ) = ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) )
100 42 45 zsubcld ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → ( 𝑀 − 𝐼 ) ∈ ℤ )
101 53 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 𝐼 ∈ ℝ )
102 18 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 𝑀 ∈ ℝ )
103 1red ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 1 ∈ ℝ )
104 101 102 103 60 lesubd ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → 1 ≤ ( 𝑀 − 𝐼 ) )
105 103 101 102 47 lesub2dd ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → ( 𝑀 − 𝐼 ) ≤ ( 𝑀 − 1 ) )
106 41 43 100 104 105 elfzd ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → ( 𝑀 − 𝐼 ) ∈ ( 1 ... ( 𝑀 − 1 ) ) )
107 fzsplit ⊢ ( ( 𝑀 − 𝐼 ) ∈ ( 1 ... ( 𝑀 − 1 ) ) → ( 1 ... ( 𝑀 − 1 ) ) = ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) )
108 106 107 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐼 = 𝑀 ) → ( 1 ... ( 𝑀 − 1 ) ) = ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) )
109 99 108 pm2.61dan ⊢ ( 𝜑 → ( 1 ... ( 𝑀 − 1 ) ) = ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) )
110 109 uneq1d ⊢ ( 𝜑 → ( ( 1 ... ( 𝑀 − 1 ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
111 21 110 eqtrd ⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) )
112 111 eqcomd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ∪ ( 𝑀 ... 𝑀 ) ) = ( 1 ... 𝑀 ) )
113 72 112 eqtrd ⊢ ( 𝜑 → ( ( ( 1 ... ( 𝑀 − 𝐼 ) ) ∪ ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) = ( 1 ... 𝑀 ) )
114 70 113 eqtrd ⊢ ( 𝜑 → ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∪ ( 1 ... ( 𝑀 − 𝐼 ) ) ) ∪ { 𝑀 } ) = ( 1 ... 𝑀 ) )
115 114 eqcomd ⊢ ( 𝜑 → ( 1 ... 𝑀 ) = ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∪ ( 1 ... ( 𝑀 − 𝐼 ) ) ) ∪ { 𝑀 } ) )
116 14 67 115 3jca ⊢ ( 𝜑 → ( ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∩ { 𝑀 } ) = ∅ ∧ ( 1 ... 𝑀 ) = ( ( ( 1 ... ( 𝐼 − 1 ) ) ∪ ( 𝐼 ... ( 𝑀 − 1 ) ) ) ∪ { 𝑀 } ) ∧ ( 1 ... 𝑀 ) = ( ( ( ( ( 𝑀 − 𝐼 ) + 1 ) ... ( 𝑀 − 1 ) ) ∪ ( 1 ... ( 𝑀 − 𝐼 ) ) ) ∪ { 𝑀 } ) ) )