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

Theorem ovollb2lem 23302
 Description: Lemma for ovollb2 23303. (Contributed by Mario Carneiro, 24-Mar-2015.)
Hypotheses
Ref Expression
ovollb2.1 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ovollb2.2 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩)
ovollb2.3 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
ovollb2.4 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
ovollb2.5 (𝜑𝐴 ran ([,] ∘ 𝐹))
ovollb2.6 (𝜑𝐵 ∈ ℝ+)
ovollb2.7 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
Assertion
Ref Expression
ovollb2lem (𝜑 → (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
Distinct variable groups:   𝐴,𝑛   𝑛,𝐹   𝐵,𝑛   𝜑,𝑛   𝑆,𝑛
Allowed substitution hints:   𝑇(𝑛)   𝐺(𝑛)

Proof of Theorem ovollb2lem
Dummy variables 𝑚 𝑦 𝑧 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovollb2.5 . . . 4 (𝜑𝐴 ran ([,] ∘ 𝐹))
2 ovollb2.4 . . . . 5 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
3 ovolficcss 23284 . . . . 5 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐹) ⊆ ℝ)
42, 3syl 17 . . . 4 (𝜑 ran ([,] ∘ 𝐹) ⊆ ℝ)
51, 4sstrd 3646 . . 3 (𝜑𝐴 ⊆ ℝ)
6 ovolcl 23292 . . 3 (𝐴 ⊆ ℝ → (vol*‘𝐴) ∈ ℝ*)
75, 6syl 17 . 2 (𝜑 → (vol*‘𝐴) ∈ ℝ*)
8 ovolfcl 23281 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
92, 8sylan 487 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
109simp1d 1093 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
11 ovollb2.6 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℝ+)
1211rphalfcld 11922 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 / 2) ∈ ℝ+)
1312adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝐵 / 2) ∈ ℝ+)
14 2nn 11223 . . . . . . . . . . . . . . 15 2 ∈ ℕ
15 nnnn0 11337 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
1615adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
17 nnexpcl 12913 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
1814, 16, 17sylancr 696 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
1918nnrpd 11908 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
2013, 19rpdivcld 11927 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑛)) ∈ ℝ+)
2120rpred 11910 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑛)) ∈ ℝ)
2210, 21resubcld 10496 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) ∈ ℝ)
239simp2d 1094 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
2423, 21readdcld 10107 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))) ∈ ℝ)
2510, 20ltsubrpd 11942 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) < (1st ‘(𝐹𝑛)))
269simp3d 1095 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)))
2723, 20ltaddrpd 11943 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) < ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))))
2810, 23, 24, 26, 27lelttrd 10233 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) < ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))))
2922, 10, 24, 25, 28lttrd 10236 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) < ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))))
3022, 24, 29ltled 10223 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) ≤ ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))))
31 df-br 4686 . . . . . . . . 9 (((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) ≤ ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))) ↔ ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ ∈ ≤ )
3230, 31sylib 208 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ ∈ ≤ )
33 opelxpi 5182 . . . . . . . . 9 ((((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) ∈ ℝ ∧ ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))) ∈ ℝ) → ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ ∈ (ℝ × ℝ))
3422, 24, 33syl2anc 694 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ ∈ (ℝ × ℝ))
3532, 34elind 3831 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ ∈ ( ≤ ∩ (ℝ × ℝ)))
36 ovollb2.2 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩)
3735, 36fmptd 6425 . . . . . 6 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
38 eqid 2651 . . . . . . 7 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
39 ovollb2.3 . . . . . . 7 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
4038, 39ovolsf 23287 . . . . . 6 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
4137, 40syl 17 . . . . 5 (𝜑𝑇:ℕ⟶(0[,)+∞))
42 frn 6091 . . . . 5 (𝑇:ℕ⟶(0[,)+∞) → ran 𝑇 ⊆ (0[,)+∞))
4341, 42syl 17 . . . 4 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
44 icossxr 12296 . . . 4 (0[,)+∞) ⊆ ℝ*
4543, 44syl6ss 3648 . . 3 (𝜑 → ran 𝑇 ⊆ ℝ*)
46 supxrcl 12183 . . 3 (ran 𝑇 ⊆ ℝ* → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
4745, 46syl 17 . 2 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
48 ovollb2.7 . . . 4 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
4911rpred 11910 . . . 4 (𝜑𝐵 ∈ ℝ)
5048, 49readdcld 10107 . . 3 (𝜑 → (sup(ran 𝑆, ℝ*, < ) + 𝐵) ∈ ℝ)
5150rexrd 10127 . 2 (𝜑 → (sup(ran 𝑆, ℝ*, < ) + 𝐵) ∈ ℝ*)
52 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
5352fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → (1st ‘(𝐹𝑛)) = (1st ‘(𝐹𝑚)))
54 oveq2 6698 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚))
5554oveq2d 6706 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → ((𝐵 / 2) / (2↑𝑛)) = ((𝐵 / 2) / (2↑𝑚)))
5653, 55oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → ((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) = ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))))
5752fveq2d 6233 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → (2nd ‘(𝐹𝑛)) = (2nd ‘(𝐹𝑚)))
5857, 55oveq12d 6708 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))) = ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))))
5956, 58opeq12d 4441 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ = ⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩)
60 opex 4962 . . . . . . . . . . . . . . 15 ⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩ ∈ V
6159, 36, 60fvmpt 6321 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → (𝐺𝑚) = ⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩)
6261adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) = ⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩)
6362fveq2d 6233 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) = (1st ‘⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩))
64 ovex 6718 . . . . . . . . . . . . 13 ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))) ∈ V
65 ovex 6718 . . . . . . . . . . . . 13 ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))) ∈ V
6664, 65op1st 7218 . . . . . . . . . . . 12 (1st ‘⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩) = ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚)))
6763, 66syl6eq 2701 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) = ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))))
68 ovolfcl 23281 . . . . . . . . . . . . . 14 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → ((1st ‘(𝐹𝑚)) ∈ ℝ ∧ (2nd ‘(𝐹𝑚)) ∈ ℝ ∧ (1st ‘(𝐹𝑚)) ≤ (2nd ‘(𝐹𝑚))))
692, 68sylan 487 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝐹𝑚)) ∈ ℝ ∧ (2nd ‘(𝐹𝑚)) ∈ ℝ ∧ (1st ‘(𝐹𝑚)) ≤ (2nd ‘(𝐹𝑚))))
7069simp1d 1093 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℝ)
7112adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐵 / 2) ∈ ℝ+)
72 nnnn0 11337 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
7372adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ0)
74 nnexpcl 12913 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
7514, 73, 74sylancr 696 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2↑𝑚) ∈ ℕ)
7675nnrpd 11908 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (2↑𝑚) ∈ ℝ+)
7771, 76rpdivcld 11927 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑚)) ∈ ℝ+)
7870, 77ltsubrpd 11942 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))) < (1st ‘(𝐹𝑚)))
7967, 78eqbrtrd 4707 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) < (1st ‘(𝐹𝑚)))
8079adantlr 751 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) < (1st ‘(𝐹𝑚)))
81 ovolfcl 23281 . . . . . . . . . . . . 13 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → ((1st ‘(𝐺𝑚)) ∈ ℝ ∧ (2nd ‘(𝐺𝑚)) ∈ ℝ ∧ (1st ‘(𝐺𝑚)) ≤ (2nd ‘(𝐺𝑚))))
8237, 81sylan 487 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝐺𝑚)) ∈ ℝ ∧ (2nd ‘(𝐺𝑚)) ∈ ℝ ∧ (1st ‘(𝐺𝑚)) ≤ (2nd ‘(𝐺𝑚))))
8382simp1d 1093 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) ∈ ℝ)
8483adantlr 751 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) ∈ ℝ)
8570adantlr 751 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℝ)
865sselda 3636 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → 𝑧 ∈ ℝ)
8786adantr 480 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℝ)
88 ltletr 10167 . . . . . . . . . 10 (((1st ‘(𝐺𝑚)) ∈ ℝ ∧ (1st ‘(𝐹𝑚)) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((1st ‘(𝐺𝑚)) < (1st ‘(𝐹𝑚)) ∧ (1st ‘(𝐹𝑚)) ≤ 𝑧) → (1st ‘(𝐺𝑚)) < 𝑧))
8984, 85, 87, 88syl3anc 1366 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (((1st ‘(𝐺𝑚)) < (1st ‘(𝐹𝑚)) ∧ (1st ‘(𝐹𝑚)) ≤ 𝑧) → (1st ‘(𝐺𝑚)) < 𝑧))
9080, 89mpand 711 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → ((1st ‘(𝐹𝑚)) ≤ 𝑧 → (1st ‘(𝐺𝑚)) < 𝑧))
9169simp2d 1094 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℝ)
9291, 77ltaddrpd 11943 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) < ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))))
9362fveq2d 6233 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐺𝑚)) = (2nd ‘⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩))
9464, 65op2nd 7219 . . . . . . . . . . . 12 (2nd ‘⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩) = ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))
9593, 94syl6eq 2701 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐺𝑚)) = ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))))
9692, 95breqtrrd 4713 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) < (2nd ‘(𝐺𝑚)))
9796adantlr 751 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) < (2nd ‘(𝐺𝑚)))
9891adantlr 751 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℝ)
9982simp2d 1094 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐺𝑚)) ∈ ℝ)
10099adantlr 751 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (2nd ‘(𝐺𝑚)) ∈ ℝ)
101 lelttr 10166 . . . . . . . . . 10 ((𝑧 ∈ ℝ ∧ (2nd ‘(𝐹𝑚)) ∈ ℝ ∧ (2nd ‘(𝐺𝑚)) ∈ ℝ) → ((𝑧 ≤ (2nd ‘(𝐹𝑚)) ∧ (2nd ‘(𝐹𝑚)) < (2nd ‘(𝐺𝑚))) → 𝑧 < (2nd ‘(𝐺𝑚))))
10287, 98, 100, 101syl3anc 1366 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → ((𝑧 ≤ (2nd ‘(𝐹𝑚)) ∧ (2nd ‘(𝐹𝑚)) < (2nd ‘(𝐺𝑚))) → 𝑧 < (2nd ‘(𝐺𝑚))))
10397, 102mpan2d 710 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (𝑧 ≤ (2nd ‘(𝐹𝑚)) → 𝑧 < (2nd ‘(𝐺𝑚))))
10490, 103anim12d 585 . . . . . . 7 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (((1st ‘(𝐹𝑚)) ≤ 𝑧𝑧 ≤ (2nd ‘(𝐹𝑚))) → ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
105104reximdva 3046 . . . . . 6 ((𝜑𝑧𝐴) → (∃𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) ≤ 𝑧𝑧 ≤ (2nd ‘(𝐹𝑚))) → ∃𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
106105ralimdva 2991 . . . . 5 (𝜑 → (∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) ≤ 𝑧𝑧 ≤ (2nd ‘(𝐹𝑚))) → ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
107 ovolficc 23283 . . . . . 6 ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ran ([,] ∘ 𝐹) ↔ ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) ≤ 𝑧𝑧 ≤ (2nd ‘(𝐹𝑚)))))
1085, 2, 107syl2anc 694 . . . . 5 (𝜑 → (𝐴 ran ([,] ∘ 𝐹) ↔ ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) ≤ 𝑧𝑧 ≤ (2nd ‘(𝐹𝑚)))))
109 ovolfioo 23282 . . . . . 6 ((𝐴 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ran ((,) ∘ 𝐺) ↔ ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
1105, 37, 109syl2anc 694 . . . . 5 (𝜑 → (𝐴 ran ((,) ∘ 𝐺) ↔ ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
111106, 108, 1103imtr4d 283 . . . 4 (𝜑 → (𝐴 ran ([,] ∘ 𝐹) → 𝐴 ran ((,) ∘ 𝐺)))
1121, 111mpd 15 . . 3 (𝜑𝐴 ran ((,) ∘ 𝐺))
11339ovollb 23293 . . 3 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ran ((,) ∘ 𝐺)) → (vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
11437, 112, 113syl2anc 694 . 2 (𝜑 → (vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
11539fveq1i 6230 . . . . . . 7 (𝑇𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
116 fzfid 12812 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
117 rge0ssre 12318 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ
118 eqid 2651 . . . . . . . . . . . . . . 15 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
119118ovolfsf 23286 . . . . . . . . . . . . . 14 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
1202, 119syl 17 . . . . . . . . . . . . 13 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
121120adantr 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
122 elfznn 12408 . . . . . . . . . . . 12 (𝑚 ∈ (1...𝑘) → 𝑚 ∈ ℕ)
123 ffvelrn 6397 . . . . . . . . . . . 12 ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ 𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) ∈ (0[,)+∞))
124121, 122, 123syl2an 493 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) ∈ (0[,)+∞))
125117, 124sseldi 3634 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) ∈ ℝ)
126125recnd 10106 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) ∈ ℂ)
12711adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → 𝐵 ∈ ℝ+)
128127, 76rpdivcld 11927 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐵 / (2↑𝑚)) ∈ ℝ+)
129128rpcnd 11912 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐵 / (2↑𝑚)) ∈ ℂ)
130122, 129sylan2 490 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1...𝑘)) → (𝐵 / (2↑𝑚)) ∈ ℂ)
131130adantlr 751 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (𝐵 / (2↑𝑚)) ∈ ℂ)
132116, 126, 131fsumadd 14514 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = (Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) + Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚))))
13338ovolfsval 23285 . . . . . . . . . . . . 13 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑚) = ((2nd ‘(𝐺𝑚)) − (1st ‘(𝐺𝑚))))
13437, 133sylan 487 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑚) = ((2nd ‘(𝐺𝑚)) − (1st ‘(𝐺𝑚))))
13591recnd 10106 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℂ)
13677rpcnd 11912 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑚)) ∈ ℂ)
13770recnd 10106 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℂ)
138137, 136subcld 10430 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))) ∈ ℂ)
139135, 136, 138addsubassd 10450 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) = ((2nd ‘(𝐹𝑚)) + (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))))))
14095, 67oveq12d 6708 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((2nd ‘(𝐺𝑚)) − (1st ‘(𝐺𝑚))) = (((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚)))))
141135, 137, 129subadd23d 10452 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (((2nd ‘(𝐹𝑚)) − (1st ‘(𝐹𝑚))) + (𝐵 / (2↑𝑚))) = ((2nd ‘(𝐹𝑚)) + ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹𝑚)))))
142118ovolfsval 23285 . . . . . . . . . . . . . . . 16 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) = ((2nd ‘(𝐹𝑚)) − (1st ‘(𝐹𝑚))))
1432, 142sylan 487 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) = ((2nd ‘(𝐹𝑚)) − (1st ‘(𝐹𝑚))))
144143oveq1d 6705 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = (((2nd ‘(𝐹𝑚)) − (1st ‘(𝐹𝑚))) + (𝐵 / (2↑𝑚))))
145136, 137, 136subsub3d 10460 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) = ((((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − (1st ‘(𝐹𝑚))))
14671rpcnd 11912 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → (𝐵 / 2) ∈ ℂ)
14775nncnd 11074 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → (2↑𝑚) ∈ ℂ)
14875nnne0d 11103 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → (2↑𝑚) ≠ 0)
149146, 146, 147, 148divdird 10877 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ ℕ) → (((𝐵 / 2) + (𝐵 / 2)) / (2↑𝑚)) = (((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))))
150127rpcnd 11912 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ ℕ) → 𝐵 ∈ ℂ)
1511502halvesd 11316 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → ((𝐵 / 2) + (𝐵 / 2)) = 𝐵)
152151oveq1d 6705 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ ℕ) → (((𝐵 / 2) + (𝐵 / 2)) / (2↑𝑚)) = (𝐵 / (2↑𝑚)))
153149, 152eqtr3d 2687 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ ℕ) → (((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))) = (𝐵 / (2↑𝑚)))
154153oveq1d 6705 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → ((((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − (1st ‘(𝐹𝑚))) = ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹𝑚))))
155145, 154eqtrd 2685 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) = ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹𝑚))))
156155oveq2d 6706 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((2nd ‘(𝐹𝑚)) + (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))))) = ((2nd ‘(𝐹𝑚)) + ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹𝑚)))))
157141, 144, 1563eqtr4d 2695 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = ((2nd ‘(𝐹𝑚)) + (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))))))
158139, 140, 1573eqtr4d 2695 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((2nd ‘(𝐺𝑚)) − (1st ‘(𝐺𝑚))) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))))
159134, 158eqtrd 2685 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑚) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))))
160122, 159sylan2 490 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐺)‘𝑚) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))))
161160adantlr 751 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐺)‘𝑚) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))))
162 simpr 476 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
163 nnuz 11761 . . . . . . . . . 10 ℕ = (ℤ‘1)
164162, 163syl6eleq 2740 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
165126, 131addcld 10097 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) ∈ ℂ)
166161, 164, 165fsumser 14505 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘))
167 eqidd 2652 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) = (((abs ∘ − ) ∘ 𝐹)‘𝑚))
168167, 164, 126fsumser 14505 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘))
169 ovollb2.1 . . . . . . . . . . 11 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
170169fveq1i 6230 . . . . . . . . . 10 (𝑆𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
171168, 170syl6eqr 2703 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) = (𝑆𝑘))
17211adantr 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → 𝐵 ∈ ℝ+)
173172rpcnd 11912 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
174 geo2sum 14648 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝐵 ∈ ℂ) → Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚)) = (𝐵 − (𝐵 / (2↑𝑘))))
175162, 173, 174syl2anc 694 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚)) = (𝐵 − (𝐵 / (2↑𝑘))))
176171, 175oveq12d 6708 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) + Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚))) = ((𝑆𝑘) + (𝐵 − (𝐵 / (2↑𝑘)))))
177132, 166, 1763eqtr3d 2693 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) = ((𝑆𝑘) + (𝐵 − (𝐵 / (2↑𝑘)))))
178115, 177syl5eq 2697 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) = ((𝑆𝑘) + (𝐵 − (𝐵 / (2↑𝑘)))))
179118, 169ovolsf 23287 . . . . . . . . . 10 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
1802, 179syl 17 . . . . . . . . 9 (𝜑𝑆:ℕ⟶(0[,)+∞))
181180ffvelrnda 6399 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ (0[,)+∞))
182117, 181sseldi 3634 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
183172rpred 11910 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝐵 ∈ ℝ)
184 nnnn0 11337 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
185184adantl 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0)
186 nnexpcl 12913 . . . . . . . . . . . 12 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
18714, 185, 186sylancr 696 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (2↑𝑘) ∈ ℕ)
188187nnrpd 11908 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (2↑𝑘) ∈ ℝ+)
189172, 188rpdivcld 11927 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐵 / (2↑𝑘)) ∈ ℝ+)
190189rpred 11910 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐵 / (2↑𝑘)) ∈ ℝ)
191183, 190resubcld 10496 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝐵 − (𝐵 / (2↑𝑘))) ∈ ℝ)
19248adantr 480 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
193 frn 6091 . . . . . . . . . . 11 (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
194180, 193syl 17 . . . . . . . . . 10 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
195194, 44syl6ss 3648 . . . . . . . . 9 (𝜑 → ran 𝑆 ⊆ ℝ*)
196195adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
197 ffn 6083 . . . . . . . . . 10 (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
198180, 197syl 17 . . . . . . . . 9 (𝜑𝑆 Fn ℕ)
199 fnfvelrn 6396 . . . . . . . . 9 ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ran 𝑆)
200198, 199sylan 487 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ran 𝑆)
201 supxrub 12192 . . . . . . . 8 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆𝑘) ∈ ran 𝑆) → (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
202196, 200, 201syl2anc 694 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
203183, 189ltsubrpd 11942 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐵 − (𝐵 / (2↑𝑘))) < 𝐵)
204191, 183, 203ltled 10223 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝐵 − (𝐵 / (2↑𝑘))) ≤ 𝐵)
205182, 191, 192, 183, 202, 204le2addd 10684 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((𝑆𝑘) + (𝐵 − (𝐵 / (2↑𝑘)))) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
206178, 205eqbrtrd 4707 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
207206ralrimiva 2995 . . . 4 (𝜑 → ∀𝑘 ∈ ℕ (𝑇𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
208 ffn 6083 . . . . 5 (𝑇:ℕ⟶(0[,)+∞) → 𝑇 Fn ℕ)
209 breq1 4688 . . . . . 6 (𝑦 = (𝑇𝑘) → (𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ (𝑇𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)))
210209ralrn 6402 . . . . 5 (𝑇 Fn ℕ → (∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑘 ∈ ℕ (𝑇𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)))
21141, 208, 2103syl 18 . . . 4 (𝜑 → (∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑘 ∈ ℕ (𝑇𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)))
212207, 211mpbird 247 . . 3 (𝜑 → ∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
213 supxrleub 12194 . . . 4 ((ran 𝑇 ⊆ ℝ* ∧ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ∈ ℝ*) → (sup(ran 𝑇, ℝ*, < ) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)))
21445, 51, 213syl2anc 694 . . 3 (𝜑 → (sup(ran 𝑇, ℝ*, < ) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)))
215212, 214mpbird 247 . 2 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
2167, 47, 51, 114, 215xrletrd 12031 1 (𝜑 → (vol*‘𝐴) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942   ∩ cin 3606   ⊆ wss 3607  ⟨cop 4216  ∪ cuni 4468   class class class wbr 4685   ↦ cmpt 4762   × cxp 5141  ran crn 5144   ∘ ccom 5147   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  supcsup 8387  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977  +∞cpnf 10109  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304   / cdiv 10722  ℕcn 11058  2c2 11108  ℕ0cn0 11330  ℤ≥cuz 11725  ℝ+crp 11870  (,)cioo 12213  [,)cico 12215  [,]cicc 12216  ...cfz 12364  seqcseq 12841  ↑cexp 12900  abscabs 14018  Σcsu 14460  vol*covol 23277 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-ioo 12217  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-ovol 23279 This theorem is referenced by:  ovollb2  23303
 Copyright terms: Public domain W3C validator