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 33799
Description: ftc1a 24008 holds for functions that obey the triangle inequality in the absence of ax-cc 9536. 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 24007 . 2 (𝜑𝐺:(𝐴[,]𝐵)⟶ℂ)
10 rphalfcl 12066 . . . . . 6 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
111, 2, 3, 4, 5, 6, 7, 8ftc1anclem6 33796 . . . . . 6 ((𝜑 ∧ (𝑦 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
1210, 11sylan2 582 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
1312adantrl 698 . . . 4 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
1410ad2antll 711 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / 2) ∈ ℝ+)
15 2rp 12045 . . . . . . . . . . . 12 2 ∈ ℝ+
16 i1ff 23651 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
1716frnd 6257 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
1817adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ran 𝑓 ⊆ ℝ)
19 i1ff 23651 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
2019frnd 6257 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ)
2120adantl 469 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ran 𝑔 ⊆ ℝ)
2218, 21unssd 3982 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ)
23 ax-resscn 10272 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℂ
2422, 23syl6ss 3804 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ)
25 i1f0rn 23657 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓)
26 elun1 3973 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ran 𝑓 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
2725, 26syl 17 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
2827adantr 468 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
29 absf 14294 . . . . . . . . . . . . . . . . . . 19 abs:ℂ⟶ℝ
30 ffn 6250 . . . . . . . . . . . . . . . . . . 19 (abs:ℂ⟶ℝ → abs Fn ℂ)
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . . 18 abs Fn ℂ
32 fnfvima 6715 . . . . . . . . . . . . . . . . . 18 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
3331, 32mp3an1 1565 . . . . . . . . . . . . . . . . 17 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
3424, 28, 33syl2anc 575 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
3534ne0d 4117 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅)
36 imassrn 5681 . . . . . . . . . . . . . . . . 17 (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ran abs
37 frn 6256 . . . . . . . . . . . . . . . . . 18 (abs:ℂ⟶ℝ → ran abs ⊆ ℝ)
3829, 37ax-mp 5 . . . . . . . . . . . . . . . . 17 ran abs ⊆ ℝ
3936, 38sstri 3801 . . . . . . . . . . . . . . . 16 (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ
40 ffun 6253 . . . . . . . . . . . . . . . . . 18 (abs:ℂ⟶ℝ → Fun abs)
4129, 40ax-mp 5 . . . . . . . . . . . . . . . . 17 Fun abs
42 i1frn 23652 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
43 i1frn 23652 . . . . . . . . . . . . . . . . . 18 (𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin)
44 unfi 8460 . . . . . . . . . . . . . . . . . 18 ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
4542, 43, 44syl2an 585 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
46 imafi 8492 . . . . . . . . . . . . . . . . 17 ((Fun abs ∧ (ran 𝑓 ∪ ran 𝑔) ∈ Fin) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
4741, 45, 46sylancr 577 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
48 fimaxre2 11248 . . . . . . . . . . . . . . . 16 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥)
4939, 47, 48sylancr 577 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥)
50 suprcl 11262 . . . . . . . . . . . . . . . 16 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
5139, 50mp3an1 1565 . . . . . . . . . . . . . . 15 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
5235, 49, 51syl2anc 575 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
5352adantr 468 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
54 0red 10322 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈ ℝ)
5524sselda 3792 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → 𝑟 ∈ ℂ)
5655abscld 14392 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ ℝ)
5756adantrr 699 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈ ℝ)
5852adantr 468 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
59 absgt0 14281 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℂ → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
6055, 59syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
6160biimpd 220 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 → 0 < (abs‘𝑟)))
6261impr 444 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < (abs‘𝑟))
6339a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ)
6463, 35, 493jca 1151 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
6564adantr 468 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
66 fnfvima 6715 . . . . . . . . . . . . . . . . . . . 20 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
6731, 66mp3an1 1565 . . . . . . . . . . . . . . . . . . 19 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
6824, 67sylan 571 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
69 suprub 11263 . . . . . . . . . . . . . . . . . 18 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7065, 68, 69syl2anc 575 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7170adantrr 699 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7254, 57, 58, 62, 71ltletrd 10476 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7372rexlimdvaa 3216 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
7473imp 395 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7553, 74elrpd 12077 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+)
76 rpmulcl 12063 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
7715, 75, 76sylancr 577 . . . . . . . . . . 11 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
78 rpdivcl 12064 . . . . . . . . . . 11 (((𝑦 / 2) ∈ ℝ+ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
7914, 77, 78syl2an 585 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
8079anassrs 455 . . . . . . . . 9 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
8180adantlr 697 . . . . . . . 8 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
82 ancom 450 . . . . . . . . . . . 12 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) ↔ (𝑦 ∈ ℝ+𝑢 ∈ (𝐴[,]𝐵)))
8382anbi2i 611 . . . . . . . . . . 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 628 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ↔ ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
8584anbi1i 612 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)))
86 an32 628 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
8785, 86bitri 266 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
8887anbi1i 612 . . . . . . . . . . . 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 628 . . . . . . . . . . . 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 266 . . . . . . . . . . 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 456 . . . . . . . . . . 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 294 . . . . . . . . . 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 6877 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑤𝑎 = 𝑢) → (𝑏𝑎) = (𝑤𝑢))
9493ancoms 448 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑢𝑏 = 𝑤) → (𝑏𝑎) = (𝑤𝑢))
9594fveq2d 6406 . . . . . . . . . . . . . 14 ((𝑎 = 𝑢𝑏 = 𝑤) → (abs‘(𝑏𝑎)) = (abs‘(𝑤𝑢)))
9695breq1d 4847 . . . . . . . . . . . . 13 ((𝑎 = 𝑢𝑏 = 𝑤) → ((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
97 fveq2 6402 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑤 → (𝐺𝑏) = (𝐺𝑤))
98 fveq2 6402 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑢 → (𝐺𝑎) = (𝐺𝑢))
9997, 98oveqan12rd 6888 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑢𝑏 = 𝑤) → ((𝐺𝑏) − (𝐺𝑎)) = ((𝐺𝑤) − (𝐺𝑢)))
10099fveq2d 6406 . . . . . . . . . . . . . 14 ((𝑎 = 𝑢𝑏 = 𝑤) → (abs‘((𝐺𝑏) − (𝐺𝑎))) = (abs‘((𝐺𝑤) − (𝐺𝑢))))
101100breq1d 4847 . . . . . . . . . . . . 13 ((𝑎 = 𝑢𝑏 = 𝑤) → ((abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦 ↔ (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
10296, 101imbi12d 335 . . . . . . . . . . . 12 ((𝑎 = 𝑢𝑏 = 𝑤) → (((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦) ↔ ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)))
103 oveq12 6877 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑢𝑎 = 𝑤) → (𝑏𝑎) = (𝑢𝑤))
104103ancoms 448 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑤𝑏 = 𝑢) → (𝑏𝑎) = (𝑢𝑤))
105104fveq2d 6406 . . . . . . . . . . . . . 14 ((𝑎 = 𝑤𝑏 = 𝑢) → (abs‘(𝑏𝑎)) = (abs‘(𝑢𝑤)))
106105breq1d 4847 . . . . . . . . . . . . 13 ((𝑎 = 𝑤𝑏 = 𝑢) → ((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
107 fveq2 6402 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑢 → (𝐺𝑏) = (𝐺𝑢))
108 fveq2 6402 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → (𝐺𝑎) = (𝐺𝑤))
109107, 108oveqan12rd 6888 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑤𝑏 = 𝑢) → ((𝐺𝑏) − (𝐺𝑎)) = ((𝐺𝑢) − (𝐺𝑤)))
110109fveq2d 6406 . . . . . . . . . . . . . 14 ((𝑎 = 𝑤𝑏 = 𝑢) → (abs‘((𝐺𝑏) − (𝐺𝑎))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
111110breq1d 4847 . . . . . . . . . . . . 13 ((𝑎 = 𝑤𝑏 = 𝑢) → ((abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦 ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦))
112106, 111imbi12d 335 . . . . . . . . . . . 12 ((𝑎 = 𝑤𝑏 = 𝑢) → (((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦) ↔ ((abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦)))
113 iccssre 12467 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
1142, 3, 113syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
115114ad4antr 715 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝐴[,]𝐵) ⊆ ℝ)
116 simp-4l 792 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑)
117114, 23syl6ss 3804 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
118117sselda 3792 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ)
119117sselda 3792 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ)
120 abssub 14283 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (abs‘(𝑤𝑢)) = (abs‘(𝑢𝑤)))
121118, 119, 120syl2anr 586 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤𝑢)) = (abs‘(𝑢𝑤)))
122121anandis 660 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤𝑢)) = (abs‘(𝑢𝑤)))
123122breq1d 4847 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
1249ffvelrnda 6575 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐺𝑤) ∈ ℂ)
1259ffvelrnda 6575 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝐺𝑢) ∈ ℂ)
126 abssub 14283 . . . . . . . . . . . . . . . . 17 (((𝐺𝑤) ∈ ℂ ∧ (𝐺𝑢) ∈ ℂ) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
127124, 125, 126syl2anr 586 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
128127anandis 660 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
129128breq1d 4847 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦 ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦))
130123, 129imbi12d 335 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦) ↔ ((abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦)))
131116, 130sylan 571 . . . . . . . . . . . 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 10368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐴 ∈ ℝ*)
1333rexrd 10368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐵 ∈ ℝ*)
134132, 133jca 503 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
135 df-icc 12394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥𝑡𝑡𝑦)})
136135elixx3g 12400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑢 ∈ ℝ*) ∧ (𝐴𝑢𝑢𝐵)))
137136simprbi 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 ∈ (𝐴[,]𝐵) → (𝐴𝑢𝑢𝐵))
138137simpld 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 ∈ (𝐴[,]𝐵) → 𝐴𝑢)
139135elixx3g 12400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝐴𝑤𝑤𝐵)))
140139simprbi 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ (𝐴[,]𝐵) → (𝐴𝑤𝑤𝐵))
141140simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ (𝐴[,]𝐵) → 𝑤𝐵)
142138, 141anim12i 602 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴𝑢𝑤𝐵))
143 ioossioo 12478 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑢𝑤𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
144134, 142, 143syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
1455adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
146144, 145sstrd 3802 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
147146sselda 3792 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡𝐷)
1488ffvelrnda 6575 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
149148abscld 14392 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ ℝ)
150149rexrd 10368 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ ℝ*)
151148absge0d 14400 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡𝐷) → 0 ≤ (abs‘(𝐹𝑡)))
152 elxrge0 12495 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((abs‘(𝐹𝑡)) ∈ (0[,]+∞) ↔ ((abs‘(𝐹𝑡)) ∈ ℝ* ∧ 0 ≤ (abs‘(𝐹𝑡))))
153150, 151, 152sylanbrc 574 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ (0[,]+∞))
154153adantlr 697 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ (0[,]+∞))
155147, 154syldan 581 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹𝑡)) ∈ (0[,]+∞))
156 0e0iccpnf 12497 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ (0[,]+∞)
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
158155, 157ifclda 4307 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
159158adantr 468 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
160159fmpttd 6601 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
161 itg2cl 23707 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
162160, 161syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
1631623adantr3 1205 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
164116, 163sylan 571 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
165164adantr 468 . . . . . . . . . . . . . . 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 782 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)))
167148adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
168147, 167syldan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
169168adantllr 701 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
170 elioore 12417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
17116ffvelrnda 6575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℝ)
172171recnd 10347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℂ)
173 ax-icn 10274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 i ∈ ℂ
17419ffvelrnda 6575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℝ)
175174recnd 10347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℂ)
176 mulcl 10299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((i ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (i · (𝑔𝑡)) ∈ ℂ)
177173, 175, 176sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (i · (𝑔𝑡)) ∈ ℂ)
178 addcl 10297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
179172, 177, 178syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
180179anandirs 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
181170, 180sylan2 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
182181adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
183182adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
184169, 183subcld 10671 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
185184abscld 14392 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
186181abscld 14392 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
187186adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
188187adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
189185, 188readdcld 10348 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
190189rexrd 10368 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
191184absge0d 14400 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
192180absge0d 14400 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
193170, 192sylan2 582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
194193adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
195194adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
196185, 188, 191, 195addge0d 10882 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
197 elxrge0 12495 . . . . . . . . . . . . . . . . . . . . . . 23 (((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞) ↔ (((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ* ∧ 0 ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))))
198190, 196, 197sylanbrc 574 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞))
199156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
200198, 199ifclda 4307 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
201200adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
202201fmpttd 6601 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞))
203 itg2cl 23707 . . . . . . . . . . . . . . . . . . 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 1205 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
206166, 205sylan 571 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
207206adantr 468 . . . . . . . . . . . . . . 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 12048 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+𝑦 ∈ ℝ*)
209208ad3antlr 713 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → 𝑦 ∈ ℝ*)
210158adantlr 697 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
211210adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
212211fmpttd 6601 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
213169, 183npcand 10675 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) + ((𝑓𝑡) + (i · (𝑔𝑡)))) = (𝐹𝑡))
214213fveq2d 6406 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) + ((𝑓𝑡) + (i · (𝑔𝑡))))) = (abs‘(𝐹𝑡)))
215184, 183abstrid 14412 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) + ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
216214, 215eqbrtrrd 4861 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹𝑡)) ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
217 iftrue 4279 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) = (abs‘(𝐹𝑡)))
218217adantl 469 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) = (abs‘(𝐹𝑡)))
219 iftrue 4279 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) = ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
220219adantl 469 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) = ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
221216, 218, 2203brtr4d 4869 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
222221ex 399 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
223 0le0 11387 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 0
224223a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0)
225 iffalse 4282 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) = 0)
226 iffalse 4282 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) = 0)
227224, 225, 2263brtr4d 4869 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
228222, 227pm2.61d1 172 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
229228ralrimivw 3151 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
230 reex 10306 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ V
231230a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ℝ ∈ V)
232 fvex 6415 . . . . . . . . . . . . . . . . . . . . . . . 24 (abs‘(𝐹𝑡)) ∈ V
233 c0ex 10313 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
234232, 233ifex 4321 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ V
235234a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ V)
236 ovex 6900 . . . . . . . . . . . . . . . . . . . . . . . 24 ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ V
237236, 233ifex 4321 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ V
238237a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ V)
239 eqidd 2803 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)))
240 eqidd 2803 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
241231, 235, 238, 239, 240ofrfval2 7139 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
242241ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
243229, 242mpbird 248 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
244 itg2le 23714 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))))
245212, 202, 243, 244syl3anc 1483 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))))
2462453adantr3 1205 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))))
247166, 246sylan 571 . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . 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 33798 . . . . . . . . . . . . . . 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 12203 . . . . . . . . . . . . . 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 782 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 𝜑)
252 simpr2 1243 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑤 ∈ (𝐴[,]𝐵))
253 oveq2 6876 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑤 → (𝐴(,)𝑥) = (𝐴(,)𝑤))
254 itgeq1 23747 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴(,)𝑥) = (𝐴(,)𝑤) → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
255253, 254syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
256 itgex 23745 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡 ∈ V
257255, 1, 256fvmpt 6497 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ (𝐴[,]𝐵) → (𝐺𝑤) = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
258252, 257syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐺𝑤) = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
2592adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝐴 ∈ ℝ)
260114sselda 3792 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ)
2612603ad2antr2 1233 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑤 ∈ ℝ)
262114sselda 3792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ)
263262rexrd 10368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ*)
2642633ad2antr1 1232 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢 ∈ ℝ*)
265 elicc1 12431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵)))
266132, 133, 265syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵)))
267266biimpa 464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵))
268267simp2d 1166 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝐴𝑢)
2692683ad2antr1 1232 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝐴𝑢)
270 simpr3 1245 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢𝑤)
271132adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ*)
272260rexrd 10368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ*)
273 elicc1 12431 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℝ*𝑤 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤)))
274271, 272, 273syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤)))
2752743ad2antr2 1233 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤)))
276264, 269, 270, 275mpbir3and 1435 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢 ∈ (𝐴[,]𝑤))
277 iooss2 12423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐵 ∈ ℝ*𝑤𝐵) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
278133, 141, 277syl2an 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
2795adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝐵) ⊆ 𝐷)
280278, 279sstrd 3802 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ 𝐷)
2812803ad2antr2 1233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐴(,)𝑤) ⊆ 𝐷)
282281sselda 3792 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → 𝑡𝐷)
283148adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
284282, 283syldan 581 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
285 eleq1w 2864 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑢 → (𝑤 ∈ (𝐴[,]𝐵) ↔ 𝑢 ∈ (𝐴[,]𝐵)))
286285anbi2d 616 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑢 → ((𝜑𝑤 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑢 ∈ (𝐴[,]𝐵))))
287 oveq2 6876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑢 → (𝐴(,)𝑤) = (𝐴(,)𝑢))
288287mpteq1d 4925 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑢 → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) = (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)))
289288eleq1d 2866 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑢 → ((𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1 ↔ (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1))
290286, 289imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑢 → (((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1) ↔ ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1)))
291 ioombl 23540 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝑤) ∈ dom vol
292291a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ∈ dom vol)
293148adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑤 ∈ (𝐴[,]𝐵)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
2948feqmptd 6464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐹 = (𝑡𝐷 ↦ (𝐹𝑡)))
295294, 7eqeltrrd 2882 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
296295adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
297280, 292, 293, 296iblss 23779 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1)
298290, 297chvarv 2436 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1)
2992983ad2antr1 1232 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1)
300 ioombl 23540 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢(,)𝑤) ∈ dom vol
301300a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ∈ dom vol)
302 fvexd 6417 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ V)
303295adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
304146, 301, 302, 303iblss 23779 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1)
3053043adantr3 1205 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1)
306259, 261, 276, 284, 299, 305itgsplitioo 23812 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡 = (∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
307258, 306eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐺𝑤) = (∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
308 simpr1 1241 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢 ∈ (𝐴[,]𝐵))
309 oveq2 6876 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑢 → (𝐴(,)𝑥) = (𝐴(,)𝑢))
310 itgeq1 23747 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴(,)𝑥) = (𝐴(,)𝑢) → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
311309, 310syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑢 → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
312 itgex 23745 . . . . . . . . . . . . . . . . . . . . . . . 24 ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 ∈ V
313311, 1, 312fvmpt 6497 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ (𝐴[,]𝐵) → (𝐺𝑢) = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
314308, 313syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐺𝑢) = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
315307, 314oveq12d 6886 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((𝐺𝑤) − (𝐺𝑢)) = ((∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡))
316 fvexd 6417 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑢)) → (𝐹𝑡) ∈ V)
317316, 298itgcl 23758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 ∈ ℂ)
318317adantrr 699 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 ∈ ℂ)
319 fvexd 6417 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ V)
320319, 304itgcl 23758 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡 ∈ ℂ)
321318, 320pncan2d 10673 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
3223213adantr3 1205 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
323315, 322eqtrd 2836 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((𝐺𝑤) − (𝐺𝑢)) = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
324323fveq2d 6406 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
325 ftc1anc.t . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))))
326 df-ov 6871 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢(,)𝑤) = ((,)‘⟨𝑢, 𝑤⟩)
327 opelxpi 5342 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))
328 ioof 12484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
329 ffn 6250 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
330328, 329ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (,) Fn (ℝ* × ℝ*)
331 iccssxr 12468 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴[,]𝐵) ⊆ ℝ*
332 xpss12 5320 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴[,]𝐵) ⊆ ℝ* ∧ (𝐴[,]𝐵) ⊆ ℝ*) → ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*))
333331, 331, 332mp2an 675 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*)
334 fnfvima 6715 . . . . . . . . . . . . . . . . . . . . . . . 24 (((,) Fn (ℝ* × ℝ*) ∧ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*) ∧ ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
335330, 333, 334mp3an12 1568 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
336327, 335syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
337326, 336syl5eqel 2885 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
338 itgeq1 23747 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑢(,)𝑤) → ∫𝑠(𝐹𝑡) d𝑡 = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
339338fveq2d 6406 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑢(,)𝑤) → (abs‘∫𝑠(𝐹𝑡) d𝑡) = (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
340 eleq2 2870 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑢(,)𝑤) → (𝑡𝑠𝑡 ∈ (𝑢(,)𝑤)))
341340ifbid 4295 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑢(,)𝑤) → if(𝑡𝑠, (abs‘(𝐹𝑡)), 0) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))
342341mpteq2dv 4932 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)))
343342fveq2d 6406 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑢(,)𝑤) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
344339, 343breq12d 4850 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑢(,)𝑤) → ((abs‘∫𝑠(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)))))
345344rspccva 3497 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))) ∧ (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
346325, 337, 345syl2an 585 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
3473463adantr3 1205 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
348324, 347eqbrtrd 4859 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
349348adantlr 697 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
350 subcl 10559 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺𝑤) ∈ ℂ ∧ (𝐺𝑢) ∈ ℂ) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
351124, 125, 350syl2anr 586 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
352351anandis 660 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
353352abscld 14392 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
354353rexrd 10368 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
3553543adantr3 1205 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
356355adantlr 697 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
357163adantlr 697 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
358208ad2antlr 709 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑦 ∈ ℝ*)
359 xrlelttr 12199 . . . . . . . . . . . . . . . . . 18 (((abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ* ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*𝑦 ∈ ℝ*) → (((abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
360356, 357, 358, 359syl3anc 1483 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (((abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
361349, 360mpand 678 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
362251, 361sylanl1 662 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
363362adantr 468 . . . . . . . . . . . . . 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 399 . . . . . . . . . . . 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 10840 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
367366anassrs 455 . . . . . . . . . 10 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
36892, 367sylanb 572 . . . . . . . . 9 ((((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
369368ralrimiva 3150 . . . . . . . 8 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
370 breq2 4841 . . . . . . . . 9 (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → ((abs‘(𝑤𝑢)) < 𝑧 ↔ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
371370rspceaimv 3506 . . . . . . . 8 ((((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
37281, 369, 371syl2anc 575 . . . . . . 7 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
373 ralnex 3176 . . . . . . . . 9 (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)
374 nne 2978 . . . . . . . . . 10 𝑟 ≠ 0 ↔ 𝑟 = 0)
375374ralbii 3164 . . . . . . . . 9 (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
376373, 375bitr3i 268 . . . . . . . 8 (¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
37716ffnd 6251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 ∈ dom ∫1𝑓 Fn ℝ)
378 fnfvelrn 6572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ran 𝑓)
379377, 378sylan 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ran 𝑓)
380 elun1 3973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑡) ∈ ran 𝑓 → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
381379, 380syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
382 eqeq1 2806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑓𝑡) → (𝑟 = 0 ↔ (𝑓𝑡) = 0))
383382rspcva 3496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓𝑡) = 0)
384381, 383sylan 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓𝑡) = 0)
385384adantllr 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓𝑡) = 0)
38619ffnd 6251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 ∈ dom ∫1𝑔 Fn ℝ)
387 fnfvelrn 6572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ran 𝑔)
388386, 387sylan 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ran 𝑔)
389 elun2 3974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔𝑡) ∈ ran 𝑔 → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
390388, 389syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
391 eqeq1 2806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑔𝑡) → (𝑟 = 0 ↔ (𝑔𝑡) = 0))
392391rspcva 3496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑔𝑡) = 0)
393392oveq2d 6884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = (i · 0))
394 it0e0 11515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (i · 0) = 0
395393, 394syl6eq 2852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = 0)
396390, 395sylan 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = 0)
397396adantlll 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = 0)
398385, 397oveq12d 6886 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((𝑓𝑡) + (i · (𝑔𝑡))) = (0 + 0))
399398an32s 634 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) = (0 + 0))
400 00id 10490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 + 0) = 0
401399, 400syl6eq 2852 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) = 0)
402401adantlll 700 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) = 0)
403402oveq2d 6884 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (if(𝑡𝐷, (𝐹𝑡), 0) − 0))
404 0cnd 10312 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ ℂ)
405148, 404ifclda 4307 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
406405subid1d 10660 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (if(𝑡𝐷, (𝐹𝑡), 0) − 0) = if(𝑡𝐷, (𝐹𝑡), 0))
407406ad3antrrr 712 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − 0) = if(𝑡𝐷, (𝐹𝑡), 0))
408403, 407eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = if(𝑡𝐷, (𝐹𝑡), 0))
409408fveq2d 6406 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = (abs‘if(𝑡𝐷, (𝐹𝑡), 0)))
410 fvif 6418 . . . . . . . . . . . . . . . . . . . . . 22 (abs‘if(𝑡𝐷, (𝐹𝑡), 0)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), (abs‘0))
411 abs0 14242 . . . . . . . . . . . . . . . . . . . . . . 23 (abs‘0) = 0
412 ifeq2 4278 . . . . . . . . . . . . . . . . . . . . . . 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 2824 . . . . . . . . . . . . . . . . . . . . 21 (abs‘if(𝑡𝐷, (𝐹𝑡), 0)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)
415409, 414syl6eq 2852 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))
416415mpteq2dva 4931 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
417416fveq2d 6406 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
418417breq1d 4847 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)))
419418biimpd 220 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)))
420419ex 399 . . . . . . . . . . . . . . 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 407 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
423422anasss 454 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
424423adantlr 697 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
425 1rp 12044 . . . . . . . . . . . . 13 1 ∈ ℝ+
426425ne0ii 4119 . . . . . . . . . . . 12 + ≠ ∅
427352anassrs 455 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
428427abscld 14392 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
429428adantlrr 703 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
430429adantlr 697 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
431 rpre 12047 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
432431rehalfcld 11540 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
433432adantl 469 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
434433ad3antlr 713 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ)
435431adantl 469 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
436435ad3antlr 713 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ)
437430rexrd 10368 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
438156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ (0[,]+∞))
439153, 438ifclda 4307 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
440439adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ ℝ) → if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
441440fmpttd 6601 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
442 itg2cl 23707 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
443441, 442syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
444443ad3antrrr 712 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
445434rexrd 10368 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ*)
446108, 107oveqan12rd 6888 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 = 𝑢𝑎 = 𝑤) → ((𝐺𝑎) − (𝐺𝑏)) = ((𝐺𝑤) − (𝐺𝑢)))
447446fveq2d 6406 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 = 𝑢𝑎 = 𝑤) → (abs‘((𝐺𝑎) − (𝐺𝑏))) = (abs‘((𝐺𝑤) − (𝐺𝑢))))
448447breq1d 4847 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑢𝑎 = 𝑤) → ((abs‘((𝐺𝑎) − (𝐺𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))))
44998, 97oveqan12rd 6888 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 = 𝑤𝑎 = 𝑢) → ((𝐺𝑎) − (𝐺𝑏)) = ((𝐺𝑢) − (𝐺𝑤)))
450449fveq2d 6406 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 = 𝑤𝑎 = 𝑢) → (abs‘((𝐺𝑎) − (𝐺𝑏))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
451450breq1d 4847 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑤𝑎 = 𝑢) → ((abs‘((𝐺𝑎) − (𝐺𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))))
452128breq1d 4847 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))))
453320abscld 14392 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ∈ ℝ)
454453rexrd 10368 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ∈ ℝ*)
455443adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
456441adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
457 breq2 4841 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((abs‘(𝐹𝑡)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
458 breq2 4841 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ 0 ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
459149leidd 10873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ≤ (abs‘(𝐹𝑡)))
460 breq1 4840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((abs‘(𝐹𝑡)) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) → ((abs‘(𝐹𝑡)) ≤ (abs‘(𝐹𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡))))
461 breq1 4840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) → (0 ≤ (abs‘(𝐹𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡))))
462460, 461ifboth 4311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((abs‘(𝐹𝑡)) ≤ (abs‘(𝐹𝑡)) ∧ 0 ≤ (abs‘(𝐹𝑡))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)))
463459, 151, 462syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑡𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)))
464463adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)))
465146ssneld 3794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (¬ 𝑡𝐷 → ¬ 𝑡 ∈ (𝑢(,)𝑤)))
466465imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡𝐷) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
467225, 223syl6eqbr 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ 0)
468466, 467syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ 0)
469457, 458, 464, 468ifbothda 4310 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))
470469ralrimivw 3151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))
471232, 233ifex 4321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ V
472471a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑡 ∈ ℝ) → if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ V)
473 eqidd 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
474231, 235, 472, 239, 473ofrfval2 7139 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
475474adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
476470, 475mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
477 itg2le 23714 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
478160, 456, 476, 477syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
479454, 162, 455, 346, 478xrletrd 12205 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
4804793adantr3 1205 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
481324, 480eqbrtrd 4859 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
482448, 451, 114, 452, 481wlogle 10840 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
483482anassrs 455 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
484483adantlrr 703 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
485484adantlr 697 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
486 simplr 776 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
487437, 444, 445, 485, 486xrlelttrd 12203 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < (𝑦 / 2))
488 rphalflt 12068 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ → (𝑦 / 2) < 𝑦)
489488adantl 469 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) < 𝑦)
490489ad3antlr 713 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) < 𝑦)
491430, 434, 436, 487, 490lttrd 10477 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)
492491a1d 25 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
493492ralrimiva 3150 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
494493ralrimivw 3151 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) → ∀𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
495 r19.2z 4249 . . . . . . . . . . . 12 ((ℝ+ ≠ ∅ ∧ ∀𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
496426, 494, 495sylancr 577 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
497424, 496syldan 581 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
498497anassrs 455 . . . . . . . . 9 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
499498anassrs 455 . . . . . . . 8 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
500376, 499sylan2b 583 . . . . . . 7 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
501372, 500pm2.61dan 838 . . . . . 6 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
502501ex 399 . . . . 5 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)))
503502rexlimdvva 3222 . . . 4 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)))
50413, 503mpd 15 . . 3 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
505504ralrimivva 3155 . 2 (𝜑 → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
506 ssid 3814 . . 3 ℂ ⊆ ℂ
507 elcncf2 22900 . . 3 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))))
508117, 506, 507sylancl 576 . 2 (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))))
5099, 505, 508mpbir2and 695 1 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2155  wne 2974  wral 3092  wrex 3093  Vcvv 3387  cun 3761  wss 3763  c0 4110  ifcif 4273  𝒫 cpw 4345  cop 4370   class class class wbr 4837  cmpt 4916   × cxp 5303  dom cdm 5305  ran crn 5306  cima 5308  Fun wfun 6089   Fn wfn 6090  wf 6091  cfv 6095  (class class class)co 6868  𝑟 cofr 7120  Fincfn 8186  supcsup 8579  cc 10213  cr 10214  0cc0 10215  1c1 10216  ici 10217   + caddc 10218   · cmul 10220  +∞cpnf 10350  *cxr 10352   < clt 10353  cle 10354  cmin 10545   / cdiv 10963  2c2 11350  +crp 12040  (,)cioo 12387  [,]cicc 12390  abscabs 14191  cnccncf 22886  volcvol 23438  1citg1 23590  2citg2 23591  𝐿1cibl 23592  citg 23593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-inf2 8779  ax-cnex 10271  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291  ax-pre-mulgt0 10292  ax-pre-sup 10293  ax-addf 10294
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-symdif 4036  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-int 4663  df-iun 4707  df-disj 4806  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-se 5265  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-isom 6104  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-of 7121  df-ofr 7122  df-om 7290  df-1st 7392  df-2nd 7393  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-1o 7790  df-2o 7791  df-oadd 7794  df-er 7973  df-map 8088  df-pm 8089  df-en 8187  df-dom 8188  df-sdom 8189  df-fin 8190  df-fi 8550  df-sup 8581  df-inf 8582  df-oi 8648  df-card 9042  df-cda 9269  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-sub 10547  df-neg 10548  df-div 10964  df-nn 11300  df-2 11358  df-3 11359  df-4 11360  df-n0 11554  df-z 11638  df-uz 11899  df-q 12002  df-rp 12041  df-xneg 12156  df-xadd 12157  df-xmul 12158  df-ioo 12391  df-ico 12393  df-icc 12394  df-fz 12544  df-fzo 12684  df-fl 12811  df-mod 12887  df-seq 13019  df-exp 13078  df-hash 13332  df-cj 14056  df-re 14057  df-im 14058  df-sqrt 14192  df-abs 14193  df-clim 14436  df-rlim 14437  df-sum 14634  df-rest 16282  df-topgen 16303  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-top 20906  df-topon 20923  df-bases 20958  df-cmp 21398  df-cncf 22888  df-ovol 23439  df-vol 23440  df-mbf 23594  df-itg1 23595  df-itg2 23596  df-ibl 23597  df-itg 23598  df-0p 23645
This theorem is referenced by:  ftc2nc  33800
  Copyright terms: Public domain W3C validator