MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovoliunlem2 Structured version   Visualization version   GIF version

Theorem ovoliunlem2 25020
Description: Lemma for ovoliun 25022. (Contributed by Mario Carneiro, 12-Jun-2014.)
Hypotheses
Ref Expression
ovoliun.t 𝑇 = seq1( + , 𝐺)
ovoliun.g 𝐺 = (𝑛 ∈ β„• ↦ (vol*β€˜π΄))
ovoliun.a ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† ℝ)
ovoliun.v ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (vol*β€˜π΄) ∈ ℝ)
ovoliun.r (πœ‘ β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
ovoliun.b (πœ‘ β†’ 𝐡 ∈ ℝ+)
ovoliun.s 𝑆 = seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›)))
ovoliun.u π‘ˆ = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))
ovoliun.h 𝐻 = (π‘˜ ∈ β„• ↦ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))))
ovoliun.j (πœ‘ β†’ 𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•))
ovoliun.f (πœ‘ β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
ovoliun.x1 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
ovoliun.x2 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
Assertion
Ref Expression
ovoliunlem2 (πœ‘ β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
Distinct variable groups:   𝐴,π‘˜   π‘˜,𝑛,𝐡   π‘˜,𝐹,𝑛   π‘˜,𝐽,𝑛   𝑛,𝐻   πœ‘,π‘˜,𝑛   𝑆,π‘˜   π‘˜,𝐺   𝑇,π‘˜   𝑛,𝐺   𝑇,𝑛
Allowed substitution hints:   𝐴(𝑛)   𝑆(𝑛)   π‘ˆ(π‘˜,𝑛)   𝐻(π‘˜)

Proof of Theorem ovoliunlem2
Dummy variables 𝑗 π‘š π‘₯ 𝑧 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovoliun.a . . . . 5 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† ℝ)
21ralrimiva 3147 . . . 4 (πœ‘ β†’ βˆ€π‘› ∈ β„• 𝐴 βŠ† ℝ)
3 iunss 5049 . . . 4 (βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† ℝ ↔ βˆ€π‘› ∈ β„• 𝐴 βŠ† ℝ)
42, 3sylibr 233 . . 3 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† ℝ)
5 ovolcl 24995 . . 3 (βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† ℝ β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ∈ ℝ*)
64, 5syl 17 . 2 (πœ‘ β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ∈ ℝ*)
7 ovoliun.f . . . . . . . . . 10 (πœ‘ β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
87adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
9 ovoliun.j . . . . . . . . . . . 12 (πœ‘ β†’ 𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•))
10 f1of 6834 . . . . . . . . . . . 12 (𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•) β†’ 𝐽:β„•βŸΆ(β„• Γ— β„•))
119, 10syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐽:β„•βŸΆ(β„• Γ— β„•))
1211ffvelcdmda 7087 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) ∈ (β„• Γ— β„•))
13 xp1st 8007 . . . . . . . . . 10 ((π½β€˜π‘˜) ∈ (β„• Γ— β„•) β†’ (1st β€˜(π½β€˜π‘˜)) ∈ β„•)
1412, 13syl 17 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(π½β€˜π‘˜)) ∈ β„•)
158, 14ffvelcdmd 7088 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
16 elovolmlem 24991 . . . . . . . 8 ((πΉβ€˜(1st β€˜(π½β€˜π‘˜))) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
1715, 16sylib 217 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
18 xp2nd 8008 . . . . . . . 8 ((π½β€˜π‘˜) ∈ (β„• Γ— β„•) β†’ (2nd β€˜(π½β€˜π‘˜)) ∈ β„•)
1912, 18syl 17 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2nd β€˜(π½β€˜π‘˜)) ∈ β„•)
2017, 19ffvelcdmd 7088 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
21 ovoliun.h . . . . . 6 𝐻 = (π‘˜ ∈ β„• ↦ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))))
2220, 21fmptd 7114 . . . . 5 (πœ‘ β†’ 𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
23 eqid 2733 . . . . . 6 ((abs ∘ βˆ’ ) ∘ 𝐻) = ((abs ∘ βˆ’ ) ∘ 𝐻)
24 ovoliun.u . . . . . 6 π‘ˆ = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))
2523, 24ovolsf 24989 . . . . 5 (𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ π‘ˆ:β„•βŸΆ(0[,)+∞))
26 frn 6725 . . . . 5 (π‘ˆ:β„•βŸΆ(0[,)+∞) β†’ ran π‘ˆ βŠ† (0[,)+∞))
2722, 25, 263syl 18 . . . 4 (πœ‘ β†’ ran π‘ˆ βŠ† (0[,)+∞))
28 icossxr 13409 . . . 4 (0[,)+∞) βŠ† ℝ*
2927, 28sstrdi 3995 . . 3 (πœ‘ β†’ ran π‘ˆ βŠ† ℝ*)
30 supxrcl 13294 . . 3 (ran π‘ˆ βŠ† ℝ* β†’ sup(ran π‘ˆ, ℝ*, < ) ∈ ℝ*)
3129, 30syl 17 . 2 (πœ‘ β†’ sup(ran π‘ˆ, ℝ*, < ) ∈ ℝ*)
32 ovoliun.r . . . 4 (πœ‘ β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
33 ovoliun.b . . . . 5 (πœ‘ β†’ 𝐡 ∈ ℝ+)
3433rpred 13016 . . . 4 (πœ‘ β†’ 𝐡 ∈ ℝ)
3532, 34readdcld 11243 . . 3 (πœ‘ β†’ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ∈ ℝ)
3635rexrd 11264 . 2 (πœ‘ β†’ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ∈ ℝ*)
37 eliun 5002 . . . . . 6 (𝑧 ∈ βˆͺ 𝑛 ∈ β„• 𝐴 ↔ βˆƒπ‘› ∈ β„• 𝑧 ∈ 𝐴)
38 ovoliun.x1 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
39383adant3 1133 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
4013adant3 1133 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ 𝐴 βŠ† ℝ)
417ffvelcdmda 7087 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
42 elovolmlem 24991 . . . . . . . . . . . . 13 ((πΉβ€˜π‘›) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
4341, 42sylib 217 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
44433adant3 1133 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
45 ovolfioo 24984 . . . . . . . . . . 11 ((𝐴 βŠ† ℝ ∧ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ))) β†’ (𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)) ↔ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—)))))
4640, 44, 45syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ (𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)) ↔ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—)))))
4739, 46mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))))
48 simp3 1139 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ 𝑧 ∈ 𝐴)
49 rsp 3245 . . . . . . . . 9 (βˆ€π‘§ ∈ 𝐴 βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))) β†’ (𝑧 ∈ 𝐴 β†’ βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—)))))
5047, 48, 49sylc 65 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))))
51 simpl1 1192 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ πœ‘)
52 f1ocnv 6846 . . . . . . . . . . . 12 (𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•) β†’ ◑𝐽:(β„• Γ— β„•)–1-1-ontoβ†’β„•)
53 f1of 6834 . . . . . . . . . . . 12 (◑𝐽:(β„• Γ— β„•)–1-1-ontoβ†’β„• β†’ ◑𝐽:(β„• Γ— β„•)βŸΆβ„•)
5451, 9, 52, 534syl 19 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ ◑𝐽:(β„• Γ— β„•)βŸΆβ„•)
55 simpl2 1193 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ 𝑛 ∈ β„•)
56 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„•)
5754, 55, 56fovcdmd 7579 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (𝑛◑𝐽𝑗) ∈ β„•)
58 2fveq3 6897 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = (𝑛◑𝐽𝑗) β†’ (1st β€˜(π½β€˜π‘˜)) = (1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))
5958fveq2d 6896 . . . . . . . . . . . . . . . . . 18 (π‘˜ = (𝑛◑𝐽𝑗) β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))) = (πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗)))))
60 2fveq3 6897 . . . . . . . . . . . . . . . . . 18 (π‘˜ = (𝑛◑𝐽𝑗) β†’ (2nd β€˜(π½β€˜π‘˜)) = (2nd β€˜(π½β€˜(𝑛◑𝐽𝑗))))
6159, 60fveq12d 6899 . . . . . . . . . . . . . . . . 17 (π‘˜ = (𝑛◑𝐽𝑗) β†’ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))) = ((πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))β€˜(2nd β€˜(π½β€˜(𝑛◑𝐽𝑗)))))
62 fvex 6905 . . . . . . . . . . . . . . . . 17 ((πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))β€˜(2nd β€˜(π½β€˜(𝑛◑𝐽𝑗)))) ∈ V
6361, 21, 62fvmpt 6999 . . . . . . . . . . . . . . . 16 ((𝑛◑𝐽𝑗) ∈ β„• β†’ (π»β€˜(𝑛◑𝐽𝑗)) = ((πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))β€˜(2nd β€˜(π½β€˜(𝑛◑𝐽𝑗)))))
6457, 63syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (π»β€˜(𝑛◑𝐽𝑗)) = ((πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))β€˜(2nd β€˜(π½β€˜(𝑛◑𝐽𝑗)))))
65 df-ov 7412 . . . . . . . . . . . . . . . . . . . . 21 (𝑛◑𝐽𝑗) = (β—‘π½β€˜βŸ¨π‘›, π‘—βŸ©)
6665fveq2i 6895 . . . . . . . . . . . . . . . . . . . 20 (π½β€˜(𝑛◑𝐽𝑗)) = (π½β€˜(β—‘π½β€˜βŸ¨π‘›, π‘—βŸ©))
6751, 9syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ 𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•))
6855, 56opelxpd 5716 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ βŸ¨π‘›, π‘—βŸ© ∈ (β„• Γ— β„•))
69 f1ocnvfv2 7275 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•) ∧ βŸ¨π‘›, π‘—βŸ© ∈ (β„• Γ— β„•)) β†’ (π½β€˜(β—‘π½β€˜βŸ¨π‘›, π‘—βŸ©)) = βŸ¨π‘›, π‘—βŸ©)
7067, 68, 69syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (π½β€˜(β—‘π½β€˜βŸ¨π‘›, π‘—βŸ©)) = βŸ¨π‘›, π‘—βŸ©)
7166, 70eqtrid 2785 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (π½β€˜(𝑛◑𝐽𝑗)) = βŸ¨π‘›, π‘—βŸ©)
7271fveq2d 6896 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (1st β€˜(π½β€˜(𝑛◑𝐽𝑗))) = (1st β€˜βŸ¨π‘›, π‘—βŸ©))
73 vex 3479 . . . . . . . . . . . . . . . . . . 19 𝑛 ∈ V
74 vex 3479 . . . . . . . . . . . . . . . . . . 19 𝑗 ∈ V
7573, 74op1st 7983 . . . . . . . . . . . . . . . . . 18 (1st β€˜βŸ¨π‘›, π‘—βŸ©) = 𝑛
7672, 75eqtrdi 2789 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (1st β€˜(π½β€˜(𝑛◑𝐽𝑗))) = 𝑛)
7776fveq2d 6896 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗)))) = (πΉβ€˜π‘›))
7871fveq2d 6896 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (2nd β€˜(π½β€˜(𝑛◑𝐽𝑗))) = (2nd β€˜βŸ¨π‘›, π‘—βŸ©))
7973, 74op2nd 7984 . . . . . . . . . . . . . . . . 17 (2nd β€˜βŸ¨π‘›, π‘—βŸ©) = 𝑗
8078, 79eqtrdi 2789 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (2nd β€˜(π½β€˜(𝑛◑𝐽𝑗))) = 𝑗)
8177, 80fveq12d 6899 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ ((πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))β€˜(2nd β€˜(π½β€˜(𝑛◑𝐽𝑗)))) = ((πΉβ€˜π‘›)β€˜π‘—))
8264, 81eqtrd 2773 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (π»β€˜(𝑛◑𝐽𝑗)) = ((πΉβ€˜π‘›)β€˜π‘—))
8382fveq2d 6896 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) = (1st β€˜((πΉβ€˜π‘›)β€˜π‘—)))
8483breq1d 5159 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ ((1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧 ↔ (1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧))
8582fveq2d 6896 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))) = (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—)))
8685breq2d 5161 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))) ↔ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))))
8784, 86anbi12d 632 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (((1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗)))) ↔ ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—)))))
8887biimprd 247 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))) β†’ ((1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))))))
89 2fveq3 6897 . . . . . . . . . . . . 13 (π‘š = (𝑛◑𝐽𝑗) β†’ (1st β€˜(π»β€˜π‘š)) = (1st β€˜(π»β€˜(𝑛◑𝐽𝑗))))
9089breq1d 5159 . . . . . . . . . . . 12 (π‘š = (𝑛◑𝐽𝑗) β†’ ((1st β€˜(π»β€˜π‘š)) < 𝑧 ↔ (1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧))
91 2fveq3 6897 . . . . . . . . . . . . 13 (π‘š = (𝑛◑𝐽𝑗) β†’ (2nd β€˜(π»β€˜π‘š)) = (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))))
9291breq2d 5161 . . . . . . . . . . . 12 (π‘š = (𝑛◑𝐽𝑗) β†’ (𝑧 < (2nd β€˜(π»β€˜π‘š)) ↔ 𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗)))))
9390, 92anbi12d 632 . . . . . . . . . . 11 (π‘š = (𝑛◑𝐽𝑗) β†’ (((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š))) ↔ ((1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))))))
9493rspcev 3613 . . . . . . . . . 10 (((𝑛◑𝐽𝑗) ∈ β„• ∧ ((1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))))) β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š))))
9557, 88, 94syl6an 683 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))) β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
9695rexlimdva 3156 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ (βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))) β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
9750, 96mpd 15 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š))))
9897rexlimdv3a 3160 . . . . . 6 (πœ‘ β†’ (βˆƒπ‘› ∈ β„• 𝑧 ∈ 𝐴 β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
9937, 98biimtrid 241 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝑛 ∈ β„• 𝐴 β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
10099ralrimiv 3146 . . . 4 (πœ‘ β†’ βˆ€π‘§ ∈ βˆͺ 𝑛 ∈ β„• π΄βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š))))
101 ovolfioo 24984 . . . . 5 ((βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† ℝ ∧ 𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ))) β†’ (βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† βˆͺ ran ((,) ∘ 𝐻) ↔ βˆ€π‘§ ∈ βˆͺ 𝑛 ∈ β„• π΄βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
1024, 22, 101syl2anc 585 . . . 4 (πœ‘ β†’ (βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† βˆͺ ran ((,) ∘ 𝐻) ↔ βˆ€π‘§ ∈ βˆͺ 𝑛 ∈ β„• π΄βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
103100, 102mpbird 257 . . 3 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† βˆͺ ran ((,) ∘ 𝐻))
10424ovollb 24996 . . 3 ((𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† βˆͺ ran ((,) ∘ 𝐻)) β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ≀ sup(ran π‘ˆ, ℝ*, < ))
10522, 103, 104syl2anc 585 . 2 (πœ‘ β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ≀ sup(ran π‘ˆ, ℝ*, < ))
106 fzfi 13937 . . . . . . 7 (1...𝑗) ∈ Fin
107 elfznn 13530 . . . . . . . . . 10 (𝑀 ∈ (1...𝑗) β†’ 𝑀 ∈ β„•)
108 ffvelcdm 7084 . . . . . . . . . . 11 ((𝐽:β„•βŸΆ(β„• Γ— β„•) ∧ 𝑀 ∈ β„•) β†’ (π½β€˜π‘€) ∈ (β„• Γ— β„•))
109 xp1st 8007 . . . . . . . . . . 11 ((π½β€˜π‘€) ∈ (β„• Γ— β„•) β†’ (1st β€˜(π½β€˜π‘€)) ∈ β„•)
110 nnre 12219 . . . . . . . . . . 11 ((1st β€˜(π½β€˜π‘€)) ∈ β„• β†’ (1st β€˜(π½β€˜π‘€)) ∈ ℝ)
111108, 109, 1103syl 18 . . . . . . . . . 10 ((𝐽:β„•βŸΆ(β„• Γ— β„•) ∧ 𝑀 ∈ β„•) β†’ (1st β€˜(π½β€˜π‘€)) ∈ ℝ)
11211, 107, 111syl2an 597 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ (1...𝑗)) β†’ (1st β€˜(π½β€˜π‘€)) ∈ ℝ)
113112ralrimiva 3147 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ∈ ℝ)
114113adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ∈ ℝ)
115 fimaxre3 12160 . . . . . . 7 (((1...𝑗) ∈ Fin ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ∈ ℝ) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯)
116106, 114, 115sylancr 588 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯)
117 fllep1 13766 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ π‘₯ ≀ ((βŒŠβ€˜π‘₯) + 1))
118117ad2antlr 726 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ π‘₯ ≀ ((βŒŠβ€˜π‘₯) + 1))
119112adantlr 714 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ (1st β€˜(π½β€˜π‘€)) ∈ ℝ)
120 simplr 768 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ π‘₯ ∈ ℝ)
121 flcl 13760 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜π‘₯) ∈ β„€)
122121peano2zd 12669 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ β„€)
123122zred 12666 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ ℝ)
124123ad2antlr 726 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ ℝ)
125 letr 11308 . . . . . . . . . . . 12 (((1st β€˜(π½β€˜π‘€)) ∈ ℝ ∧ π‘₯ ∈ ℝ ∧ ((βŒŠβ€˜π‘₯) + 1) ∈ ℝ) β†’ (((1st β€˜(π½β€˜π‘€)) ≀ π‘₯ ∧ π‘₯ ≀ ((βŒŠβ€˜π‘₯) + 1)) β†’ (1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1)))
126119, 120, 124, 125syl3anc 1372 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ (((1st β€˜(π½β€˜π‘€)) ≀ π‘₯ ∧ π‘₯ ≀ ((βŒŠβ€˜π‘₯) + 1)) β†’ (1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1)))
127118, 126mpan2d 693 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ ((1st β€˜(π½β€˜π‘€)) ≀ π‘₯ β†’ (1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1)))
128127ralimdva 3168 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯ β†’ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1)))
129128adantlr 714 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯ β†’ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1)))
130 ovoliun.t . . . . . . . . . 10 𝑇 = seq1( + , 𝐺)
131 ovoliun.g . . . . . . . . . 10 𝐺 = (𝑛 ∈ β„• ↦ (vol*β€˜π΄))
132 simpll 766 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ πœ‘)
133132, 1sylan 581 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† ℝ)
134 ovoliun.v . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (vol*β€˜π΄) ∈ ℝ)
135132, 134sylan 581 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) ∧ 𝑛 ∈ β„•) β†’ (vol*β€˜π΄) ∈ ℝ)
136132, 32syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
137132, 33syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ 𝐡 ∈ ℝ+)
138 ovoliun.s . . . . . . . . . 10 𝑆 = seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›)))
139132, 9syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ 𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•))
140132, 7syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
141132, 38sylan 581 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
142 ovoliun.x2 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
143132, 142sylan 581 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) ∧ 𝑛 ∈ β„•) β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
144 simplr 768 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ 𝑗 ∈ β„•)
145122ad2antrl 727 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ β„€)
146 simprr 772 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))
147130, 131, 133, 135, 136, 137, 138, 24, 21, 139, 140, 141, 143, 144, 145, 146ovoliunlem1 25019 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
148147expr 458 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1) β†’ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
149129, 148syld 47 . . . . . . 7 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯ β†’ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
150149rexlimdva 3156 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯ β†’ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
151116, 150mpd 15 . . . . 5 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
152151ralrimiva 3147 . . . 4 (πœ‘ β†’ βˆ€π‘— ∈ β„• (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
153 ffn 6718 . . . . 5 (π‘ˆ:β„•βŸΆ(0[,)+∞) β†’ π‘ˆ Fn β„•)
154 breq1 5152 . . . . . 6 (𝑧 = (π‘ˆβ€˜π‘—) β†’ (𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ↔ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
155154ralrn 7090 . . . . 5 (π‘ˆ Fn β„• β†’ (βˆ€π‘§ ∈ ran π‘ˆ 𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ↔ βˆ€π‘— ∈ β„• (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
15622, 25, 153, 1554syl 19 . . . 4 (πœ‘ β†’ (βˆ€π‘§ ∈ ran π‘ˆ 𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ↔ βˆ€π‘— ∈ β„• (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
157152, 156mpbird 257 . . 3 (πœ‘ β†’ βˆ€π‘§ ∈ ran π‘ˆ 𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
158 supxrleub 13305 . . . 4 ((ran π‘ˆ βŠ† ℝ* ∧ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ∈ ℝ*) β†’ (sup(ran π‘ˆ, ℝ*, < ) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ↔ βˆ€π‘§ ∈ ran π‘ˆ 𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
15929, 36, 158syl2anc 585 . . 3 (πœ‘ β†’ (sup(ran π‘ˆ, ℝ*, < ) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ↔ βˆ€π‘§ ∈ ran π‘ˆ 𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
160157, 159mpbird 257 . 2 (πœ‘ β†’ sup(ran π‘ˆ, ℝ*, < ) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
1616, 31, 36, 105, 160xrletrd 13141 1 (πœ‘ β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071   ∩ cin 3948   βŠ† wss 3949  βŸ¨cop 4635  βˆͺ cuni 4909  βˆͺ ciun 4998   class class class wbr 5149   ↦ cmpt 5232   Γ— cxp 5675  β—‘ccnv 5676  ran crn 5678   ∘ ccom 5681   Fn wfn 6539  βŸΆwf 6540  β€“1-1-ontoβ†’wf1o 6543  β€˜cfv 6544  (class class class)co 7409  1st c1st 7973  2nd c2nd 7974   ↑m cmap 8820  Fincfn 8939  supcsup 9435  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113  +∞cpnf 11245  β„*cxr 11247   < clt 11248   ≀ cle 11249   βˆ’ cmin 11444   / cdiv 11871  β„•cn 12212  2c2 12267  β„€cz 12558  β„+crp 12974  (,)cioo 13324  [,)cico 13326  ...cfz 13484  βŒŠcfl 13755  seqcseq 13966  β†‘cexp 14027  abscabs 15181  vol*covol 24979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-inf 9438  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-rp 12975  df-ioo 13328  df-ico 13330  df-fz 13485  df-fzo 13628  df-fl 13757  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-rlim 15433  df-sum 15633  df-ovol 24981
This theorem is referenced by:  ovoliunlem3  25021
  Copyright terms: Public domain W3C validator