Metamath Proof Explorer


Theorem iccelpart

Description: An element of any partitioned half-open interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020)

Ref Expression
Assertion iccelpart M p RePart M X p 0 p M i 0 ..^ M X p i p i + 1

Proof

Step Hyp Ref Expression
1 fveq2 x = 1 RePart x = RePart 1
2 fveq2 x = 1 p x = p 1
3 2 oveq2d x = 1 p 0 p x = p 0 p 1
4 3 eleq2d x = 1 X p 0 p x X p 0 p 1
5 oveq2 x = 1 0 ..^ x = 0 ..^ 1
6 fzo01 0 ..^ 1 = 0
7 5 6 eqtrdi x = 1 0 ..^ x = 0
8 7 rexeqdv x = 1 i 0 ..^ x X p i p i + 1 i 0 X p i p i + 1
9 4 8 imbi12d x = 1 X p 0 p x i 0 ..^ x X p i p i + 1 X p 0 p 1 i 0 X p i p i + 1
10 1 9 raleqbidv x = 1 p RePart x X p 0 p x i 0 ..^ x X p i p i + 1 p RePart 1 X p 0 p 1 i 0 X p i p i + 1
11 fveq2 x = y RePart x = RePart y
12 fveq2 x = y p x = p y
13 12 oveq2d x = y p 0 p x = p 0 p y
14 13 eleq2d x = y X p 0 p x X p 0 p y
15 oveq2 x = y 0 ..^ x = 0 ..^ y
16 15 rexeqdv x = y i 0 ..^ x X p i p i + 1 i 0 ..^ y X p i p i + 1
17 14 16 imbi12d x = y X p 0 p x i 0 ..^ x X p i p i + 1 X p 0 p y i 0 ..^ y X p i p i + 1
18 11 17 raleqbidv x = y p RePart x X p 0 p x i 0 ..^ x X p i p i + 1 p RePart y X p 0 p y i 0 ..^ y X p i p i + 1
19 fveq2 x = y + 1 RePart x = RePart y + 1
20 fveq2 x = y + 1 p x = p y + 1
21 20 oveq2d x = y + 1 p 0 p x = p 0 p y + 1
22 21 eleq2d x = y + 1 X p 0 p x X p 0 p y + 1
23 oveq2 x = y + 1 0 ..^ x = 0 ..^ y + 1
24 23 rexeqdv x = y + 1 i 0 ..^ x X p i p i + 1 i 0 ..^ y + 1 X p i p i + 1
25 22 24 imbi12d x = y + 1 X p 0 p x i 0 ..^ x X p i p i + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
26 19 25 raleqbidv x = y + 1 p RePart x X p 0 p x i 0 ..^ x X p i p i + 1 p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
27 fveq2 x = M RePart x = RePart M
28 fveq2 x = M p x = p M
29 28 oveq2d x = M p 0 p x = p 0 p M
30 29 eleq2d x = M X p 0 p x X p 0 p M
31 oveq2 x = M 0 ..^ x = 0 ..^ M
32 31 rexeqdv x = M i 0 ..^ x X p i p i + 1 i 0 ..^ M X p i p i + 1
33 30 32 imbi12d x = M X p 0 p x i 0 ..^ x X p i p i + 1 X p 0 p M i 0 ..^ M X p i p i + 1
34 27 33 raleqbidv x = M p RePart x X p 0 p x i 0 ..^ x X p i p i + 1 p RePart M X p 0 p M i 0 ..^ M X p i p i + 1
35 0nn0 0 0
36 fveq2 i = 0 p i = p 0
37 fv0p1e1 i = 0 p i + 1 = p 1
38 36 37 oveq12d i = 0 p i p i + 1 = p 0 p 1
39 38 eleq2d i = 0 X p i p i + 1 X p 0 p 1
40 39 rexsng 0 0 i 0 X p i p i + 1 X p 0 p 1
41 35 40 ax-mp i 0 X p i p i + 1 X p 0 p 1
42 41 biimpri X p 0 p 1 i 0 X p i p i + 1
43 42 rgenw p RePart 1 X p 0 p 1 i 0 X p i p i + 1
44 nfv p y
45 nfra1 p p RePart y X p 0 p y i 0 ..^ y X p i p i + 1
46 44 45 nfan p y p RePart y X p 0 p y i 0 ..^ y X p i p i + 1
47 nnnn0 y y 0
48 fzonn0p1 y 0 y 0 ..^ y + 1
49 47 48 syl y y 0 ..^ y + 1
50 49 ad2antrr y p y X p RePart y + 1 X p 0 p y + 1 y 0 ..^ y + 1
51 fveq2 i = y p i = p y
52 fvoveq1 i = y p i + 1 = p y + 1
53 51 52 oveq12d i = y p i p i + 1 = p y p y + 1
54 53 eleq2d i = y X p i p i + 1 X p y p y + 1
55 54 adantl y p y X p RePart y + 1 X p 0 p y + 1 i = y X p i p i + 1 X p y p y + 1
56 peano2nn y y + 1
57 56 adantr y p RePart y + 1 y + 1
58 simpr y p RePart y + 1 p RePart y + 1
59 56 nnnn0d y y + 1 0
60 0elfz y + 1 0 0 0 y + 1
61 59 60 syl y 0 0 y + 1
62 61 adantr y p RePart y + 1 0 0 y + 1
63 57 58 62 iccpartxr y p RePart y + 1 p 0 *
64 nn0fz0 y + 1 0 y + 1 0 y + 1
65 59 64 sylib y y + 1 0 y + 1
66 65 adantr y p RePart y + 1 y + 1 0 y + 1
67 57 58 66 iccpartxr y p RePart y + 1 p y + 1 *
68 63 67 jca y p RePart y + 1 p 0 * p y + 1 *
69 68 adantlr y p y X p RePart y + 1 p 0 * p y + 1 *
70 elico1 p 0 * p y + 1 * X p 0 p y + 1 X * p 0 X X < p y + 1
71 69 70 syl y p y X p RePart y + 1 X p 0 p y + 1 X * p 0 X X < p y + 1
72 simp1 X * p 0 X X < p y + 1 X *
73 72 adantl p y X X * p 0 X X < p y + 1 X *
74 simpl p y X X * p 0 X X < p y + 1 p y X
75 simpr3 p y X X * p 0 X X < p y + 1 X < p y + 1
76 73 74 75 3jca p y X X * p 0 X X < p y + 1 X * p y X X < p y + 1
77 76 ex p y X X * p 0 X X < p y + 1 X * p y X X < p y + 1
78 77 adantl y p y X X * p 0 X X < p y + 1 X * p y X X < p y + 1
79 78 adantr y p y X p RePart y + 1 X * p 0 X X < p y + 1 X * p y X X < p y + 1
80 71 79 sylbid y p y X p RePart y + 1 X p 0 p y + 1 X * p y X X < p y + 1
81 80 impr y p y X p RePart y + 1 X p 0 p y + 1 X * p y X X < p y + 1
82 nn0fz0 y 0 y 0 y
83 47 82 sylib y y 0 y
84 fzelp1 y 0 y y 0 y + 1
85 83 84 syl y y 0 y + 1
86 85 adantr y p RePart y + 1 y 0 y + 1
87 57 58 86 iccpartxr y p RePart y + 1 p y *
88 87 67 jca y p RePart y + 1 p y * p y + 1 *
89 88 ad2ant2r y p y X p RePart y + 1 X p 0 p y + 1 p y * p y + 1 *
90 elico1 p y * p y + 1 * X p y p y + 1 X * p y X X < p y + 1
91 89 90 syl y p y X p RePart y + 1 X p 0 p y + 1 X p y p y + 1 X * p y X X < p y + 1
92 81 91 mpbird y p y X p RePart y + 1 X p 0 p y + 1 X p y p y + 1
93 50 55 92 rspcedvd y p y X p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
94 93 exp43 y p y X p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
95 94 adantr y p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 p y X p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
96 iccpartres y p RePart y + 1 p 0 y RePart y
97 rspsbca p 0 y RePart y p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 [˙ p 0 y / p]˙ X p 0 p y i 0 ..^ y X p i p i + 1
98 vex p V
99 98 resex p 0 y V
100 sbcimg p 0 y V [˙ p 0 y / p]˙ X p 0 p y i 0 ..^ y X p i p i + 1 [˙ p 0 y / p]˙ X p 0 p y [˙ p 0 y / p]˙ i 0 ..^ y X p i p i + 1
101 sbcel2 [˙ p 0 y / p]˙ X p 0 p y X p 0 y / p p 0 p y
102 csbov12g p 0 y V p 0 y / p p 0 p y = p 0 y / p p 0 p 0 y / p p y
103 csbfv12 p 0 y / p p 0 = p 0 y / p p p 0 y / p 0
104 csbvarg p 0 y V p 0 y / p p = p 0 y
105 csbconstg p 0 y V p 0 y / p 0 = 0
106 104 105 fveq12d p 0 y V p 0 y / p p p 0 y / p 0 = p 0 y 0
107 103 106 syl5eq p 0 y V p 0 y / p p 0 = p 0 y 0
108 csbfv12 p 0 y / p p y = p 0 y / p p p 0 y / p y
109 csbconstg p 0 y V p 0 y / p y = y
110 104 109 fveq12d p 0 y V p 0 y / p p p 0 y / p y = p 0 y y
111 108 110 syl5eq p 0 y V p 0 y / p p y = p 0 y y
112 107 111 oveq12d p 0 y V p 0 y / p p 0 p 0 y / p p y = p 0 y 0 p 0 y y
113 102 112 eqtrd p 0 y V p 0 y / p p 0 p y = p 0 y 0 p 0 y y
114 113 eleq2d p 0 y V X p 0 y / p p 0 p y X p 0 y 0 p 0 y y
115 101 114 syl5bb p 0 y V [˙ p 0 y / p]˙ X p 0 p y X p 0 y 0 p 0 y y
116 sbcrex [˙ p 0 y / p]˙ i 0 ..^ y X p i p i + 1 i 0 ..^ y [˙ p 0 y / p]˙ X p i p i + 1
117 sbcel2 [˙ p 0 y / p]˙ X p i p i + 1 X p 0 y / p p i p i + 1
118 csbov12g p 0 y V p 0 y / p p i p i + 1 = p 0 y / p p i p 0 y / p p i + 1
119 csbfv12 p 0 y / p p i = p 0 y / p p p 0 y / p i
120 csbconstg p 0 y V p 0 y / p i = i
121 104 120 fveq12d p 0 y V p 0 y / p p p 0 y / p i = p 0 y i
122 119 121 syl5eq p 0 y V p 0 y / p p i = p 0 y i
123 csbfv12 p 0 y / p p i + 1 = p 0 y / p p p 0 y / p i + 1
124 csbconstg p 0 y V p 0 y / p i + 1 = i + 1
125 104 124 fveq12d p 0 y V p 0 y / p p p 0 y / p i + 1 = p 0 y i + 1
126 123 125 syl5eq p 0 y V p 0 y / p p i + 1 = p 0 y i + 1
127 122 126 oveq12d p 0 y V p 0 y / p p i p 0 y / p p i + 1 = p 0 y i p 0 y i + 1
128 118 127 eqtrd p 0 y V p 0 y / p p i p i + 1 = p 0 y i p 0 y i + 1
129 128 eleq2d p 0 y V X p 0 y / p p i p i + 1 X p 0 y i p 0 y i + 1
130 117 129 syl5bb p 0 y V [˙ p 0 y / p]˙ X p i p i + 1 X p 0 y i p 0 y i + 1
131 130 rexbidv p 0 y V i 0 ..^ y [˙ p 0 y / p]˙ X p i p i + 1 i 0 ..^ y X p 0 y i p 0 y i + 1
132 116 131 syl5bb p 0 y V [˙ p 0 y / p]˙ i 0 ..^ y X p i p i + 1 i 0 ..^ y X p 0 y i p 0 y i + 1
133 115 132 imbi12d p 0 y V [˙ p 0 y / p]˙ X p 0 p y [˙ p 0 y / p]˙ i 0 ..^ y X p i p i + 1 X p 0 y 0 p 0 y y i 0 ..^ y X p 0 y i p 0 y i + 1
134 100 133 bitrd p 0 y V [˙ p 0 y / p]˙ X p 0 p y i 0 ..^ y X p i p i + 1 X p 0 y 0 p 0 y y i 0 ..^ y X p 0 y i p 0 y i + 1
135 99 134 ax-mp [˙ p 0 y / p]˙ X p 0 p y i 0 ..^ y X p i p i + 1 X p 0 y 0 p 0 y y i 0 ..^ y X p 0 y i p 0 y i + 1
136 68 70 syl y p RePart y + 1 X p 0 p y + 1 X * p 0 X X < p y + 1
137 136 adantr y p RePart y + 1 ¬ p y X X p 0 p y + 1 X * p 0 X X < p y + 1
138 72 adantl y p RePart y + 1 ¬ p y X X * p 0 X X < p y + 1 X *
139 simpr2 y p RePart y + 1 ¬ p y X X * p 0 X X < p y + 1 p 0 X
140 xrltnle X * p y * X < p y ¬ p y X
141 72 87 140 syl2anr y p RePart y + 1 X * p 0 X X < p y + 1 X < p y ¬ p y X
142 141 exbiri y p RePart y + 1 X * p 0 X X < p y + 1 ¬ p y X X < p y
143 142 com23 y p RePart y + 1 ¬ p y X X * p 0 X X < p y + 1 X < p y
144 143 imp31 y p RePart y + 1 ¬ p y X X * p 0 X X < p y + 1 X < p y
145 138 139 144 3jca y p RePart y + 1 ¬ p y X X * p 0 X X < p y + 1 X * p 0 X X < p y
146 63 87 jca y p RePart y + 1 p 0 * p y *
147 146 ad2antrr y p RePart y + 1 ¬ p y X X * p 0 X X < p y + 1 p 0 * p y *
148 elico1 p 0 * p y * X p 0 p y X * p 0 X X < p y
149 147 148 syl y p RePart y + 1 ¬ p y X X * p 0 X X < p y + 1 X p 0 p y X * p 0 X X < p y
150 145 149 mpbird y p RePart y + 1 ¬ p y X X * p 0 X X < p y + 1 X p 0 p y
151 150 ex y p RePart y + 1 ¬ p y X X * p 0 X X < p y + 1 X p 0 p y
152 137 151 sylbid y p RePart y + 1 ¬ p y X X p 0 p y + 1 X p 0 p y
153 0elfz y 0 0 0 y
154 47 153 syl y 0 0 y
155 154 adantr y p RePart y + 1 0 0 y
156 fvres 0 0 y p 0 y 0 = p 0
157 155 156 syl y p RePart y + 1 p 0 y 0 = p 0
158 157 eqcomd y p RePart y + 1 p 0 = p 0 y 0
159 83 adantr y p RePart y + 1 y 0 y
160 fvres y 0 y p 0 y y = p y
161 159 160 syl y p RePart y + 1 p 0 y y = p y
162 161 eqcomd y p RePart y + 1 p y = p 0 y y
163 158 162 oveq12d y p RePart y + 1 p 0 p y = p 0 y 0 p 0 y y
164 163 eleq2d y p RePart y + 1 X p 0 p y X p 0 y 0 p 0 y y
165 164 biimpa y p RePart y + 1 X p 0 p y X p 0 y 0 p 0 y y
166 elfzofz i 0 ..^ y i 0 y
167 166 adantl y p RePart y + 1 X p 0 p y i 0 ..^ y i 0 y
168 fvres i 0 y p 0 y i = p i
169 167 168 syl y p RePart y + 1 X p 0 p y i 0 ..^ y p 0 y i = p i
170 fzofzp1 i 0 ..^ y i + 1 0 y
171 170 adantl y p RePart y + 1 i 0 ..^ y i + 1 0 y
172 fvres i + 1 0 y p 0 y i + 1 = p i + 1
173 171 172 syl y p RePart y + 1 i 0 ..^ y p 0 y i + 1 = p i + 1
174 173 adantlr y p RePart y + 1 X p 0 p y i 0 ..^ y p 0 y i + 1 = p i + 1
175 169 174 oveq12d y p RePart y + 1 X p 0 p y i 0 ..^ y p 0 y i p 0 y i + 1 = p i p i + 1
176 175 eleq2d y p RePart y + 1 X p 0 p y i 0 ..^ y X p 0 y i p 0 y i + 1 X p i p i + 1
177 176 rexbidva y p RePart y + 1 X p 0 p y i 0 ..^ y X p 0 y i p 0 y i + 1 i 0 ..^ y X p i p i + 1
178 nnz y y
179 uzid y y y
180 178 179 syl y y y
181 peano2uz y y y + 1 y
182 fzoss2 y + 1 y 0 ..^ y 0 ..^ y + 1
183 180 181 182 3syl y 0 ..^ y 0 ..^ y + 1
184 183 ad2antrr y p RePart y + 1 X p 0 p y 0 ..^ y 0 ..^ y + 1
185 ssrexv 0 ..^ y 0 ..^ y + 1 i 0 ..^ y X p i p i + 1 i 0 ..^ y + 1 X p i p i + 1
186 184 185 syl y p RePart y + 1 X p 0 p y i 0 ..^ y X p i p i + 1 i 0 ..^ y + 1 X p i p i + 1
187 177 186 sylbid y p RePart y + 1 X p 0 p y i 0 ..^ y X p 0 y i p 0 y i + 1 i 0 ..^ y + 1 X p i p i + 1
188 165 187 embantd y p RePart y + 1 X p 0 p y X p 0 y 0 p 0 y y i 0 ..^ y X p 0 y i p 0 y i + 1 i 0 ..^ y + 1 X p i p i + 1
189 188 ex y p RePart y + 1 X p 0 p y X p 0 y 0 p 0 y y i 0 ..^ y X p 0 y i p 0 y i + 1 i 0 ..^ y + 1 X p i p i + 1
190 189 adantr y p RePart y + 1 ¬ p y X X p 0 p y X p 0 y 0 p 0 y y i 0 ..^ y X p 0 y i p 0 y i + 1 i 0 ..^ y + 1 X p i p i + 1
191 152 190 syld y p RePart y + 1 ¬ p y X X p 0 p y + 1 X p 0 y 0 p 0 y y i 0 ..^ y X p 0 y i p 0 y i + 1 i 0 ..^ y + 1 X p i p i + 1
192 191 ex y p RePart y + 1 ¬ p y X X p 0 p y + 1 X p 0 y 0 p 0 y y i 0 ..^ y X p 0 y i p 0 y i + 1 i 0 ..^ y + 1 X p i p i + 1
193 192 com34 y p RePart y + 1 ¬ p y X X p 0 y 0 p 0 y y i 0 ..^ y X p 0 y i p 0 y i + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
194 193 com13 X p 0 y 0 p 0 y y i 0 ..^ y X p 0 y i p 0 y i + 1 ¬ p y X y p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
195 135 194 sylbi [˙ p 0 y / p]˙ X p 0 p y i 0 ..^ y X p i p i + 1 ¬ p y X y p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
196 97 195 syl p 0 y RePart y p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 ¬ p y X y p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
197 196 ex p 0 y RePart y p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 ¬ p y X y p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
198 197 com24 p 0 y RePart y y p RePart y + 1 ¬ p y X p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
199 96 198 mpcom y p RePart y + 1 ¬ p y X p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
200 199 ex y p RePart y + 1 ¬ p y X p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
201 200 com24 y p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 ¬ p y X p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
202 201 imp y p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 ¬ p y X p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
203 95 202 pm2.61d y p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
204 46 203 ralrimi y p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
205 204 ex y p RePart y X p 0 p y i 0 ..^ y X p i p i + 1 p RePart y + 1 X p 0 p y + 1 i 0 ..^ y + 1 X p i p i + 1
206 10 18 26 34 43 205 nnind M p RePart M X p 0 p M i 0 ..^ M X p i p i + 1