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

Theorem ovoliunlem2 25027
Description: Lemma for ovoliun 25029. (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 3146 . . . 4 (πœ‘ β†’ βˆ€π‘› ∈ β„• 𝐴 βŠ† ℝ)
3 iunss 5048 . . . 4 (βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† ℝ ↔ βˆ€π‘› ∈ β„• 𝐴 βŠ† ℝ)
42, 3sylibr 233 . . 3 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† ℝ)
5 ovolcl 25002 . . 3 (βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† ℝ β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ∈ ℝ*)
64, 5syl 17 . 2 (πœ‘ β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ∈ ℝ*)
7 ovoliun.f . . . . . . . . . 10 (πœ‘ β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
87adantr 481 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
9 ovoliun.j . . . . . . . . . . . 12 (πœ‘ β†’ 𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•))
10 f1of 6833 . . . . . . . . . . . 12 (𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•) β†’ 𝐽:β„•βŸΆ(β„• Γ— β„•))
119, 10syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 𝐽:β„•βŸΆ(β„• Γ— β„•))
1211ffvelcdmda 7086 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) ∈ (β„• Γ— β„•))
13 xp1st 8009 . . . . . . . . . 10 ((π½β€˜π‘˜) ∈ (β„• Γ— β„•) β†’ (1st β€˜(π½β€˜π‘˜)) ∈ β„•)
1412, 13syl 17 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(π½β€˜π‘˜)) ∈ β„•)
158, 14ffvelcdmd 7087 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
16 elovolmlem 24998 . . . . . . . 8 ((πΉβ€˜(1st β€˜(π½β€˜π‘˜))) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
1715, 16sylib 217 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
18 xp2nd 8010 . . . . . . . 8 ((π½β€˜π‘˜) ∈ (β„• Γ— β„•) β†’ (2nd β€˜(π½β€˜π‘˜)) ∈ β„•)
1912, 18syl 17 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2nd β€˜(π½β€˜π‘˜)) ∈ β„•)
2017, 19ffvelcdmd 7087 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
21 ovoliun.h . . . . . 6 𝐻 = (π‘˜ ∈ β„• ↦ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))))
2220, 21fmptd 7115 . . . . 5 (πœ‘ β†’ 𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
23 eqid 2732 . . . . . 6 ((abs ∘ βˆ’ ) ∘ 𝐻) = ((abs ∘ βˆ’ ) ∘ 𝐻)
24 ovoliun.u . . . . . 6 π‘ˆ = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))
2523, 24ovolsf 24996 . . . . 5 (𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ π‘ˆ:β„•βŸΆ(0[,)+∞))
26 frn 6724 . . . . 5 (π‘ˆ:β„•βŸΆ(0[,)+∞) β†’ ran π‘ˆ βŠ† (0[,)+∞))
2722, 25, 263syl 18 . . . 4 (πœ‘ β†’ ran π‘ˆ βŠ† (0[,)+∞))
28 icossxr 13411 . . . 4 (0[,)+∞) βŠ† ℝ*
2927, 28sstrdi 3994 . . 3 (πœ‘ β†’ ran π‘ˆ βŠ† ℝ*)
30 supxrcl 13296 . . 3 (ran π‘ˆ βŠ† ℝ* β†’ sup(ran π‘ˆ, ℝ*, < ) ∈ ℝ*)
3129, 30syl 17 . 2 (πœ‘ β†’ sup(ran π‘ˆ, ℝ*, < ) ∈ ℝ*)
32 ovoliun.r . . . 4 (πœ‘ β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
33 ovoliun.b . . . . 5 (πœ‘ β†’ 𝐡 ∈ ℝ+)
3433rpred 13018 . . . 4 (πœ‘ β†’ 𝐡 ∈ ℝ)
3532, 34readdcld 11245 . . 3 (πœ‘ β†’ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ∈ ℝ)
3635rexrd 11266 . 2 (πœ‘ β†’ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ∈ ℝ*)
37 eliun 5001 . . . . . 6 (𝑧 ∈ βˆͺ 𝑛 ∈ β„• 𝐴 ↔ βˆƒπ‘› ∈ β„• 𝑧 ∈ 𝐴)
38 ovoliun.x1 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
39383adant3 1132 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
4013adant3 1132 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ 𝐴 βŠ† ℝ)
417ffvelcdmda 7086 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
42 elovolmlem 24998 . . . . . . . . . . . . 13 ((πΉβ€˜π‘›) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
4341, 42sylib 217 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
44433adant3 1132 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
45 ovolfioo 24991 . . . . . . . . . . 11 ((𝐴 βŠ† ℝ ∧ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ))) β†’ (𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)) ↔ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—)))))
4640, 44, 45syl2anc 584 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ (𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)) ↔ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—)))))
4739, 46mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ βˆ€π‘§ ∈ 𝐴 βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))))
48 simp3 1138 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ 𝑧 ∈ 𝐴)
49 rsp 3244 . . . . . . . . 9 (βˆ€π‘§ ∈ 𝐴 βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))) β†’ (𝑧 ∈ 𝐴 β†’ βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—)))))
5047, 48, 49sylc 65 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))))
51 simpl1 1191 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ πœ‘)
52 f1ocnv 6845 . . . . . . . . . . . 12 (𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•) β†’ ◑𝐽:(β„• Γ— β„•)–1-1-ontoβ†’β„•)
53 f1of 6833 . . . . . . . . . . . 12 (◑𝐽:(β„• Γ— β„•)–1-1-ontoβ†’β„• β†’ ◑𝐽:(β„• Γ— β„•)βŸΆβ„•)
5451, 9, 52, 534syl 19 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ ◑𝐽:(β„• Γ— β„•)βŸΆβ„•)
55 simpl2 1192 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ 𝑛 ∈ β„•)
56 simpr 485 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ β„•)
5754, 55, 56fovcdmd 7581 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (𝑛◑𝐽𝑗) ∈ β„•)
58 2fveq3 6896 . . . . . . . . . . . . . . . . . . 19 (π‘˜ = (𝑛◑𝐽𝑗) β†’ (1st β€˜(π½β€˜π‘˜)) = (1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))
5958fveq2d 6895 . . . . . . . . . . . . . . . . . 18 (π‘˜ = (𝑛◑𝐽𝑗) β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))) = (πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗)))))
60 2fveq3 6896 . . . . . . . . . . . . . . . . . 18 (π‘˜ = (𝑛◑𝐽𝑗) β†’ (2nd β€˜(π½β€˜π‘˜)) = (2nd β€˜(π½β€˜(𝑛◑𝐽𝑗))))
6159, 60fveq12d 6898 . . . . . . . . . . . . . . . . 17 (π‘˜ = (𝑛◑𝐽𝑗) β†’ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))) = ((πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))β€˜(2nd β€˜(π½β€˜(𝑛◑𝐽𝑗)))))
62 fvex 6904 . . . . . . . . . . . . . . . . 17 ((πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))β€˜(2nd β€˜(π½β€˜(𝑛◑𝐽𝑗)))) ∈ V
6361, 21, 62fvmpt 6998 . . . . . . . . . . . . . . . 16 ((𝑛◑𝐽𝑗) ∈ β„• β†’ (π»β€˜(𝑛◑𝐽𝑗)) = ((πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))β€˜(2nd β€˜(π½β€˜(𝑛◑𝐽𝑗)))))
6457, 63syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (π»β€˜(𝑛◑𝐽𝑗)) = ((πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))β€˜(2nd β€˜(π½β€˜(𝑛◑𝐽𝑗)))))
65 df-ov 7414 . . . . . . . . . . . . . . . . . . . . 21 (𝑛◑𝐽𝑗) = (β—‘π½β€˜βŸ¨π‘›, π‘—βŸ©)
6665fveq2i 6894 . . . . . . . . . . . . . . . . . . . 20 (π½β€˜(𝑛◑𝐽𝑗)) = (π½β€˜(β—‘π½β€˜βŸ¨π‘›, π‘—βŸ©))
6751, 9syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ 𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•))
6855, 56opelxpd 5715 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ βŸ¨π‘›, π‘—βŸ© ∈ (β„• Γ— β„•))
69 f1ocnvfv2 7277 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•) ∧ βŸ¨π‘›, π‘—βŸ© ∈ (β„• Γ— β„•)) β†’ (π½β€˜(β—‘π½β€˜βŸ¨π‘›, π‘—βŸ©)) = βŸ¨π‘›, π‘—βŸ©)
7067, 68, 69syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (π½β€˜(β—‘π½β€˜βŸ¨π‘›, π‘—βŸ©)) = βŸ¨π‘›, π‘—βŸ©)
7166, 70eqtrid 2784 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (π½β€˜(𝑛◑𝐽𝑗)) = βŸ¨π‘›, π‘—βŸ©)
7271fveq2d 6895 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (1st β€˜(π½β€˜(𝑛◑𝐽𝑗))) = (1st β€˜βŸ¨π‘›, π‘—βŸ©))
73 vex 3478 . . . . . . . . . . . . . . . . . . 19 𝑛 ∈ V
74 vex 3478 . . . . . . . . . . . . . . . . . . 19 𝑗 ∈ V
7573, 74op1st 7985 . . . . . . . . . . . . . . . . . 18 (1st β€˜βŸ¨π‘›, π‘—βŸ©) = 𝑛
7672, 75eqtrdi 2788 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (1st β€˜(π½β€˜(𝑛◑𝐽𝑗))) = 𝑛)
7776fveq2d 6895 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗)))) = (πΉβ€˜π‘›))
7871fveq2d 6895 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (2nd β€˜(π½β€˜(𝑛◑𝐽𝑗))) = (2nd β€˜βŸ¨π‘›, π‘—βŸ©))
7973, 74op2nd 7986 . . . . . . . . . . . . . . . . 17 (2nd β€˜βŸ¨π‘›, π‘—βŸ©) = 𝑗
8078, 79eqtrdi 2788 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (2nd β€˜(π½β€˜(𝑛◑𝐽𝑗))) = 𝑗)
8177, 80fveq12d 6898 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ ((πΉβ€˜(1st β€˜(π½β€˜(𝑛◑𝐽𝑗))))β€˜(2nd β€˜(π½β€˜(𝑛◑𝐽𝑗)))) = ((πΉβ€˜π‘›)β€˜π‘—))
8264, 81eqtrd 2772 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (π»β€˜(𝑛◑𝐽𝑗)) = ((πΉβ€˜π‘›)β€˜π‘—))
8382fveq2d 6895 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) = (1st β€˜((πΉβ€˜π‘›)β€˜π‘—)))
8483breq1d 5158 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ ((1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧 ↔ (1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧))
8582fveq2d 6895 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))) = (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—)))
8685breq2d 5160 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))) ↔ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))))
8784, 86anbi12d 631 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (((1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗)))) ↔ ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—)))))
8887biimprd 247 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))) β†’ ((1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))))))
89 2fveq3 6896 . . . . . . . . . . . . 13 (π‘š = (𝑛◑𝐽𝑗) β†’ (1st β€˜(π»β€˜π‘š)) = (1st β€˜(π»β€˜(𝑛◑𝐽𝑗))))
9089breq1d 5158 . . . . . . . . . . . 12 (π‘š = (𝑛◑𝐽𝑗) β†’ ((1st β€˜(π»β€˜π‘š)) < 𝑧 ↔ (1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧))
91 2fveq3 6896 . . . . . . . . . . . . 13 (π‘š = (𝑛◑𝐽𝑗) β†’ (2nd β€˜(π»β€˜π‘š)) = (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))))
9291breq2d 5160 . . . . . . . . . . . 12 (π‘š = (𝑛◑𝐽𝑗) β†’ (𝑧 < (2nd β€˜(π»β€˜π‘š)) ↔ 𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗)))))
9390, 92anbi12d 631 . . . . . . . . . . 11 (π‘š = (𝑛◑𝐽𝑗) β†’ (((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š))) ↔ ((1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))))))
9493rspcev 3612 . . . . . . . . . 10 (((𝑛◑𝐽𝑗) ∈ β„• ∧ ((1st β€˜(π»β€˜(𝑛◑𝐽𝑗))) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜(𝑛◑𝐽𝑗))))) β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š))))
9557, 88, 94syl6an 682 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) ∧ 𝑗 ∈ β„•) β†’ (((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))) β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
9695rexlimdva 3155 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ (βˆƒπ‘— ∈ β„• ((1st β€˜((πΉβ€˜π‘›)β€˜π‘—)) < 𝑧 ∧ 𝑧 < (2nd β€˜((πΉβ€˜π‘›)β€˜π‘—))) β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
9750, 96mpd 15 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ 𝑧 ∈ 𝐴) β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š))))
9897rexlimdv3a 3159 . . . . . 6 (πœ‘ β†’ (βˆƒπ‘› ∈ β„• 𝑧 ∈ 𝐴 β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
9937, 98biimtrid 241 . . . . 5 (πœ‘ β†’ (𝑧 ∈ βˆͺ 𝑛 ∈ β„• 𝐴 β†’ βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
10099ralrimiv 3145 . . . 4 (πœ‘ β†’ βˆ€π‘§ ∈ βˆͺ 𝑛 ∈ β„• π΄βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š))))
101 ovolfioo 24991 . . . . 5 ((βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† ℝ ∧ 𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ))) β†’ (βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† βˆͺ ran ((,) ∘ 𝐻) ↔ βˆ€π‘§ ∈ βˆͺ 𝑛 ∈ β„• π΄βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
1024, 22, 101syl2anc 584 . . . 4 (πœ‘ β†’ (βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† βˆͺ ran ((,) ∘ 𝐻) ↔ βˆ€π‘§ ∈ βˆͺ 𝑛 ∈ β„• π΄βˆƒπ‘š ∈ β„• ((1st β€˜(π»β€˜π‘š)) < 𝑧 ∧ 𝑧 < (2nd β€˜(π»β€˜π‘š)))))
103100, 102mpbird 256 . . 3 (πœ‘ β†’ βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† βˆͺ ran ((,) ∘ 𝐻))
10424ovollb 25003 . . 3 ((𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ βˆͺ 𝑛 ∈ β„• 𝐴 βŠ† βˆͺ ran ((,) ∘ 𝐻)) β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ≀ sup(ran π‘ˆ, ℝ*, < ))
10522, 103, 104syl2anc 584 . 2 (πœ‘ β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ≀ sup(ran π‘ˆ, ℝ*, < ))
106 fzfi 13939 . . . . . . 7 (1...𝑗) ∈ Fin
107 elfznn 13532 . . . . . . . . . 10 (𝑀 ∈ (1...𝑗) β†’ 𝑀 ∈ β„•)
108 ffvelcdm 7083 . . . . . . . . . . 11 ((𝐽:β„•βŸΆ(β„• Γ— β„•) ∧ 𝑀 ∈ β„•) β†’ (π½β€˜π‘€) ∈ (β„• Γ— β„•))
109 xp1st 8009 . . . . . . . . . . 11 ((π½β€˜π‘€) ∈ (β„• Γ— β„•) β†’ (1st β€˜(π½β€˜π‘€)) ∈ β„•)
110 nnre 12221 . . . . . . . . . . 11 ((1st β€˜(π½β€˜π‘€)) ∈ β„• β†’ (1st β€˜(π½β€˜π‘€)) ∈ ℝ)
111108, 109, 1103syl 18 . . . . . . . . . 10 ((𝐽:β„•βŸΆ(β„• Γ— β„•) ∧ 𝑀 ∈ β„•) β†’ (1st β€˜(π½β€˜π‘€)) ∈ ℝ)
11211, 107, 111syl2an 596 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 ∈ (1...𝑗)) β†’ (1st β€˜(π½β€˜π‘€)) ∈ ℝ)
113112ralrimiva 3146 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ∈ ℝ)
114113adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ∈ ℝ)
115 fimaxre3 12162 . . . . . . 7 (((1...𝑗) ∈ Fin ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ∈ ℝ) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯)
116106, 114, 115sylancr 587 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯)
117 fllep1 13768 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ π‘₯ ≀ ((βŒŠβ€˜π‘₯) + 1))
118117ad2antlr 725 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ π‘₯ ≀ ((βŒŠβ€˜π‘₯) + 1))
119112adantlr 713 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ (1st β€˜(π½β€˜π‘€)) ∈ ℝ)
120 simplr 767 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ π‘₯ ∈ ℝ)
121 flcl 13762 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜π‘₯) ∈ β„€)
122121peano2zd 12671 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ β„€)
123122zred 12668 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ ℝ)
124123ad2antlr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ ℝ)
125 letr 11310 . . . . . . . . . . . 12 (((1st β€˜(π½β€˜π‘€)) ∈ ℝ ∧ π‘₯ ∈ ℝ ∧ ((βŒŠβ€˜π‘₯) + 1) ∈ ℝ) β†’ (((1st β€˜(π½β€˜π‘€)) ≀ π‘₯ ∧ π‘₯ ≀ ((βŒŠβ€˜π‘₯) + 1)) β†’ (1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1)))
126119, 120, 124, 125syl3anc 1371 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ (((1st β€˜(π½β€˜π‘€)) ≀ π‘₯ ∧ π‘₯ ≀ ((βŒŠβ€˜π‘₯) + 1)) β†’ (1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1)))
127118, 126mpan2d 692 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ ℝ) ∧ 𝑀 ∈ (1...𝑗)) β†’ ((1st β€˜(π½β€˜π‘€)) ≀ π‘₯ β†’ (1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1)))
128127ralimdva 3167 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯ β†’ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1)))
129128adantlr 713 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯ β†’ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1)))
130 ovoliun.t . . . . . . . . . 10 𝑇 = seq1( + , 𝐺)
131 ovoliun.g . . . . . . . . . 10 𝐺 = (𝑛 ∈ β„• ↦ (vol*β€˜π΄))
132 simpll 765 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ πœ‘)
133132, 1sylan 580 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† ℝ)
134 ovoliun.v . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (vol*β€˜π΄) ∈ ℝ)
135132, 134sylan 580 . . . . . . . . . 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 580 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
142 ovoliun.x2 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
143132, 142sylan 580 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) ∧ 𝑛 ∈ β„•) β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
144 simplr 767 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ 𝑗 ∈ β„•)
145122ad2antrl 726 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ β„€)
146 simprr 771 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))
147130, 131, 133, 135, 136, 137, 138, 24, 21, 139, 140, 141, 143, 144, 145, 146ovoliunlem1 25026 . . . . . . . . 9 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ (π‘₯ ∈ ℝ ∧ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
148147expr 457 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ ((βŒŠβ€˜π‘₯) + 1) β†’ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
149129, 148syld 47 . . . . . . 7 (((πœ‘ ∧ 𝑗 ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯ β†’ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
150149rexlimdva 3155 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (βˆƒπ‘₯ ∈ ℝ βˆ€π‘€ ∈ (1...𝑗)(1st β€˜(π½β€˜π‘€)) ≀ π‘₯ β†’ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
151116, 150mpd 15 . . . . 5 ((πœ‘ ∧ 𝑗 ∈ β„•) β†’ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
152151ralrimiva 3146 . . . 4 (πœ‘ β†’ βˆ€π‘— ∈ β„• (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
153 ffn 6717 . . . . 5 (π‘ˆ:β„•βŸΆ(0[,)+∞) β†’ π‘ˆ Fn β„•)
154 breq1 5151 . . . . . 6 (𝑧 = (π‘ˆβ€˜π‘—) β†’ (𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ↔ (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
155154ralrn 7089 . . . . 5 (π‘ˆ Fn β„• β†’ (βˆ€π‘§ ∈ ran π‘ˆ 𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ↔ βˆ€π‘— ∈ β„• (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
15622, 25, 153, 1554syl 19 . . . 4 (πœ‘ β†’ (βˆ€π‘§ ∈ ran π‘ˆ 𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ↔ βˆ€π‘— ∈ β„• (π‘ˆβ€˜π‘—) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
157152, 156mpbird 256 . . 3 (πœ‘ β†’ βˆ€π‘§ ∈ ran π‘ˆ 𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
158 supxrleub 13307 . . . 4 ((ran π‘ˆ βŠ† ℝ* ∧ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ∈ ℝ*) β†’ (sup(ran π‘ˆ, ℝ*, < ) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ↔ βˆ€π‘§ ∈ ran π‘ˆ 𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
15929, 36, 158syl2anc 584 . . 3 (πœ‘ β†’ (sup(ran π‘ˆ, ℝ*, < ) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ↔ βˆ€π‘§ ∈ ran π‘ˆ 𝑧 ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡)))
160157, 159mpbird 256 . 2 (πœ‘ β†’ sup(ran π‘ˆ, ℝ*, < ) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
1616, 31, 36, 105, 160xrletrd 13143 1 (πœ‘ β†’ (vol*β€˜βˆͺ 𝑛 ∈ β„• 𝐴) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  βˆƒwrex 3070   ∩ cin 3947   βŠ† wss 3948  βŸ¨cop 4634  βˆͺ cuni 4908  βˆͺ ciun 4997   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675  ran crn 5677   ∘ ccom 5680   Fn wfn 6538  βŸΆwf 6539  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  (class class class)co 7411  1st c1st 7975  2nd c2nd 7976   ↑m cmap 8822  Fincfn 8941  supcsup 9437  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115  +∞cpnf 11247  β„*cxr 11249   < clt 11250   ≀ cle 11251   βˆ’ cmin 11446   / cdiv 11873  β„•cn 12214  2c2 12269  β„€cz 12560  β„+crp 12976  (,)cioo 13326  [,)cico 13328  ...cfz 13486  βŒŠcfl 13757  seqcseq 13968  β†‘cexp 14029  abscabs 15183  vol*covol 24986
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-n0 12475  df-z 12561  df-uz 12825  df-rp 12977  df-ioo 13330  df-ico 13332  df-fz 13487  df-fzo 13630  df-fl 13759  df-seq 13969  df-exp 14030  df-hash 14293  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-clim 15434  df-rlim 15435  df-sum 15635  df-ovol 24988
This theorem is referenced by:  ovoliunlem3  25028
  Copyright terms: Public domain W3C validator