Metamath Proof Explorer

Theorem metakunt24

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

Ref Expression
Hypotheses metakunt24.1 ⊢φ→M∈ℕ
metakunt24.2 ⊢φ→I∈ℕ
metakunt24.3 ⊢φ→I≤M
Assertion metakunt24 ⊢φ→1…I−1∪I…M−1∩M=∅∧1…M=1…I−1∪I…M−1∪M∧1…M=M-I+1…M−1∪1…M−I∪M

Proof

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