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

Theorem volcn 25579
Description: The function formed by restricting a measurable set to a closed interval with a varying endpoint produces an increasing continuous function on the reals. (Contributed by Mario Carneiro, 30-Aug-2014.)
Hypothesis
Ref Expression
volcn.1 𝐹 = (𝑥 ∈ ℝ ↦ (vol‘(𝐴 ∩ (𝐵[,]𝑥))))
Assertion
Ref Expression
volcn ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → 𝐹 ∈ (ℝ–cn→ℝ))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝐹(𝑥)

Proof of Theorem volcn
Dummy variables 𝑢 𝑒 𝑣 𝑦 𝑧 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 765 . . . . . 6 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ dom vol)
2 iccmbl 25539 . . . . . . 7 ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐵[,]𝑥) ∈ dom vol)
32adantll 712 . . . . . 6 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐵[,]𝑥) ∈ dom vol)
4 inmbl 25515 . . . . . 6 ((𝐴 ∈ dom vol ∧ (𝐵[,]𝑥) ∈ dom vol) → (𝐴 ∩ (𝐵[,]𝑥)) ∈ dom vol)
51, 3, 4syl2anc 582 . . . . 5 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐴 ∩ (𝐵[,]𝑥)) ∈ dom vol)
6 mblvol 25503 . . . . 5 ((𝐴 ∩ (𝐵[,]𝑥)) ∈ dom vol → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑥))))
75, 6syl 17 . . . 4 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑥))))
8 inss2 4228 . . . . 5 (𝐴 ∩ (𝐵[,]𝑥)) ⊆ (𝐵[,]𝑥)
9 mblss 25504 . . . . . 6 ((𝐵[,]𝑥) ∈ dom vol → (𝐵[,]𝑥) ⊆ ℝ)
103, 9syl 17 . . . . 5 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐵[,]𝑥) ⊆ ℝ)
11 mblvol 25503 . . . . . . 7 ((𝐵[,]𝑥) ∈ dom vol → (vol‘(𝐵[,]𝑥)) = (vol*‘(𝐵[,]𝑥)))
123, 11syl 17 . . . . . 6 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (vol‘(𝐵[,]𝑥)) = (vol*‘(𝐵[,]𝑥)))
13 iccvolcl 25540 . . . . . . 7 ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (vol‘(𝐵[,]𝑥)) ∈ ℝ)
1413adantll 712 . . . . . 6 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (vol‘(𝐵[,]𝑥)) ∈ ℝ)
1512, 14eqeltrrd 2826 . . . . 5 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (vol*‘(𝐵[,]𝑥)) ∈ ℝ)
16 ovolsscl 25459 . . . . 5 (((𝐴 ∩ (𝐵[,]𝑥)) ⊆ (𝐵[,]𝑥) ∧ (𝐵[,]𝑥) ⊆ ℝ ∧ (vol*‘(𝐵[,]𝑥)) ∈ ℝ) → (vol*‘(𝐴 ∩ (𝐵[,]𝑥))) ∈ ℝ)
178, 10, 15, 16mp3an2i 1462 . . . 4 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (vol*‘(𝐴 ∩ (𝐵[,]𝑥))) ∈ ℝ)
187, 17eqeltrd 2825 . . 3 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) ∈ ℝ)
19 volcn.1 . . 3 𝐹 = (𝑥 ∈ ℝ ↦ (vol‘(𝐴 ∩ (𝐵[,]𝑥))))
2018, 19fmptd 7123 . 2 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → 𝐹:ℝ⟶ℝ)
21 simprr 771 . . . 4 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+)) → 𝑒 ∈ ℝ+)
22 oveq12 7428 . . . . . . . . . . . . 13 ((𝑣 = 𝑧𝑢 = 𝑦) → (𝑣𝑢) = (𝑧𝑦))
2322ancoms 457 . . . . . . . . . . . 12 ((𝑢 = 𝑦𝑣 = 𝑧) → (𝑣𝑢) = (𝑧𝑦))
2423fveq2d 6900 . . . . . . . . . . 11 ((𝑢 = 𝑦𝑣 = 𝑧) → (abs‘(𝑣𝑢)) = (abs‘(𝑧𝑦)))
2524breq1d 5159 . . . . . . . . . 10 ((𝑢 = 𝑦𝑣 = 𝑧) → ((abs‘(𝑣𝑢)) < 𝑒 ↔ (abs‘(𝑧𝑦)) < 𝑒))
26 fveq2 6896 . . . . . . . . . . . . 13 (𝑣 = 𝑧 → (𝐹𝑣) = (𝐹𝑧))
27 fveq2 6896 . . . . . . . . . . . . 13 (𝑢 = 𝑦 → (𝐹𝑢) = (𝐹𝑦))
2826, 27oveqan12rd 7439 . . . . . . . . . . . 12 ((𝑢 = 𝑦𝑣 = 𝑧) → ((𝐹𝑣) − (𝐹𝑢)) = ((𝐹𝑧) − (𝐹𝑦)))
2928fveq2d 6900 . . . . . . . . . . 11 ((𝑢 = 𝑦𝑣 = 𝑧) → (abs‘((𝐹𝑣) − (𝐹𝑢))) = (abs‘((𝐹𝑧) − (𝐹𝑦))))
3029breq1d 5159 . . . . . . . . . 10 ((𝑢 = 𝑦𝑣 = 𝑧) → ((abs‘((𝐹𝑣) − (𝐹𝑢))) < 𝑒 ↔ (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))
3125, 30imbi12d 343 . . . . . . . . 9 ((𝑢 = 𝑦𝑣 = 𝑧) → (((abs‘(𝑣𝑢)) < 𝑒 → (abs‘((𝐹𝑣) − (𝐹𝑢))) < 𝑒) ↔ ((abs‘(𝑧𝑦)) < 𝑒 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒)))
32 oveq12 7428 . . . . . . . . . . . . 13 ((𝑣 = 𝑦𝑢 = 𝑧) → (𝑣𝑢) = (𝑦𝑧))
3332ancoms 457 . . . . . . . . . . . 12 ((𝑢 = 𝑧𝑣 = 𝑦) → (𝑣𝑢) = (𝑦𝑧))
3433fveq2d 6900 . . . . . . . . . . 11 ((𝑢 = 𝑧𝑣 = 𝑦) → (abs‘(𝑣𝑢)) = (abs‘(𝑦𝑧)))
3534breq1d 5159 . . . . . . . . . 10 ((𝑢 = 𝑧𝑣 = 𝑦) → ((abs‘(𝑣𝑢)) < 𝑒 ↔ (abs‘(𝑦𝑧)) < 𝑒))
36 fveq2 6896 . . . . . . . . . . . . 13 (𝑣 = 𝑦 → (𝐹𝑣) = (𝐹𝑦))
37 fveq2 6896 . . . . . . . . . . . . 13 (𝑢 = 𝑧 → (𝐹𝑢) = (𝐹𝑧))
3836, 37oveqan12rd 7439 . . . . . . . . . . . 12 ((𝑢 = 𝑧𝑣 = 𝑦) → ((𝐹𝑣) − (𝐹𝑢)) = ((𝐹𝑦) − (𝐹𝑧)))
3938fveq2d 6900 . . . . . . . . . . 11 ((𝑢 = 𝑧𝑣 = 𝑦) → (abs‘((𝐹𝑣) − (𝐹𝑢))) = (abs‘((𝐹𝑦) − (𝐹𝑧))))
4039breq1d 5159 . . . . . . . . . 10 ((𝑢 = 𝑧𝑣 = 𝑦) → ((abs‘((𝐹𝑣) − (𝐹𝑢))) < 𝑒 ↔ (abs‘((𝐹𝑦) − (𝐹𝑧))) < 𝑒))
4135, 40imbi12d 343 . . . . . . . . 9 ((𝑢 = 𝑧𝑣 = 𝑦) → (((abs‘(𝑣𝑢)) < 𝑒 → (abs‘((𝐹𝑣) − (𝐹𝑢))) < 𝑒) ↔ ((abs‘(𝑦𝑧)) < 𝑒 → (abs‘((𝐹𝑦) − (𝐹𝑧))) < 𝑒)))
42 ssidd 4000 . . . . . . . . 9 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) → ℝ ⊆ ℝ)
43 recn 11230 . . . . . . . . . . . . 13 (𝑧 ∈ ℝ → 𝑧 ∈ ℂ)
44 recn 11230 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
45 abssub 15309 . . . . . . . . . . . . 13 ((𝑧 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (abs‘(𝑧𝑦)) = (abs‘(𝑦𝑧)))
4643, 44, 45syl2anr 595 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (abs‘(𝑧𝑦)) = (abs‘(𝑦𝑧)))
4746adantl 480 . . . . . . . . . . 11 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (abs‘(𝑧𝑦)) = (abs‘(𝑦𝑧)))
4847breq1d 5159 . . . . . . . . . 10 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((abs‘(𝑧𝑦)) < 𝑒 ↔ (abs‘(𝑦𝑧)) < 𝑒))
4920adantr 479 . . . . . . . . . . . . 13 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) → 𝐹:ℝ⟶ℝ)
50 ffvelcdm 7090 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶ℝ ∧ 𝑦 ∈ ℝ) → (𝐹𝑦) ∈ ℝ)
51 ffvelcdm 7090 . . . . . . . . . . . . . 14 ((𝐹:ℝ⟶ℝ ∧ 𝑧 ∈ ℝ) → (𝐹𝑧) ∈ ℝ)
5250, 51anim12dan 617 . . . . . . . . . . . . 13 ((𝐹:ℝ⟶ℝ ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((𝐹𝑦) ∈ ℝ ∧ (𝐹𝑧) ∈ ℝ))
5349, 52sylan 578 . . . . . . . . . . . 12 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((𝐹𝑦) ∈ ℝ ∧ (𝐹𝑧) ∈ ℝ))
54 recn 11230 . . . . . . . . . . . . 13 ((𝐹𝑧) ∈ ℝ → (𝐹𝑧) ∈ ℂ)
55 recn 11230 . . . . . . . . . . . . 13 ((𝐹𝑦) ∈ ℝ → (𝐹𝑦) ∈ ℂ)
56 abssub 15309 . . . . . . . . . . . . 13 (((𝐹𝑧) ∈ ℂ ∧ (𝐹𝑦) ∈ ℂ) → (abs‘((𝐹𝑧) − (𝐹𝑦))) = (abs‘((𝐹𝑦) − (𝐹𝑧))))
5754, 55, 56syl2anr 595 . . . . . . . . . . . 12 (((𝐹𝑦) ∈ ℝ ∧ (𝐹𝑧) ∈ ℝ) → (abs‘((𝐹𝑧) − (𝐹𝑦))) = (abs‘((𝐹𝑦) − (𝐹𝑧))))
5853, 57syl 17 . . . . . . . . . . 11 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (abs‘((𝐹𝑧) − (𝐹𝑦))) = (abs‘((𝐹𝑦) − (𝐹𝑧))))
5958breq1d 5159 . . . . . . . . . 10 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒 ↔ (abs‘((𝐹𝑦) − (𝐹𝑧))) < 𝑒))
6048, 59imbi12d 343 . . . . . . . . 9 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → (((abs‘(𝑧𝑦)) < 𝑒 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒) ↔ ((abs‘(𝑦𝑧)) < 𝑒 → (abs‘((𝐹𝑦) − (𝐹𝑧))) < 𝑒)))
61 simpr2 1192 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → 𝑧 ∈ ℝ)
62 oveq2 7427 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (𝐵[,]𝑥) = (𝐵[,]𝑧))
6362ineq2d 4210 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → (𝐴 ∩ (𝐵[,]𝑥)) = (𝐴 ∩ (𝐵[,]𝑧)))
6463fveq2d 6900 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol‘(𝐴 ∩ (𝐵[,]𝑧))))
65 fvex 6909 . . . . . . . . . . . . . . . 16 (vol‘(𝐴 ∩ (𝐵[,]𝑧))) ∈ V
6664, 19, 65fvmpt 7004 . . . . . . . . . . . . . . 15 (𝑧 ∈ ℝ → (𝐹𝑧) = (vol‘(𝐴 ∩ (𝐵[,]𝑧))))
6761, 66syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐹𝑧) = (vol‘(𝐴 ∩ (𝐵[,]𝑧))))
68 simplll 773 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → 𝐴 ∈ dom vol)
69 simplr 767 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) → 𝐵 ∈ ℝ)
7069adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → 𝐵 ∈ ℝ)
71 iccmbl 25539 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝐵[,]𝑧) ∈ dom vol)
7270, 61, 71syl2anc 582 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐵[,]𝑧) ∈ dom vol)
73 inmbl 25515 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ dom vol ∧ (𝐵[,]𝑧) ∈ dom vol) → (𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol)
7468, 72, 73syl2anc 582 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol)
75 mblvol 25503 . . . . . . . . . . . . . . 15 ((𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol → (vol‘(𝐴 ∩ (𝐵[,]𝑧))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑧))))
7674, 75syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol‘(𝐴 ∩ (𝐵[,]𝑧))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑧))))
7767, 76eqtrd 2765 . . . . . . . . . . . . 13 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐹𝑧) = (vol*‘(𝐴 ∩ (𝐵[,]𝑧))))
78 simpr1 1191 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → 𝑦 ∈ ℝ)
79 oveq2 7427 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐵[,]𝑥) = (𝐵[,]𝑦))
8079ineq2d 4210 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝐴 ∩ (𝐵[,]𝑥)) = (𝐴 ∩ (𝐵[,]𝑦)))
8180fveq2d 6900 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → (vol‘(𝐴 ∩ (𝐵[,]𝑥))) = (vol‘(𝐴 ∩ (𝐵[,]𝑦))))
82 fvex 6909 . . . . . . . . . . . . . . . 16 (vol‘(𝐴 ∩ (𝐵[,]𝑦))) ∈ V
8381, 19, 82fvmpt 7004 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ → (𝐹𝑦) = (vol‘(𝐴 ∩ (𝐵[,]𝑦))))
8478, 83syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐹𝑦) = (vol‘(𝐴 ∩ (𝐵[,]𝑦))))
85 simp1 1133 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧) → 𝑦 ∈ ℝ)
86 iccmbl 25539 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐵[,]𝑦) ∈ dom vol)
8769, 85, 86syl2an 594 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐵[,]𝑦) ∈ dom vol)
88 inmbl 25515 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ dom vol ∧ (𝐵[,]𝑦) ∈ dom vol) → (𝐴 ∩ (𝐵[,]𝑦)) ∈ dom vol)
8968, 87, 88syl2anc 582 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐴 ∩ (𝐵[,]𝑦)) ∈ dom vol)
90 mblvol 25503 . . . . . . . . . . . . . . 15 ((𝐴 ∩ (𝐵[,]𝑦)) ∈ dom vol → (vol‘(𝐴 ∩ (𝐵[,]𝑦))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑦))))
9189, 90syl 17 . . . . . . . . . . . . . 14 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol‘(𝐴 ∩ (𝐵[,]𝑦))) = (vol*‘(𝐴 ∩ (𝐵[,]𝑦))))
9284, 91eqtrd 2765 . . . . . . . . . . . . 13 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐹𝑦) = (vol*‘(𝐴 ∩ (𝐵[,]𝑦))))
9377, 92oveq12d 7437 . . . . . . . . . . . 12 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((𝐹𝑧) − (𝐹𝑦)) = ((vol*‘(𝐴 ∩ (𝐵[,]𝑧))) − (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))))
9449adantr 479 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → 𝐹:ℝ⟶ℝ)
9594, 61ffvelcdmd 7094 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐹𝑧) ∈ ℝ)
9677, 95eqeltrrd 2826 . . . . . . . . . . . . . 14 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ∈ ℝ)
9770leidd 11812 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → 𝐵𝐵)
98 simpr3 1193 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → 𝑦𝑧)
99 iccss 13427 . . . . . . . . . . . . . . . . . . 19 (((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (𝐵𝐵𝑦𝑧)) → (𝐵[,]𝑦) ⊆ (𝐵[,]𝑧))
10070, 61, 97, 98, 99syl22anc 837 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐵[,]𝑦) ⊆ (𝐵[,]𝑧))
101 sslin 4233 . . . . . . . . . . . . . . . . . 18 ((𝐵[,]𝑦) ⊆ (𝐵[,]𝑧) → (𝐴 ∩ (𝐵[,]𝑦)) ⊆ (𝐴 ∩ (𝐵[,]𝑧)))
102100, 101syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐴 ∩ (𝐵[,]𝑦)) ⊆ (𝐴 ∩ (𝐵[,]𝑧)))
103 mblss 25504 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∩ (𝐵[,]𝑧)) ∈ dom vol → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ℝ)
10474, 103syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ℝ)
105102, 104sstrd 3987 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐴 ∩ (𝐵[,]𝑦)) ⊆ ℝ)
106 iccssre 13441 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦[,]𝑧) ⊆ ℝ)
10778, 61, 106syl2anc 582 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝑦[,]𝑧) ⊆ ℝ)
108105, 107unssd 4184 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ⊆ ℝ)
10994, 78ffvelcdmd 7094 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐹𝑦) ∈ ℝ)
11092, 109eqeltrrd 2826 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ∈ ℝ)
11161, 78resubcld 11674 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝑧𝑦) ∈ ℝ)
112110, 111readdcld 11275 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧𝑦)) ∈ ℝ)
113 ovolicc 25496 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧) → (vol*‘(𝑦[,]𝑧)) = (𝑧𝑦))
114113adantl 480 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol*‘(𝑦[,]𝑧)) = (𝑧𝑦))
115114, 111eqeltrd 2825 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol*‘(𝑦[,]𝑧)) ∈ ℝ)
116 ovolun 25472 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∩ (𝐵[,]𝑦)) ⊆ ℝ ∧ (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ∈ ℝ) ∧ ((𝑦[,]𝑧) ⊆ ℝ ∧ (vol*‘(𝑦[,]𝑧)) ∈ ℝ)) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (vol*‘(𝑦[,]𝑧))))
117105, 110, 107, 115, 116syl22anc 837 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (vol*‘(𝑦[,]𝑧))))
118114oveq2d 7435 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (vol*‘(𝑦[,]𝑧))) = ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧𝑦)))
119117, 118breqtrd 5175 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧𝑦)))
120 ovollecl 25456 . . . . . . . . . . . . . . 15 ((((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ⊆ ℝ ∧ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧𝑦)) ∈ ℝ ∧ (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧𝑦))) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ∈ ℝ)
121108, 112, 119, 120syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))) ∈ ℝ)
12270adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝐵𝑦) → 𝐵 ∈ ℝ)
12361adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝐵𝑦) → 𝑧 ∈ ℝ)
12478adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝐵𝑦) → 𝑦 ∈ ℝ)
125 simpr 483 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝐵𝑦) → 𝐵𝑦)
12698adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝐵𝑦) → 𝑦𝑧)
127 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧) → 𝑧 ∈ ℝ)
128 elicc2 13424 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 ∈ (𝐵[,]𝑧) ↔ (𝑦 ∈ ℝ ∧ 𝐵𝑦𝑦𝑧)))
12969, 127, 128syl2an 594 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝑦 ∈ (𝐵[,]𝑧) ↔ (𝑦 ∈ ℝ ∧ 𝐵𝑦𝑦𝑧)))
130129adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝐵𝑦) → (𝑦 ∈ (𝐵[,]𝑧) ↔ (𝑦 ∈ ℝ ∧ 𝐵𝑦𝑦𝑧)))
131124, 125, 126, 130mpbir3and 1339 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝐵𝑦) → 𝑦 ∈ (𝐵[,]𝑧))
132 iccsplit 13497 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ∈ (𝐵[,]𝑧)) → (𝐵[,]𝑧) = ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))
133122, 123, 131, 132syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝐵𝑦) → (𝐵[,]𝑧) = ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))
134 eqimss 4035 . . . . . . . . . . . . . . . . . . 19 ((𝐵[,]𝑧) = ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))
135133, 134syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝐵𝑦) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))
13678adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝑦𝐵) → 𝑦 ∈ ℝ)
13761adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝑦𝐵) → 𝑧 ∈ ℝ)
138 simpr 483 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝑦𝐵) → 𝑦𝐵)
139137leidd 11812 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝑦𝐵) → 𝑧𝑧)
140 iccss 13427 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) ∧ (𝑦𝐵𝑧𝑧)) → (𝐵[,]𝑧) ⊆ (𝑦[,]𝑧))
141136, 137, 138, 139, 140syl22anc 837 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝑦𝐵) → (𝐵[,]𝑧) ⊆ (𝑦[,]𝑧))
142 ssun4 4173 . . . . . . . . . . . . . . . . . . 19 ((𝐵[,]𝑧) ⊆ (𝑦[,]𝑧) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))
143141, 142syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) ∧ 𝑦𝐵) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))
14470, 78, 135, 143lecasei 11352 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)))
145 sslin 4233 . . . . . . . . . . . . . . . . 17 ((𝐵[,]𝑧) ⊆ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))))
146144, 145syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))))
147 indi 4272 . . . . . . . . . . . . . . . . 17 (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) = ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝐴 ∩ (𝑦[,]𝑧)))
148 inss2 4228 . . . . . . . . . . . . . . . . . 18 (𝐴 ∩ (𝑦[,]𝑧)) ⊆ (𝑦[,]𝑧)
149 unss2 4179 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∩ (𝑦[,]𝑧)) ⊆ (𝑦[,]𝑧) → ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝐴 ∩ (𝑦[,]𝑧))) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)))
150148, 149ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝐴 ∩ (𝑦[,]𝑧))) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))
151147, 150eqsstri 4011 . . . . . . . . . . . . . . . 16 (𝐴 ∩ ((𝐵[,]𝑦) ∪ (𝑦[,]𝑧))) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))
152146, 151sstrdi 3989 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)))
153 ovolss 25458 . . . . . . . . . . . . . . 15 (((𝐴 ∩ (𝐵[,]𝑧)) ⊆ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ∧ ((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧)) ⊆ ℝ) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))))
154152, 108, 153syl2anc 582 . . . . . . . . . . . . . 14 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ (vol*‘((𝐴 ∩ (𝐵[,]𝑦)) ∪ (𝑦[,]𝑧))))
15596, 121, 112, 154, 119letrd 11403 . . . . . . . . . . . . 13 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧𝑦)))
15696, 110, 111lesubadd2d 11845 . . . . . . . . . . . . 13 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (((vol*‘(𝐴 ∩ (𝐵[,]𝑧))) − (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) ≤ (𝑧𝑦) ↔ (vol*‘(𝐴 ∩ (𝐵[,]𝑧))) ≤ ((vol*‘(𝐴 ∩ (𝐵[,]𝑦))) + (𝑧𝑦))))
157155, 156mpbird 256 . . . . . . . . . . . 12 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((vol*‘(𝐴 ∩ (𝐵[,]𝑧))) − (vol*‘(𝐴 ∩ (𝐵[,]𝑦)))) ≤ (𝑧𝑦))
15893, 157eqbrtrd 5171 . . . . . . . . . . 11 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((𝐹𝑧) − (𝐹𝑦)) ≤ (𝑧𝑦))
15995, 109resubcld 11674 . . . . . . . . . . . 12 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((𝐹𝑧) − (𝐹𝑦)) ∈ ℝ)
160 simplr 767 . . . . . . . . . . . . 13 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → 𝑒 ∈ ℝ+)
161160rpred 13051 . . . . . . . . . . . 12 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → 𝑒 ∈ ℝ)
162 lelttr 11336 . . . . . . . . . . . 12 ((((𝐹𝑧) − (𝐹𝑦)) ∈ ℝ ∧ (𝑧𝑦) ∈ ℝ ∧ 𝑒 ∈ ℝ) → ((((𝐹𝑧) − (𝐹𝑦)) ≤ (𝑧𝑦) ∧ (𝑧𝑦) < 𝑒) → ((𝐹𝑧) − (𝐹𝑦)) < 𝑒))
163159, 111, 161, 162syl3anc 1368 . . . . . . . . . . 11 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((((𝐹𝑧) − (𝐹𝑦)) ≤ (𝑧𝑦) ∧ (𝑧𝑦) < 𝑒) → ((𝐹𝑧) − (𝐹𝑦)) < 𝑒))
164158, 163mpand 693 . . . . . . . . . 10 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((𝑧𝑦) < 𝑒 → ((𝐹𝑧) − (𝐹𝑦)) < 𝑒))
165 abssubge0 15310 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧) → (abs‘(𝑧𝑦)) = (𝑧𝑦))
166165adantl 480 . . . . . . . . . . 11 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (abs‘(𝑧𝑦)) = (𝑧𝑦))
167166breq1d 5159 . . . . . . . . . 10 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((abs‘(𝑧𝑦)) < 𝑒 ↔ (𝑧𝑦) < 𝑒))
168 ovolss 25458 . . . . . . . . . . . . . 14 (((𝐴 ∩ (𝐵[,]𝑦)) ⊆ (𝐴 ∩ (𝐵[,]𝑧)) ∧ (𝐴 ∩ (𝐵[,]𝑧)) ⊆ ℝ) → (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ≤ (vol*‘(𝐴 ∩ (𝐵[,]𝑧))))
169102, 104, 168syl2anc 582 . . . . . . . . . . . . 13 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (vol*‘(𝐴 ∩ (𝐵[,]𝑦))) ≤ (vol*‘(𝐴 ∩ (𝐵[,]𝑧))))
170169, 92, 773brtr4d 5181 . . . . . . . . . . . 12 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (𝐹𝑦) ≤ (𝐹𝑧))
171109, 95, 170abssubge0d 15414 . . . . . . . . . . 11 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → (abs‘((𝐹𝑧) − (𝐹𝑦))) = ((𝐹𝑧) − (𝐹𝑦)))
172171breq1d 5159 . . . . . . . . . 10 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒 ↔ ((𝐹𝑧) − (𝐹𝑦)) < 𝑒))
173164, 167, 1723imtr4d 293 . . . . . . . . 9 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧)) → ((abs‘(𝑧𝑦)) < 𝑒 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))
17431, 41, 42, 60, 173wlogle 11779 . . . . . . . 8 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) → ((abs‘(𝑧𝑦)) < 𝑒 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))
175174anassrs 466 . . . . . . 7 (((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → ((abs‘(𝑧𝑦)) < 𝑒 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))
176175ralrimiva 3135 . . . . . 6 ((((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ ℝ) → ∀𝑧 ∈ ℝ ((abs‘(𝑧𝑦)) < 𝑒 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))
177176anasss 465 . . . . 5 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑒 ∈ ℝ+𝑦 ∈ ℝ)) → ∀𝑧 ∈ ℝ ((abs‘(𝑧𝑦)) < 𝑒 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))
178177ancom2s 648 . . . 4 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+)) → ∀𝑧 ∈ ℝ ((abs‘(𝑧𝑦)) < 𝑒 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))
179 breq2 5153 . . . . 5 (𝑑 = 𝑒 → ((abs‘(𝑧𝑦)) < 𝑑 ↔ (abs‘(𝑧𝑦)) < 𝑒))
180179rspceaimv 3612 . . . 4 ((𝑒 ∈ ℝ+ ∧ ∀𝑧 ∈ ℝ ((abs‘(𝑧𝑦)) < 𝑒 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒)) → ∃𝑑 ∈ ℝ+𝑧 ∈ ℝ ((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))
18121, 178, 180syl2anc 582 . . 3 (((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) ∧ (𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+)) → ∃𝑑 ∈ ℝ+𝑧 ∈ ℝ ((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))
182181ralrimivva 3190 . 2 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → ∀𝑦 ∈ ℝ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ ℝ ((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))
183 ax-resscn 11197 . . 3 ℝ ⊆ ℂ
184 elcncf2 24854 . . 3 ((ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ) → (𝐹 ∈ (ℝ–cn→ℝ) ↔ (𝐹:ℝ⟶ℝ ∧ ∀𝑦 ∈ ℝ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ ℝ ((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒))))
185183, 183, 184mp2an 690 . 2 (𝐹 ∈ (ℝ–cn→ℝ) ↔ (𝐹:ℝ⟶ℝ ∧ ∀𝑦 ∈ ℝ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ ℝ ((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐹𝑧) − (𝐹𝑦))) < 𝑒)))
18620, 182, 185sylanbrc 581 1 ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ) → 𝐹 ∈ (ℝ–cn→ℝ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3050  wrex 3059  cun 3942  cin 3943  wss 3944   class class class wbr 5149  cmpt 5232  dom cdm 5678  wf 6545  cfv 6549  (class class class)co 7419  cc 11138  cr 11139   + caddc 11143   < clt 11280  cle 11281  cmin 11476  +crp 13009  [,]cicc 13362  abscabs 15217  cnccncf 24840  vol*covol 25435  volcvol 25436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-inf2 9666  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217  ax-pre-sup 11218
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8847  df-pm 8848  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fi 9436  df-sup 9467  df-inf 9468  df-oi 9535  df-dju 9926  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904  df-nn 12246  df-2 12308  df-3 12309  df-n0 12506  df-z 12592  df-uz 12856  df-q 12966  df-rp 13010  df-xneg 13127  df-xadd 13128  df-xmul 13129  df-ioo 13363  df-ico 13365  df-icc 13366  df-fz 13520  df-fzo 13663  df-fl 13793  df-seq 14003  df-exp 14063  df-hash 14326  df-cj 15082  df-re 15083  df-im 15084  df-sqrt 15218  df-abs 15219  df-clim 15468  df-rlim 15469  df-sum 15669  df-rest 17407  df-topgen 17428  df-psmet 21288  df-xmet 21289  df-met 21290  df-bl 21291  df-mopn 21292  df-top 22840  df-topon 22857  df-bases 22893  df-cmp 23335  df-cncf 24842  df-ovol 25437  df-vol 25438
This theorem is referenced by:  volivth  25580
  Copyright terms: Public domain W3C validator