Metamath Proof Explorer

Theorem metakunt24

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

Ref Expression
Hypotheses metakunt24.1 
|- ( ph -> M e. NN )
metakunt24.2 
|- ( ph -> I e. NN )
metakunt24.3 
|- ( ph -> I <_ M )
Assertion metakunt24 
|- ( ph -> ( ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = (/) /\ ( 1 ... M ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. { M } ) /\ ( 1 ... M ) = ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) u. ( 1 ... ( M - I ) ) ) u. { M } ) ) )

Proof

Step Hyp Ref Expression
1 metakunt24.1 
 |-  ( ph -> M e. NN )
2 metakunt24.2 
 |-  ( ph -> I e. NN )
3 metakunt24.3 
 |-  ( ph -> I <_ M )
4 indir 
 |-  ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) )
5 4 a1i 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) ) )
6 1 2 3 metakunt18 
 |-  ( ph -> ( ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) /\ ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = (/) /\ ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i { M } ) = (/) /\ ( ( 1 ... ( M - I ) ) i^i { M } ) = (/) ) ) )
7 6 simpld 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) )
8 7 simp2d 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) )
9 7 simp3d 
 |-  ( ph -> ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) )
10 8 9 uneq12d 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) ) = ( (/) u. (/) ) )
11 unidm 
 |-  ( (/) u. (/) ) = (/)
12 11 a1i 
 |-  ( ph -> ( (/) u. (/) ) = (/) )
13 10 12 eqtrd 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i { M } ) u. ( ( I ... ( M - 1 ) ) i^i { M } ) ) = (/) )
14 5 13 eqtrd 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = (/) )
15 1zzd 
 |-  ( ph -> 1 e. ZZ )
16 1 nnzd 
 |-  ( ph -> M e. ZZ )
17 1 nnge1d 
 |-  ( ph -> 1 <_ M )
18 1 nnred 
 |-  ( ph -> M e. RR )
19 18 leidd 
 |-  ( ph -> M <_ M )
20 15 16 16 17 19 elfzd 
 |-  ( ph -> M e. ( 1 ... M ) )
21 20 fzsplitnd 
 |-  ( ph -> ( 1 ... M ) = ( ( 1 ... ( M - 1 ) ) u. ( 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 ) ) u. ( I ... ( M - 1 ) ) ) = ( ( 1 ... ( M - 1 ) ) u. ( M ... ( M - 1 ) ) ) )
26 25 uneq1d 
 |-  ( I = M -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. ( M ... M ) ) = ( ( ( 1 ... ( M - 1 ) ) u. ( M ... ( M - 1 ) ) ) u. ( M ... M ) ) )
27 26 adantl 
 |-  ( ( ph /\ I = M ) -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. ( M ... M ) ) = ( ( ( 1 ... ( M - 1 ) ) u. ( M ... ( M - 1 ) ) ) u. ( M ... M ) ) )
28 18 ltm1d 
 |-  ( ph -> ( M - 1 ) < M )
29 16 15 zsubcld 
 |-  ( ph -> ( M - 1 ) e. ZZ )
30 fzn 
 |-  ( ( M e. ZZ /\ ( M - 1 ) e. ZZ ) -> ( ( M - 1 ) < M <-> ( M ... ( M - 1 ) ) = (/) ) )
31 16 29 30 syl2anc 
 |-  ( ph -> ( ( M - 1 ) < M <-> ( M ... ( M - 1 ) ) = (/) ) )
32 28 31 mpbid 
 |-  ( ph -> ( M ... ( M - 1 ) ) = (/) )
33 32 adantr 
 |-  ( ( ph /\ I = M ) -> ( M ... ( M - 1 ) ) = (/) )
34 33 uneq2d 
 |-  ( ( ph /\ I = M ) -> ( ( 1 ... ( M - 1 ) ) u. ( M ... ( M - 1 ) ) ) = ( ( 1 ... ( M - 1 ) ) u. (/) ) )
35 un0 
 |-  ( ( 1 ... ( M - 1 ) ) u. (/) ) = ( 1 ... ( M - 1 ) )
36 35 a1i 
 |-  ( ( ph /\ I = M ) -> ( ( 1 ... ( M - 1 ) ) u. (/) ) = ( 1 ... ( M - 1 ) ) )
37 34 36 eqtrd 
 |-  ( ( ph /\ I = M ) -> ( ( 1 ... ( M - 1 ) ) u. ( M ... ( M - 1 ) ) ) = ( 1 ... ( M - 1 ) ) )
38 37 uneq1d 
 |-  ( ( ph /\ I = M ) -> ( ( ( 1 ... ( M - 1 ) ) u. ( M ... ( M - 1 ) ) ) u. ( M ... M ) ) = ( ( 1 ... ( M - 1 ) ) u. ( M ... M ) ) )
39 27 38 eqtrd 
 |-  ( ( ph /\ I = M ) -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. ( M ... M ) ) = ( ( 1 ... ( M - 1 ) ) u. ( M ... M ) ) )
40 39 eqcomd 
 |-  ( ( ph /\ I = M ) -> ( ( 1 ... ( M - 1 ) ) u. ( M ... M ) ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. ( M ... M ) ) )
41 15 adantr 
 |-  ( ( ph /\ -. I = M ) -> 1 e. ZZ )
42 16 adantr 
 |-  ( ( ph /\ -. I = M ) -> M e. ZZ )
43 42 41 zsubcld 
 |-  ( ( ph /\ -. I = M ) -> ( M - 1 ) e. ZZ )
44 2 nnzd 
 |-  ( ph -> I e. ZZ )
45 44 adantr 
 |-  ( ( ph /\ -. I = M ) -> I e. ZZ )
46 2 nnge1d 
 |-  ( ph -> 1 <_ I )
47 46 adantr 
 |-  ( ( ph /\ -. 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 
 |-  ( ( ph /\ -. I = M ) -> M =/= I )
53 2 nnred 
 |-  ( ph -> I e. RR )
54 53 18 3 leltned 
 |-  ( ph -> ( I < M <-> M =/= I ) )
55 54 adantr 
 |-  ( ( ph /\ -. I = M ) -> ( I < M <-> M =/= I ) )
56 52 55 mpbird 
 |-  ( ( ph /\ -. I = M ) -> I < M )
57 zltlem1 
 |-  ( ( I e. ZZ /\ M e. ZZ ) -> ( I < M <-> I <_ ( M - 1 ) ) )
58 44 16 57 syl2anc 
 |-  ( ph -> ( I < M <-> I <_ ( M - 1 ) ) )
59 58 adantr 
 |-  ( ( ph /\ -. I = M ) -> ( I < M <-> I <_ ( M - 1 ) ) )
60 56 59 mpbid 
 |-  ( ( ph /\ -. I = M ) -> I <_ ( M - 1 ) )
61 41 43 45 47 60 fzsplitnr 
 |-  ( ( ph /\ -. I = M ) -> ( 1 ... ( M - 1 ) ) = ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
62 61 uneq1d 
 |-  ( ( ph /\ -. I = M ) -> ( ( 1 ... ( M - 1 ) ) u. ( M ... M ) ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. ( M ... M ) ) )
63 40 62 pm2.61dan 
 |-  ( ph -> ( ( 1 ... ( M - 1 ) ) u. ( M ... M ) ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. ( M ... M ) ) )
64 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
65 16 64 syl 
 |-  ( ph -> ( M ... M ) = { M } )
66 65 uneq2d 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. ( M ... M ) ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. { M } ) )
67 21 63 66 3eqtrd 
 |-  ( ph -> ( 1 ... M ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. { M } ) )
68 uncom 
 |-  ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) u. ( 1 ... ( M - I ) ) ) = ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) )
69 68 a1i 
 |-  ( ph -> ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) u. ( 1 ... ( M - I ) ) ) = ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) )
70 69 uneq1d 
 |-  ( ph -> ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) u. ( 1 ... ( M - I ) ) ) u. { M } ) = ( ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) u. { M } ) )
71 65 uneq2d 
 |-  ( ph -> ( ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) u. ( M ... M ) ) = ( ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) u. { M } ) )
72 71 eqcomd 
 |-  ( ph -> ( ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) u. { M } ) = ( ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) u. ( M ... M ) ) )
73 fz10 
 |-  ( 1 ... 0 ) = (/)
74 73 uneq1i 
 |-  ( ( 1 ... 0 ) u. ( 1 ... ( M - 1 ) ) ) = ( (/) u. ( 1 ... ( M - 1 ) ) )
75 74 a1i 
 |-  ( ph -> ( ( 1 ... 0 ) u. ( 1 ... ( M - 1 ) ) ) = ( (/) u. ( 1 ... ( M - 1 ) ) ) )
76 75 adantr 
 |-  ( ( ph /\ I = M ) -> ( ( 1 ... 0 ) u. ( 1 ... ( M - 1 ) ) ) = ( (/) u. ( 1 ... ( M - 1 ) ) ) )
77 uncom 
 |-  ( ( 1 ... ( M - 1 ) ) u. (/) ) = ( (/) u. ( 1 ... ( M - 1 ) ) )
78 77 eqeq1i 
 |-  ( ( ( 1 ... ( M - 1 ) ) u. (/) ) = ( 1 ... ( M - 1 ) ) <-> ( (/) u. ( 1 ... ( M - 1 ) ) ) = ( 1 ... ( M - 1 ) ) )
79 78 imbi2i 
 |-  ( ( ( ph /\ I = M ) -> ( ( 1 ... ( M - 1 ) ) u. (/) ) = ( 1 ... ( M - 1 ) ) ) <-> ( ( ph /\ I = M ) -> ( (/) u. ( 1 ... ( M - 1 ) ) ) = ( 1 ... ( M - 1 ) ) ) )
80 36 79 mpbi 
 |-  ( ( ph /\ I = M ) -> ( (/) u. ( 1 ... ( M - 1 ) ) ) = ( 1 ... ( M - 1 ) ) )
81 76 80 eqtrd 
 |-  ( ( ph /\ I = M ) -> ( ( 1 ... 0 ) u. ( 1 ... ( M - 1 ) ) ) = ( 1 ... ( M - 1 ) ) )
82 81 eqcomd 
 |-  ( ( ph /\ I = M ) -> ( 1 ... ( M - 1 ) ) = ( ( 1 ... 0 ) u. ( 1 ... ( M - 1 ) ) ) )
83 oveq2 
 |-  ( I = M -> ( M - I ) = ( M - M ) )
84 83 adantl 
 |-  ( ( ph /\ I = M ) -> ( M - I ) = ( M - M ) )
85 18 recnd 
 |-  ( ph -> M e. CC )
86 85 subidd 
 |-  ( ph -> ( M - M ) = 0 )
87 86 adantr 
 |-  ( ( ph /\ I = M ) -> ( M - M ) = 0 )
88 84 87 eqtrd 
 |-  ( ( ph /\ I = M ) -> ( M - I ) = 0 )
89 88 oveq2d 
 |-  ( ( ph /\ I = M ) -> ( 1 ... ( M - I ) ) = ( 1 ... 0 ) )
90 83 oveq1d 
 |-  ( I = M -> ( ( M - I ) + 1 ) = ( ( M - M ) + 1 ) )
91 90 adantl 
 |-  ( ( ph /\ I = M ) -> ( ( M - I ) + 1 ) = ( ( M - M ) + 1 ) )
92 87 oveq1d 
 |-  ( ( ph /\ I = M ) -> ( ( M - M ) + 1 ) = ( 0 + 1 ) )
93 91 92 eqtrd 
 |-  ( ( ph /\ I = M ) -> ( ( M - I ) + 1 ) = ( 0 + 1 ) )
94 1e0p1 
 |-  1 = ( 0 + 1 )
95 93 94 eqtr4di 
 |-  ( ( ph /\ I = M ) -> ( ( M - I ) + 1 ) = 1 )
96 95 oveq1d 
 |-  ( ( ph /\ I = M ) -> ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) = ( 1 ... ( M - 1 ) ) )
97 89 96 uneq12d 
 |-  ( ( ph /\ I = M ) -> ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) = ( ( 1 ... 0 ) u. ( 1 ... ( M - 1 ) ) ) )
98 97 eqcomd 
 |-  ( ( ph /\ I = M ) -> ( ( 1 ... 0 ) u. ( 1 ... ( M - 1 ) ) ) = ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) )
99 82 98 eqtrd 
 |-  ( ( ph /\ I = M ) -> ( 1 ... ( M - 1 ) ) = ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) )
100 42 45 zsubcld 
 |-  ( ( ph /\ -. I = M ) -> ( M - I ) e. ZZ )
101 53 adantr 
 |-  ( ( ph /\ -. I = M ) -> I e. RR )
102 18 adantr 
 |-  ( ( ph /\ -. I = M ) -> M e. RR )
103 1red 
 |-  ( ( ph /\ -. I = M ) -> 1 e. RR )
104 101 102 103 60 lesubd 
 |-  ( ( ph /\ -. I = M ) -> 1 <_ ( M - I ) )
105 103 101 102 47 lesub2dd 
 |-  ( ( ph /\ -. I = M ) -> ( M - I ) <_ ( M - 1 ) )
106 41 43 100 104 105 elfzd 
 |-  ( ( ph /\ -. I = M ) -> ( M - I ) e. ( 1 ... ( M - 1 ) ) )
107 fzsplit 
 |-  ( ( M - I ) e. ( 1 ... ( M - 1 ) ) -> ( 1 ... ( M - 1 ) ) = ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) )
108 106 107 syl 
 |-  ( ( ph /\ -. I = M ) -> ( 1 ... ( M - 1 ) ) = ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) )
109 99 108 pm2.61dan 
 |-  ( ph -> ( 1 ... ( M - 1 ) ) = ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) )
110 109 uneq1d 
 |-  ( ph -> ( ( 1 ... ( M - 1 ) ) u. ( M ... M ) ) = ( ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) u. ( M ... M ) ) )
111 21 110 eqtrd 
 |-  ( ph -> ( 1 ... M ) = ( ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) u. ( M ... M ) ) )
112 111 eqcomd 
 |-  ( ph -> ( ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) u. ( M ... M ) ) = ( 1 ... M ) )
113 72 112 eqtrd 
 |-  ( ph -> ( ( ( 1 ... ( M - I ) ) u. ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) ) u. { M } ) = ( 1 ... M ) )
114 70 113 eqtrd 
 |-  ( ph -> ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) u. ( 1 ... ( M - I ) ) ) u. { M } ) = ( 1 ... M ) )
115 114 eqcomd 
 |-  ( ph -> ( 1 ... M ) = ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) u. ( 1 ... ( M - I ) ) ) u. { M } ) )
116 14 67 115 3jca 
 |-  ( ph -> ( ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = (/) /\ ( 1 ... M ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. { M } ) /\ ( 1 ... M ) = ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) u. ( 1 ... ( M - I ) ) ) u. { M } ) ) )