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

Theorem ovolscalem1 23327
Description: Lemma for ovolsca 23329. (Contributed by Mario Carneiro, 6-Apr-2015.)
Hypotheses
Ref Expression
ovolsca.1 (𝜑𝐴 ⊆ ℝ)
ovolsca.2 (𝜑𝐶 ∈ ℝ+)
ovolsca.3 (𝜑𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})
ovolsca.4 (𝜑 → (vol*‘𝐴) ∈ ℝ)
ovolsca.5 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
ovolsca.6 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩)
ovolsca.7 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
ovolsca.8 (𝜑𝐴 ran ((,) ∘ 𝐹))
ovolsca.9 (𝜑𝑅 ∈ ℝ+)
ovolsca.10 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))
Assertion
Ref Expression
ovolscalem1 (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
Distinct variable groups:   𝑥,𝑛,𝐴   𝐵,𝑛   𝑛,𝐹,𝑥   𝑛,𝐺   𝑥,𝑅   𝐶,𝑛,𝑥   𝜑,𝑛   𝑥,𝑆
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑅(𝑛)   𝑆(𝑛)   𝐺(𝑥)

Proof of Theorem ovolscalem1
Dummy variables 𝑘 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovolsca.3 . . . 4 (𝜑𝐵 = {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴})
2 ssrab2 3720 . . . 4 {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ⊆ ℝ
31, 2syl6eqss 3688 . . 3 (𝜑𝐵 ⊆ ℝ)
4 ovolcl 23292 . . 3 (𝐵 ⊆ ℝ → (vol*‘𝐵) ∈ ℝ*)
53, 4syl 17 . 2 (𝜑 → (vol*‘𝐵) ∈ ℝ*)
6 ovolsca.7 . . . . . . . . . . . 12 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
7 ovolfcl 23281 . . . . . . . . . . . 12 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
86, 7sylan 487 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
98simp3d 1095 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)))
108simp1d 1093 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
118simp2d 1094 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
12 ovolsca.2 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ ℝ+)
1312rpregt0d 11916 . . . . . . . . . . . 12 (𝜑 → (𝐶 ∈ ℝ ∧ 0 < 𝐶))
1413adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶))
15 lediv1 10926 . . . . . . . . . . 11 (((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)) ↔ ((1st ‘(𝐹𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹𝑛)) / 𝐶)))
1610, 11, 14, 15syl3anc 1366 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)) ↔ ((1st ‘(𝐹𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹𝑛)) / 𝐶)))
179, 16mpbid 222 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹𝑛)) / 𝐶))
18 df-br 4686 . . . . . . . . 9 (((1st ‘(𝐹𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹𝑛)) / 𝐶) ↔ ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ ≤ )
1917, 18sylib 208 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ ≤ )
2012adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝐶 ∈ ℝ+)
2110, 20rerpdivcld 11941 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) / 𝐶) ∈ ℝ)
2211, 20rerpdivcld 11941 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐹𝑛)) / 𝐶) ∈ ℝ)
23 opelxpi 5182 . . . . . . . . 9 ((((1st ‘(𝐹𝑛)) / 𝐶) ∈ ℝ ∧ ((2nd ‘(𝐹𝑛)) / 𝐶) ∈ ℝ) → ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ (ℝ × ℝ))
2421, 22, 23syl2anc 694 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ (ℝ × ℝ))
2519, 24elind 3831 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ ( ≤ ∩ (ℝ × ℝ)))
26 ovolsca.6 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩)
2725, 26fmptd 6425 . . . . . 6 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
28 eqid 2651 . . . . . . 7 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
29 eqid 2651 . . . . . . 7 seq1( + , ((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − ) ∘ 𝐺))
3028, 29ovolsf 23287 . . . . . 6 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞))
3127, 30syl 17 . . . . 5 (𝜑 → seq1( + , ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞))
32 frn 6091 . . . . 5 (seq1( + , ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞) → ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ (0[,)+∞))
3331, 32syl 17 . . . 4 (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ (0[,)+∞))
34 icossxr 12296 . . . 4 (0[,)+∞) ⊆ ℝ*
3533, 34syl6ss 3648 . . 3 (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ*)
36 supxrcl 12183 . . 3 (ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ ℝ*)
3735, 36syl 17 . 2 (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ ℝ*)
38 ovolsca.4 . . . . 5 (𝜑 → (vol*‘𝐴) ∈ ℝ)
3938, 12rerpdivcld 11941 . . . 4 (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℝ)
40 ovolsca.9 . . . . 5 (𝜑𝑅 ∈ ℝ+)
4140rpred 11910 . . . 4 (𝜑𝑅 ∈ ℝ)
4239, 41readdcld 10107 . . 3 (𝜑 → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ)
4342rexrd 10127 . 2 (𝜑 → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ*)
441eleq2d 2716 . . . . . . 7 (𝜑 → (𝑦𝐵𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}))
45 oveq2 6698 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐶 · 𝑥) = (𝐶 · 𝑦))
4645eleq1d 2715 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐶 · 𝑥) ∈ 𝐴 ↔ (𝐶 · 𝑦) ∈ 𝐴))
4746elrab 3396 . . . . . . 7 (𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ↔ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴))
4844, 47syl6bb 276 . . . . . 6 (𝜑 → (𝑦𝐵 ↔ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)))
49 simprr 811 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → (𝐶 · 𝑦) ∈ 𝐴)
50 ovolsca.8 . . . . . . . . . . 11 (𝜑𝐴 ran ((,) ∘ 𝐹))
51 ovolsca.1 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ)
52 ovolfioo 23282 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
5351, 6, 52syl2anc 694 . . . . . . . . . . 11 (𝜑 → (𝐴 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
5450, 53mpbid 222 . . . . . . . . . 10 (𝜑 → ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
5554adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
56 breq2 4689 . . . . . . . . . . . 12 (𝑥 = (𝐶 · 𝑦) → ((1st ‘(𝐹𝑛)) < 𝑥 ↔ (1st ‘(𝐹𝑛)) < (𝐶 · 𝑦)))
57 breq1 4688 . . . . . . . . . . . 12 (𝑥 = (𝐶 · 𝑦) → (𝑥 < (2nd ‘(𝐹𝑛)) ↔ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛))))
5856, 57anbi12d 747 . . . . . . . . . . 11 (𝑥 = (𝐶 · 𝑦) → (((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) ↔ ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)))))
5958rexbidv 3081 . . . . . . . . . 10 (𝑥 = (𝐶 · 𝑦) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)))))
6059rspcv 3336 . . . . . . . . 9 ((𝐶 · 𝑦) ∈ 𝐴 → (∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) → ∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)))))
6149, 55, 60sylc 65 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛))))
62 opex 4962 . . . . . . . . . . . . . . . 16 ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ V
6326fvmpt2 6330 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ ∧ ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ V) → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩)
6462, 63mpan2 707 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩)
6564fveq2d 6233 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = (1st ‘⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩))
66 ovex 6718 . . . . . . . . . . . . . . 15 ((1st ‘(𝐹𝑛)) / 𝐶) ∈ V
67 ovex 6718 . . . . . . . . . . . . . . 15 ((2nd ‘(𝐹𝑛)) / 𝐶) ∈ V
6866, 67op1st 7218 . . . . . . . . . . . . . 14 (1st ‘⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩) = ((1st ‘(𝐹𝑛)) / 𝐶)
6965, 68syl6eq 2701 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) / 𝐶))
7069adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) / 𝐶))
7170breq1d 4695 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛)) < 𝑦 ↔ ((1st ‘(𝐹𝑛)) / 𝐶) < 𝑦))
7210adantlr 751 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
73 simplrl 817 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑦 ∈ ℝ)
7414adantlr 751 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶))
75 ltdivmul 10936 . . . . . . . . . . . 12 (((1st ‘(𝐹𝑛)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (((1st ‘(𝐹𝑛)) / 𝐶) < 𝑦 ↔ (1st ‘(𝐹𝑛)) < (𝐶 · 𝑦)))
7672, 73, 74, 75syl3anc 1366 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹𝑛)) / 𝐶) < 𝑦 ↔ (1st ‘(𝐹𝑛)) < (𝐶 · 𝑦)))
7771, 76bitr2d 269 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ↔ (1st ‘(𝐺𝑛)) < 𝑦))
7811adantlr 751 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
79 ltmuldiv2 10935 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹𝑛)) / 𝐶)))
8073, 78, 74, 79syl3anc 1366 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹𝑛)) / 𝐶)))
8164fveq2d 6233 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩))
8266, 67op2nd 7219 . . . . . . . . . . . . . 14 (2nd ‘⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩) = ((2nd ‘(𝐹𝑛)) / 𝐶)
8381, 82syl6eq 2701 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = ((2nd ‘(𝐹𝑛)) / 𝐶))
8483adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = ((2nd ‘(𝐹𝑛)) / 𝐶))
8584breq2d 4697 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹𝑛)) / 𝐶)))
8680, 85bitr4d 271 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)) ↔ 𝑦 < (2nd ‘(𝐺𝑛))))
8777, 86anbi12d 747 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛))) ↔ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
8887rexbidva 3078 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
8961, 88mpbid 222 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛))))
9089ex 449 . . . . . 6 (𝜑 → ((𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
9148, 90sylbid 230 . . . . 5 (𝜑 → (𝑦𝐵 → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
9291ralrimiv 2994 . . . 4 (𝜑 → ∀𝑦𝐵𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛))))
93 ovolfioo 23282 . . . . 5 ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐵 ran ((,) ∘ 𝐺) ↔ ∀𝑦𝐵𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
943, 27, 93syl2anc 694 . . . 4 (𝜑 → (𝐵 ran ((,) ∘ 𝐺) ↔ ∀𝑦𝐵𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
9592, 94mpbird 247 . . 3 (𝜑𝐵 ran ((,) ∘ 𝐺))
9629ovollb 23293 . . 3 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐵 ran ((,) ∘ 𝐺)) → (vol*‘𝐵) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ))
9727, 95, 96syl2anc 694 . 2 (𝜑 → (vol*‘𝐵) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ))
98 fzfid 12812 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
9912rpcnd 11912 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
10099adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
101 simpl 472 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝜑)
102 elfznn 12408 . . . . . . . . . 10 (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ)
10311, 10resubcld 10496 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ∈ ℝ)
104101, 102, 103syl2an 493 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ∈ ℝ)
105104recnd 10106 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ∈ ℂ)
10612rpne0d 11915 . . . . . . . . 9 (𝜑𝐶 ≠ 0)
107106adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝐶 ≠ 0)
10898, 100, 105, 107fsumdivc 14562 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) = Σ𝑛 ∈ (1...𝑘)(((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶))
10983, 69oveq12d 6708 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))) = (((2nd ‘(𝐹𝑛)) / 𝐶) − ((1st ‘(𝐹𝑛)) / 𝐶)))
110109adantl 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))) = (((2nd ‘(𝐹𝑛)) / 𝐶) − ((1st ‘(𝐹𝑛)) / 𝐶)))
11128ovolfsval 23285 . . . . . . . . . . 11 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))))
11227, 111sylan 487 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))))
11311recnd 10106 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℂ)
11410recnd 10106 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℂ)
11512rpcnne0d 11919 . . . . . . . . . . . 12 (𝜑 → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0))
116115adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0))
117 divsubdir 10759 . . . . . . . . . . 11 (((2nd ‘(𝐹𝑛)) ∈ ℂ ∧ (1st ‘(𝐹𝑛)) ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) = (((2nd ‘(𝐹𝑛)) / 𝐶) − ((1st ‘(𝐹𝑛)) / 𝐶)))
118113, 114, 116, 117syl3anc 1366 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) = (((2nd ‘(𝐹𝑛)) / 𝐶) − ((1st ‘(𝐹𝑛)) / 𝐶)))
119110, 112, 1183eqtr4d 2695 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶))
120101, 102, 119syl2an 493 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶))
121 simpr 476 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
122 nnuz 11761 . . . . . . . . 9 ℕ = (ℤ‘1)
123121, 122syl6eleq 2740 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
124103, 20rerpdivcld 11941 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ∈ ℝ)
125124recnd 10106 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ∈ ℂ)
126101, 102, 125syl2an 493 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ∈ ℂ)
127120, 123, 126fsumser 14505 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)(((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘))
128108, 127eqtrd 2685 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘))
129 ovolsca.10 . . . . . . . . . . 11 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))
130 eqid 2651 . . . . . . . . . . . . . . . 16 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
131 ovolsca.5 . . . . . . . . . . . . . . . 16 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
132130, 131ovolsf 23287 . . . . . . . . . . . . . . 15 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
1336, 132syl 17 . . . . . . . . . . . . . 14 (𝜑𝑆:ℕ⟶(0[,)+∞))
134 frn 6091 . . . . . . . . . . . . . 14 (𝑆:ℕ⟶(0[,)+∞) → ran 𝑆 ⊆ (0[,)+∞))
135133, 134syl 17 . . . . . . . . . . . . 13 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
136135, 34syl6ss 3648 . . . . . . . . . . . 12 (𝜑 → ran 𝑆 ⊆ ℝ*)
13712, 40rpmulcld 11926 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 · 𝑅) ∈ ℝ+)
138137rpred 11910 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · 𝑅) ∈ ℝ)
13938, 138readdcld 10107 . . . . . . . . . . . . 13 (𝜑 → ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ)
140139rexrd 10127 . . . . . . . . . . . 12 (𝜑 → ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ*)
141 supxrleub 12194 . . . . . . . . . . . 12 ((ran 𝑆 ⊆ ℝ* ∧ ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ*) → (sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))))
142136, 140, 141syl2anc 694 . . . . . . . . . . 11 (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))))
143129, 142mpbid 222 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))
144 ffn 6083 . . . . . . . . . . . 12 (𝑆:ℕ⟶(0[,)+∞) → 𝑆 Fn ℕ)
145133, 144syl 17 . . . . . . . . . . 11 (𝜑𝑆 Fn ℕ)
146 breq1 4688 . . . . . . . . . . . 12 (𝑥 = (𝑆𝑘) → (𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ (𝑆𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))))
147146ralrn 6402 . . . . . . . . . . 11 (𝑆 Fn ℕ → (∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))))
148145, 147syl 17 . . . . . . . . . 10 (𝜑 → (∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))))
149143, 148mpbid 222 . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))
150149r19.21bi 2961 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))
1516adantr 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
152130ovolfsval 23285 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))))
153151, 102, 152syl2an 493 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))))
154153, 123, 105fsumser 14505 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘))
155131fveq1i 6230 . . . . . . . . 9 (𝑆𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
156154, 155syl6eqr 2703 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) = (𝑆𝑘))
15739recnd 10106 . . . . . . . . . . 11 (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℂ)
15840rpcnd 11912 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℂ)
15999, 157, 158adddid 10102 . . . . . . . . . 10 (𝜑 → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((𝐶 · ((vol*‘𝐴) / 𝐶)) + (𝐶 · 𝑅)))
16038recnd 10106 . . . . . . . . . . . 12 (𝜑 → (vol*‘𝐴) ∈ ℂ)
161160, 99, 106divcan2d 10841 . . . . . . . . . . 11 (𝜑 → (𝐶 · ((vol*‘𝐴) / 𝐶)) = (vol*‘𝐴))
162161oveq1d 6705 . . . . . . . . . 10 (𝜑 → ((𝐶 · ((vol*‘𝐴) / 𝐶)) + (𝐶 · 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅)))
163159, 162eqtrd 2685 . . . . . . . . 9 (𝜑 → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅)))
164163adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅)))
165150, 156, 1643brtr4d 4717 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)))
16698, 104fsumrecl 14509 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ∈ ℝ)
16742adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ)
16813adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶))
169 ledivmul 10937 . . . . . . . 8 ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ∈ ℝ ∧ (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅))))
170166, 167, 168, 169syl3anc 1366 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅))))
171165, 170mpbird 247 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
172128, 171eqbrtrrd 4709 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
173172ralrimiva 2995 . . . 4 (𝜑 → ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
174 ffn 6083 . . . . . 6 (seq1( + , ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞) → seq1( + , ((abs ∘ − ) ∘ 𝐺)) Fn ℕ)
17531, 174syl 17 . . . . 5 (𝜑 → seq1( + , ((abs ∘ − ) ∘ 𝐺)) Fn ℕ)
176 breq1 4688 . . . . . 6 (𝑦 = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) → (𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)))
177176ralrn 6402 . . . . 5 (seq1( + , ((abs ∘ − ) ∘ 𝐺)) Fn ℕ → (∀𝑦 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)))
178175, 177syl 17 . . . 4 (𝜑 → (∀𝑦 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)))
179173, 178mpbird 247 . . 3 (𝜑 → ∀𝑦 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
180 supxrleub 12194 . . . 4 ((ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* ∧ (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ*) → (sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑦 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)))
18135, 43, 180syl2anc 694 . . 3 (𝜑 → (sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑦 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)))
182179, 181mpbird 247 . 2 (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
1835, 37, 43, 97, 182xrletrd 12031 1 (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  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   · cmul 9979  +∞cpnf 10109  *cxr 10111   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  cn 11058  cuz 11725  +crp 11870  (,)cioo 12213  [,)cico 12215  ...cfz 12364  seqcseq 12841  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-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:  ovolscalem2  23328
  Copyright terms: Public domain W3C validator