Theorem ftc1anclem8 38067

Description: Lemma for ftc1anc 38068. (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 38066	. 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 780	. . . 4 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
11		3simpa 1154	. . . 4 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤) → (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)))
12		ioossre 13351	. . . . . . . . 9 ⊢ (𝑢(,)𝑤) ⊆ ℝ
13	12	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑢(,)𝑤) ⊆ ℝ)
14		rembl 25525	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
15	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ℝ ∈ dom vol)
16		fvex 6840	. . . . . . . . . 10 ⊢ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ V
17		c0ex 11129	. . . . . . . . . 10 ⊢ 0 ∈ V
18	16, 17	ifex 4505	. . . . . . . . 9 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V
19	18	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
20		eldifn 4062	. . . . . . . . . 10 ⊢ (𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤)) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
21	20	adantl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤))) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
22	21	iffalsed 4465	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
23		iftrue 4460	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
24	23	mpteq2ia 5167	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
25		resmpt 5989	. . . . . . . . . . . 12 ⊢ ((𝑢(,)𝑤) ⊆ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
26	12, 25	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
27	24, 26	eqtr4i 2765	. . . . . . . . . 10 ⊢ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤))
28		i1ff 25661	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
29	28	ffvelcdmda 7025	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
30	29	recnd 11164	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℂ)
31		ax-icn 11088	. . . . . . . . . . . . . . . . 17 ⊢ i ∈ ℂ
32		i1ff 25661	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
33	32	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
34	33	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
35		mulcl 11113	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ)
36	31, 34, 35	sylancr 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
37		addcl 11111	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
38	30, 36, 37	syl2an 602	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
39	38	anandirs 685	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
40		reex 11120	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
41	40	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ℝ ∈ V)
42	29	adantlr 721	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
43	36	adantll 720	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
44	28	feqmptd 6895	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ dom ∫1 → 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
45	44	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
46	40	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → ℝ ∈ V)
47	31	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → i ∈ ℂ)
48		fconstmpt 5680	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i)
49	48	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i))
50	32	feqmptd 6895	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡)))
51	46, 47, 33, 49, 50	offval2 7640	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ dom ∫1 → ((ℝ × {i}) ∘f · 𝑔) = (𝑡 ∈ ℝ ↦ (i · (𝑔‘𝑡))))
52	51	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((ℝ × {i}) ∘f · 𝑔) = (𝑡 ∈ ℝ ↦ (i · (𝑔‘𝑡))))
53	41, 42, 43, 45, 52	offval2 7640	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔)) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
54		absf 15291	. . . . . . . . . . . . . . . 16 ⊢ abs:ℂ⟶ℝ
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → abs:ℂ⟶ℝ)
56	55	feqmptd 6895	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
57		fveq2 6827	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) → (abs‘𝑥) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
58	39, 53, 56, 57	fmptco 7071	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) = (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
59		ftc1anclem3 38062	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ∈ dom ∫1)
60	58, 59	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ dom ∫1)
61		i1fmbf 25660	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn)
62	60, 61	syl 17	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn)
63		ioombl 25550	. . . . . . . . . . 11 ⊢ (𝑢(,)𝑤) ∈ dom vol
64		mbfres 25629	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn ∧ (𝑢(,)𝑤) ∈ dom vol) → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) ∈ MblFn)
65	62, 63, 64	sylancl 592	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) ∈ MblFn)
66	27, 65	eqeltrid 2843	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
67	66	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
68	13, 15, 19, 22, 67	mbfss 25631	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
69	68	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
70	39	abscld 15392	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
71	39	absge0d 15400	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
72		elrege0 13398	. . . . . . . . . 10 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ↔ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
73	70, 71, 72	sylanbrc 589	. . . . . . . . 9 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞))
74		0e0icopnf 13402	. . . . . . . . 9 ⊢ 0 ∈ (0[,)+∞)
75		ifcl 4500	. . . . . . . . 9 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
76	73, 74, 75	sylancl 592	. . . . . . . 8 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
77	76	fmpttd 7056	. . . . . . 7 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
78	77	ad2antlr 733	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
79	70	rexrd 11186	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ*)
80		elxrge0 13401	. . . . . . . . . . 11 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ↔ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
81	79, 71, 80	sylanbrc 589	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞))
82		0e0iccpnf 13403	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]+∞)
83		ifcl 4500	. . . . . . . . . 10 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
84	81, 82, 83	sylancl 592	. . . . . . . . 9 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
85	84	fmpttd 7056	. . . . . . . 8 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
86	85	ad2antlr 733	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
87		ifcl 4500	. . . . . . . . . . 11 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
88	81, 82, 87	sylancl 592	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
89	88	fmpttd 7056	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
90		ffn 6655	. . . . . . . . . . . . . . 15 ⊢ (𝑓:ℝ⟶ℝ → 𝑓 Fn ℝ)
91		frn 6662	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:ℝ⟶ℝ → ran 𝑓 ⊆ ℝ)
92		ax-resscn 11086	. . . . . . . . . . . . . . . 16 ⊢ ℝ ⊆ ℂ
93	91, 92	sstrdi 3927	. . . . . . . . . . . . . . 15 ⊢ (𝑓:ℝ⟶ℝ → ran 𝑓 ⊆ ℂ)
94		ffn 6655	. . . . . . . . . . . . . . . . 17 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ)
95	54, 94	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ abs Fn ℂ
96		fnco 6603	. . . . . . . . . . . . . . . 16 ⊢ ((abs Fn ℂ ∧ 𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ) → (abs ∘ 𝑓) Fn ℝ)
97	95, 96	mp3an1 1456	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ) → (abs ∘ 𝑓) Fn ℝ)
98	90, 93, 97	syl2anc 590	. . . . . . . . . . . . . 14 ⊢ (𝑓:ℝ⟶ℝ → (abs ∘ 𝑓) Fn ℝ)
99	28, 98	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ 𝑓) Fn ℝ)
100	99	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑓) Fn ℝ)
101		ffn 6655	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℝ⟶ℝ → 𝑔 Fn ℝ)
102		frn 6662	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℝ⟶ℝ → ran 𝑔 ⊆ ℝ)
103	102, 92	sstrdi 3927	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℝ⟶ℝ → ran 𝑔 ⊆ ℂ)
104		fnco 6603	. . . . . . . . . . . . . . . 16 ⊢ ((abs Fn ℂ ∧ 𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ) → (abs ∘ 𝑔) Fn ℝ)
105	95, 104	mp3an1 1456	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ) → (abs ∘ 𝑔) Fn ℝ)
106	101, 103, 105	syl2anc 590	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℝ⟶ℝ → (abs ∘ 𝑔) Fn ℝ)
107	32, 106	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (abs ∘ 𝑔) Fn ℝ)
108	107	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑔) Fn ℝ)
109		inidm 4155	. . . . . . . . . . . 12 ⊢ (ℝ ∩ ℝ) = ℝ
110	28	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑓:ℝ⟶ℝ)
111		fvco3 6927	. . . . . . . . . . . . 13 ⊢ ((𝑓:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑓)‘𝑡) = (abs‘(𝑓‘𝑡)))
112	110, 111	sylan 586	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑓)‘𝑡) = (abs‘(𝑓‘𝑡)))
113	32	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑔:ℝ⟶ℝ)
114		fvco3 6927	. . . . . . . . . . . . 13 ⊢ ((𝑔:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑔)‘𝑡) = (abs‘(𝑔‘𝑡)))
115	113, 114	sylan 586	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑔)‘𝑡) = (abs‘(𝑔‘𝑡)))
116	100, 108, 41, 41, 109, 112, 115	offval 7629	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ 𝑓) ∘f + (abs ∘ 𝑔)) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
117	30	addridd 11337	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + 0) = (𝑓‘𝑡))
118	117	mpteq2dva 5165	. . . . . . . . . . . . . . . 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 5680	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
124	123	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
125	119, 121, 120, 122, 124	offval2 7640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ((ℝ × {i}) ∘f · (ℝ × {0})) = (𝑡 ∈ ℝ ↦ (i · 0)))
126		it0e0 12391	. . . . . . . . . . . . . . . . . . 19 ⊢ (i · 0) = 0
127	126	mpteq2i 5168	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ ℝ ↦ (i · 0)) = (𝑡 ∈ ℝ ↦ 0)
128	125, 127	eqtrdi 2790	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ((ℝ × {i}) ∘f · (ℝ × {0})) = (𝑡 ∈ ℝ ↦ 0))
129	119, 29, 120, 44, 128	offval2 7640	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ dom ∫1 → (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0}))) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + 0)))
130	118, 129, 44	3eqtr4d 2784	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ dom ∫1 → (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0}))) = 𝑓)
131	130	coeq2d 5804	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0})))) = (abs ∘ 𝑓))
132		i1f0 25672	. . . . . . . . . . . . . . 15 ⊢ (ℝ × {0}) ∈ dom ∫1
133		ftc1anclem3 38062	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ (ℝ × {0}) ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0})))) ∈ dom ∫1)
134	132, 133	mpan2 697	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0})))) ∈ dom ∫1)
135	131, 134	eqeltrrd 2840	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ 𝑓) ∈ dom ∫1)
136	135	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑓) ∈ dom ∫1)
137		coeq2 5800	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (abs ∘ 𝑓) = (abs ∘ 𝑔))
138	137	eleq1d 2824	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((abs ∘ 𝑓) ∈ dom ∫1 ↔ (abs ∘ 𝑔) ∈ dom ∫1))
139	138, 135	vtoclga 3520	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (abs ∘ 𝑔) ∈ dom ∫1)
140	139	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑔) ∈ dom ∫1)
141	136, 140	i1fadd 25680	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ 𝑓) ∘f + (abs ∘ 𝑔)) ∈ dom ∫1)
142	116, 141	eqeltrrd 2840	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1)
143	30	abscld 15392	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓‘𝑡)) ∈ ℝ)
144	30	absge0d 15400	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(𝑓‘𝑡)))
145		elrege0 13398	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘(𝑓‘𝑡)) ∈ (0[,)+∞) ↔ ((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑓‘𝑡))))
146	143, 144, 145	sylanbrc 589	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓‘𝑡)) ∈ (0[,)+∞))
147	34	abscld 15392	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ ℝ)
148	34	absge0d 15400	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(𝑔‘𝑡)))
149		elrege0 13398	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘(𝑔‘𝑡)) ∈ (0[,)+∞) ↔ ((abs‘(𝑔‘𝑡)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑔‘𝑡))))
150	147, 148, 149	sylanbrc 589	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ (0[,)+∞))
151		ge0addcl 13404	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑓‘𝑡)) ∈ (0[,)+∞) ∧ (abs‘(𝑔‘𝑡)) ∈ (0[,)+∞)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
152	146, 150, 151	syl2an 602	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
153	152	anandirs 685	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
154	153	fmpttd 7056	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞))
155		0plef 25657	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞) ↔ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
156	154, 155	sylib 219	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
157	156	simprd 496	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
158		itg2itg1 25721	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) = (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
159		itg1cl 25670	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
160	159	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
161	158, 160	eqeltrd 2839	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
162	142, 157, 161	syl2anc 590	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
163		icossicc 13380	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
164		fss 6671	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞))
165	154, 163, 164	sylancl 592	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞))
166		0re 11137	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
167		ifcl 4500	. . . . . . . . . . . . . 14 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
168	70, 166, 167	sylancl 592	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
169		readdcl 11112	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ (abs‘(𝑔‘𝑡)) ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
170	143, 147, 169	syl2an 602	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
171	170	anandirs 685	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
172	70	leidd 11707	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
173		breq1 5075	. . . . . . . . . . . . . . 15 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
174		breq1 5075	. . . . . . . . . . . . . . 15 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
175	173, 174	ifboth 4494	. . . . . . . . . . . . . 14 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
176	172, 71, 175	syl2anc 590	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
177		abstri 15284	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
178	30, 36, 177	syl2an 602	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
179	178	anandirs 685	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
180		absmul 15247	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (abs‘(i · (𝑔‘𝑡))) = ((abs‘i) · (abs‘(𝑔‘𝑡))))
181	31, 34, 180	sylancr 593	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = ((abs‘i) · (abs‘(𝑔‘𝑡))))
182		absi 15239	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs‘i) = 1
183	182	oveq1i 7366	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘i) · (abs‘(𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡)))
184	181, 183	eqtrdi 2790	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡))))
185	147	recnd 11164	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ ℂ)
186	185	mullidd 11154	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (1 · (abs‘(𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
187	184, 186	eqtrd 2774	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
188	187	adantll 720	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
189	188	oveq2d 7372	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))) = ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
190	179, 189	breqtrd 5098	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
191	168, 70, 171, 176, 190	letrd 11294	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
192	191	ralrimiva 3131	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ∀𝑡 ∈ ℝ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
193		eqidd 2740	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
194		eqidd 2740	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
195	41, 168, 171, 193, 194	ofrfval2 7641	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
196	192, 195	mpbird 258	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
197		itg2le 25724	. . . . . . . . . 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 1379	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
199		itg2lecl 25723	. . . . . . . . 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 1379	. . . . . . . 8 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
201	200	ad2antlr 733	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
202	89	ad2antlr 733	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
203		breq1 5075	. . . . . . . . . . 11 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
204		breq1 5075	. . . . . . . . . . 11 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
205		elioore 13319	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
206	205, 172	sylan2 599	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
207	206	adantll 720	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
208	207	adantlr 721	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
209	2	rexrd 11186	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
210	3	rexrd 11186	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
211	209, 210	jca 516	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
212		df-icc 13296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)})
213	212	elixx3g 13302	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑢 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
214	213	simprbi 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))
215	214	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢)
216	212	elixx3g 13302	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)))
217	216	simprbi 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))
218	217	simprd 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵)
219	215, 218	anim12i 619	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵))
220		ioossioo 13385	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
221	211, 219, 220	syl2an 602	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
222	5	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
223	221, 222	sstrd 3925	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
224	223	sselda 3915	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
225		iftrue 4460	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
226	224, 225	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
227	226	adantllr 725	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
228	208, 227	breqtrrd 5100	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
229		breq2 5076	. . . . . . . . . . . . 13 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
230		breq2 5076	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
231	6	sselda 3915	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ)
232	231	adantlr 721	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ)
233	71	adantll 720	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
234	232, 233	syldan 597	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
235		0le0 12273	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
236	235	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ≤ 0)
237	229, 230, 234, 236	ifbothda 4493	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
238	237	ad2antrr 732	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
239	203, 204, 228, 238	ifbothda 4493	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
240	239	ralrimivw 3135	. . . . . . . . 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 4505	. . . . . . . . . . . 12 ⊢ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V
244	243	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
245		eqidd 2740	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
246		eqidd 2740	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
247	241, 242, 244, 245, 246	ofrfval2 7641	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
248	247	ad2antrr 732	. . . . . . . . 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 258	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
250		itg2le 25724	. . . . . . . 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 1379	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))))
252		itg2lecl 25723	. . . . . . 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 1379	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
254	8	ffvelcdmda 7025	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
255	254	adantlr 721	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
256	224, 255	syldan 597	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
257	256	adantllr 725	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
258	205, 39	sylan2 599	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
259	258	adantll 720	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
260	259	adantlr 721	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
261	257, 260	subcld 11496	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
262	261	abscld 15392	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
263	261	absge0d 15400	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
264		elrege0 13398	. . . . . . . . . 10 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,)+∞) ↔ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ ∧ 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
265	262, 263, 264	sylanbrc 589	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,)+∞))
266	74	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,)+∞))
267	265, 266	ifclda 4490	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,)+∞))
268	267	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,)+∞))
269	268	fmpttd 7056	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,)+∞))
270	262	rexrd 11186	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
271		elxrge0 13401	. . . . . . . . . . 11 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
272	270, 263, 271	sylanbrc 589	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞))
273	82	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
274	272, 273	ifclda 4490	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
275	274	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
276	275	fmpttd 7056	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞))
277		recncf 24887	. . . . . . . . . . . . 13 ⊢ ℜ ∈ (ℂ–cn→ℝ)
278		prid1g 4692	. . . . . . . . . . . . 13 ⊢ (ℜ ∈ (ℂ–cn→ℝ) → ℜ ∈ {ℜ, ℑ})
279	277, 278	ax-mp 5	. . . . . . . . . . . 12 ⊢ ℜ ∈ {ℜ, ℑ}
280		ftc1anclem2 38061	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℜ ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
281	279, 280	mp3an3 1458	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
282	8, 7, 281	syl2anc 590	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
283		imcncf 24888	. . . . . . . . . . . . 13 ⊢ ℑ ∈ (ℂ–cn→ℝ)
284		prid2g 4693	. . . . . . . . . . . . 13 ⊢ (ℑ ∈ (ℂ–cn→ℝ) → ℑ ∈ {ℜ, ℑ})
285	283, 284	ax-mp 5	. . . . . . . . . . . 12 ⊢ ℑ ∈ {ℜ, ℑ}
286		ftc1anclem2 38061	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℑ ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
287	285, 286	mp3an3 1458	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
288	8, 7, 287	syl2anc 590	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
289	282, 288	readdcld 11165	. . . . . . . . 9 ⊢ (𝜑 → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
290	289	ad2antrr 732	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
291	201, 290	readdcld 11165	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) ∈ ℝ)
292		ge0addcl 13404	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
293	292	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞))
294		ifcl 4500	. . . . . . . . . . . . . . 15 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
295	73, 74, 294	sylancl 592	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
296	295	fmpttd 7056	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
297	296	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
298	292	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞))
299	254	recld 15147	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘(𝐹‘𝑡)) ∈ ℝ)
300	299	recnd 11164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘(𝐹‘𝑡)) ∈ ℂ)
301	300	abscld 15392	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ)
302	300	absge0d 15400	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(ℜ‘(𝐹‘𝑡))))
303		elrege0 13398	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘(ℜ‘(𝐹‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘(ℜ‘(𝐹‘𝑡)))))
304	301, 302, 303	sylanbrc 589	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ (0[,)+∞))
305	74	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ (0[,)+∞))
306	304, 305	ifclda 4490	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
307	306	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
308	307	fmpttd 7056	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)):ℝ⟶(0[,)+∞))
309	254	imcld 15148	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℑ‘(𝐹‘𝑡)) ∈ ℝ)
310	309	recnd 11164	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℑ‘(𝐹‘𝑡)) ∈ ℂ)
311	310	abscld 15392	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ)
312	310	absge0d 15400	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(ℑ‘(𝐹‘𝑡))))
313		elrege0 13398	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘(ℑ‘(𝐹‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘(ℑ‘(𝐹‘𝑡)))))
314	311, 312, 313	sylanbrc 589	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ (0[,)+∞))
315	314, 305	ifclda 4490	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
316	315	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
317	316	fmpttd 7056	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)):ℝ⟶(0[,)+∞))
318	298, 308, 317, 241, 241, 109	off 7638	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))):ℝ⟶(0[,)+∞))
319	318	adantr 481	. . . . . . . . . . . 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 7638	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,)+∞))
322		fss 6671	. . . . . . . . . . 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 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞))
324	323	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞))
325		0xr 11183	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ*
326	325	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ ℝ*)
327	270, 326	ifclda 4490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
328	254	adantlr 721	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
329	39	adantll 720	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
330	232, 329	syldan 597	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
331	328, 330	subcld 11496	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
332	331	abscld 15392	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
333	332	rexrd 11186	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
334	325	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ*)
335	333, 334	ifclda 4490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
336	335	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
337	330	abscld 15392	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
338		0red 11138	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ)
339	337, 338	ifclda 4490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
340		0red 11138	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ)
341	301, 340	ifclda 4490	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ ℝ)
342	311, 340	ifclda 4490	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ ℝ)
343	341, 342	readdcld 11165	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ ℝ)
344	343	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ ℝ)
345	339, 344	readdcld 11165	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
346	345	rexrd 11186	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ*)
347	346	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ*)
348		breq1 5075	. . . . . . . . . . . . 13 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
349		breq1 5075	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
350	224	adantllr 725	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
351	332	leidd 11707	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
352	351	adantlr 721	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
353		iftrue 4460	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
354	353	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
355	352, 354	breqtrrd 5100	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
356	350, 355	syldan 597	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
357		breq2 5076	. . . . . . . . . . . . . . 15 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
358		breq2 5076	. . . . . . . . . . . . . . 15 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
359	331	absge0d 15400	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
360	357, 358, 359, 236	ifbothda 4493	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
361	360	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
362	348, 349, 356, 361	ifbothda 4493	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
363	254	negcld 11483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → -(𝐹‘𝑡) ∈ ℂ)
364	363	adantlr 721	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → -(𝐹‘𝑡) ∈ ℂ)
365	330, 364	addcld 11155	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)) ∈ ℂ)
366	365	abscld 15392	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ∈ ℝ)
367	363	abscld 15392	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ∈ ℝ)
368	367	adantlr 721	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ∈ ℝ)
369	337, 368	readdcld 11165	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))) ∈ ℝ)
370	301, 311	readdcld 11165	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ ℝ)
371	370	adantlr 721	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ ℝ)
372	337, 371	readdcld 11165	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))) ∈ ℝ)
373	330, 364	abstrid 15412	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))))
374		mulcl 11113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((i ∈ ℂ ∧ (ℑ‘(𝐹‘𝑡)) ∈ ℂ) → (i · (ℑ‘(𝐹‘𝑡))) ∈ ℂ)
375	31, 310, 374	sylancr 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (i · (ℑ‘(𝐹‘𝑡))) ∈ ℂ)
376	300, 375	abstrid 15412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(i · (ℑ‘(𝐹‘𝑡))))))
377	254	absnegd 15405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) = (abs‘(𝐹‘𝑡)))
378	254	replimd 15150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) = ((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡)))))
379	378	fveq2d 6831	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) = (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))))
380	377, 379	eqtrd 2774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) = (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))))
381		absmul 15247	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((i ∈ ℂ ∧ (ℑ‘(𝐹‘𝑡)) ∈ ℂ) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))))
382	31, 310, 381	sylancr 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))))
383	182	oveq1i 7366	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))) = (1 · (abs‘(ℑ‘(𝐹‘𝑡))))
384	382, 383	eqtrdi 2790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = (1 · (abs‘(ℑ‘(𝐹‘𝑡)))))
385	311	recnd 11164	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℂ)
386	385	mullidd 11154	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (1 · (abs‘(ℑ‘(𝐹‘𝑡)))) = (abs‘(ℑ‘(𝐹‘𝑡))))
387	384, 386	eqtr2d 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) = (abs‘(i · (ℑ‘(𝐹‘𝑡)))))
388	387	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) = ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(i · (ℑ‘(𝐹‘𝑡))))))
389	376, 380, 388	3brtr4d 5104	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
390	389	adantlr 721	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
391	368, 371, 337, 390	leadd2dd 11756	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
392	366, 369, 372, 373, 391	letrd 11294	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
393	328, 330	abssubd 15409	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡))))
394	353	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
395	330, 328	negsubd 11502	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)) = (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡)))
396	395	fveq2d 6831	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡))))
397	393, 394, 396	3eqtr4d 2784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))))
398		iftrue 4460	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
399	398	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
400	392, 397, 399	3brtr4d 5104	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
401	400	ex 413	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)))
402	235	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → 0 ≤ 0)
403		iffalse 4463	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0)
404		iffalse 4463	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = 0)
405	402, 403, 404	3brtr4d 5104	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
406	401, 405	pm2.61d1 181	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
407		iftrue 4460	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) = (abs‘(ℜ‘(𝐹‘𝑡))))
408		iftrue 4460	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) = (abs‘(ℑ‘(𝐹‘𝑡))))
409	407, 408	oveq12d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
410	225, 409	oveq12d 7374	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
411	410, 398	eqtr4d 2777	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
412		00id 11312	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 0) = 0
413	412	oveq2i 7367	. . . . . . . . . . . . . . . . 17 ⊢ (0 + (0 + 0)) = (0 + 0)
414	413, 412	eqtri 2762	. . . . . . . . . . . . . . . 16 ⊢ (0 + (0 + 0)) = 0
415		iffalse 4463	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
416		iffalse 4463	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) = 0)
417		iffalse 4463	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) = 0)
418	416, 417	oveq12d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (0 + 0))
419	415, 418	oveq12d 7374	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = (0 + (0 + 0)))
420	414, 419, 404	3eqtr4a 2800	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
421	411, 420	pm2.61i 183	. . . . . . . . . . . . . 14 ⊢ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)
422	406, 421	breqtrrdi 5114	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
423	422	adantr 481	. . . . . . . . . . . 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 13104	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
425	424	ralrimivw 3135	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
426		fvex 6840	. . . . . . . . . . . . . 14 ⊢ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V
427	426, 17	ifex 4505	. . . . . . . . . . . . 13 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V
428	427	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V)
429		ovexd 7391	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ V)
430		eqidd 2740	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
431		ovexd 7391	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ V)
432	341	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ ℝ)
433	342	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ ℝ)
434		eqidd 2740	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))
435		eqidd 2740	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))
436	241, 432, 433, 434, 435	offval2 7640	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
437	241, 244, 431, 246, 436	offval2 7640	. . . . . . . . . . . 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 7641	. . . . . . . . . . 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 732	. . . . . . . . . 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 258	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘r ≤ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
441		itg2le 25724	. . . . . . . . 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 1379	. . . . . . . 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 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 𝐷 ⊆ ℝ)
444	243	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
445		eldifn 4062	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
446	445	iffalsed 4465	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
447	446	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
448		ovexd 7391	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ V)
449	41, 42, 448, 45, 52	offval2 7640	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔)) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
450	39, 449, 56, 57	fmptco 7071	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) = (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
451	450	reseq1d 5930	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) = ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ 𝐷))
452	6	resmptd 5992	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
453	451, 452	sylan9eqr 2796	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
454	225	mpteq2ia 5167	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
455	453, 454	eqtr4di 2792	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
456		i1fmbf 25660	. . . . . . . . . . . . . . 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 6665	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐹 = 𝐷)
459		iblmbf 25752	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
460		mbfdm 25611	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
461	7, 459, 460	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐹 ∈ dom vol)
462	458, 461	eqeltrrd 2840	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ dom vol)
463		mbfres 25629	. . . . . . . . . . . . . 14 ⊢ (((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ∈ MblFn ∧ 𝐷 ∈ dom vol) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) ∈ MblFn)
464	457, 462, 463	syl2anr 603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) ∈ MblFn)
465	455, 464	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
466	443, 15, 444, 447, 465	mbfss 25631	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
467	200	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
468		0cnd 11128	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
469	300, 468	ifclda 4490	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℂ)
470	469	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℂ)
471		eqidd 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)))
472	54	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → abs:ℂ⟶ℝ)
473	472	feqmptd 6895	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
474		fveq2 6827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) → (abs‘𝑥) = (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)))
475		fvif 6843	. . . . . . . . . . . . . . . . . 18 ⊢ (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0))
476		abs0 15238	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs‘0) = 0
477		ifeq2 4459	. . . . . . . . . . . . . . . . . . 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 2762	. . . . . . . . . . . . . . . . 17 ⊢ (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)
480	474, 479	eqtrdi 2790	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) → (abs‘𝑥) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))
481	470, 471, 473, 480	fmptco 7071	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))
482	299, 340	ifclda 4490	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
483	482	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
484	483	fmpttd 7056	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)):ℝ⟶ℝ)
485	14	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℝ ∈ dom vol)
486	482	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
487	445	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
488	487	iffalsed 4465	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) = 0)
489		iftrue 4460	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) = (ℜ‘(𝐹‘𝑡)))
490	489	mpteq2ia 5167	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡)))
491	8	feqmptd 6895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
492	7, 459	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 ∈ MblFn)
493	491, 492	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn)
494	254	ismbfcn2 25623	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)))
495	493, 494	mpbid 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))
496	495	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn)
497	490, 496	eqeltrid 2843	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn)
498	6, 485, 486, 488, 497	mbfss 25631	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn)
499		ftc1anclem1 38060	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) ∈ MblFn)
500	484, 498, 499	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) ∈ MblFn)
501	481, 500	eqeltrrd 2840	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∈ MblFn)
502	501, 308, 282, 317, 288	itg2addnc 38041	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
503	502, 289	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ (𝜑 → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
504	503	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
505	466, 297, 467, 319, 504	itg2addnc 38041	. . . . . . . . . 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 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
507	506	oveq2d 7372	. . . . . . . . . 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 2774	. . . . . . . . 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 481	. . . . . . . 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 5098	. . . . . . 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 25723	. . . . . . 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 1379	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ)
513	69, 78, 253, 269, 512	itg2addnc 38041	. . . . 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 7640	. . . . . . . . 9 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
515		eqeq2 2751	. . . . . . . . . . 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 2751	. . . . . . . . . . 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 4460	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
518	23, 517	oveq12d 7374	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
519	518	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
520		iffalse 4463	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
521		iffalse 4463	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0)
522	520, 521	oveq12d 7374	. . . . . . . . . . . . 13 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (0 + 0))
523	522, 412	eqtrdi 2790	. . . . . . . . . . . 12 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0)
524	523	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0)
525	515, 516, 519, 524	ifbothda 4493	. . . . . . . . . 10 ⊢ (𝜑 → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0))
526	525	mpteq2dv 5166	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
527	514, 526	eqtrd 2774	. . . . . . . 8 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
528	527	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
529		simplr 774	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
530	258	abscld 15392	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
531	530	recnd 11164	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
532	529, 531	sylan 586	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
533	262	recnd 11164	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℂ)
534	532, 533	addcomd 11339	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
535	534	ifeq1da 4486	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
536	535	mpteq2dv 5166	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
537	528, 536	eqtrd 2774	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
538	537	fveq2d 6831	. . . . 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 2776	. . . 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 602	. . 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 481	. 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 12944	. . . 4 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
543	542	2halvesd 12414	. . 3 ⊢ (𝑦 ∈ ℝ+ → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
544	543	ad3antlr 737	. 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 5103	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 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   ≠ wne 2934  ∀wral 3053  ∃wrex 3063  Vcvv 3431   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  ifcif 4454  {csn 4555  {cpr 4557   class class class wbr 5072   ↦ cmpt 5153   × cxp 5616  dom cdm 5618  ran crn 5619   ↾ cres 5620   “ cima 5621   ∘ ccom 5622   Fn wfn 6480  ⟶wf 6481  ‘cfv 6485  (class class class)co 7356   ∘_f cof 7618   ∘_r cofr 7619  supcsup 9343  ℂcc 11027  ℝcr 11028  0cc0 11029  1c1 11030  ici 11031   + caddc 11032   · cmul 11034  +∞cpnf 11167  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171   − cmin 11368  -cneg 11369   / cdiv 11798  2c2 12227  ℝ⁺crp 12933  (,)cioo 13289  [,)cico 13291  [,]cicc 13292  ℜcre 15050  ℑcim 15051  abscabs 15187  –cn→ccncf 24861  volcvol 25448  MblFncmbf 25599  ∫₁citg1 25600  ∫₂citg2 25601  𝐿¹cibl 25602  ∫citg 25603  0_𝑝c0p 25654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-inf2 9553  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107  ax-addf 11108

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-disj 5040  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-ofr 7621  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8633  df-map 8765  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9314  df-sup 9345  df-inf 9346  df-oi 9415  df-dju 9816  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-n0 12429  df-z 12516  df-uz 12780  df-q 12890  df-rp 12934  df-xneg 13054  df-xadd 13055  df-xmul 13056  df-ioo 13293  df-ico 13295  df-icc 13296  df-fz 13453  df-fzo 13600  df-fl 13742  df-seq 13955  df-exp 14015  df-hash 14284  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15441  df-rlim 15442  df-sum 15640  df-rest 17376  df-topgen 17397  df-psmet 21339  df-xmet 21340  df-met 21341  df-bl 21342  df-mopn 21343  df-top 22877  df-topon 22894  df-bases 22929  df-cmp 23370  df-cncf 24863  df-ovol 25449  df-vol 25450  df-mbf 25604  df-itg1 25605  df-itg2 25606  df-ibl 25607  df-0p 25655

This theorem is referenced by:  ftc1anc  38068