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

Theorem ftc1a 24091
Description: The Fundamental Theorem of Calculus, part one. The function 𝐺 formed by varying the right endpoint of an integral of 𝐹 is continuous if 𝐹 is integrable. (Contributed by Mario Carneiro, 1-Sep-2014.)
Hypotheses
Ref Expression
ftc1.g 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡)
ftc1.a (𝜑𝐴 ∈ ℝ)
ftc1.b (𝜑𝐵 ∈ ℝ)
ftc1.le (𝜑𝐴𝐵)
ftc1.s (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
ftc1.d (𝜑𝐷 ⊆ ℝ)
ftc1.i (𝜑𝐹 ∈ 𝐿1)
ftc1a.f (𝜑𝐹:𝐷⟶ℂ)
Assertion
Ref Expression
ftc1a (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Distinct variable groups:   𝑥,𝑡,𝐷   𝑡,𝐴,𝑥   𝑡,𝐵,𝑥   𝜑,𝑡,𝑥   𝑡,𝐹,𝑥
Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1a
Dummy variables 𝑠 𝑢 𝑤 𝑦 𝑧 𝑟 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ftc1.g . . 3 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡)
2 ftc1.a . . 3 (𝜑𝐴 ∈ ℝ)
3 ftc1.b . . 3 (𝜑𝐵 ∈ ℝ)
4 ftc1.le . . 3 (𝜑𝐴𝐵)
5 ftc1.s . . 3 (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
6 ftc1.d . . 3 (𝜑𝐷 ⊆ ℝ)
7 ftc1.i . . 3 (𝜑𝐹 ∈ 𝐿1)
8 ftc1a.f . . 3 (𝜑𝐹:𝐷⟶ℂ)
91, 2, 3, 4, 5, 6, 7, 8ftc1lem2 24090 . 2 (𝜑𝐺:(𝐴[,]𝐵)⟶ℂ)
10 fvexd 6390 . . . . . . 7 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑤𝐷) → (𝐹𝑤) ∈ V)
118feqmptd 6438 . . . . . . . . 9 (𝜑𝐹 = (𝑤𝐷 ↦ (𝐹𝑤)))
1211, 7eqeltrrd 2845 . . . . . . . 8 (𝜑 → (𝑤𝐷 ↦ (𝐹𝑤)) ∈ 𝐿1)
1312adantr 472 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → (𝑤𝐷 ↦ (𝐹𝑤)) ∈ 𝐿1)
14 simpr 477 . . . . . . 7 ((𝜑𝑒 ∈ ℝ+) → 𝑒 ∈ ℝ+)
1510, 13, 14itgcn 23900 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → ∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒))
16 oveq12 6851 . . . . . . . . . . . . . . 15 ((𝑠 = 𝑧𝑟 = 𝑦) → (𝑠𝑟) = (𝑧𝑦))
1716fveq2d 6379 . . . . . . . . . . . . . 14 ((𝑠 = 𝑧𝑟 = 𝑦) → (abs‘(𝑠𝑟)) = (abs‘(𝑧𝑦)))
1817breq1d 4819 . . . . . . . . . . . . 13 ((𝑠 = 𝑧𝑟 = 𝑦) → ((abs‘(𝑠𝑟)) < 𝑑 ↔ (abs‘(𝑧𝑦)) < 𝑑))
19 fveq2 6375 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑧 → (𝐺𝑠) = (𝐺𝑧))
20 fveq2 6375 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑦 → (𝐺𝑟) = (𝐺𝑦))
2119, 20oveqan12d 6861 . . . . . . . . . . . . . . 15 ((𝑠 = 𝑧𝑟 = 𝑦) → ((𝐺𝑠) − (𝐺𝑟)) = ((𝐺𝑧) − (𝐺𝑦)))
2221fveq2d 6379 . . . . . . . . . . . . . 14 ((𝑠 = 𝑧𝑟 = 𝑦) → (abs‘((𝐺𝑠) − (𝐺𝑟))) = (abs‘((𝐺𝑧) − (𝐺𝑦))))
2322breq1d 4819 . . . . . . . . . . . . 13 ((𝑠 = 𝑧𝑟 = 𝑦) → ((abs‘((𝐺𝑠) − (𝐺𝑟))) < 𝑒 ↔ (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))
2418, 23imbi12d 335 . . . . . . . . . . . 12 ((𝑠 = 𝑧𝑟 = 𝑦) → (((abs‘(𝑠𝑟)) < 𝑑 → (abs‘((𝐺𝑠) − (𝐺𝑟))) < 𝑒) ↔ ((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒)))
2524ancoms 450 . . . . . . . . . . 11 ((𝑟 = 𝑦𝑠 = 𝑧) → (((abs‘(𝑠𝑟)) < 𝑑 → (abs‘((𝐺𝑠) − (𝐺𝑟))) < 𝑒) ↔ ((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒)))
26 oveq12 6851 . . . . . . . . . . . . . . 15 ((𝑠 = 𝑦𝑟 = 𝑧) → (𝑠𝑟) = (𝑦𝑧))
2726fveq2d 6379 . . . . . . . . . . . . . 14 ((𝑠 = 𝑦𝑟 = 𝑧) → (abs‘(𝑠𝑟)) = (abs‘(𝑦𝑧)))
2827breq1d 4819 . . . . . . . . . . . . 13 ((𝑠 = 𝑦𝑟 = 𝑧) → ((abs‘(𝑠𝑟)) < 𝑑 ↔ (abs‘(𝑦𝑧)) < 𝑑))
29 fveq2 6375 . . . . . . . . . . . . . . . 16 (𝑠 = 𝑦 → (𝐺𝑠) = (𝐺𝑦))
30 fveq2 6375 . . . . . . . . . . . . . . . 16 (𝑟 = 𝑧 → (𝐺𝑟) = (𝐺𝑧))
3129, 30oveqan12d 6861 . . . . . . . . . . . . . . 15 ((𝑠 = 𝑦𝑟 = 𝑧) → ((𝐺𝑠) − (𝐺𝑟)) = ((𝐺𝑦) − (𝐺𝑧)))
3231fveq2d 6379 . . . . . . . . . . . . . 14 ((𝑠 = 𝑦𝑟 = 𝑧) → (abs‘((𝐺𝑠) − (𝐺𝑟))) = (abs‘((𝐺𝑦) − (𝐺𝑧))))
3332breq1d 4819 . . . . . . . . . . . . 13 ((𝑠 = 𝑦𝑟 = 𝑧) → ((abs‘((𝐺𝑠) − (𝐺𝑟))) < 𝑒 ↔ (abs‘((𝐺𝑦) − (𝐺𝑧))) < 𝑒))
3428, 33imbi12d 335 . . . . . . . . . . . 12 ((𝑠 = 𝑦𝑟 = 𝑧) → (((abs‘(𝑠𝑟)) < 𝑑 → (abs‘((𝐺𝑠) − (𝐺𝑟))) < 𝑒) ↔ ((abs‘(𝑦𝑧)) < 𝑑 → (abs‘((𝐺𝑦) − (𝐺𝑧))) < 𝑒)))
3534ancoms 450 . . . . . . . . . . 11 ((𝑟 = 𝑧𝑠 = 𝑦) → (((abs‘(𝑠𝑟)) < 𝑑 → (abs‘((𝐺𝑠) − (𝐺𝑟))) < 𝑒) ↔ ((abs‘(𝑦𝑧)) < 𝑑 → (abs‘((𝐺𝑦) − (𝐺𝑧))) < 𝑒)))
36 iccssre 12457 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
372, 3, 36syl2anc 579 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
3837ad2antrr 717 . . . . . . . . . . 11 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) → (𝐴[,]𝐵) ⊆ ℝ)
3937ad3antrrr 721 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐴[,]𝐵) ⊆ ℝ)
40 simprr 789 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ (𝐴[,]𝐵))
4139, 40sseldd 3762 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ ℝ)
4241recnd 10322 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑧 ∈ ℂ)
43 simprl 787 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ (𝐴[,]𝐵))
4439, 43sseldd 3762 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℝ)
4544recnd 10322 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝑦 ∈ ℂ)
4642, 45abssubd 14479 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (abs‘(𝑧𝑦)) = (abs‘(𝑦𝑧)))
4746breq1d 4819 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑧𝑦)) < 𝑑 ↔ (abs‘(𝑦𝑧)) < 𝑑))
489ad3antrrr 721 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → 𝐺:(𝐴[,]𝐵)⟶ℂ)
4948, 40ffvelrnd 6550 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐺𝑧) ∈ ℂ)
5048, 43ffvelrnd 6550 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (𝐺𝑦) ∈ ℂ)
5149, 50abssubd 14479 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑧) − (𝐺𝑦))) = (abs‘((𝐺𝑦) − (𝐺𝑧))))
5251breq1d 4819 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒 ↔ (abs‘((𝐺𝑦) − (𝐺𝑧))) < 𝑒))
5347, 52imbi12d 335 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒) ↔ ((abs‘(𝑦𝑧)) < 𝑑 → (abs‘((𝐺𝑦) − (𝐺𝑧))) < 𝑒)))
54 simpr3 1252 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → 𝑦𝑧)
552adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → 𝐴 ∈ ℝ)
563adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → 𝐵 ∈ ℝ)
574adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → 𝐴𝐵)
585adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → (𝐴(,)𝐵) ⊆ 𝐷)
596adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → 𝐷 ⊆ ℝ)
607adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → 𝐹 ∈ 𝐿1)
618adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → 𝐹:𝐷⟶ℂ)
62 simpr1 1248 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → 𝑦 ∈ (𝐴[,]𝐵))
63 simpr2 1250 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → 𝑧 ∈ (𝐴[,]𝐵))
641, 55, 56, 57, 58, 59, 60, 61, 62, 63ftc1lem1 24089 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) ∧ 𝑦𝑧) → ((𝐺𝑧) − (𝐺𝑦)) = ∫(𝑦(,)𝑧)(𝐹𝑡) d𝑡)
6554, 64mpdan 678 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → ((𝐺𝑧) − (𝐺𝑦)) = ∫(𝑦(,)𝑧)(𝐹𝑡) d𝑡)
6665adantlr 706 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → ((𝐺𝑧) − (𝐺𝑦)) = ∫(𝑦(,)𝑧)(𝐹𝑡) d𝑡)
6766ad2ant2r 753 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → ((𝐺𝑧) − (𝐺𝑦)) = ∫(𝑦(,)𝑧)(𝐹𝑡) d𝑡)
6867fveq2d 6379 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (abs‘((𝐺𝑧) − (𝐺𝑦))) = (abs‘∫(𝑦(,)𝑧)(𝐹𝑡) d𝑡))
69 fvexd 6390 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (𝐹𝑡) ∈ V)
702ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝐴 ∈ ℝ)
7170rexrd 10343 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝐴 ∈ ℝ*)
72 simprl1 1281 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝑦 ∈ (𝐴[,]𝐵))
733ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝐵 ∈ ℝ)
74 elicc2 12440 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵)))
7570, 73, 74syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵)))
7672, 75mpbid 223 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵))
7776simp2d 1173 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝐴𝑦)
78 iooss1 12412 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℝ*𝐴𝑦) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝑧))
7971, 77, 78syl2anc 579 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝑧))
8073rexrd 10343 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝐵 ∈ ℝ*)
81 simprl2 1283 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝑧 ∈ (𝐴[,]𝐵))
82 elicc2 12440 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴𝑧𝑧𝐵)))
8370, 73, 82syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑧 ∈ (𝐴[,]𝐵) ↔ (𝑧 ∈ ℝ ∧ 𝐴𝑧𝑧𝐵)))
8481, 83mpbid 223 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑧 ∈ ℝ ∧ 𝐴𝑧𝑧𝐵))
8584simp3d 1174 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝑧𝐵)
86 iooss2 12413 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ ℝ*𝑧𝐵) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵))
8780, 85, 86syl2anc 579 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝐴(,)𝑧) ⊆ (𝐴(,)𝐵))
8879, 87sstrd 3771 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ (𝐴(,)𝐵))
895ad3antrrr 721 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝐴(,)𝐵) ⊆ 𝐷)
9088, 89sstrd 3771 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑦(,)𝑧) ⊆ 𝐷)
91 ioombl 23623 . . . . . . . . . . . . . . . . . 18 (𝑦(,)𝑧) ∈ dom vol
9291a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑦(,)𝑧) ∈ dom vol)
93 fvexd 6390 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ V)
948feqmptd 6438 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹 = (𝑡𝐷 ↦ (𝐹𝑡)))
9594, 7eqeltrrd 2845 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
9695ad3antrrr 721 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
9790, 92, 93, 96iblss 23862 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹𝑡)) ∈ 𝐿1)
9869, 97itgcl 23841 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(𝐹𝑡) d𝑡 ∈ ℂ)
9998abscld 14462 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹𝑡) d𝑡) ∈ ℝ)
100 iblmbf 23825 . . . . . . . . . . . . . . . . . 18 ((𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹𝑡)) ∈ 𝐿1 → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹𝑡)) ∈ MblFn)
10197, 100syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (𝐹𝑡)) ∈ MblFn)
102101, 69mbfmptcl 23694 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (𝐹𝑡) ∈ ℂ)
103102abscld 14462 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) ∧ 𝑡 ∈ (𝑦(,)𝑧)) → (abs‘(𝐹𝑡)) ∈ ℝ)
10469, 97iblabs 23886 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑡 ∈ (𝑦(,)𝑧) ↦ (abs‘(𝐹𝑡))) ∈ 𝐿1)
105103, 104itgrecl 23855 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(abs‘(𝐹𝑡)) d𝑡 ∈ ℝ)
106 simprl 787 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) → 𝑒 ∈ ℝ+)
107106ad2antrr 717 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝑒 ∈ ℝ+)
108107rpred 12070 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝑒 ∈ ℝ)
10969, 97itgabs 23892 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹𝑡) d𝑡) ≤ ∫(𝑦(,)𝑧)(abs‘(𝐹𝑡)) d𝑡)
110 mblvol 23588 . . . . . . . . . . . . . . . . . 18 ((𝑦(,)𝑧) ∈ dom vol → (vol‘(𝑦(,)𝑧)) = (vol*‘(𝑦(,)𝑧)))
11191, 110ax-mp 5 . . . . . . . . . . . . . . . . 17 (vol‘(𝑦(,)𝑧)) = (vol*‘(𝑦(,)𝑧))
112 ioossre 12437 . . . . . . . . . . . . . . . . . . 19 (𝑦(,)𝑧) ⊆ ℝ
113 ovolcl 23536 . . . . . . . . . . . . . . . . . . 19 ((𝑦(,)𝑧) ⊆ ℝ → (vol*‘(𝑦(,)𝑧)) ∈ ℝ*)
114112, 113mp1i 13 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ∈ ℝ*)
11584simp1d 1172 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝑧 ∈ ℝ)
11676simp1d 1172 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝑦 ∈ ℝ)
117115, 116resubcld 10712 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑧𝑦) ∈ ℝ)
118117rexrd 10343 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑧𝑦) ∈ ℝ*)
119 simprr 789 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) → 𝑑 ∈ ℝ+)
120119ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝑑 ∈ ℝ+)
121120rpxrd 12071 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝑑 ∈ ℝ*)
122 ioossicc 12461 . . . . . . . . . . . . . . . . . . . 20 (𝑦(,)𝑧) ⊆ (𝑦[,]𝑧)
123 iccssre 12457 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦[,]𝑧) ⊆ ℝ)
124116, 115, 123syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑦[,]𝑧) ⊆ ℝ)
125 ovolss 23543 . . . . . . . . . . . . . . . . . . . 20 (((𝑦(,)𝑧) ⊆ (𝑦[,]𝑧) ∧ (𝑦[,]𝑧) ⊆ ℝ) → (vol*‘(𝑦(,)𝑧)) ≤ (vol*‘(𝑦[,]𝑧)))
126122, 124, 125sylancr 581 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ≤ (vol*‘(𝑦[,]𝑧)))
127 simprl3 1285 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → 𝑦𝑧)
128 ovolicc 23581 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦𝑧) → (vol*‘(𝑦[,]𝑧)) = (𝑧𝑦))
129116, 115, 127, 128syl3anc 1490 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (vol*‘(𝑦[,]𝑧)) = (𝑧𝑦))
130126, 129breqtrd 4835 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) ≤ (𝑧𝑦))
131116, 115, 127abssubge0d 14457 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (abs‘(𝑧𝑦)) = (𝑧𝑦))
132 simprr 789 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (abs‘(𝑧𝑦)) < 𝑑)
133131, 132eqbrtrrd 4833 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (𝑧𝑦) < 𝑑)
134114, 118, 121, 130, 133xrlelttrd 12193 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (vol*‘(𝑦(,)𝑧)) < 𝑑)
135111, 134syl5eqbr 4844 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (vol‘(𝑦(,)𝑧)) < 𝑑)
13690, 135jca 507 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → ((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑))
137 sseq1 3786 . . . . . . . . . . . . . . . . . 18 (𝑢 = (𝑦(,)𝑧) → (𝑢𝐷 ↔ (𝑦(,)𝑧) ⊆ 𝐷))
138 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑢 = (𝑦(,)𝑧) → (vol‘𝑢) = (vol‘(𝑦(,)𝑧)))
139138breq1d 4819 . . . . . . . . . . . . . . . . . 18 (𝑢 = (𝑦(,)𝑧) → ((vol‘𝑢) < 𝑑 ↔ (vol‘(𝑦(,)𝑧)) < 𝑑))
140137, 139anbi12d 624 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑦(,)𝑧) → ((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) ↔ ((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑)))
141 2fveq3 6380 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑡 → (abs‘(𝐹𝑤)) = (abs‘(𝐹𝑡)))
142141cbvitgv 23834 . . . . . . . . . . . . . . . . . . 19 𝑢(abs‘(𝐹𝑤)) d𝑤 = ∫𝑢(abs‘(𝐹𝑡)) d𝑡
143 itgeq1 23830 . . . . . . . . . . . . . . . . . . 19 (𝑢 = (𝑦(,)𝑧) → ∫𝑢(abs‘(𝐹𝑡)) d𝑡 = ∫(𝑦(,)𝑧)(abs‘(𝐹𝑡)) d𝑡)
144142, 143syl5eq 2811 . . . . . . . . . . . . . . . . . 18 (𝑢 = (𝑦(,)𝑧) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 = ∫(𝑦(,)𝑧)(abs‘(𝐹𝑡)) d𝑡)
145144breq1d 4819 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑦(,)𝑧) → (∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒 ↔ ∫(𝑦(,)𝑧)(abs‘(𝐹𝑡)) d𝑡 < 𝑒))
146140, 145imbi12d 335 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑦(,)𝑧) → (((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒) ↔ (((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑) → ∫(𝑦(,)𝑧)(abs‘(𝐹𝑡)) d𝑡 < 𝑒)))
147 simplr 785 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒))
148146, 147, 92rspcdva 3467 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (((𝑦(,)𝑧) ⊆ 𝐷 ∧ (vol‘(𝑦(,)𝑧)) < 𝑑) → ∫(𝑦(,)𝑧)(abs‘(𝐹𝑡)) d𝑡 < 𝑒))
149136, 148mpd 15 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → ∫(𝑦(,)𝑧)(abs‘(𝐹𝑡)) d𝑡 < 𝑒)
15099, 105, 108, 109, 149lelttrd 10449 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (abs‘∫(𝑦(,)𝑧)(𝐹𝑡) d𝑡) < 𝑒)
15168, 150eqbrtrd 4831 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ ((𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧) ∧ (abs‘(𝑧𝑦)) < 𝑑)) → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒)
152151expr 448 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵) ∧ 𝑦𝑧)) → ((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))
15325, 35, 38, 53, 152wlogle 10815 . . . . . . . . . 10 ((((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑧 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))
154153ralrimivva 3118 . . . . . . . . 9 (((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) ∧ ∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒)) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))
155154ex 401 . . . . . . . 8 ((𝜑 ∧ (𝑒 ∈ ℝ+𝑑 ∈ ℝ+)) → (∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒)))
156155anassrs 459 . . . . . . 7 (((𝜑𝑒 ∈ ℝ+) ∧ 𝑑 ∈ ℝ+) → (∀𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒)))
157156reximdva 3163 . . . . . 6 ((𝜑𝑒 ∈ ℝ+) → (∃𝑑 ∈ ℝ+𝑢 ∈ dom vol((𝑢𝐷 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘(𝐹𝑤)) d𝑤 < 𝑒) → ∃𝑑 ∈ ℝ+𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒)))
15815, 157mpd 15 . . . . 5 ((𝜑𝑒 ∈ ℝ+) → ∃𝑑 ∈ ℝ+𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))
159 r19.12 3210 . . . . 5 (∃𝑑 ∈ ℝ+𝑦 ∈ (𝐴[,]𝐵)∀𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒) → ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))
160158, 159syl 17 . . . 4 ((𝜑𝑒 ∈ ℝ+) → ∀𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))
161160ralrimiva 3113 . . 3 (𝜑 → ∀𝑒 ∈ ℝ+𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))
162 ralcom 3245 . . 3 (∀𝑒 ∈ ℝ+𝑦 ∈ (𝐴[,]𝐵)∃𝑑 ∈ ℝ+𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))
163161, 162sylib 209 . 2 (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))
164 ax-resscn 10246 . . . 4 ℝ ⊆ ℂ
16537, 164syl6ss 3773 . . 3 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
166 ssid 3783 . . 3 ℂ ⊆ ℂ
167 elcncf2 22972 . . 3 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))))
168165, 166, 167sylancl 580 . 2 (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑦 ∈ (𝐴[,]𝐵)∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ (𝐴[,]𝐵)((abs‘(𝑧𝑦)) < 𝑑 → (abs‘((𝐺𝑧) − (𝐺𝑦))) < 𝑒))))
1699, 163, 168mpbir2and 704 1 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  wrex 3056  Vcvv 3350  wss 3732   class class class wbr 4809  cmpt 4888  dom cdm 5277  wf 6064  cfv 6068  (class class class)co 6842  cc 10187  cr 10188  *cxr 10327   < clt 10328  cle 10329  cmin 10520  +crp 12028  (,)cioo 12377  [,]cicc 12380  abscabs 14261  cnccncf 22958  vol*covol 23520  volcvol 23521  MblFncmbf 23672  𝐿1cibl 23675  citg 23676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cc 9510  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-symdif 4005  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-disj 4778  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-ofr 7096  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-omul 7769  df-er 7947  df-map 8062  df-pm 8063  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-acn 9019  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ioc 12382  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-clim 14506  df-rlim 14507  df-sum 14704  df-struct 16134  df-ndx 16135  df-slot 16136  df-base 16138  df-sets 16139  df-ress 16140  df-plusg 16229  df-mulr 16230  df-starv 16231  df-sca 16232  df-vsca 16233  df-ip 16234  df-tset 16235  df-ple 16236  df-ds 16238  df-unif 16239  df-hom 16240  df-cco 16241  df-rest 16351  df-topn 16352  df-0g 16370  df-gsum 16371  df-topgen 16372  df-pt 16373  df-prds 16376  df-xrs 16430  df-qtop 16435  df-imas 16436  df-xps 16438  df-mre 16514  df-mrc 16515  df-acs 16517  df-mgm 17510  df-sgrp 17552  df-mnd 17563  df-submnd 17604  df-mulg 17810  df-cntz 18015  df-cmn 18461  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-cnfld 20020  df-top 20978  df-topon 20995  df-topsp 21017  df-bases 21030  df-cn 21311  df-cnp 21312  df-cmp 21470  df-tx 21645  df-hmeo 21838  df-xms 22404  df-ms 22405  df-tms 22406  df-cncf 22960  df-ovol 23522  df-vol 23523  df-mbf 23677  df-itg1 23678  df-itg2 23679  df-ibl 23680  df-itg 23681  df-0p 23728
This theorem is referenced by:  ftc2  24098
  Copyright terms: Public domain W3C validator