Theorem ftc1anc 36159

Description: ftc1a 25401 holds for functions that obey the triangle inequality in the absence of ax-cc 10371. 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 25400	. 2 ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ)
10		rphalfcl 12942	. . . . . 6 ⊢ (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
11	1, 2, 3, 4, 5, 6, 7, 8	ftc1anclem6 36156	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))
12	10, 11	sylan2 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))
13	12	adantrl 714	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))
14	10	ad2antll 727	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / 2) ∈ ℝ+)
15		2rp 12920	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ+
16		i1ff 25040	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
17	16	frnd 6676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
18	17	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ran 𝑓 ⊆ ℝ)
19		i1ff 25040	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
20	19	frnd 6676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ)
21	20	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ran 𝑔 ⊆ ℝ)
22	18, 21	unssd 4146	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ)
23		ax-resscn 11108	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℂ
24	22, 23	sstrdi 3956	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ)
25		i1f0rn 25046	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓)
26		elun1 4136	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ran 𝑓 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
27	25, 26	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
28	27	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
29		absf 15222	. . . . . . . . . . . . . . . . . . 19 ⊢ abs:ℂ⟶ℝ
30		ffn 6668	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ)
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ abs Fn ℂ
32		fnfvima 7183	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
33	31, 32	mp3an1 1448	. . . . . . . . . . . . . . . . 17 ⊢ (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
34	24, 28, 33	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
35	34	ne0d 4295	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅)
36		imassrn 6024	. . . . . . . . . . . . . . . . 17 ⊢ (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ran abs
37		frn 6675	. . . . . . . . . . . . . . . . . 18 ⊢ (abs:ℂ⟶ℝ → ran abs ⊆ ℝ)
38	29, 37	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ran abs ⊆ ℝ
39	36, 38	sstri 3953	. . . . . . . . . . . . . . . 16 ⊢ (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ
40		ffun 6671	. . . . . . . . . . . . . . . . . 18 ⊢ (abs:ℂ⟶ℝ → Fun abs)
41	29, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ Fun abs
42		i1frn 25041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
43		i1frn 25041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin)
44		unfi 9116	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
45	42, 43, 44	syl2an 596	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
46		imafi 9119	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun abs ∧ (ran 𝑓 ∪ ran 𝑔) ∈ Fin) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
47	41, 45, 46	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
48		fimaxre2 12100	. . . . . . . . . . . . . . . 16 ⊢ (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥)
49	39, 47, 48	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥)
50		suprcl 12115	. . . . . . . . . . . . . . . 16 ⊢ (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
51	39, 50	mp3an1 1448	. . . . . . . . . . . . . . 15 ⊢ (((abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
52	35, 49, 51	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
53	52	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
54		0red 11158	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈ ℝ)
55	24	sselda 3944	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → 𝑟 ∈ ℂ)
56	55	abscld 15321	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ ℝ)
57	56	adantrr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈ ℝ)
58	52	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
59		absgt0 15209	. . . . . . . . . . . . . . . . . . 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 455	. . . . . . . . . . . . . . . 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 1128	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥))
65	64	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥))
66		fnfvima 7183	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
67	31, 66	mp3an1 1448	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
68	24, 67	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
69		suprub 12116	. . . . . . . . . . . . . . . . . 18 ⊢ ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
70	65, 68, 69	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
71	70	adantrr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
72	54, 57, 58, 62, 71	ltletrd 11315	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
73	72	rexlimdvaa 3153	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
74	73	imp 407	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
75	53, 74	elrpd 12954	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+)
76		rpmulcl 12938	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
77	15, 75, 76	sylancr 587	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
78		rpdivcl 12940	. . . . . . . . . . 11 ⊢ (((𝑦 / 2) ∈ ℝ+ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
79	14, 77, 78	syl2an 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
80	79	anassrs 468	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
81	80	adantlr 713	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
82		ancom 461	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) ↔ (𝑦 ∈ ℝ+ ∧ 𝑢 ∈ (𝐴[,]𝐵)))
83	82	anbi2i 623	. . . . . . . . . . 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 644	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ↔ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
85	84	anbi1i 624	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)))
86		an32 644	. . . . . . . . . . . . . 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 274	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
88	87	anbi1i 624	. . . . . . . . . . . 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 644	. . . . . . . . . . . 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 274	. . . . . . . . . . 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 469	. . . . . . . . . . 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 302	. . . . . . . . . 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 7366	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → (𝑏 − 𝑎) = (𝑤 − 𝑢))
94	93	ancoms 459	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (𝑏 − 𝑎) = (𝑤 − 𝑢))
95	94	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑤 − 𝑢)))
96	95	breq1d 5115	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
97		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑤 → (𝐺‘𝑏) = (𝐺‘𝑤))
98		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑢 → (𝐺‘𝑎) = (𝐺‘𝑢))
99	97, 98	oveqan12rd 7377	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((𝐺‘𝑏) − (𝐺‘𝑎)) = ((𝐺‘𝑤) − (𝐺‘𝑢)))
100	99	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) = (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))))
101	100	breq1d 5115	. . . . . . . . . . . . 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 7366	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → (𝑏 − 𝑎) = (𝑢 − 𝑤))
104	103	ancoms 459	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (𝑏 − 𝑎) = (𝑢 − 𝑤))
105	104	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑢 − 𝑤)))
106	105	breq1d 5115	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
107		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑢 → (𝐺‘𝑏) = (𝐺‘𝑢))
108		fveq2 6842	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑤 → (𝐺‘𝑎) = (𝐺‘𝑤))
109	107, 108	oveqan12rd 7377	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((𝐺‘𝑏) − (𝐺‘𝑎)) = ((𝐺‘𝑢) − (𝐺‘𝑤)))
110	109	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
111	110	breq1d 5115	. . . . . . . . . . . . 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 13346	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
114	2, 3, 113	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
115	114	ad4antr 730	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝐴[,]𝐵) ⊆ ℝ)
116		simp-4l 781	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑)
117	114, 23	sstrdi 3956	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
118	117	sselda 3944	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ)
119	117	sselda 3944	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ)
120		abssub 15211	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤)))
121	118, 119, 120	syl2anr 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤)))
122	121	anandis 676	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤)))
123	122	breq1d 5115	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
124	9	ffvelcdmda 7035	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑤) ∈ ℂ)
125	9	ffvelcdmda 7035	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝐺‘𝑢) ∈ ℂ)
126		abssub 15211	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺‘𝑤) ∈ ℂ ∧ (𝐺‘𝑢) ∈ ℂ) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
127	124, 125, 126	syl2anr 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
128	127	anandis 676	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
129	128	breq1d 5115	. . . . . . . . . . . . . 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 580	. . . . . . . . . . . 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 11205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
133	3	rexrd 11205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
134	132, 133	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
135		df-icc 13271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)})
136	135	elixx3g 13277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑢 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
137	136	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))
138	137	simpld 495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢)
139	135	elixx3g 13277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)))
140	139	simprbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))
141	140	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵)
142	138, 141	anim12i 613	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵))
143		ioossioo 13358	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
144	134, 142, 143	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
145	5	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
146	144, 145	sstrd 3954	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
147	146	sselda 3944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
148	8	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
149	148	abscld 15321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ ℝ)
150	149	rexrd 11205	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ ℝ*)
151	148	absge0d 15329	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(𝐹‘𝑡)))
152		elxrge0 13374	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((abs‘(𝐹‘𝑡)) ∈ (0[,]+∞) ↔ ((abs‘(𝐹‘𝑡)) ∈ ℝ* ∧ 0 ≤ (abs‘(𝐹‘𝑡))))
153	150, 151, 152	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞))
154	153	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞))
155	147, 154	syldan 591	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞))
156		0e0iccpnf 13376	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ (0[,]+∞)
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
158	155, 157	ifclda 4521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
159	158	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
160	159	fmpttd 7063	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
161		itg2cl 25097	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
162	160, 161	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
163	162	3adantr3 1171	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
164	116, 163	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
165	164	adantr 481	. . . . . . . . . . . . . . 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 773	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
167	148	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
168	147, 167	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
169	168	adantllr 717	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
170		elioore 13294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
171	16	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
172	171	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℂ)
173		ax-icn 11110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ i ∈ ℂ
174	19	ffvelcdmda 7035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
175	174	recnd 11183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
176		mulcl 11135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ)
177	173, 175, 176	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
178		addcl 11133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
179	172, 177, 178	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
180	179	anandirs 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
181	170, 180	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
182	181	adantll 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
183	182	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
184	169, 183	subcld 11512	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
185	184	abscld 15321	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
186	181	abscld 15321	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
187	186	adantll 712	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
188	187	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
189	185, 188	readdcld 11184	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
190	189	rexrd 11205	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
191	184	absge0d 15329	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
192	180	absge0d 15329	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
193	170, 192	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
194	193	adantll 712	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
195	194	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
196	185, 188, 191, 195	addge0d 11731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
197		elxrge0 13374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔ (((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
198	190, 196, 197	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . 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 4521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
201	200	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
202	201	fmpttd 7063	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞))
203		itg2cl 25097	. . . . . . . . . . . . . . . . . . 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 1171	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ*)
206	166, 205	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ*)
207	206	adantr 481	. . . . . . . . . . . . . . 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 12924	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ*)
209	208	ad3antlr 729	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → 𝑦 ∈ ℝ*)
210	158	adantlr 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
211	210	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
212	211	fmpttd 7063	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
213	169, 183	npcand 11516	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (𝐹‘𝑡))
214	213	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘(𝐹‘𝑡)))
215	184, 183	abstrid 15341	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
216	214, 215	eqbrtrrd 5129	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹‘𝑡)) ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
217		iftrue 4492	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡)))
218	217	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡)))
219		iftrue 4492	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
220	219	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
221	216, 218, 220	3brtr4d 5137	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
222	221	ex 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
223		0le0 12254	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≤ 0
224	223	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0)
225		iffalse 4495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = 0)
226		iffalse 4495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0)
227	224, 225, 226	3brtr4d 5137	. . . . . . . . . . . . . . . . . . . . . 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 3147	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
230		reex 11142	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ∈ V
231	230	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ℝ ∈ V)
232		fvex 6855	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (abs‘(𝐹‘𝑡)) ∈ V
233		c0ex 11149	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ V
234	232, 233	ifex 4536	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ V
235	234	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ V)
236		ovex 7390	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V
237	236, 233	ifex 4536	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V
238	237	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V)
239		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))
240		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
241	231, 235, 238, 239, 240	ofrfval2 7638	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
242	241	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 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 256	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
244		itg2le 25104	. . . . . . . . . . . . . . . . . . 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 1371	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
246	245	3adantr3 1171	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
247	166, 246	sylan 580	. . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . 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 36158	. . . . . . . . . . . . . . 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 13079	. . . . . . . . . . . . . 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 773	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 𝜑)
252		simpr2 1195	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑤 ∈ (𝐴[,]𝐵))
253		oveq2 7365	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑤 → (𝐴(,)𝑥) = (𝐴(,)𝑤))
254		itgeq1 25137	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑤) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
255	253, 254	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
256		itgex 25135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡 ∈ V
257	255, 1, 256	fvmpt 6948	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐺‘𝑤) = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
258	252, 257	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑤) = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
259	2	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝐴 ∈ ℝ)
260	114	sselda 3944	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ)
261	260	3ad2antr2 1189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑤 ∈ ℝ)
262	114	sselda 3944	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ)
263	262	rexrd 11205	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ*)
264	263	3ad2antr1 1188	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ ℝ*)
265		elicc1 13308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
266	132, 133, 265	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
267	266	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))
268	267	simp2d 1143	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑢)
269	268	3ad2antr1 1188	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝐴 ≤ 𝑢)
270		simpr3 1196	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ≤ 𝑤)
271	132	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ*)
272	260	rexrd 11205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ*)
273		elicc1 13308	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤)))
274	271, 272, 273	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤)))
275	274	3ad2antr2 1189	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤)))
276	264, 269, 270, 275	mpbir3and 1342	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ (𝐴[,]𝑤))
277		iooss2 13300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑤 ≤ 𝐵) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
278	133, 141, 277	syl2an 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
279	5	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝐵) ⊆ 𝐷)
280	278, 279	sstrd 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ 𝐷)
281	280	3ad2antr2 1189	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐴(,)𝑤) ⊆ 𝐷)
282	281	sselda 3944	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → 𝑡 ∈ 𝐷)
283	148	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
284	282, 283	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
285		eleq1w 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑢 → (𝑤 ∈ (𝐴[,]𝐵) ↔ 𝑢 ∈ (𝐴[,]𝐵)))
286	285	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑢 → ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵))))
287		oveq2 7365	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑢 → (𝐴(,)𝑤) = (𝐴(,)𝑢))
288	287	mpteq1d 5200	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑢 → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) = (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)))
289	288	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑢 → ((𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔ (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1))
290	286, 289	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑢 → (((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1) ↔ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1)))
291		ioombl 24929	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴(,)𝑤) ∈ dom vol
292	291	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ∈ dom vol)
293	148	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
294	8	feqmptd 6910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
295	294, 7	eqeltrrd 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
296	295	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
297	280, 292, 293, 296	iblss 25169	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
298	290, 297	chvarvv 2002	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
299	298	3ad2antr1 1188	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
300		ioombl 24929	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢(,)𝑤) ∈ dom vol
301	300	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ∈ dom vol)
302		fvexd 6857	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ V)
303	295	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
304	146, 301, 302, 303	iblss 25169	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
305	304	3adantr3 1171	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
306	259, 261, 276, 284, 299, 305	itgsplitioo 25202	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡 = (∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
307	258, 306	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑤) = (∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
308		simpr1 1194	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ (𝐴[,]𝐵))
309		oveq2 7365	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑢 → (𝐴(,)𝑥) = (𝐴(,)𝑢))
310		itgeq1 25137	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑢) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
311	309, 310	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑢 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
312		itgex 25135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ V
313	311, 1, 312	fvmpt 6948	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐺‘𝑢) = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
314	308, 313	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑢) = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
315	307, 314	oveq12d 7375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) = ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡))
316		fvexd 6857	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑢)) → (𝐹‘𝑡) ∈ V)
317	316, 298	itgcl 25148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ ℂ)
318	317	adantrr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ ℂ)
319		fvexd 6857	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ V)
320	319, 304	itgcl 25148	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡 ∈ ℂ)
321	318, 320	pncan2d 11514	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
322	321	3adantr3 1171	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
323	315, 322	eqtrd 2776	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
324	323	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
325		ftc1anc.t	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))))
326		df-ov 7360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢(,)𝑤) = ((,)‘⟨𝑢, 𝑤⟩)
327		opelxpi 5670	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))
328		ioof 13364	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
329		ffn 6668	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
330	328, 329	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (,) Fn (ℝ* × ℝ*)
331		iccssxr 13347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴[,]𝐵) ⊆ ℝ*
332		xpss12 5648	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴[,]𝐵) ⊆ ℝ* ∧ (𝐴[,]𝐵) ⊆ ℝ*) → ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*))
333	331, 331, 332	mp2an 690	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*)
334		fnfvima 7183	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((,) Fn (ℝ* × ℝ*) ∧ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*) ∧ ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
335	330, 333, 334	mp3an12 1451	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
336	327, 335	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
337	326, 336	eqeltrid 2842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
338		itgeq1 25137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑢(,)𝑤) → ∫𝑠(𝐹‘𝑡) d𝑡 = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
339	338	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑢(,)𝑤) → (abs‘∫𝑠(𝐹‘𝑡) d𝑡) = (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
340		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ 𝑠 ↔ 𝑡 ∈ (𝑢(,)𝑤)))
341	340	ifbid 4509	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑢(,)𝑤) → if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))
342	341	mpteq2dv 5207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))
343	342	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑢(,)𝑤) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
344	339, 343	breq12d 5118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑢(,)𝑤) → ((abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))))
345	344	rspccva 3580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) ∧ (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
346	325, 337, 345	syl2an 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
347	346	3adantr3 1171	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
348	324, 347	eqbrtrd 5127	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
349	348	adantlr 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
350		subcl 11400	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺‘𝑤) ∈ ℂ ∧ (𝐺‘𝑢) ∈ ℂ) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
351	124, 125, 350	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
352	351	anandis 676	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
353	352	abscld 15321	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
354	353	rexrd 11205	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
355	354	3adantr3 1171	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
356	355	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
357	163	adantlr 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
358	208	ad2antlr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑦 ∈ ℝ*)
359		xrlelttr 13075	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ* ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
360	356, 357, 358, 359	syl3anc 1371	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
361	349, 360	mpand 693	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
362	251, 361	sylanl1 678	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
363	362	adantr 481	. . . . . . . . . . . . . 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 413	. . . . . . . . . . . 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 11688	. . . . . . . . . . 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 468	. . . . . . . . . 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 581	. . . . . . . . 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 3143	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
370		breq2 5109	. . . . . . . . 9 ⊢ (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → ((abs‘(𝑤 − 𝑢)) < 𝑧 ↔ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
371	370	rspceaimv 3585	. . . . . . . 8 ⊢ ((((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
372	81, 369, 371	syl2anc 584	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
373		ralnex 3075	. . . . . . . . 9 ⊢ (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)
374		nne 2947	. . . . . . . . . 10 ⊢ (¬ 𝑟 ≠ 0 ↔ 𝑟 = 0)
375	374	ralbii 3096	. . . . . . . . 9 ⊢ (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
376	373, 375	bitr3i 276	. . . . . . . 8 ⊢ (¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
377	16	ffnd 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 ∈ dom ∫1 → 𝑓 Fn ℝ)
378		fnfvelrn 7031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ran 𝑓)
379	377, 378	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ran 𝑓)
380		elun1 4136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓‘𝑡) ∈ ran 𝑓 → (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
381	379, 380	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
382		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑟 = (𝑓‘𝑡) → (𝑟 = 0 ↔ (𝑓‘𝑡) = 0))
383	382	rspcva 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0)
384	381, 383	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0)
385	384	adantllr 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0)
386	19	ffnd 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 Fn ℝ)
387		fnfvelrn 7031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ran 𝑔)
388	386, 387	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ran 𝑔)
389		elun2 4137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔‘𝑡) ∈ ran 𝑔 → (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
390	388, 389	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
391		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑟 = (𝑔‘𝑡) → (𝑟 = 0 ↔ (𝑔‘𝑡) = 0))
392	391	rspcva 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑔‘𝑡) = 0)
393	392	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = (i · 0))
394		it0e0 12375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (i · 0) = 0
395	393, 394	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0)
396	390, 395	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0)
397	396	adantlll 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0)
398	385, 397	oveq12d 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = (0 + 0))
399	398	an32s 650	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = (0 + 0))
400		00id 11330	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 + 0) = 0
401	399, 400	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = 0)
402	401	adantlll 716	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = 0)
403	402	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0))
404		0cnd 11148	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
405	148, 404	ifclda 4521	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
406	405	subid1d 11501	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
407	406	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
408	403, 407	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
409	408	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
410		fvif 6858	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0))
411		abs0 15170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (abs‘0) = 0
412		ifeq2 4491	. . . . . . . . . . . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)
415	409, 414	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))
416	415	mpteq2dva 5205	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
417	416	fveq2d 6846	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
418	417	breq1d 5115	. . . . . . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . 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 419	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
423	422	anasss 467	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
424	423	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
425		1rp 12919	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ+
426	425	ne0ii 4297	. . . . . . . . . . . 12 ⊢ ℝ+ ≠ ∅
427	352	anassrs 468	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
428	427	abscld 15321	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
429	428	adantlrr 719	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
430	429	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
431		rpre 12923	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
432	431	rehalfcld 12400	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
433	432	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
434	433	ad3antlr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ)
435	431	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
436	435	ad3antlr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ)
437	430	rexrd 11205	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
438	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ (0[,]+∞))
439	153, 438	ifclda 4521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
440	439	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
441	440	fmpttd 7063	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
442		itg2cl 25097	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
443	441, 442	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
444	443	ad3antrrr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
445	434	rexrd 11205	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ*)
446	108, 107	oveqan12rd 7377	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → ((𝐺‘𝑎) − (𝐺‘𝑏)) = ((𝐺‘𝑤) − (𝐺‘𝑢)))
447	446	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → (abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) = (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))))
448	447	breq1d 5115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))))
449	98, 97	oveqan12rd 7377	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → ((𝐺‘𝑎) − (𝐺‘𝑏)) = ((𝐺‘𝑢) − (𝐺‘𝑤)))
450	449	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → (abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
451	450	breq1d 5115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))))
452	128	breq1d 5115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))))
453	320	abscld 15321	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ∈ ℝ)
454	453	rexrd 11205	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ∈ ℝ*)
455	443	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
456	441	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
457		breq2 5109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((abs‘(𝐹‘𝑡)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
458		breq2 5109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0 ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
459	149	leidd 11721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)))
460		breq1 5108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((abs‘(𝐹‘𝑡)) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) → ((abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))))
461		breq1 5108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) → (0 ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))))
462	460, 461	ifboth 4525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)) ∧ 0 ≤ (abs‘(𝐹‘𝑡))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))
463	459, 151, 462	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))
464	463	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))
465	146	ssneld 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (¬ 𝑡 ∈ 𝐷 → ¬ 𝑡 ∈ (𝑢(,)𝑤)))
466	465	imp 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ 𝐷) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
467	225, 223	eqbrtrdi 5144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0)
468	466, 467	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0)
469	457, 458, 464, 468	ifbothda 4524	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))
470	469	ralrimivw 3147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))
471	232, 233	ifex 4536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ V
472	471	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ V)
473		eqidd 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
474	231, 235, 472, 239, 473	ofrfval2 7638	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
475	474	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
476	470, 475	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
477		itg2le 25104	. . . . . . . . . . . . . . . . . . . . . . . . 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 1371	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
479	454, 162, 455, 346, 478	xrletrd 13081	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
480	479	3adantr3 1171	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
481	324, 480	eqbrtrd 5127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
482	448, 451, 114, 452, 481	wlogle 11688	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
483	482	anassrs 468	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
484	483	adantlrr 719	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
485	484	adantlr 713	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
486		simplr 767	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
487	437, 444, 445, 485, 486	xrlelttrd 13079	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < (𝑦 / 2))
488		rphalflt 12944	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → (𝑦 / 2) < 𝑦)
489	488	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) < 𝑦)
490	489	ad3antlr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) < 𝑦)
491	430, 434, 436, 487, 490	lttrd 11316	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)
492	491	a1d 25	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
493	492	ralrimiva 3143	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
494	493	ralrimivw 3147	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∀𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
495		r19.2z 4452	. . . . . . . . . . . 12 ⊢ ((ℝ+ ≠ ∅ ∧ ∀𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
496	426, 494, 495	sylancr 587	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
497	424, 496	syldan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
498	497	anassrs 468	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
499	498	anassrs 468	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
500	376, 499	sylan2b 594	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
501	372, 500	pm2.61dan 811	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
502	501	ex 413	. . . . 5 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))
503	502	rexlimdvva 3205	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))
504	13, 503	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
505	504	ralrimivva 3197	. 2 ⊢ (𝜑 → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
506		ssid 3966	. . 3 ⊢ ℂ ⊆ ℂ
507		elcncf2 24253	. . 3 ⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))))
508	117, 506, 507	sylancl 586	. 2 ⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))))
509	9, 505, 508	mpbir2and 711	1 ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  Vcvv 3445   ∪ cun 3908   ⊆ wss 3910  ∅c0 4282  ifcif 4486  𝒫 cpw 4560  ⟨cop 4592   class class class wbr 5105   ↦ cmpt 5188   × cxp 5631  dom cdm 5633  ran crn 5634   “ cima 5636  Fun wfun 6490   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496  (class class class)co 7357   ∘_r cofr 7616  Fincfn 8883  supcsup 9376  ℂcc 11049  ℝcr 11050  0cc0 11051  1c1 11052  ici 11053   + caddc 11054   · cmul 11056  +∞cpnf 11186  ℝ^*cxr 11188   < clt 11189   ≤ cle 11190   − cmin 11385   / cdiv 11812  2c2 12208  ℝ⁺crp 12915  (,)cioo 13264  [,]cicc 13267  abscabs 15119  –cn→ccncf 24239  volcvol 24827  ∫₁citg1 24979  ∫₂citg2 24980  𝐿¹cibl 24981  ∫citg 24982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-symdif 4202  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-ofr 7618  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-n0 12414  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-rlim 15371  df-sum 15571  df-rest 17304  df-topgen 17325  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-top 22243  df-topon 22260  df-bases 22296  df-cmp 22738  df-cncf 24241  df-ovol 24828  df-vol 24829  df-mbf 24983  df-itg1 24984  df-itg2 24985  df-ibl 24986  df-itg 24987  df-0p 25034

This theorem is referenced by:  ftc2nc  36160