Theorem ftc1anclem8 36871

Description: Lemma for ftc1anc 36872. (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 36870	. 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 771	. . . 4 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
11		3simpa 1146	. . . 4 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤) → (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)))
12		ioossre 13389	. . . . . . . . 9 ⊢ (𝑢(,)𝑤) ⊆ ℝ
13	12	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑢(,)𝑤) ⊆ ℝ)
14		rembl 25289	. . . . . . . . 9 ⊢ ℝ ∈ dom vol
15	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ℝ ∈ dom vol)
16		fvex 6903	. . . . . . . . . 10 ⊢ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ V
17		c0ex 11212	. . . . . . . . . 10 ⊢ 0 ∈ V
18	16, 17	ifex 4577	. . . . . . . . 9 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V
19	18	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
20		eldifn 4126	. . . . . . . . . 10 ⊢ (𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤)) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
21	20	adantl 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤))) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
22	21	iffalsed 4538	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
23		iftrue 4533	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
24	23	mpteq2ia 5250	. . . . . . . . . . 11 ⊢ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
25		resmpt 6036	. . . . . . . . . . . 12 ⊢ ((𝑢(,)𝑤) ⊆ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
26	12, 25	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
27	24, 26	eqtr4i 2761	. . . . . . . . . 10 ⊢ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤))
28		i1ff 25425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
29	28	ffvelcdmda 7085	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
30	29	recnd 11246	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℂ)
31		ax-icn 11171	. . . . . . . . . . . . . . . . 17 ⊢ i ∈ ℂ
32		i1ff 25425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
33	32	ffvelcdmda 7085	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
34	33	recnd 11246	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
35		mulcl 11196	. . . . . . . . . . . . . . . . 17 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ)
36	31, 34, 35	sylancr 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
37		addcl 11194	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
38	30, 36, 37	syl2an 594	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
39	38	anandirs 675	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
40		reex 11203	. . . . . . . . . . . . . . . 16 ⊢ ℝ ∈ V
41	40	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ℝ ∈ V)
42	29	adantlr 711	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
43	36	adantll 710	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
44	28	feqmptd 6959	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ dom ∫1 → 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
45	44	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)))
46	40	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → ℝ ∈ V)
47	31	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → i ∈ ℂ)
48		fconstmpt 5737	. . . . . . . . . . . . . . . . . 18 ⊢ (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i)
49	48	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i))
50	32	feqmptd 6959	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡)))
51	46, 47, 33, 49, 50	offval2 7692	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 ∈ dom ∫1 → ((ℝ × {i}) ∘f · 𝑔) = (𝑡 ∈ ℝ ↦ (i · (𝑔‘𝑡))))
52	51	adantl 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((ℝ × {i}) ∘f · 𝑔) = (𝑡 ∈ ℝ ↦ (i · (𝑔‘𝑡))))
53	41, 42, 43, 45, 52	offval2 7692	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔)) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
54		absf 15288	. . . . . . . . . . . . . . . 16 ⊢ abs:ℂ⟶ℝ
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → abs:ℂ⟶ℝ)
56	55	feqmptd 6959	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
57		fveq2 6890	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) → (abs‘𝑥) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
58	39, 53, 56, 57	fmptco 7128	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) = (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
59		ftc1anclem3 36866	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ∈ dom ∫1)
60	58, 59	eqeltrrd 2832	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ dom ∫1)
61		i1fmbf 25424	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn)
62	60, 61	syl 17	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn)
63		ioombl 25314	. . . . . . . . . . 11 ⊢ (𝑢(,)𝑤) ∈ dom vol
64		mbfres 25393	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn ∧ (𝑢(,)𝑤) ∈ dom vol) → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) ∈ MblFn)
65	62, 63, 64	sylancl 584	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) ∈ MblFn)
66	27, 65	eqeltrid 2835	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
67	66	adantl 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
68	13, 15, 19, 22, 67	mbfss 25395	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
69	68	adantr 479	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
70	39	abscld 15387	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
71	39	absge0d 15395	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
72		elrege0 13435	. . . . . . . . . 10 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ↔ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
73	70, 71, 72	sylanbrc 581	. . . . . . . . 9 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞))
74		0e0icopnf 13439	. . . . . . . . 9 ⊢ 0 ∈ (0[,)+∞)
75		ifcl 4572	. . . . . . . . 9 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
76	73, 74, 75	sylancl 584	. . . . . . . 8 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
77	76	fmpttd 7115	. . . . . . 7 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
78	77	ad2antlr 723	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
79	70	rexrd 11268	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ*)
80		elxrge0 13438	. . . . . . . . . . 11 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ↔ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
81	79, 71, 80	sylanbrc 581	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞))
82		0e0iccpnf 13440	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]+∞)
83		ifcl 4572	. . . . . . . . . 10 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
84	81, 82, 83	sylancl 584	. . . . . . . . 9 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
85	84	fmpttd 7115	. . . . . . . 8 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
86	85	ad2antlr 723	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
87		ifcl 4572	. . . . . . . . . . 11 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
88	81, 82, 87	sylancl 584	. . . . . . . . . 10 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,]+∞))
89	88	fmpttd 7115	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
90		ffn 6716	. . . . . . . . . . . . . . 15 ⊢ (𝑓:ℝ⟶ℝ → 𝑓 Fn ℝ)
91		frn 6723	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:ℝ⟶ℝ → ran 𝑓 ⊆ ℝ)
92		ax-resscn 11169	. . . . . . . . . . . . . . . 16 ⊢ ℝ ⊆ ℂ
93	91, 92	sstrdi 3993	. . . . . . . . . . . . . . 15 ⊢ (𝑓:ℝ⟶ℝ → ran 𝑓 ⊆ ℂ)
94		ffn 6716	. . . . . . . . . . . . . . . . 17 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ)
95	54, 94	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ abs Fn ℂ
96		fnco 6666	. . . . . . . . . . . . . . . 16 ⊢ ((abs Fn ℂ ∧ 𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ) → (abs ∘ 𝑓) Fn ℝ)
97	95, 96	mp3an1 1446	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ) → (abs ∘ 𝑓) Fn ℝ)
98	90, 93, 97	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (𝑓:ℝ⟶ℝ → (abs ∘ 𝑓) Fn ℝ)
99	28, 98	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ 𝑓) Fn ℝ)
100	99	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑓) Fn ℝ)
101		ffn 6716	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℝ⟶ℝ → 𝑔 Fn ℝ)
102		frn 6723	. . . . . . . . . . . . . . . 16 ⊢ (𝑔:ℝ⟶ℝ → ran 𝑔 ⊆ ℝ)
103	102, 92	sstrdi 3993	. . . . . . . . . . . . . . 15 ⊢ (𝑔:ℝ⟶ℝ → ran 𝑔 ⊆ ℂ)
104		fnco 6666	. . . . . . . . . . . . . . . 16 ⊢ ((abs Fn ℂ ∧ 𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ) → (abs ∘ 𝑔) Fn ℝ)
105	95, 104	mp3an1 1446	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ) → (abs ∘ 𝑔) Fn ℝ)
106	101, 103, 105	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (𝑔:ℝ⟶ℝ → (abs ∘ 𝑔) Fn ℝ)
107	32, 106	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (abs ∘ 𝑔) Fn ℝ)
108	107	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑔) Fn ℝ)
109		inidm 4217	. . . . . . . . . . . 12 ⊢ (ℝ ∩ ℝ) = ℝ
110	28	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑓:ℝ⟶ℝ)
111		fvco3 6989	. . . . . . . . . . . . 13 ⊢ ((𝑓:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑓)‘𝑡) = (abs‘(𝑓‘𝑡)))
112	110, 111	sylan 578	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑓)‘𝑡) = (abs‘(𝑓‘𝑡)))
113	32	adantl 480	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 𝑔:ℝ⟶ℝ)
114		fvco3 6989	. . . . . . . . . . . . 13 ⊢ ((𝑔:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑔)‘𝑡) = (abs‘(𝑔‘𝑡)))
115	113, 114	sylan 578	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs ∘ 𝑔)‘𝑡) = (abs‘(𝑔‘𝑡)))
116	100, 108, 41, 41, 109, 112, 115	offval 7681	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ 𝑓) ∘f + (abs ∘ 𝑔)) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
117	30	addridd 11418	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + 0) = (𝑓‘𝑡))
118	117	mpteq2dva 5247	. . . . . . . . . . . . . . . 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 5737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
124	123	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
125	119, 121, 120, 122, 124	offval2 7692	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ((ℝ × {i}) ∘f · (ℝ × {0})) = (𝑡 ∈ ℝ ↦ (i · 0)))
126		it0e0 12438	. . . . . . . . . . . . . . . . . . 19 ⊢ (i · 0) = 0
127	126	mpteq2i 5252	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ ℝ ↦ (i · 0)) = (𝑡 ∈ ℝ ↦ 0)
128	125, 127	eqtrdi 2786	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ dom ∫1 → ((ℝ × {i}) ∘f · (ℝ × {0})) = (𝑡 ∈ ℝ ↦ 0))
129	119, 29, 120, 44, 128	offval2 7692	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ dom ∫1 → (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0}))) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + 0)))
130	118, 129, 44	3eqtr4d 2780	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ dom ∫1 → (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0}))) = 𝑓)
131	130	coeq2d 5861	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0})))) = (abs ∘ 𝑓))
132		i1f0 25436	. . . . . . . . . . . . . . 15 ⊢ (ℝ × {0}) ∈ dom ∫1
133		ftc1anclem3 36866	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ (ℝ × {0}) ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0})))) ∈ dom ∫1)
134	132, 133	mpan2 687	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · (ℝ × {0})))) ∈ dom ∫1)
135	131, 134	eqeltrrd 2832	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ dom ∫1 → (abs ∘ 𝑓) ∈ dom ∫1)
136	135	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑓) ∈ dom ∫1)
137		coeq2 5857	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑔 → (abs ∘ 𝑓) = (abs ∘ 𝑔))
138	137	eleq1d 2816	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑔 → ((abs ∘ 𝑓) ∈ dom ∫1 ↔ (abs ∘ 𝑔) ∈ dom ∫1))
139	138, 135	vtoclga 3565	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ dom ∫1 → (abs ∘ 𝑔) ∈ dom ∫1)
140	139	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ 𝑔) ∈ dom ∫1)
141	136, 140	i1fadd 25444	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ 𝑓) ∘f + (abs ∘ 𝑔)) ∈ dom ∫1)
142	116, 141	eqeltrrd 2832	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1)
143	30	abscld 15387	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓‘𝑡)) ∈ ℝ)
144	30	absge0d 15395	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(𝑓‘𝑡)))
145		elrege0 13435	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘(𝑓‘𝑡)) ∈ (0[,)+∞) ↔ ((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑓‘𝑡))))
146	143, 144, 145	sylanbrc 581	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑓‘𝑡)) ∈ (0[,)+∞))
147	34	abscld 15387	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ ℝ)
148	34	absge0d 15395	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘(𝑔‘𝑡)))
149		elrege0 13435	. . . . . . . . . . . . . . . 16 ⊢ ((abs‘(𝑔‘𝑡)) ∈ (0[,)+∞) ↔ ((abs‘(𝑔‘𝑡)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑔‘𝑡))))
150	147, 148, 149	sylanbrc 581	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ (0[,)+∞))
151		ge0addcl 13441	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑓‘𝑡)) ∈ (0[,)+∞) ∧ (abs‘(𝑔‘𝑡)) ∈ (0[,)+∞)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
152	146, 150, 151	syl2an 594	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
153	152	anandirs 675	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞))
154	153	fmpttd 7115	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞))
155		0plef 25421	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞) ↔ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
156	154, 155	sylib 217	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
157	156	simprd 494	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
158		itg2itg1 25486	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) = (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
159		itg1cl 25434	. . . . . . . . . . . 12 ⊢ ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
160	159	adantr 479	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫1‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
161	158, 160	eqeltrd 2831	. . . . . . . . . 10 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
162	142, 157, 161	syl2anc 582	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ)
163		icossicc 13417	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
164		fss 6733	. . . . . . . . . . 11 ⊢ (((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞))
165	154, 163, 164	sylancl 584	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞))
166		0re 11220	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
167		ifcl 4572	. . . . . . . . . . . . . 14 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
168	70, 166, 167	sylancl 584	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
169		readdcl 11195	. . . . . . . . . . . . . . 15 ⊢ (((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ (abs‘(𝑔‘𝑡)) ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
170	143, 147, 169	syl2an 594	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
171	170	anandirs 675	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ)
172	70	leidd 11784	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
173		breq1 5150	. . . . . . . . . . . . . . 15 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
174		breq1 5150	. . . . . . . . . . . . . . 15 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
175	173, 174	ifboth 4566	. . . . . . . . . . . . . 14 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
176	172, 71, 175	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
177		abstri 15281	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
178	30, 36, 177	syl2an 594	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
179	178	anandirs 675	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))))
180		absmul 15245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (abs‘(i · (𝑔‘𝑡))) = ((abs‘i) · (abs‘(𝑔‘𝑡))))
181	31, 34, 180	sylancr 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = ((abs‘i) · (abs‘(𝑔‘𝑡))))
182		absi 15237	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs‘i) = 1
183	182	oveq1i 7421	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘i) · (abs‘(𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡)))
184	181, 183	eqtrdi 2786	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡))))
185	147	recnd 11246	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ ℂ)
186	185	mullidd 11236	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (1 · (abs‘(𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
187	184, 186	eqtrd 2770	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
188	187	adantll 710	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡)))
189	188	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))) = ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
190	179, 189	breqtrd 5173	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
191	168, 70, 171, 176, 190	letrd 11375	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
192	191	ralrimiva 3144	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ∀𝑡 ∈ ℝ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))
193		eqidd 2731	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
194		eqidd 2731	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
195	41, 168, 171, 193, 194	ofrfval2 7693	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
196	192, 195	mpbird 256	. . . . . . . . . 10 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))
197		itg2le 25489	. . . . . . . . . 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 1369	. . . . . . . . 9 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))))
199		itg2lecl 25488	. . . . . . . . 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 1369	. . . . . . . 8 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
201	200	ad2antlr 723	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
202	89	ad2antlr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞))
203		breq1 5150	. . . . . . . . . . 11 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
204		breq1 5150	. . . . . . . . . . 11 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
205		elioore 13358	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
206	205, 172	sylan2 591	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
207	206	adantll 710	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
208	207	adantlr 711	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
209	2	rexrd 11268	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
210	3	rexrd 11268	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
211	209, 210	jca 510	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
212		df-icc 13335	. . . . . . . . . . . . . . . . . . . . 21 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)})
213	212	elixx3g 13341	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑢 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
214	213	simprbi 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))
215	214	simpld 493	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢)
216	212	elixx3g 13341	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)))
217	216	simprbi 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))
218	217	simprd 494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵)
219	215, 218	anim12i 611	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵))
220		ioossioo 13422	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
221	211, 219, 220	syl2an 594	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
222	5	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
223	221, 222	sstrd 3991	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
224	223	sselda 3981	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
225		iftrue 4533	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
226	224, 225	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
227	226	adantllr 715	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
228	208, 227	breqtrrd 5175	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
229		breq2 5151	. . . . . . . . . . . . 13 ⊢ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
230		breq2 5151	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
231	6	sselda 3981	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ)
232	231	adantlr 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ)
233	71	adantll 710	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
234	232, 233	syldan 589	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
235		0le0 12317	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 0
236	235	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ≤ 0)
237	229, 230, 234, 236	ifbothda 4565	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
238	237	ad2antrr 722	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
239	203, 204, 228, 238	ifbothda 4565	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))
240	239	ralrimivw 3148	. . . . . . . . 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 4577	. . . . . . . . . . . 12 ⊢ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V
244	243	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
245		eqidd 2731	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
246		eqidd 2731	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
247	241, 242, 244, 245, 246	ofrfval2 7693	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
248	247	ad2antrr 722	. . . . . . . . 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 256	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
250		itg2le 25489	. . . . . . . 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 1369	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))))
252		itg2lecl 25488	. . . . . . 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 1369	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
254	8	ffvelcdmda 7085	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
255	254	adantlr 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
256	224, 255	syldan 589	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
257	256	adantllr 715	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
258	205, 39	sylan2 591	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
259	258	adantll 710	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
260	259	adantlr 711	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
261	257, 260	subcld 11575	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
262	261	abscld 15387	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
263	261	absge0d 15395	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
264		elrege0 13435	. . . . . . . . . 10 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,)+∞) ↔ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ ∧ 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
265	262, 263, 264	sylanbrc 581	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,)+∞))
266	74	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,)+∞))
267	265, 266	ifclda 4562	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,)+∞))
268	267	adantr 479	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,)+∞))
269	268	fmpttd 7115	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,)+∞))
270	262	rexrd 11268	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
271		elxrge0 13438	. . . . . . . . . . 11 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
272	270, 263, 271	sylanbrc 581	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞))
273	82	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
274	272, 273	ifclda 4562	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
275	274	adantr 479	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
276	275	fmpttd 7115	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞))
277		recncf 24642	. . . . . . . . . . . . 13 ⊢ ℜ ∈ (ℂ–cn→ℝ)
278		prid1g 4763	. . . . . . . . . . . . 13 ⊢ (ℜ ∈ (ℂ–cn→ℝ) → ℜ ∈ {ℜ, ℑ})
279	277, 278	ax-mp 5	. . . . . . . . . . . 12 ⊢ ℜ ∈ {ℜ, ℑ}
280		ftc1anclem2 36865	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℜ ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
281	279, 280	mp3an3 1448	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
282	8, 7, 281	syl2anc 582	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
283		imcncf 24643	. . . . . . . . . . . . 13 ⊢ ℑ ∈ (ℂ–cn→ℝ)
284		prid2g 4764	. . . . . . . . . . . . 13 ⊢ (ℑ ∈ (ℂ–cn→ℝ) → ℑ ∈ {ℜ, ℑ})
285	283, 284	ax-mp 5	. . . . . . . . . . . 12 ⊢ ℑ ∈ {ℜ, ℑ}
286		ftc1anclem2 36865	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℑ ∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
287	285, 286	mp3an3 1448	. . . . . . . . . . 11 ⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
288	8, 7, 287	syl2anc 582	. . . . . . . . . 10 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
289	282, 288	readdcld 11247	. . . . . . . . 9 ⊢ (𝜑 → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
290	289	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
291	201, 290	readdcld 11247	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) ∈ ℝ)
292		ge0addcl 13441	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞)) → (𝑥 + 𝑦) ∈ (0[,)+∞))
293	292	adantl 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞))
294		ifcl 4572	. . . . . . . . . . . . . . 15 ⊢ (((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ∧ 0 ∈ (0[,)+∞)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
295	73, 74, 294	sylancl 584	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ (0[,)+∞))
296	295	fmpttd 7115	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
297	296	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,)+∞))
298	292	adantl 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞))
299	254	recld 15145	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘(𝐹‘𝑡)) ∈ ℝ)
300	299	recnd 11246	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘(𝐹‘𝑡)) ∈ ℂ)
301	300	abscld 15387	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ)
302	300	absge0d 15395	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(ℜ‘(𝐹‘𝑡))))
303		elrege0 13435	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘(ℜ‘(𝐹‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘(ℜ‘(𝐹‘𝑡)))))
304	301, 302, 303	sylanbrc 581	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ (0[,)+∞))
305	74	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ (0[,)+∞))
306	304, 305	ifclda 4562	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
307	306	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
308	307	fmpttd 7115	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)):ℝ⟶(0[,)+∞))
309	254	imcld 15146	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℑ‘(𝐹‘𝑡)) ∈ ℝ)
310	309	recnd 11246	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℑ‘(𝐹‘𝑡)) ∈ ℂ)
311	310	abscld 15387	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ)
312	310	absge0d 15395	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(ℑ‘(𝐹‘𝑡))))
313		elrege0 13435	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs‘(ℑ‘(𝐹‘𝑡))) ∈ (0[,)+∞) ↔ ((abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ ∧ 0 ≤ (abs‘(ℑ‘(𝐹‘𝑡)))))
314	311, 312, 313	sylanbrc 581	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ (0[,)+∞))
315	314, 305	ifclda 4562	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
316	315	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ (0[,)+∞))
317	316	fmpttd 7115	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)):ℝ⟶(0[,)+∞))
318	298, 308, 317, 241, 241, 109	off 7690	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))):ℝ⟶(0[,)+∞))
319	318	adantr 479	. . . . . . . . . . . 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 7690	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,)+∞))
322		fss 6733	. . . . . . . . . . 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 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞))
324	323	adantr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞))
325		0xr 11265	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ*
326	325	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ ℝ*)
327	270, 326	ifclda 4562	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
328	254	adantlr 711	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
329	39	adantll 710	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
330	232, 329	syldan 589	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
331	328, 330	subcld 11575	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
332	331	abscld 15387	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
333	332	rexrd 11268	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
334	325	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ*)
335	333, 334	ifclda 4562	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
336	335	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ ℝ*)
337	330	abscld 15387	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
338		0red 11221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ)
339	337, 338	ifclda 4562	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ)
340		0red 11221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ)
341	301, 340	ifclda 4562	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ ℝ)
342	311, 340	ifclda 4562	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ ℝ)
343	341, 342	readdcld 11247	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ ℝ)
344	343	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ ℝ)
345	339, 344	readdcld 11247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)
346	345	rexrd 11268	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ*)
347	346	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ*)
348		breq1 5150	. . . . . . . . . . . . 13 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
349		breq1 5150	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
350	224	adantllr 715	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
351	332	leidd 11784	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
352	351	adantlr 711	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
353		iftrue 4533	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
354	353	adantl 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
355	352, 354	breqtrrd 5175	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
356	350, 355	syldan 589	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
357		breq2 5151	. . . . . . . . . . . . . . 15 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
358		breq2 5151	. . . . . . . . . . . . . . 15 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
359	331	absge0d 15395	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
360	357, 358, 359, 236	ifbothda 4565	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
361	360	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
362	348, 349, 356, 361	ifbothda 4565	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
363	254	negcld 11562	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → -(𝐹‘𝑡) ∈ ℂ)
364	363	adantlr 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → -(𝐹‘𝑡) ∈ ℂ)
365	330, 364	addcld 11237	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)) ∈ ℂ)
366	365	abscld 15387	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ∈ ℝ)
367	363	abscld 15387	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ∈ ℝ)
368	367	adantlr 711	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ∈ ℝ)
369	337, 368	readdcld 11247	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))) ∈ ℝ)
370	301, 311	readdcld 11247	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ ℝ)
371	370	adantlr 711	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ ℝ)
372	337, 371	readdcld 11247	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))) ∈ ℝ)
373	330, 364	abstrid 15407	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))))
374		mulcl 11196	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((i ∈ ℂ ∧ (ℑ‘(𝐹‘𝑡)) ∈ ℂ) → (i · (ℑ‘(𝐹‘𝑡))) ∈ ℂ)
375	31, 310, 374	sylancr 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (i · (ℑ‘(𝐹‘𝑡))) ∈ ℂ)
376	300, 375	abstrid 15407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(i · (ℑ‘(𝐹‘𝑡))))))
377	254	absnegd 15400	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) = (abs‘(𝐹‘𝑡)))
378	254	replimd 15148	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) = ((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡)))))
379	378	fveq2d 6894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) = (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))))
380	377, 379	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) = (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))))
381		absmul 15245	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((i ∈ ℂ ∧ (ℑ‘(𝐹‘𝑡)) ∈ ℂ) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))))
382	31, 310, 381	sylancr 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))))
383	182	oveq1i 7421	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))) = (1 · (abs‘(ℑ‘(𝐹‘𝑡))))
384	382, 383	eqtrdi 2786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(i · (ℑ‘(𝐹‘𝑡)))) = (1 · (abs‘(ℑ‘(𝐹‘𝑡)))))
385	311	recnd 11246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℂ)
386	385	mullidd 11236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (1 · (abs‘(ℑ‘(𝐹‘𝑡)))) = (abs‘(ℑ‘(𝐹‘𝑡))))
387	384, 386	eqtr2d 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) = (abs‘(i · (ℑ‘(𝐹‘𝑡)))))
388	387	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) = ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(i · (ℑ‘(𝐹‘𝑡))))))
389	376, 380, 388	3brtr4d 5179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
390	389	adantlr 711	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
391	368, 371, 337, 390	leadd2dd 11833	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
392	366, 369, 372, 373, 391	letrd 11375	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
393	328, 330	abssubd 15404	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡))))
394	353	adantl 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
395	330, 328	negsubd 11581	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)) = (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡)))
396	395	fveq2d 6894	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡))))
397	393, 394, 396	3eqtr4d 2780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))))
398		iftrue 4533	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
399	398	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
400	392, 397, 399	3brtr4d 5179	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
401	400	ex 411	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)))
402	235	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → 0 ≤ 0)
403		iffalse 4536	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0)
404		iffalse 4536	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = 0)
405	402, 403, 404	3brtr4d 5179	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
406	401, 405	pm2.61d1 180	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
407		iftrue 4533	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) = (abs‘(ℜ‘(𝐹‘𝑡))))
408		iftrue 4533	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) = (abs‘(ℑ‘(𝐹‘𝑡))))
409	407, 408	oveq12d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))
410	225, 409	oveq12d 7429	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))))
411	410, 398	eqtr4d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
412		00id 11393	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 0) = 0
413	412	oveq2i 7422	. . . . . . . . . . . . . . . . 17 ⊢ (0 + (0 + 0)) = (0 + 0)
414	413, 412	eqtri 2758	. . . . . . . . . . . . . . . 16 ⊢ (0 + (0 + 0)) = 0
415		iffalse 4536	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
416		iffalse 4536	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) = 0)
417		iffalse 4536	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) = 0)
418	416, 417	oveq12d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (0 + 0))
419	415, 418	oveq12d 7429	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = (0 + (0 + 0)))
420	414, 419, 404	3eqtr4a 2796	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))
421	411, 420	pm2.61i 182	. . . . . . . . . . . . . 14 ⊢ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)
422	406, 421	breqtrrdi 5189	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
423	422	adantr 479	. . . . . . . . . . . 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 13145	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
425	424	ralrimivw 3148	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
426		fvex 6903	. . . . . . . . . . . . . 14 ⊢ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V
427	426, 17	ifex 4577	. . . . . . . . . . . . 13 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V
428	427	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V)
429		ovexd 7446	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ V)
430		eqidd 2731	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
431		ovexd 7446	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ V)
432	341	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ ℝ)
433	342	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ ℝ)
434		eqidd 2731	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))
435		eqidd 2731	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))
436	241, 432, 433, 434, 435	offval2 7692	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))
437	241, 244, 431, 246, 436	offval2 7692	. . . . . . . . . . . 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 7693	. . . . . . . . . . 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 722	. . . . . . . . . 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 256	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘r ≤ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
441		itg2le 25489	. . . . . . . . 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 1369	. . . . . . . 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 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → 𝐷 ⊆ ℝ)
444	243	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V)
445		eldifn 4126	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷)
446	445	iffalsed 4538	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
447	446	adantl 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
448		ovexd 7446	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ V)
449	41, 42, 448, 45, 52	offval2 7692	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔)) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
450	39, 449, 56, 57	fmptco 7128	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) = (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
451	450	reseq1d 5979	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) = ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ 𝐷))
452	6	resmptd 6039	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
453	451, 452	sylan9eqr 2792	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
454	225	mpteq2ia 5250	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
455	453, 454	eqtr4di 2788	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))
456		i1fmbf 25424	. . . . . . . . . . . . . . 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 6727	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐹 = 𝐷)
459		iblmbf 25517	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
460		mbfdm 25375	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
461	7, 459, 460	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐹 ∈ dom vol)
462	458, 461	eqeltrrd 2832	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ dom vol)
463		mbfres 25393	. . . . . . . . . . . . . 14 ⊢ (((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ∈ MblFn ∧ 𝐷 ∈ dom vol) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) ∈ MblFn)
464	457, 462, 463	syl2anr 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((abs ∘ (𝑓 ∘f + ((ℝ × {i}) ∘f · 𝑔))) ↾ 𝐷) ∈ MblFn)
465	455, 464	eqeltrrd 2832	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
466	443, 15, 444, 447, 465	mbfss 25395	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn)
467	200	adantl 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ)
468		0cnd 11211	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
469	300, 468	ifclda 4562	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℂ)
470	469	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℂ)
471		eqidd 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)))
472	54	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → abs:ℂ⟶ℝ)
473	472	feqmptd 6959	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
474		fveq2 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) → (abs‘𝑥) = (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)))
475		fvif 6906	. . . . . . . . . . . . . . . . . 18 ⊢ (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0))
476		abs0 15236	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs‘0) = 0
477		ifeq2 4532	. . . . . . . . . . . . . . . . . . 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 2758	. . . . . . . . . . . . . . . . 17 ⊢ (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)
480	474, 479	eqtrdi 2786	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) → (abs‘𝑥) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))
481	470, 471, 473, 480	fmptco 7128	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))
482	299, 340	ifclda 4562	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
483	482	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
484	483	fmpttd 7115	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)):ℝ⟶ℝ)
485	14	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ℝ ∈ dom vol)
486	482	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ)
487	445	adantl 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷)
488	487	iffalsed 4538	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) = 0)
489		iftrue 4533	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) = (ℜ‘(𝐹‘𝑡)))
490	489	mpteq2ia 5250	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡)))
491	8	feqmptd 6959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
492	7, 459	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 ∈ MblFn)
493	491, 492	eqeltrrd 2832	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn)
494	254	ismbfcn2 25387	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)))
495	493, 494	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))
496	495	simpld 493	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn)
497	490, 496	eqeltrid 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn)
498	6, 485, 486, 488, 497	mbfss 25395	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn)
499		ftc1anclem1 36864	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) ∈ MblFn)
500	484, 498, 499	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) ∈ MblFn)
501	481, 500	eqeltrrd 2832	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∈ MblFn)
502	501, 308, 282, 317, 288	itg2addnc 36845	. . . . . . . . . . . . 13 ⊢ (𝜑 → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
503	502, 289	eqeltrd 2831	. . . . . . . . . . . 12 ⊢ (𝜑 → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
504	503	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ)
505	466, 297, 467, 319, 504	itg2addnc 36845	. . . . . . . . . 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 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))
507	506	oveq2d 7427	. . . . . . . . . 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 2770	. . . . . . . . 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 479	. . . . . . . 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 5173	. . . . . . 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 25488	. . . . . . 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 1369	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ)
513	69, 78, 253, 269, 512	itg2addnc 36845	. . . . 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 7692	. . . . . . . . 9 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
515		eqeq2 2742	. . . . . . . . . . 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 2742	. . . . . . . . . . 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 4533	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
518	23, 517	oveq12d 7429	. . . . . . . . . . . 12 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
519	518	adantl 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
520		iffalse 4536	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0)
521		iffalse 4536	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0)
522	520, 521	oveq12d 7429	. . . . . . . . . . . . 13 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (0 + 0))
523	522, 412	eqtrdi 2786	. . . . . . . . . . . 12 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0)
524	523	adantl 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0)
525	515, 516, 519, 524	ifbothda 4565	. . . . . . . . . 10 ⊢ (𝜑 → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0))
526	525	mpteq2dv 5249	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
527	514, 526	eqtrd 2770	. . . . . . . 8 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
528	527	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)))
529		simplr 765	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
530	258	abscld 15387	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
531	530	recnd 11246	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
532	529, 531	sylan 578	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
533	262	recnd 11246	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℂ)
534	532, 533	addcomd 11420	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
535	534	ifeq1da 4558	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
536	535	mpteq2dv 5249	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
537	528, 536	eqtrd 2770	. . . . . 6 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘f + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
538	537	fveq2d 6894	. . . . 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 2772	. . . 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 594	. . 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 479	. 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 12988	. . . 4 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ)
543	542	2halvesd 12462	. . 3 ⊢ (𝑦 ∈ ℝ+ → ((𝑦 / 2) + (𝑦 / 2)) = 𝑦)
544	543	ad3antlr 727	. 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 5178	1 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < 𝑦)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  Vcvv 3472   ∖ cdif 3944   ∪ cun 3945   ⊆ wss 3947  ifcif 4527  {csn 4627  {cpr 4629   class class class wbr 5147   ↦ cmpt 5230   × cxp 5673  dom cdm 5675  ran crn 5676   ↾ cres 5677   “ cima 5678   ∘ ccom 5679   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542  (class class class)co 7411   ∘_f cof 7670   ∘_r cofr 7671  supcsup 9437  ℂcc 11110  ℝcr 11111  0cc0 11112  1c1 11113  ici 11114   + caddc 11115   · cmul 11117  +∞cpnf 11249  ℝ^*cxr 11251   < clt 11252   ≤ cle 11253   − cmin 11448  -cneg 11449   / cdiv 11875  2c2 12271  ℝ⁺crp 12978  (,)cioo 13328  [,)cico 13330  [,]cicc 13331  ℜcre 15048  ℑcim 15049  abscabs 15185  –cn→ccncf 24616  volcvol 25212  MblFncmbf 25363  ∫₁citg1 25364  ∫₂citg2 25365  𝐿¹cibl 25366  ∫citg 25367  0_𝑝c0p 25418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-disj 5113  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-ofr 7673  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ioo 13332  df-ico 13334  df-icc 13335  df-fz 13489  df-fzo 13632  df-fl 13761  df-seq 13971  df-exp 14032  df-hash 14295  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-clim 15436  df-rlim 15437  df-sum 15637  df-rest 17372  df-topgen 17393  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-top 22616  df-topon 22633  df-bases 22669  df-cmp 23111  df-cncf 24618  df-ovol 25213  df-vol 25214  df-mbf 25368  df-itg1 25369  df-itg2 25370  df-ibl 25371  df-0p 25419

This theorem is referenced by:  ftc1anc  36872