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

Theorem ovolscalem1 25416
Description: Lemma for ovolsca 25418. (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 4073 . . . 4 {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ⊆ ℝ
31, 2eqsstrdi 4032 . . 3 (𝜑𝐵 ⊆ ℝ)
4 ovolcl 25381 . . 3 (𝐵 ⊆ ℝ → (vol*‘𝐵) ∈ ℝ*)
53, 4syl 17 . 2 (𝜑 → (vol*‘𝐵) ∈ ℝ*)
6 ovolsca.7 . . . . . . . . . . . 12 (𝜑𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
7 ovolfcl 25369 . . . . . . . . . . . 12 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
86, 7sylan 579 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛))))
98simp3d 1142 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)))
108simp1d 1140 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
118simp2d 1141 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
12 ovolsca.2 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ ℝ+)
1312rpregt0d 13040 . . . . . . . . . . . 12 (𝜑 → (𝐶 ∈ ℝ ∧ 0 < 𝐶))
1413adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶))
15 lediv1 12095 . . . . . . . . . . 11 (((1st ‘(𝐹𝑛)) ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)) ↔ ((1st ‘(𝐹𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹𝑛)) / 𝐶)))
1610, 11, 14, 15syl3anc 1369 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) ≤ (2nd ‘(𝐹𝑛)) ↔ ((1st ‘(𝐹𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹𝑛)) / 𝐶)))
179, 16mpbid 231 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹𝑛)) / 𝐶))
18 df-br 5143 . . . . . . . . 9 (((1st ‘(𝐹𝑛)) / 𝐶) ≤ ((2nd ‘(𝐹𝑛)) / 𝐶) ↔ ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ ≤ )
1917, 18sylib 217 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ ≤ )
2012adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝐶 ∈ ℝ+)
2110, 20rerpdivcld 13065 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) / 𝐶) ∈ ℝ)
2211, 20rerpdivcld 13065 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐹𝑛)) / 𝐶) ∈ ℝ)
2321, 22opelxpd 5711 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ (ℝ × ℝ))
2419, 23elind 4190 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ ( ≤ ∩ (ℝ × ℝ)))
25 ovolsca.6 . . . . . . 7 𝐺 = (𝑛 ∈ ℕ ↦ ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩)
2624, 25fmptd 7118 . . . . . 6 (𝜑𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
27 eqid 2727 . . . . . . 7 ((abs ∘ − ) ∘ 𝐺) = ((abs ∘ − ) ∘ 𝐺)
28 eqid 2727 . . . . . . 7 seq1( + , ((abs ∘ − ) ∘ 𝐺)) = seq1( + , ((abs ∘ − ) ∘ 𝐺))
2927, 28ovolsf 25375 . . . . . 6 (𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞))
3026, 29syl 17 . . . . 5 (𝜑 → seq1( + , ((abs ∘ − ) ∘ 𝐺)):ℕ⟶(0[,)+∞))
3130frnd 6724 . . . 4 (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ (0[,)+∞))
32 icossxr 13427 . . . 4 (0[,)+∞) ⊆ ℝ*
3331, 32sstrdi 3990 . . 3 (𝜑 → ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ*)
34 supxrcl 13312 . . 3 (ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ ℝ*)
3533, 34syl 17 . 2 (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ∈ ℝ*)
36 ovolsca.4 . . . . 5 (𝜑 → (vol*‘𝐴) ∈ ℝ)
3736, 12rerpdivcld 13065 . . . 4 (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℝ)
38 ovolsca.9 . . . . 5 (𝜑𝑅 ∈ ℝ+)
3938rpred 13034 . . . 4 (𝜑𝑅 ∈ ℝ)
4037, 39readdcld 11259 . . 3 (𝜑 → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ)
4140rexrd 11280 . 2 (𝜑 → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ*)
421eleq2d 2814 . . . . . . 7 (𝜑 → (𝑦𝐵𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴}))
43 oveq2 7422 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐶 · 𝑥) = (𝐶 · 𝑦))
4443eleq1d 2813 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐶 · 𝑥) ∈ 𝐴 ↔ (𝐶 · 𝑦) ∈ 𝐴))
4544elrab 3680 . . . . . . 7 (𝑦 ∈ {𝑥 ∈ ℝ ∣ (𝐶 · 𝑥) ∈ 𝐴} ↔ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴))
4642, 45bitrdi 287 . . . . . 6 (𝜑 → (𝑦𝐵 ↔ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)))
47 breq2 5146 . . . . . . . . . . 11 (𝑥 = (𝐶 · 𝑦) → ((1st ‘(𝐹𝑛)) < 𝑥 ↔ (1st ‘(𝐹𝑛)) < (𝐶 · 𝑦)))
48 breq1 5145 . . . . . . . . . . 11 (𝑥 = (𝐶 · 𝑦) → (𝑥 < (2nd ‘(𝐹𝑛)) ↔ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛))))
4947, 48anbi12d 630 . . . . . . . . . 10 (𝑥 = (𝐶 · 𝑦) → (((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) ↔ ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)))))
5049rexbidv 3173 . . . . . . . . 9 (𝑥 = (𝐶 · 𝑦) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)))))
51 ovolsca.8 . . . . . . . . . . 11 (𝜑𝐴 ran ((,) ∘ 𝐹))
52 ovolsca.1 . . . . . . . . . . . 12 (𝜑𝐴 ⊆ ℝ)
53 ovolfioo 25370 . . . . . . . . . . . 12 ((𝐴 ⊆ ℝ ∧ 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐴 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
5452, 6, 53syl2anc 583 . . . . . . . . . . 11 (𝜑 → (𝐴 ran ((,) ∘ 𝐹) ↔ ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛)))))
5551, 54mpbid 231 . . . . . . . . . 10 (𝜑 → ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
5655adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∀𝑥𝐴𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < 𝑥𝑥 < (2nd ‘(𝐹𝑛))))
57 simprr 772 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → (𝐶 · 𝑦) ∈ 𝐴)
5850, 56, 57rspcdva 3608 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛))))
59 opex 5460 . . . . . . . . . . . . . . . 16 ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ V
6025fvmpt2 7010 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℕ ∧ ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩ ∈ V) → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩)
6159, 60mpan2 690 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → (𝐺𝑛) = ⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩)
6261fveq2d 6895 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = (1st ‘⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩))
63 ovex 7447 . . . . . . . . . . . . . . 15 ((1st ‘(𝐹𝑛)) / 𝐶) ∈ V
64 ovex 7447 . . . . . . . . . . . . . . 15 ((2nd ‘(𝐹𝑛)) / 𝐶) ∈ V
6563, 64op1st 7993 . . . . . . . . . . . . . 14 (1st ‘⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩) = ((1st ‘(𝐹𝑛)) / 𝐶)
6662, 65eqtrdi 2783 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) / 𝐶))
6766adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐺𝑛)) = ((1st ‘(𝐹𝑛)) / 𝐶))
6867breq1d 5152 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐺𝑛)) < 𝑦 ↔ ((1st ‘(𝐹𝑛)) / 𝐶) < 𝑦))
6910adantlr 714 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℝ)
70 simplrl 776 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → 𝑦 ∈ ℝ)
7114adantlr 714 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶))
72 ltdivmul 12105 . . . . . . . . . . . 12 (((1st ‘(𝐹𝑛)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → (((1st ‘(𝐹𝑛)) / 𝐶) < 𝑦 ↔ (1st ‘(𝐹𝑛)) < (𝐶 · 𝑦)))
7369, 70, 71, 72syl3anc 1369 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹𝑛)) / 𝐶) < 𝑦 ↔ (1st ‘(𝐹𝑛)) < (𝐶 · 𝑦)))
7468, 73bitr2d 280 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ↔ (1st ‘(𝐺𝑛)) < 𝑦))
7511adantlr 714 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℝ)
76 ltmuldiv2 12104 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ (2nd ‘(𝐹𝑛)) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹𝑛)) / 𝐶)))
7770, 75, 71, 76syl3anc 1369 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹𝑛)) / 𝐶)))
7861fveq2d 6895 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = (2nd ‘⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩))
7963, 64op2nd 7994 . . . . . . . . . . . . . 14 (2nd ‘⟨((1st ‘(𝐹𝑛)) / 𝐶), ((2nd ‘(𝐹𝑛)) / 𝐶)⟩) = ((2nd ‘(𝐹𝑛)) / 𝐶)
8078, 79eqtrdi 2783 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (2nd ‘(𝐺𝑛)) = ((2nd ‘(𝐹𝑛)) / 𝐶))
8180adantl 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐺𝑛)) = ((2nd ‘(𝐹𝑛)) / 𝐶))
8281breq2d 5154 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (𝑦 < (2nd ‘(𝐺𝑛)) ↔ 𝑦 < ((2nd ‘(𝐹𝑛)) / 𝐶)))
8377, 82bitr4d 282 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → ((𝐶 · 𝑦) < (2nd ‘(𝐹𝑛)) ↔ 𝑦 < (2nd ‘(𝐺𝑛))))
8474, 83anbi12d 630 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) ∧ 𝑛 ∈ ℕ) → (((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛))) ↔ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
8584rexbidva 3171 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → (∃𝑛 ∈ ℕ ((1st ‘(𝐹𝑛)) < (𝐶 · 𝑦) ∧ (𝐶 · 𝑦) < (2nd ‘(𝐹𝑛))) ↔ ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
8658, 85mpbid 231 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴)) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛))))
8786ex 412 . . . . . 6 (𝜑 → ((𝑦 ∈ ℝ ∧ (𝐶 · 𝑦) ∈ 𝐴) → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
8846, 87sylbid 239 . . . . 5 (𝜑 → (𝑦𝐵 → ∃𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
8988ralrimiv 3140 . . . 4 (𝜑 → ∀𝑦𝐵𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛))))
90 ovolfioo 25370 . . . . 5 ((𝐵 ⊆ ℝ ∧ 𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ))) → (𝐵 ran ((,) ∘ 𝐺) ↔ ∀𝑦𝐵𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
913, 26, 90syl2anc 583 . . . 4 (𝜑 → (𝐵 ran ((,) ∘ 𝐺) ↔ ∀𝑦𝐵𝑛 ∈ ℕ ((1st ‘(𝐺𝑛)) < 𝑦𝑦 < (2nd ‘(𝐺𝑛)))))
9289, 91mpbird 257 . . 3 (𝜑𝐵 ran ((,) ∘ 𝐺))
9328ovollb 25382 . . 3 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐵 ran ((,) ∘ 𝐺)) → (vol*‘𝐵) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ))
9426, 92, 93syl2anc 583 . 2 (𝜑 → (vol*‘𝐵) ≤ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ))
95 fzfid 13956 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (1...𝑘) ∈ Fin)
9612rpcnd 13036 . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
9796adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝐶 ∈ ℂ)
98 simpl 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → 𝜑)
99 elfznn 13548 . . . . . . . . . 10 (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ)
10011, 10resubcld 11658 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ∈ ℝ)
10198, 99, 100syl2an 595 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ∈ ℝ)
102101recnd 11258 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ∈ ℂ)
10312rpne0d 13039 . . . . . . . . 9 (𝜑𝐶 ≠ 0)
104103adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝐶 ≠ 0)
10595, 97, 102, 104fsumdivc 15750 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) = Σ𝑛 ∈ (1...𝑘)(((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶))
10680, 66oveq12d 7432 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))) = (((2nd ‘(𝐹𝑛)) / 𝐶) − ((1st ‘(𝐹𝑛)) / 𝐶)))
107106adantl 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))) = (((2nd ‘(𝐹𝑛)) / 𝐶) − ((1st ‘(𝐹𝑛)) / 𝐶)))
10827ovolfsval 25373 . . . . . . . . . . 11 ((𝐺:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))))
10926, 108sylan 579 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = ((2nd ‘(𝐺𝑛)) − (1st ‘(𝐺𝑛))))
11011recnd 11258 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (2nd ‘(𝐹𝑛)) ∈ ℂ)
11110recnd 11258 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (1st ‘(𝐹𝑛)) ∈ ℂ)
11212rpcnne0d 13043 . . . . . . . . . . . 12 (𝜑 → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0))
113112adantr 480 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0))
114 divsubdir 11924 . . . . . . . . . . 11 (((2nd ‘(𝐹𝑛)) ∈ ℂ ∧ (1st ‘(𝐹𝑛)) ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) = (((2nd ‘(𝐹𝑛)) / 𝐶) − ((1st ‘(𝐹𝑛)) / 𝐶)))
115110, 111, 113, 114syl3anc 1369 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) = (((2nd ‘(𝐹𝑛)) / 𝐶) − ((1st ‘(𝐹𝑛)) / 𝐶)))
116107, 109, 1153eqtr4d 2777 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶))
11798, 99, 116syl2an 595 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐺)‘𝑛) = (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶))
118 simpr 484 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
119 nnuz 12881 . . . . . . . . 9 ℕ = (ℤ‘1)
120118, 119eleqtrdi 2838 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
121100, 20rerpdivcld 13065 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ∈ ℝ)
122121recnd 11258 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ∈ ℂ)
12398, 99, 122syl2an 595 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ∈ ℂ)
124117, 120, 123fsumser 15694 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)(((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘))
125105, 124eqtrd 2767 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘))
126 ovolsca.10 . . . . . . . . . . 11 (𝜑 → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))
127 eqid 2727 . . . . . . . . . . . . . . . 16 ((abs ∘ − ) ∘ 𝐹) = ((abs ∘ − ) ∘ 𝐹)
128 ovolsca.5 . . . . . . . . . . . . . . . 16 𝑆 = seq1( + , ((abs ∘ − ) ∘ 𝐹))
129127, 128ovolsf 25375 . . . . . . . . . . . . . . 15 (𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
1306, 129syl 17 . . . . . . . . . . . . . 14 (𝜑𝑆:ℕ⟶(0[,)+∞))
131130frnd 6724 . . . . . . . . . . . . 13 (𝜑 → ran 𝑆 ⊆ (0[,)+∞))
132131, 32sstrdi 3990 . . . . . . . . . . . 12 (𝜑 → ran 𝑆 ⊆ ℝ*)
13312, 38rpmulcld 13050 . . . . . . . . . . . . . . 15 (𝜑 → (𝐶 · 𝑅) ∈ ℝ+)
134133rpred 13034 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · 𝑅) ∈ ℝ)
13536, 134readdcld 11259 . . . . . . . . . . . . 13 (𝜑 → ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ)
136135rexrd 11280 . . . . . . . . . . . 12 (𝜑 → ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ*)
137 supxrleub 13323 . . . . . . . . . . . 12 ((ran 𝑆 ⊆ ℝ* ∧ ((vol*‘𝐴) + (𝐶 · 𝑅)) ∈ ℝ*) → (sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))))
138132, 136, 137syl2anc 583 . . . . . . . . . . 11 (𝜑 → (sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))))
139126, 138mpbid 231 . . . . . . . . . 10 (𝜑 → ∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))
140130ffnd 6717 . . . . . . . . . . 11 (𝜑𝑆 Fn ℕ)
141 breq1 5145 . . . . . . . . . . . 12 (𝑥 = (𝑆𝑘) → (𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ (𝑆𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))))
142141ralrn 7092 . . . . . . . . . . 11 (𝑆 Fn ℕ → (∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))))
143140, 142syl 17 . . . . . . . . . 10 (𝜑 → (∀𝑥 ∈ ran 𝑆 𝑥 ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)) ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅))))
144139, 143mpbid 231 . . . . . . . . 9 (𝜑 → ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))
145144r19.21bi 3243 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝑆𝑘) ≤ ((vol*‘𝐴) + (𝐶 · 𝑅)))
1466adantr 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
147127ovolfsval 25373 . . . . . . . . . . 11 ((𝐹:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑛 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))))
148146, 99, 147syl2an 595 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (((abs ∘ − ) ∘ 𝐹)‘𝑛) = ((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))))
149148, 120, 102fsumser 15694 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘))
150128fveq1i 6892 . . . . . . . . 9 (𝑆𝑘) = (seq1( + , ((abs ∘ − ) ∘ 𝐹))‘𝑘)
151149, 150eqtr4di 2785 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) = (𝑆𝑘))
15237recnd 11258 . . . . . . . . . . 11 (𝜑 → ((vol*‘𝐴) / 𝐶) ∈ ℂ)
15338rpcnd 13036 . . . . . . . . . . 11 (𝜑𝑅 ∈ ℂ)
15496, 152, 153adddid 11254 . . . . . . . . . 10 (𝜑 → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((𝐶 · ((vol*‘𝐴) / 𝐶)) + (𝐶 · 𝑅)))
15536recnd 11258 . . . . . . . . . . . 12 (𝜑 → (vol*‘𝐴) ∈ ℂ)
156155, 96, 103divcan2d 12008 . . . . . . . . . . 11 (𝜑 → (𝐶 · ((vol*‘𝐴) / 𝐶)) = (vol*‘𝐴))
157156oveq1d 7429 . . . . . . . . . 10 (𝜑 → ((𝐶 · ((vol*‘𝐴) / 𝐶)) + (𝐶 · 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅)))
158154, 157eqtrd 2767 . . . . . . . . 9 (𝜑 → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅)))
159158adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)) = ((vol*‘𝐴) + (𝐶 · 𝑅)))
160145, 151, 1593brtr4d 5174 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅)))
16195, 101fsumrecl 15698 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ∈ ℝ)
16240adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ)
16313adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐶 ∈ ℝ ∧ 0 < 𝐶))
164 ledivmul 12106 . . . . . . . 8 ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ∈ ℝ ∧ (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ ∧ (𝐶 ∈ ℝ ∧ 0 < 𝐶)) → ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅))))
165161, 162, 163, 164syl3anc 1369 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ((Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) ≤ (𝐶 · (((vol*‘𝐴) / 𝐶) + 𝑅))))
166160, 165mpbird 257 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → (Σ𝑛 ∈ (1...𝑘)((2nd ‘(𝐹𝑛)) − (1st ‘(𝐹𝑛))) / 𝐶) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
167125, 166eqbrtrrd 5166 . . . . 5 ((𝜑𝑘 ∈ ℕ) → (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
168167ralrimiva 3141 . . . 4 (𝜑 → ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
16930ffnd 6717 . . . . 5 (𝜑 → seq1( + , ((abs ∘ − ) ∘ 𝐺)) Fn ℕ)
170 breq1 5145 . . . . . 6 (𝑦 = (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) → (𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)))
171170ralrn 7092 . . . . 5 (seq1( + , ((abs ∘ − ) ∘ 𝐺)) Fn ℕ → (∀𝑦 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)))
172169, 171syl 17 . . . 4 (𝜑 → (∀𝑦 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑘 ∈ ℕ (seq1( + , ((abs ∘ − ) ∘ 𝐺))‘𝑘) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)))
173168, 172mpbird 257 . . 3 (𝜑 → ∀𝑦 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
174 supxrleub 13323 . . . 4 ((ran seq1( + , ((abs ∘ − ) ∘ 𝐺)) ⊆ ℝ* ∧ (((vol*‘𝐴) / 𝐶) + 𝑅) ∈ ℝ*) → (sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑦 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)))
17533, 41, 174syl2anc 583 . . 3 (𝜑 → (sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅) ↔ ∀𝑦 ∈ ran seq1( + , ((abs ∘ − ) ∘ 𝐺))𝑦 ≤ (((vol*‘𝐴) / 𝐶) + 𝑅)))
176173, 175mpbird 257 . 2 (𝜑 → sup(ran seq1( + , ((abs ∘ − ) ∘ 𝐺)), ℝ*, < ) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
1775, 35, 41, 94, 176xrletrd 13159 1 (𝜑 → (vol*‘𝐵) ≤ (((vol*‘𝐴) / 𝐶) + 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1085   = wceq 1534  wcel 2099  wne 2935  wral 3056  wrex 3065  {crab 3427  Vcvv 3469  cin 3943  wss 3944  cop 4630   cuni 4903   class class class wbr 5142  cmpt 5225   × cxp 5670  ran crn 5673  ccom 5676   Fn wfn 6537  wf 6538  cfv 6542  (class class class)co 7414  1st c1st 7983  2nd c2nd 7984  supcsup 9449  cc 11122  cr 11123  0cc0 11124  1c1 11125   + caddc 11127   · cmul 11129  +∞cpnf 11261  *cxr 11263   < clt 11264  cle 11265  cmin 11460   / cdiv 11887  cn 12228  cuz 12838  +crp 12992  (,)cioo 13342  [,)cico 13344  ...cfz 13502  seqcseq 13984  abscabs 15199  Σcsu 15650  vol*covol 25365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-inf2 9650  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201  ax-pre-sup 11202
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7863  df-1st 7985  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-er 8716  df-map 8836  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-sup 9451  df-inf 9452  df-oi 9519  df-card 9948  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-sub 11462  df-neg 11463  df-div 11888  df-nn 12229  df-2 12291  df-3 12292  df-n0 12489  df-z 12575  df-uz 12839  df-rp 12993  df-ioo 13346  df-ico 13348  df-fz 13503  df-fzo 13646  df-seq 13985  df-exp 14045  df-hash 14308  df-cj 15064  df-re 15065  df-im 15066  df-sqrt 15200  df-abs 15201  df-clim 15450  df-sum 15651  df-ovol 25367
This theorem is referenced by:  ovolscalem2  25417
  Copyright terms: Public domain W3C validator