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 34118
Description: ftc1a 24237 holds for functions that obey the triangle inequality in the absence of ax-cc 9592. 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 24236 . 2 (𝜑𝐺:(𝐴[,]𝐵)⟶ℂ)
10 rphalfcl 12166 . . . . . 6 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
111, 2, 3, 4, 5, 6, 7, 8ftc1anclem6 34115 . . . . . 6 ((𝜑 ∧ (𝑦 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
1210, 11sylan2 586 . . . . 5 ((𝜑𝑦 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
1312adantrl 706 . . . 4 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
1410ad2antll 719 . . . . . . . . . . 11 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / 2) ∈ ℝ+)
15 2rp 12142 . . . . . . . . . . . 12 2 ∈ ℝ+
16 i1ff 23880 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
1716frnd 6298 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
1817adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ran 𝑓 ⊆ ℝ)
19 i1ff 23880 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
2019frnd 6298 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ)
2120adantl 475 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ran 𝑔 ⊆ ℝ)
2218, 21unssd 4012 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ)
23 ax-resscn 10329 . . . . . . . . . . . . . . . . . 18 ℝ ⊆ ℂ
2422, 23syl6ss 3833 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ)
25 i1f0rn 23886 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓)
26 elun1 4003 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ran 𝑓 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
2725, 26syl 17 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
2827adantr 474 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
29 absf 14484 . . . . . . . . . . . . . . . . . . 19 abs:ℂ⟶ℝ
30 ffn 6291 . . . . . . . . . . . . . . . . . . 19 (abs:ℂ⟶ℝ → abs Fn ℂ)
3129, 30ax-mp 5 . . . . . . . . . . . . . . . . . 18 abs Fn ℂ
32 fnfvima 6769 . . . . . . . . . . . . . . . . . 18 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
3331, 32mp3an1 1521 . . . . . . . . . . . . . . . . 17 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
3424, 28, 33syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
3534ne0d 4150 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅)
36 imassrn 5731 . . . . . . . . . . . . . . . . 17 (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ran abs
37 frn 6297 . . . . . . . . . . . . . . . . . 18 (abs:ℂ⟶ℝ → ran abs ⊆ ℝ)
3829, 37ax-mp 5 . . . . . . . . . . . . . . . . 17 ran abs ⊆ ℝ
3936, 38sstri 3830 . . . . . . . . . . . . . . . 16 (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ
40 ffun 6294 . . . . . . . . . . . . . . . . . 18 (abs:ℂ⟶ℝ → Fun abs)
4129, 40ax-mp 5 . . . . . . . . . . . . . . . . 17 Fun abs
42 i1frn 23881 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
43 i1frn 23881 . . . . . . . . . . . . . . . . . 18 (𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin)
44 unfi 8515 . . . . . . . . . . . . . . . . . 18 ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
4542, 43, 44syl2an 589 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
46 imafi 8547 . . . . . . . . . . . . . . . . 17 ((Fun abs ∧ (ran 𝑓 ∪ ran 𝑔) ∈ Fin) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
4741, 45, 46sylancr 581 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
48 fimaxre2 11323 . . . . . . . . . . . . . . . 16 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥)
4939, 47, 48sylancr 581 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥)
50 suprcl 11337 . . . . . . . . . . . . . . . 16 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
5139, 50mp3an1 1521 . . . . . . . . . . . . . . 15 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
5235, 49, 51syl2anc 579 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
5352adantr 474 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
54 0red 10380 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈ ℝ)
5524sselda 3821 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → 𝑟 ∈ ℂ)
5655abscld 14583 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ ℝ)
5756adantrr 707 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈ ℝ)
5852adantr 474 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
59 absgt0 14471 . . . . . . . . . . . . . . . . . . 19 (𝑟 ∈ ℂ → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
6055, 59syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
6160biimpd 221 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 → 0 < (abs‘𝑟)))
6261impr 448 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < (abs‘𝑟))
6339a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ)
6463, 35, 493jca 1119 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
6564adantr 474 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
66 fnfvima 6769 . . . . . . . . . . . . . . . . . . . 20 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
6731, 66mp3an1 1521 . . . . . . . . . . . . . . . . . . 19 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
6824, 67sylan 575 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
69 suprub 11338 . . . . . . . . . . . . . . . . . 18 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7065, 68, 69syl2anc 579 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7170adantrr 707 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7254, 57, 58, 62, 71ltletrd 10536 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7372rexlimdvaa 3214 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
7473imp 397 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
7553, 74elrpd 12178 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+)
76 rpmulcl 12162 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
7715, 75, 76sylancr 581 . . . . . . . . . . 11 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
78 rpdivcl 12164 . . . . . . . . . . 11 (((𝑦 / 2) ∈ ℝ+ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
7914, 77, 78syl2an 589 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
8079anassrs 461 . . . . . . . . 9 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
8180adantlr 705 . . . . . . . 8 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
82 ancom 454 . . . . . . . . . . . 12 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) ↔ (𝑦 ∈ ℝ+𝑢 ∈ (𝐴[,]𝐵)))
8382anbi2i 616 . . . . . . . . . . 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 636 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ↔ ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
8584anbi1i 617 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)))
86 an32 636 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
8785, 86bitri 267 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
8887anbi1i 617 . . . . . . . . . . . 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 636 . . . . . . . . . . . 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 267 . . . . . . . . . . 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 462 . . . . . . . . . . 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 295 . . . . . . . . . 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 6931 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑤𝑎 = 𝑢) → (𝑏𝑎) = (𝑤𝑢))
9493ancoms 452 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑢𝑏 = 𝑤) → (𝑏𝑎) = (𝑤𝑢))
9594fveq2d 6450 . . . . . . . . . . . . . 14 ((𝑎 = 𝑢𝑏 = 𝑤) → (abs‘(𝑏𝑎)) = (abs‘(𝑤𝑢)))
9695breq1d 4896 . . . . . . . . . . . . 13 ((𝑎 = 𝑢𝑏 = 𝑤) → ((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
97 fveq2 6446 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑤 → (𝐺𝑏) = (𝐺𝑤))
98 fveq2 6446 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑢 → (𝐺𝑎) = (𝐺𝑢))
9997, 98oveqan12rd 6942 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑢𝑏 = 𝑤) → ((𝐺𝑏) − (𝐺𝑎)) = ((𝐺𝑤) − (𝐺𝑢)))
10099fveq2d 6450 . . . . . . . . . . . . . 14 ((𝑎 = 𝑢𝑏 = 𝑤) → (abs‘((𝐺𝑏) − (𝐺𝑎))) = (abs‘((𝐺𝑤) − (𝐺𝑢))))
101100breq1d 4896 . . . . . . . . . . . . 13 ((𝑎 = 𝑢𝑏 = 𝑤) → ((abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦 ↔ (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
10296, 101imbi12d 336 . . . . . . . . . . . 12 ((𝑎 = 𝑢𝑏 = 𝑤) → (((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦) ↔ ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)))
103 oveq12 6931 . . . . . . . . . . . . . . . 16 ((𝑏 = 𝑢𝑎 = 𝑤) → (𝑏𝑎) = (𝑢𝑤))
104103ancoms 452 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑤𝑏 = 𝑢) → (𝑏𝑎) = (𝑢𝑤))
105104fveq2d 6450 . . . . . . . . . . . . . 14 ((𝑎 = 𝑤𝑏 = 𝑢) → (abs‘(𝑏𝑎)) = (abs‘(𝑢𝑤)))
106105breq1d 4896 . . . . . . . . . . . . 13 ((𝑎 = 𝑤𝑏 = 𝑢) → ((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
107 fveq2 6446 . . . . . . . . . . . . . . . 16 (𝑏 = 𝑢 → (𝐺𝑏) = (𝐺𝑢))
108 fveq2 6446 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → (𝐺𝑎) = (𝐺𝑤))
109107, 108oveqan12rd 6942 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑤𝑏 = 𝑢) → ((𝐺𝑏) − (𝐺𝑎)) = ((𝐺𝑢) − (𝐺𝑤)))
110109fveq2d 6450 . . . . . . . . . . . . . 14 ((𝑎 = 𝑤𝑏 = 𝑢) → (abs‘((𝐺𝑏) − (𝐺𝑎))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
111110breq1d 4896 . . . . . . . . . . . . 13 ((𝑎 = 𝑤𝑏 = 𝑢) → ((abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦 ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦))
112106, 111imbi12d 336 . . . . . . . . . . . 12 ((𝑎 = 𝑤𝑏 = 𝑢) → (((abs‘(𝑏𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑏) − (𝐺𝑎))) < 𝑦) ↔ ((abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦)))
113 iccssre 12567 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
1142, 3, 113syl2anc 579 . . . . . . . . . . . . 13 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
115114ad4antr 722 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝐴[,]𝐵) ⊆ ℝ)
116 simp-4l 773 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑)
117114, 23syl6ss 3833 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
118117sselda 3821 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ)
119117sselda 3821 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ)
120 abssub 14473 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (abs‘(𝑤𝑢)) = (abs‘(𝑢𝑤)))
121118, 119, 120syl2anr 590 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤𝑢)) = (abs‘(𝑢𝑤)))
122121anandis 668 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤𝑢)) = (abs‘(𝑢𝑤)))
123122breq1d 4896 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
1249ffvelrnda 6623 . . . . . . . . . . . . . . . . 17 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐺𝑤) ∈ ℂ)
1259ffvelrnda 6623 . . . . . . . . . . . . . . . . 17 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝐺𝑢) ∈ ℂ)
126 abssub 14473 . . . . . . . . . . . . . . . . 17 (((𝐺𝑤) ∈ ℂ ∧ (𝐺𝑢) ∈ ℂ) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
127124, 125, 126syl2anr 590 . . . . . . . . . . . . . . . 16 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
128127anandis 668 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
129128breq1d 4896 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦 ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦))
130123, 129imbi12d 336 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦) ↔ ((abs‘(𝑢𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑢) − (𝐺𝑤))) < 𝑦)))
131116, 130sylan 575 . . . . . . . . . . . 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 10426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐴 ∈ ℝ*)
1333rexrd 10426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐵 ∈ ℝ*)
134132, 133jca 507 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
135 df-icc 12494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥𝑡𝑡𝑦)})
136135elixx3g 12500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑢 ∈ ℝ*) ∧ (𝐴𝑢𝑢𝐵)))
137136simprbi 492 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 ∈ (𝐴[,]𝐵) → (𝐴𝑢𝑢𝐵))
138137simpld 490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢 ∈ (𝐴[,]𝐵) → 𝐴𝑢)
139135elixx3g 12500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝐴𝑤𝑤𝐵)))
140139simprbi 492 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 ∈ (𝐴[,]𝐵) → (𝐴𝑤𝑤𝐵))
141140simprd 491 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ (𝐴[,]𝐵) → 𝑤𝐵)
142138, 141anim12i 606 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴𝑢𝑤𝐵))
143 ioossioo 12578 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑢𝑤𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
144134, 142, 143syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
1455adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
146144, 145sstrd 3831 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
147146sselda 3821 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡𝐷)
1488ffvelrnda 6623 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
149148abscld 14583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ ℝ)
150149rexrd 10426 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ ℝ*)
151148absge0d 14591 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑡𝐷) → 0 ≤ (abs‘(𝐹𝑡)))
152 elxrge0 12595 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((abs‘(𝐹𝑡)) ∈ (0[,]+∞) ↔ ((abs‘(𝐹𝑡)) ∈ ℝ* ∧ 0 ≤ (abs‘(𝐹𝑡))))
153150, 151, 152sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ (0[,]+∞))
154153adantlr 705 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (abs‘(𝐹𝑡)) ∈ (0[,]+∞))
155147, 154syldan 585 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹𝑡)) ∈ (0[,]+∞))
156 0e0iccpnf 12597 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ (0[,]+∞)
157156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
158155, 157ifclda 4341 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
159158adantr 474 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
160159fmpttd 6649 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
161 itg2cl 23936 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
162160, 161syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
1631623adantr3 1173 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
164116, 163sylan 575 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
165164adantr 474 . . . . . . . . . . . . . . 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 765 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)))
167148adantlr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
168147, 167syldan 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
169168adantllr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
170 elioore 12517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
17116ffvelrnda 6623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℝ)
172171recnd 10405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℂ)
173 ax-icn 10331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 i ∈ ℂ
17419ffvelrnda 6623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℝ)
175174recnd 10405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℂ)
176 mulcl 10356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((i ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (i · (𝑔𝑡)) ∈ ℂ)
177173, 175, 176sylancr 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (i · (𝑔𝑡)) ∈ ℂ)
178 addcl 10354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
179172, 177, 178syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
180179anandirs 669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
181170, 180sylan2 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
182181adantll 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
183182adantlr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
184169, 183subcld 10734 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
185184abscld 14583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
186181abscld 14583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
187186adantll 704 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
188187adantlr 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
189185, 188readdcld 10406 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
190189rexrd 10426 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
191184absge0d 14591 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
192180absge0d 14591 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
193170, 192sylan2 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
194193adantll 704 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
195194adantlr 705 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
196185, 188, 191, 195addge0d 10951 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
197 elxrge0 12595 . . . . . . . . . . . . . . . . . . . . . . 23 (((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞) ↔ (((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ* ∧ 0 ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))))
198190, 196, 197sylanbrc 578 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞))
199156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
200198, 199ifclda 4341 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
201200adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
202201fmpttd 6649 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞))
203 itg2cl 23936 . . . . . . . . . . . . . . . . . . 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 1173 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
206166, 205sylan 575 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
207206adantr 474 . . . . . . . . . . . . . . 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 12148 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+𝑦 ∈ ℝ*)
209208ad3antlr 721 . . . . . . . . . . . . . . 15 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → 𝑦 ∈ ℝ*)
210158adantlr 705 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
211210adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
212211fmpttd 6649 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
213169, 183npcand 10738 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) + ((𝑓𝑡) + (i · (𝑔𝑡)))) = (𝐹𝑡))
214213fveq2d 6450 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) + ((𝑓𝑡) + (i · (𝑔𝑡))))) = (abs‘(𝐹𝑡)))
215184, 183abstrid 14603 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) + ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
216214, 215eqbrtrrd 4910 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹𝑡)) ≤ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
217 iftrue 4313 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) = (abs‘(𝐹𝑡)))
218217adantl 475 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) = (abs‘(𝐹𝑡)))
219 iftrue 4313 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) = ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
220219adantl 475 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) = ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
221216, 218, 2203brtr4d 4918 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
222221ex 403 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
223 0le0 11483 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ≤ 0
224223a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0)
225 iffalse 4316 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) = 0)
226 iffalse 4316 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) = 0)
227224, 225, 2263brtr4d 4918 . . . . . . . . . . . . . . . . . . . . . 22 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
228222, 227pm2.61d1 173 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
229228ralrimivw 3149 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
230 reex 10363 . . . . . . . . . . . . . . . . . . . . . . 23 ℝ ∈ V
231230a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ℝ ∈ V)
232 fvex 6459 . . . . . . . . . . . . . . . . . . . . . . . 24 (abs‘(𝐹𝑡)) ∈ V
233 c0ex 10370 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
234232, 233ifex 4355 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ V
235234a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ∈ V)
236 ovex 6954 . . . . . . . . . . . . . . . . . . . . . . . 24 ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ V
237236, 233ifex 4355 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ V
238237a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ V)
239 eqidd 2779 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)))
240 eqidd 2779 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
241231, 235, 238, 239, 240ofrfval2 7192 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
242241ad2antrr 716 . . . . . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
244 itg2le 23943 . . . . . . . . . . . . . . . . . . 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 1439 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))))
2462453adantr3 1173 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) + (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))), 0))))
247166, 246sylan 575 . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . . 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 34117 . . . . . . . . . . . . . . 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 12303 . . . . . . . . . . . . . 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 765 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 𝜑)
252 simpr2 1207 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑤 ∈ (𝐴[,]𝐵))
253 oveq2 6930 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑤 → (𝐴(,)𝑥) = (𝐴(,)𝑤))
254 itgeq1 23976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴(,)𝑥) = (𝐴(,)𝑤) → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
255253, 254syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑤 → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
256 itgex 23974 . . . . . . . . . . . . . . . . . . . . . . . . 25 ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡 ∈ V
257255, 1, 256fvmpt 6542 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ (𝐴[,]𝐵) → (𝐺𝑤) = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
258252, 257syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐺𝑤) = ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡)
2592adantr 474 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝐴 ∈ ℝ)
260114sselda 3821 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ)
2612603ad2antr2 1197 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑤 ∈ ℝ)
262114sselda 3821 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ)
263262rexrd 10426 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ*)
2642633ad2antr1 1196 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢 ∈ ℝ*)
265 elicc1 12531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵)))
266132, 133, 265syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵)))
267266biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ ℝ*𝐴𝑢𝑢𝐵))
268267simp2d 1134 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝐴𝑢)
2692683ad2antr1 1196 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝐴𝑢)
270 simpr3 1209 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢𝑤)
271132adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ*)
272260rexrd 10426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ*)
273 elicc1 12531 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴 ∈ ℝ*𝑤 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤)))
274271, 272, 273syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤)))
2752743ad2antr2 1197 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ*𝐴𝑢𝑢𝑤)))
276264, 269, 270, 275mpbir3and 1399 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢 ∈ (𝐴[,]𝑤))
277 iooss2 12523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐵 ∈ ℝ*𝑤𝐵) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
278133, 141, 277syl2an 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
2795adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝐵) ⊆ 𝐷)
280278, 279sstrd 3831 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ 𝐷)
2812803ad2antr2 1197 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐴(,)𝑤) ⊆ 𝐷)
282281sselda 3821 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → 𝑡𝐷)
283148adantlr 705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
284282, 283syldan 585 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
285 eleq1w 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑢 → (𝑤 ∈ (𝐴[,]𝐵) ↔ 𝑢 ∈ (𝐴[,]𝐵)))
286285anbi2d 622 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑢 → ((𝜑𝑤 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑢 ∈ (𝐴[,]𝐵))))
287 oveq2 6930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑤 = 𝑢 → (𝐴(,)𝑤) = (𝐴(,)𝑢))
288287mpteq1d 4973 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑤 = 𝑢 → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) = (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)))
289288eleq1d 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 = 𝑢 → ((𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1 ↔ (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1))
290286, 289imbi12d 336 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 = 𝑢 → (((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1) ↔ ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1)))
291 ioombl 23769 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴(,)𝑤) ∈ dom vol
292291a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ∈ dom vol)
293148adantlr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑤 ∈ (𝐴[,]𝐵)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
2948feqmptd 6509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝐹 = (𝑡𝐷 ↦ (𝐹𝑡)))
295294, 7eqeltrrd 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
296295adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
297280, 292, 293, 296iblss 24008 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1)
298290, 297chvarv 2361 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1)
2992983ad2antr1 1196 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹𝑡)) ∈ 𝐿1)
300 ioombl 23769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑢(,)𝑤) ∈ dom vol
301300a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ∈ dom vol)
302 fvexd 6461 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ V)
303295adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
304146, 301, 302, 303iblss 24008 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1)
3053043adantr3 1173 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹𝑡)) ∈ 𝐿1)
306259, 261, 276, 284, 299, 305itgsplitioo 24041 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ∫(𝐴(,)𝑤)(𝐹𝑡) d𝑡 = (∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
307258, 306eqtrd 2814 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐺𝑤) = (∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
308 simpr1 1205 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑢 ∈ (𝐴[,]𝐵))
309 oveq2 6930 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝑢 → (𝐴(,)𝑥) = (𝐴(,)𝑢))
310 itgeq1 23976 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐴(,)𝑥) = (𝐴(,)𝑢) → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
311309, 310syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑢 → ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
312 itgex 23974 . . . . . . . . . . . . . . . . . . . . . . . 24 ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 ∈ V
313311, 1, 312fvmpt 6542 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑢 ∈ (𝐴[,]𝐵) → (𝐺𝑢) = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
314308, 313syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝐺𝑢) = ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡)
315307, 314oveq12d 6940 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((𝐺𝑤) − (𝐺𝑢)) = ((∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡))
316 fvexd 6461 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑢)) → (𝐹𝑡) ∈ V)
317316, 298itgcl 23987 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 ∈ ℂ)
318317adantrr 707 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 ∈ ℂ)
319 fvexd 6461 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ V)
320319, 304itgcl 23987 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡 ∈ ℂ)
321318, 320pncan2d 10736 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
3223213adantr3 1173 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
323315, 322eqtrd 2814 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((𝐺𝑤) − (𝐺𝑢)) = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
324323fveq2d 6450 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) = (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
325 ftc1anc.t . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))))
326 df-ov 6925 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢(,)𝑤) = ((,)‘⟨𝑢, 𝑤⟩)
327 opelxpi 5392 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))
328 ioof 12584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
329 ffn 6291 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
330328, 329ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 (,) Fn (ℝ* × ℝ*)
331 iccssxr 12568 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴[,]𝐵) ⊆ ℝ*
332 xpss12 5370 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐴[,]𝐵) ⊆ ℝ* ∧ (𝐴[,]𝐵) ⊆ ℝ*) → ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*))
333331, 331, 332mp2an 682 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*)
334 fnfvima 6769 . . . . . . . . . . . . . . . . . . . . . . . 24 (((,) Fn (ℝ* × ℝ*) ∧ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*) ∧ ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
335330, 333, 334mp3an12 1524 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
336327, 335syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
337326, 336syl5eqel 2863 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
338 itgeq1 23976 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑢(,)𝑤) → ∫𝑠(𝐹𝑡) d𝑡 = ∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡)
339338fveq2d 6450 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑢(,)𝑤) → (abs‘∫𝑠(𝐹𝑡) d𝑡) = (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡))
340 eleq2 2848 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑠 = (𝑢(,)𝑤) → (𝑡𝑠𝑡 ∈ (𝑢(,)𝑤)))
341340ifbid 4329 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑠 = (𝑢(,)𝑤) → if(𝑡𝑠, (abs‘(𝐹𝑡)), 0) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))
342341mpteq2dv 4980 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)))
343342fveq2d 6450 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠 = (𝑢(,)𝑤) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
344339, 343breq12d 4899 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑢(,)𝑤) → ((abs‘∫𝑠(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)))))
345344rspccva 3510 . . . . . . . . . . . . . . . . . . . . 21 ((∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝑠, (abs‘(𝐹𝑡)), 0))) ∧ (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
346325, 337, 345syl2an 589 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
3473463adantr3 1173 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
348324, 347eqbrtrd 4908 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
349348adantlr 705 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))))
350 subcl 10621 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺𝑤) ∈ ℂ ∧ (𝐺𝑢) ∈ ℂ) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
351124, 125, 350syl2anr 590 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
352351anandis 668 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
353352abscld 14583 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
354353rexrd 10426 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
3553543adantr3 1173 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
356355adantlr 705 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
357163adantlr 705 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
358208ad2antlr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → 𝑦 ∈ ℝ*)
359 xrlelttr 12299 . . . . . . . . . . . . . . . . . 18 (((abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ* ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∈ ℝ*𝑦 ∈ ℝ*) → (((abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
360356, 357, 358, 359syl3anc 1439 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (((abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
361349, 360mpand 685 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
362251, 361sylanl1 670 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) < 𝑦 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
363362adantr 474 . . . . . . . . . . . . . 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 403 . . . . . . . . . . . 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 10908 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
367366anassrs 461 . . . . . . . . . 10 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
36892, 367sylanb 576 . . . . . . . . 9 ((((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
369368ralrimiva 3148 . . . . . . . 8 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
370 breq2 4890 . . . . . . . . 9 (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → ((abs‘(𝑤𝑢)) < 𝑧 ↔ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
371370rspceaimv 3519 . . . . . . . 8 ((((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
37281, 369, 371syl2anc 579 . . . . . . 7 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
373 ralnex 3174 . . . . . . . . 9 (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)
374 nne 2973 . . . . . . . . . 10 𝑟 ≠ 0 ↔ 𝑟 = 0)
375374ralbii 3162 . . . . . . . . 9 (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
376373, 375bitr3i 269 . . . . . . . 8 (¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
37716ffnd 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 ∈ dom ∫1𝑓 Fn ℝ)
378 fnfvelrn 6620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ran 𝑓)
379377, 378sylan 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ran 𝑓)
380 elun1 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑓𝑡) ∈ ran 𝑓 → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
381379, 380syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
382 eqeq1 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑟 = (𝑓𝑡) → (𝑟 = 0 ↔ (𝑓𝑡) = 0))
383382rspcva 3509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓𝑡) = 0)
384381, 383sylan 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓𝑡) = 0)
385384adantllr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓𝑡) = 0)
38619ffnd 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑔 ∈ dom ∫1𝑔 Fn ℝ)
387 fnfvelrn 6620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ran 𝑔)
388386, 387sylan 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ran 𝑔)
389 elun2 4004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑔𝑡) ∈ ran 𝑔 → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
390388, 389syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
391 eqeq1 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑟 = (𝑔𝑡) → (𝑟 = 0 ↔ (𝑔𝑡) = 0))
392391rspcva 3509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑔𝑡) = 0)
393392oveq2d 6938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = (i · 0))
394 it0e0 11604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (i · 0) = 0
395393, 394syl6eq 2830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = 0)
396390, 395sylan 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = 0)
397396adantlll 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔𝑡)) = 0)
398385, 397oveq12d 6940 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((𝑓𝑡) + (i · (𝑔𝑡))) = (0 + 0))
399398an32s 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) = (0 + 0))
400 00id 10551 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 + 0) = 0
401399, 400syl6eq 2830 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) = 0)
402401adantlll 708 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) = 0)
403402oveq2d 6938 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = (if(𝑡𝐷, (𝐹𝑡), 0) − 0))
404 0cnd 10369 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ ℂ)
405148, 404ifclda 4341 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
406405subid1d 10723 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (if(𝑡𝐷, (𝐹𝑡), 0) − 0) = if(𝑡𝐷, (𝐹𝑡), 0))
407406ad3antrrr 720 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − 0) = if(𝑡𝐷, (𝐹𝑡), 0))
408403, 407eqtrd 2814 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) = if(𝑡𝐷, (𝐹𝑡), 0))
409408fveq2d 6450 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = (abs‘if(𝑡𝐷, (𝐹𝑡), 0)))
410 fvif 6462 . . . . . . . . . . . . . . . . . . . . . 22 (abs‘if(𝑡𝐷, (𝐹𝑡), 0)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), (abs‘0))
411 abs0 14432 . . . . . . . . . . . . . . . . . . . . . . 23 (abs‘0) = 0
412 ifeq2 4312 . . . . . . . . . . . . . . . . . . . . . . 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 2802 . . . . . . . . . . . . . . . . . . . . 21 (abs‘if(𝑡𝐷, (𝐹𝑡), 0)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)
415409, 414syl6eq 2830 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))
416415mpteq2dva 4979 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
417416fveq2d 6450 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
418417breq1d 4896 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)))
419418biimpd 221 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)))
420419ex 403 . . . . . . . . . . . . . . 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 411 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
423422anasss 460 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
424423adantlr 705 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
425 1rp 12141 . . . . . . . . . . . . 13 1 ∈ ℝ+
426425ne0ii 4152 . . . . . . . . . . . 12 + ≠ ∅
427352anassrs 461 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((𝐺𝑤) − (𝐺𝑢)) ∈ ℂ)
428427abscld 14583 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
429428adantlrr 711 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
430429adantlr 705 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ)
431 rpre 12145 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
432431rehalfcld 11629 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
433432adantl 475 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
434433ad3antlr 721 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ)
435431adantl 475 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
436435ad3antlr 721 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ)
437430rexrd 10426 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ∈ ℝ*)
438156a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ (0[,]+∞))
439153, 438ifclda 4341 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
440439adantr 474 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡 ∈ ℝ) → if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ (0[,]+∞))
441440fmpttd 6649 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
442 itg2cl 23936 . . . . . . . . . . . . . . . . . . 19 ((𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
443441, 442syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
444443ad3antrrr 720 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
445434rexrd 10426 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ*)
446108, 107oveqan12rd 6942 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 = 𝑢𝑎 = 𝑤) → ((𝐺𝑎) − (𝐺𝑏)) = ((𝐺𝑤) − (𝐺𝑢)))
447446fveq2d 6450 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 = 𝑢𝑎 = 𝑤) → (abs‘((𝐺𝑎) − (𝐺𝑏))) = (abs‘((𝐺𝑤) − (𝐺𝑢))))
448447breq1d 4896 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑢𝑎 = 𝑤) → ((abs‘((𝐺𝑎) − (𝐺𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))))
44998, 97oveqan12rd 6942 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 = 𝑤𝑎 = 𝑢) → ((𝐺𝑎) − (𝐺𝑏)) = ((𝐺𝑢) − (𝐺𝑤)))
450449fveq2d 6450 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 = 𝑤𝑎 = 𝑢) → (abs‘((𝐺𝑎) − (𝐺𝑏))) = (abs‘((𝐺𝑢) − (𝐺𝑤))))
451450breq1d 4896 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏 = 𝑤𝑎 = 𝑢) → ((abs‘((𝐺𝑎) − (𝐺𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))))
452128breq1d 4896 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ↔ (abs‘((𝐺𝑢) − (𝐺𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))))
453320abscld 14583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ∈ ℝ)
454453rexrd 10426 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ∈ ℝ*)
455443adantr 474 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) ∈ ℝ*)
456441adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)):ℝ⟶(0[,]+∞))
457 breq2 4890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((abs‘(𝐹𝑡)) = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
458 breq2 4890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 = if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ 0 ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
459149leidd 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑𝑡𝐷) → (abs‘(𝐹𝑡)) ≤ (abs‘(𝐹𝑡)))
460 breq1 4889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((abs‘(𝐹𝑡)) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) → ((abs‘(𝐹𝑡)) ≤ (abs‘(𝐹𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡))))
461 breq1 4889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) → (0 ≤ (abs‘(𝐹𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡))))
462460, 461ifboth 4345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((abs‘(𝐹𝑡)) ≤ (abs‘(𝐹𝑡)) ∧ 0 ≤ (abs‘(𝐹𝑡))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)))
463459, 151, 462syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑡𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)))
464463adantlr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ (abs‘(𝐹𝑡)))
465146ssneld 3823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (¬ 𝑡𝐷 → ¬ 𝑡 ∈ (𝑢(,)𝑤)))
466465imp 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡𝐷) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
467225, 223syl6eqbr 4925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ 0)
468466, 467syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ 0)
469457, 458, 464, 468ifbothda 4344 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))
470469ralrimivw 3149 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))
471232, 233ifex 4355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ V
472471a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑡 ∈ ℝ) → if(𝑡𝐷, (abs‘(𝐹𝑡)), 0) ∈ V)
473 eqidd 2779 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
474231, 235, 472, 239, 473ofrfval2 7192 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
475474adantr 474 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0) ≤ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
476470, 475mpbird 249 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0)))
477 itg2le 23943 . . . . . . . . . . . . . . . . . . . . . . . . 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 1439 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
479454, 162, 455, 346, 478xrletrd 12305 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
4804793adantr3 1173 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
481324, 480eqbrtrd 4908 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
482448, 451, 114, 452, 481wlogle 10908 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
483482anassrs 461 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
484483adantlrr 711 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
485484adantlr 705 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))))
486 simplr 759 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2))
487437, 444, 445, 485, 486xrlelttrd 12303 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < (𝑦 / 2))
488 rphalflt 12168 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℝ+ → (𝑦 / 2) < 𝑦)
489488adantl 475 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) < 𝑦)
490489ad3antlr 721 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) < 𝑦)
491430, 434, 436, 487, 490lttrd 10537 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)
492491a1d 25 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
493492ralrimiva 3148 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
494493ralrimivw 3149 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) → ∀𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
495 r19.2z 4283 . . . . . . . . . . . 12 ((ℝ+ ≠ ∅ ∧ ∀𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
496426, 494, 495sylancr 581 . . . . . . . . . . 11 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡𝐷, (abs‘(𝐹𝑡)), 0))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
497424, 496syldan 585 . . . . . . . . . 10 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
498497anassrs 461 . . . . . . . . 9 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
499498anassrs 461 . . . . . . . 8 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
500376, 499sylan2b 587 . . . . . . 7 (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
501372, 500pm2.61dan 803 . . . . . 6 ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
502501ex 403 . . . . 5 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)))
503502rexlimdvva 3221 . . . 4 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (∃𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦)))
50413, 503mpd 15 . . 3 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
505504ralrimivva 3153 . 2 (𝜑 → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))
506 ssid 3842 . . 3 ℂ ⊆ ℂ
507 elcncf2 23101 . . 3 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))))
508117, 506, 507sylancl 580 . 2 (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤𝑢)) < 𝑧 → (abs‘((𝐺𝑤) − (𝐺𝑢))) < 𝑦))))
5099, 505, 508mpbir2and 703 1 (𝜑𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1071   = wceq 1601  wcel 2107  wne 2969  wral 3090  wrex 3091  Vcvv 3398  cun 3790  wss 3792  c0 4141  ifcif 4307  𝒫 cpw 4379  cop 4404   class class class wbr 4886  cmpt 4965   × cxp 5353  dom cdm 5355  ran crn 5356  cima 5358  Fun wfun 6129   Fn wfn 6130  wf 6131  cfv 6135  (class class class)co 6922  𝑟 cofr 7173  Fincfn 8241  supcsup 8634  cc 10270  cr 10271  0cc0 10272  1c1 10273  ici 10274   + caddc 10275   · cmul 10277  +∞cpnf 10408  *cxr 10410   < clt 10411  cle 10412  cmin 10606   / cdiv 11032  2c2 11430  +crp 12137  (,)cioo 12487  [,]cicc 12490  abscabs 14381  cnccncf 23087  volcvol 23667  1citg1 23819  2citg2 23820  𝐿1cibl 23821  citg 23822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-symdif 4067  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-disj 4855  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-ofr 7175  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fi 8605  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-n0 11643  df-z 11729  df-uz 11993  df-q 12096  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-ioo 12491  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-clim 14627  df-rlim 14628  df-sum 14825  df-rest 16469  df-topgen 16490  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137  df-mopn 20138  df-top 21106  df-topon 21123  df-bases 21158  df-cmp 21599  df-cncf 23089  df-ovol 23668  df-vol 23669  df-mbf 23823  df-itg1 23824  df-itg2 23825  df-ibl 23826  df-itg 23827  df-0p 23874
This theorem is referenced by:  ftc2nc  34119
  Copyright terms: Public domain W3C validator