Theorem ftc1anclem8 33492

Description: Lemma for ftc1anc 33493. (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 33491	. 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 798	. . . 4 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
11		3simpa 1058	. . . 4 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤) → (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)))
12		ioossre 12235	. . . . . . . . 9 ⊢ (𝑢(,)𝑤) ⊆ ℝ
13	12	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑢(,)𝑤) ⊆ ℝ)
14		rembl 23308	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
15	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ℝ ∈ dom vol)
16		fvex 6201	. . . . . . . . . 10 ⊢ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ V
17		c0ex 10034	. . . . . . . . . 10 ⊢ 0 ∈ V
18	16, 17	ifex 4156	. . . . . . . . 9 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V
19	18	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
20		eldifn 3733	. . . . . . . . . 10 ⊢ (𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤)) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
21	20	adantl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤))) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
22	21	iffalsed 4097	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
23		iftrue 4092	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
24	23	mpteq2ia 4740	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
25		resmpt 5449	. . . . . . . . . . . 12 ⊢ ((𝑢(,)𝑤) ⊆ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
26	12, 25	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
27	24, 26	eqtr4i 2647	. . . . . . . . . 10 ⊢ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤))
28		i1ff 23443	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
29	28	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
30	29	recnd 10068	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℂ)
31		ax-icn 9995	. . . . . . . . . . . . . . . . 17 ⊢ i ∈ ℂ
32		i1ff 23443	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
33	32	ffvelrnda 6359	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
34	33	recnd 10068	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
35		mulcl 10020	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ)
36	31, 34, 35	sylancr 695	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
37		addcl 10018	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
38	30, 36, 37	syl2an 494	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
39	38	anandirs 874	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
40		reex 10027	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
41	40	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ℝ ∈ V)
42	29	adantlr 751	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
43	36	adantll 750	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
44	28	feqmptd 6249	. . . . . . . . . . . . . . . 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 5163	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i)
49	48	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i))
50	32	feqmptd 6249	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡)))
51	46, 47, 33, 49, 50	offval2 6914	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ dom ∫1 → ((ℝ × {i}) ∘𝑓 · 𝑔) = (𝑡 ∈ ℝ ↦ (i · (𝑔‘𝑡))))
52	51	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((ℝ × {i}) ∘𝑓 · 𝑔) = (𝑡 ∈ ℝ ↦ (i · (𝑔‘𝑡))))
53	41, 42, 43, 45, 52	offval2 6914	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔)) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
54		absf 14077	. . . . . . . . . . . . . . . 16 ⊢ abs:ℂ⟶ℝ
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → abs:ℂ⟶ℝ)
56	55	feqmptd 6249	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
57		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) → (abs‘𝑥) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
58	39, 53, 56, 57	fmptco 6396	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) = (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
59		ftc1anclem3 33487	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ∈ dom ∫1)
60	58, 59	eqeltrrd 2702	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ dom ∫1)
61		i1fmbf 23442	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn)
62	60, 61	syl 17	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn)
63		ioombl 23333	. . . . . . . . . . 11 ⊢ (𝑢(,)𝑤) ∈ dom vol
64		mbfres 23411	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn ∧ (𝑢(,)𝑤) ∈ dom vol) → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) ∈ MblFn)
65	62, 63, 64	sylancl 694	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) ∈ MblFn)
66	27, 65	syl5eqel 2705	. . . . . . . . 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 23413	. . . . . . 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 14175	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
71	39	absge0d 14183	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
72		elrege0 12278	. . . . . . . . . 10 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ↔ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
73	70, 71, 72	sylanbrc 698	. . . . . . . . 9 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞))
74		0e0icopnf 12282	. . . . . . . . 9 ⊢ 0 ∈ (0[,)+∞)
75		ifcl 4130	. . . . . . . . 9 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
76	73, 74, 75	sylancl 694	. . . . . . . 8 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
77		eqid 2622	. . . . . . . 8 ⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
78	76, 77	fmptd 6385	. . . . . . 7 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
79	78	ad2antlr 763	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
80	70	rexrd 10089	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ*)
81		elxrge0 12281	. . . . . . . . . . 11 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ↔ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
82	80, 71, 81	sylanbrc 698	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞))
83		0e0iccpnf 12283	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]+∞)
84		ifcl 4130	. . . . . . . . . 10 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
85	82, 83, 84	sylancl 694	. . . . . . . . 9 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
86	85, 77	fmptd 6385	. . . . . . . 8 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
87	86	ad2antlr 763	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
88		ifcl 4130	. . . . . . . . . . 11 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
89	82, 83, 88	sylancl 694	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
90		eqid 2622	. . . . . . . . . 10 ⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
91	89, 90	fmptd 6385	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
92		ffn 6045	. . . . . . . . . . . . . . 15 ⊢ (𝑓:ℝ⟶ℝ → 𝑓 Fn ℝ)
93		frn 6053	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:ℝ⟶ℝ → ran 𝑓 ⊆ ℝ)
94		ax-resscn 9993	. . . . . . . . . . . . . . . 16 ⊢ ℝ ⊆ ℂ
95	93, 94	syl6ss 3615	. . . . . . . . . . . . . . 15 ⊢ (𝑓:ℝ⟶ℝ → ran 𝑓 ⊆ ℂ)
96		ffn 6045	. . . . . . . . . . . . . . . . 17 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ)
97	54, 96	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ abs Fn ℂ
98		fnco 5999	. . . . . . . . . . . . . . . 16 ⊢ ((abs Fn ℂ ∧ 𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ) → (abs ∘ 𝑓) Fn ℝ)
99	97, 98	mp3an1 1411	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ) → (abs ∘ 𝑓) Fn ℝ)
100	92, 95, 99	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (𝑓:ℝ⟶ℝ → (abs ∘ 𝑓) Fn ℝ)
101	28, 100	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ 𝑓) Fn ℝ)
102	101	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑓) Fn ℝ)
103		ffn 6045	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℝ⟶ℝ → 𝑔 Fn ℝ)
104		frn 6053	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℝ⟶ℝ → ran 𝑔 ⊆ ℝ)
105	104, 94	syl6ss 3615	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℝ⟶ℝ → ran 𝑔 ⊆ ℂ)
106		fnco 5999	. . . . . . . . . . . . . . . 16 ⊢ ((abs Fn ℂ ∧ 𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ) → (abs ∘ 𝑔) Fn ℝ)
107	97, 106	mp3an1 1411	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ) → (abs ∘ 𝑔) Fn ℝ)
108	103, 105, 107	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℝ⟶ℝ → (abs ∘ 𝑔) Fn ℝ)
109	32, 108	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (abs ∘ 𝑔) Fn ℝ)
110	109	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑔) Fn ℝ)
111		inidm 3822	. . . . . . . . . . . 12 ⊢ (ℝ ∩ ℝ) = ℝ
112	28	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑓:ℝ⟶ℝ)
113		fvco3 6275	. . . . . . . . . . . . 13 ⊢ ((𝑓:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑓)‘𝑡) = (abs‘(𝑓‘𝑡)))
114	112, 113	sylan 488	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑓)‘𝑡) = (abs‘(𝑓‘𝑡)))
115	32	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑔:ℝ⟶ℝ)
116		fvco3 6275	. . . . . . . . . . . . 13 ⊢ ((𝑔:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑔)‘𝑡) = (abs‘(𝑔‘𝑡)))
117	115, 116	sylan 488	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑔)‘𝑡) = (abs‘(𝑔‘𝑡)))
118	102, 110, 41, 41, 111, 114, 117	offval 6904	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ 𝑓) ∘𝑓 + (abs ∘ 𝑔)) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
119	30	addid1d 10236	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + 0) = (𝑓‘𝑡))
120	119	mpteq2dva 4744	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + 0)) = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
121	40	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ℝ ∈ V)
122	17	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ∈ V)
123	31	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → i ∈ ℂ)
124	48	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i))
125		fconstmpt 5163	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
126	125	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
127	121, 123, 122, 124, 126	offval2 6914	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ((ℝ × {i}) ∘𝑓 · (ℝ × {0})) = (𝑡 ∈ ℝ ↦ (i · 0)))
128		it0e0 11254	. . . . . . . . . . . . . . . . . . 19 ⊢ (i · 0) = 0
129	128	mpteq2i 4741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ ℝ ↦ (i · 0)) = (𝑡 ∈ ℝ ↦ 0)
130	127, 129	syl6eq 2672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ((ℝ × {i}) ∘𝑓 · (ℝ × {0})) = (𝑡 ∈ ℝ ↦ 0))
131	121, 29, 122, 44, 130	offval2 6914	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ dom ∫1 → (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · (ℝ × {0}))) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + 0)))
132	120, 131, 44	3eqtr4d 2666	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ dom ∫1 → (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · (ℝ × {0}))) = 𝑓)
133	132	coeq2d 5284	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · (ℝ × {0})))) = (abs ∘ 𝑓))
134		i1f0 23454	. . . . . . . . . . . . . . 15 ⊢ (ℝ × {0}) ∈ dom ∫1
135		ftc1anclem3 33487	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ (ℝ × {0}) ∈ dom ∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · (ℝ × {0})))) ∈ dom ∫1)
136	134, 135	mpan2 707	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · (ℝ × {0})))) ∈ dom ∫1)
137	133, 136	eqeltrrd 2702	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ 𝑓) ∈ dom ∫1)
138	137	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑓) ∈ dom ∫1)
139		coeq2 5280	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (abs ∘ 𝑓) = (abs ∘ 𝑔))
140	139	eleq1d 2686	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((abs ∘ 𝑓) ∈ dom ∫1 ↔ (abs ∘ 𝑔) ∈ dom ∫1))
141	140, 137	vtoclga 3272	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (abs ∘ 𝑔) ∈ dom ∫1)
142	141	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑔) ∈ dom ∫1)
143	138, 142	i1fadd 23462	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ 𝑓) ∘𝑓 + (abs ∘ 𝑔)) ∈ dom ∫1)
144	118, 143	eqeltrrd 2702	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1)
145	30	abscld 14175	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓‘𝑡)) ∈ ℝ)
146	30	absge0d 14183	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(𝑓‘𝑡)))
147		elrege0 12278	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘(𝑓‘𝑡)) ∈ (0[,)+∞) ↔ ((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑓‘𝑡))))
148	145, 146, 147	sylanbrc 698	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓‘𝑡)) ∈ (0[,)+∞))
149	34	abscld 14175	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ ℝ)
150	34	absge0d 14183	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(𝑔‘𝑡)))
151		elrege0 12278	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘(𝑔‘𝑡)) ∈ (0[,)+∞) ↔ ((abs‘(𝑔‘𝑡)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑔‘𝑡))))
152	149, 150, 151	sylanbrc 698	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ (0[,)+∞))
153		ge0addcl 12284	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑓‘𝑡)) ∈ (0[,)+∞) ∧ (abs‘(𝑔‘𝑡)) ∈ (0[,)+∞)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
154	148, 152, 153	syl2an 494	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
155	154	anandirs 874	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
156		eqid 2622	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
157	155, 156	fmptd 6385	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞))
158		0plef 23439	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞) ↔ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶ℝ ∧ 0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
159	157, 158	sylib 208	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶ℝ ∧ 0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
160	159	simprd 479	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
161		itg2itg1 23503	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) = (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
162		itg1cl 23452	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
163	162	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
164	161, 163	eqeltrd 2701	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
165	144, 160, 164	syl2anc 693	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
166		icossicc 12260	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
167		fss 6056	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞))
168	157, 166, 167	sylancl 694	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞))
169		0re 10040	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
170		ifcl 4130	. . . . . . . . . . . . . 14 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
171	70, 169, 170	sylancl 694	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
172		readdcl 10019	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ (abs‘(𝑔‘𝑡)) ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
173	145, 149, 172	syl2an 494	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
174	173	anandirs 874	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
175	70	leidd 10594	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
176		breq1 4656	. . . . . . . . . . . . . . 15 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
177		breq1 4656	. . . . . . . . . . . . . . 15 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
178	176, 177	ifboth 4124	. . . . . . . . . . . . . 14 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
179	175, 71, 178	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
180		abstri 14070	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
181	30, 36, 180	syl2an 494	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
182	181	anandirs 874	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
183		absmul 14034	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (abs‘(i · (𝑔‘𝑡))) = ((abs‘i) · (abs‘(𝑔‘𝑡))))
184	31, 34, 183	sylancr 695	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = ((abs‘i) · (abs‘(𝑔‘𝑡))))
185		absi 14026	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs‘i) = 1
186	185	oveq1i 6660	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘i) · (abs‘(𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡)))
187	184, 186	syl6eq 2672	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡))))
188	149	recnd 10068	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ ℂ)
189	188	mulid2d 10058	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (1 · (abs‘(𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
190	187, 189	eqtrd 2656	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
191	190	adantll 750	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
192	191	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))) = ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
193	182, 192	breqtrd 4679	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
194	171, 70, 174, 179, 193	letrd 10194	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
195	194	ralrimiva 2966	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ∀𝑡 ∈ ℝ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
196		eqidd 2623	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
197		eqidd 2623	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
198	41, 171, 174, 196, 197	ofrfval2 6915	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
199	195, 198	mpbird 247	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
200		itg2le 23506	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
201	91, 168, 199, 200	syl3anc 1326	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
202		itg2lecl 23505	. . . . . . . . 9 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
203	91, 165, 201, 202	syl3anc 1326	. . . . . . . 8 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
204	203	ad2antlr 763	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
205	91	ad2antlr 763	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
206		breq1 4656	. . . . . . . . . . 11 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
207		breq1 4656	. . . . . . . . . . 11 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
208		elioore 12205	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
209	208, 175	sylan2 491	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
210	209	adantll 750	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
211	210	adantlr 751	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
212	2	rexrd 10089	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
213	3	rexrd 10089	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
214	212, 213	jca 554	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
215		df-icc 12182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)})
216	215	elixx3g 12188	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑢 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
217	216	simprbi 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))
218	217	simpld 475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢)
219	215	elixx3g 12188	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)))
220	219	simprbi 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))
221	220	simprd 479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵)
222	218, 221	anim12i 590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵))
223		ioossioo 12265	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
224	214, 222, 223	syl2an 494	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
225	5	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
226	224, 225	sstrd 3613	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
227	226	sselda 3603	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
228		iftrue 4092	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
229	227, 228	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
230	229	adantllr 755	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
231	211, 230	breqtrrd 4681	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
232		breq2 4657	. . . . . . . . . . . . 13 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
233		breq2 4657	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
234	6	sselda 3603	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ)
235	234	adantlr 751	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ)
236	71	adantll 750	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
237	235, 236	syldan 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
238		0le0 11110	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
239	238	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ≤ 0)
240	232, 233, 237, 239	ifbothda 4123	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
241	240	ad2antrr 762	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
242	206, 207, 231, 241	ifbothda 4123	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
243	242	ralrimivw 2967	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
244	40	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ ∈ V)
245	18	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
246	16, 17	ifex 4156	. . . . . . . . . . . 12 ⊢ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V
247	246	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
248		eqidd 2623	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
249		eqidd 2623	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
250	244, 245, 247, 248, 249	ofrfval2 6915	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
251	250	ad2antrr 762	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
252	243, 251	mpbird 247	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
253		itg2le 23506	. . . . . . . 8 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))))
254	87, 205, 252, 253	syl3anc 1326	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))))
255		itg2lecl 23505	. . . . . . 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))) ∈ ℝ)
256	87, 204, 254, 255	syl3anc 1326	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
257	8	ffvelrnda 6359	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
258	257	adantlr 751	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
259	227, 258	syldan 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
260	259	adantllr 755	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
261	208, 39	sylan2 491	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
262	261	adantll 750	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
263	262	adantlr 751	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
264	260, 263	subcld 10392	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
265	264	abscld 14175	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
266	264	absge0d 14183	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
267		elrege0 12278	. . . . . . . . . 10 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,)+∞) ↔ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ ∧ 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
268	265, 266, 267	sylanbrc 698	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,)+∞))
269	74	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,)+∞))
270	268, 269	ifclda 4120	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,)+∞))
271	270	adantr 481	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,)+∞))
272		eqid 2622	. . . . . . 7 ⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
273	271, 272	fmptd 6385	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,)+∞))
274	265	rexrd 10089	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
275		elxrge0 12281	. . . . . . . . . . 11 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
276	274, 266, 275	sylanbrc 698	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞))
277	83	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
278	276, 277	ifclda 4120	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
279	278	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
280	279, 272	fmptd 6385	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞))
281		recncf 22705	. . . . . . . . . . . . 13 ⊢ ℜ ∈ (ℂ–cn→ℝ)
282		prid1g 4295	. . . . . . . . . . . . 13 ⊢ (ℜ ∈ (ℂ–cn→ℝ) → ℜ ∈ {ℜ, ℑ})
283	281, 282	ax-mp 5	. . . . . . . . . . . 12 ⊢ ℜ ∈ {ℜ, ℑ}
284		ftc1anclem2 33486	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℜ ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
285	283, 284	mp3an3 1413	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
286	8, 7, 285	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
287		imcncf 22706	. . . . . . . . . . . . 13 ⊢ ℑ ∈ (ℂ–cn→ℝ)
288		prid2g 4296	. . . . . . . . . . . . 13 ⊢ (ℑ ∈ (ℂ–cn→ℝ) → ℑ ∈ {ℜ, ℑ})
289	287, 288	ax-mp 5	. . . . . . . . . . . 12 ⊢ ℑ ∈ {ℜ, ℑ}
290		ftc1anclem2 33486	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℑ ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
291	289, 290	mp3an3 1413	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
292	8, 7, 291	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
293	286, 292	readdcld 10069	. . . . . . . . 9 ⊢ (𝜑 → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
294	293	ad2antrr 762	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
295	204, 294	readdcld 10069	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) ∈ ℝ)
296		ge0addcl 12284	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
297	296	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞))
298		ifcl 4130	. . . . . . . . . . . . . . 15 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
299	73, 74, 298	sylancl 694	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
300	299, 90	fmptd 6385	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
301	300	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
302	296	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞))
303	257	recld 13934	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘(𝐹‘𝑡)) ∈ ℝ)
304	303	recnd 10068	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘(𝐹‘𝑡)) ∈ ℂ)
305	304	abscld 14175	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ)
306	304	absge0d 14183	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(ℜ‘(𝐹‘𝑡))))
307		elrege0 12278	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘(ℜ‘(𝐹‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘(ℜ‘(𝐹‘𝑡)))))
308	305, 306, 307	sylanbrc 698	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ (0[,)+∞))
309	74	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ (0[,)+∞))
310	308, 309	ifclda 4120	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
311	310	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
312		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))
313	311, 312	fmptd 6385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)):ℝ⟶(0[,)+∞))
314	257	imcld 13935	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℑ‘(𝐹‘𝑡)) ∈ ℝ)
315	314	recnd 10068	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℑ‘(𝐹‘𝑡)) ∈ ℂ)
316	315	abscld 14175	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ)
317	315	absge0d 14183	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(ℑ‘(𝐹‘𝑡))))
318		elrege0 12278	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘(ℑ‘(𝐹‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘(ℑ‘(𝐹‘𝑡)))))
319	316, 317, 318	sylanbrc 698	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ (0[,)+∞))
320	319, 309	ifclda 4120	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
321	320	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
322		eqid 2622	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))
323	321, 322	fmptd 6385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)):ℝ⟶(0[,)+∞))
324	302, 313, 323, 244, 244, 111	off 6912	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))):ℝ⟶(0[,)+∞))
325	324	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))):ℝ⟶(0[,)+∞))
326	40	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ℝ ∈ V)
327	297, 301, 325, 326, 326, 111	off 6912	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,)+∞))
328		fss 6056	. . . . . . . . . . 11 ⊢ ((((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞))
329	327, 166, 328	sylancl 694	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞))
330	329	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞))
331		0xr 10086	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ*
332	331	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ ℝ*)
333	274, 332	ifclda 4120	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
334	257	adantlr 751	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
335	39	adantll 750	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
336	235, 335	syldan 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
337	334, 336	subcld 10392	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
338	337	abscld 14175	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
339	338	rexrd 10089	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
340	331	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ*)
341	339, 340	ifclda 4120	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
342	341	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
343	336	abscld 14175	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
344		0red 10041	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ)
345	343, 344	ifclda 4120	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
346		0red 10041	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ)
347	305, 346	ifclda 4120	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ ℝ)
348	316, 346	ifclda 4120	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ ℝ)
349	347, 348	readdcld 10069	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ ℝ)
350	349	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ ℝ)
351	345, 350	readdcld 10069	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
352	351	rexrd 10089	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ*)
353	352	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ*)
354		breq1 4656	. . . . . . . . . . . . 13 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
355		breq1 4656	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
356	227	adantllr 755	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
357	338	leidd 10594	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
358	357	adantlr 751	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
359		iftrue 4092	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
360	359	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
361	358, 360	breqtrrd 4681	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
362	356, 361	syldan 487	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
363		breq2 4657	. . . . . . . . . . . . . . 15 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
364		breq2 4657	. . . . . . . . . . . . . . 15 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
365	337	absge0d 14183	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
366	363, 364, 365, 239	ifbothda 4123	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
367	366	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
368	354, 355, 362, 367	ifbothda 4123	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
369	257	negcld 10379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → -(𝐹‘𝑡) ∈ ℂ)
370	369	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → -(𝐹‘𝑡) ∈ ℂ)
371	336, 370	addcld 10059	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)) ∈ ℂ)
372	371	abscld 14175	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ∈ ℝ)
373	369	abscld 14175	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ∈ ℝ)
374	373	adantlr 751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ∈ ℝ)
375	343, 374	readdcld 10069	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))) ∈ ℝ)
376	305, 316	readdcld 10069	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ ℝ)
377	376	adantlr 751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ ℝ)
378	343, 377	readdcld 10069	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))) ∈ ℝ)
379	336, 370	abstrid 14195	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))))
380		mulcl 10020	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((i ∈ ℂ ∧ (ℑ‘(𝐹‘𝑡)) ∈ ℂ) → (i · (ℑ‘(𝐹‘𝑡))) ∈ ℂ)
381	31, 315, 380	sylancr 695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (i · (ℑ‘(𝐹‘𝑡))) ∈ ℂ)
382	304, 381	abstrid 14195	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(i · (ℑ‘(𝐹‘𝑡))))))
383	257	absnegd 14188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) = (abs‘(𝐹‘𝑡)))
384	257	replimd 13937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) = ((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡)))))
385	384	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) = (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))))
386	383, 385	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) = (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))))
387		absmul 14034	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((i ∈ ℂ ∧ (ℑ‘(𝐹‘𝑡)) ∈ ℂ) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))))
388	31, 315, 387	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))))
389	185	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))) = (1 · (abs‘(ℑ‘(𝐹‘𝑡))))
390	388, 389	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = (1 · (abs‘(ℑ‘(𝐹‘𝑡)))))
391	316	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℂ)
392	391	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (1 · (abs‘(ℑ‘(𝐹‘𝑡)))) = (abs‘(ℑ‘(𝐹‘𝑡))))
393	390, 392	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) = (abs‘(i · (ℑ‘(𝐹‘𝑡)))))
394	393	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) = ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(i · (ℑ‘(𝐹‘𝑡))))))
395	382, 386, 394	3brtr4d 4685	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
396	395	adantlr 751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
397	374, 377, 343, 396	leadd2dd 10642	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
398	372, 375, 378, 379, 397	letrd 10194	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
399	334, 336	abssubd 14192	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡))))
400	359	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
401	336, 334	negsubd 10398	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)) = (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡)))
402	401	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡))))
403	399, 400, 402	3eqtr4d 2666	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))))
404		iftrue 4092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
405	404	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
406	398, 403, 405	3brtr4d 4685	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
407	406	ex 450	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)))
408	238	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → 0 ≤ 0)
409		iffalse 4095	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0)
410		iffalse 4095	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = 0)
411	408, 409, 410	3brtr4d 4685	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
412	407, 411	pm2.61d1 171	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
413		iftrue 4092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) = (abs‘(ℜ‘(𝐹‘𝑡))))
414		iftrue 4092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) = (abs‘(ℑ‘(𝐹‘𝑡))))
415	413, 414	oveq12d 6668	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
416	228, 415	oveq12d 6668	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
417	416, 404	eqtr4d 2659	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
418		00id 10211	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 0) = 0
419	418	oveq2i 6661	. . . . . . . . . . . . . . . . 17 ⊢ (0 + (0 + 0)) = (0 + 0)
420	419, 418	eqtri 2644	. . . . . . . . . . . . . . . 16 ⊢ (0 + (0 + 0)) = 0
421		iffalse 4095	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
422		iffalse 4095	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) = 0)
423		iffalse 4095	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) = 0)
424	422, 423	oveq12d 6668	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (0 + 0))
425	421, 424	oveq12d 6668	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = (0 + (0 + 0)))
426	420, 425, 410	3eqtr4a 2682	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
427	417, 426	pm2.61i 176	. . . . . . . . . . . . . 14 ⊢ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)
428	412, 427	syl6breqr 4695	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
429	428	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
430	333, 342, 353, 368, 429	xrletrd 11993	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
431	430	ralrimivw 2967	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
432		fvex 6201	. . . . . . . . . . . . . 14 ⊢ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V
433	432, 17	ifex 4156	. . . . . . . . . . . . 13 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V
434	433	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V)
435		ovexd 6680	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ V)
436		eqidd 2623	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
437		ovexd 6680	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ V)
438	347	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ ℝ)
439	348	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ ℝ)
440		eqidd 2623	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))
441		eqidd 2623	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))
442	244, 438, 439, 440, 441	offval2 6914	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
443	244, 247, 437, 249, 442	offval2 6914	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
444	244, 434, 435, 436, 443	ofrfval2 6915	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
445	444	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
446	431, 445	mpbird 247	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
447		itg2le 23506	. . . . . . . . 9 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞) ∧ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
448	280, 330, 446, 447	syl3anc 1326	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
449	6	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 𝐷 ⊆ ℝ)
450	246	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
451		eldifn 3733	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
452	451	iffalsed 4097	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
453	452	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
454		ovexd 6680	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ V)
455	41, 42, 454, 45, 52	offval2 6914	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔)) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
456	39, 455, 56, 57	fmptco 6396	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) = (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
457	456	reseq1d 5395	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ↾ 𝐷) = ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ 𝐷))
458	6	resmptd 5452	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
459	457, 458	sylan9eqr 2678	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
460	228	mpteq2ia 4740	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
461	459, 460	syl6eqr 2674	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
462		i1fmbf 23442	. . . . . . . . . . . . . . 15 ⊢ ((abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ∈ dom ∫1 → (abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ∈ MblFn)
463	59, 462	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ∈ MblFn)
464		fdm 6051	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐷⟶ℂ → dom 𝐹 = 𝐷)
465	8, 464	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐹 = 𝐷)
466		iblmbf 23534	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
467		mbfdm 23395	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
468	7, 466, 467	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐹 ∈ dom vol)
469	465, 468	eqeltrrd 2702	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ dom vol)
470		mbfres 23411	. . . . . . . . . . . . . 14 ⊢ (((abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ∈ MblFn ∧ 𝐷 ∈ dom vol) → ((abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ↾ 𝐷) ∈ MblFn)
471	463, 469, 470	syl2anr 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘𝑓 + ((ℝ × {i}) ∘𝑓 · 𝑔))) ↾ 𝐷) ∈ MblFn)
472	461, 471	eqeltrrd 2702	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
473	449, 15, 450, 453, 472	mbfss 23413	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
474	203	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
475		0cnd 10033	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
476	304, 475	ifclda 4120	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℂ)
477	476	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℂ)
478		eqidd 2623	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)))
479	54	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → abs:ℂ⟶ℝ)
480	479	feqmptd 6249	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
481		fveq2 6191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) → (abs‘𝑥) = (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)))
482		fvif 6204	. . . . . . . . . . . . . . . . . 18 ⊢ (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0))
483		abs0 14025	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs‘0) = 0
484		ifeq2 4091	. . . . . . . . . . . . . . . . . . 19 ⊢ ((abs‘0) = 0 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))
485	483, 484	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)
486	482, 485	eqtri 2644	. . . . . . . . . . . . . . . . 17 ⊢ (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)
487	481, 486	syl6eq 2672	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) → (abs‘𝑥) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))
488	477, 478, 480, 487	fmptco 6396	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))
489	303, 346	ifclda 4120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
490	489	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
491		eqid 2622	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))
492	490, 491	fmptd 6385	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)):ℝ⟶ℝ)
493	14	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℝ ∈ dom vol)
494	489	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
495	451	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
496	495	iffalsed 4097	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) = 0)
497		iftrue 4092	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) = (ℜ‘(𝐹‘𝑡)))
498	497	mpteq2ia 4740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡)))
499	8	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
500	7, 466	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 ∈ MblFn)
501	499, 500	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn)
502	257	ismbfcn2 23406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)))
503	501, 502	mpbid 222	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))
504	503	simpld 475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn)
505	498, 504	syl5eqel 2705	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn)
506	6, 493, 494, 496, 505	mbfss 23413	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn)
507		ftc1anclem1 33485	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) ∈ MblFn)
508	492, 506, 507	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) ∈ MblFn)
509	488, 508	eqeltrrd 2702	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∈ MblFn)
510	509, 313, 286, 323, 292	itg2addnc 33464	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
511	510, 293	eqeltrd 2701	. . . . . . . . . . . 12 ⊢ (𝜑 → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
512	511	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
513	473, 301, 474, 325, 512	itg2addnc 33464	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
514	510	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
515	514	oveq2d 6666	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
516	513, 515	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
517	516	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
518	448, 517	breqtrd 4679	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))))
519		itg2lecl 23505	. . . . . . 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))) ∈ ℝ)
520	280, 295, 518, 519	syl3anc 1326	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ)
521	69, 79, 256, 273, 520	itg2addnc 33464	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))))
522	244, 245, 434, 248, 436	offval2 6914	. . . . . . . . 9 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
523		eqeq2 2633	. . . . . . . . . . 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)))
524		eqeq2 2633	. . . . . . . . . . 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)))
525		iftrue 4092	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
526	23, 525	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
527	526	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
528		iffalse 4095	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
529		iffalse 4095	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0)
530	528, 529	oveq12d 6668	. . . . . . . . . . . . 13 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (0 + 0))
531	530, 418	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0)
532	531	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0)
533	523, 524, 527, 532	ifbothda 4123	. . . . . . . . . 10 ⊢ (𝜑 → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0))
534	533	mpteq2dv 4745	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
535	522, 534	eqtrd 2656	. . . . . . . 8 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
536	535	ad2antrr 762	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
537		simplr 792	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
538	261	abscld 14175	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
539	538	recnd 10068	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
540	537, 539	sylan 488	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
541	265	recnd 10068	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℂ)
542	540, 541	addcomd 10238	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
543	542	ifeq1da 4116	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
544	543	mpteq2dv 4745	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
545	536, 544	eqtrd 2656	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
546	545	fveq2d 6195	. . . . 5 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
547	521, 546	eqtr3d 2658	. . . 4 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
548	10, 11, 547	syl2an 494	. . 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))))
549	548	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))))
550		rpcn 11841	. . . 4 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
551	550	2halvesd 11278	. . 3 ⊢ (𝑦 ∈ ℝ+ → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
552	551	ad3antlr 767	. 2 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
553	9, 549, 552	3brtr3d 4684	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 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  Vcvv 3200   ∖ cdif 3571   ∪ cun 3572   ⊆ wss 3574  ifcif 4086  {csn 4177  {cpr 4179   class class class wbr 4653   ↦ cmpt 4729   × cxp 5112  dom cdm 5114  ran crn 5115   ↾ cres 5116   “ cima 5117   ∘ ccom 5118   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888  (class class class)co 6650   ∘_𝑓 cof 6895   ∘_𝑟 cofr 6896  supcsup 8346  ℂcc 9934  ℝcr 9935  0cc0 9936  1c1 9937  ici 9938   + caddc 9939   · cmul 9941  +∞cpnf 10071  ℝ^*cxr 10073   < clt 10074   ≤ cle 10075   − cmin 10266  -cneg 10267   / cdiv 10684  2c2 11070  ℝ⁺crp 11832  (,)cioo 12175  [,)cico 12177  [,]cicc 12178  ℜcre 13837  ℑcim 13838  abscabs 13974  –cn→ccncf 22679  volcvol 23232  MblFncmbf 23383  ∫₁citg1 23384  ∫₂citg2 23385  𝐿¹cibl 23386  ∫citg 23387  0_𝑝c0p 23436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-ofr 6898  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-sum 14417  df-rest 16083  df-topgen 16104  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-top 20699  df-topon 20716  df-bases 20750  df-cmp 21190  df-cncf 22681  df-ovol 23233  df-vol 23234  df-mbf 23388  df-itg1 23389  df-itg2 23390  df-ibl 23391  df-0p 23437

This theorem is referenced by:  ftc1anc  33493