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

Theorem ftc1anclem7 35155
 Description: Lemma for ftc1anc 35157. (Contributed by Brendan Leahy, 13-May-2018.)
Hypotheses
Ref Expression
ftc1anc.g 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡)
ftc1anc.a (𝜑𝐴 ∈ ℝ)
ftc1anc.b (𝜑𝐵 ∈ ℝ)
ftc1anc.le (𝜑𝐴𝐵)
ftc1anc.s (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
ftc1anc.d (𝜑𝐷 ⊆ ℝ)
ftc1anc.i (𝜑𝐹 ∈ 𝐿1)
ftc1anc.f (𝜑𝐹:𝐷⟶ℂ)
Assertion
Ref Expression
ftc1anclem7 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))) < ((𝑦 / 2) + (𝑦 / 2)))
Distinct variable groups:   𝑓,𝑔,𝑟,𝑡,𝑢,𝑤,𝑥,𝑦,𝐴   𝐵,𝑓,𝑔,𝑟,𝑡,𝑢,𝑤,𝑥,𝑦   𝐷,𝑓,𝑔,𝑟,𝑡,𝑢,𝑤,𝑥,𝑦   𝑓,𝐹,𝑔,𝑟,𝑡,𝑢,𝑤,𝑥,𝑦   𝜑,𝑓,𝑔,𝑟,𝑡,𝑢,𝑤,𝑥,𝑦   𝑓,𝐺,𝑔,𝑟,𝑢,𝑤,𝑦
Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1anclem7
StepHypRef Expression
1 i1ff 24290 . . . . . . . . . . 11 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
21ffvelrnda 6829 . . . . . . . . . 10 ((𝑓 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℝ)
32recnd 10661 . . . . . . . . 9 ((𝑓 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℂ)
4 ax-icn 10588 . . . . . . . . . 10 i ∈ ℂ
5 i1ff 24290 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
65ffvelrnda 6829 . . . . . . . . . . 11 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℝ)
76recnd 10661 . . . . . . . . . 10 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℂ)
8 mulcl 10613 . . . . . . . . . 10 ((i ∈ ℂ ∧ (𝑔𝑥) ∈ ℂ) → (i · (𝑔𝑥)) ∈ ℂ)
94, 7, 8sylancr 590 . . . . . . . . 9 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (i · (𝑔𝑥)) ∈ ℂ)
10 addcl 10611 . . . . . . . . 9 (((𝑓𝑥) ∈ ℂ ∧ (i · (𝑔𝑥)) ∈ ℂ) → ((𝑓𝑥) + (i · (𝑔𝑥))) ∈ ℂ)
113, 9, 10syl2an 598 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑥 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑥 ∈ ℝ)) → ((𝑓𝑥) + (i · (𝑔𝑥))) ∈ ℂ)
1211anandirs 678 . . . . . . 7 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑓𝑥) + (i · (𝑔𝑥))) ∈ ℂ)
13 reex 10620 . . . . . . . . 9 ℝ ∈ V
1413a1i 11 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ℝ ∈ V)
152adantlr 714 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℝ)
16 ovexd 7171 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (i · (𝑔𝑥)) ∈ V)
171feqmptd 6709 . . . . . . . . 9 (𝑓 ∈ dom ∫1𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
1817adantr 484 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
1913a1i 11 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → ℝ ∈ V)
204a1i 11 . . . . . . . . . 10 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → i ∈ ℂ)
21 fconstmpt 5579 . . . . . . . . . . 11 (ℝ × {i}) = (𝑥 ∈ ℝ ↦ i)
2221a1i 11 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → (ℝ × {i}) = (𝑥 ∈ ℝ ↦ i))
235feqmptd 6709 . . . . . . . . . 10 (𝑔 ∈ dom ∫1𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
2419, 20, 6, 22, 23offval2 7409 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → ((ℝ × {i}) ∘f · 𝑔) = (𝑥 ∈ ℝ ↦ (i · (𝑔𝑥))))
2524adantl 485 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((ℝ × {i}) ∘f · 𝑔) = (𝑥 ∈ ℝ ↦ (i · (𝑔𝑥))))
2614, 15, 16, 18, 25offval2 7409 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑓f + ((ℝ × {i}) ∘f · 𝑔)) = (𝑥 ∈ ℝ ↦ ((𝑓𝑥) + (i · (𝑔𝑥)))))
27 absf 14692 . . . . . . . . 9 abs:ℂ⟶ℝ
2827a1i 11 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → abs:ℂ⟶ℝ)
2928feqmptd 6709 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → abs = (𝑡 ∈ ℂ ↦ (abs‘𝑡)))
30 fveq2 6646 . . . . . . 7 (𝑡 = ((𝑓𝑥) + (i · (𝑔𝑥))) → (abs‘𝑡) = (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))
3112, 26, 29, 30fmptco 6869 . . . . . 6 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs ∘ (𝑓f + ((ℝ × {i}) ∘f · 𝑔))) = (𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥))))))
32 ftc1anclem3 35151 . . . . . 6 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs ∘ (𝑓f + ((ℝ × {i}) ∘f · 𝑔))) ∈ dom ∫1)
3331, 32eqeltrrd 2891 . . . . 5 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥))))) ∈ dom ∫1)
34 ioombl 24179 . . . . 5 (𝑢(,)𝑤) ∈ dom vol
35 fveq2 6646 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑓𝑥) = (𝑓𝑡))
36 fveq2 6646 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
3736oveq2d 7152 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (i · (𝑔𝑥)) = (i · (𝑔𝑡)))
3835, 37oveq12d 7154 . . . . . . . . . . 11 (𝑥 = 𝑡 → ((𝑓𝑥) + (i · (𝑔𝑥))) = ((𝑓𝑡) + (i · (𝑔𝑡))))
3938fveq2d 6650 . . . . . . . . . 10 (𝑥 = 𝑡 → (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))) = (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
40 eqid 2798 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥))))) = (𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))
41 fvex 6659 . . . . . . . . . 10 (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ V
4239, 40, 41fvmpt 6746 . . . . . . . . 9 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))‘𝑡) = (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
4342eqcomd 2804 . . . . . . . 8 (𝑡 ∈ ℝ → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) = ((𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))‘𝑡))
4443ifeq1d 4443 . . . . . . 7 (𝑡 ∈ ℝ → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) = if(𝑡 ∈ (𝑢(,)𝑤), ((𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))‘𝑡), 0))
4544mpteq2ia 5122 . . . . . 6 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))‘𝑡), 0))
4645i1fres 24319 . . . . 5 (((𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥))))) ∈ dom ∫1 ∧ (𝑢(,)𝑤) ∈ dom vol) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1)
4733, 34, 46sylancl 589 . . . 4 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1)
48 breq2 5035 . . . . . . 7 ((abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) → (0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ↔ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
49 breq2 5035 . . . . . . 7 (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
50 elioore 12759 . . . . . . . 8 (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
51 eleq1w 2872 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑥 ∈ ℝ ↔ 𝑡 ∈ ℝ))
5251anbi2d 631 . . . . . . . . . . 11 (𝑥 = 𝑡 → (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ↔ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)))
5338eleq1d 2874 . . . . . . . . . . 11 (𝑥 = 𝑡 → (((𝑓𝑥) + (i · (𝑔𝑥))) ∈ ℂ ↔ ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ))
5452, 53imbi12d 348 . . . . . . . . . 10 (𝑥 = 𝑡 → ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑓𝑥) + (i · (𝑔𝑥))) ∈ ℂ) ↔ (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)))
5554, 12chvarvv 2005 . . . . . . . . 9 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
5655absge0d 14799 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
5750, 56sylan2 595 . . . . . . 7 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
58 0le0 11729 . . . . . . . 8 0 ≤ 0
5958a1i 11 . . . . . . 7 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ 0)
6048, 49, 57, 59ifbothda 4462 . . . . . 6 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))
6160ralrimivw 3150 . . . . 5 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ∀𝑡 ∈ ℝ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))
62 ax-resscn 10586 . . . . . . . 8 ℝ ⊆ ℂ
6362a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ℝ ⊆ ℂ)
64 c0ex 10627 . . . . . . . . . 10 0 ∈ V
6541, 64ifex 4473 . . . . . . . . 9 if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ∈ V
66 eqid 2798 . . . . . . . . 9 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))
6765, 66fnmpti 6464 . . . . . . . 8 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) Fn ℝ
6867a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) Fn ℝ)
6963, 680pledm 24287 . . . . . 6 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ↔ (ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))))
7064a1i 11 . . . . . . 7 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ∈ V)
7165a1i 11 . . . . . . 7 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ∈ V)
72 fconstmpt 5579 . . . . . . . 8 (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
7372a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
74 eqidd 2799 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
7514, 70, 71, 73, 74ofrfval2 7410 . . . . . 6 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
7669, 75bitrd 282 . . . . 5 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
7761, 76mpbird 260 . . . 4 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
78 itg2itg1 24350 . . . . 5 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1 ∧ 0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))))
79 itg1cl 24299 . . . . . 6 ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
8079adantr 484 . . . . 5 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1 ∧ 0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) → (∫1‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
8178, 80eqeltrd 2890 . . . 4 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1 ∧ 0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
8247, 77, 81syl2anc 587 . . 3 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
8382ad6antlr 736 . 2 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
84 simplll 774 . . . . 5 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)))
85 ftc1anc.a . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
8685rexrd 10683 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ*)
87 ftc1anc.b . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℝ)
8887rexrd 10683 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ*)
8986, 88jca 515 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
90 df-icc 12736 . . . . . . . . . . . . . . . . . . . . . 22 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥𝑡𝑡𝑦)})
9190elixx3g 12742 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑢 ∈ ℝ*) ∧ (𝐴𝑢𝑢𝐵)))
9291simprbi 500 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ (𝐴[,]𝐵) → (𝐴𝑢𝑢𝐵))
9392simpld 498 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ (𝐴[,]𝐵) → 𝐴𝑢)
9490elixx3g 12742 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝐴𝑤𝑤𝐵)))
9594simprbi 500 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝐴[,]𝐵) → (𝐴𝑤𝑤𝐵))
9695simprd 499 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝐴[,]𝐵) → 𝑤𝐵)
9793, 96anim12i 615 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴𝑢𝑤𝐵))
98 ioossioo 12822 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑢𝑤𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
9989, 97, 98syl2an 598 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
100 ftc1anc.s . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
101100adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
10299, 101sstrd 3925 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
1031023adantr3 1168 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑢(,)𝑤) ⊆ 𝐷)
104103sselda 3915 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡𝐷)
105 ftc1anc.f . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝐷⟶ℂ)
106105ffvelrnda 6829 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
107106adantlr 714 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
108104, 107syldan 594 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
109108adantllr 718 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
11055adantll 713 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
11150, 110sylan2 595 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
112111adantlr 714 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
113109, 112subcld 10989 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
114113abscld 14791 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
115114rexrd 10683 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
116113absge0d 14799 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
117 elxrge0 12838 . . . . . . . . 9 ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
118115, 116, 117sylanbrc 586 . . . . . . . 8 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞))
119 0e0iccpnf 12840 . . . . . . . . 9 0 ∈ (0[,]+∞)
120119a1i 11 . . . . . . . 8 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
121118, 120ifclda 4459 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
122121adantr 484 . . . . . 6 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
123122fmpttd 6857 . . . . 5 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞))
12484, 123sylan 583 . . . 4 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞))
125 rpre 12388 . . . . . 6 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
126125rehalfcld 11875 . . . . 5 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
127126ad2antlr 726 . . . 4 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑦 / 2) ∈ ℝ)
128 simpll 766 . . . . . . . 8 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)))
129102sselda 3915 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡𝐷)
130129adantllr 718 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡𝐷)
131106adantlr 714 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
132 ftc1anc.d . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐷 ⊆ ℝ)
133132sselda 3915 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡𝐷) → 𝑡 ∈ ℝ)
134133adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → 𝑡 ∈ ℝ)
135134, 110syldan 594 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
136131, 135subcld 10989 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → ((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
137136abscld 14791 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
138137rexrd 10683 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
139138adantlr 714 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
140130, 139syldan 594 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
141136absge0d 14799 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
142141adantlr 714 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
143130, 142syldan 594 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
144140, 143, 117sylanbrc 586 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞))
145119a1i 11 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
146144, 145ifclda 4459 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
147146adantr 484 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
148147fmpttd 6857 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞))
149 itg2cl 24346 . . . . . . . . 9 ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
150148, 149syl 17 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
151128, 150sylan 583 . . . . . . 7 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
152 rphalfcl 12407 . . . . . . . . 9 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
153152rpxrd 12423 . . . . . . . 8 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ*)
154153ad2antlr 726 . . . . . . 7 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑦 / 2) ∈ ℝ*)
155 0cnd 10626 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ ℂ)
156106, 155ifclda 4459 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
157 subcl 10877 . . . . . . . . . . . . . . . 16 ((if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ ∧ ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
158156, 55, 157syl2an 598 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
159158anassrs 471 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
160159abscld 14791 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
161160rexrd 10683 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
162159absge0d 14799 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
163 elxrge0 12838 . . . . . . . . . . . 12 ((abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
164161, 162, 163sylanbrc 586 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞))
165164fmpttd 6857 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))):ℝ⟶(0[,]+∞))
166 itg2cl 24346 . . . . . . . . . 10 ((𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) ∈ ℝ*)
167165, 166syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) ∈ ℝ*)
168167ad3antrrr 729 . . . . . . . 8 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) ∈ ℝ*)
169165adantr 484 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))):ℝ⟶(0[,]+∞))
170 breq1 5034 . . . . . . . . . . . . 13 ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
171 breq1 5034 . . . . . . . . . . . . 13 (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) → (0 ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
172137leidd 11198 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
173 iftrue 4431 . . . . . . . . . . . . . . . . . . 19 (𝑡𝐷 → if(𝑡𝐷, (𝐹𝑡), 0) = (𝐹𝑡))
174173fvoveq1d 7158 . . . . . . . . . . . . . . . . . 18 (𝑡𝐷 → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
175174adantl 485 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
176172, 175breqtrrd 5059 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
177176adantlr 714 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
178130, 177syldan 594 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
179178adantlr 714 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
180162adantlr 714 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
181180adantr 484 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
182170, 171, 179, 181ifbothda 4462 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
183182ralrimiva 3149 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
18413a1i 11 . . . . . . . . . . . . 13 (𝜑 → ℝ ∈ V)
185 fvex 6659 . . . . . . . . . . . . . . 15 (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ V
186185, 64ifex 4473 . . . . . . . . . . . . . 14 if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ V
187186a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ V)
188 fvexd 6661 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ V)
189 eqidd 2799 . . . . . . . . . . . . 13 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
190 eqidd 2799 . . . . . . . . . . . . 13 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
191184, 187, 188, 189, 190ofrfval2 7410 . . . . . . . . . . . 12 (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
192191ad2antrr 725 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
193183, 192mpbird 260 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
194 itg2le 24353 . . . . . . . . . 10 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))))
195148, 169, 193, 194syl3anc 1368 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))))
196128, 195sylan 583 . . . . . . . 8 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))))
197 simpllr 775 . . . . . . . 8 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
198151, 168, 154, 196, 197xrlelttrd 12544 . . . . . . 7 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) < (𝑦 / 2))
199151, 154, 198xrltled 12534 . . . . . 6 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (𝑦 / 2))
200199adantllr 718 . . . . 5 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (𝑦 / 2))
2012003adantr3 1168 . . . 4 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (𝑦 / 2))
202 itg2lecl 24352 . . . 4 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑦 / 2) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (𝑦 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ)
203124, 127, 201, 202syl3anc 1368 . . 3 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ)
204203adantr 484 . 2 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ)
205126ad3antlr 730 . 2 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (𝑦 / 2) ∈ ℝ)
20682adantr 484 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
207 2rp 12385 . . . . . . . . 9 2 ∈ ℝ+
208 imassrn 5908 . . . . . . . . . . . . . . . 16 (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ran abs
209 frn 6494 . . . . . . . . . . . . . . . . 17 (abs:ℂ⟶ℝ → ran abs ⊆ ℝ)
21027, 209ax-mp 5 . . . . . . . . . . . . . . . 16 ran abs ⊆ ℝ
211208, 210sstri 3924 . . . . . . . . . . . . . . 15 (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ
212211a1i 11 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ)
2131frnd 6495 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
214213adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ran 𝑓 ⊆ ℝ)
2155frnd 6495 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ)
216215adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ran 𝑔 ⊆ ℝ)
217214, 216unssd 4113 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ)
218217, 62sstrdi 3927 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ)
219 i1f0rn 24296 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓)
220 elun1 4103 . . . . . . . . . . . . . . . . . 18 (0 ∈ ran 𝑓 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
221219, 220syl 17 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
222221adantr 484 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
223 ffn 6488 . . . . . . . . . . . . . . . . . 18 (abs:ℂ⟶ℝ → abs Fn ℂ)
22427, 223ax-mp 5 . . . . . . . . . . . . . . . . 17 abs Fn ℂ
225 fnfvima 6974 . . . . . . . . . . . . . . . . 17 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
226224, 225mp3an1 1445 . . . . . . . . . . . . . . . 16 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
227218, 222, 226syl2anc 587 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
228227ne0d 4251 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅)
229 ffun 6491 . . . . . . . . . . . . . . . . 17 (abs:ℂ⟶ℝ → Fun abs)
23027, 229ax-mp 5 . . . . . . . . . . . . . . . 16 Fun abs
231 i1frn 24291 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
232 i1frn 24291 . . . . . . . . . . . . . . . . 17 (𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin)
233 unfi 8772 . . . . . . . . . . . . . . . . 17 ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
234231, 232, 233syl2an 598 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
235 imafi 8804 . . . . . . . . . . . . . . . 16 ((Fun abs ∧ (ran 𝑓 ∪ ran 𝑔) ∈ Fin) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
236230, 234, 235sylancr 590 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
237 fimaxre2 11577 . . . . . . . . . . . . . . 15 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥)
238211, 236, 237sylancr 590 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥)
239 suprcl 11591 . . . . . . . . . . . . . 14 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
240212, 228, 238, 239syl3anc 1368 . . . . . . . . . . . . 13 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
241240adantr 484 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
242 0red 10636 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈ ℝ)
243218sselda 3915 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → 𝑟 ∈ ℂ)
244243abscld 14791 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ ℝ)
245244adantrr 716 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈ ℝ)
246 absgt0 14679 . . . . . . . . . . . . . . . 16 (𝑟 ∈ ℂ → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
247243, 246syl 17 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
248247biimpa 480 . . . . . . . . . . . . . 14 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) ∧ 𝑟 ≠ 0) → 0 < (abs‘𝑟))
249248anasss 470 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < (abs‘𝑟))
250212, 228, 2383jca 1125 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
251250adantr 484 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
252 fnfvima 6974 . . . . . . . . . . . . . . . . 17 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
253224, 252mp3an1 1445 . . . . . . . . . . . . . . . 16 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
254218, 253sylan 583 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
255 suprub 11592 . . . . . . . . . . . . . . 15 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
256251, 254, 255syl2anc 587 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
257256adantrr 716 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
258242, 245, 241, 249, 257ltletrd 10792 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
259241, 258elrpd 12419 . . . . . . . . . . 11 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+)
260259rexlimdvaa 3244 . . . . . . . . . 10 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+))
261260imp 410 . . . . . . . . 9 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+)
262 rpmulcl 12403 . . . . . . . . 9 ((2 ∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
263207, 261, 262sylancr 590 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
264206, 263rerpdivcld 12453 . . . . . . 7 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
265264adantll 713 . . . . . 6 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
266265adantlr 714 . . . . 5 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
267266ad3antrrr 729 . . . 4 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
268 simp-4l 782 . . . . . 6 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑)
269 iccssre 12810 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
27085, 87, 269syl2anc 587 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
271270, 62sstrdi 3927 . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
272271sselda 3915 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ)
273271sselda 3915 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ)
274 subcl 10877 . . . . . . . . . 10 ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (𝑤𝑢) ∈ ℂ)
275272, 273, 274syl2anr 599 . . . . . . . . 9 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → (𝑤𝑢) ∈ ℂ)
276275anandis 677 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑤𝑢) ∈ ℂ)
277276abscld 14791 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤𝑢)) ∈ ℝ)
2782773adantr3 1168 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘(𝑤𝑢)) ∈ ℝ)
279268, 278sylan 583 . . . . 5 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘(𝑤𝑢)) ∈ ℝ)
280279adantr 484 . . . 4 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (abs‘(𝑤𝑢)) ∈ ℝ)
281 rpdivcl 12405 . . . . . . . . 9 (((𝑦 / 2) ∈ ℝ+ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
282152, 263, 281syl2anr 599 . . . . . . . 8 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
283282rpred 12422 . . . . . . 7 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
284283adantlll 717 . . . . . 6 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
285284adantllr 718 . . . . 5 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
286285ad2antrr 725 . . . 4 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
287270sseld 3914 . . . . . . . . . . 11 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) → 𝑢 ∈ ℝ))
288270sseld 3914 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ∈ ℝ))
289 idd 24 . . . . . . . . . . 11 (𝜑 → (𝑢𝑤𝑢𝑤))
290287, 288, 2893anim123d 1440 . . . . . . . . . 10 (𝜑 → ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤) → (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)))
291290ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤) → (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)))
292291imp 410 . . . . . . . 8 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤))
29355abscld 14791 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
294293rexrd 10683 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ*)
295 elxrge0 12838 . . . . . . . . . . . . . . . . . 18 ((abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ (0[,]+∞) ↔ ((abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
296294, 56, 295sylanbrc 586 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ (0[,]+∞))
297 ifcl 4469 . . . . . . . . . . . . . . . . 17 (((abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ∈ (0[,]+∞))
298296, 119, 297sylancl 589 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ∈ (0[,]+∞))
299298fmpttd 6857 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)):ℝ⟶(0[,]+∞))
300240recnd 10661 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℂ)
3013002timesd 11871 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) = (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
302240, 240readdcld 10662 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ)
303302rexrd 10683 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ*)
304 abs0 14640 . . . . . . . . . . . . . . . . . . . . . . 23 (abs‘0) = 0
305304, 227eqeltrrid 2895 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
306 suprub 11592 . . . . . . . . . . . . . . . . . . . . . 22 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ 0 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → 0 ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
307250, 305, 306syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
308240, 240, 307, 307addge0d 11208 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
309 elxrge0 12838 . . . . . . . . . . . . . . . . . . . 20 ((sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞) ↔ ((sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ* ∧ 0 ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))))
310303, 308, 309sylanbrc 586 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞))
311301, 310eqeltrd 2890 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞))
312 ifcl 4469 . . . . . . . . . . . . . . . . . 18 (((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
313311, 119, 312sylancl 589 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
314313adantr 484 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
315314fmpttd 6857 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)):ℝ⟶(0[,]+∞))
3161ffvelrnda 6829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℝ)
317316recnd 10661 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℂ)
318317abscld 14791 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(𝑓𝑡)) ∈ ℝ)
3195ffvelrnda 6829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℝ)
320319recnd 10661 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℂ)
321320abscld 14791 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(𝑔𝑡)) ∈ ℝ)
322 readdcl 10612 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((abs‘(𝑓𝑡)) ∈ ℝ ∧ (abs‘(𝑔𝑡)) ∈ ℝ) → ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))) ∈ ℝ)
323318, 321, 322syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))) ∈ ℝ)
324323anandirs 678 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))) ∈ ℝ)
325302adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ)
326 mulcl 10613 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((i ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (i · (𝑔𝑡)) ∈ ℂ)
3274, 320, 326sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (i · (𝑔𝑡)) ∈ ℂ)
328 abstri 14685 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ ((abs‘(𝑓𝑡)) + (abs‘(i · (𝑔𝑡)))))
329317, 327, 328syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ ((abs‘(𝑓𝑡)) + (abs‘(i · (𝑔𝑡)))))
330329anandirs 678 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ ((abs‘(𝑓𝑡)) + (abs‘(i · (𝑔𝑡)))))
331 absmul 14649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((i ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (abs‘(i · (𝑔𝑡))) = ((abs‘i) · (abs‘(𝑔𝑡))))
3324, 320, 331sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(i · (𝑔𝑡))) = ((abs‘i) · (abs‘(𝑔𝑡))))
333 absi 14641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (abs‘i) = 1
334333oveq1i 7146 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((abs‘i) · (abs‘(𝑔𝑡))) = (1 · (abs‘(𝑔𝑡)))
335332, 334eqtrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(i · (𝑔𝑡))) = (1 · (abs‘(𝑔𝑡))))
336321recnd 10661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(𝑔𝑡)) ∈ ℂ)
337336mulid2d 10651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (1 · (abs‘(𝑔𝑡))) = (abs‘(𝑔𝑡)))
338335, 337eqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(i · (𝑔𝑡))) = (abs‘(𝑔𝑡)))
339338adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔𝑡))) = (abs‘(𝑔𝑡)))
340339oveq2d 7152 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓𝑡)) + (abs‘(i · (𝑔𝑡)))) = ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))))
341330, 340breqtrd 5057 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))))
342318adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓𝑡)) ∈ ℝ)
343321adantll 713 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔𝑡)) ∈ ℝ)
344240adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
345250adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
346218adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ)
3471ffnd 6489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ dom ∫1𝑓 Fn ℝ)
348 fnfvelrn 6826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ran 𝑓)
349347, 348sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ran 𝑓)
350 elun1 4103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑡) ∈ ran 𝑓 → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
351349, 350syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
352351adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
353 fnfvima 6974 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑓𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
354224, 353mp3an1 1445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑓𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
355346, 352, 354syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
356 suprub 11592 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ (abs‘(𝑓𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘(𝑓𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
357345, 355, 356syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
3585ffnd 6489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑔 ∈ dom ∫1𝑔 Fn ℝ)
359 fnfvelrn 6826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ran 𝑔)
360358, 359sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ran 𝑔)
361 elun2 4104 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔𝑡) ∈ ran 𝑔 → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
362360, 361syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
363362adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
364 fnfvima 6974 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑔𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
365224, 364mp3an1 1445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑔𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
366346, 363, 365syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
367 suprub 11592 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ (abs‘(𝑔𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘(𝑔𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
368345, 366, 367syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
369342, 343, 344, 344, 357, 368le2addd 11251 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))) ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
370293, 324, 325, 341, 369letrd 10789 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
371301adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) = (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
372370, 371breqtrrd 5059 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
37350, 372sylan2 595 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
374 iftrue 4431 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) = (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
375374adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) = (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
376 iftrue 4431 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) = (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
377376adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) = (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
378373, 375, 3773brtr4d 5063 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))
379378ex 416 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)))
38058a1i 11 . . . . . . . . . . . . . . . . . . 19 𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0)
381 iffalse 4434 . . . . . . . . . . . . . . . . . . 19 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) = 0)
382 iffalse 4434 . . . . . . . . . . . . . . . . . . 19 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) = 0)
383380, 381, 3823brtr4d 5063 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))
384379, 383pm2.61d1 183 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))
385384ralrimivw 3150 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))
386 ovex 7169 . . . . . . . . . . . . . . . . . . 19 (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ V
387386, 64ifex 4473 . . . . . . . . . . . . . . . . . 18 if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈ V
388387a1i 11 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈ V)
389 eqidd 2799 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)))
39014, 71, 388, 74, 389ofrfval2 7410 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)))
391385, 390mpbird 260 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)))
392 itg2le 24353 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))))
393299, 315, 391, 392syl3anc 1368 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))))
394393adantr 484 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))))
395 mblvol 24144 . . . . . . . . . . . . . . . . 17 ((𝑢(,)𝑤) ∈ dom vol → (vol‘(𝑢(,)𝑤)) = (vol*‘(𝑢(,)𝑤)))
39634, 395ax-mp 5 . . . . . . . . . . . . . . . 16 (vol‘(𝑢(,)𝑤)) = (vol*‘(𝑢(,)𝑤))
397 ovolioo 24182 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (vol*‘(𝑢(,)𝑤)) = (𝑤𝑢))
398396, 397syl5eq 2845 . . . . . . . . . . . . . . 15 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (vol‘(𝑢(,)𝑤)) = (𝑤𝑢))
399 resubcl 10942 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℝ ∧ 𝑢 ∈ ℝ) → (𝑤𝑢) ∈ ℝ)
400399ancoms 462 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ) → (𝑤𝑢) ∈ ℝ)
4014003adant3 1129 . . . . . . . . . . . . . . 15 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (𝑤𝑢) ∈ ℝ)
402398, 401eqeltrd 2890 . . . . . . . . . . . . . 14 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (vol‘(𝑢(,)𝑤)) ∈ ℝ)
403 elrege0 12835 . . . . . . . . . . . . . . . . 17 (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞) ↔ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ ∧ 0 ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
404240, 307, 403sylanbrc 586 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞))
405 ge0addcl 12841 . . . . . . . . . . . . . . . 16 ((sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞) ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞)) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
406404, 404, 405syl2anc 587 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
407301, 406eqeltrd 2890 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
408 itg2const 24354 . . . . . . . . . . . . . . 15 (((𝑢(,)𝑤) ∈ dom vol ∧ (vol‘(𝑢(,)𝑤)) ∈ ℝ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) = ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
40934, 408mp3an1 1445 . . . . . . . . . . . . . 14 (((vol‘(𝑢(,)𝑤)) ∈ ℝ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) = ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
410402, 407, 409syl2anr 599 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) = ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
411394, 410breqtrd 5057 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
412411adantll 713 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
413412adantlr 714 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
41482ad3antlr 730 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
415402adantl 485 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (vol‘(𝑢(,)𝑤)) ∈ ℝ)
416263adantll 713 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
417416adantr 484 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
418414, 415, 417ledivmuld 12475 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤ (vol‘(𝑢(,)𝑤)) ↔ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤)))))
419413, 418mpbird 260 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤ (vol‘(𝑢(,)𝑤)))
420 abssubge0 14682 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (abs‘(𝑤𝑢)) = (𝑤𝑢))
421397, 420eqtr4d 2836 . . . . . . . . . . 11 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (vol*‘(𝑢(,)𝑤)) = (abs‘(𝑤𝑢)))
422396, 421syl5eq 2845 . . . . . . . . . 10 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (vol‘(𝑢(,)𝑤)) = (abs‘(𝑤𝑢)))
423422adantl 485 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (vol‘(𝑢(,)𝑤)) = (abs‘(𝑤𝑢)))
424419, 423breqtrd 5057 . . . . . . . 8 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤ (abs‘(𝑤𝑢)))
425292, 424syldan 594 . . . . . . 7 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤ (abs‘(𝑤𝑢)))
426425adantllr 718 . . . . . 6 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤ (abs‘(𝑤𝑢)))
427426adantlr 714 . . . . 5 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤ (abs‘(𝑤𝑢)))
428427adantr 484 . . . 4 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤ (abs‘(𝑤𝑢)))
429 simpr 488 . . . 4 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))))
430267, 280, 286, 428, 429lelttrd 10790 . . 3 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))))
43182adantl 485 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
432431ad3antrrr 729 . . . . 5 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
433126adantl 485 . . . . 5 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
434416adantlr 714 . . . . . 6 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
435434adantr 484 . . . . 5 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
436432, 433, 435ltdiv1d 12467 . . . 4 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) < (𝑦 / 2) ↔ ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
437436ad2antrr 725 . . 3 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) < (𝑦 / 2) ↔ ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
438430, 437mpbird 260 . 2 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) < (𝑦 / 2))
439198adantllr 718 . . . 4 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) < (𝑦 / 2))
4404393adantr3 1168 . . 3 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) < (𝑦 / 2))
441440adantr 484 . 2 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) < (𝑦 / 2))
44283, 204, 205, 205, 438, 441lt2addd 11255 1 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))) < ((𝑦 / 2) + (𝑦 / 2)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  ifcif 4425  {csn 4525   class class class wbr 5031   ↦ cmpt 5111   × cxp 5518  dom cdm 5520  ran crn 5521   “ cima 5523   ∘ ccom 5524  Fun wfun 6319   Fn wfn 6320  ⟶wf 6321  ‘cfv 6325  (class class class)co 7136   ∘f cof 7389   ∘r cofr 7390  Fincfn 8495  supcsup 8891  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530  ici 10531   + caddc 10532   · cmul 10534  +∞cpnf 10664  ℝ*cxr 10666   < clt 10667   ≤ cle 10668   − cmin 10862   / cdiv 11289  2c2 11683  ℝ+crp 12380  (,)cioo 12729  [,)cico 12731  [,]cicc 12732  abscabs 14588  vol*covol 24076  volcvol 24077  ∫1citg1 24229  ∫2citg2 24230  𝐿1cibl 24231  ∫citg 24232  0𝑝c0p 24283 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-inf2 9091  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-disj 4997  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-of 7391  df-ofr 7392  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-er 8275  df-map 8394  df-pm 8395  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fi 8862  df-sup 8893  df-inf 8894  df-oi 8961  df-dju 9317  df-card 9355  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11629  df-2 11691  df-3 11692  df-n0 11889  df-z 11973  df-uz 12235  df-q 12340  df-rp 12381  df-xneg 12498  df-xadd 12499  df-xmul 12500  df-ioo 12733  df-ico 12735  df-icc 12736  df-fz 12889  df-fzo 13032  df-fl 13160  df-seq 13368  df-exp 13429  df-hash 13690  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-rlim 14841  df-sum 15038  df-rest 16691  df-topgen 16712  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-top 21509  df-topon 21526  df-bases 21561  df-cmp 22002  df-ovol 24078  df-vol 24079  df-mbf 24233  df-itg1 24234  df-itg2 24235  df-0p 24284 This theorem is referenced by:  ftc1anclem8  35156
 Copyright terms: Public domain W3C validator