Theorem ftc1anc 37025

Description: ftc1a 25893 holds for functions that obey the triangle inequality in the absence of ax-cc 10425. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.)

Hypotheses

Ref	Expression
ftc1anc.g	⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)
ftc1anc.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
ftc1anc.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
ftc1anc.le	⊢ (𝜑 → 𝐴 ≤ 𝐵)
ftc1anc.s	⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
ftc1anc.d	⊢ (𝜑 → 𝐷 ⊆ ℝ)
ftc1anc.i	⊢ (𝜑 → 𝐹 ∈ 𝐿1)
ftc1anc.f	⊢ (𝜑 → 𝐹:𝐷⟶ℂ)
ftc1anc.t	⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))))

Assertion

Ref	Expression
ftc1anc	⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))

Distinct variable groups:   𝑡,𝑠,𝑥,𝐴   𝐵,𝑠,𝑡,𝑥   𝐷,𝑠,𝑡,𝑥   𝐹,𝑠,𝑡,𝑥   𝜑,𝑠,𝑡,𝑥   𝐺,𝑠

Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1anc

Dummy variables 𝑎 𝑏 𝑓 𝑔 𝑟 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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	ftc1lem2 25892	. 2 ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ)
10		rphalfcl 12997	. . . . . 6 ⊢ (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
11	1, 2, 3, 4, 5, 6, 7, 8	ftc1anclem6 37022	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))
12	10, 11	sylan2 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))
13	12	adantrl 713	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))
14	10	ad2antll 726	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / 2) ∈ ℝ+)
15		2rp 12975	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ+
16		i1ff 25526	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
17	16	frnd 6715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
18	17	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ran 𝑓 ⊆ ℝ)
19		i1ff 25526	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
20	19	frnd 6715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ)
21	20	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ran 𝑔 ⊆ ℝ)
22	18, 21	unssd 4178	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ)
23		ax-resscn 11162	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℂ
24	22, 23	sstrdi 3986	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ)
25		i1f0rn 25532	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓)
26		elun1 4168	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ran 𝑓 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
27	25, 26	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
28	27	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
29		absf 15280	. . . . . . . . . . . . . . . . . . 19 ⊢ abs:ℂ⟶ℝ
30		ffn 6707	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ)
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ abs Fn ℂ
32		fnfvima 7226	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
33	31, 32	mp3an1 1444	. . . . . . . . . . . . . . . . 17 ⊢ (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
34	24, 28, 33	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
35	34	ne0d 4327	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅)
36		imassrn 6060	. . . . . . . . . . . . . . . . 17 ⊢ (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ran abs
37		frn 6714	. . . . . . . . . . . . . . . . . 18 ⊢ (abs:ℂ⟶ℝ → ran abs ⊆ ℝ)
38	29, 37	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ran abs ⊆ ℝ
39	36, 38	sstri 3983	. . . . . . . . . . . . . . . 16 ⊢ (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ
40		ffun 6710	. . . . . . . . . . . . . . . . . 18 ⊢ (abs:ℂ⟶ℝ → Fun abs)
41	29, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ Fun abs
42		i1frn 25527	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
43		i1frn 25527	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin)
44		unfi 9167	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
45	42, 43, 44	syl2an 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
46		imafi 9170	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun abs ∧ (ran 𝑓 ∪ ran 𝑔) ∈ Fin) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
47	41, 45, 46	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
48		fimaxre2 12155	. . . . . . . . . . . . . . . 16 ⊢ (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥)
49	39, 47, 48	sylancr 586	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥)
50		suprcl 12170	. . . . . . . . . . . . . . . 16 ⊢ (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
51	39, 50	mp3an1 1444	. . . . . . . . . . . . . . 15 ⊢ (((abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
52	35, 49, 51	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
53	52	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
54		0red 11213	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈ ℝ)
55	24	sselda 3974	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → 𝑟 ∈ ℂ)
56	55	abscld 15379	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ ℝ)
57	56	adantrr 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈ ℝ)
58	52	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
59		absgt0 15267	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ ℂ → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
60	55, 59	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
61	60	biimpd 228	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 → 0 < (abs‘𝑟)))
62	61	impr 454	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < (abs‘𝑟))
63	39	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ)
64	63, 35, 49	3jca 1125	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥))
65	64	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥))
66		fnfvima 7226	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
67	31, 66	mp3an1 1444	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
68	24, 67	sylan 579	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
69		suprub 12171	. . . . . . . . . . . . . . . . . 18 ⊢ ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
70	65, 68, 69	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
71	70	adantrr 714	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
72	54, 57, 58, 62, 71	ltletrd 11370	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
73	72	rexlimdvaa 3148	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
74	73	imp 406	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
75	53, 74	elrpd 13009	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+)
76		rpmulcl 12993	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
77	15, 75, 76	sylancr 586	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
78		rpdivcl 12995	. . . . . . . . . . 11 ⊢ (((𝑦 / 2) ∈ ℝ+ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
79	14, 77, 78	syl2an 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
80	79	anassrs 467	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
81	80	adantlr 712	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
82		ancom 460	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) ↔ (𝑦 ∈ ℝ+ ∧ 𝑢 ∈ (𝐴[,]𝐵)))
83	82	anbi2i 622	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ↔ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑦 ∈ ℝ+ ∧ 𝑢 ∈ (𝐴[,]𝐵))))
84		an32 643	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ↔ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
85	84	anbi1i 623	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)))
86		an32 643	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
87	85, 86	bitri 275	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
88	87	anbi1i 623	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ↔ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0))
89		an32 643	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ↔ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
90	88, 89	bitri 275	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ↔ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
91		anass 468	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑢 ∈ (𝐴[,]𝐵)) ↔ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑦 ∈ ℝ+ ∧ 𝑢 ∈ (𝐴[,]𝐵))))
92	83, 90, 91	3bitr4i 303	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ↔ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑢 ∈ (𝐴[,]𝐵)))
93		oveq12 7410	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → (𝑏 − 𝑎) = (𝑤 − 𝑢))
94	93	ancoms 458	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (𝑏 − 𝑎) = (𝑤 − 𝑢))
95	94	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑤 − 𝑢)))
96	95	breq1d 5148	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
97		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑤 → (𝐺‘𝑏) = (𝐺‘𝑤))
98		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑢 → (𝐺‘𝑎) = (𝐺‘𝑢))
99	97, 98	oveqan12rd 7421	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((𝐺‘𝑏) − (𝐺‘𝑎)) = ((𝐺‘𝑤) − (𝐺‘𝑢)))
100	99	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) = (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))))
101	100	breq1d 5148	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦 ↔ (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
102	96, 101	imbi12d 344	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦) ↔ ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))
103		oveq12 7410	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → (𝑏 − 𝑎) = (𝑢 − 𝑤))
104	103	ancoms 458	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (𝑏 − 𝑎) = (𝑢 − 𝑤))
105	104	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑢 − 𝑤)))
106	105	breq1d 5148	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
107		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑢 → (𝐺‘𝑏) = (𝐺‘𝑢))
108		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑤 → (𝐺‘𝑎) = (𝐺‘𝑤))
109	107, 108	oveqan12rd 7421	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((𝐺‘𝑏) − (𝐺‘𝑎)) = ((𝐺‘𝑢) − (𝐺‘𝑤)))
110	109	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
111	110	breq1d 5148	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦 ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦))
112	106, 111	imbi12d 344	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦) ↔ ((abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦)))
113		iccssre 13402	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
114	2, 3, 113	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
115	114	ad4antr 729	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝐴[,]𝐵) ⊆ ℝ)
116		simp-4l 780	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑)
117	114, 23	sstrdi 3986	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
118	117	sselda 3974	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ)
119	117	sselda 3974	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ)
120		abssub 15269	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤)))
121	118, 119, 120	syl2anr 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤)))
122	121	anandis 675	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤)))
123	122	breq1d 5148	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
124	9	ffvelcdmda 7076	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑤) ∈ ℂ)
125	9	ffvelcdmda 7076	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑢) ∈ ℂ)
126		abssub 15269	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺‘𝑤) ∈ ℂ ∧ (𝐺‘𝑢) ∈ ℂ) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
127	124, 125, 126	syl2anr 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
128	127	anandis 675	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
129	128	breq1d 5148	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦 ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦))
130	123, 129	imbi12d 344	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) ↔ ((abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦)))
131	116, 130	sylan 579	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) ↔ ((abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦)))
132	2	rexrd 11260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
133	3	rexrd 11260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
134	132, 133	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
135		df-icc 13327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)})
136	135	elixx3g 13333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑢 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
137	136	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))
138	137	simpld 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢)
139	135	elixx3g 13333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)))
140	139	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))
141	140	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵)
142	138, 141	anim12i 612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵))
143		ioossioo 13414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
144	134, 142, 143	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
145	5	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
146	144, 145	sstrd 3984	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
147	146	sselda 3974	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
148	8	ffvelcdmda 7076	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
149	148	abscld 15379	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ ℝ)
150	149	rexrd 11260	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ ℝ*)
151	148	absge0d 15387	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(𝐹‘𝑡)))
152		elxrge0 13430	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((abs‘(𝐹‘𝑡)) ∈ (0[,]+∞) ↔ ((abs‘(𝐹‘𝑡)) ∈ ℝ* ∧ 0 ≤ (abs‘(𝐹‘𝑡))))
153	150, 151, 152	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞))
154	153	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞))
155	147, 154	syldan 590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞))
156		0e0iccpnf 13432	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ (0[,]+∞)
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
158	155, 157	ifclda 4555	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
159	158	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
160	159	fmpttd 7106	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
161		itg2cl 25583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
162	160, 161	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
163	162	3adantr3 1168	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
164	116, 163	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
165	164	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
166		simplll 772	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
167	148	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
168	147, 167	syldan 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
169	168	adantllr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
170		elioore 13350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
171	16	ffvelcdmda 7076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
172	171	recnd 11238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℂ)
173		ax-icn 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ i ∈ ℂ
174	19	ffvelcdmda 7076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
175	174	recnd 11238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
176		mulcl 11189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ)
177	173, 175, 176	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
178		addcl 11187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
179	172, 177, 178	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
180	179	anandirs 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
181	170, 180	sylan2 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
182	181	adantll 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
183	182	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
184	169, 183	subcld 11567	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
185	184	abscld 15379	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
186	181	abscld 15379	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
187	186	adantll 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
188	187	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
189	185, 188	readdcld 11239	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
190	189	rexrd 11260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
191	184	absge0d 15387	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
192	180	absge0d 15387	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
193	170, 192	sylan2 592	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
194	193	adantll 711	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
195	194	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
196	185, 188, 191, 195	addge0d 11786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
197		elxrge0 13430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔ (((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
198	190, 196, 197	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞))
199	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
200	198, 199	ifclda 4555	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
201	200	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
202	201	fmpttd 7106	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞))
203		itg2cl 25583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ*)
204	202, 203	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ*)
205	204	3adantr3 1168	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ*)
206	166, 205	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ*)
207	206	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑓 ∈ 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))) ∈ ℝ*)
208		rpxr 12979	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ*)
209	208	ad3antlr 728	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → 𝑦 ∈ ℝ*)
210	158	adantlr 712	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
211	210	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
212	211	fmpttd 7106	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
213	169, 183	npcand 11571	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (𝐹‘𝑡))
214	213	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘(𝐹‘𝑡)))
215	184, 183	abstrid 15399	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
216	214, 215	eqbrtrrd 5162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹‘𝑡)) ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
217		iftrue 4526	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡)))
218	217	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡)))
219		iftrue 4526	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
220	219	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
221	216, 218, 220	3brtr4d 5170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
222	221	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
223		0le0 12309	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≤ 0
224	223	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0)
225		iffalse 4529	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = 0)
226		iffalse 4529	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0)
227	224, 225, 226	3brtr4d 5170	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
228	222, 227	pm2.61d1 180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
229	228	ralrimivw 3142	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
230		reex 11196	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ∈ V
231	230	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ℝ ∈ V)
232		fvex 6894	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (abs‘(𝐹‘𝑡)) ∈ V
233		c0ex 11204	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ V
234	232, 233	ifex 4570	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ V
235	234	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ V)
236		ovex 7434	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V
237	236, 233	ifex 4570	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V
238	237	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V)
239		eqidd 2725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))
240		eqidd 2725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
241	231, 235, 238, 239, 240	ofrfval2 7684	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
242	241	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
243	229, 242	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
244		itg2le 25590	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
245	212, 202, 243, 244	syl3anc 1368	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
246	245	3adantr3 1168	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
247	166, 246	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
248	247	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
249	1, 2, 3, 4, 5, 6, 7, 8	ftc1anclem8 37024	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑓 ∈ 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))) < 𝑦)
250	165, 207, 209, 248, 249	xrlelttrd 13135	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦)
251		simplll 772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 𝜑)
252		simpr2 1192	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑤 ∈ (𝐴[,]𝐵))
253		oveq2 7409	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑤 → (𝐴(,)𝑥) = (𝐴(,)𝑤))
254		itgeq1 25623	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑤) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
255	253, 254	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
256		itgex 25621	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡 ∈ V
257	255, 1, 256	fvmpt 6988	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐺‘𝑤) = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
258	252, 257	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑤) = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
259	2	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝐴 ∈ ℝ)
260	114	sselda 3974	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ)
261	260	3ad2antr2 1186	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑤 ∈ ℝ)
262	114	sselda 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ)
263	262	rexrd 11260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ*)
264	263	3ad2antr1 1185	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ ℝ*)
265		elicc1 13364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
266	132, 133, 265	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
267	266	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))
268	267	simp2d 1140	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑢)
269	268	3ad2antr1 1185	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝐴 ≤ 𝑢)
270		simpr3 1193	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ≤ 𝑤)
271	132	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ*)
272	260	rexrd 11260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ*)
273		elicc1 13364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤)))
274	271, 272, 273	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤)))
275	274	3ad2antr2 1186	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤)))
276	264, 269, 270, 275	mpbir3and 1339	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ (𝐴[,]𝑤))
277		iooss2 13356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑤 ≤ 𝐵) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
278	133, 141, 277	syl2an 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
279	5	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝐵) ⊆ 𝐷)
280	278, 279	sstrd 3984	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ 𝐷)
281	280	3ad2antr2 1186	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐴(,)𝑤) ⊆ 𝐷)
282	281	sselda 3974	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → 𝑡 ∈ 𝐷)
283	148	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
284	282, 283	syldan 590	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
285		eleq1w 2808	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑢 → (𝑤 ∈ (𝐴[,]𝐵) ↔ 𝑢 ∈ (𝐴[,]𝐵)))
286	285	anbi2d 628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑢 → ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵))))
287		oveq2 7409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑢 → (𝐴(,)𝑤) = (𝐴(,)𝑢))
288	287	mpteq1d 5233	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑢 → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) = (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)))
289	288	eleq1d 2810	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑢 → ((𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔ (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1))
290	286, 289	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑢 → (((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1) ↔ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1)))
291		ioombl 25415	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴(,)𝑤) ∈ dom vol
292	291	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ∈ dom vol)
293	148	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
294	8	feqmptd 6950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
295	294, 7	eqeltrrd 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
296	295	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
297	280, 292, 293, 296	iblss 25655	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
298	290, 297	chvarvv 1994	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
299	298	3ad2antr1 1185	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
300		ioombl 25415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢(,)𝑤) ∈ dom vol
301	300	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ∈ dom vol)
302		fvexd 6896	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ V)
303	295	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
304	146, 301, 302, 303	iblss 25655	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
305	304	3adantr3 1168	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
306	259, 261, 276, 284, 299, 305	itgsplitioo 25688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡 = (∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
307	258, 306	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑤) = (∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
308		simpr1 1191	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ (𝐴[,]𝐵))
309		oveq2 7409	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑢 → (𝐴(,)𝑥) = (𝐴(,)𝑢))
310		itgeq1 25623	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑢) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
311	309, 310	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑢 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
312		itgex 25621	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ V
313	311, 1, 312	fvmpt 6988	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐺‘𝑢) = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
314	308, 313	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑢) = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
315	307, 314	oveq12d 7419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) = ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡))
316		fvexd 6896	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑢)) → (𝐹‘𝑡) ∈ V)
317	316, 298	itgcl 25634	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ ℂ)
318	317	adantrr 714	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ ℂ)
319		fvexd 6896	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ V)
320	319, 304	itgcl 25634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡 ∈ ℂ)
321	318, 320	pncan2d 11569	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
322	321	3adantr3 1168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
323	315, 322	eqtrd 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
324	323	fveq2d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
325		ftc1anc.t	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))))
326		df-ov 7404	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢(,)𝑤) = ((,)‘⟨𝑢, 𝑤⟩)
327		opelxpi 5703	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))
328		ioof 13420	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
329		ffn 6707	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
330	328, 329	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (,) Fn (ℝ* × ℝ*)
331		iccssxr 13403	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴[,]𝐵) ⊆ ℝ*
332		xpss12 5681	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴[,]𝐵) ⊆ ℝ* ∧ (𝐴[,]𝐵) ⊆ ℝ*) → ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*))
333	331, 331, 332	mp2an 689	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*)
334		fnfvima 7226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((,) Fn (ℝ* × ℝ*) ∧ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*) ∧ ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
335	330, 333, 334	mp3an12 1447	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
336	327, 335	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
337	326, 336	eqeltrid 2829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
338		itgeq1 25623	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑢(,)𝑤) → ∫𝑠(𝐹‘𝑡) d𝑡 = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
339	338	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑢(,)𝑤) → (abs‘∫𝑠(𝐹‘𝑡) d𝑡) = (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
340		eleq2 2814	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ 𝑠 ↔ 𝑡 ∈ (𝑢(,)𝑤)))
341	340	ifbid 4543	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑢(,)𝑤) → if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))
342	341	mpteq2dv 5240	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))
343	342	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑢(,)𝑤) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
344	339, 343	breq12d 5151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑢(,)𝑤) → ((abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))))
345	344	rspccva 3603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) ∧ (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
346	325, 337, 345	syl2an 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
347	346	3adantr3 1168	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
348	324, 347	eqbrtrd 5160	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
349	348	adantlr 712	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
350		subcl 11455	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺‘𝑤) ∈ ℂ ∧ (𝐺‘𝑢) ∈ ℂ) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
351	124, 125, 350	syl2anr 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
352	351	anandis 675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
353	352	abscld 15379	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
354	353	rexrd 11260	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
355	354	3adantr3 1168	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
356	355	adantlr 712	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
357	163	adantlr 712	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
358	208	ad2antlr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑦 ∈ ℝ*)
359		xrlelttr 13131	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ* ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
360	356, 357, 358, 359	syl3anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
361	349, 360	mpand 692	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
362	251, 361	sylanl1 677	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
363	362	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
364	250, 363	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)
365	364	ex 412	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
366	102, 112, 115, 131, 365	wlogle 11743	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
367	366	anassrs 467	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
368	92, 367	sylanb 580	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
369	368	ralrimiva 3138	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
370		breq2 5142	. . . . . . . . 9 ⊢ (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → ((abs‘(𝑤 − 𝑢)) < 𝑧 ↔ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
371	370	rspceaimv 3609	. . . . . . . 8 ⊢ ((((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
372	81, 369, 371	syl2anc 583	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
373		ralnex 3064	. . . . . . . . 9 ⊢ (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)
374		nne 2936	. . . . . . . . . 10 ⊢ (¬ 𝑟 ≠ 0 ↔ 𝑟 = 0)
375	374	ralbii 3085	. . . . . . . . 9 ⊢ (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
376	373, 375	bitr3i 277	. . . . . . . 8 ⊢ (¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
377	16	ffnd 6708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 ∈ dom ∫1 → 𝑓 Fn ℝ)
378		fnfvelrn 7072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ran 𝑓)
379	377, 378	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ran 𝑓)
380		elun1 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓‘𝑡) ∈ ran 𝑓 → (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
381	379, 380	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
382		eqeq1 2728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑟 = (𝑓‘𝑡) → (𝑟 = 0 ↔ (𝑓‘𝑡) = 0))
383	382	rspcva 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0)
384	381, 383	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0)
385	384	adantllr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0)
386	19	ffnd 6708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 Fn ℝ)
387		fnfvelrn 7072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ran 𝑔)
388	386, 387	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ran 𝑔)
389		elun2 4169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔‘𝑡) ∈ ran 𝑔 → (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
390	388, 389	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
391		eqeq1 2728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑟 = (𝑔‘𝑡) → (𝑟 = 0 ↔ (𝑔‘𝑡) = 0))
392	391	rspcva 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑔‘𝑡) = 0)
393	392	oveq2d 7417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = (i · 0))
394		it0e0 12430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (i · 0) = 0
395	393, 394	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0)
396	390, 395	sylan 579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0)
397	396	adantlll 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0)
398	385, 397	oveq12d 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = (0 + 0))
399	398	an32s 649	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = (0 + 0))
400		00id 11385	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 + 0) = 0
401	399, 400	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = 0)
402	401	adantlll 715	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = 0)
403	402	oveq2d 7417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0))
404		0cnd 11203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
405	148, 404	ifclda 4555	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
406	405	subid1d 11556	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
407	406	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
408	403, 407	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
409	408	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
410		fvif 6897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0))
411		abs0 15228	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (abs‘0) = 0
412		ifeq2 4525	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((abs‘0) = 0 → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))
413	411, 412	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)
414	410, 413	eqtri 2752	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)
415	409, 414	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))
416	415	mpteq2dva 5238	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
417	416	fveq2d 6885	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
418	417	breq1d 5148	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)))
419	418	biimpd 228	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)))
420	419	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0 → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))))
421	420	com23 86	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))))
422	421	imp32 418	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
423	422	anasss 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
424	423	adantlr 712	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
425		1rp 12974	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ+
426	425	ne0ii 4329	. . . . . . . . . . . 12 ⊢ ℝ+ ≠ ∅
427	352	anassrs 467	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
428	427	abscld 15379	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
429	428	adantlrr 718	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
430	429	adantlr 712	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
431		rpre 12978	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
432	431	rehalfcld 12455	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
433	432	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
434	433	ad3antlr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ)
435	431	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
436	435	ad3antlr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ)
437	430	rexrd 11260	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
438	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ (0[,]+∞))
439	153, 438	ifclda 4555	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
440	439	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
441	440	fmpttd 7106	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
442		itg2cl 25583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
443	441, 442	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
444	443	ad3antrrr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
445	434	rexrd 11260	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ*)
446	108, 107	oveqan12rd 7421	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → ((𝐺‘𝑎) − (𝐺‘𝑏)) = ((𝐺‘𝑤) − (𝐺‘𝑢)))
447	446	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → (abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) = (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))))
448	447	breq1d 5148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))))
449	98, 97	oveqan12rd 7421	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → ((𝐺‘𝑎) − (𝐺‘𝑏)) = ((𝐺‘𝑢) − (𝐺‘𝑤)))
450	449	fveq2d 6885	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → (abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
451	450	breq1d 5148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))))
452	128	breq1d 5148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))))
453	320	abscld 15379	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ∈ ℝ)
454	453	rexrd 11260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ∈ ℝ*)
455	443	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
456	441	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
457		breq2 5142	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((abs‘(𝐹‘𝑡)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
458		breq2 5142	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0 ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
459	149	leidd 11776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)))
460		breq1 5141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((abs‘(𝐹‘𝑡)) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) → ((abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))))
461		breq1 5141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) → (0 ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))))
462	460, 461	ifboth 4559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)) ∧ 0 ≤ (abs‘(𝐹‘𝑡))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))
463	459, 151, 462	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))
464	463	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))
465	146	ssneld 3976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (¬ 𝑡 ∈ 𝐷 → ¬ 𝑡 ∈ (𝑢(,)𝑤)))
466	465	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ 𝐷) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
467	225, 223	eqbrtrdi 5177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0)
468	466, 467	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0)
469	457, 458, 464, 468	ifbothda 4558	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))
470	469	ralrimivw 3142	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))
471	232, 233	ifex 4570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ V
472	471	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ V)
473		eqidd 2725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
474	231, 235, 472, 239, 473	ofrfval2 7684	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
475	474	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
476	470, 475	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
477		itg2le 25590	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
478	160, 456, 476, 477	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
479	454, 162, 455, 346, 478	xrletrd 13137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
480	479	3adantr3 1168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
481	324, 480	eqbrtrd 5160	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
482	448, 451, 114, 452, 481	wlogle 11743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
483	482	anassrs 467	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
484	483	adantlrr 718	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
485	484	adantlr 712	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
486		simplr 766	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
487	437, 444, 445, 485, 486	xrlelttrd 13135	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < (𝑦 / 2))
488		rphalflt 12999	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → (𝑦 / 2) < 𝑦)
489	488	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) < 𝑦)
490	489	ad3antlr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) < 𝑦)
491	430, 434, 436, 487, 490	lttrd 11371	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)
492	491	a1d 25	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
493	492	ralrimiva 3138	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
494	493	ralrimivw 3142	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∀𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
495		r19.2z 4486	. . . . . . . . . . . 12 ⊢ ((ℝ+ ≠ ∅ ∧ ∀𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
496	426, 494, 495	sylancr 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
497	424, 496	syldan 590	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
498	497	anassrs 467	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
499	498	anassrs 467	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
500	376, 499	sylan2b 593	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
501	372, 500	pm2.61dan 810	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
502	501	ex 412	. . . . 5 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))
503	502	rexlimdvva 3203	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))
504	13, 503	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
505	504	ralrimivva 3192	. 2 ⊢ (𝜑 → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
506		ssid 3996	. . 3 ⊢ ℂ ⊆ ℂ
507		elcncf2 24731	. . 3 ⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))))
508	117, 506, 507	sylancl 585	. 2 ⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))))
509	9, 505, 508	mpbir2and 710	1 ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   ≠ wne 2932  ∀wral 3053  ∃wrex 3062  Vcvv 3466   ∪ cun 3938   ⊆ wss 3940  ∅c0 4314  ifcif 4520  𝒫 cpw 4594  ⟨cop 4626   class class class wbr 5138   ↦ cmpt 5221   × cxp 5664  dom cdm 5666  ran crn 5667   “ cima 5669  Fun wfun 6527   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  (class class class)co 7401   ∘_r cofr 7662  Fincfn 8934  supcsup 9430  ℂcc 11103  ℝcr 11104  0cc0 11105  1c1 11106  ici 11107   + caddc 11108   · cmul 11110  +∞cpnf 11241  ℝ^*cxr 11243   < clt 11244   ≤ cle 11245   − cmin 11440   / cdiv 11867  2c2 12263  ℝ⁺crp 12970  (,)cioo 13320  [,]cicc 13323  abscabs 15177  –cn→ccncf 24717  volcvol 25313  ∫₁citg1 25465  ∫₂citg2 25466  𝐿¹cibl 25467  ∫citg 25468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9631  ax-cnex 11161  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182  ax-pre-sup 11183  ax-addf 11184

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-symdif 4234  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-disj 5104  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-ofr 7664  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8698  df-map 8817  df-pm 8818  df-en 8935  df-dom 8936  df-sdom 8937  df-fin 8938  df-fi 9401  df-sup 9432  df-inf 9433  df-oi 9500  df-dju 9891  df-card 9929  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-n0 12469  df-z 12555  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-rlim 15429  df-sum 15629  df-rest 17366  df-topgen 17387  df-psmet 21219  df-xmet 21220  df-met 21221  df-bl 21222  df-mopn 21223  df-top 22717  df-topon 22734  df-bases 22770  df-cmp 23212  df-cncf 24719  df-ovol 25314  df-vol 25315  df-mbf 25469  df-itg1 25470  df-itg2 25471  df-ibl 25472  df-itg 25473  df-0p 25520

This theorem is referenced by:  ftc2nc  37026