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

Theorem ovnhoilem2 38434
 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. Second part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
ovnhoilem2.x
ovnhoilem2.n
ovnhoilem2.a
ovnhoilem2.b
ovnhoilem2.i
ovnhoilem2.l
ovnhoilem2.m Σ^
ovnhoilem2.f
ovnhoilem2.s
Assertion
Ref Expression
ovnhoilem2 voln*
Distinct variable groups:   ,,,,,   ,,,,,   ,,   ,,,,,,   ,,,,,,   ,,   ,,   ,,,,,,,   ,,,,   ,,,,,,   ,,
Allowed substitution hints:   ()   (,,,)   (,,,)   (,,,,,,)   (,,,,,,)   (,,)   (,,)   (,,,,,,)

Proof of Theorem ovnhoilem2
StepHypRef Expression
1 ovnhoilem2.m . . . . . . . . . 10 Σ^
21eleq2i 2523 . . . . . . . . 9 Σ^
3 rabid 2969 . . . . . . . . 9 Σ^ Σ^
42, 3bitri 253 . . . . . . . 8 Σ^
54biimpi 198 . . . . . . 7 Σ^
65simprd 465 . . . . . 6 Σ^
76adantl 468 . . . . 5 Σ^
8 ovnhoilem2.l . . . . . . . . . 10
9 ovnhoilem2.x . . . . . . . . . . 11
1093ad2ant1 1030 . . . . . . . . . 10 Σ^
11 ovnhoilem2.a . . . . . . . . . . 11
12113ad2ant1 1030 . . . . . . . . . 10 Σ^
13 ovnhoilem2.b . . . . . . . . . . 11
14133ad2ant1 1030 . . . . . . . . . 10 Σ^
15 elmapi 7498 . . . . . . . . . . . . . . . . . . 19
1615ffvelrnda 6027 . . . . . . . . . . . . . . . . . 18
17 elmapi 7498 . . . . . . . . . . . . . . . . . 18
1816, 17syl 17 . . . . . . . . . . . . . . . . 17
1918ffvelrnda 6027 . . . . . . . . . . . . . . . 16
20 xp1st 6828 . . . . . . . . . . . . . . . 16
2119, 20syl 17 . . . . . . . . . . . . . . 15
22 eqid 2453 . . . . . . . . . . . . . . 15
2321, 22fmptd 6051 . . . . . . . . . . . . . 14
24 reex 9635 . . . . . . . . . . . . . . . 16
2524a1i 11 . . . . . . . . . . . . . . 15
26 1nn 10627 . . . . . . . . . . . . . . . . . . 19
2726a1i 11 . . . . . . . . . . . . . . . . . 18
2815, 27ffvelrnd 6028 . . . . . . . . . . . . . . . . 17
29 elmapex 7497 . . . . . . . . . . . . . . . . . 18
3029simprd 465 . . . . . . . . . . . . . . . . 17
3128, 30syl 17 . . . . . . . . . . . . . . . 16
3231adantr 467 . . . . . . . . . . . . . . 15
33 elmapg 7490 . . . . . . . . . . . . . . 15
3425, 32, 33syl2anc 667 . . . . . . . . . . . . . 14
3523, 34mpbird 236 . . . . . . . . . . . . 13
36 eqid 2453 . . . . . . . . . . . . 13
3735, 36fmptd 6051 . . . . . . . . . . . 12
38 id 22 . . . . . . . . . . . . . 14
39 nnex 10622 . . . . . . . . . . . . . . . 16
4039mptex 6141 . . . . . . . . . . . . . . 15
4140a1i 11 . . . . . . . . . . . . . 14
42 ovnhoilem2.f . . . . . . . . . . . . . . 15
4342fvmpt2 5962 . . . . . . . . . . . . . 14
4438, 41, 43syl2anc 667 . . . . . . . . . . . . 13
4544feq1d 5719 . . . . . . . . . . . 12
4637, 45mpbird 236 . . . . . . . . . . 11
47463ad2ant2 1031 . . . . . . . . . 10 Σ^
48 xp2nd 6829 . . . . . . . . . . . . . . . 16
4919, 48syl 17 . . . . . . . . . . . . . . 15
50 eqid 2453 . . . . . . . . . . . . . . 15
5149, 50fmptd 6051 . . . . . . . . . . . . . 14
52 elmapg 7490 . . . . . . . . . . . . . . 15
5325, 32, 52syl2anc 667 . . . . . . . . . . . . . 14
5451, 53mpbird 236 . . . . . . . . . . . . 13
55 eqid 2453 . . . . . . . . . . . . 13
5654, 55fmptd 6051 . . . . . . . . . . . 12
5739mptex 6141 . . . . . . . . . . . . . . 15
5857a1i 11 . . . . . . . . . . . . . 14
59 ovnhoilem2.s . . . . . . . . . . . . . . 15
6059fvmpt2 5962 . . . . . . . . . . . . . 14
6138, 58, 60syl2anc 667 . . . . . . . . . . . . 13
6261feq1d 5719 . . . . . . . . . . . 12
6356, 62mpbird 236 . . . . . . . . . . 11
64633ad2ant2 1031 . . . . . . . . . 10 Σ^
65 simp3 1011 . . . . . . . . . . . 12
66 ovnhoilem2.i . . . . . . . . . . . . . 14
6766a1i 11 . . . . . . . . . . . . 13
68 fveq2 5870 . . . . . . . . . . . . . . . . . . . . . 22
6968fveq1d 5872 . . . . . . . . . . . . . . . . . . . . 21
7069fveq2d 5874 . . . . . . . . . . . . . . . . . . . 20
7169fveq2d 5874 . . . . . . . . . . . . . . . . . . . 20
7270, 71oveq12d 6313 . . . . . . . . . . . . . . . . . . 19
7372ixpeq2dv 7543 . . . . . . . . . . . . . . . . . 18
7473cbviunv 4320 . . . . . . . . . . . . . . . . 17
7574a1i 11 . . . . . . . . . . . . . . . 16
7615ffvelrnda 6027 . . . . . . . . . . . . . . . . . . . . 21
77 elmapi 7498 . . . . . . . . . . . . . . . . . . . . 21
7876, 77syl 17 . . . . . . . . . . . . . . . . . . . 20
7978adantr 467 . . . . . . . . . . . . . . . . . . 19
80 simpr 463 . . . . . . . . . . . . . . . . . . 19
8179, 80fvovco 37479 . . . . . . . . . . . . . . . . . 18
8281ixpeq2dva 7542 . . . . . . . . . . . . . . . . 17
8382iuneq2dv 4303 . . . . . . . . . . . . . . . 16
84 simpl 459 . . . . . . . . . . . . . . . . . . . . . . . . 25
8540a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
8684, 85, 43syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . 24
8786fveq1d 5872 . . . . . . . . . . . . . . . . . . . . . . 23
88 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . 24
89 mptexg 6140 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9031, 89syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25
9190adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24
9236fvmpt2 5962 . . . . . . . . . . . . . . . . . . . . . . . 24
9388, 91, 92syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . 23
9487, 93eqtrd 2487 . . . . . . . . . . . . . . . . . . . . . 22
9594fveq1d 5872 . . . . . . . . . . . . . . . . . . . . 21
9695adantr 467 . . . . . . . . . . . . . . . . . . . 20
97 eqidd 2454 . . . . . . . . . . . . . . . . . . . . . 22
98 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . 24
9998fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23
10099fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . 22
101 simpr 463 . . . . . . . . . . . . . . . . . . . . . 22
102 fvex 5880 . . . . . . . . . . . . . . . . . . . . . . 23
103102a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
10497, 100, 101, 103fvmptd 5959 . . . . . . . . . . . . . . . . . . . . 21
105104adantlr 722 . . . . . . . . . . . . . . . . . . . 20
10696, 105eqtrd 2487 . . . . . . . . . . . . . . . . . . 19
10761fveq1d 5872 . . . . . . . . . . . . . . . . . . . . . . . 24
108107adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23
109 mptexg 6140 . . . . . . . . . . . . . . . . . . . . . . . . . 26
11031, 109syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25
111110adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24
11255fvmpt2 5962 . . . . . . . . . . . . . . . . . . . . . . . 24
11388, 111, 112syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . 23
114108, 113eqtrd 2487 . . . . . . . . . . . . . . . . . . . . . 22
115114fveq1d 5872 . . . . . . . . . . . . . . . . . . . . 21
116115adantr 467 . . . . . . . . . . . . . . . . . . . 20
117 eqidd 2454 . . . . . . . . . . . . . . . . . . . . . 22
118 fveq2 5870 . . . . . . . . . . . . . . . . . . . . . . . 24
119118fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23
120119adantl 468 . . . . . . . . . . . . . . . . . . . . . 22
121 fvex 5880 . . . . . . . . . . . . . . . . . . . . . . 23
122121a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
123117, 120, 101, 122fvmptd 5959 . . . . . . . . . . . . . . . . . . . . 21
124123adantlr 722 . . . . . . . . . . . . . . . . . . . 20
125116, 124eqtrd 2487 . . . . . . . . . . . . . . . . . . 19
126106, 125oveq12d 6313 . . . . . . . . . . . . . . . . . 18
127126ixpeq2dva 7542 . . . . . . . . . . . . . . . . 17
128127iuneq2dv 4303 . . . . . . . . . . . . . . . 16
12975, 83, 1283eqtr4d 2497 . . . . . . . . . . . . . . 15
130129adantl 468 . . . . . . . . . . . . . 14
1311303adant3 1029 . . . . . . . . . . . . 13
13267, 131sseq12d 3463 . . . . . . . . . . . 12
13365, 132mpbid 214 . . . . . . . . . . 11
1341333adant3r 1266 . . . . . . . . . 10 Σ^
1358, 10, 12, 14, 47, 64, 134hoidmvle 38432 . . . . . . . . 9 Σ^ Σ^
136 simpl 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26
137136fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . . . 25
138137fveq1d 5872 . . . . . . . . . . . . . . . . . . . . . . . 24
139138fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23
140139mpteq2dva 4492 . . . . . . . . . . . . . . . . . . . . . 22
141140fveq1d 5872 . . . . . . . . . . . . . . . . . . . . 21
142141adantr 467 . . . . . . . . . . . . . . . . . . . 20
143 eqidd 2454 . . . . . . . . . . . . . . . . . . . . . 22
144 fveq2 5870 . . . . . . . . . . . . . . . . . . . . . . . 24
145144fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23
146145adantl 468 . . . . . . . . . . . . . . . . . . . . . 22
147 id 22 . . . . . . . . . . . . . . . . . . . . . 22
148 fvex 5880 . . . . . . . . . . . . . . . . . . . . . . 23
149148a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
150143, 146, 147, 149fvmptd 5959 . . . . . . . . . . . . . . . . . . . . 21
151150adantl 468 . . . . . . . . . . . . . . . . . . . 20
152142, 151eqtrd 2487 . . . . . . . . . . . . . . . . . . 19
153138fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23
154153mpteq2dva 4492 . . . . . . . . . . . . . . . . . . . . . 22
155154fveq1d 5872 . . . . . . . . . . . . . . . . . . . . 21
156155adantr 467 . . . . . . . . . . . . . . . . . . . 20
157 eqidd 2454 . . . . . . . . . . . . . . . . . . . . . 22
158144fveq2d 5874 . . . . . . . . . . . . . . . . . . . . . . 23
159158adantl 468 . . . . . . . . . . . . . . . . . . . . . 22
160 fvex 5880 . . . . . . . . . . . . . . . . . . . . . . 23
161160a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
162157, 159, 147, 161fvmptd 5959 . . . . . . . . . . . . . . . . . . . . 21
163162adantl 468 . . . . . . . . . . . . . . . . . . . 20
164156, 163eqtrd 2487 . . . . . . . . . . . . . . . . . . 19
165152, 164oveq12d 6313 . . . . . . . . . . . . . . . . . 18
166165fveq2d 5874 . . . . . . . . . . . . . . . . 17
167166prodeq2dv 13989 . . . . . . . . . . . . . . . 16
168167cbvmptv 4498 . . . . . . . . . . . . . . 15
169168a1i 11 . . . . . . . . . . . . . 14
17081eqcomd 2459 . . . . . . . . . . . . . . . . 17
171170fveq2d 5874 . . . . . . . . . . . . . . . 16
172171prodeq2dv 13989 . . . . . . . . . . . . . . 15
173172mpteq2dva 4492 . . . . . . . . . . . . . 14
174169, 173eqtrd 2487 . . . . . . . . . . . . 13
175174fveq2d 5874 . . . . . . . . . . . 12 Σ^ Σ^
1761753ad2ant2 1031 . . . . . . . . . . 11 Σ^ Σ^ Σ^
17794adantll 721 . . . . . . . . . . . . . . . 16
178114adantll 721 . . . . . . . . . . . . . . . 16
179177, 178oveq12d 6313 . . . . . . . . . . . . . . 15
1809ad2antrr 733 . . . . . . . . . . . . . . . 16
181 ovnhoilem2.n . . . . . . . . . . . . . . . . 17
182181ad2antrr 733 . . . . . . . . . . . . . . . 16
18319adantlll 725 . . . . . . . . . . . . . . . . . 18
184183, 20syl 17 . . . . . . . . . . . . . . . . 17
185184, 22fmptd 6051 . . . . . . . . . . . . . . . 16
186183, 48syl 17 . . . . . . . . . . . . . . . . 17
187186, 50fmptd 6051 . . . . . . . . . . . . . . . 16
1888, 180, 182, 185, 187hoidmvn0val 38416 . . . . . . . . . . . . . . 15
189179, 188eqtrd 2487 . . . . . . . . . . . . . 14
190189mpteq2dva 4492 . . . . . . . . . . . . 13
191190fveq2d 5874 . . . . . . . . . . . 12 Σ^ Σ^
1921913adant3 1029 . . . . . . . . . . 11 Σ^ Σ^ Σ^
193 simp3 1011 . . . . . . . . . . 11 Σ^ Σ^
194176, 192, 1933eqtr4d 2497 . . . . . . . . . 10 Σ^ Σ^
1951943adant3l 1265 . . . . . . . . 9 Σ^ Σ^
196135, 195breqtrd 4430 . . . . . . . 8 Σ^
1971963exp 1208 . . . . . . 7 Σ^
198197adantr 467 . . . . . 6 Σ^
199198rexlimdv 2879 . . . . 5 Σ^
2007, 199mpd 15 . . . 4
201200ralrimiva 2804 . . 3
202 ssrab2 3516 . . . . . 6 Σ^
2031, 202eqsstri 3464 . . . . 5
204203a1i 11 . . . 4
205 icossxr 11726 . . . . 5
2068, 9, 11, 13hoidmvcl 38414 . . . . 5
207205, 206sseldi 3432 . . . 4
208 infxrgelb 11628 . . . 4 inf
209204, 207, 208syl2anc 667 . . 3 inf
210201, 209mpbird 236 . 2 inf
21166a1i 11 . . . . 5
212 nfv 1763 . . . . . 6
21311ffvelrnda 6027 . . . . . 6
21413ffvelrnda 6027 . . . . . . 7
215214rexrd 9695 . . . . . 6
216212, 213, 215hoissrrn2 38410 . . . . 5
217211, 216eqsstrd 3468 . . . 4
2189, 181, 217, 1ovnn0val 38383 . . 3 voln* inf
219218eqcomd 2459 . 2 inf voln*
220210, 219breqtrd 4430 1 voln*
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 986   wceq 1446   wcel 1889   wne 2624  wral 2739  wrex 2740  crab 2743  cvv 3047   wss 3406  c0 3733  cif 3883  ciun 4281   class class class wbr 4405   cmpt 4464   cxp 4835   ccom 4841  wf 5581  cfv 5585  (class class class)co 6295   cmpt2 6297  c1st 6796  c2nd 6797   cmap 7477  cixp 7527  cfn 7574  infcinf 7960  cr 9543  cc0 9544  c1 9545   cpnf 9677  cxr 9679   clt 9680   cle 9681  cn 10616  cico 11644  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