Theorem ftc1anclem8

Description: Lemma for ftc1anc . (Contributed by Brendan Leahy, 29-May-2018)

	Ref	Expression
Hypotheses	ftc1anc.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
	ftc1anc.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ftc1anc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ftc1anc.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ftc1anc.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
	ftc1anc.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
	ftc1anc.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
	ftc1anc.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
Assertion	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 ) ) ) < 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		ftc1anc.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2		ftc1anc.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3		ftc1anc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		ftc1anc.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5		ftc1anc.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
6		ftc1anc.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
7		ftc1anc.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
8		ftc1anc.f	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
9	1 2 3 4 5 6 7 8	ftc1anclem7	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) ) ∧ ( abs ‘ ( 𝑤 − 𝑢 ) ) < ( ( 𝑦 / 2 ) / ( 2 · sup ( ( abs “ ( ran 𝑓 ∪ ran 𝑔 ) ) , ℝ , < ) ) ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ) < ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) )
10		simplll	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( if ( 𝑡 ∈ 𝐷 , ( 𝐹 ‘ 𝑡 ) , 0 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) ) < ( 𝑦 / 2 ) ) ∧ ∃ 𝑟 ∈ ( ran 𝑓 ∪ ran 𝑔 ) 𝑟 ≠ 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) )
11		3simpa	⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑢 ≤ 𝑤 ) → ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) )
12		ioossre	⊢ ( 𝑢 (,) 𝑤 ) ⊆ ℝ
13	12	a1i	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑢 (,) 𝑤 ) ⊆ ℝ )
14		rembl	⊢ ℝ ∈ dom vol
15	14	a1i	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ℝ ∈ dom vol )
16		fvex	⊢ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ V
17		c0ex	⊢ 0 ∈ V
18	16 17	ifex	⊢ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ V
19	18	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ V )
20		eldifn	⊢ ( 𝑡 ∈ ( ℝ ∖ ( 𝑢 (,) 𝑤 ) ) → ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) )
21	20	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( ℝ ∖ ( 𝑢 (,) 𝑤 ) ) ) → ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) )
22	21	iffalsed	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( ℝ ∖ ( 𝑢 (,) 𝑤 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = 0 )
23		iftrue	⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
24	23	mpteq2ia	⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
25		resmpt	⊢ ( ( 𝑢 (,) 𝑤 ) ⊆ ℝ → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↾ ( 𝑢 (,) 𝑤 ) ) = ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
26	12 25	ax-mp	⊢ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↾ ( 𝑢 (,) 𝑤 ) ) = ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
27	24 26	eqtr4i	⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) = ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↾ ( 𝑢 (,) 𝑤 ) )
28		i1ff	⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 : ℝ ⟶ ℝ )
29	28	ffvelrnda	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℝ )
30	29	recnd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℂ )
31		ax-icn	⊢ i ∈ ℂ
32		i1ff	⊢ ( 𝑔 ∈ dom ∫1 → 𝑔 : ℝ ⟶ ℝ )
33	32	ffvelrnda	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℝ )
34	33	recnd	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 𝑔 ‘ 𝑡 ) ∈ ℂ )
35		mulcl	⊢ ( ( i ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
36	31 34 35	sylancr	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
37		addcl	⊢ ( ( ( 𝑓 ‘ 𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
38	30 36 37	syl2an	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
39	38	anandirs	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
40		reex	⊢ ℝ ∈ V
41	40	a1i	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ℝ ∈ V )
42	29	adantlr	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( 𝑓 ‘ 𝑡 ) ∈ ℝ )
43	36	adantll	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
44	28	feqmptd	⊢ ( 𝑓 ∈ dom ∫1 → 𝑓 = ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) )
45	44	adantr	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 𝑓 = ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) )
46	40	a1i	⊢ ( 𝑔 ∈ dom ∫1 → ℝ ∈ V )
47	31	a1i	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → i ∈ ℂ )
48		fconstmpt	⊢ ( ℝ × { i } ) = ( 𝑡 ∈ ℝ ↦ i )
49	48	a1i	⊢ ( 𝑔 ∈ dom ∫1 → ( ℝ × { i } ) = ( 𝑡 ∈ ℝ ↦ i ) )
50	32	feqmptd	⊢ ( 𝑔 ∈ dom ∫1 → 𝑔 = ( 𝑡 ∈ ℝ ↦ ( 𝑔 ‘ 𝑡 ) ) )
51	46 47 33 49 50	offval2	⊢ ( 𝑔 ∈ dom ∫1 → ( ( ℝ × { i } ) ∘f · 𝑔 ) = ( 𝑡 ∈ ℝ ↦ ( i · ( 𝑔 ‘ 𝑡 ) ) ) )
52	51	adantl	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( ℝ × { i } ) ∘f · 𝑔 ) = ( 𝑡 ∈ ℝ ↦ ( i · ( 𝑔 ‘ 𝑡 ) ) ) )
53	41 42 43 45 52	offval2	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
54		absf	⊢ abs : ℂ ⟶ ℝ
55	54	a1i	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → abs : ℂ ⟶ ℝ )
56	55	feqmptd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → abs = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) ) )
57		fveq2	⊢ ( 𝑥 = ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
58	39 53 56 57	fmptco	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
59		ftc1anclem3	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ∈ dom ∫1 )
60	58 59	eqeltrrd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ dom ∫1 )
61		i1fmbf	⊢ ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ dom ∫1 → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ MblFn )
62	60 61	syl	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ MblFn )
63		ioombl	⊢ ( 𝑢 (,) 𝑤 ) ∈ dom vol
64		mbfres	⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ MblFn ∧ ( 𝑢 (,) 𝑤 ) ∈ dom vol ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↾ ( 𝑢 (,) 𝑤 ) ) ∈ MblFn )
65	62 63 64	sylancl	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↾ ( 𝑢 (,) 𝑤 ) ) ∈ MblFn )
66	27 65	eqeltrid	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ MblFn )
67	66	adantl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ MblFn )
68	13 15 19 22 67	mbfss	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ MblFn )
69	68	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ MblFn )
70	39	abscld	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ )
71	39	absge0d	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
72		elrege0	⊢ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
73	70 71 72	sylanbrc	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,) +∞ ) )
74		0e0icopnf	⊢ 0 ∈ ( 0 [,) +∞ )
75		ifcl	⊢ ( ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,) +∞ ) ∧ 0 ∈ ( 0 [,) +∞ ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
76	73 74 75	sylancl	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
77	76	fmpttd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
78	77	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
79	70	rexrd	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ* )
80		elxrge0	⊢ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
81	79 71 80	sylanbrc	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,] +∞ ) )
82		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
83		ifcl	⊢ ( ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
84	81 82 83	sylancl	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
85	84	fmpttd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
86	85	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
87		ifcl	⊢ ( ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
88	81 82 87	sylancl	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
89	88	fmpttd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
90		ffn	⊢ ( 𝑓 : ℝ ⟶ ℝ → 𝑓 Fn ℝ )
91		frn	⊢ ( 𝑓 : ℝ ⟶ ℝ → ran 𝑓 ⊆ ℝ )
92		ax-resscn	⊢ ℝ ⊆ ℂ
93	91 92	sstrdi	⊢ ( 𝑓 : ℝ ⟶ ℝ → ran 𝑓 ⊆ ℂ )
94		ffn	⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
95	54 94	ax-mp	⊢ abs Fn ℂ
96		fnco	⊢ ( ( abs Fn ℂ ∧ 𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ ) → ( abs ∘ 𝑓 ) Fn ℝ )
97	95 96	mp3an1	⊢ ( ( 𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ ) → ( abs ∘ 𝑓 ) Fn ℝ )
98	90 93 97	syl2anc	⊢ ( 𝑓 : ℝ ⟶ ℝ → ( abs ∘ 𝑓 ) Fn ℝ )
99	28 98	syl	⊢ ( 𝑓 ∈ dom ∫1 → ( abs ∘ 𝑓 ) Fn ℝ )
100	99	adantr	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ∘ 𝑓 ) Fn ℝ )
101		ffn	⊢ ( 𝑔 : ℝ ⟶ ℝ → 𝑔 Fn ℝ )
102		frn	⊢ ( 𝑔 : ℝ ⟶ ℝ → ran 𝑔 ⊆ ℝ )
103	102 92	sstrdi	⊢ ( 𝑔 : ℝ ⟶ ℝ → ran 𝑔 ⊆ ℂ )
104		fnco	⊢ ( ( abs Fn ℂ ∧ 𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ ) → ( abs ∘ 𝑔 ) Fn ℝ )
105	95 104	mp3an1	⊢ ( ( 𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ ) → ( abs ∘ 𝑔 ) Fn ℝ )
106	101 103 105	syl2anc	⊢ ( 𝑔 : ℝ ⟶ ℝ → ( abs ∘ 𝑔 ) Fn ℝ )
107	32 106	syl	⊢ ( 𝑔 ∈ dom ∫1 → ( abs ∘ 𝑔 ) Fn ℝ )
108	107	adantl	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ∘ 𝑔 ) Fn ℝ )
109		inidm	⊢ ( ℝ ∩ ℝ ) = ℝ
110	28	adantr	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 𝑓 : ℝ ⟶ ℝ )
111		fvco3	⊢ ( ( 𝑓 : ℝ ⟶ ℝ ∧ 𝑡 ∈ ℝ ) → ( ( abs ∘ 𝑓 ) ‘ 𝑡 ) = ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) )
112	110 111	sylan	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ∘ 𝑓 ) ‘ 𝑡 ) = ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) )
113	32	adantl	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 𝑔 : ℝ ⟶ ℝ )
114		fvco3	⊢ ( ( 𝑔 : ℝ ⟶ ℝ ∧ 𝑡 ∈ ℝ ) → ( ( abs ∘ 𝑔 ) ‘ 𝑡 ) = ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
115	113 114	sylan	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ∘ 𝑔 ) ‘ 𝑡 ) = ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
116	100 108 41 41 109 112 115	offval	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( abs ∘ 𝑓 ) ∘f + ( abs ∘ 𝑔 ) ) = ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) )
117	30	addid1d	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) + 0 ) = ( 𝑓 ‘ 𝑡 ) )
118	117	mpteq2dva	⊢ ( 𝑓 ∈ dom ∫1 → ( 𝑡 ∈ ℝ ↦ ( ( 𝑓 ‘ 𝑡 ) + 0 ) ) = ( 𝑡 ∈ ℝ ↦ ( 𝑓 ‘ 𝑡 ) ) )
119	40	a1i	⊢ ( 𝑓 ∈ dom ∫1 → ℝ ∈ V )
120	17	a1i	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → 0 ∈ V )
121	31	a1i	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → i ∈ ℂ )
122	48	a1i	⊢ ( 𝑓 ∈ dom ∫1 → ( ℝ × { i } ) = ( 𝑡 ∈ ℝ ↦ i ) )
123		fconstmpt	⊢ ( ℝ × { 0 } ) = ( 𝑡 ∈ ℝ ↦ 0 )
124	123	a1i	⊢ ( 𝑓 ∈ dom ∫1 → ( ℝ × { 0 } ) = ( 𝑡 ∈ ℝ ↦ 0 ) )
125	119 121 120 122 124	offval2	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ℝ × { i } ) ∘f · ( ℝ × { 0 } ) ) = ( 𝑡 ∈ ℝ ↦ ( i · 0 ) ) )
126		it0e0	⊢ ( i · 0 ) = 0
127	126	mpteq2i	⊢ ( 𝑡 ∈ ℝ ↦ ( i · 0 ) ) = ( 𝑡 ∈ ℝ ↦ 0 )
128	125 127	eqtrdi	⊢ ( 𝑓 ∈ dom ∫1 → ( ( ℝ × { i } ) ∘f · ( ℝ × { 0 } ) ) = ( 𝑡 ∈ ℝ ↦ 0 ) )
129	119 29 120 44 128	offval2	⊢ ( 𝑓 ∈ dom ∫1 → ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · ( ℝ × { 0 } ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝑓 ‘ 𝑡 ) + 0 ) ) )
130	118 129 44	3eqtr4d	⊢ ( 𝑓 ∈ dom ∫1 → ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · ( ℝ × { 0 } ) ) ) = 𝑓 )
131	130	coeq2d	⊢ ( 𝑓 ∈ dom ∫1 → ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · ( ℝ × { 0 } ) ) ) ) = ( abs ∘ 𝑓 ) )
132		i1f0	⊢ ( ℝ × { 0 } ) ∈ dom ∫1
133		ftc1anclem3	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ ( ℝ × { 0 } ) ∈ dom ∫1 ) → ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · ( ℝ × { 0 } ) ) ) ) ∈ dom ∫1 )
134	132 133	mpan2	⊢ ( 𝑓 ∈ dom ∫1 → ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · ( ℝ × { 0 } ) ) ) ) ∈ dom ∫1 )
135	131 134	eqeltrrd	⊢ ( 𝑓 ∈ dom ∫1 → ( abs ∘ 𝑓 ) ∈ dom ∫1 )
136	135	adantr	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ∘ 𝑓 ) ∈ dom ∫1 )
137		coeq2	⊢ ( 𝑓 = 𝑔 → ( abs ∘ 𝑓 ) = ( abs ∘ 𝑔 ) )
138	137	eleq1d	⊢ ( 𝑓 = 𝑔 → ( ( abs ∘ 𝑓 ) ∈ dom ∫1 ↔ ( abs ∘ 𝑔 ) ∈ dom ∫1 ) )
139	138 135	vtoclga	⊢ ( 𝑔 ∈ dom ∫1 → ( abs ∘ 𝑔 ) ∈ dom ∫1 )
140	139	adantl	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ∘ 𝑔 ) ∈ dom ∫1 )
141	136 140	i1fadd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( abs ∘ 𝑓 ) ∘f + ( abs ∘ 𝑔 ) ) ∈ dom ∫1 )
142	116 141	eqeltrrd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ dom ∫1 )
143	30	abscld	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ )
144	30	absge0d	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) )
145		elrege0	⊢ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ) )
146	143 144 145	sylanbrc	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ( 0 [,) +∞ ) )
147	34	abscld	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ℝ )
148	34	absge0d	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
149		elrege0	⊢ ( ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
150	147 148 149	sylanbrc	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ( 0 [,) +∞ ) )
151		ge0addcl	⊢ ( ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ( 0 [,) +∞ ) ∧ ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ( 0 [,) +∞ ) ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) )
152	146 150 151	syl2an	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) )
153	152	anandirs	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) )
154	153	fmpttd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
155		0plef	⊢ ( ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) ↔ ( ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
156	154 155	sylib	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
157	156	simprd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) )
158		itg2itg1	⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( ∫1 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
159		itg1cl	⊢ ( ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
160	159	adantr	⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) → ( ∫1 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
161	158 160	eqeltrd	⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
162	142 157 161	syl2anc	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
163		icossicc	⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
164		fss	⊢ ( ( ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
165	154 163 164	sylancl	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
166		0re	⊢ 0 ∈ ℝ
167		ifcl	⊢ ( ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ℝ )
168	70 166 167	sylancl	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ℝ )
169		readdcl	⊢ ( ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ℝ ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℝ )
170	143 147 169	syl2an	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℝ )
171	170	anandirs	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℝ )
172	70	leidd	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
173		breq1	⊢ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) → ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ↔ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
174		breq1	⊢ ( 0 = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) → ( 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ↔ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
175	173 174	ifboth	⊢ ( ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∧ 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
176	172 71 175	syl2anc	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
177		abstri	⊢ ( ( ( 𝑓 ‘ 𝑡 ) ∈ ℂ ∧ ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
178	30 36 177	syl2an	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
179	178	anandirs	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
180		absmul	⊢ ( ( i ∈ ℂ ∧ ( 𝑔 ‘ 𝑡 ) ∈ ℂ ) → ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
181	31 34 180	sylancr	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
182		absi	⊢ ( abs ‘ i ) = 1
183	182	oveq1i	⊢ ( ( abs ‘ i ) · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) = ( 1 · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
184	181 183	eqtrdi	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( 1 · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
185	147	recnd	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ∈ ℂ )
186	185	mulid2d	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( 1 · ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
187	184 186	eqtrd	⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
188	187	adantll	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) = ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) )
189	188	oveq2d	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
190	179 189	breqtrd	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
191	168 70 171 176 190	letrd	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
192	191	ralrimiva	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) )
193		eqidd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
194		eqidd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) = ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) )
195	41 168 171 193 194	ofrfval2	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) )
196	192 195	mpbird	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) )
197		itg2le	⊢ ( ( ( 𝑡 ∈ ℝ ↦ 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	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ ( ( abs ‘ ( 𝑓 ‘ 𝑡 ) ) + ( abs ‘ ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
199		itg2lecl	⊢ ( ( ( 𝑡 ∈ ℝ ↦ 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	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
201	200	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
202	89	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
203		breq1	⊢ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) → ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
204		breq1	⊢ ( 0 = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) → ( 0 ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
205		elioore	⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → 𝑡 ∈ ℝ )
206	205 172	sylan2	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
207	206	adantll	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
208	207	adantlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
209	2	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
210	3	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
211	209 210	jca	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
212		df-icc	⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑡 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦 ) } )
213	212	elixx3g	⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑢 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵 ) ) )
214	213	simprbi	⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵 ) )
215	214	simpld	⊢ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) → 𝐴 ≤ 𝑢 )
216	212	elixx3g	⊢ ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵 ) ) )
217	216	simprbi	⊢ ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵 ) )
218	217	simprd	⊢ ( 𝑤 ∈ ( 𝐴 [,] 𝐵 ) → 𝑤 ≤ 𝐵 )
219	215 218	anim12i	⊢ ( ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵 ) )
220		ioossioo	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵 ) ) → ( 𝑢 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) )
221	211 219 220	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑢 (,) 𝑤 ) ⊆ ( 𝐴 (,) 𝐵 ) )
222	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
223	221 222	sstrd	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑢 (,) 𝑤 ) ⊆ 𝐷 )
224	223	sselda	⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 𝑡 ∈ 𝐷 )
225		iftrue	⊢ ( 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
226	224 225	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
227	226	adantllr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
228	208 227	breqtrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) )
229		breq2	⊢ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) → ( 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ↔ 0 ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
230		breq2	⊢ ( 0 = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
231	6	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → 𝑡 ∈ ℝ )
232	231	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → 𝑡 ∈ ℝ )
233	71	adantll	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
234	232 233	syldan	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → 0 ≤ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
235		0le0	⊢ 0 ≤ 0
236	235	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ≤ 0 )
237	229 230 234 236	ifbothda	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → 0 ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) )
238	237	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) )
239	203 204 228 238	ifbothda	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) )
240	239	ralrimivw	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) )
241	40	a1i	⊢ ( 𝜑 → ℝ ∈ V )
242	18	a1i	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ V )
243	16 17	ifex	⊢ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ V
244	243	a1i	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ V )
245		eqidd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
246		eqidd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
247	241 242 244 245 246	ofrfval2	⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ↔ ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
248	247	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘r ≤ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
250		itg2le	⊢ ( ( ( 𝑡 ∈ ℝ ↦ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) )
252		itg2lecl	⊢ ( ( ( 𝑡 ∈ ℝ ↦ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
254	8	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
255	254	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
256	224 255	syldan	⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
257	256	adantllr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
258	205 39	sylan2	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
259	258	adantll	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
260	259	adantlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
261	257 260	subcld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
262	261	abscld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
263	261	absge0d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
264		elrege0	⊢ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
265	262 263 264	sylanbrc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,) +∞ ) )
266	74	a1i	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ∈ ( 0 [,) +∞ ) )
267	265 266	ifclda	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
268	267	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
269	268	fmpttd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
270	262	rexrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* )
271		elxrge0	⊢ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
272	270 263 271	sylanbrc	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ( 0 [,] +∞ ) )
273	82	a1i	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ∈ ( 0 [,] +∞ ) )
274	272 273	ifclda	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
275	274	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
276	275	fmpttd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
277		recncf	⊢ ℜ ∈ ( ℂ –cn→ ℝ )
278		prid1g	⊢ ( ℜ ∈ ( ℂ –cn→ ℝ ) → ℜ ∈ { ℜ , ℑ } )
279	277 278	ax-mp	⊢ ℜ ∈ { ℜ , ℑ }
280		ftc1anclem2	⊢ ( ( 𝐹 : 𝐷 ⟶ ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℜ ∈ { ℜ , ℑ } ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ ℝ )
281	279 280	mp3an3	⊢ ( ( 𝐹 : 𝐷 ⟶ ℂ ∧ 𝐹 ∈ 𝐿1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ ℝ )
282	8 7 281	syl2anc	⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ ℝ )
283		imcncf	⊢ ℑ ∈ ( ℂ –cn→ ℝ )
284		prid2g	⊢ ( ℑ ∈ ( ℂ –cn→ ℝ ) → ℑ ∈ { ℜ , ℑ } )
285	283 284	ax-mp	⊢ ℑ ∈ { ℜ , ℑ }
286		ftc1anclem2	⊢ ( ( 𝐹 : 𝐷 ⟶ ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℑ ∈ { ℜ , ℑ } ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ ℝ )
287	285 286	mp3an3	⊢ ( ( 𝐹 : 𝐷 ⟶ ℂ ∧ 𝐹 ∈ 𝐿1 ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ ℝ )
288	8 7 287	syl2anc	⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ ℝ )
289	282 288	readdcld	⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) ∈ ℝ )
290	289	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) ∈ ℝ )
291	201 290	readdcld	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) + ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) ) ∈ ℝ )
292		ge0addcl	⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
293	292	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
294		ifcl	⊢ ( ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ( 0 [,) +∞ ) ∧ 0 ∈ ( 0 [,) +∞ ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
295	73 74 294	sylancl	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
296	295	fmpttd	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
297	296	adantl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
298	292	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
299	254	recld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ )
300	299	recnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ )
301	300	abscld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ )
302	300	absge0d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → 0 ≤ ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
303		elrege0	⊢ ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
304	301 302 303	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) )
305	74	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ∈ ( 0 [,) +∞ ) )
306	304 305	ifclda	⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
307	306	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
308	307	fmpttd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
309	254	imcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ )
310	309	recnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ )
311	310	abscld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ )
312	310	absge0d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → 0 ≤ ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
313		elrege0	⊢ ( ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
314	311 312 313	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ( 0 [,) +∞ ) )
315	314 305	ifclda	⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
316	315	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
317	316	fmpttd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
318	298 308 317 241 241 109	off	⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
319	318	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
320	40	a1i	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ℝ ∈ V )
321	293 297 319 320 320 109	off	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘f + ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
322		fss	⊢ ( ( ( ( 𝑡 ∈ ℝ ↦ 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	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘f + ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
324	323	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘f + ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
325		0xr	⊢ 0 ∈ ℝ*
326	325	a1i	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ∈ ℝ* )
327	270 326	ifclda	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ℝ* )
328	254	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
329	39	adantll	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
330	232 329	syldan	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ∈ ℂ )
331	328 330	subcld	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
332	331	abscld	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
333	332	rexrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℝ* )
334	325	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ∈ ℝ* )
335	333 334	ifclda	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ℝ* )
336	335	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ ℝ* )
337	330	abscld	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ )
338		0red	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ∈ ℝ )
339	337 338	ifclda	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ ℝ )
340		0red	⊢ ( ( 𝜑 ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ∈ ℝ )
341	301 340	ifclda	⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ∈ ℝ )
342	311 340	ifclda	⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ∈ ℝ )
343	341 342	readdcld	⊢ ( 𝜑 → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∈ ℝ )
344	343	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∈ ℝ )
345	339 344	readdcld	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ ℝ )
346	345	rexrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ ℝ* )
347	346	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ ℝ* )
348		breq1	⊢ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) )
349		breq1	⊢ ( 0 = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) → ( 0 ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ↔ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) )
350	224	adantllr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 𝑡 ∈ 𝐷 )
351	332	leidd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
352	351	adantlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
353		iftrue	⊢ ( 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
354	353	adantl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
355	352 354	breqtrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) )
356	350 355	syldan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) )
357		breq2	⊢ ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) → ( 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↔ 0 ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) )
358		breq2	⊢ ( 0 = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) )
359	331	absge0d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → 0 ≤ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
360	357 358 359 236	ifbothda	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → 0 ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) )
361	360	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → 0 ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) )
362	348 349 356 361	ifbothda	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) )
363	254	negcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → - ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
364	363	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → - ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
365	330 364	addcld	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) + - ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ )
366	365	abscld	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) + - ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ )
367	363	abscld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ - ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ )
368	367	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ - ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ )
369	337 368	readdcld	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ - ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ )
370	301 311	readdcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ∈ ℝ )
371	370	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ∈ ℝ )
372	337 371	readdcld	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) ∈ ℝ )
373	330 364	abstrid	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) + - ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ - ( 𝐹 ‘ 𝑡 ) ) ) )
374		mulcl	⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ ) → ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℂ )
375	31 310 374	sylancr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℂ )
376	300 375	abstrid	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) + ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) ≤ ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
377	254	absnegd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ - ( 𝐹 ‘ 𝑡 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) )
378	254	replimd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) = ( ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) + ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
379	378	fveq2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) = ( abs ‘ ( ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) + ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
380	377 379	eqtrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ - ( 𝐹 ‘ 𝑡 ) ) = ( abs ‘ ( ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) + ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
381		absmul	⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ ) → ( abs ‘ ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
382	31 310 381	sylancr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
383	182	oveq1i	⊢ ( ( abs ‘ i ) · ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) = ( 1 · ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
384	382 383	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) = ( 1 · ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
385	311	recnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℂ )
386	385	mulid2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 1 · ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) = ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
387	384 386	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) = ( abs ‘ ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
388	387	oveq2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) = ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( i · ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
389	376 380 388	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ - ( 𝐹 ‘ 𝑡 ) ) ≤ ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
390	389	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ - ( 𝐹 ‘ 𝑡 ) ) ≤ ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
391	368 371 337 390	leadd2dd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ - ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
392	366 369 372 373 391	letrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) + - ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
393	328 330	abssubd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) = ( abs ‘ ( ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) − ( 𝐹 ‘ 𝑡 ) ) ) )
394	353	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
395	330 328	negsubd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) + - ( 𝐹 ‘ 𝑡 ) ) = ( ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) − ( 𝐹 ‘ 𝑡 ) ) )
396	395	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( abs ‘ ( ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) + - ( 𝐹 ‘ 𝑡 ) ) ) = ( abs ‘ ( ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) − ( 𝐹 ‘ 𝑡 ) ) ) )
397	393 394 396	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) = ( abs ‘ ( ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) + - ( 𝐹 ‘ 𝑡 ) ) ) )
398		iftrue	⊢ ( 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) , 0 ) = ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
399	398	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ 𝐷 , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) , 0 ) = ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
400	392 397 399	3brtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) , 0 ) )
401	400	ex	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) , 0 ) ) )
402	235	a1i	⊢ ( ¬ 𝑡 ∈ 𝐷 → 0 ≤ 0 )
403		iffalse	⊢ ( ¬ 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) = 0 )
404		iffalse	⊢ ( ¬ 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) , 0 ) = 0 )
405	402 403 404	3brtr4d	⊢ ( ¬ 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) , 0 ) )
406	401 405	pm2.61d1	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ if ( 𝑡 ∈ 𝐷 , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) , 0 ) )
407		iftrue	⊢ ( 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) = ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
408		iftrue	⊢ ( 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) = ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) )
409	407 408	oveq12d	⊢ ( 𝑡 ∈ 𝐷 → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) = ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) )
410	225 409	oveq12d	⊢ ( 𝑡 ∈ 𝐷 → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) = ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) )
411	410 398	eqtr4d	⊢ ( 𝑡 ∈ 𝐷 → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) = if ( 𝑡 ∈ 𝐷 , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) , 0 ) )
412		00id	⊢ ( 0 + 0 ) = 0
413	412	oveq2i	⊢ ( 0 + ( 0 + 0 ) ) = ( 0 + 0 )
414	413 412	eqtri	⊢ ( 0 + ( 0 + 0 ) ) = 0
415		iffalse	⊢ ( ¬ 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = 0 )
416		iffalse	⊢ ( ¬ 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) = 0 )
417		iffalse	⊢ ( ¬ 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) = 0 )
418	416 417	oveq12d	⊢ ( ¬ 𝑡 ∈ 𝐷 → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) = ( 0 + 0 ) )
419	415 418	oveq12d	⊢ ( ¬ 𝑡 ∈ 𝐷 → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) = ( 0 + ( 0 + 0 ) ) )
420	414 419 404	3eqtr4a	⊢ ( ¬ 𝑡 ∈ 𝐷 → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) = if ( 𝑡 ∈ 𝐷 , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) , 0 ) )
421	411 420	pm2.61i	⊢ ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) = if ( 𝑡 ∈ 𝐷 , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) + ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ) ) , 0 )
422	406 421	breqtrrdi	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) )
423	422	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) )
425	424	ralrimivw	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ∀ 𝑡 ∈ ℝ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ≤ ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) )
426		fvex	⊢ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ V
427	426 17	ifex	⊢ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ V
428	427	a1i	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ∈ V )
429		ovexd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ V )
430		eqidd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) )
431		ovexd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∈ V )
432	341	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ∈ ℝ )
433	342	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ∈ ℝ )
434		eqidd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) )
435		eqidd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) )
436	241 432 433 434 435	offval2	⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) + if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) )
437	241 244 431 246 436	offval2	⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ 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	⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ∘r ≤ ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘f + ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) )
441		itg2le	⊢ ( ( ( 𝑡 ∈ ℝ ↦ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → 𝐷 ⊆ ℝ )
444	243	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ∈ V )
445		eldifn	⊢ ( 𝑡 ∈ ( ℝ ∖ 𝐷 ) → ¬ 𝑡 ∈ 𝐷 )
446	445	iffalsed	⊢ ( 𝑡 ∈ ( ℝ ∖ 𝐷 ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = 0 )
447	446	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ 𝑡 ∈ ( ℝ ∖ 𝐷 ) ) → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = 0 )
448		ovexd	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ℝ ) → ( i · ( 𝑔 ‘ 𝑡 ) ) ∈ V )
449	41 42 448 45 52	offval2	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) = ( 𝑡 ∈ ℝ ↦ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
450	39 449 56 57	fmptco	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
451	450	reseq1d	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ↾ 𝐷 ) = ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↾ 𝐷 ) )
452	6	resmptd	⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ↾ 𝐷 ) = ( 𝑡 ∈ 𝐷 ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
453	451 452	sylan9eqr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ↾ 𝐷 ) = ( 𝑡 ∈ 𝐷 ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
454	225	mpteq2ia	⊢ ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) = ( 𝑡 ∈ 𝐷 ↦ ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) )
455	453 454	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ↾ 𝐷 ) = ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) )
456		i1fmbf	⊢ ( ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ∈ dom ∫1 → ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ∈ MblFn )
457	59 456	syl	⊢ ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ∈ MblFn )
458	8	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐷 )
459		iblmbf	⊢ ( 𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn )
460		mbfdm	⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
461	7 459 460	3syl	⊢ ( 𝜑 → dom 𝐹 ∈ dom vol )
462	458 461	eqeltrrd	⊢ ( 𝜑 → 𝐷 ∈ dom vol )
463		mbfres	⊢ ( ( ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ∈ MblFn ∧ 𝐷 ∈ dom vol ) → ( ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ↾ 𝐷 ) ∈ MblFn )
464	457 462 463	syl2anr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ( abs ∘ ( 𝑓 ∘f + ( ( ℝ × { i } ) ∘f · 𝑔 ) ) ) ↾ 𝐷 ) ∈ MblFn )
465	455 464	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ MblFn )
466	443 15 444 447 465	mbfss	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∈ MblFn )
467	200	adantl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) ∈ ℝ )
468		0cnd	⊢ ( ( 𝜑 ∧ ¬ 𝑡 ∈ 𝐷 ) → 0 ∈ ℂ )
469	300 468	ifclda	⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ℂ )
470	469	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ℂ )
471		eqidd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) )
472	54	a1i	⊢ ( 𝜑 → abs : ℂ ⟶ ℝ )
473	472	feqmptd	⊢ ( 𝜑 → abs = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) ) )
474		fveq2	⊢ ( 𝑥 = if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) → ( abs ‘ 𝑥 ) = ( abs ‘ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) )
475		fvif	⊢ ( abs ‘ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , ( abs ‘ 0 ) )
476		abs0	⊢ ( abs ‘ 0 ) = 0
477		ifeq2	⊢ ( ( abs ‘ 0 ) = 0 → if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , ( abs ‘ 0 ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) )
478	476 477	ax-mp	⊢ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , ( abs ‘ 0 ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 )
479	475 478	eqtri	⊢ ( abs ‘ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 )
480	474 479	eqtrdi	⊢ ( 𝑥 = if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) → ( abs ‘ 𝑥 ) = if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) )
481	470 471 473 480	fmptco	⊢ ( 𝜑 → ( abs ∘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) )
482	299 340	ifclda	⊢ ( 𝜑 → if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ℝ )
483	482	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℝ ) → if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ℝ )
484	483	fmpttd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ℝ )
485	14	a1i	⊢ ( 𝜑 → ℝ ∈ dom vol )
486	482	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ∈ ℝ )
487	445	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ℝ ∖ 𝐷 ) ) → ¬ 𝑡 ∈ 𝐷 )
488	487	iffalsed	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ℝ ∖ 𝐷 ) ) → if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) = 0 )
489		iftrue	⊢ ( 𝑡 ∈ 𝐷 → if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) = ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) )
490	489	mpteq2ia	⊢ ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) = ( 𝑡 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) )
491	8	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) )
492	7 459	syl	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
493	491 492	eqeltrrd	⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ MblFn )
494	254	ismbfcn2	⊢ ( 𝜑 → ( ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ MblFn ↔ ( ( 𝑡 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ MblFn ∧ ( 𝑡 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ MblFn ) ) )
495	493 494	mpbid	⊢ ( 𝜑 → ( ( 𝑡 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ MblFn ∧ ( 𝑡 ∈ 𝐷 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ MblFn ) )
496	495	simpld	⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ MblFn )
497	490 496	eqeltrid	⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∈ MblFn )
498	6 485 486 488 497	mbfss	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∈ MblFn )
499		ftc1anclem1	⊢ ( ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) : ℝ ⟶ ℝ ∧ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ∈ MblFn ) → ( abs ∘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ MblFn )
500	484 498 499	syl2anc	⊢ ( 𝜑 → ( abs ∘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) , 0 ) ) ) ∈ MblFn )
501	481 500	eqeltrrd	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∈ MblFn )
502	501 308 282 317 288	itg2addnc	⊢ ( 𝜑 → ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) = ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) )
503	502 289	eqeltrd	⊢ ( 𝜑 → ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) ∈ ℝ )
504	503	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) ∈ ℝ )
505	466 297 467 319 504	itg2addnc	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) → ( ∫2 ‘ ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) = ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) )
507	506	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ≤ ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ) + ( ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℜ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐷 , ( abs ‘ ( ℑ ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ) ) )
511		itg2lecl	⊢ ( ( ( 𝑡 ∈ ℝ ↦ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) ∈ ℝ )
513	69 78 253 269 512	itg2addnc	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) )
515		eqeq2	⊢ ( ( ( 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	⊢ ( 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	⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) = ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
518	23 517	oveq12d	⊢ ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) = ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
519	518	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) = ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) )
520		iffalse	⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) = 0 )
521		iffalse	⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) = 0 )
522	520 521	oveq12d	⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) = ( 0 + 0 ) )
523	522 412	eqtrdi	⊢ ( ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) → ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) = 0 )
524	523	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) = 0 )
525	515 516 519 524	ifbothda	⊢ ( 𝜑 → ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) , 0 ) )
526	525	mpteq2dv	⊢ ( 𝜑 → ( 𝑡 ∈ ℝ ↦ ( if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) + if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) , 0 ) ) )
527	514 526	eqtrd	⊢ ( 𝜑 → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) , 0 ) ) )
528	527	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) , 0 ) ) )
529		simplr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) )
530	258	abscld	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℝ )
531	530	recnd	⊢ ( ( ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
532	529 531	sylan	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ∈ ℂ )
533	262	recnd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ∈ ℂ )
534	532 533	addcomd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) ∧ 𝑡 ∈ ( 𝑢 (,) 𝑤 ) ) → ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) = ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) )
535	534	ifeq1da	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) , 0 ) = if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) )
536	535	mpteq2dv	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) + ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) ) , 0 ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) )
537	528 536	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) ) ∧ ( 𝑢 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑤 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) , 0 ) ) ∘f + ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) ) = ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ ( 𝑢 (,) 𝑤 ) , ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) + ( abs ‘ ( ( 𝑓 ‘ 𝑡 ) + ( i · ( 𝑔 ‘ 𝑡 ) ) ) ) ) , 0 ) ) )
538	537	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℂ )
543	542	2halvesd	⊢ ( 𝑦 ∈ ℝ+ → ( ( 𝑦 / 2 ) + ( 𝑦 / 2 ) ) = 𝑦 )
544	543	ad3antlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ 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 ) ) ) < 𝑦 )