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 36054
Description: ftc1a 25323 holds for functions that obey the triangle inequality in the absence of ax-cc 10304. 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 12870 . . . . . 6 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ+)
111, 2, 3, 4, 5, 6, 7, 8ftc1anclem6 36051 . . . . . 6 ((πœ‘ ∧ (𝑦 / 2) ∈ ℝ+) β†’ βˆƒπ‘“ ∈ dom ∫1βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2))
1210, 11sylan2 593 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ ℝ+) β†’ βˆƒπ‘“ ∈ dom ∫1βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2))
1312adantrl 714 . . . 4 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) β†’ βˆƒπ‘“ ∈ dom ∫1βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2))
1410ad2antll 727 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) β†’ (𝑦 / 2) ∈ ℝ+)
15 2rp 12848 . . . . . . . . . . . 12 2 ∈ ℝ+
16 i1ff 24962 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ dom ∫1 β†’ 𝑓:β„βŸΆβ„)
1716frnd 6671 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 β†’ ran 𝑓 βŠ† ℝ)
1817adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ran 𝑓 βŠ† ℝ)
19 i1ff 24962 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ dom ∫1 β†’ 𝑔:β„βŸΆβ„)
2019frnd 6671 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 β†’ ran 𝑔 βŠ† ℝ)
2120adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ran 𝑔 βŠ† ℝ)
2218, 21unssd 4144 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† ℝ)
23 ax-resscn 11041 . . . . . . . . . . . . . . . . . 18 ℝ βŠ† β„‚
2422, 23sstrdi 3954 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚)
25 i1f0rn 24968 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 β†’ 0 ∈ ran 𝑓)
26 elun1 4134 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ran 𝑓 β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
2725, 26syl 17 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
2827adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
29 absf 15156 . . . . . . . . . . . . . . . . . . 19 abs:β„‚βŸΆβ„
30 ffn 6663 . . . . . . . . . . . . . . . . . . 19 (abs:β„‚βŸΆβ„ β†’ abs Fn β„‚)
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . . 18 abs Fn β„‚
32 fnfvima 7177 . . . . . . . . . . . . . . . . . 18 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
3331, 32mp3an1 1448 . . . . . . . . . . . . . . . . 17 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
3424, 28, 33syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
3534ne0d 4293 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ…)
36 imassrn 6020 . . . . . . . . . . . . . . . . 17 (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ran abs
37 frn 6670 . . . . . . . . . . . . . . . . . 18 (abs:β„‚βŸΆβ„ β†’ ran abs βŠ† ℝ)
3829, 37ax-mp 5 . . . . . . . . . . . . . . . . 17 ran abs βŠ† ℝ
3936, 38sstri 3951 . . . . . . . . . . . . . . . 16 (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ
40 ffun 6666 . . . . . . . . . . . . . . . . . 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 9049 . . . . . . . . . . . . . . . . . 18 ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) β†’ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin)
4542, 43, 44syl2an 596 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin)
46 imafi 9052 . . . . . . . . . . . . . . . . 17 ((Fun abs ∧ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin)
4741, 45, 46sylancr 587 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin)
48 fimaxre2 12033 . . . . . . . . . . . . . . . 16 (((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯)
4939, 47, 48sylancr 587 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯)
50 suprcl 12048 . . . . . . . . . . . . . . . 16 (((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
5139, 50mp3an1 1448 . . . . . . . . . . . . . . 15 (((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
5235, 49, 51syl2anc 584 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
5352adantr 481 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
54 0red 11091 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 ∈ ℝ)
5524sselda 3942 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ π‘Ÿ ∈ β„‚)
5655abscld 15255 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ ℝ)
5756adantrr 715 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ (absβ€˜π‘Ÿ) ∈ ℝ)
5852adantr 481 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
59 absgt0 15143 . . . . . . . . . . . . . . . . . . 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 455 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 < (absβ€˜π‘Ÿ))
6339a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ)
6463, 35, 493jca 1128 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯))
6564adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ ((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯))
66 fnfvima 7177 . . . . . . . . . . . . . . . . . . . 20 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
6731, 66mp3an1 1448 . . . . . . . . . . . . . . . . . . 19 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
6824, 67sylan 580 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
69 suprub 12049 . . . . . . . . . . . . . . . . . 18 ((((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) ∧ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
7065, 68, 69syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
7170adantrr 715 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
7254, 57, 58, 62, 71ltletrd 11248 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 < sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
7372rexlimdvaa 3151 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0 β†’ 0 < sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
7473imp 407 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ 0 < sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
7553, 74elrpd 12882 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+)
76 rpmulcl 12866 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
7715, 75, 76sylancr 587 . . . . . . . . . . 11 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
78 rpdivcl 12868 . . . . . . . . . . 11 (((𝑦 / 2) ∈ ℝ+ ∧ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
7914, 77, 78syl2an 596 . . . . . . . . . 10 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0)) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
8079anassrs 468 . . . . . . . . 9 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
8180adantlr 713 . . . . . . . 8 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
82 ancom 461 . . . . . . . . . . . 12 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+) ↔ (𝑦 ∈ ℝ+ ∧ 𝑒 ∈ (𝐴[,]𝐡)))
8382anbi2i 623 . . . . . . . . . . 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 644 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ↔ ((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)))
8584anbi1i 624 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ↔ (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)))
86 an32 644 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ↔ (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)))
8785, 86bitri 274 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ↔ (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)))
8887anbi1i 624 . . . . . . . . . . . 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 644 . . . . . . . . . . . 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 274 . . . . . . . . . . 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 469 . . . . . . . . . . 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 302 . . . . . . . . . 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 7358 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑀 ∧ π‘Ž = 𝑒) β†’ (𝑏 βˆ’ π‘Ž) = (𝑀 βˆ’ 𝑒))
9493ancoms 459 . . . . . . . . . . . . . . 15 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ (𝑏 βˆ’ π‘Ž) = (𝑀 βˆ’ 𝑒))
9594fveq2d 6841 . . . . . . . . . . . . . 14 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ (absβ€˜(𝑏 βˆ’ π‘Ž)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
9695breq1d 5113 . . . . . . . . . . . . 13 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ ((absβ€˜(𝑏 βˆ’ π‘Ž)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ↔ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))))
97 fveq2 6837 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑀 β†’ (πΊβ€˜π‘) = (πΊβ€˜π‘€))
98 fveq2 6837 . . . . . . . . . . . . . . . 16 (π‘Ž = 𝑒 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜π‘’))
9997, 98oveqan12rd 7369 . . . . . . . . . . . . . . 15 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ ((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž)) = ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)))
10099fveq2d 6841 . . . . . . . . . . . . . 14 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ (absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) = (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))))
101100breq1d 5113 . . . . . . . . . . . . 13 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ ((absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) < 𝑦 ↔ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
10296, 101imbi12d 344 . . . . . . . . . . . 12 ((π‘Ž = 𝑒 ∧ 𝑏 = 𝑀) β†’ (((absβ€˜(𝑏 βˆ’ π‘Ž)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) < 𝑦) ↔ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)))
103 oveq12 7358 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑒 ∧ π‘Ž = 𝑀) β†’ (𝑏 βˆ’ π‘Ž) = (𝑒 βˆ’ 𝑀))
104103ancoms 459 . . . . . . . . . . . . . . 15 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ (𝑏 βˆ’ π‘Ž) = (𝑒 βˆ’ 𝑀))
105104fveq2d 6841 . . . . . . . . . . . . . 14 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ (absβ€˜(𝑏 βˆ’ π‘Ž)) = (absβ€˜(𝑒 βˆ’ 𝑀)))
106105breq1d 5113 . . . . . . . . . . . . 13 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ ((absβ€˜(𝑏 βˆ’ π‘Ž)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ↔ (absβ€˜(𝑒 βˆ’ 𝑀)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))))
107 fveq2 6837 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑒 β†’ (πΊβ€˜π‘) = (πΊβ€˜π‘’))
108 fveq2 6837 . . . . . . . . . . . . . . . 16 (π‘Ž = 𝑀 β†’ (πΊβ€˜π‘Ž) = (πΊβ€˜π‘€))
109107, 108oveqan12rd 7369 . . . . . . . . . . . . . . 15 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ ((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž)) = ((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€)))
110109fveq2d 6841 . . . . . . . . . . . . . 14 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ (absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) = (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))))
111110breq1d 5113 . . . . . . . . . . . . 13 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ ((absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) < 𝑦 ↔ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) < 𝑦))
112106, 111imbi12d 344 . . . . . . . . . . . 12 ((π‘Ž = 𝑀 ∧ 𝑏 = 𝑒) β†’ (((absβ€˜(𝑏 βˆ’ π‘Ž)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘) βˆ’ (πΊβ€˜π‘Ž))) < 𝑦) ↔ ((absβ€˜(𝑒 βˆ’ 𝑀)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) < 𝑦)))
113 iccssre 13274 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴[,]𝐡) βŠ† ℝ)
1142, 3, 113syl2anc 584 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
115114ad4antr 730 . . . . . . . . . . . 12 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (𝐴[,]𝐡) βŠ† ℝ)
116 simp-4l 781 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ πœ‘)
117114, 23sstrdi 3954 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† β„‚)
118117sselda 3942 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑀 ∈ β„‚)
119117sselda 3942 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝑒 ∈ β„‚)
120 abssub 15145 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ β„‚ ∧ 𝑒 ∈ β„‚) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) = (absβ€˜(𝑒 βˆ’ 𝑀)))
121118, 119, 120syl2anr 597 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ (πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) = (absβ€˜(𝑒 βˆ’ 𝑀)))
122121anandis 676 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) = (absβ€˜(𝑒 βˆ’ 𝑀)))
123122breq1d 5113 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ↔ (absβ€˜(𝑒 βˆ’ 𝑀)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))))
1249ffvelcdmda 7029 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (πΊβ€˜π‘€) ∈ β„‚)
1259ffvelcdmda 7029 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ (πΊβ€˜π‘’) ∈ β„‚)
126 abssub 15145 . . . . . . . . . . . . . . . . 17 (((πΊβ€˜π‘€) ∈ β„‚ ∧ (πΊβ€˜π‘’) ∈ β„‚) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) = (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))))
127124, 125, 126syl2anr 597 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ (πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) = (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))))
128127anandis 676 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) = (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))))
129128breq1d 5113 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦 ↔ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) < 𝑦))
130123, 129imbi12d 344 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦) ↔ ((absβ€˜(𝑒 βˆ’ 𝑀)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) < 𝑦)))
131116, 130sylan 580 . . . . . . . . . . . 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 11138 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐴 ∈ ℝ*)
1333rexrd 11138 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐡 ∈ ℝ*)
134132, 133jca 512 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*))
135 df-icc 13199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 [,] = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑑 ∈ ℝ* ∣ (π‘₯ ≀ 𝑑 ∧ 𝑑 ≀ 𝑦)})
136135elixx3g 13205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑒 ∈ (𝐴[,]𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑒 ∈ ℝ*) ∧ (𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡)))
137136simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑒 ∈ (𝐴[,]𝐡) β†’ (𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡))
138137simpld 495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒 ∈ (𝐴[,]𝐡) β†’ 𝐴 ≀ 𝑒)
139135elixx3g 13205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 ∈ (𝐴[,]𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑀 ∈ ℝ*) ∧ (𝐴 ≀ 𝑀 ∧ 𝑀 ≀ 𝐡)))
140139simprbi 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 ∈ (𝐴[,]𝐡) β†’ (𝐴 ≀ 𝑀 ∧ 𝑀 ≀ 𝐡))
141140simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ (𝐴[,]𝐡) β†’ 𝑀 ≀ 𝐡)
142138, 141anim12i 613 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴 ≀ 𝑒 ∧ 𝑀 ≀ 𝐡))
143 ioossioo 13286 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*) ∧ (𝐴 ≀ 𝑒 ∧ 𝑀 ≀ 𝐡)) β†’ (𝑒(,)𝑀) βŠ† (𝐴(,)𝐡))
144134, 142, 143syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) βŠ† (𝐴(,)𝐡))
1455adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝐴(,)𝐡) βŠ† 𝐷)
146144, 145sstrd 3952 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) βŠ† 𝐷)
147146sselda 3942 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
1488ffvelcdmda 7029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
149148abscld 15255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(πΉβ€˜π‘‘)) ∈ ℝ)
150149rexrd 11138 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(πΉβ€˜π‘‘)) ∈ ℝ*)
151148absge0d 15263 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ 0 ≀ (absβ€˜(πΉβ€˜π‘‘)))
152 elxrge0 13302 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((absβ€˜(πΉβ€˜π‘‘)) ∈ (0[,]+∞) ↔ ((absβ€˜(πΉβ€˜π‘‘)) ∈ ℝ* ∧ 0 ≀ (absβ€˜(πΉβ€˜π‘‘))))
153150, 151, 152sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(πΉβ€˜π‘‘)) ∈ (0[,]+∞))
154153adantlr 713 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(πΉβ€˜π‘‘)) ∈ (0[,]+∞))
155147, 154syldan 591 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜(πΉβ€˜π‘‘)) ∈ (0[,]+∞))
156 0e0iccpnf 13304 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ (0[,]+∞)
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ∈ (0[,]+∞))
158155, 157ifclda 4519 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
159158adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
160159fmpttd 7057 . . . . . . . . . . . . . . . . . . 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 1171 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
164116, 163sylan 580 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
165164adantr 481 . . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . . . 17 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
167148adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
168147, 167syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
169168adantllr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
170 elioore 13222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 ∈ (𝑒(,)𝑀) β†’ 𝑑 ∈ ℝ)
17116ffvelcdmda 7029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ℝ)
172171recnd 11116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ β„‚)
173 ax-icn 11043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 i ∈ β„‚
17419ffvelcdmda 7029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ℝ)
175174recnd 11116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ β„‚)
176 mulcl 11068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((i ∈ β„‚ ∧ (π‘”β€˜π‘‘) ∈ β„‚) β†’ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚)
177173, 175, 176sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚)
178 addcl 11066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((π‘“β€˜π‘‘) ∈ β„‚ ∧ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
179172, 177, 178syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
180179anandirs 677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
181170, 180sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
182181adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
183182adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
184169, 183subcld 11445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
185184abscld 15255 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
186181abscld 15255 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ)
187186adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ)
188187adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ)
189185, 188readdcld 11117 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
190189rexrd 11138 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
191184absge0d 15263 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
192180absge0d 15263 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
193170, 192sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
194193adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
195194adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
196185, 188, 191, 195addge0d 11664 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
197 elxrge0 13302 . . . . . . . . . . . . . . . . . . . . . . 23 (((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞) ↔ (((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ* ∧ 0 ≀ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
198190, 196, 197sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞))
199156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ∈ (0[,]+∞))
200198, 199ifclda 4519 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
201200adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
202201fmpttd 7057 . . . . . . . . . . . . . . . . . . 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 1171 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
206166, 205sylan 580 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
207206adantr 481 . . . . . . . . . . . . . . 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 12852 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ*)
209208ad3antlr 729 . . . . . . . . . . . . . . 15 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ 𝑦 ∈ ℝ*)
210158adantlr 713 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
211210adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
212211fmpttd 7057 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞))
213169, 183npcand 11449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) + ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = (πΉβ€˜π‘‘))
214213fveq2d 6841 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜(((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) + ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = (absβ€˜(πΉβ€˜π‘‘)))
215184, 183abstrid 15275 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜(((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) + ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
216214, 215eqbrtrrd 5127 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜(πΉβ€˜π‘‘)) ≀ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
217 iftrue 4490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) = (absβ€˜(πΉβ€˜π‘‘)))
218217adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) = (absβ€˜(πΉβ€˜π‘‘)))
219 iftrue 4490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) = ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
220219adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) = ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
221216, 218, 2203brtr4d 5135 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))
222221ex 413 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
223 0le0 12187 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≀ 0
224223a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ 0 ≀ 0)
225 iffalse 4493 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) = 0)
226 iffalse 4493 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) = 0)
227224, 225, 2263brtr4d 5135 . . . . . . . . . . . . . . . . . . . . . 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 3145 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))
230 reex 11075 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ V
231230a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ℝ ∈ V)
232 fvex 6850 . . . . . . . . . . . . . . . . . . . . . . . 24 (absβ€˜(πΉβ€˜π‘‘)) ∈ V
233 c0ex 11082 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
234232, 233ifex 4534 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ V
235234a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ V)
236 ovex 7382 . . . . . . . . . . . . . . . . . . . . . . . 24 ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ V
237236, 233ifex 4534 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ V
238237a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ V)
239 eqidd 2738 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)))
240 eqidd 2738 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
241231, 235, 238, 239, 240ofrfval2 7628 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
242241ad2antrr 724 . . . . . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . . . . . 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 1371 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))))
2462453adantr3 1171 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) + (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))))
247166, 246sylan 580 . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . 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 36053 . . . . . . . . . . . . . . 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 13007 . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ πœ‘)
252 simpr2 1195 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑀 ∈ (𝐴[,]𝐡))
253 oveq2 7357 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ = 𝑀 β†’ (𝐴(,)π‘₯) = (𝐴(,)𝑀))
254 itgeq1 25059 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴(,)π‘₯) = (𝐴(,)𝑀) β†’ ∫(𝐴(,)π‘₯)(πΉβ€˜π‘‘) d𝑑 = ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
255253, 254syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = 𝑀 β†’ ∫(𝐴(,)π‘₯)(πΉβ€˜π‘‘) d𝑑 = ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
256 itgex 25057 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑 ∈ V
257255, 1, 256fvmpt 6943 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 ∈ (𝐴[,]𝐡) β†’ (πΊβ€˜π‘€) = ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
258252, 257syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (πΊβ€˜π‘€) = ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
2592adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝐴 ∈ ℝ)
260114sselda 3942 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑀 ∈ ℝ)
2612603ad2antr2 1189 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑀 ∈ ℝ)
262114sselda 3942 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝑒 ∈ ℝ)
263262rexrd 11138 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝑒 ∈ ℝ*)
2642633ad2antr1 1188 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑒 ∈ ℝ*)
265 elicc1 13236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*) β†’ (𝑒 ∈ (𝐴[,]𝐡) ↔ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡)))
266132, 133, 265syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑒 ∈ (𝐴[,]𝐡) ↔ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡)))
267266biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡))
268267simp2d 1143 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝐴 ≀ 𝑒)
2692683ad2antr1 1188 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝐴 ≀ 𝑒)
270 simpr3 1196 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑒 ≀ 𝑀)
271132adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝐴 ∈ ℝ*)
272260rexrd 11138 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑀 ∈ ℝ*)
273 elicc1 13236 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℝ* ∧ 𝑀 ∈ ℝ*) β†’ (𝑒 ∈ (𝐴[,]𝑀) ↔ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝑀)))
274271, 272, 273syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑒 ∈ (𝐴[,]𝑀) ↔ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝑀)))
2752743ad2antr2 1189 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑒 ∈ (𝐴[,]𝑀) ↔ (𝑒 ∈ ℝ* ∧ 𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝑀)))
276264, 269, 270, 275mpbir3and 1342 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑒 ∈ (𝐴[,]𝑀))
277 iooss2 13228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐡 ∈ ℝ* ∧ 𝑀 ≀ 𝐡) β†’ (𝐴(,)𝑀) βŠ† (𝐴(,)𝐡))
278133, 141, 277syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴(,)𝑀) βŠ† (𝐴(,)𝐡))
2795adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴(,)𝐡) βŠ† 𝐷)
280278, 279sstrd 3952 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴(,)𝑀) βŠ† 𝐷)
2812803ad2antr2 1189 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝐴(,)𝑀) βŠ† 𝐷)
282281sselda 3942 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝐴(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
283148adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
284282, 283syldan 591 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝐴(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
285 eleq1w 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = 𝑒 β†’ (𝑀 ∈ (𝐴[,]𝐡) ↔ 𝑒 ∈ (𝐴[,]𝐡)))
286285anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 = 𝑒 β†’ ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) ↔ (πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡))))
287 oveq2 7357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 = 𝑒 β†’ (𝐴(,)𝑀) = (𝐴(,)𝑒))
288287mpteq1d 5198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑀 = 𝑒 β†’ (𝑑 ∈ (𝐴(,)𝑀) ↦ (πΉβ€˜π‘‘)) = (𝑑 ∈ (𝐴(,)𝑒) ↦ (πΉβ€˜π‘‘)))
289288eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 = 𝑒 β†’ ((𝑑 ∈ (𝐴(,)𝑀) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1 ↔ (𝑑 ∈ (𝐴(,)𝑒) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1))
290286, 289imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 = 𝑒 β†’ (((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑑 ∈ (𝐴(,)𝑀) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1) ↔ ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ (𝑑 ∈ (𝐴(,)𝑒) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)))
291 ioombl 24851 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝑀) ∈ dom vol
292291a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴(,)𝑀) ∈ dom vol)
293148adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
2948feqmptd 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ 𝐹 = (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)))
295294, 7eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
296295adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
297280, 292, 293, 296iblss 25091 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑑 ∈ (𝐴(,)𝑀) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
298290, 297chvarvv 2002 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ (𝑑 ∈ (𝐴(,)𝑒) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
2992983ad2antr1 1188 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑑 ∈ (𝐴(,)𝑒) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
300 ioombl 24851 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒(,)𝑀) ∈ dom vol
301300a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) ∈ dom vol)
302 fvexd 6852 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ V)
303295adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
304146, 301, 302, 303iblss 25091 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ (𝑒(,)𝑀) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
3053043adantr3 1171 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑑 ∈ (𝑒(,)𝑀) ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
306259, 261, 276, 284, 299, 305itgsplitioo 25124 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ∫(𝐴(,)𝑀)(πΉβ€˜π‘‘) d𝑑 = (∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 + ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑))
307258, 306eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (πΊβ€˜π‘€) = (∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 + ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑))
308 simpr1 1194 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑒 ∈ (𝐴[,]𝐡))
309 oveq2 7357 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ = 𝑒 β†’ (𝐴(,)π‘₯) = (𝐴(,)𝑒))
310 itgeq1 25059 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴(,)π‘₯) = (𝐴(,)𝑒) β†’ ∫(𝐴(,)π‘₯)(πΉβ€˜π‘‘) d𝑑 = ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑)
311309, 310syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = 𝑒 β†’ ∫(𝐴(,)π‘₯)(πΉβ€˜π‘‘) d𝑑 = ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑)
312 itgex 25057 . . . . . . . . . . . . . . . . . . . . . . . 24 ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 ∈ V
313311, 1, 312fvmpt 6943 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ (𝐴[,]𝐡) β†’ (πΊβ€˜π‘’) = ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑)
314308, 313syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (πΊβ€˜π‘’) = ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑)
315307, 314oveq12d 7367 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) = ((∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 + ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) βˆ’ ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑))
316 fvexd 6852 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ 𝑑 ∈ (𝐴(,)𝑒)) β†’ (πΉβ€˜π‘‘) ∈ V)
317316, 298itgcl 25070 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 ∈ β„‚)
318317adantrr 715 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 ∈ β„‚)
319 fvexd 6852 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ V)
320319, 304itgcl 25070 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑 ∈ β„‚)
321318, 320pncan2d 11447 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 + ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) βˆ’ ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑) = ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
3223213adantr3 1171 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑 + ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) βˆ’ ∫(𝐴(,)𝑒)(πΉβ€˜π‘‘) d𝑑) = ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
323315, 322eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) = ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
324323fveq2d 6841 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) = (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑))
325 ftc1anc.t . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ βˆ€π‘  ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)))(absβ€˜βˆ«π‘ (πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0))))
326 df-ov 7352 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒(,)𝑀) = ((,)β€˜βŸ¨π‘’, π‘€βŸ©)
327 opelxpi 5667 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ βŸ¨π‘’, π‘€βŸ© ∈ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)))
328 ioof 13292 . . . . . . . . . . . . . . . . . . . . . . . . 25 (,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ
329 ffn 6663 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ β†’ (,) Fn (ℝ* Γ— ℝ*))
330328, 329ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (,) Fn (ℝ* Γ— ℝ*)
331 iccssxr 13275 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴[,]𝐡) βŠ† ℝ*
332 xpss12 5645 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴[,]𝐡) βŠ† ℝ* ∧ (𝐴[,]𝐡) βŠ† ℝ*) β†’ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)) βŠ† (ℝ* Γ— ℝ*))
333331, 331, 332mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)) βŠ† (ℝ* Γ— ℝ*)
334 fnfvima 7177 . . . . . . . . . . . . . . . . . . . . . . . 24 (((,) Fn (ℝ* Γ— ℝ*) ∧ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)) βŠ† (ℝ* Γ— ℝ*) ∧ βŸ¨π‘’, π‘€βŸ© ∈ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡))) β†’ ((,)β€˜βŸ¨π‘’, π‘€βŸ©) ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡))))
335330, 333, 334mp3an12 1451 . . . . . . . . . . . . . . . . . . . . . . 23 (βŸ¨π‘’, π‘€βŸ© ∈ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)) β†’ ((,)β€˜βŸ¨π‘’, π‘€βŸ©) ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡))))
336327, 335syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ ((,)β€˜βŸ¨π‘’, π‘€βŸ©) ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡))))
337326, 336eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑒(,)𝑀) ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡))))
338 itgeq1 25059 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑒(,)𝑀) β†’ βˆ«π‘ (πΉβ€˜π‘‘) d𝑑 = ∫(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑)
339338fveq2d 6841 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑒(,)𝑀) β†’ (absβ€˜βˆ«π‘ (πΉβ€˜π‘‘) d𝑑) = (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑))
340 eleq2 2826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑒(,)𝑀) β†’ (𝑑 ∈ 𝑠 ↔ 𝑑 ∈ (𝑒(,)𝑀)))
341340ifbid 4507 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑒(,)𝑀) β†’ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0) = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))
342341mpteq2dv 5205 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑒(,)𝑀) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)))
343342fveq2d 6841 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑒(,)𝑀) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0))) = (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
344339, 343breq12d 5116 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑒(,)𝑀) β†’ ((absβ€˜βˆ«π‘ (πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0))) ↔ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)))))
345344rspccva 3578 . . . . . . . . . . . . . . . . . . . . 21 ((βˆ€π‘  ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)))(absβ€˜βˆ«π‘ (πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝑠, (absβ€˜(πΉβ€˜π‘‘)), 0))) ∧ (𝑒(,)𝑀) ∈ ((,) β€œ ((𝐴[,]𝐡) Γ— (𝐴[,]𝐡)))) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
346325, 337, 345syl2an 596 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
3473463adantr3 1171 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
348324, 347eqbrtrd 5125 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
349348adantlr 713 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))))
350 subcl 11333 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πΊβ€˜π‘€) ∈ β„‚ ∧ (πΊβ€˜π‘’) ∈ β„‚) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) ∈ β„‚)
351124, 125, 350syl2anr 597 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ (πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) ∈ β„‚)
352351anandis 676 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) ∈ β„‚)
353352abscld 15255 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ)
354353rexrd 11138 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ*)
3553543adantr3 1171 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ*)
356355adantlr 713 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ*)
357163adantlr 713 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
358208ad2antlr 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ 𝑦 ∈ ℝ*)
359 xrlelttr 13003 . . . . . . . . . . . . . . . . . 18 (((absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ* ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ* ∧ 𝑦 ∈ ℝ*) β†’ (((absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) < 𝑦) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
360356, 357, 358, 359syl3anc 1371 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (((absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) < 𝑦) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
361349, 360mpand 693 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) < 𝑦 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
362251, 361sylanl1 678 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) < 𝑦 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
363362adantr 481 . . . . . . . . . . . . . 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 413 . . . . . . . . . . . 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 11621 . . . . . . . . . . 11 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
367366anassrs 468 . . . . . . . . . 10 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
36892, 367sylanb 581 . . . . . . . . 9 ((((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
369368ralrimiva 3141 . . . . . . . 8 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
370 breq2 5107 . . . . . . . . 9 (𝑧 = ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 ↔ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))))
371370rspceaimv 3583 . . . . . . . 8 ((((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+ ∧ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
37281, 369, 371syl2anc 584 . . . . . . 7 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
373 ralnex 3073 . . . . . . . . 9 (βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) Β¬ π‘Ÿ β‰  0 ↔ Β¬ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0)
374 nne 2945 . . . . . . . . . 10 (Β¬ π‘Ÿ β‰  0 ↔ π‘Ÿ = 0)
375374ralbii 3094 . . . . . . . . 9 (βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) Β¬ π‘Ÿ β‰  0 ↔ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0)
376373, 375bitr3i 276 . . . . . . . 8 (Β¬ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0 ↔ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0)
37716ffnd 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 ∈ dom ∫1 β†’ 𝑓 Fn ℝ)
378 fnfvelrn 7026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓 Fn ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ran 𝑓)
379377, 378sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ran 𝑓)
380 elun1 4134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((π‘“β€˜π‘‘) ∈ ran 𝑓 β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
381379, 380syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
382 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (π‘Ÿ = (π‘“β€˜π‘‘) β†’ (π‘Ÿ = 0 ↔ (π‘“β€˜π‘‘) = 0))
383382rspcva 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (π‘“β€˜π‘‘) = 0)
384381, 383sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (π‘“β€˜π‘‘) = 0)
385384adantllr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (π‘“β€˜π‘‘) = 0)
38619ffnd 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 ∈ dom ∫1 β†’ 𝑔 Fn ℝ)
387 fnfvelrn 7026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔 Fn ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ran 𝑔)
388386, 387sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ran 𝑔)
389 elun2 4135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((π‘”β€˜π‘‘) ∈ ran 𝑔 β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
390388, 389syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
391 eqeq1 2741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (π‘Ÿ = (π‘”β€˜π‘‘) β†’ (π‘Ÿ = 0 ↔ (π‘”β€˜π‘‘) = 0))
392391rspcva 3577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (π‘”β€˜π‘‘) = 0)
393392oveq2d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (i Β· (π‘”β€˜π‘‘)) = (i Β· 0))
394 it0e0 12308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (i Β· 0) = 0
395393, 394eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (i Β· (π‘”β€˜π‘‘)) = 0)
396390, 395sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (i Β· (π‘”β€˜π‘‘)) = 0)
397396adantlll 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (i Β· (π‘”β€˜π‘‘)) = 0)
398385, 397oveq12d 7367 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) = (0 + 0))
399398an32s 650 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) = (0 + 0))
400 00id 11263 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 + 0) = 0
401399, 400eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) = 0)
402401adantlll 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) = 0)
403402oveq2d 7365 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ 0))
404 0cnd 11081 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ Β¬ 𝑑 ∈ 𝐷) β†’ 0 ∈ β„‚)
405148, 404ifclda 4519 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) ∈ β„‚)
406405subid1d 11434 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ 0) = if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))
407406ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ 0) = if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))
408403, 407eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))
409408fveq2d 6841 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = (absβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
410 fvif 6853 . . . . . . . . . . . . . . . . . . . . . 22 (absβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), (absβ€˜0))
411 abs0 15104 . . . . . . . . . . . . . . . . . . . . . . 23 (absβ€˜0) = 0
412 ifeq2 4489 . . . . . . . . . . . . . . . . . . . . . . 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 2765 . . . . . . . . . . . . . . . . . . . . 21 (absβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)
415409, 414eqtrdi 2793 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))
416415mpteq2dva 5203 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
417416fveq2d 6841 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) = (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
418417breq1d 5113 . . . . . . . . . . . . . . . . 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 413 . . . . . . . . . . . . . . 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 419 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2))
423422anasss 467 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2))
424423adantlr 713 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2))
425 1rp 12847 . . . . . . . . . . . . 13 1 ∈ ℝ+
426425ne0ii 4295 . . . . . . . . . . . 12 ℝ+ β‰  βˆ…
427352anassrs 468 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)) ∈ β„‚)
428427abscld 15255 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ)
429428adantlrr 719 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ)
430429adantlr 713 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ)
431 rpre 12851 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ)
432431rehalfcld 12333 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ)
433432adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+) β†’ (𝑦 / 2) ∈ ℝ)
434433ad3antlr 729 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑦 / 2) ∈ ℝ)
435431adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+) β†’ 𝑦 ∈ ℝ)
436435ad3antlr 729 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑦 ∈ ℝ)
437430rexrd 11138 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ∈ ℝ*)
438156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ Β¬ 𝑑 ∈ 𝐷) β†’ 0 ∈ (0[,]+∞))
439153, 438ifclda 4519 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
440439adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ (0[,]+∞))
441440fmpttd 7057 . . . . . . . . . . . . . . . . . . 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 728 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
445434rexrd 11138 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑦 / 2) ∈ ℝ*)
446108, 107oveqan12rd 7369 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 = 𝑒 ∧ π‘Ž = 𝑀) β†’ ((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘)) = ((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’)))
447446fveq2d 6841 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 = 𝑒 ∧ π‘Ž = 𝑀) β†’ (absβ€˜((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘))) = (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))))
448447breq1d 5113 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑒 ∧ π‘Ž = 𝑀) β†’ ((absβ€˜((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ↔ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))))
44998, 97oveqan12rd 7369 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 = 𝑀 ∧ π‘Ž = 𝑒) β†’ ((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘)) = ((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€)))
450449fveq2d 6841 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 = 𝑀 ∧ π‘Ž = 𝑒) β†’ (absβ€˜((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘))) = (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))))
451450breq1d 5113 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑀 ∧ π‘Ž = 𝑒) β†’ ((absβ€˜((πΊβ€˜π‘Ž) βˆ’ (πΊβ€˜π‘))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ↔ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))))
452128breq1d 5113 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ↔ (absβ€˜((πΊβ€˜π‘’) βˆ’ (πΊβ€˜π‘€))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))))
453320abscld 15255 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ∈ ℝ)
454453rexrd 11138 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ∈ ℝ*)
455443adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) ∈ ℝ*)
456441adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)):β„βŸΆ(0[,]+∞))
457 breq2 5107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((absβ€˜(πΉβ€˜π‘‘)) = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) β†’ (if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘)) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
458 breq2 5107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 = if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) β†’ (if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ 0 ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
459149leidd 11654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(πΉβ€˜π‘‘)) ≀ (absβ€˜(πΉβ€˜π‘‘)))
460 breq1 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((absβ€˜(πΉβ€˜π‘‘)) = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) β†’ ((absβ€˜(πΉβ€˜π‘‘)) ≀ (absβ€˜(πΉβ€˜π‘‘)) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘))))
461 breq1 5106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0 = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) β†’ (0 ≀ (absβ€˜(πΉβ€˜π‘‘)) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘))))
462460, 461ifboth 4523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((absβ€˜(πΉβ€˜π‘‘)) ≀ (absβ€˜(πΉβ€˜π‘‘)) ∧ 0 ≀ (absβ€˜(πΉβ€˜π‘‘))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘)))
463459, 151, 462syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘)))
464463adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ (absβ€˜(πΉβ€˜π‘‘)))
465146ssneld 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (Β¬ 𝑑 ∈ 𝐷 β†’ Β¬ 𝑑 ∈ (𝑒(,)𝑀)))
466465imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ Β¬ 𝑑 ∈ 𝐷) β†’ Β¬ 𝑑 ∈ (𝑒(,)𝑀))
467225, 223eqbrtrdi 5142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ 0)
468466, 467syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ Β¬ 𝑑 ∈ 𝐷) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ 0)
469457, 458, 464, 468ifbothda 4522 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))
470469ralrimivw 3145 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))
471232, 233ifex 4534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ V
472471a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0) ∈ V)
473 eqidd 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
474231, 235, 472, 239, 473ofrfval2 7628 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
475474adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0) ≀ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0)))
476470, 475mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . 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 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜(πΉβ€˜π‘‘)), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
479454, 162, 455, 346, 478xrletrd 13009 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
4804793adantr3 1171 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜βˆ«(𝑒(,)𝑀)(πΉβ€˜π‘‘) d𝑑) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
481324, 480eqbrtrd 5125 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
482448, 451, 114, 452, 481wlogle 11621 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
483482anassrs 468 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
484483adantlrr 719 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
485484adantlr 713 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))))
486 simplr 767 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2))
487437, 444, 445, 485, 486xrlelttrd 13007 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < (𝑦 / 2))
488 rphalflt 12872 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) < 𝑦)
489488adantl 482 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+) β†’ (𝑦 / 2) < 𝑦)
490489ad3antlr 729 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝑦 / 2) < 𝑦)
491430, 434, 436, 487, 490lttrd 11249 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)
492491a1d 25 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ ((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
493492ralrimiva 3141 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) β†’ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
494493ralrimivw 3145 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) β†’ βˆ€π‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
495 r19.2z 4450 . . . . . . . . . . . 12 ((ℝ+ β‰  βˆ… ∧ βˆ€π‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
496426, 494, 495sylancr 587 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ 𝐷, (absβ€˜(πΉβ€˜π‘‘)), 0))) < (𝑦 / 2)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
497424, 496syldan 591 . . . . . . . . . 10 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0))) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
498497anassrs 468 . . . . . . . . 9 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
499498anassrs 468 . . . . . . . 8 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆ€π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ = 0) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
500376, 499sylan2b 594 . . . . . . 7 (((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ Β¬ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
501372, 500pm2.61dan 811 . . . . . 6 ((((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
502501ex 413 . . . . 5 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)))
503502rexlimdvva 3203 . . . 4 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) β†’ (βˆƒπ‘“ ∈ dom ∫1βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦)))
50413, 503mpd 15 . . 3 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ ℝ+)) β†’ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
505504ralrimivva 3195 . 2 (πœ‘ β†’ βˆ€π‘’ ∈ (𝐴[,]𝐡)βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))
506 ssid 3964 . . 3 β„‚ βŠ† β„‚
507 elcncf2 24175 . . 3 (((𝐴[,]𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (𝐺 ∈ ((𝐴[,]𝐡)–cnβ†’β„‚) ↔ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ βˆ€π‘’ ∈ (𝐴[,]𝐡)βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))))
508117, 506, 507sylancl 586 . 2 (πœ‘ β†’ (𝐺 ∈ ((𝐴[,]𝐡)–cnβ†’β„‚) ↔ (𝐺:(𝐴[,]𝐡)βŸΆβ„‚ ∧ βˆ€π‘’ ∈ (𝐴[,]𝐡)βˆ€π‘¦ ∈ ℝ+ βˆƒπ‘§ ∈ ℝ+ βˆ€π‘€ ∈ (𝐴[,]𝐡)((absβ€˜(𝑀 βˆ’ 𝑒)) < 𝑧 β†’ (absβ€˜((πΊβ€˜π‘€) βˆ’ (πΊβ€˜π‘’))) < 𝑦))))
5099, 505, 508mpbir2and 711 1 (πœ‘ β†’ 𝐺 ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3443   βˆͺ cun 3906   βŠ† wss 3908  βˆ…c0 4280  ifcif 4484  π’« cpw 4558  βŸ¨cop 4590   class class class wbr 5103   ↦ cmpt 5186   Γ— cxp 5628  dom cdm 5630  ran crn 5631   β€œ cima 5633  Fun wfun 6485   Fn wfn 6486  βŸΆwf 6487  β€˜cfv 6491  (class class class)co 7349   ∘r cofr 7606  Fincfn 8816  supcsup 9309  β„‚cc 10982  β„cr 10983  0cc0 10984  1c1 10985  ici 10986   + caddc 10987   Β· cmul 10989  +∞cpnf 11119  β„*cxr 11121   < clt 11122   ≀ cle 11123   βˆ’ cmin 11318   / cdiv 11745  2c2 12141  β„+crp 12843  (,)cioo 13192  [,]cicc 13195  abscabs 15052  β€“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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7662  ax-inf2 9510  ax-cnex 11040  ax-resscn 11041  ax-1cn 11042  ax-icn 11043  ax-addcl 11044  ax-addrcl 11045  ax-mulcl 11046  ax-mulrcl 11047  ax-mulcom 11048  ax-addass 11049  ax-mulass 11050  ax-distr 11051  ax-i2m1 11052  ax-1ne0 11053  ax-1rid 11054  ax-rnegex 11055  ax-rrecex 11056  ax-cnre 11057  ax-pre-lttri 11058  ax-pre-lttrn 11059  ax-pre-ltadd 11060  ax-pre-mulgt0 11061  ax-pre-sup 11062  ax-addf 11063
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-symdif 4200  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-disj 5069  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5528  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5585  df-se 5586  df-we 5587  df-xp 5636  df-rel 5637  df-cnv 5638  df-co 5639  df-dm 5640  df-rn 5641  df-res 5642  df-ima 5643  df-pred 6249  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6443  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-isom 6500  df-riota 7305  df-ov 7352  df-oprab 7353  df-mpo 7354  df-of 7607  df-ofr 7608  df-om 7793  df-1st 7911  df-2nd 7912  df-frecs 8179  df-wrecs 8210  df-recs 8284  df-rdg 8323  df-1o 8379  df-2o 8380  df-er 8581  df-map 8700  df-pm 8701  df-en 8817  df-dom 8818  df-sdom 8819  df-fin 8820  df-fi 9280  df-sup 9311  df-inf 9312  df-oi 9379  df-dju 9770  df-card 9808  df-pnf 11124  df-mnf 11125  df-xr 11126  df-ltxr 11127  df-le 11128  df-sub 11320  df-neg 11321  df-div 11746  df-nn 12087  df-2 12149  df-3 12150  df-4 12151  df-n0 12347  df-z 12433  df-uz 12696  df-q 12802  df-rp 12844  df-xneg 12961  df-xadd 12962  df-xmul 12963  df-ioo 13196  df-ico 13198  df-icc 13199  df-fz 13353  df-fzo 13496  df-fl 13625  df-mod 13703  df-seq 13835  df-exp 13896  df-hash 14158  df-cj 14917  df-re 14918  df-im 14919  df-sqrt 15053  df-abs 15054  df-clim 15304  df-rlim 15305  df-sum 15505  df-rest 17238  df-topgen 17259  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  36055
  Copyright terms: Public domain W3C validator