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

Theorem ovollb2lem 24875
Description: Lemma for ovollb2 24876. (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 24856 . . . . 5 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ran ([,] ∘ 𝐹) ⊆ ℝ)
42, 3syl 17 . . . 4 (𝜑 ran ([,] ∘ 𝐹) ⊆ ℝ)
51, 4sstrd 3958 . . 3 (𝜑𝐴 ⊆ ℝ)
6 ovolcl 24865 . . 3 (𝐴 ⊆ ℝ → (vol*‘𝐴) ∈ ℝ*)
75, 6syl 17 . 2 (𝜑 → (vol*‘𝐴) ∈ ℝ*)
8 ovolfcl 24853 . . . . . . . . . . . . 13 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
92, 8sylan 581 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
109simp1d 1143 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
11 ovollb2.6 . . . . . . . . . . . . . . 15 (𝜑𝐵 ∈ ℝ+)
1211rphalfcld 12977 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 / 2) ∈ ℝ+)
1312adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝐵 / 2) ∈ ℝ+)
14 2nn 12234 . . . . . . . . . . . . . . 15 2 ∈ ℕ
15 nnnn0 12428 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
1615adantl 483 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
17 nnexpcl 13989 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
1814, 16, 17sylancr 588 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℕ)
1918nnrpd 12963 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (2↑𝑛) ∈ ℝ+)
2013, 19rpdivcld 12982 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑛)) ∈ ℝ+)
2120rpred 12965 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑛)) ∈ ℝ)
2210, 21resubcld 11591 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) ∈ ℝ)
239simp2d 1144 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
2423, 21readdcld 11192 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))) ∈ ℝ)
2510, 20ltsubrpd 12997 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) < (1st ‘(𝐹𝑛)))
269simp3d 1145 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)))
2723, 20ltaddrpd 12998 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) < ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))))
2810, 23, 24, 26, 27lelttrd 11321 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) < ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))))
2922, 10, 24, 25, 28lttrd 11324 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) < ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))))
3022, 24, 29ltled 11311 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) ≤ ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))))
31 df-br 5110 . . . . . . . . 9 (((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) ≤ ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))) ↔ ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ ∈ ≤ )
3230, 31sylib 217 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ ∈ ≤ )
3322, 24opelxpd 5675 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ ∈ (ℝ × ℝ))
3432, 33elind 4158 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ ∈ ( ≤ ∩ (ℝ × ℝ)))
35 ovollb2.2 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩)
3634, 35fmptd 7066 . . . . . 6 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
37 eqid 2733 . . . . . . 7 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
38 ovollb2.3 . . . . . . 7 𝑇 = seq1( + , ((abs ∘ − ) ∘ 𝐺))
3937, 38ovolsf 24859 . . . . . 6 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑇:ℕ⟶(0[,)+∞))
4036, 39syl 17 . . . . 5 (𝜑𝑇:ℕ⟶(0[,)+∞))
4140frnd 6680 . . . 4 (𝜑 → ran 𝑇 ⊆ (0[,)+∞))
42 icossxr 13358 . . . 4 (0[,)+∞) ⊆ ℝ*
4341, 42sstrdi 3960 . . 3 (𝜑 → ran 𝑇 ⊆ ℝ*)
44 supxrcl 13243 . . 3 (ran 𝑇 ⊆ ℝ* → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
4543, 44syl 17 . 2 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ*)
46 ovollb2.7 . . . 4 (𝜑 → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
4711rpred 12965 . . . 4 (𝜑𝐵 ∈ ℝ)
4846, 47readdcld 11192 . . 3 (𝜑 → (sup(ran 𝑆, ℝ*, < ) + 𝐵) ∈ ℝ)
4948rexrd 11213 . 2 (𝜑 → (sup(ran 𝑆, ℝ*, < ) + 𝐵) ∈ ℝ*)
50 2fveq3 6851 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → (1st ‘(𝐹𝑛)) = (1st ‘(𝐹𝑚)))
51 oveq2 7369 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑚 → (2↑𝑛) = (2↑𝑚))
5251oveq2d 7377 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → ((𝐵 / 2) / (2↑𝑛)) = ((𝐵 / 2) / (2↑𝑚)))
5350, 52oveq12d 7379 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → ((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))) = ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))))
54 2fveq3 6851 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑚 → (2nd ‘(𝐹𝑛)) = (2nd ‘(𝐹𝑚)))
5554, 52oveq12d 7379 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑚 → ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛))) = ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))))
5653, 55opeq12d 4842 . . . . . . . . . . . . . . 15 (𝑛 = 𝑚 → ⟨((1st ‘(𝐹𝑛)) − ((𝐵 / 2) / (2↑𝑛))), ((2nd ‘(𝐹𝑛)) + ((𝐵 / 2) / (2↑𝑛)))⟩ = ⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩)
57 opex 5425 . . . . . . . . . . . . . . 15 ⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩ ∈ V
5856, 35, 57fvmpt 6952 . . . . . . . . . . . . . 14 (𝑚 ∈ ℕ → (𝐺𝑚) = ⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩)
5958adantl 483 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐺𝑚) = ⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩)
6059fveq2d 6850 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) = (1st ‘⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩))
61 ovex 7394 . . . . . . . . . . . . 13 ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))) ∈ V
62 ovex 7394 . . . . . . . . . . . . 13 ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))) ∈ V
6361, 62op1st 7933 . . . . . . . . . . . 12 (1st ‘⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩) = ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚)))
6460, 63eqtrdi 2789 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) = ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))))
65 ovolfcl 24853 . . . . . . . . . . . . . 14 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → ((1st ‘(𝐹𝑚)) ∈ ℝ ∧ (2nd ‘(𝐹𝑚)) ∈ ℝ ∧ (1st ‘(𝐹𝑚)) ≤ (2nd ‘(𝐹𝑚))))
662, 65sylan 581 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝐹𝑚)) ∈ ℝ ∧ (2nd ‘(𝐹𝑚)) ∈ ℝ ∧ (1st ‘(𝐹𝑚)) ≤ (2nd ‘(𝐹𝑚))))
6766simp1d 1143 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℝ)
6812adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (𝐵 / 2) ∈ ℝ+)
69 nnnn0 12428 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → 𝑚 ∈ ℕ0)
7069adantl 483 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℕ0)
71 nnexpcl 13989 . . . . . . . . . . . . . . 15 ((2 ∈ ℕ ∧ 𝑚 ∈ ℕ0) → (2↑𝑚) ∈ ℕ)
7214, 70, 71sylancr 588 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2↑𝑚) ∈ ℕ)
7372nnrpd 12963 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (2↑𝑚) ∈ ℝ+)
7468, 73rpdivcld 12982 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑚)) ∈ ℝ+)
7567, 74ltsubrpd 12997 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))) < (1st ‘(𝐹𝑚)))
7664, 75eqbrtrd 5131 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) < (1st ‘(𝐹𝑚)))
7776adantlr 714 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) < (1st ‘(𝐹𝑚)))
78 ovolfcl 24853 . . . . . . . . . . . . 13 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → ((1st ‘(𝐺𝑚)) ∈ ℝ ∧ (2nd ‘(𝐺𝑚)) ∈ ℝ ∧ (1st ‘(𝐺𝑚)) ≤ (2nd ‘(𝐺𝑚))))
7936, 78sylan 581 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝐺𝑚)) ∈ ℝ ∧ (2nd ‘(𝐺𝑚)) ∈ ℝ ∧ (1st ‘(𝐺𝑚)) ≤ (2nd ‘(𝐺𝑚))))
8079simp1d 1143 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) ∈ ℝ)
8180adantlr 714 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (1st ‘(𝐺𝑚)) ∈ ℝ)
8267adantlr 714 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℝ)
835sselda 3948 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → 𝑧 ∈ ℝ)
8483adantr 482 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → 𝑧 ∈ ℝ)
85 ltletr 11255 . . . . . . . . . 10 (((1st ‘(𝐺𝑚)) ∈ ℝ ∧ (1st ‘(𝐹𝑚)) ∈ ℝ ∧ 𝑧 ∈ ℝ) → (((1st ‘(𝐺𝑚)) < (1st ‘(𝐹𝑚)) ∧ (1st ‘(𝐹𝑚)) ≤ 𝑧) → (1st ‘(𝐺𝑚)) < 𝑧))
8681, 82, 84, 85syl3anc 1372 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (((1st ‘(𝐺𝑚)) < (1st ‘(𝐹𝑚)) ∧ (1st ‘(𝐹𝑚)) ≤ 𝑧) → (1st ‘(𝐺𝑚)) < 𝑧))
8777, 86mpand 694 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → ((1st ‘(𝐹𝑚)) ≤ 𝑧 → (1st ‘(𝐺𝑚)) < 𝑧))
8866simp2d 1144 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℝ)
8988, 74ltaddrpd 12998 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) < ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))))
9059fveq2d 6850 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐺𝑚)) = (2nd ‘⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩))
9161, 62op2nd 7934 . . . . . . . . . . . 12 (2nd ‘⟨((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))), ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))⟩) = ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚)))
9290, 91eqtrdi 2789 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐺𝑚)) = ((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))))
9389, 92breqtrrd 5137 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) < (2nd ‘(𝐺𝑚)))
9493adantlr 714 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) < (2nd ‘(𝐺𝑚)))
9588adantlr 714 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℝ)
9679simp2d 1144 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐺𝑚)) ∈ ℝ)
9796adantlr 714 . . . . . . . . . 10 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (2nd ‘(𝐺𝑚)) ∈ ℝ)
98 lelttr 11253 . . . . . . . . . 10 ((𝑧 ∈ ℝ ∧ (2nd ‘(𝐹𝑚)) ∈ ℝ ∧ (2nd ‘(𝐺𝑚)) ∈ ℝ) → ((𝑧 ≤ (2nd ‘(𝐹𝑚)) ∧ (2nd ‘(𝐹𝑚)) < (2nd ‘(𝐺𝑚))) → 𝑧 < (2nd ‘(𝐺𝑚))))
9984, 95, 97, 98syl3anc 1372 . . . . . . . . 9 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → ((𝑧 ≤ (2nd ‘(𝐹𝑚)) ∧ (2nd ‘(𝐹𝑚)) < (2nd ‘(𝐺𝑚))) → 𝑧 < (2nd ‘(𝐺𝑚))))
10094, 99mpan2d 693 . . . . . . . 8 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (𝑧 ≤ (2nd ‘(𝐹𝑚)) → 𝑧 < (2nd ‘(𝐺𝑚))))
10187, 100anim12d 610 . . . . . . 7 (((𝜑𝑧𝐴) ∧ 𝑚 ∈ ℕ) → (((1st ‘(𝐹𝑚)) ≤ 𝑧𝑧 ≤ (2nd ‘(𝐹𝑚))) → ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
102101reximdva 3162 . . . . . 6 ((𝜑𝑧𝐴) → (∃𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) ≤ 𝑧𝑧 ≤ (2nd ‘(𝐹𝑚))) → ∃𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
103102ralimdva 3161 . . . . 5 (𝜑 → (∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) ≤ 𝑧𝑧 ≤ (2nd ‘(𝐹𝑚))) → ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
104 ovolficc 24855 . . . . . 6 ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ran ([,] ∘ 𝐹) ↔ ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) ≤ 𝑧𝑧 ≤ (2nd ‘(𝐹𝑚)))))
1055, 2, 104syl2anc 585 . . . . 5 (𝜑 → (𝐴 ran ([,] ∘ 𝐹) ↔ ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐹𝑚)) ≤ 𝑧𝑧 ≤ (2nd ‘(𝐹𝑚)))))
106 ovolfioo 24854 . . . . . 6 ((𝐴 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ran ((,) ∘ 𝐺) ↔ ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
1075, 36, 106syl2anc 585 . . . . 5 (𝜑 → (𝐴 ran ((,) ∘ 𝐺) ↔ ∀𝑧𝐴𝑚 ∈ ℕ ((1st ‘(𝐺𝑚)) < 𝑧𝑧 < (2nd ‘(𝐺𝑚)))))
108103, 105, 1073imtr4d 294 . . . 4 (𝜑 → (𝐴 ran ([,] ∘ 𝐹) → 𝐴 ran ((,) ∘ 𝐺)))
1091, 108mpd 15 . . 3 (𝜑𝐴 ran ((,) ∘ 𝐺))
11038ovollb 24866 . . 3 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ran ((,) ∘ 𝐺)) → (vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
11136, 109, 110syl2anc 585 . 2 (𝜑 → (vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
11238fveq1i 6847 . . . . . . 7 (𝑇𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘)
113 fzfid 13887 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
114 rge0ssre 13382 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ
115 eqid 2733 . . . . . . . . . . . . . . 15 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
116115ovolfsf 24858 . . . . . . . . . . . . . 14 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
1172, 116syl 17 . . . . . . . . . . . . 13 (𝜑 → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
118117adantr 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → ((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞))
119 elfznn 13479 . . . . . . . . . . . 12 (𝑚 ∈ (1...𝑘) → 𝑚 ∈ ℕ)
120 ffvelcdm 7036 . . . . . . . . . . . 12 ((((abs ∘ − ) ∘ 𝐹):ℕ⟶(0[,)+∞) ∧ 𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) ∈ (0[,)+∞))
121118, 119, 120syl2an 597 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) ∈ (0[,)+∞))
122114, 121sselid 3946 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) ∈ ℝ)
123122recnd 11191 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) ∈ ℂ)
12411adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → 𝐵 ∈ ℝ+)
125124, 73rpdivcld 12982 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (𝐵 / (2↑𝑚)) ∈ ℝ+)
126125rpcnd 12967 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝐵 / (2↑𝑚)) ∈ ℂ)
127119, 126sylan2 594 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1...𝑘)) → (𝐵 / (2↑𝑚)) ∈ ℂ)
128127adantlr 714 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (𝐵 / (2↑𝑚)) ∈ ℂ)
129113, 123, 128fsumadd 15633 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = (Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) + Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚))))
13037ovolfsval 24857 . . . . . . . . . . . . 13 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑚) = ((2nd ‘(𝐺𝑚)) − (1st ‘(𝐺𝑚))))
13136, 130sylan 581 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑚) = ((2nd ‘(𝐺𝑚)) − (1st ‘(𝐺𝑚))))
13288recnd 11191 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (2nd ‘(𝐹𝑚)) ∈ ℂ)
13374rpcnd 12967 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((𝐵 / 2) / (2↑𝑚)) ∈ ℂ)
13467recnd 11191 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (1st ‘(𝐹𝑚)) ∈ ℂ)
135134, 133subcld 11520 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))) ∈ ℂ)
136132, 133, 135addsubassd 11540 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → (((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) = ((2nd ‘(𝐹𝑚)) + (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))))))
13792, 64oveq12d 7379 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((2nd ‘(𝐺𝑚)) − (1st ‘(𝐺𝑚))) = (((2nd ‘(𝐹𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚)))))
138132, 134, 126subadd23d 11542 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → (((2nd ‘(𝐹𝑚)) − (1st ‘(𝐹𝑚))) + (𝐵 / (2↑𝑚))) = ((2nd ‘(𝐹𝑚)) + ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹𝑚)))))
139115ovolfsval 24857 . . . . . . . . . . . . . . . 16 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) = ((2nd ‘(𝐹𝑚)) − (1st ‘(𝐹𝑚))))
1402, 139sylan 581 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) = ((2nd ‘(𝐹𝑚)) − (1st ‘(𝐹𝑚))))
141140oveq1d 7376 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = (((2nd ‘(𝐹𝑚)) − (1st ‘(𝐹𝑚))) + (𝐵 / (2↑𝑚))))
142133, 134, 133subsub3d 11550 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) = ((((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − (1st ‘(𝐹𝑚))))
14368rpcnd 12967 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → (𝐵 / 2) ∈ ℂ)
14472nncnd 12177 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → (2↑𝑚) ∈ ℂ)
14572nnne0d 12211 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → (2↑𝑚) ≠ 0)
146143, 143, 144, 145divdird 11977 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ ℕ) → (((𝐵 / 2) + (𝐵 / 2)) / (2↑𝑚)) = (((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))))
147124rpcnd 12967 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ ℕ) → 𝐵 ∈ ℂ)
1481472halvesd 12407 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑚 ∈ ℕ) → ((𝐵 / 2) + (𝐵 / 2)) = 𝐵)
149148oveq1d 7376 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ ℕ) → (((𝐵 / 2) + (𝐵 / 2)) / (2↑𝑚)) = (𝐵 / (2↑𝑚)))
150146, 149eqtr3d 2775 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ ℕ) → (((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))) = (𝐵 / (2↑𝑚)))
151150oveq1d 7376 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ ℕ) → ((((𝐵 / 2) / (2↑𝑚)) + ((𝐵 / 2) / (2↑𝑚))) − (1st ‘(𝐹𝑚))) = ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹𝑚))))
152142, 151eqtrd 2773 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ ℕ) → (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚)))) = ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹𝑚))))
153152oveq2d 7377 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ ℕ) → ((2nd ‘(𝐹𝑚)) + (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))))) = ((2nd ‘(𝐹𝑚)) + ((𝐵 / (2↑𝑚)) − (1st ‘(𝐹𝑚)))))
154138, 141, 1533eqtr4d 2783 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ ℕ) → ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = ((2nd ‘(𝐹𝑚)) + (((𝐵 / 2) / (2↑𝑚)) − ((1st ‘(𝐹𝑚)) − ((𝐵 / 2) / (2↑𝑚))))))
155136, 137, 1543eqtr4d 2783 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → ((2nd ‘(𝐺𝑚)) − (1st ‘(𝐺𝑚))) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))))
156131, 155eqtrd 2773 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑚) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))))
157119, 156sylan2 594 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐺)‘𝑚) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))))
158157adantlr 714 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐺)‘𝑚) = ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))))
159 simpr 486 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
160 nnuz 12814 . . . . . . . . . 10 ℕ = (ℤ‘1)
161159, 160eleqtrdi 2844 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
162123, 128addcld 11182 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → ((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) ∈ ℂ)
163158, 161, 162fsumser 15623 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)((((abs ∘ − ) ∘ 𝐹)‘𝑚) + (𝐵 / (2↑𝑚))) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘))
164 eqidd 2734 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑚 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐹)‘𝑚) = (((abs ∘ − ) ∘ 𝐹)‘𝑚))
165164, 161, 123fsumser 15623 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘))
166 ovollb2.1 . . . . . . . . . . 11 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
167166fveq1i 6847 . . . . . . . . . 10 (𝑆𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
168165, 167eqtr4di 2791 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) = (𝑆𝑘))
16911adantr 482 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → 𝐵 ∈ ℝ+)
170169rpcnd 12967 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝐵 ∈ ℂ)
171 geo2sum 15766 . . . . . . . . . 10 ((𝑘 ∈ ℕ ∧ 𝐵 ∈ ℂ) → Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚)) = (𝐵 − (𝐵 / (2↑𝑘))))
172159, 170, 171syl2anc 585 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚)) = (𝐵 − (𝐵 / (2↑𝑘))))
173168, 172oveq12d 7379 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (Σ𝑚 ∈ (1...𝑘)(((abs ∘ − ) ∘ 𝐹)‘𝑚) + Σ𝑚 ∈ (1...𝑘)(𝐵 / (2↑𝑚))) = ((𝑆𝑘) + (𝐵 − (𝐵 / (2↑𝑘)))))
174129, 163, 1733eqtr3d 2781 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) = ((𝑆𝑘) + (𝐵 − (𝐵 / (2↑𝑘)))))
175112, 174eqtrid 2785 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) = ((𝑆𝑘) + (𝐵 − (𝐵 / (2↑𝑘)))))
176115, 166ovolsf 24859 . . . . . . . . . 10 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
1772, 176syl 17 . . . . . . . . 9 (𝜑𝑆:ℕ⟶(0[,)+∞))
178177ffvelcdmda 7039 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ (0[,)+∞))
179114, 178sselid 3946 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ℝ)
180169rpred 12965 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝐵 ∈ ℝ)
181 nnnn0 12428 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
182181adantl 483 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0)
183 nnexpcl 13989 . . . . . . . . . . . 12 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
18414, 182, 183sylancr 588 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (2↑𝑘) ∈ ℕ)
185184nnrpd 12963 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (2↑𝑘) ∈ ℝ+)
186169, 185rpdivcld 12982 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐵 / (2↑𝑘)) ∈ ℝ+)
187186rpred 12965 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐵 / (2↑𝑘)) ∈ ℝ)
188180, 187resubcld 11591 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝐵 − (𝐵 / (2↑𝑘))) ∈ ℝ)
18946adantr 482 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
190177frnd 6680 . . . . . . . . . 10 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
191190, 42sstrdi 3960 . . . . . . . . 9 (𝜑 → ran 𝑆 ⊆ ℝ*)
192191adantr 482 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ran 𝑆 ⊆ ℝ*)
193177ffnd 6673 . . . . . . . . 9 (𝜑𝑆 Fn ℕ)
194 fnfvelrn 7035 . . . . . . . . 9 ((𝑆 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ran 𝑆)
195193, 194sylan 581 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ∈ ran 𝑆)
196 supxrub 13252 . . . . . . . 8 ((ran 𝑆 ⊆ ℝ* ∧ (𝑆𝑘) ∈ ran 𝑆) → (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
197192, 195, 196syl2anc 585 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ≤ sup(ran 𝑆, ℝ*, < ))
198180, 186ltsubrpd 12997 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐵 − (𝐵 / (2↑𝑘))) < 𝐵)
199188, 180, 198ltled 11311 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (𝐵 − (𝐵 / (2↑𝑘))) ≤ 𝐵)
200179, 188, 189, 180, 197, 199le2addd 11782 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → ((𝑆𝑘) + (𝐵 − (𝐵 / (2↑𝑘)))) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
201175, 200eqbrtrd 5131 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (𝑇𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
202201ralrimiva 3140 . . . 4 (𝜑 → ∀𝑘 ∈ ℕ (𝑇𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
203 ffn 6672 . . . . 5 (𝑇:ℕ⟶(0[,)+∞) → 𝑇 Fn ℕ)
204 breq1 5112 . . . . . 6 (𝑦 = (𝑇𝑘) → (𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ (𝑇𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)))
205204ralrn 7042 . . . . 5 (𝑇 Fn ℕ → (∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑘 ∈ ℕ (𝑇𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)))
20640, 203, 2053syl 18 . . . 4 (𝜑 → (∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑘 ∈ ℕ (𝑇𝑘) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)))
207202, 206mpbird 257 . . 3 (𝜑 → ∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
208 supxrleub 13254 . . . 4 ((ran 𝑇 ⊆ ℝ* ∧ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ∈ ℝ*) → (sup(ran 𝑇, ℝ*, < ) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)))
20943, 49, 208syl2anc 585 . . 3 (𝜑 → (sup(ran 𝑇, ℝ*, < ) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵) ↔ ∀𝑦 ∈ ran 𝑇 𝑦 ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵)))
210207, 209mpbird 257 . 2 (𝜑 → sup(ran 𝑇, ℝ*, < ) ≤ (sup(ran 𝑆, ℝ*, < ) + 𝐵))
2117, 45, 49, 111, 210xrletrd 13090 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 3061  wrex 3070  cin 3913  wss 3914  cop 4596   cuni 4869   class class class wbr 5109  cmpt 5192   × cxp 5635  ran crn 5638  ccom 5641   Fn wfn 6495  wf 6496  cfv 6500  (class class class)co 7361  1st c1st 7923  2nd c2nd 7924  supcsup 9384  cc 11057  cr 11058  0cc0 11059  1c1 11060   + caddc 11062  +∞cpnf 11194  *cxr 11196   < clt 11197  cle 11198  cmin 11393   / cdiv 11820  cn 12161  2c2 12216  0cn0 12421  cuz 12771  +crp 12923  (,)cioo 13273  [,)cico 13275  [,]cicc 13276  ...cfz 13433  seqcseq 13915  cexp 13976  abscabs 15128  Σcsu 15579  vol*covol 24849
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 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
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 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-sup 9386  df-inf 9387  df-oi 9454  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-n0 12422  df-z 12508  df-uz 12772  df-rp 12924  df-ioo 13277  df-ico 13279  df-icc 13280  df-fz 13434  df-fzo 13577  df-seq 13916  df-exp 13977  df-hash 14240  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-clim 15379  df-sum 15580  df-ovol 24851
This theorem is referenced by:  ovollb2  24876
  Copyright terms: Public domain W3C validator