Theorem ftc1anclem8 36568

Description: Lemma for ftc1anc 36569. (Contributed by Brendan Leahy, 29-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
ftc1anclem8	⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < 𝑦)

Distinct variable groups:   𝑓,𝑔,𝑟,𝑡,𝑢,𝑤,𝑥,𝑦,𝐴   𝐵,𝑓,𝑔,𝑟,𝑡,𝑢,𝑤,𝑥,𝑦   𝐷,𝑓,𝑔,𝑟,𝑡,𝑢,𝑤,𝑥,𝑦   𝑓,𝐹,𝑔,𝑟,𝑡,𝑢,𝑤,𝑥,𝑦   𝜑,𝑓,𝑔,𝑟,𝑡,𝑢,𝑤,𝑥,𝑦   𝑓,𝐺,𝑔,𝑟,𝑢,𝑤,𝑦

Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1anclem8

Step	Hyp	Ref	Expression
1		ftc1anc.g	. . 3 ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)
2		ftc1anc.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		ftc1anc.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4		ftc1anc.le	. . 3 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
5		ftc1anc.s	. . 3 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
6		ftc1anc.d	. . 3 ⊢ (𝜑 → 𝐷 ⊆ ℝ)
7		ftc1anc.i	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝐿1)
8		ftc1anc.f	. . 3 ⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
9	1, 2, 3, 4, 5, 6, 7, 8	ftc1anclem7 36567	. 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‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) < ((𝑦 / 2) + (𝑦 / 2)))
10		simplll 774	. . . 4 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
11		3simpa 1149	. . . 4 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤) → (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)))
12		ioossre 13385	. . . . . . . . 9 ⊢ (𝑢(,)𝑤) ⊆ ℝ
13	12	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑢(,)𝑤) ⊆ ℝ)
14		rembl 25057	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
15	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ℝ ∈ dom vol)
16		fvex 6905	. . . . . . . . . 10 ⊢ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ V
17		c0ex 11208	. . . . . . . . . 10 ⊢ 0 ∈ V
18	16, 17	ifex 4579	. . . . . . . . 9 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V
19	18	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
20		eldifn 4128	. . . . . . . . . 10 ⊢ (𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤)) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
21	20	adantl 483	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤))) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
22	21	iffalsed 4540	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
23		iftrue 4535	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
24	23	mpteq2ia 5252	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
25		resmpt 6038	. . . . . . . . . . . 12 ⊢ ((𝑢(,)𝑤) ⊆ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
26	12, 25	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
27	24, 26	eqtr4i 2764	. . . . . . . . . 10 ⊢ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤))
28		i1ff 25193	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
29	28	ffvelcdmda 7087	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
30	29	recnd 11242	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℂ)
31		ax-icn 11169	. . . . . . . . . . . . . . . . 17 ⊢ i ∈ ℂ
32		i1ff 25193	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
33	32	ffvelcdmda 7087	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
34	33	recnd 11242	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
35		mulcl 11194	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ)
36	31, 34, 35	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
37		addcl 11192	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
38	30, 36, 37	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
39	38	anandirs 678	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
40		reex 11201	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
41	40	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ℝ ∈ V)
42	29	adantlr 714	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
43	36	adantll 713	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
44	28	feqmptd 6961	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ dom ∫1 → 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
45	44	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
46	40	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → ℝ ∈ V)
47	31	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → i ∈ ℂ)
48		fconstmpt 5739	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i)
49	48	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i))
50	32	feqmptd 6961	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡)))
51	46, 47, 33, 49, 50	offval2 7690	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ dom ∫1 → ((ℝ × {i}) ∘f · 𝑔) = (𝑡 ∈ ℝ ↦ (i · (𝑔‘𝑡))))
52	51	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((ℝ × {i}) ∘f · 𝑔) = (𝑡 ∈ ℝ ↦ (i · (𝑔‘𝑡))))
53	41, 42, 43, 45, 52	offval2 7690	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔)) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
54		absf 15284	. . . . . . . . . . . . . . . 16 ⊢ abs:ℂ⟶ℝ
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → abs:ℂ⟶ℝ)
56	55	feqmptd 6961	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
57		fveq2 6892	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) → (abs‘𝑥) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
58	39, 53, 56, 57	fmptco 7127	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) = (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
59		ftc1anclem3 36563	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ∈ dom ∫1)
60	58, 59	eqeltrrd 2835	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ dom ∫1)
61		i1fmbf 25192	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn)
62	60, 61	syl 17	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn)
63		ioombl 25082	. . . . . . . . . . 11 ⊢ (𝑢(,)𝑤) ∈ dom vol
64		mbfres 25161	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn ∧ (𝑢(,)𝑤) ∈ dom vol) → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) ∈ MblFn)
65	62, 63, 64	sylancl 587	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) ∈ MblFn)
66	27, 65	eqeltrid 2838	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
67	66	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
68	13, 15, 19, 22, 67	mbfss 25163	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
69	68	adantr 482	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
70	39	abscld 15383	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
71	39	absge0d 15391	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
72		elrege0 13431	. . . . . . . . . 10 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ↔ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
73	70, 71, 72	sylanbrc 584	. . . . . . . . 9 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞))
74		0e0icopnf 13435	. . . . . . . . 9 ⊢ 0 ∈ (0[,)+∞)
75		ifcl 4574	. . . . . . . . 9 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
76	73, 74, 75	sylancl 587	. . . . . . . 8 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
77	76	fmpttd 7115	. . . . . . 7 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
78	77	ad2antlr 726	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
79	70	rexrd 11264	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ*)
80		elxrge0 13434	. . . . . . . . . . 11 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ↔ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
81	79, 71, 80	sylanbrc 584	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞))
82		0e0iccpnf 13436	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]+∞)
83		ifcl 4574	. . . . . . . . . 10 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
84	81, 82, 83	sylancl 587	. . . . . . . . 9 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
85	84	fmpttd 7115	. . . . . . . 8 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
86	85	ad2antlr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
87		ifcl 4574	. . . . . . . . . . 11 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
88	81, 82, 87	sylancl 587	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
89	88	fmpttd 7115	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
90		ffn 6718	. . . . . . . . . . . . . . 15 ⊢ (𝑓:ℝ⟶ℝ → 𝑓 Fn ℝ)
91		frn 6725	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:ℝ⟶ℝ → ran 𝑓 ⊆ ℝ)
92		ax-resscn 11167	. . . . . . . . . . . . . . . 16 ⊢ ℝ ⊆ ℂ
93	91, 92	sstrdi 3995	. . . . . . . . . . . . . . 15 ⊢ (𝑓:ℝ⟶ℝ → ran 𝑓 ⊆ ℂ)
94		ffn 6718	. . . . . . . . . . . . . . . . 17 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ)
95	54, 94	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ abs Fn ℂ
96		fnco 6668	. . . . . . . . . . . . . . . 16 ⊢ ((abs Fn ℂ ∧ 𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ) → (abs ∘ 𝑓) Fn ℝ)
97	95, 96	mp3an1 1449	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ) → (abs ∘ 𝑓) Fn ℝ)
98	90, 93, 97	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝑓:ℝ⟶ℝ → (abs ∘ 𝑓) Fn ℝ)
99	28, 98	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ 𝑓) Fn ℝ)
100	99	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑓) Fn ℝ)
101		ffn 6718	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℝ⟶ℝ → 𝑔 Fn ℝ)
102		frn 6725	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℝ⟶ℝ → ran 𝑔 ⊆ ℝ)
103	102, 92	sstrdi 3995	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℝ⟶ℝ → ran 𝑔 ⊆ ℂ)
104		fnco 6668	. . . . . . . . . . . . . . . 16 ⊢ ((abs Fn ℂ ∧ 𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ) → (abs ∘ 𝑔) Fn ℝ)
105	95, 104	mp3an1 1449	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ) → (abs ∘ 𝑔) Fn ℝ)
106	101, 103, 105	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℝ⟶ℝ → (abs ∘ 𝑔) Fn ℝ)
107	32, 106	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (abs ∘ 𝑔) Fn ℝ)
108	107	adantl 483	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑔) Fn ℝ)
109		inidm 4219	. . . . . . . . . . . 12 ⊢ (ℝ ∩ ℝ) = ℝ
110	28	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑓:ℝ⟶ℝ)
111		fvco3 6991	. . . . . . . . . . . . 13 ⊢ ((𝑓:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑓)‘𝑡) = (abs‘(𝑓‘𝑡)))
112	110, 111	sylan 581	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑓)‘𝑡) = (abs‘(𝑓‘𝑡)))
113	32	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑔:ℝ⟶ℝ)
114		fvco3 6991	. . . . . . . . . . . . 13 ⊢ ((𝑔:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑔)‘𝑡) = (abs‘(𝑔‘𝑡)))
115	113, 114	sylan 581	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑔)‘𝑡) = (abs‘(𝑔‘𝑡)))
116	100, 108, 41, 41, 109, 112, 115	offval 7679	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ 𝑓) ∘f + (abs ∘ 𝑔)) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
117	30	addridd 11414	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + 0) = (𝑓‘𝑡))
118	117	mpteq2dva 5249	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + 0)) = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
119	40	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ℝ ∈ V)
120	17	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ∈ V)
121	31	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → i ∈ ℂ)
122	48	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i))
123		fconstmpt 5739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
124	123	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
125	119, 121, 120, 122, 124	offval2 7690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ((ℝ × {i}) ∘f · (ℝ × {0})) = (𝑡 ∈ ℝ ↦ (i · 0)))
126		it0e0 12434	. . . . . . . . . . . . . . . . . . 19 ⊢ (i · 0) = 0
127	126	mpteq2i 5254	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ ℝ ↦ (i · 0)) = (𝑡 ∈ ℝ ↦ 0)
128	125, 127	eqtrdi 2789	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ((ℝ × {i}) ∘f · (ℝ × {0})) = (𝑡 ∈ ℝ ↦ 0))
129	119, 29, 120, 44, 128	offval2 7690	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ dom ∫1 → (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0}))) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + 0)))
130	118, 129, 44	3eqtr4d 2783	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ dom ∫1 → (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0}))) = 𝑓)
131	130	coeq2d 5863	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0})))) = (abs ∘ 𝑓))
132		i1f0 25204	. . . . . . . . . . . . . . 15 ⊢ (ℝ × {0}) ∈ dom ∫1
133		ftc1anclem3 36563	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ (ℝ × {0}) ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0})))) ∈ dom ∫1)
134	132, 133	mpan2 690	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0})))) ∈ dom ∫1)
135	131, 134	eqeltrrd 2835	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ 𝑓) ∈ dom ∫1)
136	135	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑓) ∈ dom ∫1)
137		coeq2 5859	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (abs ∘ 𝑓) = (abs ∘ 𝑔))
138	137	eleq1d 2819	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((abs ∘ 𝑓) ∈ dom ∫1 ↔ (abs ∘ 𝑔) ∈ dom ∫1))
139	138, 135	vtoclga 3566	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (abs ∘ 𝑔) ∈ dom ∫1)
140	139	adantl 483	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑔) ∈ dom ∫1)
141	136, 140	i1fadd 25212	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ 𝑓) ∘f + (abs ∘ 𝑔)) ∈ dom ∫1)
142	116, 141	eqeltrrd 2835	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1)
143	30	abscld 15383	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓‘𝑡)) ∈ ℝ)
144	30	absge0d 15391	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(𝑓‘𝑡)))
145		elrege0 13431	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘(𝑓‘𝑡)) ∈ (0[,)+∞) ↔ ((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑓‘𝑡))))
146	143, 144, 145	sylanbrc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓‘𝑡)) ∈ (0[,)+∞))
147	34	abscld 15383	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ ℝ)
148	34	absge0d 15391	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(𝑔‘𝑡)))
149		elrege0 13431	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘(𝑔‘𝑡)) ∈ (0[,)+∞) ↔ ((abs‘(𝑔‘𝑡)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑔‘𝑡))))
150	147, 148, 149	sylanbrc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ (0[,)+∞))
151		ge0addcl 13437	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑓‘𝑡)) ∈ (0[,)+∞) ∧ (abs‘(𝑔‘𝑡)) ∈ (0[,)+∞)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
152	146, 150, 151	syl2an 597	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
153	152	anandirs 678	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
154	153	fmpttd 7115	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞))
155		0plef 25189	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞) ↔ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
156	154, 155	sylib 217	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
157	156	simprd 497	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
158		itg2itg1 25254	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) = (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
159		itg1cl 25202	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
160	159	adantr 482	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
161	158, 160	eqeltrd 2834	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
162	142, 157, 161	syl2anc 585	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
163		icossicc 13413	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
164		fss 6735	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞))
165	154, 163, 164	sylancl 587	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞))
166		0re 11216	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
167		ifcl 4574	. . . . . . . . . . . . . 14 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
168	70, 166, 167	sylancl 587	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
169		readdcl 11193	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ (abs‘(𝑔‘𝑡)) ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
170	143, 147, 169	syl2an 597	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
171	170	anandirs 678	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
172	70	leidd 11780	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
173		breq1 5152	. . . . . . . . . . . . . . 15 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
174		breq1 5152	. . . . . . . . . . . . . . 15 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
175	173, 174	ifboth 4568	. . . . . . . . . . . . . 14 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
176	172, 71, 175	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
177		abstri 15277	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
178	30, 36, 177	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
179	178	anandirs 678	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
180		absmul 15241	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (abs‘(i · (𝑔‘𝑡))) = ((abs‘i) · (abs‘(𝑔‘𝑡))))
181	31, 34, 180	sylancr 588	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = ((abs‘i) · (abs‘(𝑔‘𝑡))))
182		absi 15233	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs‘i) = 1
183	182	oveq1i 7419	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘i) · (abs‘(𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡)))
184	181, 183	eqtrdi 2789	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡))))
185	147	recnd 11242	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ ℂ)
186	185	mullidd 11232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (1 · (abs‘(𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
187	184, 186	eqtrd 2773	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
188	187	adantll 713	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
189	188	oveq2d 7425	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))) = ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
190	179, 189	breqtrd 5175	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
191	168, 70, 171, 176, 190	letrd 11371	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
192	191	ralrimiva 3147	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ∀𝑡 ∈ ℝ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
193		eqidd 2734	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
194		eqidd 2734	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
195	41, 168, 171, 193, 194	ofrfval2 7691	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
196	192, 195	mpbird 257	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
197		itg2le 25257	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
198	89, 165, 196, 197	syl3anc 1372	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
199		itg2lecl 25256	. . . . . . . . 9 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
200	89, 162, 198, 199	syl3anc 1372	. . . . . . . 8 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
201	200	ad2antlr 726	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
202	89	ad2antlr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
203		breq1 5152	. . . . . . . . . . 11 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
204		breq1 5152	. . . . . . . . . . 11 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
205		elioore 13354	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
206	205, 172	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
207	206	adantll 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
208	207	adantlr 714	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
209	2	rexrd 11264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
210	3	rexrd 11264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
211	209, 210	jca 513	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
212		df-icc 13331	. . . . . . . . . . . . . . . . . . . . 21 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)})
213	212	elixx3g 13337	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑢 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
214	213	simprbi 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))
215	214	simpld 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢)
216	212	elixx3g 13337	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)))
217	216	simprbi 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))
218	217	simprd 497	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵)
219	215, 218	anim12i 614	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵))
220		ioossioo 13418	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
221	211, 219, 220	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
222	5	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
223	221, 222	sstrd 3993	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
224	223	sselda 3983	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
225		iftrue 4535	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
226	224, 225	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
227	226	adantllr 718	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
228	208, 227	breqtrrd 5177	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
229		breq2 5153	. . . . . . . . . . . . 13 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
230		breq2 5153	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
231	6	sselda 3983	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ)
232	231	adantlr 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ)
233	71	adantll 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
234	232, 233	syldan 592	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
235		0le0 12313	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
236	235	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ≤ 0)
237	229, 230, 234, 236	ifbothda 4567	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
238	237	ad2antrr 725	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
239	203, 204, 228, 238	ifbothda 4567	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
240	239	ralrimivw 3151	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
241	40	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ V)
242	18	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
243	16, 17	ifex 4579	. . . . . . . . . . . 12 ⊢ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V
244	243	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
245		eqidd 2734	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
246		eqidd 2734	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
247	241, 242, 244, 245, 246	ofrfval2 7691	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
248	247	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
249	240, 248	mpbird 257	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
250		itg2le 25257	. . . . . . . 8 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))))
251	86, 202, 249, 250	syl3anc 1372	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))))
252		itg2lecl 25256	. . . . . . 7 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
253	86, 201, 251, 252	syl3anc 1372	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
254	8	ffvelcdmda 7087	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
255	254	adantlr 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
256	224, 255	syldan 592	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
257	256	adantllr 718	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
258	205, 39	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
259	258	adantll 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
260	259	adantlr 714	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
261	257, 260	subcld 11571	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
262	261	abscld 15383	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
263	261	absge0d 15391	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
264		elrege0 13431	. . . . . . . . . 10 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,)+∞) ↔ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ ∧ 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
265	262, 263, 264	sylanbrc 584	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,)+∞))
266	74	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,)+∞))
267	265, 266	ifclda 4564	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,)+∞))
268	267	adantr 482	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,)+∞))
269	268	fmpttd 7115	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,)+∞))
270	262	rexrd 11264	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
271		elxrge0 13434	. . . . . . . . . . 11 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
272	270, 263, 271	sylanbrc 584	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞))
273	82	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
274	272, 273	ifclda 4564	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
275	274	adantr 482	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
276	275	fmpttd 7115	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞))
277		recncf 24418	. . . . . . . . . . . . 13 ⊢ ℜ ∈ (ℂ–cn→ℝ)
278		prid1g 4765	. . . . . . . . . . . . 13 ⊢ (ℜ ∈ (ℂ–cn→ℝ) → ℜ ∈ {ℜ, ℑ})
279	277, 278	ax-mp 5	. . . . . . . . . . . 12 ⊢ ℜ ∈ {ℜ, ℑ}
280		ftc1anclem2 36562	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℜ ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
281	279, 280	mp3an3 1451	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
282	8, 7, 281	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
283		imcncf 24419	. . . . . . . . . . . . 13 ⊢ ℑ ∈ (ℂ–cn→ℝ)
284		prid2g 4766	. . . . . . . . . . . . 13 ⊢ (ℑ ∈ (ℂ–cn→ℝ) → ℑ ∈ {ℜ, ℑ})
285	283, 284	ax-mp 5	. . . . . . . . . . . 12 ⊢ ℑ ∈ {ℜ, ℑ}
286		ftc1anclem2 36562	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℑ ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
287	285, 286	mp3an3 1451	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
288	8, 7, 287	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
289	282, 288	readdcld 11243	. . . . . . . . 9 ⊢ (𝜑 → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
290	289	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
291	201, 290	readdcld 11243	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) ∈ ℝ)
292		ge0addcl 13437	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
293	292	adantl 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞))
294		ifcl 4574	. . . . . . . . . . . . . . 15 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
295	73, 74, 294	sylancl 587	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
296	295	fmpttd 7115	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
297	296	adantl 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
298	292	adantl 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞))
299	254	recld 15141	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘(𝐹‘𝑡)) ∈ ℝ)
300	299	recnd 11242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘(𝐹‘𝑡)) ∈ ℂ)
301	300	abscld 15383	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ)
302	300	absge0d 15391	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(ℜ‘(𝐹‘𝑡))))
303		elrege0 13431	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘(ℜ‘(𝐹‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘(ℜ‘(𝐹‘𝑡)))))
304	301, 302, 303	sylanbrc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ (0[,)+∞))
305	74	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ (0[,)+∞))
306	304, 305	ifclda 4564	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
307	306	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
308	307	fmpttd 7115	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)):ℝ⟶(0[,)+∞))
309	254	imcld 15142	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℑ‘(𝐹‘𝑡)) ∈ ℝ)
310	309	recnd 11242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℑ‘(𝐹‘𝑡)) ∈ ℂ)
311	310	abscld 15383	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ)
312	310	absge0d 15391	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(ℑ‘(𝐹‘𝑡))))
313		elrege0 13431	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘(ℑ‘(𝐹‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘(ℑ‘(𝐹‘𝑡)))))
314	311, 312, 313	sylanbrc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ (0[,)+∞))
315	314, 305	ifclda 4564	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
316	315	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
317	316	fmpttd 7115	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)):ℝ⟶(0[,)+∞))
318	298, 308, 317, 241, 241, 109	off 7688	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))):ℝ⟶(0[,)+∞))
319	318	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))):ℝ⟶(0[,)+∞))
320	40	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ℝ ∈ V)
321	293, 297, 319, 320, 320, 109	off 7688	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,)+∞))
322		fss 6735	. . . . . . . . . . 11 ⊢ ((((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞))
323	321, 163, 322	sylancl 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞))
324	323	adantr 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞))
325		0xr 11261	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ*
326	325	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ ℝ*)
327	270, 326	ifclda 4564	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
328	254	adantlr 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
329	39	adantll 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
330	232, 329	syldan 592	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
331	328, 330	subcld 11571	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
332	331	abscld 15383	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
333	332	rexrd 11264	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
334	325	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ*)
335	333, 334	ifclda 4564	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
336	335	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
337	330	abscld 15383	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
338		0red 11217	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ)
339	337, 338	ifclda 4564	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
340		0red 11217	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ)
341	301, 340	ifclda 4564	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ ℝ)
342	311, 340	ifclda 4564	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ ℝ)
343	341, 342	readdcld 11243	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ ℝ)
344	343	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ ℝ)
345	339, 344	readdcld 11243	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
346	345	rexrd 11264	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ*)
347	346	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ*)
348		breq1 5152	. . . . . . . . . . . . 13 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
349		breq1 5152	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
350	224	adantllr 718	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
351	332	leidd 11780	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
352	351	adantlr 714	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
353		iftrue 4535	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
354	353	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
355	352, 354	breqtrrd 5177	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
356	350, 355	syldan 592	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
357		breq2 5153	. . . . . . . . . . . . . . 15 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
358		breq2 5153	. . . . . . . . . . . . . . 15 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
359	331	absge0d 15391	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
360	357, 358, 359, 236	ifbothda 4567	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
361	360	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
362	348, 349, 356, 361	ifbothda 4567	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
363	254	negcld 11558	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → -(𝐹‘𝑡) ∈ ℂ)
364	363	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → -(𝐹‘𝑡) ∈ ℂ)
365	330, 364	addcld 11233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)) ∈ ℂ)
366	365	abscld 15383	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ∈ ℝ)
367	363	abscld 15383	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ∈ ℝ)
368	367	adantlr 714	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ∈ ℝ)
369	337, 368	readdcld 11243	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))) ∈ ℝ)
370	301, 311	readdcld 11243	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ ℝ)
371	370	adantlr 714	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ ℝ)
372	337, 371	readdcld 11243	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))) ∈ ℝ)
373	330, 364	abstrid 15403	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))))
374		mulcl 11194	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((i ∈ ℂ ∧ (ℑ‘(𝐹‘𝑡)) ∈ ℂ) → (i · (ℑ‘(𝐹‘𝑡))) ∈ ℂ)
375	31, 310, 374	sylancr 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (i · (ℑ‘(𝐹‘𝑡))) ∈ ℂ)
376	300, 375	abstrid 15403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(i · (ℑ‘(𝐹‘𝑡))))))
377	254	absnegd 15396	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) = (abs‘(𝐹‘𝑡)))
378	254	replimd 15144	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) = ((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡)))))
379	378	fveq2d 6896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) = (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))))
380	377, 379	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) = (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))))
381		absmul 15241	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((i ∈ ℂ ∧ (ℑ‘(𝐹‘𝑡)) ∈ ℂ) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))))
382	31, 310, 381	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))))
383	182	oveq1i 7419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))) = (1 · (abs‘(ℑ‘(𝐹‘𝑡))))
384	382, 383	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = (1 · (abs‘(ℑ‘(𝐹‘𝑡)))))
385	311	recnd 11242	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℂ)
386	385	mullidd 11232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (1 · (abs‘(ℑ‘(𝐹‘𝑡)))) = (abs‘(ℑ‘(𝐹‘𝑡))))
387	384, 386	eqtr2d 2774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) = (abs‘(i · (ℑ‘(𝐹‘𝑡)))))
388	387	oveq2d 7425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) = ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(i · (ℑ‘(𝐹‘𝑡))))))
389	376, 380, 388	3brtr4d 5181	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
390	389	adantlr 714	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
391	368, 371, 337, 390	leadd2dd 11829	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
392	366, 369, 372, 373, 391	letrd 11371	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
393	328, 330	abssubd 15400	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡))))
394	353	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
395	330, 328	negsubd 11577	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)) = (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡)))
396	395	fveq2d 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡))))
397	393, 394, 396	3eqtr4d 2783	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))))
398		iftrue 4535	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
399	398	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
400	392, 397, 399	3brtr4d 5181	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
401	400	ex 414	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)))
402	235	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → 0 ≤ 0)
403		iffalse 4538	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0)
404		iffalse 4538	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = 0)
405	402, 403, 404	3brtr4d 5181	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
406	401, 405	pm2.61d1 180	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
407		iftrue 4535	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) = (abs‘(ℜ‘(𝐹‘𝑡))))
408		iftrue 4535	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) = (abs‘(ℑ‘(𝐹‘𝑡))))
409	407, 408	oveq12d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
410	225, 409	oveq12d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
411	410, 398	eqtr4d 2776	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
412		00id 11389	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 0) = 0
413	412	oveq2i 7420	. . . . . . . . . . . . . . . . 17 ⊢ (0 + (0 + 0)) = (0 + 0)
414	413, 412	eqtri 2761	. . . . . . . . . . . . . . . 16 ⊢ (0 + (0 + 0)) = 0
415		iffalse 4538	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
416		iffalse 4538	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) = 0)
417		iffalse 4538	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) = 0)
418	416, 417	oveq12d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (0 + 0))
419	415, 418	oveq12d 7427	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = (0 + (0 + 0)))
420	414, 419, 404	3eqtr4a 2799	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
421	411, 420	pm2.61i 182	. . . . . . . . . . . . . 14 ⊢ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)
422	406, 421	breqtrrdi 5191	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
423	422	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
424	327, 336, 347, 362, 423	xrletrd 13141	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
425	424	ralrimivw 3151	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
426		fvex 6905	. . . . . . . . . . . . . 14 ⊢ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V
427	426, 17	ifex 4579	. . . . . . . . . . . . 13 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V
428	427	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V)
429		ovexd 7444	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ V)
430		eqidd 2734	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
431		ovexd 7444	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ V)
432	341	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ ℝ)
433	342	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ ℝ)
434		eqidd 2734	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))
435		eqidd 2734	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))
436	241, 432, 433, 434, 435	offval2 7690	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
437	241, 244, 431, 246, 436	offval2 7690	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
438	241, 428, 429, 430, 437	ofrfval2 7691	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘r ≤ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
439	438	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘r ≤ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
440	425, 439	mpbird 257	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘r ≤ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
441		itg2le 25257	. . . . . . . . 9 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞) ∧ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘r ≤ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
442	276, 324, 440, 441	syl3anc 1372	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
443	6	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 𝐷 ⊆ ℝ)
444	243	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
445		eldifn 4128	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
446	445	iffalsed 4540	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
447	446	adantl 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
448		ovexd 7444	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ V)
449	41, 42, 448, 45, 52	offval2 7690	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔)) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
450	39, 449, 56, 57	fmptco 7127	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) = (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
451	450	reseq1d 5981	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) = ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ 𝐷))
452	6	resmptd 6041	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
453	451, 452	sylan9eqr 2795	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
454	225	mpteq2ia 5252	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
455	453, 454	eqtr4di 2791	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
456		i1fmbf 25192	. . . . . . . . . . . . . . 15 ⊢ ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ∈ dom ∫1 → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ∈ MblFn)
457	59, 456	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ∈ MblFn)
458	8	fdmd 6729	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐹 = 𝐷)
459		iblmbf 25285	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
460		mbfdm 25143	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
461	7, 459, 460	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐹 ∈ dom vol)
462	458, 461	eqeltrrd 2835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ dom vol)
463		mbfres 25161	. . . . . . . . . . . . . 14 ⊢ (((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ∈ MblFn ∧ 𝐷 ∈ dom vol) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) ∈ MblFn)
464	457, 462, 463	syl2anr 598	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) ∈ MblFn)
465	455, 464	eqeltrrd 2835	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
466	443, 15, 444, 447, 465	mbfss 25163	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
467	200	adantl 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
468		0cnd 11207	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
469	300, 468	ifclda 4564	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℂ)
470	469	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℂ)
471		eqidd 2734	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)))
472	54	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → abs:ℂ⟶ℝ)
473	472	feqmptd 6961	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
474		fveq2 6892	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) → (abs‘𝑥) = (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)))
475		fvif 6908	. . . . . . . . . . . . . . . . . 18 ⊢ (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0))
476		abs0 15232	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs‘0) = 0
477		ifeq2 4534	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs‘0) = 0 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))
478	476, 477	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)
479	475, 478	eqtri 2761	. . . . . . . . . . . . . . . . 17 ⊢ (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)
480	474, 479	eqtrdi 2789	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) → (abs‘𝑥) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))
481	470, 471, 473, 480	fmptco 7127	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))
482	299, 340	ifclda 4564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
483	482	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
484	483	fmpttd 7115	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)):ℝ⟶ℝ)
485	14	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℝ ∈ dom vol)
486	482	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
487	445	adantl 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
488	487	iffalsed 4540	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) = 0)
489		iftrue 4535	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) = (ℜ‘(𝐹‘𝑡)))
490	489	mpteq2ia 5252	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡)))
491	8	feqmptd 6961	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
492	7, 459	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 ∈ MblFn)
493	491, 492	eqeltrrd 2835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn)
494	254	ismbfcn2 25155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)))
495	493, 494	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))
496	495	simpld 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn)
497	490, 496	eqeltrid 2838	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn)
498	6, 485, 486, 488, 497	mbfss 25163	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn)
499		ftc1anclem1 36561	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) ∈ MblFn)
500	484, 498, 499	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) ∈ MblFn)
501	481, 500	eqeltrrd 2835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∈ MblFn)
502	501, 308, 282, 317, 288	itg2addnc 36542	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
503	502, 289	eqeltrd 2834	. . . . . . . . . . . 12 ⊢ (𝜑 → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
504	503	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
505	466, 297, 467, 319, 504	itg2addnc 36542	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
506	502	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
507	506	oveq2d 7425	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
508	505, 507	eqtrd 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
509	508	adantr 482	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
510	442, 509	breqtrd 5175	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
511		itg2lecl 25256	. . . . . . 7 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ)
512	276, 291, 510, 511	syl3anc 1372	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ)
513	69, 78, 253, 269, 512	itg2addnc 36542	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))))
514	241, 242, 428, 245, 430	offval2 7690	. . . . . . . . 9 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
515		eqeq2 2745	. . . . . . . . . . 11 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0) → ((if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) ↔ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
516		eqeq2 2745	. . . . . . . . . . 11 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0) → ((if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0 ↔ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
517		iftrue 4535	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
518	23, 517	oveq12d 7427	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
519	518	adantl 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
520		iffalse 4538	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
521		iffalse 4538	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0)
522	520, 521	oveq12d 7427	. . . . . . . . . . . . 13 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (0 + 0))
523	522, 412	eqtrdi 2789	. . . . . . . . . . . 12 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0)
524	523	adantl 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0)
525	515, 516, 519, 524	ifbothda 4567	. . . . . . . . . 10 ⊢ (𝜑 → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0))
526	525	mpteq2dv 5251	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
527	514, 526	eqtrd 2773	. . . . . . . 8 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
528	527	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
529		simplr 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
530	258	abscld 15383	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
531	530	recnd 11242	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
532	529, 531	sylan 581	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
533	262	recnd 11242	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℂ)
534	532, 533	addcomd 11416	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
535	534	ifeq1da 4560	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
536	535	mpteq2dv 5251	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
537	528, 536	eqtrd 2773	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
538	537	fveq2d 6896	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
539	513, 538	eqtr3d 2775	. . . 4 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
540	10, 11, 539	syl2an 597	. . 3 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
541	540	adantr 482	. 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‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
542		rpcn 12984	. . . 4 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
543	542	2halvesd 12458	. . 3 ⊢ (𝑦 ∈ ℝ+ → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
544	543	ad3antlr 730	. 2 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
545	9, 541, 544	3brtr3d 5180	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 · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < 𝑦)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  Vcvv 3475   ∖ cdif 3946   ∪ cun 3947   ⊆ wss 3949  ifcif 4529  {csn 4629  {cpr 4631   class class class wbr 5149   ↦ cmpt 5232   × cxp 5675  dom cdm 5677  ran crn 5678   ↾ cres 5679   “ cima 5680   ∘ ccom 5681   Fn wfn 6539  ⟶wf 6540  ‘cfv 6544  (class class class)co 7409   ∘_f cof 7668   ∘_r cofr 7669  supcsup 9435  ℂcc 11108  ℝcr 11109  0cc0 11110  1c1 11111  ici 11112   + caddc 11113   · cmul 11115  +∞cpnf 11245  ℝ^*cxr 11247   < clt 11248   ≤ cle 11249   − cmin 11444  -cneg 11445   / cdiv 11871  2c2 12267  ℝ⁺crp 12974  (,)cioo 13324  [,)cico 13326  [,]cicc 13327  ℜcre 15044  ℑcim 15045  abscabs 15181  –cn→ccncf 24392  volcvol 24980  MblFncmbf 25131  ∫₁citg1 25132  ∫₂citg2 25133  𝐿¹cibl 25134  ∫citg 25135  0_𝑝c0p 25186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188  ax-addf 11189

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-of 7670  df-ofr 7671  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-er 8703  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fi 9406  df-sup 9437  df-inf 9438  df-oi 9505  df-dju 9896  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-z 12559  df-uz 12823  df-q 12933  df-rp 12975  df-xneg 13092  df-xadd 13093  df-xmul 13094  df-ioo 13328  df-ico 13330  df-icc 13331  df-fz 13485  df-fzo 13628  df-fl 13757  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-rlim 15433  df-sum 15633  df-rest 17368  df-topgen 17389  df-psmet 20936  df-xmet 20937  df-met 20938  df-bl 20939  df-mopn 20940  df-top 22396  df-topon 22413  df-bases 22449  df-cmp 22891  df-cncf 24394  df-ovol 24981  df-vol 24982  df-mbf 25136  df-itg1 25137  df-itg2 25138  df-ibl 25139  df-0p 25187

This theorem is referenced by:  ftc1anc  36569