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

Theorem ovnhoilem1 38433
 Description: The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. First part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
ovnhoilem1.x
ovnhoilem1.a
ovnhoilem1.b
ovnhoilem1.c
ovnhoilem1.m Σ^
ovnhoilem1.h
Assertion
Ref Expression
ovnhoilem1 voln*
Distinct variable groups:   ,,,   ,,,   ,,   ,,   ,,,,   ,,
Allowed substitution hints:   (,)   ()   ()   (,)   (,)   (,,,)

Proof of Theorem ovnhoilem1
StepHypRef Expression
1 ovnhoilem1.x . . 3
2 ovnhoilem1.c . . . . 5
32a1i 11 . . . 4
4 nfv 1763 . . . . 5
5 ovnhoilem1.a . . . . . 6
65ffvelrnda 6027 . . . . 5
7 ovnhoilem1.b . . . . . . 7
87ffvelrnda 6027 . . . . . 6
98rexrd 9695 . . . . 5
104, 6, 9hoissrrn2 38410 . . . 4
113, 10eqsstrd 3468 . . 3
12 ovnhoilem1.m . . 3 Σ^
131, 11, 12ovnval2 38377 . 2 voln* inf
14 iftrue 3889 . . . . 5 inf
1514adantl 468 . . . 4 inf
16 0xr 9692 . . . . . . 7
1716a1i 11 . . . . . 6
18 pnfxr 11419 . . . . . . 7
1918a1i 11 . . . . . 6
204, 1, 6, 8hoiprodcl3 38412 . . . . . 6
21 icogelb 11693 . . . . . 6
2217, 19, 20, 21syl3anc 1269 . . . . 5
2322adantr 467 . . . 4
2415, 23eqbrtrd 4426 . . 3 inf
25 iffalse 3892 . . . . 5 inf inf
2625adantl 468 . . . 4 inf inf
27 ssrab2 3516 . . . . . . 7 Σ^
2812, 27eqsstri 3464 . . . . . 6
2928a1i 11 . . . . 5
30 icossxr 11726 . . . . . . . . . 10
3130, 20sseldi 3432 . . . . . . . . 9
3231adantr 467 . . . . . . . 8
33 opelxpi 4869 . . . . . . . . . . . . . . . . 17
346, 8, 33syl2anc 667 . . . . . . . . . . . . . . . 16
35 0re 9648 . . . . . . . . . . . . . . . . . 18
36 opelxpi 4869 . . . . . . . . . . . . . . . . . 18
3735, 35, 36mp2an 679 . . . . . . . . . . . . . . . . 17
3837a1i 11 . . . . . . . . . . . . . . . 16
3934, 38ifcld 3926 . . . . . . . . . . . . . . 15
40 eqid 2453 . . . . . . . . . . . . . . 15
4139, 40fmptd 6051 . . . . . . . . . . . . . 14
42 reex 9635 . . . . . . . . . . . . . . . . 17
4342, 42xpex 6600 . . . . . . . . . . . . . . . 16
441, 43jctil 540 . . . . . . . . . . . . . . 15
45 elmapg 7490 . . . . . . . . . . . . . . 15
4644, 45syl 17 . . . . . . . . . . . . . 14
4741, 46mpbird 236 . . . . . . . . . . . . 13
4847adantr 467 . . . . . . . . . . . 12
49 ovnhoilem1.h . . . . . . . . . . . 12
5048, 49fmptd 6051 . . . . . . . . . . 11
51 ovex 6323 . . . . . . . . . . . 12
52 nnex 10622 . . . . . . . . . . . 12
5351, 52elmap 7505 . . . . . . . . . . 11
5450, 53sylibr 216 . . . . . . . . . 10
5554adantr 467 . . . . . . . . 9
56 eqidd 2454 . . . . . . . . . . . . 13
57 eqid 2453 . . . . . . . . . . . . . . . . . . 19
5834, 57fmptd 6051 . . . . . . . . . . . . . . . . . 18
5949a1i 11 . . . . . . . . . . . . . . . . . . . 20
60 iftrue 3889 . . . . . . . . . . . . . . . . . . . . . 22
6160mpteq2dv 4493 . . . . . . . . . . . . . . . . . . . . 21
6261adantl 468 . . . . . . . . . . . . . . . . . . . 20
63 1nn 10627 . . . . . . . . . . . . . . . . . . . . 21
6463a1i 11 . . . . . . . . . . . . . . . . . . . 20
65 mptexg 6140 . . . . . . . . . . . . . . . . . . . . 21
661, 65syl 17 . . . . . . . . . . . . . . . . . . . 20
6759, 62, 64, 66fvmptd 5959 . . . . . . . . . . . . . . . . . . 19
6867feq1d 5719 . . . . . . . . . . . . . . . . . 18
6958, 68mpbird 236 . . . . . . . . . . . . . . . . 17
7069adantr 467 . . . . . . . . . . . . . . . 16
71 simpr 463 . . . . . . . . . . . . . . . 16
7270, 71fvovco 37479 . . . . . . . . . . . . . . 15
7334elexd 3058 . . . . . . . . . . . . . . . . . . 19
7467, 73fvmpt2d 5964 . . . . . . . . . . . . . . . . . 18
7574fveq2d 5874 . . . . . . . . . . . . . . . . 17
76 fvex 5880 . . . . . . . . . . . . . . . . . . 19
77 fvex 5880 . . . . . . . . . . . . . . . . . . 19
7876, 77op1st 6806 . . . . . . . . . . . . . . . . . 18
7978a1i 11 . . . . . . . . . . . . . . . . 17
8075, 79eqtrd 2487 . . . . . . . . . . . . . . . 16
8174fveq2d 5874 . . . . . . . . . . . . . . . . 17
8276, 77op2nd 6807 . . . . . . . . . . . . . . . . . 18
8382a1i 11 . . . . . . . . . . . . . . . . 17
8481, 83eqtrd 2487 . . . . . . . . . . . . . . . 16
8580, 84oveq12d 6313 . . . . . . . . . . . . . . 15
8672, 85eqtrd 2487 . . . . . . . . . . . . . 14
8786ixpeq2dva 7542 . . . . . . . . . . . . 13
8856, 3, 873eqtr4d 2497 . . . . . . . . . . . 12
89 fveq2 5870 . . . . . . . . . . . . . . . . 17
9089coeq2d 5000 . . . . . . . . . . . . . . . 16
9190fveq1d 5872 . . . . . . . . . . . . . . 15
9291ixpeq2dv 7543 . . . . . . . . . . . . . 14
9392ssiun2s 4325 . . . . . . . . . . . . 13
9463, 93ax-mp 5 . . . . . . . . . . . 12
9588, 94syl6eqss 3484 . . . . . . . . . . 11
9695adantr 467 . . . . . . . . . 10
9786fveq2d 5874 . . . . . . . . . . . . . 14
9897eqcomd 2459 . . . . . . . . . . . . 13
9998prodeq2dv 13989 . . . . . . . . . . . 12
10099adantr 467 . . . . . . . . . . 11
101 1red 9663 . . . . . . . . . . . . . 14
102 icossicc 11728 . . . . . . . . . . . . . . 15
1034, 1, 69hoiprodcl 38379 . . . . . . . . . . . . . . 15
104102, 103sseldi 3432 . . . . . . . . . . . . . 14
10591fveq2d 5874 . . . . . . . . . . . . . . 15
106105prodeq2ad 37682 . . . . . . . . . . . . . 14
107101, 104, 106sge0snmpt 38235 . . . . . . . . . . . . 13 Σ^
108107eqcomd 2459 . . . . . . . . . . . 12 Σ^
109108adantr 467 . . . . . . . . . . 11 Σ^
110 nfv 1763 . . . . . . . . . . . 12
11152a1i 11 . . . . . . . . . . . 12
112 snssi 4119 . . . . . . . . . . . . . 14
11363, 112ax-mp 5 . . . . . . . . . . . . 13
114113a1i 11 . . . . . . . . . . . 12
115 nfv 1763 . . . . . . . . . . . . . 14
1161ad2antrr 733 . . . . . . . . . . . . . 14
117 simpl 459 . . . . . . . . . . . . . . . 16
118 elsni 3995 . . . . . . . . . . . . . . . . 17
119118adantl 468 . . . . . . . . . . . . . . . 16
12069adantr 467 . . . . . . . . . . . . . . . . 17
12189adantl 468 . . . . . . . . . . . . . . . . . 18
122121feq1d 5719 . . . . . . . . . . . . . . . . 17
123120, 122mpbird 236 . . . . . . . . . . . . . . . 16
124117, 119, 123syl2anc 667 . . . . . . . . . . . . . . 15
125124adantlr 722 . . . . . . . . . . . . . 14
126115, 116, 125hoiprodcl 38379 . . . . . . . . . . . . 13
127102, 126sseldi 3432 . . . . . . . . . . . 12
128 eqid 2453 . . . . . . . . . . . . . . . . . . . . . . 23
12938, 128fmptd 6051 . . . . . . . . . . . . . . . . . . . . . 22
130129adantr 467 . . . . . . . . . . . . . . . . . . . . 21
131 simpl 459 . . . . . . . . . . . . . . . . . . . . . . . 24
132 eldifi 3557 . . . . . . . . . . . . . . . . . . . . . . . . 25
133132adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24
13448elexd 3058 . . . . . . . . . . . . . . . . . . . . . . . . 25
13559, 134fvmpt2d 5964 . . . . . . . . . . . . . . . . . . . . . . . 24
136131, 133, 135syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . 23
137 eldifsni 4101 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
138137neneqd 2631 . . . . . . . . . . . . . . . . . . . . . . . . . 26
139138iffalsed 3894 . . . . . . . . . . . . . . . . . . . . . . . . 25
140139mpteq2dv 4493 . . . . . . . . . . . . . . . . . . . . . . . 24
141140adantl 468 . . . . . . . . . . . . . . . . . . . . . . 23
142136, 141eqtrd 2487 . . . . . . . . . . . . . . . . . . . . . 22
143142feq1d 5719 . . . . . . . . . . . . . . . . . . . . 21
144130, 143mpbird 236 . . . . . . . . . . . . . . . . . . . 20
145144adantr 467 . . . . . . . . . . . . . . . . . . 19
146 simpr 463 . . . . . . . . . . . . . . . . . . 19
147145, 146fvovco 37479 . . . . . . . . . . . . . . . . . 18
14837elexi 3057 . . . . . . . . . . . . . . . . . . . . . . 23
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
150142, 149fvmpt2d 5964 . . . . . . . . . . . . . . . . . . . . 21
151150fveq2d 5874 . . . . . . . . . . . . . . . . . . . 20
15216elexi 3057 . . . . . . . . . . . . . . . . . . . . . 22
153152, 152op1st 6806 . . . . . . . . . . . . . . . . . . . . 21
154153a1i 11 . . . . . . . . . . . . . . . . . . . 20
155151, 154eqtrd 2487 . . . . . . . . . . . . . . . . . . 19
156150fveq2d 5874 . . . . . . . . . . . . . . . . . . . 20
157152, 152op2nd 6807 . . . . . . . . . . . . . . . . . . . . 21
158157a1i 11 . . . . . . . . . . . . . . . . . . . 20
159156, 158eqtrd 2487 . . . . . . . . . . . . . . . . . . 19
160155, 159oveq12d 6313 . . . . . . . . . . . . . . . . . 18
161 0le0 10706 . . . . . . . . . . . . . . . . . . . 20
162 ico0 11689 . . . . . . . . . . . . . . . . . . . . 21
16316, 16, 162mp2an 679 . . . . . . . . . . . . . . . . . . . 20
164161, 163mpbir 213 . . . . . . . . . . . . . . . . . . 19
165164a1i 11 . . . . . . . . . . . . . . . . . 18
166147, 160, 1653eqtrd 2491 . . . . . . . . . . . . . . . . 17
167166fveq2d 5874 . . . . . . . . . . . . . . . 16
168 vol0 37846 . . . . . . . . . . . . . . . . 17
169168a1i 11 . . . . . . . . . . . . . . . 16
170167, 169eqtrd 2487 . . . . . . . . . . . . . . 15
171170prodeq2dv 13989 . . . . . . . . . . . . . 14
172171adantlr 722 . . . . . . . . . . . . 13
173 0cnd 9641 . . . . . . . . . . . . . . 15
174 fprodconst 14044 . . . . . . . . . . . . . . 15
1751, 173, 174syl2anc 667 . . . . . . . . . . . . . 14
176175ad2antrr 733 . . . . . . . . . . . . 13
177 neqne 37384 . . . . . . . . . . . . . . . . 17
178177adantl 468 . . . . . . . . . . . . . . . 16
1791adantr 467 . . . . . . . . . . . . . . . . 17
180 hashnncl 12554 . . . . . . . . . . . . . . . . 17
181179, 180syl 17 . . . . . . . . . . . . . . . 16
182178, 181mpbird 236 . . . . . . . . . . . . . . 15
183 0exp 12314 . . . . . . . . . . . . . . 15
184182, 183syl 17 . . . . . . . . . . . . . 14
185184adantr 467 . . . . . . . . . . . . 13
186172, 176, 1853eqtrd 2491 . . . . . . . . . . . 12
187110, 111, 114, 127, 186sge0ss 38264 . . . . . . . . . . 11 Σ^ Σ^
188100, 109, 1873eqtrd 2491 . . . . . . . . . 10 Σ^
18996, 188jca 535 . . . . . . . . 9 Σ^
190 nfcv 2594 . . . . . . . . . . . . . . 15
191 nfcv 2594 . . . . . . . . . . . . . . . . 17
192 nfmpt1 4495 . . . . . . . . . . . . . . . . 17
193191, 192nfmpt 4494 . . . . . . . . . . . . . . . 16
19449, 193nfcxfr 2592 . . . . . . . . . . . . . . 15
195190, 194nfeq 2605 . . . . . . . . . . . . . 14
196 fveq1 5869 . . . . . . . . . . . . . . . . 17
197196coeq2d 5000 . . . . . . . . . . . . . . . 16
198197fveq1d 5872 . . . . . . . . . . . . . . 15
199198adantr 467 . . . . . . . . . . . . . 14
200195, 199ixpeq2d 37420 . . . . . . . . . . . . 13
201200iuneq2d 4308 . . . . . . . . . . . 12
202201sseq2d 3462 . . . . . . . . . . 11
203198fveq2d 5874 . . . . . . . . . . . . . . . . 17
204203a1d 26 . . . . . . . . . . . . . . . 16
205195, 204ralrimi 2790 . . . . . . . . . . . . . . 15
206205prodeq2d 13988 . . . . . . . . . . . . . 14
207206mpteq2dv 4493 . . . . . . . . . . . . 13
208207fveq2d 5874 . . . . . . . . . . . 12 Σ^ Σ^
209208eqeq2d 2463 . . . . . . . . . . 11 Σ^ Σ^
210202, 209anbi12d 718 . . . . . . . . . 10 Σ^ Σ^
211210rspcev 3152 . . . . . . . . 9 Σ^ Σ^
21255, 189, 211syl2anc 667 . . . . . . . 8 Σ^
21332, 212jca 535 . . . . . . 7 Σ^
214 eqeq1 2457 . . . . . . . . . 10 Σ^ Σ^
215214anbi2d 711 . . . . . . . . 9 Σ^ Σ^
216215rexbidv 2903 . . . . . . . 8 Σ^ Σ^
217216elrab 3198 . . . . . . 7 Σ^ Σ^
218213, 217sylibr 216 . . . . . 6 Σ^
21912eqcomi 2462 . . . . . . 7 Σ^
220219a1i 11 . . . . . 6 Σ^
221218, 220eleqtrd 2533 . . . . 5
222 infxrlb 11627 . . . . 5 inf
22329, 221, 222syl2anc 667 . . . 4 inf
22426, 223eqbrtrd 4426 . . 3 inf
22524, 224pm2.61dan 801 . 2 inf
22613, 225eqbrtrd 4426 1 voln*
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 188   wa 371   wceq 1446   wcel 1889   wne 2624  wrex 2740  crab 2743  cvv 3047   cdif 3403   wss 3406  c0 3733  cif 3883  csn 3970  cop 3976  ciun 4281   class class class wbr 4405   cmpt 4464   cxp 4835   ccom 4841  wf 5581  cfv 5585  (class class class)co 6295  c1st 6796  c2nd 6797   cmap 7477  cixp 7527  cfn 7574  infcinf 7960  cc 9542  cr 9543  cc0 9544  c1 9545   cpnf 9677  cxr 9679   clt 9680   cle 9681  cn 10616  cico 11644  cicc 11645  cexp 12279  chash 12522  cprod 13971  cvol 22427  Σ^csumge0 38214  voln*covoln 38367 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-inf2 8151  ax-cnex 9600  ax-resscn 9601  ax-1cn 9602  ax-icn 9603  ax-addcl 9604  ax-addrcl 9605  ax-mulcl 9606  ax-mulrcl 9607  ax-mulcom 9608  ax-addass 9609  ax-mulass 9610  ax-distr 9611  ax-i2m1 9612  ax-1ne0 9613  ax-1rid 9614  ax-rnegex 9615  ax-rrecex 9616  ax-cnre 9617  ax-pre-lttri 9618  ax-pre-lttrn 9619  ax-pre-ltadd 9620  ax-pre-mulgt0 9621  ax-pre-sup 9622 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-fal 1452  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-nel 2627  df-ral 2744  df-rex 2745  df-reu 2746  df-rmo 2747  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-int 4238  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-se 4797  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-isom 5594  df-riota 6257  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6536  df-om 6698  df-1st 6798  df-2nd 6799  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-2o 7188  df-oadd 7191  df-er 7368  df-map 7479  df-pm 7480  df-ixp 7528  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-fi 7930  df-sup 7961  df-inf 7962  df-oi 8030  df-card 8378  df-cda 8603  df-pnf 9682  df-mnf 9683  df-xr 9684  df-ltxr 9685  df-le 9686  df-sub 9867  df-neg 9868  df-div 10277  df-nn 10617  df-2 10675  df-3 10676  df-n0 10877  df-z 10945  df-uz 11167  df-q 11272  df-rp 11310  df-xneg 11416  df-xadd 11417  df-xmul 11418  df-ioo 11646  df-ico 11648  df-icc 11649  df-fz 11792  df-fzo 11923  df-fl 12035  df-seq 12221  df-exp 12280  df-hash 12523  df-cj 13174  df-re 13175  df-im 13176  df-sqrt 13310  df-abs 13311  df-clim 13564  df-rlim 13565  df-sum 13765  df-prod 13972  df-rest 15333  df-topgen 15354  df-psmet 18974  df-xmet 18975  df-met 18976  df-bl 18977  df-mopn 18978  df-top 19933  df-bases 19934  df-topon 19935  df-cmp 20414  df-ovol 22428  df-vol 22430  df-sumge0 38215  df-ovoln 38368 This theorem is referenced by:  ovnhoi  38435
 Copyright terms: Public domain W3C validator