Theorem ovollb2 24092

Description: It is often more convenient to do calculations with *closed* coverings rather than open ones; here we show that it makes no difference (compare ovollb 24082). (Contributed by Mario Carneiro, 24-Mar-2015.)

Hypothesis

Ref	Expression
ovollb2.1	⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))

Assertion

Ref	Expression
ovollb2	⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))

Proof of Theorem ovollb2

Dummy variables 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 487	. . . . . . 7 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹))
2		ovolficcss 24072	. . . . . . . 8 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
3	2	adantr 483	. . . . . . 7 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → ∪ ran ([,] ∘ 𝐹) ⊆ ℝ)
4	1, 3	sstrd 3979	. . . . . 6 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → 𝐴 ⊆ ℝ)
5		ovolcl 24081	. . . . . 6 ⊢ (𝐴 ⊆ ℝ → (vol*‘𝐴) ∈ ℝ*)
6	4, 5	syl 17	. . . . 5 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘𝐴) ∈ ℝ*)
7	6	adantr 483	. . . 4 ⊢ (((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) = +∞) → (vol*‘𝐴) ∈ ℝ*)
8		pnfge 12528	. . . 4 ⊢ ((vol*‘𝐴) ∈ ℝ* → (vol*‘𝐴) ≤ +∞)
9	7, 8	syl 17	. . 3 ⊢ (((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) = +∞) → (vol*‘𝐴) ≤ +∞)
10		simpr 487	. . 3 ⊢ (((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) = +∞) → sup(ran 𝑆, ℝ*, < ) = +∞)
11	9, 10	breqtrrd 5096	. 2 ⊢ (((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) = +∞) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
12		eqid 2823	. . . . . . . . 9 ⊢ ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
13		ovollb2.1	. . . . . . . . 9 ⊢ 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
14	12, 13	ovolsf 24075	. . . . . . . 8 ⊢ (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
15	14	adantr 483	. . . . . . 7 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → 𝑆:ℕ⟶(0[,)+∞))
16	15	frnd 6523	. . . . . 6 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → ran 𝑆 ⊆ (0[,)+∞))
17		rge0ssre 12847	. . . . . 6 ⊢ (0[,)+∞) ⊆ ℝ
18	16, 17	sstrdi 3981	. . . . 5 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → ran 𝑆 ⊆ ℝ)
19		1nn 11651	. . . . . . . 8 ⊢ 1 ∈ ℕ
20	15	fdmd 6525	. . . . . . . 8 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → dom 𝑆 = ℕ)
21	19, 20	eleqtrrid 2922	. . . . . . 7 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → 1 ∈ dom 𝑆)
22	21	ne0d 4303	. . . . . 6 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → dom 𝑆 ≠ ∅)
23		dm0rn0 5797	. . . . . . 7 ⊢ (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
24	23	necon3bii 3070	. . . . . 6 ⊢ (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
25	22, 24	sylib 220	. . . . 5 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → ran 𝑆 ≠ ∅)
26		supxrre2 12727	. . . . 5 ⊢ ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅) → (sup(ran 𝑆, ℝ*, < ) ∈ ℝ ↔ sup(ran 𝑆, ℝ*, < ) ≠ +∞))
27	18, 25, 26	syl2anc 586	. . . 4 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (sup(ran 𝑆, ℝ*, < ) ∈ ℝ ↔ sup(ran 𝑆, ℝ*, < ) ≠ +∞))
28	27	biimpar 480	. . 3 ⊢ (((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) ≠ +∞) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
29		2fveq3 6677	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (1st ‘(𝐹‘𝑚)) = (1st ‘(𝐹‘𝑛)))
30		oveq2 7166	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (2↑𝑚) = (2↑𝑛))
31	30	oveq2d 7174	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → ((𝑥 / 2) / (2↑𝑚)) = ((𝑥 / 2) / (2↑𝑛)))
32	29, 31	oveq12d 7176	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((1st ‘(𝐹‘𝑚)) − ((𝑥 / 2) / (2↑𝑚))) = ((1st ‘(𝐹‘𝑛)) − ((𝑥 / 2) / (2↑𝑛))))
33		2fveq3 6677	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (2nd ‘(𝐹‘𝑚)) = (2nd ‘(𝐹‘𝑛)))
34	33, 31	oveq12d 7176	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((2nd ‘(𝐹‘𝑚)) + ((𝑥 / 2) / (2↑𝑚))) = ((2nd ‘(𝐹‘𝑛)) + ((𝑥 / 2) / (2↑𝑛))))
35	32, 34	opeq12d 4813	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ⟨((1st ‘(𝐹‘𝑚)) − ((𝑥 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝑥 / 2) / (2↑𝑚)))⟩ = ⟨((1st ‘(𝐹‘𝑛)) − ((𝑥 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝑥 / 2) / (2↑𝑛)))⟩)
36	35	cbvmptv 5171	. . . . . 6 ⊢ (𝑚 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑚)) − ((𝑥 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝑥 / 2) / (2↑𝑚)))⟩) = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑛)) − ((𝑥 / 2) / (2↑𝑛))), ((2nd ‘(𝐹‘𝑛)) + ((𝑥 / 2) / (2↑𝑛)))⟩)
37		eqid 2823	. . . . . 6 ⊢ seq1( + , ((abs ∘ − ) ∘ (𝑚 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑚)) − ((𝑥 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝑥 / 2) / (2↑𝑚)))⟩))) = seq1( + , ((abs ∘ − ) ∘ (𝑚 ∈ ℕ ↦ ⟨((1st ‘(𝐹‘𝑚)) − ((𝑥 / 2) / (2↑𝑚))), ((2nd ‘(𝐹‘𝑚)) + ((𝑥 / 2) / (2↑𝑚)))⟩)))
38		simplll 773	. . . . . 6 ⊢ ((((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
39		simpllr 774	. . . . . 6 ⊢ ((((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹))
40		simpr 487	. . . . . 6 ⊢ ((((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
41		simplr 767	. . . . . 6 ⊢ ((((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
42	13, 36, 37, 38, 39, 40, 41	ovollb2lem 24091	. . . . 5 ⊢ ((((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ) ∧ 𝑥 ∈ ℝ+) → (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝑥))
43	42	ralrimiva 3184	. . . 4 ⊢ (((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ) → ∀𝑥 ∈ ℝ+ (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝑥))
44		xralrple 12601	. . . . 5 ⊢ (((vol*‘𝐴) ∈ ℝ* ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ) → ((vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ) ↔ ∀𝑥 ∈ ℝ+ (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝑥)))
45	6, 44	sylan 582	. . . 4 ⊢ (((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ) → ((vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ) ↔ ∀𝑥 ∈ ℝ+ (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝑥)))
46	43, 45	mpbird 259	. . 3 ⊢ (((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) ∈ ℝ) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
47	28, 46	syldan 593	. 2 ⊢ (((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) ∧ sup(ran 𝑆, ℝ*, < ) ≠ +∞) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
48	11, 47	pm2.61dane 3106	1 ⊢ ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ⊆ ∪ ran ([,] ∘ 𝐹)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  ∀wral 3140   ∩ cin 3937   ⊆ wss 3938  ∅c0 4293  ⟨cop 4575  ∪ cuni 4840   class class class wbr 5068   ↦ cmpt 5148   × cxp 5555  dom cdm 5557  ran crn 5558   ∘ ccom 5561  ⟶wf 6353  ‘cfv 6357  (class class class)co 7158  1^st c1st 7689  2^nd c2nd 7690  supcsup 8906  ℝcr 10538  0cc0 10539  1c1 10540   + caddc 10542  +∞cpnf 10674  ℝ^*cxr 10676   < clt 10677   ≤ cle 10678   − cmin 10872   / cdiv 11299  ℕcn 11640  2c2 11695  ℝ⁺crp 12392  [,)cico 12743  [,]cicc 12744  seqcseq 13372  ↑cexp 13432  abscabs 14595  vol*covol 24065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-inf2 9106  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616  ax-pre-sup 10617

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-se 5517  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-isom 6366  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-oadd 8108  df-er 8291  df-map 8410  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-sup 8908  df-inf 8909  df-oi 8976  df-card 9370  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-div 11300  df-nn 11641  df-2 11703  df-3 11704  df-n0 11901  df-z 11985  df-uz 12247  df-q 12352  df-rp 12393  df-ioo 12745  df-ico 12747  df-icc 12748  df-fz 12896  df-fzo 13037  df-seq 13373  df-exp 13433  df-hash 13694  df-cj 14460  df-re 14461  df-im 14462  df-sqrt 14596  df-abs 14597  df-clim 14847  df-sum 15045  df-ovol 24067

This theorem is referenced by:  ovolctb  24093  ovolicc1  24119  ioombl1lem4  24164  uniiccvol  24183