Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hspmbllem2 Structured version   Visualization version   Unicode version

Theorem hspmbllem2 38567
 Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (b) of Lemma 115F of [Fremlin1] p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
Hypotheses
Ref Expression
hspmbllem2.h
hspmbllem2.x
hspmbllem2.k
hspmbllem2.y
hspmbllem2.e
hspmbllem2.c
hspmbllem2.d
hspmbllem2.a
hspmbllem2.g Σ^ voln*
hspmbllem2.r voln*
hspmbllem2.i voln*
hspmbllem2.f voln*
hspmbllem2.l
hspmbllem2.t
hspmbllem2.s
Assertion
Ref Expression
hspmbllem2 voln* voln* voln*
Distinct variable groups:   ,,   ,,,,,,   ,,,,,,,   ,,   ,,,,,,,,,   ,,,,   ,,,,   ,,,,,,,,,   ,,,,,,,,,   ,,,,,,,,,
Allowed substitution hints:   (,,,,,,)   (,,)   (,)   (,,,,)   (,,,,)   (,,,,,,,,)   (,,,,,,)   (,,,,,,,,)

Proof of Theorem hspmbllem2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 hspmbllem2.i . . 3 voln*
2 hspmbllem2.f . . 3 voln*
31, 2readdcld 9688 . 2 voln* voln*
4 hspmbllem2.r . . . 4 voln*
5 hspmbllem2.e . . . . 5
65rpred 11364 . . . 4
74, 6readdcld 9688 . . 3 voln*
8 nfv 1769 . . . 4
9 nnex 10637 . . . . 5
109a1i 11 . . . 4
11 icossicc 11746 . . . . 5
12 hspmbllem2.l . . . . . 6
13 hspmbllem2.x . . . . . . 7
1413adantr 472 . . . . . 6
15 hspmbllem2.c . . . . . . . 8
1615ffvelrnda 6037 . . . . . . 7
17 elmapi 7511 . . . . . . 7
1816, 17syl 17 . . . . . 6
19 hspmbllem2.d . . . . . . . 8
2019ffvelrnda 6037 . . . . . . 7
21 elmapi 7511 . . . . . . 7
2220, 21syl 17 . . . . . 6
2312, 14, 18, 22hoidmvcl 38522 . . . . 5
2411, 23sseldi 3416 . . . 4
258, 10, 24sge0clmpt 38381 . . 3 Σ^
26 hspmbllem2.k . . . . . . . . 9
27 ne0i 3728 . . . . . . . . 9
2826, 27syl 17 . . . . . . . 8
2928adantr 472 . . . . . . 7
3012, 14, 29, 18, 22hoidmvn0val 38524 . . . . . 6
3130mpteq2dva 4482 . . . . 5
3231fveq2d 5883 . . . 4 Σ^ Σ^
33 hspmbllem2.g . . . 4 Σ^ voln*
3432, 33eqbrtrd 4416 . . 3 Σ^ voln*
357, 25, 34ge0lere 37730 . 2 Σ^
36 hspmbllem2.t . . . . . . . . 9
37 hspmbllem2.y . . . . . . . . . 10
3837adantr 472 . . . . . . . . 9
3936, 38, 14, 22hsphoif 38516 . . . . . . . 8
4012, 14, 18, 39hoidmvcl 38522 . . . . . . 7
4111, 40sseldi 3416 . . . . . 6
428, 10, 41sge0clmpt 38381 . . . . 5 Σ^
43 oveq2 6316 . . . . . . . . . . 11
44 eqeq1 2475 . . . . . . . . . . . 12
45 prodeq1 14040 . . . . . . . . . . . 12
4644, 45ifbieq2d 3897 . . . . . . . . . . 11
4743, 43, 46mpt2eq123dv 6372 . . . . . . . . . 10
4847cbvmptv 4488 . . . . . . . . 9
4912, 48eqtri 2493 . . . . . . . 8
50 diffi 7821 . . . . . . . . . . 11
5113, 50syl 17 . . . . . . . . . 10
52 snfi 7668 . . . . . . . . . . 11
5352a1i 11 . . . . . . . . . 10
54 unfi 7856 . . . . . . . . . 10
5551, 53, 54syl2anc 673 . . . . . . . . 9
5655adantr 472 . . . . . . . 8
57 snidg 3986 . . . . . . . . . . . 12
5826, 57syl 17 . . . . . . . . . . 11
59 elun2 3593 . . . . . . . . . . 11
6058, 59syl 17 . . . . . . . . . 10
61 neldifsnd 4091 . . . . . . . . . 10
6260, 61eldifd 3401 . . . . . . . . 9
6362adantr 472 . . . . . . . 8
64 eqid 2471 . . . . . . . 8
65 eqid 2471 . . . . . . . 8
66 uncom 3569 . . . . . . . . . . . . 13
6766a1i 11 . . . . . . . . . . . 12
6826snssd 4108 . . . . . . . . . . . . 13
69 undif 3839 . . . . . . . . . . . . 13
7068, 69sylib 201 . . . . . . . . . . . 12
7167, 70eqtrd 2505 . . . . . . . . . . 11
7271adantr 472 . . . . . . . . . 10
7372feq2d 5725 . . . . . . . . 9
7418, 73mpbird 240 . . . . . . . 8
7572feq2d 5725 . . . . . . . . 9
7622, 75mpbird 240 . . . . . . . 8
7749, 56, 63, 64, 38, 65, 74, 76hsphoidmvle 38526 . . . . . . 7
7871fveq2d 5883 . . . . . . . . . 10
79 eqidd 2472 . . . . . . . . . 10
8036a1i 11 . . . . . . . . . . . . 13
8171oveq2d 6324 . . . . . . . . . . . . . . . 16
8271mpteq1d 4477 . . . . . . . . . . . . . . . 16
8381, 82mpteq12dv 4474 . . . . . . . . . . . . . . 15
8483eqcomd 2477 . . . . . . . . . . . . . 14
8584mpteq2dv 4483 . . . . . . . . . . . . 13
8680, 85eqtr2d 2506 . . . . . . . . . . . 12
8786fveq1d 5881 . . . . . . . . . . 11
8887fveq1d 5881 . . . . . . . . . 10
8978, 79, 88oveq123d 6329 . . . . . . . . 9
9089adantr 472 . . . . . . . 8
9178adantr 472 . . . . . . . . 9
9291oveqd 6325 . . . . . . . 8
9390, 92breq12d 4408 . . . . . . 7
9477, 93mpbid 215 . . . . . 6
958, 10, 41, 24, 94sge0lempt 38366 . . . . 5 Σ^ Σ^
9635, 42, 95ge0lere 37730 . . . 4 Σ^
97 hspmbllem2.s . . . . . . . . . 10
9897, 38, 14, 18hoidifhspf 38558 . . . . . . . . 9
9912, 14, 98, 22hoidmvcl 38522 . . . . . . . 8
100 eqid 2471 . . . . . . . 8
10199, 100fmptd 6061 . . . . . . 7
10211a1i 11 . . . . . . 7
103101, 102fssd 5750 . . . . . 6
10410, 103sge0cl 38337 . . . . 5 Σ^
10511, 99sseldi 3416 . . . . . 6
10626adantr 472 . . . . . . 7
10712, 14, 18, 22, 106, 97, 38hoidifhspdmvle 38560 . . . . . 6
1088, 10, 105, 24, 107sge0lempt 38366 . . . . 5 Σ^ Σ^
10935, 104, 108ge0lere 37730 . . . 4 Σ^
11037adantr 472 . . . . . . . . 9
11113adantr 472 . . . . . . . . 9
112 eleq1 2537 . . . . . . . . . . . 12
113112anbi2d 718 . . . . . . . . . . 11
114 fveq2 5879 . . . . . . . . . . . 12
115114feq1d 5724 . . . . . . . . . . 11
116113, 115imbi12d 327 . . . . . . . . . 10
117116, 22chvarv 2120 . . . . . . . . 9
11836, 110, 111, 117hsphoif 38516 . . . . . . . 8
119 reex 9648 . . . . . . . . . . . 12
120119a1i 11 . . . . . . . . . . 11
121120, 13jca 541 . . . . . . . . . 10
122121adantr 472 . . . . . . . . 9
123 elmapg 7503 . . . . . . . . 9
124122, 123syl 17 . . . . . . . 8
125118, 124mpbird 240 . . . . . . 7
126 eqid 2471 . . . . . . 7
127125, 126fmptd 6061 . . . . . 6
128 simpl 464 . . . . . . . . . . . 12
129 elinel1 3610 . . . . . . . . . . . . 13
130129adantl 473 . . . . . . . . . . . 12
131 hspmbllem2.a . . . . . . . . . . . . . 14
132131sselda 3418 . . . . . . . . . . . . 13
133 eliun 4274 . . . . . . . . . . . . 13
134132, 133sylib 201 . . . . . . . . . . . 12
135128, 130, 134syl2anc 673 . . . . . . . . . . 11
136128adantr 472 . . . . . . . . . . . . 13
137 elinel2 3611 . . . . . . . . . . . . . . 15
138137adantl 473 . . . . . . . . . . . . . 14
139138adantr 472 . . . . . . . . . . . . 13
140 simpr 468 . . . . . . . . . . . . 13
141 ixpfn 7546 . . . . . . . . . . . . . . . . 17
142141adantl 473 . . . . . . . . . . . . . . . 16
143 nfv 1769 . . . . . . . . . . . . . . . . . 18
144 nfcv 2612 . . . . . . . . . . . . . . . . . . 19
145 nfixp1 7560 . . . . . . . . . . . . . . . . . . 19
146144, 145nfel 2624 . . . . . . . . . . . . . . . . . 18
147143, 146nfan 2031 . . . . . . . . . . . . . . . . 17
148183adant3 1050 . . . . . . . . . . . . . . . . . . . . . 22
149 simp3 1032 . . . . . . . . . . . . . . . . . . . . . 22
150148, 149ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . 21
151150rexrd 9708 . . . . . . . . . . . . . . . . . . . 20
152151ad5ant135 1280 . . . . . . . . . . . . . . . . . . 19
153393adant3 1050 . . . . . . . . . . . . . . . . . . . . . 22
154153, 149ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . 21
155154rexrd 9708 . . . . . . . . . . . . . . . . . . . 20
156155ad5ant135 1280 . . . . . . . . . . . . . . . . . . 19
157 iftrue 3878 . . . . . . . . . . . . . . . . . . . . . . . 24
158 ioossre 11721 . . . . . . . . . . . . . . . . . . . . . . . . 25
159158a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
160157, 159eqsstrd 3452 . . . . . . . . . . . . . . . . . . . . . . 23
161 iffalse 3881 . . . . . . . . . . . . . . . . . . . . . . . 24
162 ssid 3437 . . . . . . . . . . . . . . . . . . . . . . . . 25
163162a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
164161, 163eqsstrd 3452 . . . . . . . . . . . . . . . . . . . . . . 23
165160, 164pm2.61i 169 . . . . . . . . . . . . . . . . . . . . . 22
166 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25
167 hspmbllem2.h . . . . . . . . . . . . . . . . . . . . . . . . . . 27
168167, 13, 26, 37hspval 38549 . . . . . . . . . . . . . . . . . . . . . . . . . 26
169168adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
170166, 169eleqtrd 2551 . . . . . . . . . . . . . . . . . . . . . . . 24
171170adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
172 simpr 468 . . . . . . . . . . . . . . . . . . . . . . 23
173 vex 3034 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
174173elixp 7547 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
175174biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . . 26
176175simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . 25
177176adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
178 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . 24
179 rspa 2774 . . . . . . . . . . . . . . . . . . . . . . . 24
180177, 178, 179syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . 23
181171, 172, 180syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
182165, 181sseldi 3416 . . . . . . . . . . . . . . . . . . . . 21
183182rexrd 9708 . . . . . . . . . . . . . . . . . . . 20
184183ad4ant14 1259 . . . . . . . . . . . . . . . . . . 19
185151ad4ant124 1261 . . . . . . . . . . . . . . . . . . . . 21
186223adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . 24
187186, 149ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . . 23
188187rexrd 9708 . . . . . . . . . . . . . . . . . . . . . 22
189188ad4ant124 1261 . . . . . . . . . . . . . . . . . . . . 21
190173elixp 7547 . . . . . . . . . . . . . . . . . . . . . . . . . 26
191190biimpi 199 . . . . . . . . . . . . . . . . . . . . . . . . 25
192191simprd 470 . . . . . . . . . . . . . . . . . . . . . . . 24
193192adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
194 simpr 468 . . . . . . . . . . . . . . . . . . . . . . 23
195 rspa 2774 . . . . . . . . . . . . . . . . . . . . . . 23
196193, 194, 195syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
197196adantll 728 . . . . . . . . . . . . . . . . . . . . 21
198 icogelb 11711 . . . . . . . . . . . . . . . . . . . . 21
199185, 189, 197, 198syl3anc 1292 . . . . . . . . . . . . . . . . . . . 20
200199ad5ant1345 1282 . . . . . . . . . . . . . . . . . . 19
201 icoltub 37703 . . . . . . . . . . . . . . . . . . . . . . . . 25
202185, 189, 197, 201syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . 24
203202ad5ant1345 1282 . . . . . . . . . . . . . . . . . . . . . . 23
204203ad2antrr 740 . . . . . . . . . . . . . . . . . . . . . 22
205 simpll 768 . . . . . . . . . . . . . . . . . . . . . . . . . 26
206 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26
207205, 206jca 541 . . . . . . . . . . . . . . . . . . . . . . . . 25
2082073ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . 24
209 simp2 1031 . . . . . . . . . . . . . . . . . . . . . . . 24
210 simp3 1032 . . . . . . . . . . . . . . . . . . . . . . . 24
211 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
212211breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
213212biimpa 492 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
214213iftrued 3880 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
215211eqcomd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
216215adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
217214, 216eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2182173adant1 1048 . . . . . . . . . . . . . . . . . . . . . . . . 25
219 breq2 4399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
220 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
221219, 220ifbieq2d 3897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
222221ifeq2d 3891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
223222mpteq2dv 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
224223mpteq2dv 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
225224adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
226 ovex 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
227226mptex 6152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
228227a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
22980, 225, 37, 228fvmptd 5969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
230229adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
231 fveq1 5878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
232231breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
233232, 231ifbieq1d 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
234231, 233ifeq12d 3892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
235234mpteq2dv 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
236235adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
237 mptexg 6151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
23813, 237syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
239238adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
240230, 236, 20, 239fvmptd 5969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
241240fveq1d 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2422413adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
243 simpl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
244 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
245243, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
246244, 245eqeltrd 2549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
247 eqidd 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
248 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
249 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
250249breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
251250, 249ifbieq1d 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
252248, 249, 251ifbieq12d 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
253252adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
254 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
255 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
256255a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
257 ifexg 3941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
258256, 37, 257syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
259 ifexg 3941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
260256, 258, 259syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
261260adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
262247, 253, 254, 261fvmptd 5969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
263243, 246, 262syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
264 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
265212, 211ifbieq1d 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
266264, 211, 265ifbieq12d 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
267266adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
268263, 267eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2692683adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
270 neldifsnd 4091 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
271270iffalsed 3883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2722713ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
273242, 269, 2723eqtrrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2742733expa 1231 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2752743adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . 25
276218, 275eqtr3d 2507 . . . . . . . . . . . . . . . . . . . . . . . 24
277208, 209, 210, 276syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . 23
278277ad5ant145 1281 . . . . . . . . . . . . . . . . . . . . . 22
279204, 278breqtrd 4420 . . . . . . . . . . . . . . . . . . . . 21
280 mnfxr 11437 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
281280a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
28237rexrd 9708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
283282adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2842833ad2ant1 1051 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2851813adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2861573ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
287285, 286eleqtrd 2551 . . . . . . . . . . . . . . . . . . . . . . . . . 26
288 iooltub 37706 . . . . . . . . . . . . . . . . . . . . . . . . . 26
289281, 284, 287, 288syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . . . 25
2902893adant1r 1285 . . . . . . . . . . . . . . . . . . . . . . . 24
291290ad4ant123 1260 . . . . . . . . . . . . . . . . . . . . . . 23
292 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
293212notbid 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
294293adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
295292, 294mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
296295iffalsed 3883 . . . . . . . . . . . . . . . . . . . . . . . . . 26
297 eqidd 2472 . . . . . . . . . . . . . . . . . . . . . . . . . 26
298296, 297eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . . . . . 25
299298adantll 728 . . . . . . . . . . . . . . . . . . . . . . . 24
300274adantlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26
301300adantlllr 37424 . . . . . . . . . . . . . . . . . . . . . . . . 25
302301adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
303299, 302eqtrd 2505 . . . . . . . . . . . . . . . . . . . . . . 23
304291, 303breqtrd 4420 . . . . . . . . . . . . . . . . . . . . . 22
305304ad5ant1345 1282 . . . . . . . . . . . . . . . . . . . . 21
306279, 305pm2.61dan 808 . . . . . . . . . . . . . . . . . . . 20
307203adantr 472 . . . . . . . . . . . . . . . . . . . . 21
3082403adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . . . 26
309252adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3102613adant2 1049 . . . . . . . . . . . . . . . . . . . . . . . . . 26
311308, 309, 149, 310fvmptd 5969 . . . . . . . . . . . . . . . . . . . . . . . . 25
3123113expa 1231 . . . . . . . . . . . . . . . . . . . . . . . 24
313312adantllr 733 . . . . . . . . . . . . . . . . . . . . . . 23
314313ad4ant13 1258 . . . . . . . . . . . . . . . . . . . . . 22
315 simpl 464 . . . . . . . . . . . . . . . . . . . . . . . . 25
316 neqne 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
317 nelsn 3992 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
318316, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26
319318adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25
320315, 319eldifd 3401 . . . . . . . . . . . . . . . . . . . . . . . 24
321320iftrued 3880 . . . . . . . . . . . . . . . . . . . . . . 23
322321adantll 728 . . . . . . . . . . . . . . . . . . . . . 22
323314, 322eqtr2d 2506 . . . . . . . . . . . . . . . . . . . . 21