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

Theorem ftc1anclem7 33823
Description: Lemma for ftc1anc 33825. (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 23663 . . . . . . . . . . 11 (𝑓 ∈ dom ∫1𝑓:ℝ⟶ℝ)
21ffvelrnda 6502 . . . . . . . . . 10 ((𝑓 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℝ)
32recnd 10270 . . . . . . . . 9 ((𝑓 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℂ)
4 ax-icn 10197 . . . . . . . . . 10 i ∈ ℂ
5 i1ff 23663 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
65ffvelrnda 6502 . . . . . . . . . . 11 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℝ)
76recnd 10270 . . . . . . . . . 10 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℂ)
8 mulcl 10222 . . . . . . . . . 10 ((i ∈ ℂ ∧ (𝑔𝑥) ∈ ℂ) → (i · (𝑔𝑥)) ∈ ℂ)
94, 7, 8sylancr 567 . . . . . . . . 9 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (i · (𝑔𝑥)) ∈ ℂ)
10 addcl 10220 . . . . . . . . 9 (((𝑓𝑥) ∈ ℂ ∧ (i · (𝑔𝑥)) ∈ ℂ) → ((𝑓𝑥) + (i · (𝑔𝑥))) ∈ ℂ)
113, 9, 10syl2an 575 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑥 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑥 ∈ ℝ)) → ((𝑓𝑥) + (i · (𝑔𝑥))) ∈ ℂ)
1211anandirs 650 . . . . . . 7 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑓𝑥) + (i · (𝑔𝑥))) ∈ ℂ)
13 reex 10229 . . . . . . . . 9 ℝ ∈ V
1413a1i 11 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ℝ ∈ V)
152adantlr 686 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (𝑓𝑥) ∈ ℝ)
16 ovexd 6825 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (i · (𝑔𝑥)) ∈ V)
171feqmptd 6391 . . . . . . . . 9 (𝑓 ∈ dom ∫1𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
1817adantr 466 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓𝑥)))
1913a1i 11 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → ℝ ∈ V)
204a1i 11 . . . . . . . . . 10 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → i ∈ ℂ)
21 fconstmpt 5303 . . . . . . . . . . 11 (ℝ × {i}) = (𝑥 ∈ ℝ ↦ i)
2221a1i 11 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → (ℝ × {i}) = (𝑥 ∈ ℝ ↦ i))
235feqmptd 6391 . . . . . . . . . 10 (𝑔 ∈ dom ∫1𝑔 = (𝑥 ∈ ℝ ↦ (𝑔𝑥)))
2419, 20, 6, 22, 23offval2 7061 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → ((ℝ × {i}) ∘𝑓 · 𝑔) = (𝑥 ∈ ℝ ↦ (i · (𝑔𝑥))))
2524adantl 467 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((ℝ × {i}) ∘𝑓 · 𝑔) = (𝑥 ∈ ℝ ↦ (i · (𝑔𝑥))))
2614, 15, 16, 18, 25offval2 7061 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑓𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔)) = (𝑥 ∈ ℝ ↦ ((𝑓𝑥) + (i · (𝑔𝑥)))))
27 absf 14285 . . . . . . . . 9 abs:ℂ⟶ℝ
2827a1i 11 . . . . . . . 8 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → abs:ℂ⟶ℝ)
2928feqmptd 6391 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → abs = (𝑡 ∈ ℂ ↦ (abs‘𝑡)))
30 fveq2 6332 . . . . . . 7 (𝑡 = ((𝑓𝑥) + (i · (𝑔𝑥))) → (abs‘𝑡) = (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))
3112, 26, 29, 30fmptco 6539 . . . . . 6 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs ∘ (𝑓𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) = (𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥))))))
32 ftc1anclem3 33819 . . . . . 6 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs ∘ (𝑓𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ∈ dom ∫1)
3331, 32eqeltrrd 2851 . . . . 5 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥))))) ∈ dom ∫1)
34 ioombl 23553 . . . . 5 (𝑢(,)𝑤) ∈ dom vol
35 fveq2 6332 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑓𝑥) = (𝑓𝑡))
36 fveq2 6332 . . . . . . . . . . . . 13 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
3736oveq2d 6809 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (i · (𝑔𝑥)) = (i · (𝑔𝑡)))
3835, 37oveq12d 6811 . . . . . . . . . . 11 (𝑥 = 𝑡 → ((𝑓𝑥) + (i · (𝑔𝑥))) = ((𝑓𝑡) + (i · (𝑔𝑡))))
3938fveq2d 6336 . . . . . . . . . 10 (𝑥 = 𝑡 → (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))) = (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
40 eqid 2771 . . . . . . . . . 10 (𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥))))) = (𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))
41 fvex 6342 . . . . . . . . . 10 (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ V
4239, 40, 41fvmpt 6424 . . . . . . . . 9 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))‘𝑡) = (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
4342eqcomd 2777 . . . . . . . 8 (𝑡 ∈ ℝ → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) = ((𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))‘𝑡))
4443ifeq1d 4243 . . . . . . 7 (𝑡 ∈ ℝ → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) = if(𝑡 ∈ (𝑢(,)𝑤), ((𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))‘𝑡), 0))
4544mpteq2ia 4874 . . . . . 6 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥)))))‘𝑡), 0))
4645i1fres 23692 . . . . 5 (((𝑥 ∈ ℝ ↦ (abs‘((𝑓𝑥) + (i · (𝑔𝑥))))) ∈ dom ∫1 ∧ (𝑢(,)𝑤) ∈ dom vol) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1)
4733, 34, 46sylancl 566 . . . 4 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1)
48 breq2 4790 . . . . . . 7 ((abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) → (0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ↔ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
49 breq2 4790 . . . . . . 7 (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
50 elioore 12410 . . . . . . . 8 (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
51 eleq1w 2833 . . . . . . . . . . . 12 (𝑥 = 𝑡 → (𝑥 ∈ ℝ ↔ 𝑡 ∈ ℝ))
5251anbi2d 606 . . . . . . . . . . 11 (𝑥 = 𝑡 → (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ↔ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)))
5338eleq1d 2835 . . . . . . . . . . 11 (𝑥 = 𝑡 → (((𝑓𝑥) + (i · (𝑔𝑥))) ∈ ℂ ↔ ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ))
5452, 53imbi12d 333 . . . . . . . . . 10 (𝑥 = 𝑡 → ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ((𝑓𝑥) + (i · (𝑔𝑥))) ∈ ℂ) ↔ (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)))
5554, 12chvarv 2425 . . . . . . . . 9 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
5655absge0d 14391 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
5750, 56sylan2 572 . . . . . . 7 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
58 0le0 11312 . . . . . . . 8 0 ≤ 0
5958a1i 11 . . . . . . 7 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ 0)
6048, 49, 57, 59ifbothda 4262 . . . . . 6 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))
6160ralrimivw 3116 . . . . 5 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ∀𝑡 ∈ ℝ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))
62 ax-resscn 10195 . . . . . . . 8 ℝ ⊆ ℂ
6362a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ℝ ⊆ ℂ)
64 c0ex 10236 . . . . . . . . . 10 0 ∈ V
6541, 64ifex 4295 . . . . . . . . 9 if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ∈ V
66 eqid 2771 . . . . . . . . 9 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))
6765, 66fnmpti 6162 . . . . . . . 8 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) Fn ℝ
6867a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) Fn ℝ)
6963, 680pledm 23660 . . . . . 6 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (0𝑝𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ↔ (ℝ × {0}) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ 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 5303 . . . . . . . 8 (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
7372a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
74 eqidd 2772 . . . . . . 7 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
7514, 70, 71, 73, 74ofrfval2 7062 . . . . . 6 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((ℝ × {0}) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
7669, 75bitrd 268 . . . . 5 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (0𝑝𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
7761, 76mpbird 247 . . . 4 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0𝑝𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)))
78 itg2itg1 23723 . . . . 5 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1 ∧ 0𝑝𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))))
79 itg1cl 23672 . . . . . 6 ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
8079adantr 466 . . . . 5 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1 ∧ 0𝑝𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) → (∫1‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
8178, 80eqeltrd 2850 . . . 4 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∈ dom ∫1 ∧ 0𝑝𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
8247, 77, 81syl2anc 565 . . 3 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
8382ad6antlr 714 . 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 750 . . . . 5 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)))
85 ftc1anc.a . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
8685rexrd 10291 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ*)
87 ftc1anc.b . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℝ)
8887rexrd 10291 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ*)
8986, 88jca 495 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 ∈ ℝ*𝐵 ∈ ℝ*))
90 df-icc 12387 . . . . . . . . . . . . . . . . . . . . . 22 [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥𝑡𝑡𝑦)})
9190elixx3g 12393 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑢 ∈ ℝ*) ∧ (𝐴𝑢𝑢𝐵)))
9291simprbi 478 . . . . . . . . . . . . . . . . . . . 20 (𝑢 ∈ (𝐴[,]𝐵) → (𝐴𝑢𝑢𝐵))
9392simpld 476 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ (𝐴[,]𝐵) → 𝐴𝑢)
9490elixx3g 12393 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝐴𝑤𝑤𝐵)))
9594simprbi 478 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ (𝐴[,]𝐵) → (𝐴𝑤𝑤𝐵))
9695simprd 477 . . . . . . . . . . . . . . . . . . 19 (𝑤 ∈ (𝐴[,]𝐵) → 𝑤𝐵)
9793, 96anim12i 592 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴𝑢𝑤𝐵))
98 ioossioo 12471 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) ∧ (𝐴𝑢𝑤𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
9989, 97, 98syl2an 575 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
100 ftc1anc.s . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
101100adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
10299, 101sstrd 3762 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
1031023adantr3 1176 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑢(,)𝑤) ⊆ 𝐷)
104103sselda 3752 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡𝐷)
105 ftc1anc.f . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝐷⟶ℂ)
106105ffvelrnda 6502 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
107106adantlr 686 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
108104, 107syldan 571 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
109108adantllr 690 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹𝑡) ∈ ℂ)
11055adantll 685 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
11150, 110sylan2 572 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
112111adantlr 686 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
113109, 112subcld 10594 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
114113abscld 14383 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
115114rexrd 10291 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
116113absge0d 14391 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
117 elxrge0 12488 . . . . . . . . 9 ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
118115, 116, 117sylanbrc 564 . . . . . . . 8 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞))
119 0e0iccpnf 12490 . . . . . . . . 9 0 ∈ (0[,]+∞)
120119a1i 11 . . . . . . . 8 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
121118, 120ifclda 4259 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
122121adantr 466 . . . . . 6 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
123 eqid 2771 . . . . . 6 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))
124122, 123fmptd 6527 . . . . 5 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞))
12584, 124sylan 561 . . . 4 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞))
126 rpre 12042 . . . . . 6 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
127126rehalfcld 11481 . . . . 5 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
128127ad2antlr 698 . . . 4 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑦 / 2) ∈ ℝ)
129 simpll 742 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)))
130102sselda 3752 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡𝐷)
131130adantllr 690 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡𝐷)
132106adantlr 686 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
133 ftc1anc.d . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐷 ⊆ ℝ)
134133sselda 3752 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑡𝐷) → 𝑡 ∈ ℝ)
135134adantlr 686 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → 𝑡 ∈ ℝ)
136135, 110syldan 571 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ)
137132, 136subcld 10594 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → ((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
138137abscld 14383 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
139138rexrd 10291 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
140139adantlr 686 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
141131, 140syldan 571 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
142137absge0d 14391 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
143142adantlr 686 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
144131, 143syldan 571 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
145141, 144, 117sylanbrc 564 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞))
146119a1i 11 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
147145, 146ifclda 4259 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
148147adantr 466 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ (0[,]+∞))
149148, 123fmptd 6527 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞))
150 itg2cl 23719 . . . . . . . . . 10 ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
151149, 150syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
152129, 151sylan 561 . . . . . . . 8 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ*)
153 0cnd 10235 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ ℂ)
154106, 153ifclda 4259 . . . . . . . . . . . . . . . 16 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
155 subcl 10482 . . . . . . . . . . . . . . . 16 ((if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ ∧ ((𝑓𝑡) + (i · (𝑔𝑡))) ∈ ℂ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
156154, 55, 155syl2an 575 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ)) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
157156anassrs 458 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℂ)
158157abscld 14383 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ)
159158rexrd 10291 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ*)
160157absge0d 14391 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
161 elxrge0 12488 . . . . . . . . . . . 12 ((abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
162159, 160, 161sylanbrc 564 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ (0[,]+∞))
163 eqid 2771 . . . . . . . . . . 11 (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
164162, 163fmptd 6527 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))):ℝ⟶(0[,]+∞))
165 itg2cl 23719 . . . . . . . . . 10 ((𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) ∈ ℝ*)
166164, 165syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) ∈ ℝ*)
167166ad3antrrr 701 . . . . . . . 8 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) ∈ ℝ*)
168 rphalfcl 12061 . . . . . . . . . 10 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
169168rpxrd 12076 . . . . . . . . 9 (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ*)
170169ad2antlr 698 . . . . . . . 8 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑦 / 2) ∈ ℝ*)
171164adantr 466 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))):ℝ⟶(0[,]+∞))
172 breq1 4789 . . . . . . . . . . . . 13 ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) → ((abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
173 breq1 4789 . . . . . . . . . . . . 13 (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) → (0 ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
174138leidd 10796 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
175 iftrue 4231 . . . . . . . . . . . . . . . . . . 19 (𝑡𝐷 → if(𝑡𝐷, (𝐹𝑡), 0) = (𝐹𝑡))
176175fvoveq1d 6815 . . . . . . . . . . . . . . . . . 18 (𝑡𝐷 → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
177176adantl 467 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) = (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
178174, 177breqtrrd 4814 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
179178adantlr 686 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡𝐷) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
180131, 179syldan 571 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
181180adantlr 686 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
182160adantlr 686 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
183182adantr 466 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
184172, 173, 181, 183ifbothda 4262 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
185184ralrimiva 3115 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))
18613a1i 11 . . . . . . . . . . . . 13 (𝜑 → ℝ ∈ V)
187 fvex 6342 . . . . . . . . . . . . . . 15 (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ V
188187, 64ifex 4295 . . . . . . . . . . . . . 14 if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ V
189188a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ∈ V)
190 fvexd 6344 . . . . . . . . . . . . 13 ((𝜑𝑡 ∈ ℝ) → (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))) ∈ V)
191 eqidd 2772 . . . . . . . . . . . . 13 (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)))
192 eqidd 2772 . . . . . . . . . . . . 13 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
193186, 189, 190, 191, 192ofrfval2 7062 . . . . . . . . . . . 12 (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
194193ad2antrr 697 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0) ≤ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
195185, 194mpbird 247 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))))
196 itg2le 23726 . . . . . . . . . 10 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡)))))):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))))
197149, 171, 195, 196syl3anc 1476 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))))
198129, 197sylan 561 . . . . . . . 8 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))))
199 simpllr 752 . . . . . . . 8 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2))
200152, 167, 170, 198, 199xrlelttrd 12196 . . . . . . 7 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) < (𝑦 / 2))
201 xrltle 12187 . . . . . . . 8 (((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ* ∧ (𝑦 / 2) ∈ ℝ*) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (𝑦 / 2)))
202152, 170, 201syl2anc 565 . . . . . . 7 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (𝑦 / 2)))
203200, 202mpd 15 . . . . . 6 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (𝑦 / 2))
204203adantllr 690 . . . . 5 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (𝑦 / 2))
2052043adantr3 1176 . . . 4 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (𝑦 / 2))
206 itg2lecl 23725 . . . 4 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑦 / 2) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ≤ (𝑦 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ)
207125, 128, 205, 206syl3anc 1476 . . 3 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) ∈ ℝ)
208207adantr 466 . 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))) ∈ ℝ)
209127ad3antlr 702 . 2 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (𝑦 / 2) ∈ ℝ)
21082adantr 466 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
211 2rp 12040 . . . . . . . . 9 2 ∈ ℝ+
212 imassrn 5618 . . . . . . . . . . . . . . . 16 (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ran abs
213 frn 6193 . . . . . . . . . . . . . . . . 17 (abs:ℂ⟶ℝ → ran abs ⊆ ℝ)
21427, 213ax-mp 5 . . . . . . . . . . . . . . . 16 ran abs ⊆ ℝ
215212, 214sstri 3761 . . . . . . . . . . . . . . 15 (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ
216215a1i 11 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ)
217 frn 6193 . . . . . . . . . . . . . . . . . . . 20 (𝑓:ℝ⟶ℝ → ran 𝑓 ⊆ ℝ)
2181, 217syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
219218adantr 466 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ran 𝑓 ⊆ ℝ)
220 frn 6193 . . . . . . . . . . . . . . . . . . . 20 (𝑔:ℝ⟶ℝ → ran 𝑔 ⊆ ℝ)
2215, 220syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ)
222221adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ran 𝑔 ⊆ ℝ)
223219, 222unssd 3940 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ)
224223, 62syl6ss 3764 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ)
225 i1f0rn 23669 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓)
226 elun1 3931 . . . . . . . . . . . . . . . . . 18 (0 ∈ ran 𝑓 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
227225, 226syl 17 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
228227adantr 466 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
229 ffn 6185 . . . . . . . . . . . . . . . . . 18 (abs:ℂ⟶ℝ → abs Fn ℂ)
23027, 229ax-mp 5 . . . . . . . . . . . . . . . . 17 abs Fn ℂ
231 fnfvima 6639 . . . . . . . . . . . . . . . . 17 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
232230, 231mp3an1 1559 . . . . . . . . . . . . . . . 16 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
233224, 228, 232syl2anc 565 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
234 ne0i 4069 . . . . . . . . . . . . . . 15 ((abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅)
235233, 234syl 17 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅)
236 ffun 6188 . . . . . . . . . . . . . . . . 17 (abs:ℂ⟶ℝ → Fun abs)
23727, 236ax-mp 5 . . . . . . . . . . . . . . . 16 Fun abs
238 i1frn 23664 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
239 i1frn 23664 . . . . . . . . . . . . . . . . 17 (𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin)
240 unfi 8383 . . . . . . . . . . . . . . . . 17 ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
241238, 239, 240syl2an 575 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
242 imafi 8415 . . . . . . . . . . . . . . . 16 ((Fun abs ∧ (ran 𝑓 ∪ ran 𝑔) ∈ Fin) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
243237, 241, 242sylancr 567 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
244 fimaxre2 11171 . . . . . . . . . . . . . . 15 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥)
245215, 243, 244sylancr 567 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥)
246 suprcl 11185 . . . . . . . . . . . . . 14 (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
247216, 235, 245, 246syl3anc 1476 . . . . . . . . . . . . 13 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
248247adantr 466 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
249 0red 10243 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈ ℝ)
250224sselda 3752 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → 𝑟 ∈ ℂ)
251250abscld 14383 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ ℝ)
252251adantrr 688 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈ ℝ)
253 absgt0 14272 . . . . . . . . . . . . . . . 16 (𝑟 ∈ ℂ → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
254250, 253syl 17 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
255254biimpa 462 . . . . . . . . . . . . . 14 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) ∧ 𝑟 ≠ 0) → 0 < (abs‘𝑟))
256255anasss 457 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < (abs‘𝑟))
257216, 235, 2453jca 1122 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
258257adantr 466 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
259 fnfvima 6639 . . . . . . . . . . . . . . . . 17 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
260230, 259mp3an1 1559 . . . . . . . . . . . . . . . 16 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
261224, 260sylan 561 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
262 suprub 11186 . . . . . . . . . . . . . . 15 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
263258, 261, 262syl2anc 565 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
264263adantrr 688 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
265249, 252, 248, 256, 264ltletrd 10399 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
266248, 265elrpd 12072 . . . . . . . . . . 11 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+)
267266rexlimdvaa 3180 . . . . . . . . . 10 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+))
268267imp 393 . . . . . . . . 9 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+)
269 rpmulcl 12058 . . . . . . . . 9 ((2 ∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
270211, 268, 269sylancr 567 . . . . . . . 8 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
271210, 270rerpdivcld 12106 . . . . . . 7 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
272271adantll 685 . . . . . 6 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
273272adantlr 686 . . . . 5 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
274273ad3antrrr 701 . . . 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 𝑔)), ℝ, < ))) ∈ ℝ)
275 simp-4l 760 . . . . . 6 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑)
276 iccssre 12460 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
27785, 87, 276syl2anc 565 . . . . . . . . . . . 12 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
278277, 62syl6ss 3764 . . . . . . . . . . 11 (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
279278sselda 3752 . . . . . . . . . 10 ((𝜑𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ)
280278sselda 3752 . . . . . . . . . 10 ((𝜑𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ)
281 subcl 10482 . . . . . . . . . 10 ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (𝑤𝑢) ∈ ℂ)
282279, 280, 281syl2anr 576 . . . . . . . . 9 (((𝜑𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑𝑤 ∈ (𝐴[,]𝐵))) → (𝑤𝑢) ∈ ℂ)
283282anandis 649 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑤𝑢) ∈ ℂ)
284283abscld 14383 . . . . . . 7 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤𝑢)) ∈ ℝ)
2852843adantr3 1176 . . . . . 6 ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘(𝑤𝑢)) ∈ ℝ)
286275, 285sylan 561 . . . . 5 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (abs‘(𝑤𝑢)) ∈ ℝ)
287286adantr 466 . . . 4 (((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) ∧ (abs‘(𝑤𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (abs‘(𝑤𝑢)) ∈ ℝ)
288 rpdivcl 12059 . . . . . . . . 9 (((𝑦 / 2) ∈ ℝ+ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
289168, 270, 288syl2anr 576 . . . . . . . 8 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
290289rpred 12075 . . . . . . 7 ((((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
291290adantlll 689 . . . . . 6 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
292291adantllr 690 . . . . 5 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ)
293292ad2antrr 697 . . . 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 𝑔)), ℝ, < ))) ∈ ℝ)
294277sseld 3751 . . . . . . . . . . 11 (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) → 𝑢 ∈ ℝ))
295277sseld 3751 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ∈ ℝ))
296 idd 24 . . . . . . . . . . 11 (𝜑 → (𝑢𝑤𝑢𝑤))
297294, 295, 2963anim123d 1554 . . . . . . . . . 10 (𝜑 → ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤) → (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)))
298297ad2antrr 697 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤) → (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)))
299298imp 393 . . . . . . . 8 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤))
30055abscld 14383 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ)
301300rexrd 10291 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ*)
302 elxrge0 12488 . . . . . . . . . . . . . . . . . 18 ((abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ (0[,]+∞) ↔ ((abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝑓𝑡) + (i · (𝑔𝑡))))))
303301, 56, 302sylanbrc 564 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ (0[,]+∞))
304 ifcl 4269 . . . . . . . . . . . . . . . . 17 (((abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ∈ (0[,]+∞))
305303, 119, 304sylancl 566 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ∈ (0[,]+∞))
306305, 66fmptd 6527 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)):ℝ⟶(0[,]+∞))
307247recnd 10270 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℂ)
3083072timesd 11477 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) = (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
309247, 247readdcld 10271 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ)
310309rexrd 10291 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ*)
311 abs0 14233 . . . . . . . . . . . . . . . . . . . . . . 23 (abs‘0) = 0
312311, 233syl5eqelr 2855 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
313 suprub 11186 . . . . . . . . . . . . . . . . . . . . . 22 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ 0 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → 0 ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
314257, 312, 313syl2anc 565 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
315247, 247, 314, 314addge0d 10805 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → 0 ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
316 elxrge0 12488 . . . . . . . . . . . . . . . . . . . 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 𝑔)), ℝ, < ))))
317310, 315, 316sylanbrc 564 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞))
318308, 317eqeltrd 2850 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞))
319 ifcl 4269 . . . . . . . . . . . . . . . . . 18 (((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
320318, 119, 319sylancl 566 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
321320adantr 466 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
322 eqid 2771 . . . . . . . . . . . . . . . 16 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))
323321, 322fmptd 6527 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)):ℝ⟶(0[,]+∞))
3241ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℝ)
325324recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ℂ)
326325abscld 14383 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(𝑓𝑡)) ∈ ℝ)
3275ffvelrnda 6502 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℝ)
328327recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℂ)
329328abscld 14383 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(𝑔𝑡)) ∈ ℝ)
330 readdcl 10221 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((abs‘(𝑓𝑡)) ∈ ℝ ∧ (abs‘(𝑔𝑡)) ∈ ℝ) → ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))) ∈ ℝ)
331326, 329, 330syl2an 575 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))) ∈ ℝ)
332331anandirs 650 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))) ∈ ℝ)
333309adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ)
334 mulcl 10222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((i ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (i · (𝑔𝑡)) ∈ ℂ)
3354, 328, 334sylancr 567 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (i · (𝑔𝑡)) ∈ ℂ)
336 abstri 14278 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓𝑡) ∈ ℂ ∧ (i · (𝑔𝑡)) ∈ ℂ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ ((abs‘(𝑓𝑡)) + (abs‘(i · (𝑔𝑡)))))
337325, 335, 336syl2an 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ ((abs‘(𝑓𝑡)) + (abs‘(i · (𝑔𝑡)))))
338337anandirs 650 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ ((abs‘(𝑓𝑡)) + (abs‘(i · (𝑔𝑡)))))
339 absmul 14242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((i ∈ ℂ ∧ (𝑔𝑡) ∈ ℂ) → (abs‘(i · (𝑔𝑡))) = ((abs‘i) · (abs‘(𝑔𝑡))))
3404, 328, 339sylancr 567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(i · (𝑔𝑡))) = ((abs‘i) · (abs‘(𝑔𝑡))))
341 absi 14234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (abs‘i) = 1
342341oveq1i 6803 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((abs‘i) · (abs‘(𝑔𝑡))) = (1 · (abs‘(𝑔𝑡)))
343340, 342syl6eq 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(i · (𝑔𝑡))) = (1 · (abs‘(𝑔𝑡))))
344329recnd 10270 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(𝑔𝑡)) ∈ ℂ)
345344mulid2d 10260 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (1 · (abs‘(𝑔𝑡))) = (abs‘(𝑔𝑡)))
346343, 345eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (abs‘(i · (𝑔𝑡))) = (abs‘(𝑔𝑡)))
347346adantll 685 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔𝑡))) = (abs‘(𝑔𝑡)))
348347oveq2d 6809 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓𝑡)) + (abs‘(i · (𝑔𝑡)))) = ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))))
349338, 348breqtrd 4812 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))))
350326adantlr 686 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓𝑡)) ∈ ℝ)
351329adantll 685 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔𝑡)) ∈ ℝ)
352247adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
353257adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥))
354224adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ)
355 ffn 6185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑓:ℝ⟶ℝ → 𝑓 Fn ℝ)
3561, 355syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ dom ∫1𝑓 Fn ℝ)
357 fnfvelrn 6499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ran 𝑓)
358356, 357sylan 561 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ ran 𝑓)
359 elun1 3931 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓𝑡) ∈ ran 𝑓 → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
360358, 359syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
361360adantlr 686 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
362 fnfvima 6639 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑓𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
363230, 362mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ (𝑓𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑓𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
364354, 361, 363syl2anc 565 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
365 suprub 11186 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ (abs‘(𝑓𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘(𝑓𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
366353, 364, 365syl2anc 565 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
367 ffn 6185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑔:ℝ⟶ℝ → 𝑔 Fn ℝ)
3685, 367syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑔 ∈ dom ∫1𝑔 Fn ℝ)
369 fnfvelrn 6499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ran 𝑔)
370368, 369sylan 561 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ran 𝑔)
371 elun2 3932 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔𝑡) ∈ ran 𝑔 → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
372370, 371syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
373372adantll 685 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
374 fnfvima 6639 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑔𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
375230, 374mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ (𝑔𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑔𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
376354, 373, 375syl2anc 565 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
377 suprub 11186 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦𝑥) ∧ (abs‘(𝑔𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘(𝑔𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
378353, 376, 377syl2anc 565 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
379350, 351, 352, 352, 366, 378le2addd 10848 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓𝑡)) + (abs‘(𝑔𝑡))) ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
380300, 332, 333, 349, 379letrd 10396 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
381308adantr 466 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) = (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
382380, 381breqtrrd 4814 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
38350, 382sylan2 572 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))) ≤ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
384 iftrue 4231 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) = (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
385384adantl 467 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) = (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))))
386 iftrue 4231 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) = (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
387386adantl 467 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) = (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
388383, 385, 3873brtr4d 4818 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))
389388ex 397 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)))
39058a1i 11 . . . . . . . . . . . . . . . . . . 19 𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0)
391 iffalse 4234 . . . . . . . . . . . . . . . . . . 19 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) = 0)
392 iffalse 4234 . . . . . . . . . . . . . . . . . . 19 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) = 0)
393390, 391, 3923brtr4d 4818 . . . . . . . . . . . . . . . . . 18 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))
394389, 393pm2.61d1 172 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))
395394ralrimivw 3116 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))
396 ovex 6823 . . . . . . . . . . . . . . . . . . 19 (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ V
397396, 64ifex 4295 . . . . . . . . . . . . . . . . . 18 if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈ V
398397a1i 11 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈ V)
399 eqidd 2772 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)))
40014, 71, 398, 74, 399ofrfval2 7062 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)))
401395, 400mpbird 247 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)))
402 itg2le 23726 . . . . . . . . . . . . . . 15 (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))))
403306, 323, 401, 402syl3anc 1476 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))))
404403adantr 466 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))))
405 mblvol 23518 . . . . . . . . . . . . . . . . 17 ((𝑢(,)𝑤) ∈ dom vol → (vol‘(𝑢(,)𝑤)) = (vol*‘(𝑢(,)𝑤)))
40634, 405ax-mp 5 . . . . . . . . . . . . . . . 16 (vol‘(𝑢(,)𝑤)) = (vol*‘(𝑢(,)𝑤))
407 ovolioo 23556 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (vol*‘(𝑢(,)𝑤)) = (𝑤𝑢))
408406, 407syl5eq 2817 . . . . . . . . . . . . . . 15 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (vol‘(𝑢(,)𝑤)) = (𝑤𝑢))
409 resubcl 10547 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ℝ ∧ 𝑢 ∈ ℝ) → (𝑤𝑢) ∈ ℝ)
410409ancoms 455 . . . . . . . . . . . . . . . 16 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ) → (𝑤𝑢) ∈ ℝ)
4114103adant3 1126 . . . . . . . . . . . . . . 15 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (𝑤𝑢) ∈ ℝ)
412408, 411eqeltrd 2850 . . . . . . . . . . . . . 14 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (vol‘(𝑢(,)𝑤)) ∈ ℝ)
413 elrege0 12485 . . . . . . . . . . . . . . . . 17 (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞) ↔ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ ∧ 0 ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
414247, 314, 413sylanbrc 564 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞))
415 ge0addcl 12491 . . . . . . . . . . . . . . . 16 ((sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞) ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞)) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
416414, 414, 415syl2anc 565 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
417308, 416eqeltrd 2850 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
418 itg2const 23727 . . . . . . . . . . . . . . 15 (((𝑢(,)𝑤) ∈ dom vol ∧ (vol‘(𝑢(,)𝑤)) ∈ ℝ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) = ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
41934, 418mp3an1 1559 . . . . . . . . . . . . . 14 (((vol‘(𝑢(,)𝑤)) ∈ ℝ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) = ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
420412, 417, 419syl2anr 576 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) = ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
421404, 420breqtrd 4812 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
422421adantll 685 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
423422adantlr 686 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ≤ ((2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) · (vol‘(𝑢(,)𝑤))))
42482ad3antlr 702 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
425412adantl 467 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (vol‘(𝑢(,)𝑤)) ∈ ℝ)
426270adantll 685 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
427426adantr 466 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
428424, 425, 427ledivmuld 12128 . . . . . . . . . 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‘(𝑢(,)𝑤)))))
429423, 428mpbird 247 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤ (vol‘(𝑢(,)𝑤)))
430 abssubge0 14275 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (abs‘(𝑤𝑢)) = (𝑤𝑢))
431407, 430eqtr4d 2808 . . . . . . . . . . 11 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (vol*‘(𝑢(,)𝑤)) = (abs‘(𝑤𝑢)))
432406, 431syl5eq 2817 . . . . . . . . . 10 ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤) → (vol‘(𝑢(,)𝑤)) = (abs‘(𝑤𝑢)))
433432adantl 467 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → (vol‘(𝑢(,)𝑤)) = (abs‘(𝑤𝑢)))
434429, 433breqtrd 4812 . . . . . . . 8 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤ (abs‘(𝑤𝑢)))
435299, 434syldan 571 . . . . . . 7 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤ (abs‘(𝑤𝑢)))
436435adantllr 690 . . . . . 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‘(𝑤𝑢)))
437436adantlr 686 . . . . 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‘(𝑤𝑢)))
438437adantr 466 . . . 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‘(𝑤𝑢)))
439 simpr 471 . . . 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 𝑔)), ℝ, < ))))
440274, 287, 293, 438, 439lelttrd 10397 . . 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 𝑔)), ℝ, < ))))
44182adantl 467 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
442441ad3antrrr 701 . . . . 5 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓𝑡) + (i · (𝑔𝑡)))), 0))) ∈ ℝ)
443127adantl 467 . . . . 5 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
444426adantlr 686 . . . . . 6 ((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
445444adantr 466 . . . . 5 (((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
446442, 443, 445ltdiv1d 12120 . . . 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 𝑔)), ℝ, < )))))
447446ad2antrr 697 . . 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 𝑔)), ℝ, < )))))
448440, 447mpbird 247 . 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))
449200adantllr 690 . . . 4 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) < (𝑦 / 2))
4504493adantr3 1176 . . 3 ((((((𝜑 ∧ (𝑓 ∈ dom ∫1𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡𝐷, (𝐹𝑡), 0) − ((𝑓𝑡) + (i · (𝑔𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹𝑡) − ((𝑓𝑡) + (i · (𝑔𝑡))))), 0))) < (𝑦 / 2))
451450adantr 466 . 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))
45283, 208, 209, 209, 448, 451lt2addd 10852 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 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  Vcvv 3351  cun 3721  wss 3723  c0 4063  ifcif 4225  {csn 4316   class class class wbr 4786  cmpt 4863   × cxp 5247  dom cdm 5249  ran crn 5250  cima 5252  ccom 5253  Fun wfun 6025   Fn wfn 6026  wf 6027  cfv 6031  (class class class)co 6793  𝑓 cof 7042  𝑟 cofr 7043  Fincfn 8109  supcsup 8502  cc 10136  cr 10137  0cc0 10138  1c1 10139  ici 10140   + caddc 10141   · cmul 10143  +∞cpnf 10273  *cxr 10275   < clt 10276  cle 10277  cmin 10468   / cdiv 10886  2c2 11272  +crp 12035  (,)cioo 12380  [,)cico 12382  [,]cicc 12383  abscabs 14182  vol*covol 23450  volcvol 23451  1citg1 23603  2citg2 23604  𝐿1cibl 23605  citg 23606  0𝑝c0p 23656
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216  ax-addf 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-disj 4755  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-ofr 7045  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-z 11580  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ioo 12384  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-rlim 14428  df-sum 14625  df-rest 16291  df-topgen 16312  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-top 20919  df-topon 20936  df-bases 20971  df-cmp 21411  df-ovol 23452  df-vol 23453  df-mbf 23607  df-itg1 23608  df-itg2 23609  df-0p 23657
This theorem is referenced by:  ftc1anclem8  33824
  Copyright terms: Public domain W3C validator