Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ftc1anc Structured version   Visualization version   GIF version

Theorem ftc1anc 36045
Description: ftc1a 25323 holds for functions that obey the triangle inequality in the absence of ax-cc 10305. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.)
Hypotheses
Ref Expression
ftc1anc.g 𝐺 = (π‘₯ ∈ (𝐴[,]𝐡) ↦ ∫(𝐴(,)π‘₯)(πΉβ€˜π‘‘) d𝑑)
ftc1anc.a (πœ‘ β†’ 𝐴 ∈ ℝ)
ftc1anc.b (πœ‘ β†’ 𝐡 ∈ ℝ)
ftc1anc.le (πœ‘ β†’ 𝐴 ≀ 𝐡)
ftc1anc.s (πœ‘ β†’ (𝐴(,)𝐡) βŠ† 𝐷)
ftc1anc.d (πœ‘ β†’ 𝐷 βŠ† ℝ)
ftc1anc.i (πœ‘ β†’ 𝐹 ∈ 𝐿1)
ftc1anc.f (πœ‘ β†’ 𝐹:π·βŸΆβ„‚)
ftc1anc.t (πœ‘ β†’ βˆ€π‘  ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)))(absβ€˜βˆ«π‘ (πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0))))
Assertion
Ref Expression
ftc1anc (πœ‘ β†’ 𝐺 ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
Distinct variable groups:   𝑑,𝑠,π‘₯,𝐴   𝐡,𝑠,𝑑,π‘₯   𝐷,𝑠,𝑑,π‘₯   𝐹,𝑠,𝑑,π‘₯   πœ‘,𝑠,𝑑,π‘₯   𝐺,𝑠
Allowed substitution hints:   𝐺(π‘₯,𝑑)

Proof of Theorem ftc1anc
Dummy variables π‘Ž 𝑏 𝑓 𝑔 π‘Ÿ 𝑒 𝑀 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ftc1anc.g . . 3 𝐺 = (π‘₯ ∈ (𝐴[,]𝐡) ↦ ∫(𝐴(,)π‘₯)(πΉβ€˜π‘‘) d𝑑)
2 ftc1anc.a . . 3 (πœ‘ β†’ 𝐴 ∈ ℝ)
3 ftc1anc.b . . 3 (πœ‘ β†’ 𝐡 ∈ ℝ)
4 ftc1anc.le . . 3 (πœ‘ β†’ 𝐴 ≀ 𝐡)
5 ftc1anc.s . . 3 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† 𝐷)
6 ftc1anc.d . . 3 (πœ‘ β†’ 𝐷 βŠ† ℝ)
7 ftc1anc.i . . 3 (πœ‘ β†’ 𝐹 ∈ 𝐿1)
8 ftc1anc.f . . 3 (πœ‘ β†’ 𝐹:π·βŸΆβ„‚)
91, 2, 3, 4, 5, 6, 7, 8ftc1lem2 25322 . 2 (πœ‘ β†’ 𝐺:(𝐴[,]𝐡)βŸΆβ„‚)
10 rphalfcl 12871 . . . . . 6 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ+)
111, 2, 3, 4, 5, 6, 7, 8ftc1anclem6 36042 . . . . . 6 ((πœ‘ ∧ (𝑦 / 2) ∈ ℝ+) β†’ βˆƒπ‘“ ∈ dom ∫1βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2))
1210, 11sylan2 594 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘“ ∈ dom ∫1βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2))
1312adantrl 715 . . . 4 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) β†’ βˆƒπ‘“ ∈ dom ∫1βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2))
1410ad2antll 728 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) β†’ (𝑦 / 2) ∈ ℝ+)
15 2rp 12849 . . . . . . . . . . . 12 2 ∈ ℝ+
16 i1ff 24962 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ dom ∫1 β†’ 𝑓:β„βŸΆβ„)
1716frnd 6672 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 β†’ ran 𝑓 βŠ† ℝ)
1817adantr 482 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ran 𝑓 βŠ† ℝ)
19 i1ff 24962 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ dom ∫1 β†’ 𝑔:β„βŸΆβ„)
2019frnd 6672 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 β†’ ran 𝑔 βŠ† ℝ)
2120adantl 483 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ran 𝑔 βŠ† ℝ)
2218, 21unssd 4145 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† ℝ)
23 ax-resscn 11042 . . . . . . . . . . . . . . . . . 18 ℝ βŠ† β„‚
2422, 23sstrdi 3955 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚)
25 i1f0rn 24968 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 β†’ 0 ∈ ran 𝑓)
26 elun1 4135 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ran 𝑓 β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
2725, 26syl 17 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
2827adantr 482 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
29 absf 15157 . . . . . . . . . . . . . . . . . . 19 abs:β„‚βŸΆβ„
30 ffn 6664 . . . . . . . . . . . . . . . . . . 19 (abs:β„‚βŸΆβ„ β†’ abs Fn β„‚)
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . . 18 abs Fn β„‚
32 fnfvima 7178 . . . . . . . . . . . . . . . . . 18 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
3331, 32mp3an1 1449 . . . . . . . . . . . . . . . . 17 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
3424, 28, 33syl2anc 585 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
3534ne0d 4294 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ…)
36 imassrn 6021 . . . . . . . . . . . . . . . . 17 (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ran abs
37 frn 6671 . . . . . . . . . . . . . . . . . 18 (abs:β„‚βŸΆβ„ β†’ ran abs βŠ† ℝ)
3829, 37ax-mp 5 . . . . . . . . . . . . . . . . 17 ran abs βŠ† ℝ
3936, 38sstri 3952 . . . . . . . . . . . . . . . 16 (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ
40 ffun 6667 . . . . . . . . . . . . . . . . . 18 (abs:β„‚βŸΆβ„ β†’ Fun abs)
4129, 40ax-mp 5 . . . . . . . . . . . . . . . . 17 Fun abs
42 i1frn 24963 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 β†’ ran 𝑓 ∈ Fin)
43 i1frn 24963 . . . . . . . . . . . . . . . . . 18 (𝑔 ∈ dom ∫1 β†’ ran 𝑔 ∈ Fin)
44 unfi 9050 . . . . . . . . . . . . . . . . . 18 ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) β†’ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin)
4542, 43, 44syl2an 597 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin)
46 imafi 9053 . . . . . . . . . . . . . . . . 17 ((Fun abs ∧ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin)
4741, 45, 46sylancr 588 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin)
48 fimaxre2 12034 . . . . . . . . . . . . . . . 16 (((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯)
4939, 47, 48sylancr 588 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯)
50 suprcl 12049 . . . . . . . . . . . . . . . 16 (((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
5139, 50mp3an1 1449 . . . . . . . . . . . . . . 15 (((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
5235, 49, 51syl2anc 585 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
5352adantr 482 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
54 0red 11092 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 ∈ ℝ)
5524sselda 3943 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ π‘Ÿ ∈ β„‚)
5655abscld 15256 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ ℝ)
5756adantrr 716 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ (absβ€˜π‘Ÿ) ∈ ℝ)
5852adantr 482 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
59 absgt0 15144 . . . . . . . . . . . . . . . . . . 19 (π‘Ÿ ∈ β„‚ β†’ (π‘Ÿ β‰  0 ↔ 0 < (absβ€˜π‘Ÿ)))
6055, 59syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (π‘Ÿ β‰  0 ↔ 0 < (absβ€˜π‘Ÿ)))
6160biimpd 228 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (π‘Ÿ β‰  0 β†’ 0 < (absβ€˜π‘Ÿ)))
6261impr 456 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 < (absβ€˜π‘Ÿ))
6339a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ)
6463, 35, 493jca 1129 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯))
6564adantr 482 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ ((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯))
66 fnfvima 7178 . . . . . . . . . . . . . . . . . . . 20 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
6731, 66mp3an1 1449 . . . . . . . . . . . . . . . . . . 19 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
6824, 67sylan 581 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
69 suprub 12050 . . . . . . . . . . . . . . . . . 18 ((((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) ∧ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
7065, 68, 69syl2anc 585 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
7170adantrr 716 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
7254, 57, 58, 62, 71ltletrd 11249 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 < sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
7372rexlimdvaa 3152 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0 β†’ 0 < sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
7473imp 408 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ 0 < sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
7553, 74elrpd 12883 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+)
76 rpmulcl 12867 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
7715, 75, 76sylancr 588 . . . . . . . . . . 11 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
78 rpdivcl 12869 . . . . . . . . . . 11 (((𝑦 / 2) ∈ ℝ+ ∧ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
7914, 77, 78syl2an 597 . . . . . . . . . 10 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0)) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
8079anassrs 469 . . . . . . . . 9 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
8180adantlr 714 . . . . . . . 8 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
82 ancom 462 . . . . . . . . . . . 12 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+) ↔ (𝑦 ∈ ℝ+ ∧ 𝑒 ∈ (𝐴[,]𝐡)))
8382anbi2i 624 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ↔ ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑦 ∈ ℝ+ ∧ 𝑒 ∈ (𝐴[,]𝐡))))
84 an32 645 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ↔ ((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)))
8584anbi1i 625 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ↔ (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)))
86 an32 645 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ↔ (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)))
8785, 86bitri 275 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ↔ (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)))
8887anbi1i 625 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ↔ ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0))
89 an32 645 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ↔ ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)))
9088, 89bitri 275 . . . . . . . . . . 11 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ↔ ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)))
91 anass 470 . . . . . . . . . . 11 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑒 ∈ (𝐴[,]𝐡)) ↔ ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑦 ∈ ℝ+ ∧ 𝑒 ∈ (𝐴[,]𝐡))))
9283, 90, 913bitr4i 303 . . . . . . . . . 10 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ↔ (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑒 ∈ (𝐴[,]𝐡)))
93 oveq12 7359 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑀 ∧ π‘Ž = 𝑒) β†’ (𝑏 βˆ’ π‘Ž) = (𝑀 βˆ’ 𝑒))
9493ancoms 460 . . . . . . . . . . . . . . 15 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ (𝑏 βˆ’ π‘Ž) = (𝑀 βˆ’ 𝑒))
9594fveq2d 6842 . . . . . . . . . . . . . 14 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ (absβ€˜(𝑏 βˆ’ π‘Ž)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
9695breq1d 5114 . . . . . . . . . . . . 13 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ ((absβ€˜(𝑏 βˆ’ π‘Ž)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ↔ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))))
97 fveq2 6838 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑀 β†’ (πΊβ€˜π‘) = (πΊβ€˜π‘€))
98 fveq2 6838 . . . . . . . . . . . . . . . 16 (π‘Ž = 𝑒 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜π‘’))
9997, 98oveqan12rd 7370 . . . . . . . . . . . . . . 15 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ ((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž)) = ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)))
10099fveq2d 6842 . . . . . . . . . . . . . 14 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ (absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) = (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))))
101100breq1d 5114 . . . . . . . . . . . . 13 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ ((absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) < 𝑦 ↔ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
10296, 101imbi12d 345 . . . . . . . . . . . 12 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ (((absβ€˜(𝑏 βˆ’ π‘Ž)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) < 𝑦) ↔ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)))
103 oveq12 7359 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑒 ∧ π‘Ž = 𝑀) β†’ (𝑏 βˆ’ π‘Ž) = (𝑒 βˆ’ 𝑀))
104103ancoms 460 . . . . . . . . . . . . . . 15 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ (𝑏 βˆ’ π‘Ž) = (𝑒 βˆ’ 𝑀))
105104fveq2d 6842 . . . . . . . . . . . . . 14 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ (absβ€˜(𝑏 βˆ’ π‘Ž)) = (absβ€˜(𝑒 βˆ’ 𝑀)))
106105breq1d 5114 . . . . . . . . . . . . 13 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ ((absβ€˜(𝑏 βˆ’ π‘Ž)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ↔ (absβ€˜(𝑒 βˆ’ 𝑀)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))))
107 fveq2 6838 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑒 β†’ (πΊβ€˜π‘) = (πΊβ€˜π‘’))
108 fveq2 6838 . . . . . . . . . . . . . . . 16 (π‘Ž = 𝑀 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜π‘€))
109107, 108oveqan12rd 7370 . . . . . . . . . . . . . . 15 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ ((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž)) = ((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€)))
110109fveq2d 6842 . . . . . . . . . . . . . 14 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ (absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) = (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))))
111110breq1d 5114 . . . . . . . . . . . . 13 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ ((absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) < 𝑦 ↔ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) < 𝑦))
112106, 111imbi12d 345 . . . . . . . . . . . 12 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ (((absβ€˜(𝑏 βˆ’ π‘Ž)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) < 𝑦) ↔ ((absβ€˜(𝑒 βˆ’ 𝑀)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) < 𝑦)))
113 iccssre 13275 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴[,]𝐡) βŠ† ℝ)
1142, 3, 113syl2anc 585 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
115114ad4antr 731 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (𝐴[,]𝐡) βŠ† ℝ)
116 simp-4l 782 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ πœ‘)
117114, 23sstrdi 3955 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† β„‚)
118117sselda 3943 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑀 ∈ β„‚)
119117sselda 3943 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝑒 ∈ β„‚)
120 abssub 15146 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ β„‚ ∧ 𝑒 ∈ β„‚) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) = (absβ€˜(𝑒 βˆ’ 𝑀)))
121118, 119, 120syl2anr 598 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ (πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) = (absβ€˜(𝑒 βˆ’ 𝑀)))
122121anandis 677 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) = (absβ€˜(𝑒 βˆ’ 𝑀)))
123122breq1d 5114 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ↔ (absβ€˜(𝑒 βˆ’ 𝑀)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))))
1249ffvelcdmda 7030 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (πΊβ€˜π‘€) ∈ β„‚)
1259ffvelcdmda 7030 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ (πΊβ€˜π‘’) ∈ β„‚)
126 abssub 15146 . . . . . . . . . . . . . . . . 17 (((πΊβ€˜π‘€) ∈ β„‚ ∧ (πΊβ€˜π‘’) ∈ β„‚) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) = (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))))
127124, 125, 126syl2anr 598 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ (πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) = (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))))
128127anandis 677 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) = (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))))
129128breq1d 5114 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦 ↔ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) < 𝑦))
130123, 129imbi12d 345 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦) ↔ ((absβ€˜(𝑒 βˆ’ 𝑀)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) < 𝑦)))
131116, 130sylan 581 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦) ↔ ((absβ€˜(𝑒 βˆ’ 𝑀)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) < 𝑦)))
1322rexrd 11139 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐴 ∈ ℝ*)
1333rexrd 11139 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐡 ∈ ℝ*)
134132, 133jca 513 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*))
135 df-icc 13200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 [,] = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑑 ∈ ℝ* ∣ (π‘₯ ≀ 𝑑 ∧ 𝑑 ≀ 𝑦)})
136135elixx3g 13206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑒 ∈ (𝐴[,]𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑒 ∈ ℝ*) ∧ (𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡)))
137136simprbi 498 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 ∈ (𝐴[,]𝐡) β†’ (𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡))
138137simpld 496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒 ∈ (𝐴[,]𝐡) β†’ 𝐴 ≀ 𝑒)
139135elixx3g 13206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 ∈ (𝐴[,]𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑀 ∈ ℝ*) ∧ (𝐴 ≀ 𝑀 ∧ 𝑀 ≀ 𝐡)))
140139simprbi 498 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 ∈ (𝐴[,]𝐡) β†’ (𝐴 ≀ 𝑀 ∧ 𝑀 ≀ 𝐡))
141140simprd 497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ (𝐴[,]𝐡) β†’ 𝑀 ≀ 𝐡)
142138, 141anim12i 614 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴 ≀ 𝑒 ∧ 𝑀 ≀ 𝐡))
143 ioossioo 13287 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*) ∧ (𝐴 ≀ 𝑒 ∧ 𝑀 ≀ 𝐡)) β†’ (𝑒(,)𝑀) βŠ† (𝐴(,)𝐡))
144134, 142, 143syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) βŠ† (𝐴(,)𝐡))
1455adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝐴(,)𝐡) βŠ† 𝐷)
146144, 145sstrd 3953 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) βŠ† 𝐷)
147146sselda 3943 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
1488ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
149148abscld 15256 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(πΉβ€˜π‘‘)) ∈ ℝ)
150149rexrd 11139 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(πΉβ€˜π‘‘)) ∈ ℝ*)
151148absge0d 15264 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ 0 ≀ (absβ€˜(πΉβ€˜π‘‘)))
152 elxrge0 13303 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((absβ€˜(πΉβ€˜π‘‘)) ∈ (0[,]+∞) ↔ ((absβ€˜(πΉβ€˜π‘‘)) ∈ ℝ* ∧ 0 ≀ (absβ€˜(πΉβ€˜π‘‘))))
153150, 151, 152sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(πΉβ€˜π‘‘)) ∈ (0[,]+∞))
154153adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(πΉβ€˜π‘‘)) ∈ (0[,]+∞))
155147, 154syldan 592 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜(πΉβ€˜π‘‘)) ∈ (0[,]+∞))
156 0e0iccpnf 13305 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ (0[,]+∞)
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ∈ (0[,]+∞))
158155, 157ifclda 4520 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
159158adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
160159fmpttd 7058 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞))
161 itg2cl 25019 . . . . . . . . . . . . . . . . . . 19 ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
162160, 161syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
1631623adantr3 1172 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
164116, 163sylan 581 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
165164adantr 482 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
166 simplll 774 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
167148adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
168147, 167syldan 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
169168adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
170 elioore 13223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 ∈ (𝑒(,)𝑀) β†’ 𝑑 ∈ ℝ)
17116ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ℝ)
172171recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ β„‚)
173 ax-icn 11044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 i ∈ β„‚
17419ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ℝ)
175174recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ β„‚)
176 mulcl 11069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((i ∈ β„‚ ∧ (π‘”β€˜π‘‘) ∈ β„‚) β†’ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚)
177173, 175, 176sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚)
178 addcl 11067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((π‘“β€˜π‘‘) ∈ β„‚ ∧ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
179172, 177, 178syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
180179anandirs 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
181170, 180sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
182181adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
183182adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
184169, 183subcld 11446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
185184abscld 15256 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
186181abscld 15256 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ)
187186adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ)
188187adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ)
189185, 188readdcld 11118 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
190189rexrd 11139 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
191184absge0d 15264 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
192180absge0d 15264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
193170, 192sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
194193adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
195194adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
196185, 188, 191, 195addge0d 11665 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
197 elxrge0 13303 . . . . . . . . . . . . . . . . . . . . . . 23 (((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞) ↔ (((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ* ∧ 0 ≀ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
198190, 196, 197sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞))
199156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ∈ (0[,]+∞))
200198, 199ifclda 4520 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
201200adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
202201fmpttd 7058 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞))
203 itg2cl 25019 . . . . . . . . . . . . . . . . . . 19 ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
204202, 203syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
2052043adantr3 1172 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
206166, 205sylan 581 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
207206adantr 482 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
208 rpxr 12853 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ*)
209208ad3antlr 730 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ 𝑦 ∈ ℝ*)
210158adantlr 714 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
211210adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
212211fmpttd 7058 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞))
213169, 183npcand 11450 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) + ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = (πΉβ€˜π‘‘))
214213fveq2d 6842 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜(((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) + ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = (absβ€˜(πΉβ€˜π‘‘)))
215184, 183abstrid 15276 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜(((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) + ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
216214, 215eqbrtrrd 5128 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜(πΉβ€˜π‘‘)) ≀ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
217 iftrue 4491 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) = (absβ€˜(πΉβ€˜π‘‘)))
218217adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) = (absβ€˜(πΉβ€˜π‘‘)))
219 iftrue 4491 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) = ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
220219adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) = ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
221216, 218, 2203brtr4d 5136 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))
222221ex 414 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
223 0le0 12188 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≀ 0
224223a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ 0 ≀ 0)
225 iffalse 4494 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) = 0)
226 iffalse 4494 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) = 0)
227224, 225, 2263brtr4d 5136 . . . . . . . . . . . . . . . . . . . . . 22 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))
228222, 227pm2.61d1 180 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))
229228ralrimivw 3146 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))
230 reex 11076 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ V
231230a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ℝ ∈ V)
232 fvex 6851 . . . . . . . . . . . . . . . . . . . . . . . 24 (absβ€˜(πΉβ€˜π‘‘)) ∈ V
233 c0ex 11083 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
234232, 233ifex 4535 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ V
235234a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ V)
236 ovex 7383 . . . . . . . . . . . . . . . . . . . . . . . 24 ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ V
237236, 233ifex 4535 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ V
238237a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ V)
239 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)))
240 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
241231, 235, 238, 239, 240ofrfval2 7629 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
242241ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
243229, 242mpbird 257 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
244 itg2le 25026 . . . . . . . . . . . . . . . . . . 19 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞) ∧ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞) ∧ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))))
245212, 202, 243, 244syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))))
2462453adantr3 1172 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))))
247166, 246sylan 581 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))))
248247adantr 482 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))))
2491, 2, 3, 4, 5, 6, 7, 8ftc1anclem8 36044 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) < 𝑦)
250165, 207, 209, 248, 249xrlelttrd 13008 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) < 𝑦)
251 simplll 774 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ πœ‘)
252 simpr2 1196 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑀 ∈ (𝐴[,]𝐡))
253 oveq2 7358 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ = 𝑀 β†’ (𝐴(,)π‘₯) = (𝐴(,)𝑀))
254 itgeq1 25059 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴(,)π‘₯) = (𝐴(,)𝑀) β†’ ∫(𝐴(,)π‘₯)(πΉβ€˜π‘‘) d𝑑 = ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
255253, 254syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = 𝑀 β†’ ∫(𝐴(,)π‘₯)(πΉβ€˜π‘‘) d𝑑 = ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
256 itgex 25057 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑 ∈ V
257255, 1, 256fvmpt 6944 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 ∈ (𝐴[,]𝐡) β†’ (πΊβ€˜π‘€) = ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
258252, 257syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (πΊβ€˜π‘€) = ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
2592adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝐴 ∈ ℝ)
260114sselda 3943 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑀 ∈ ℝ)
2612603ad2antr2 1190 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑀 ∈ ℝ)
262114sselda 3943 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝑒 ∈ ℝ)
263262rexrd 11139 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝑒 ∈ ℝ*)
2642633ad2antr1 1189 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑒 ∈ ℝ*)
265 elicc1 13237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*) β†’ (𝑒 ∈ (𝐴[,]𝐡) ↔ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡)))
266132, 133, 265syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑒 ∈ (𝐴[,]𝐡) ↔ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡)))
267266biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡))
268267simp2d 1144 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝐴 ≀ 𝑒)
2692683ad2antr1 1189 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝐴 ≀ 𝑒)
270 simpr3 1197 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑒 ≀ 𝑀)
271132adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝐴 ∈ ℝ*)
272260rexrd 11139 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑀 ∈ ℝ*)
273 elicc1 13237 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℝ* ∧ 𝑀 ∈ ℝ*) β†’ (𝑒 ∈ (𝐴[,]𝑀) ↔ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝑀)))
274271, 272, 273syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑒 ∈ (𝐴[,]𝑀) ↔ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝑀)))
2752743ad2antr2 1190 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑒 ∈ (𝐴[,]𝑀) ↔ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝑀)))
276264, 269, 270, 275mpbir3and 1343 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑒 ∈ (𝐴[,]𝑀))
277 iooss2 13229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐡 ∈ ℝ* ∧ 𝑀 ≀ 𝐡) β†’ (𝐴(,)𝑀) βŠ† (𝐴(,)𝐡))
278133, 141, 277syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴(,)𝑀) βŠ† (𝐴(,)𝐡))
2795adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴(,)𝐡) βŠ† 𝐷)
280278, 279sstrd 3953 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴(,)𝑀) βŠ† 𝐷)
2812803ad2antr2 1190 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝐴(,)𝑀) βŠ† 𝐷)
282281sselda 3943 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝐴(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
283148adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
284282, 283syldan 592 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝐴(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
285 eleq1w 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = 𝑒 β†’ (𝑀 ∈ (𝐴[,]𝐡) ↔ 𝑒 ∈ (𝐴[,]𝐡)))
286285anbi2d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 = 𝑒 β†’ ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) ↔ (πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡))))
287 oveq2 7358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = 𝑒 β†’ (𝐴(,)𝑀) = (𝐴(,)𝑒))
288287mpteq1d 5199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = 𝑒 β†’ (𝑑 ∈ (𝐴(,)𝑀) ↦ (πΉβ€˜π‘‘)) = (𝑑 ∈ (𝐴(,)𝑒) ↦ (πΉβ€˜π‘‘)))
289288eleq1d 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 = 𝑒 β†’ ((𝑑 ∈ (𝐴(,)𝑀) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1 ↔ (𝑑 ∈ (𝐴(,)𝑒) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1))
290286, 289imbi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = 𝑒 β†’ (((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑑 ∈ (𝐴(,)𝑀) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1) ↔ ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ (𝑑 ∈ (𝐴(,)𝑒) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)))
291 ioombl 24851 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝑀) ∈ dom vol
292291a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴(,)𝑀) ∈ dom vol)
293148adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
2948feqmptd 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ 𝐹 = (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)))
295294, 7eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
296295adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
297280, 292, 293, 296iblss 25091 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑑 ∈ (𝐴(,)𝑀) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
298290, 297chvarvv 2003 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ (𝑑 ∈ (𝐴(,)𝑒) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
2992983ad2antr1 1189 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑑 ∈ (𝐴(,)𝑒) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
300 ioombl 24851 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒(,)𝑀) ∈ dom vol
301300a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) ∈ dom vol)
302 fvexd 6853 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ V)
303295adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
304146, 301, 302, 303iblss 25091 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ (𝑒(,)𝑀) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
3053043adantr3 1172 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑑 ∈ (𝑒(,)𝑀) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
306259, 261, 276, 284, 299, 305itgsplitioo 25124 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑 = (∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 + ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑))
307258, 306eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (πΊβ€˜π‘€) = (∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 + ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑))
308 simpr1 1195 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑒 ∈ (𝐴[,]𝐡))
309 oveq2 7358 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = 𝑒 β†’ (𝐴(,)π‘₯) = (𝐴(,)𝑒))
310 itgeq1 25059 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴(,)π‘₯) = (𝐴(,)𝑒) β†’ ∫(𝐴(,)π‘₯)(πΉβ€˜π‘‘) d𝑑 = ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑)
311309, 310syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = 𝑒 β†’ ∫(𝐴(,)π‘₯)(πΉβ€˜π‘‘) d𝑑 = ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑)
312 itgex 25057 . . . . . . . . . . . . . . . . . . . . . . . 24 ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 ∈ V
313311, 1, 312fvmpt 6944 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ (𝐴[,]𝐡) β†’ (πΊβ€˜π‘’) = ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑)
314308, 313syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (πΊβ€˜π‘’) = ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑)
315307, 314oveq12d 7368 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) = ((∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 + ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) βˆ’ ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑))
316 fvexd 6853 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ 𝑑 ∈ (𝐴(,)𝑒)) β†’ (πΉβ€˜π‘‘) ∈ V)
317316, 298itgcl 25070 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 ∈ β„‚)
318317adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 ∈ β„‚)
319 fvexd 6853 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ V)
320319, 304itgcl 25070 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑 ∈ β„‚)
321318, 320pncan2d 11448 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 + ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) βˆ’ ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑) = ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
3223213adantr3 1172 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 + ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) βˆ’ ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑) = ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
323315, 322eqtrd 2778 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) = ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
324323fveq2d 6842 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) = (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑))
325 ftc1anc.t . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ βˆ€π‘  ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)))(absβ€˜βˆ«π‘ (πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0))))
326 df-ov 7353 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒(,)𝑀) = ((,)β€˜βŸ¨π‘’, π‘€βŸ©)
327 opelxpi 5668 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ βŸ¨π‘’, π‘€βŸ© ∈ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)))
328 ioof 13293 . . . . . . . . . . . . . . . . . . . . . . . . 25 (,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ
329 ffn 6664 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ β†’ (,) Fn (ℝ* Γ— ℝ*))
330328, 329ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (,) Fn (ℝ* Γ— ℝ*)
331 iccssxr 13276 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴[,]𝐡) βŠ† ℝ*
332 xpss12 5646 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴[,]𝐡) βŠ† ℝ* ∧ (𝐴[,]𝐡) βŠ† ℝ*) β†’ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)) βŠ† (ℝ* Γ— ℝ*))
333331, 331, 332mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)) βŠ† (ℝ* Γ— ℝ*)
334 fnfvima 7178 . . . . . . . . . . . . . . . . . . . . . . . 24 (((,) Fn (ℝ* Γ— ℝ*) ∧ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)) βŠ† (ℝ* Γ— ℝ*) ∧ βŸ¨π‘’, π‘€βŸ© ∈ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡))) β†’ ((,)β€˜βŸ¨π‘’, π‘€βŸ©) ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡))))
335330, 333, 334mp3an12 1452 . . . . . . . . . . . . . . . . . . . . . . 23 (βŸ¨π‘’, π‘€βŸ© ∈ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)) β†’ ((,)β€˜βŸ¨π‘’, π‘€βŸ©) ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡))))
336327, 335syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ ((,)β€˜βŸ¨π‘’, π‘€βŸ©) ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡))))
337326, 336eqeltrid 2843 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑒(,)𝑀) ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡))))
338 itgeq1 25059 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑒(,)𝑀) β†’ βˆ«π‘ (πΉβ€˜π‘‘) d𝑑 = ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
339338fveq2d 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑒(,)𝑀) β†’ (absβ€˜βˆ«π‘ (πΉβ€˜π‘‘) d𝑑) = (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑))
340 eleq2 2827 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑒(,)𝑀) β†’ (𝑑 ∈ 𝑠 ↔ 𝑑 ∈ (𝑒(,)𝑀)))
341340ifbid 4508 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑒(,)𝑀) β†’ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0) = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))
342341mpteq2dv 5206 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑒(,)𝑀) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)))
343342fveq2d 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑒(,)𝑀) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0))) = (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
344339, 343breq12d 5117 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑒(,)𝑀) β†’ ((absβ€˜βˆ«π‘ (πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0))) ↔ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)))))
345344rspccva 3579 . . . . . . . . . . . . . . . . . . . . 21 ((βˆ€π‘  ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)))(absβ€˜βˆ«π‘ (πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0))) ∧ (𝑒(,)𝑀) ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)))) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
346325, 337, 345syl2an 597 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
3473463adantr3 1172 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
348324, 347eqbrtrd 5126 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
349348adantlr 714 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
350 subcl 11334 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πΊβ€˜π‘€) ∈ β„‚ ∧ (πΊβ€˜π‘’) ∈ β„‚) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) ∈ β„‚)
351124, 125, 350syl2anr 598 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ (πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) ∈ β„‚)
352351anandis 677 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) ∈ β„‚)
353352abscld 15256 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ)
354353rexrd 11139 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ*)
3553543adantr3 1172 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ*)
356355adantlr 714 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ*)
357163adantlr 714 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
358208ad2antlr 726 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑦 ∈ ℝ*)
359 xrlelttr 13004 . . . . . . . . . . . . . . . . . 18 (((absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ* ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ* ∧ 𝑦 ∈ ℝ*) β†’ (((absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) < 𝑦) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
360356, 357, 358, 359syl3anc 1372 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (((absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) < 𝑦) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
361349, 360mpand 694 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) < 𝑦 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
362251, 361sylanl1 679 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) < 𝑦 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
363362adantr 482 . . . . . . . . . . . . . 14 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) < 𝑦 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
364250, 363mpd 15 . . . . . . . . . . . . 13 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)
365364ex 414 . . . . . . . . . . . 12 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
366102, 112, 115, 131, 365wlogle 11622 . . . . . . . . . . 11 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
367366anassrs 469 . . . . . . . . . 10 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
36892, 367sylanb 582 . . . . . . . . 9 ((((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
369368ralrimiva 3142 . . . . . . . 8 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
370 breq2 5108 . . . . . . . . 9 (𝑧 = ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 ↔ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))))
371370rspceaimv 3584 . . . . . . . 8 ((((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
37281, 369, 371syl2anc 585 . . . . . . 7 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
373 ralnex 3074 . . . . . . . . 9 (βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) Β¬ π‘Ÿ β‰  0 ↔ Β¬ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0)
374 nne 2946 . . . . . . . . . 10 (Β¬ π‘Ÿ β‰  0 ↔ π‘Ÿ = 0)
375374ralbii 3095 . . . . . . . . 9 (βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) Β¬ π‘Ÿ β‰  0 ↔ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0)
376373, 375bitr3i 277 . . . . . . . 8 (Β¬ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0 ↔ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0)
37716ffnd 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 ∈ dom ∫1 β†’ 𝑓 Fn ℝ)
378 fnfvelrn 7027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓 Fn ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ran 𝑓)
379377, 378sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ran 𝑓)
380 elun1 4135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((π‘“β€˜π‘‘) ∈ ran 𝑓 β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
381379, 380syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
382 eqeq1 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘Ÿ = (π‘“β€˜π‘‘) β†’ (π‘Ÿ = 0 ↔ (π‘“β€˜π‘‘) = 0))
383382rspcva 3578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (π‘“β€˜π‘‘) = 0)
384381, 383sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (π‘“β€˜π‘‘) = 0)
385384adantllr 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (π‘“β€˜π‘‘) = 0)
38619ffnd 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 ∈ dom ∫1 β†’ 𝑔 Fn ℝ)
387 fnfvelrn 7027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔 Fn ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ran 𝑔)
388386, 387sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ran 𝑔)
389 elun2 4136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((π‘”β€˜π‘‘) ∈ ran 𝑔 β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
390388, 389syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
391 eqeq1 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘Ÿ = (π‘”β€˜π‘‘) β†’ (π‘Ÿ = 0 ↔ (π‘”β€˜π‘‘) = 0))
392391rspcva 3578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (π‘”β€˜π‘‘) = 0)
393392oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (i Β· (π‘”β€˜π‘‘)) = (i Β· 0))
394 it0e0 12309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (i Β· 0) = 0
395393, 394eqtrdi 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (i Β· (π‘”β€˜π‘‘)) = 0)
396390, 395sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (i Β· (π‘”β€˜π‘‘)) = 0)
397396adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (i Β· (π‘”β€˜π‘‘)) = 0)
398385, 397oveq12d 7368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) = (0 + 0))
399398an32s 651 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) = (0 + 0))
400 00id 11264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 + 0) = 0
401399, 400eqtrdi 2794 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) = 0)
402401adantlll 717 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) = 0)
403402oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ 0))
404 0cnd 11082 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ Β¬ 𝑑 ∈ 𝐷) β†’ 0 ∈ β„‚)
405148, 404ifclda 4520 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) ∈ β„‚)
406405subid1d 11435 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ 0) = if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))
407406ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ 0) = if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))
408403, 407eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))
409408fveq2d 6842 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = (absβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
410 fvif 6854 . . . . . . . . . . . . . . . . . . . . . 22 (absβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), (absβ€˜0))
411 abs0 15105 . . . . . . . . . . . . . . . . . . . . . . 23 (absβ€˜0) = 0
412 ifeq2 4490 . . . . . . . . . . . . . . . . . . . . . . 23 ((absβ€˜0) = 0 β†’ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), (absβ€˜0)) = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))
413411, 412ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), (absβ€˜0)) = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)
414410, 413eqtri 2766 . . . . . . . . . . . . . . . . . . . . 21 (absβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)
415409, 414eqtrdi 2794 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))
416415mpteq2dva 5204 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
417416fveq2d 6842 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) = (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
418417breq1d 5114 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ↔ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)))
419418biimpd 228 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)))
420419ex 414 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) β†’ (βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0 β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2))))
421420com23 86 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) β†’ (βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0 β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2))))
422421imp32 420 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2))
423422anasss 468 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2))
424423adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2))
425 1rp 12848 . . . . . . . . . . . . 13 1 ∈ ℝ+
426425ne0ii 4296 . . . . . . . . . . . 12 ℝ+ β‰  βˆ…
427352anassrs 469 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) ∈ β„‚)
428427abscld 15256 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ)
429428adantlrr 720 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ)
430429adantlr 714 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ)
431 rpre 12852 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ)
432431rehalfcld 12334 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ)
433432adantl 483 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+) β†’ (𝑦 / 2) ∈ ℝ)
434433ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑦 / 2) ∈ ℝ)
435431adantl 483 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+) β†’ 𝑦 ∈ ℝ)
436435ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑦 ∈ ℝ)
437430rexrd 11139 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ*)
438156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ Β¬ 𝑑 ∈ 𝐷) β†’ 0 ∈ (0[,]+∞))
439153, 438ifclda 4520 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
440439adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
441440fmpttd 7058 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞))
442 itg2cl 25019 . . . . . . . . . . . . . . . . . . 19 ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
443441, 442syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
444443ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
445434rexrd 11139 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑦 / 2) ∈ ℝ*)
446108, 107oveqan12rd 7370 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 = 𝑒 ∧ π‘Ž = 𝑀) β†’ ((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘)) = ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)))
447446fveq2d 6842 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 = 𝑒 ∧ π‘Ž = 𝑀) β†’ (absβ€˜((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘))) = (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))))
448447breq1d 5114 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑒 ∧ π‘Ž = 𝑀) β†’ ((absβ€˜((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ↔ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))))
44998, 97oveqan12rd 7370 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 = 𝑀 ∧ π‘Ž = 𝑒) β†’ ((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘)) = ((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€)))
450449fveq2d 6842 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 = 𝑀 ∧ π‘Ž = 𝑒) β†’ (absβ€˜((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘))) = (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))))
451450breq1d 5114 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑀 ∧ π‘Ž = 𝑒) β†’ ((absβ€˜((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ↔ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))))
452128breq1d 5114 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ↔ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))))
453320abscld 15256 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ∈ ℝ)
454453rexrd 11139 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ∈ ℝ*)
455443adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
456441adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞))
457 breq2 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((absβ€˜(πΉβ€˜π‘‘)) = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) β†’ (if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘)) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
458 breq2 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) β†’ (if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ 0 ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
459149leidd 11655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(πΉβ€˜π‘‘)) ≀ (absβ€˜(πΉβ€˜π‘‘)))
460 breq1 5107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((absβ€˜(πΉβ€˜π‘‘)) = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) β†’ ((absβ€˜(πΉβ€˜π‘‘)) ≀ (absβ€˜(πΉβ€˜π‘‘)) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘))))
461 breq1 5107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0 = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) β†’ (0 ≀ (absβ€˜(πΉβ€˜π‘‘)) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘))))
462460, 461ifboth 4524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((absβ€˜(πΉβ€˜π‘‘)) ≀ (absβ€˜(πΉβ€˜π‘‘)) ∧ 0 ≀ (absβ€˜(πΉβ€˜π‘‘))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘)))
463459, 151, 462syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘)))
464463adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘)))
465146ssneld 3945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (Β¬ 𝑑 ∈ 𝐷 β†’ Β¬ 𝑑 ∈ (𝑒(,)𝑀)))
466465imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ Β¬ 𝑑 ∈ 𝐷) β†’ Β¬ 𝑑 ∈ (𝑒(,)𝑀))
467225, 223eqbrtrdi 5143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ 0)
468466, 467syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ Β¬ 𝑑 ∈ 𝐷) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ 0)
469457, 458, 464, 468ifbothda 4523 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))
470469ralrimivw 3146 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))
471232, 233ifex 4535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ V
472471a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ V)
473 eqidd 2739 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
474231, 235, 472, 239, 473ofrfval2 7629 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
475474adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
476470, 475mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
477 itg2le 25026 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞) ∧ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞) ∧ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
478160, 456, 476, 477syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
479454, 162, 455, 346, 478xrletrd 13010 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
4804793adantr3 1172 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
481324, 480eqbrtrd 5126 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
482448, 451, 114, 452, 481wlogle 11622 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
483482anassrs 469 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
484483adantlrr 720 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
485484adantlr 714 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
486 simplr 768 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2))
487437, 444, 445, 485, 486xrlelttrd 13008 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < (𝑦 / 2))
488 rphalflt 12873 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) < 𝑦)
489488adantl 483 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+) β†’ (𝑦 / 2) < 𝑦)
490489ad3antlr 730 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑦 / 2) < 𝑦)
491430, 434, 436, 487, 490lttrd 11250 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)
492491a1d 25 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
493492ralrimiva 3142 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) β†’ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
494493ralrimivw 3146 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) β†’ βˆ€π‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
495 r19.2z 4451 . . . . . . . . . . . 12 ((ℝ+ β‰  βˆ… ∧ βˆ€π‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
496426, 494, 495sylancr 588 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
497424, 496syldan 592 . . . . . . . . . 10 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0))) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
498497anassrs 469 . . . . . . . . 9 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
499498anassrs 469 . . . . . . . 8 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
500376, 499sylan2b 595 . . . . . . 7 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ Β¬ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
501372, 500pm2.61dan 812 . . . . . 6 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
502501ex 414 . . . . 5 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)))
503502rexlimdvva 3204 . . . 4 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) β†’ (βˆƒπ‘“ ∈ dom ∫1βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)))
50413, 503mpd 15 . . 3 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
505504ralrimivva 3196 . 2 (πœ‘ β†’ βˆ€π‘’ ∈ (𝐴[,]𝐡)βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
506 ssid 3965 . . 3 β„‚ βŠ† β„‚
507 elcncf2 24175 . . 3 (((𝐴[,]𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (𝐺 ∈ ((𝐴[,]𝐡)–cnβ†’β„‚) ↔ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ βˆ€π‘’ ∈ (𝐴[,]𝐡)βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))))
508117, 506, 507sylancl 587 . 2 (πœ‘ β†’ (𝐺 ∈ ((𝐴[,]𝐡)–cnβ†’β„‚) ↔ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ βˆ€π‘’ ∈ (𝐴[,]𝐡)βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))))
5099, 505, 508mpbir2and 712 1 (πœ‘ β†’ 𝐺 ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2942  βˆ€wral 3063  βˆƒwrex 3072  Vcvv 3444   βˆͺ cun 3907   βŠ† wss 3909  βˆ…c0 4281  ifcif 4485  π’« cpw 4559  βŸ¨cop 4591   class class class wbr 5104   ↦ cmpt 5187   Γ— cxp 5629  dom cdm 5631  ran crn 5632   β€œ cima 5634  Fun wfun 6486   Fn wfn 6487  βŸΆwf 6488  β€˜cfv 6492  (class class class)co 7350   ∘r cofr 7607  Fincfn 8817  supcsup 9310  β„‚cc 10983  β„cr 10984  0cc0 10985  1c1 10986  ici 10987   + caddc 10988   Β· cmul 10990  +∞cpnf 11120  β„*cxr 11122   < clt 11123   ≀ cle 11124   βˆ’ cmin 11319   / cdiv 11746  2c2 12142  β„+crp 12844  (,)cioo 13193  [,]cicc 13196  abscabs 15053  β€“cnβ†’ccncf 24161  volcvol 24749  βˆ«1citg1 24901  βˆ«2citg2 24902  πΏ1cibl 24903  βˆ«citg 24904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-inf2 9511  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063  ax-addf 11064
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-symdif 4201  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-disj 5070  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-of 7608  df-ofr 7609  df-om 7794  df-1st 7912  df-2nd 7913  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8582  df-map 8701  df-pm 8702  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-fi 9281  df-sup 9312  df-inf 9313  df-oi 9380  df-dju 9771  df-card 9809  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-4 12152  df-n0 12348  df-z 12434  df-uz 12697  df-q 12803  df-rp 12845  df-xneg 12962  df-xadd 12963  df-xmul 12964  df-ioo 13197  df-ico 13199  df-icc 13200  df-fz 13354  df-fzo 13497  df-fl 13626  df-mod 13704  df-seq 13836  df-exp 13897  df-hash 14159  df-cj 14918  df-re 14919  df-im 14920  df-sqrt 15054  df-abs 15055  df-clim 15305  df-rlim 15306  df-sum 15506  df-rest 17239  df-topgen 17260  df-psmet 20711  df-xmet 20712  df-met 20713  df-bl 20714  df-mopn 20715  df-top 22165  df-topon 22182  df-bases 22218  df-cmp 22660  df-cncf 24163  df-ovol 24750  df-vol 24751  df-mbf 24905  df-itg1 24906  df-itg2 24907  df-ibl 24908  df-itg 24909  df-0p 24956
This theorem is referenced by:  ftc2nc  36046
  Copyright terms: Public domain W3C validator