Theorem ftc1anc 38587

Description: ftc1a 26337 holds for functions that obey the triangle inequality in the absence of ax-cc 10494. 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 26336	. 2 ⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ)
10		rphalfcl 13130	. . . . . 6 ⊢ (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ+)
11	1, 2, 3, 4, 5, 6, 7, 8	ftc1anclem6 38584	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 / 2) ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))
12	10, 11	sylan2 605	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))
13	12	adantrl 729	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2))
14	10	ad2antll 742	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / 2) ∈ ℝ+)
15		2rp 13106	. . . . . . . . . . . 12 ⊢ 2 ∈ ℝ+
16		i1ff 25977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ dom ∫1 → 𝑓:ℝ⟶ℝ)
17	16	frnd 6710	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ⊆ ℝ)
18	17	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ran 𝑓 ⊆ ℝ)
19		i1ff 25977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ∈ dom ∫1 → 𝑔:ℝ⟶ℝ)
20	19	frnd 6710	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ∈ dom ∫1 → ran 𝑔 ⊆ ℝ)
21	20	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ran 𝑔 ⊆ ℝ)
22	18, 21	unssd 4138	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ)
23		ax-resscn 11238	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℂ
24	22, 23	sstrdi 3943	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ)
25		i1f0rn 25983	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ dom ∫1 → 0 ∈ ran 𝑓)
26		elun1 4128	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 ∈ ran 𝑓 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
27	25, 26	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
28	27	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔))
29		absf 15485	. . . . . . . . . . . . . . . . . . 19 ⊢ abs:ℂ⟶ℝ
30		ffn 6701	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ)
31	29, 30	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ abs Fn ℂ
32		fnfvima 7231	. . . . . . . . . . . . . . . . . 18 ⊢ ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
33	31, 32	mp3an1 1477	. . . . . . . . . . . . . . . . 17 ⊢ (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
34	24, 28, 33	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
35	34	ne0d 4288	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅)
36		imassrn 6065	. . . . . . . . . . . . . . . . 17 ⊢ (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ran abs
37		frn 6709	. . . . . . . . . . . . . . . . . 18 ⊢ (abs:ℂ⟶ℝ → ran abs ⊆ ℝ)
38	29, 37	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ran abs ⊆ ℝ
39	36, 38	sstri 3940	. . . . . . . . . . . . . . . 16 ⊢ (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ
40		ffun 6704	. . . . . . . . . . . . . . . . . 18 ⊢ (abs:ℂ⟶ℝ → Fun abs)
41	29, 40	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ Fun abs
42		i1frn 25978	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ dom ∫1 → ran 𝑓 ∈ Fin)
43		i1frn 25978	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ dom ∫1 → ran 𝑔 ∈ Fin)
44		unfi 9170	. . . . . . . . . . . . . . . . . 18 ⊢ ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
45	42, 43, 44	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin)
46		imafi 9291	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun abs ∧ (ran 𝑓 ∪ ran 𝑔) ∈ Fin) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
47	41, 45, 46	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin)
48		fimaxre2 12243	. . . . . . . . . . . . . . . 16 ⊢ (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥)
49	39, 47, 48	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥)
50		suprcl 12258	. . . . . . . . . . . . . . . 16 ⊢ (((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
51	39, 50	mp3an1 1477	. . . . . . . . . . . . . . 15 ⊢ (((abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
52	35, 49, 51	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
53	52	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
54		0red 11292	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈ ℝ)
55	24	sselda 3931	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → 𝑟 ∈ ℂ)
56	55	abscld 15586	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ ℝ)
57	56	adantrr 730	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈ ℝ)
58	52	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ)
59		absgt0 15472	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 ∈ ℂ → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
60	55, 59	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 ↔ 0 < (abs‘𝑟)))
61	60	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (𝑟 ≠ 0 → 0 < (abs‘𝑟)))
62	61	impr 460	. . . . . . . . . . . . . . . 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 1146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥))
65	64	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥))
66		fnfvima 7231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((abs Fn ℂ ∧ (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
67	31, 66	mp3an1 1477	. . . . . . . . . . . . . . . . . . 19 ⊢ (((ran 𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
68	24, 67	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)))
69		suprub 12259	. . . . . . . . . . . . . . . . . 18 ⊢ ((((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
70	65, 68, 69	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
71	70	adantrr 730	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
72	54, 57, 58, 62, 71	ltletrd 11451	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
73	72	rexlimdvaa 3165	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))
74	73	imp 412	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 0 < sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))
75	53, 74	elrpd 13142	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+)
76		rpmulcl 13126	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
77	15, 75, 76	sylancr 599	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+)
78		rpdivcl 13128	. . . . . . . . . . 11 ⊢ (((𝑦 / 2) ∈ ℝ+ ∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
79	14, 77, 78	syl2an 608	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
80	79	anassrs 473	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
81	80	adantlr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
82		ancom 466	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) ↔ (𝑦 ∈ ℝ+ ∧ 𝑢 ∈ (𝐴[,]𝐵)))
83	82	anbi2i 635	. . . . . . . . . . 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 659	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ↔ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
85	84	anbi1i 636	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)))
86		an32 659	. . . . . . . . . . . . . 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 278	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ↔ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)))
88	87	anbi1i 636	. . . . . . . . . . . 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 659	. . . . . . . . . . . 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 278	. . . . . . . . . . 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 474	. . . . . . . . . . 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 306	. . . . . . . . . 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 7421	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → (𝑏 − 𝑎) = (𝑤 − 𝑢))
94	93	ancoms 464	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (𝑏 − 𝑎) = (𝑤 − 𝑢))
95	94	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑤 − 𝑢)))
96	95	breq1d 5113	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
97		fveq2 6877	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑤 → (𝐺‘𝑏) = (𝐺‘𝑤))
98		fveq2 6877	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑢 → (𝐺‘𝑎) = (𝐺‘𝑢))
99	97, 98	oveqan12rd 7432	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((𝐺‘𝑏) − (𝐺‘𝑎)) = ((𝐺‘𝑤) − (𝐺‘𝑢)))
100	99	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) = (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))))
101	100	breq1d 5113	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → ((abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦 ↔ (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
102	96, 101	imbi12d 347	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑤) → (((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦) ↔ ((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))
103		oveq12 7421	. . . . . . . . . . . . . . . 16 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → (𝑏 − 𝑎) = (𝑢 − 𝑤))
104	103	ancoms 464	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (𝑏 − 𝑎) = (𝑢 − 𝑤))
105	104	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (abs‘(𝑏 − 𝑎)) = (abs‘(𝑢 − 𝑤)))
106	105	breq1d 5113	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ↔ (abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
107		fveq2 6877	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑢 → (𝐺‘𝑏) = (𝐺‘𝑢))
108		fveq2 6877	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑤 → (𝐺‘𝑎) = (𝐺‘𝑤))
109	107, 108	oveqan12rd 7432	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((𝐺‘𝑏) − (𝐺‘𝑎)) = ((𝐺‘𝑢) − (𝐺‘𝑤)))
110	109	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
111	110	breq1d 5113	. . . . . . . . . . . . 13 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → ((abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦 ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦))
112	106, 111	imbi12d 347	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑤 ∧ 𝑏 = 𝑢) → (((abs‘(𝑏 − 𝑎)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑏) − (𝐺‘𝑎))) < 𝑦) ↔ ((abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦)))
113		iccssre 13541	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
114	2, 3, 113	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
115	114	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝐴[,]𝐵) ⊆ ℝ)
116		simp-4l 795	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑)
117	114, 23	sstrdi 3943	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ)
118	117	sselda 3931	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ)
119	117	sselda 3931	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ)
120		abssub 15474	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤)))
121	118, 119, 120	syl2anr 609	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤)))
122	121	anandis 691	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) = (abs‘(𝑢 − 𝑤)))
123	122	breq1d 5113	. . . . . . . . . . . . . 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 15474	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺‘𝑤) ∈ ℂ ∧ (𝐺‘𝑢) ∈ ℂ) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
127	124, 125, 126	syl2anr 609	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
128	127	anandis 691	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
129	128	breq1d 5113	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦 ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦))
130	123, 129	imbi12d 347	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦) ↔ ((abs‘(𝑢 − 𝑤)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) < 𝑦)))
131	116, 130	sylan 592	. . . . . . . . . . . 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 11340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
133	3	rexrd 11340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
134	132, 133	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*))
135		df-icc 13464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ [,] = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)})
136	135	elixx3g 13470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑢 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
137	136	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))
138	137	simpld 500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢)
139	135	elixx3g 13470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)))
140	139	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))
141	140	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵)
142	138, 141	anim12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵))
143		ioossioo 13553	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
144	134, 142, 143	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵))
145	5	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷)
146	144, 145	sstrd 3941	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷)
147	146	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷)
148	8	ffvelcdmda 7076	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
149	148	abscld 15586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ ℝ)
150	149	rexrd 11340	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ ℝ*)
151	148	absge0d 15594	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘(𝐹‘𝑡)))
152		elxrge0 13569	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((abs‘(𝐹‘𝑡)) ∈ (0[,]+∞) ↔ ((abs‘(𝐹‘𝑡)) ∈ ℝ* ∧ 0 ≤ (abs‘(𝐹‘𝑡))))
153	150, 151, 152	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞))
154	153	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞))
155	147, 154	syldan 603	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(𝐹‘𝑡)) ∈ (0[,]+∞))
156		0e0iccpnf 13571	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ (0[,]+∞)
157	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈ (0[,]+∞))
158	155, 157	ifclda 4518	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
159	158	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
160	159	fmpttd 7107	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
161		itg2cl 26033	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
162	160, 161	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
163	162	3adantr3 1190	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
164	116, 163	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
165	164	adantr 486	. . . . . . . . . . . . . . 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 787	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
167	148	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
168	147, 167	syldan 603	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
169	168	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
170		elioore 13487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ)
171	16	ffvelcdmda 7076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℝ)
172	171	recnd 11318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ℂ)
173		ax-icn 11240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ i ∈ ℂ
174	19	ffvelcdmda 7076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℝ)
175	174	recnd 11318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ℂ)
176		mulcl 11265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((i ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ)
177	173, 175, 176	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ)
178		addcl 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
179	172, 177, 178	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
180	179	anandirs 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
181	170, 180	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
182	181	adantll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
183	182	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)
184	169, 183	subcld 11650	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ)
185	184	abscld 15586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
186	181	abscld 15586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
187	186	adantll 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
188	187	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ)
189	185, 188	readdcld 11319	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ)
190	189	rexrd 11340	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ*)
191	184	absge0d 15594	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
192	180	absge0d 15594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
193	170, 192	sylan2 605	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
194	193	adantll 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
195	194	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))
196	185, 188, 191, 195	addge0d 11873	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
197		elxrge0 13569	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔ (((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))
198	190, 196, 197	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . 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 4518	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
201	200	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ (0[,]+∞))
202	201	fmpttd 7107	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞))
203		itg2cl 26033	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ*)
204	202, 203	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ*)
205	204	3adantr3 1190	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ*)
206	166, 205	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ*)
207	206	adantr 486	. . . . . . . . . . . . . . 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 13111	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ*)
209	208	ad3antlr 744	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))) → 𝑦 ∈ ℝ*)
210	158	adantlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
211	210	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
212	211	fmpttd 7107	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
213	169, 183	npcand 11654	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (𝐹‘𝑡))
214	213	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘(((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘(𝐹‘𝑡)))
215	184, 183	abstrid 15606	. . . . . . . . . . . . . . . . . . . . . . . . 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 4488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡)))
218	217	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡)))
219		iftrue 4488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))
220	219	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 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 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
223		0le0 12425	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ≤ 0
224	223	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0)
225		iffalse 4491	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) = 0)
226		iffalse 4491	. . . . . . . . . . . . . . . . . . . . . . 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 182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
229	228	ralrimivw 3159	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))
230		reex 11272	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ℝ ∈ V
231	230	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ℝ ∈ V)
232		fvex 6890	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (abs‘(𝐹‘𝑡)) ∈ V
233		c0ex 11281	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ V
234	232, 233	ifex 4533	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ V
235	234	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ∈ V)
236		ovex 7445	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V
237	236, 233	ifex 4533	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V
238	237	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V)
239		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))
240		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
241	231, 235, 238, 239, 240	ofrfval2 7703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
242	241	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 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 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))
244		itg2le 26040	. . . . . . . . . . . . . . . . . . 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 1398	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
246	245	3adantr3 1190	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))
247	166, 246	sylan 592	. . . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . . . 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 38586	. . . . . . . . . . . . . . 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 13270	. . . . . . . . . . . . . 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 787	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → 𝜑)
252		simpr2 1214	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑤 ∈ (𝐴[,]𝐵))
253		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑤 → (𝐴(,)𝑥) = (𝐴(,)𝑤))
254		itgeq1 26073	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑤) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
255	253, 254	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑤 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
256		itgex 26071	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡 ∈ V
257	255, 1, 256	fvmpt 6985	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐺‘𝑤) = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
258	252, 257	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑤) = ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡)
259	2	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝐴 ∈ ℝ)
260	114	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ)
261	260	3ad2antr2 1208	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑤 ∈ ℝ)
262	114	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ)
263	262	rexrd 11340	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℝ*)
264	263	3ad2antr1 1207	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ ℝ*)
265		elicc1 13501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
266	132, 133, 265	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)))
267	266	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))
268	267	simp2d 1161	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑢)
269	268	3ad2antr1 1207	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝐴 ≤ 𝑢)
270		simpr3 1215	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ≤ 𝑤)
271	132	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ*)
272	260	rexrd 11340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℝ*)
273		elicc1 13501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤)))
274	271, 272, 273	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤)))
275	274	3ad2antr2 1208	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑢 ∈ (𝐴[,]𝑤) ↔ (𝑢 ∈ ℝ* ∧ 𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝑤)))
276	264, 269, 270, 275	mpbir3and 1361	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ (𝐴[,]𝑤))
277		iooss2 13493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑤 ≤ 𝐵) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
278	133, 141, 277	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ (𝐴(,)𝐵))
279	5	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝐵) ⊆ 𝐷)
280	278, 279	sstrd 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ⊆ 𝐷)
281	280	3ad2antr2 1208	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐴(,)𝑤) ⊆ 𝐷)
282	281	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → 𝑡 ∈ 𝐷)
283	148	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
284	282, 283	syldan 603	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝐴(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ)
285		eleq1w 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑢 → (𝑤 ∈ (𝐴[,]𝐵) ↔ 𝑢 ∈ (𝐴[,]𝐵)))
286	285	anbi2d 642	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑢 → ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵))))
287		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑤 = 𝑢 → (𝐴(,)𝑤) = (𝐴(,)𝑢))
288	287	mpteq1d 5195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑤 = 𝑢 → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) = (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)))
289	288	eleq1d 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑤 = 𝑢 → ((𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔ (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1))
290	286, 289	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 = 𝑢 → (((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1) ↔ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1)))
291		ioombl 25866	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴(,)𝑤) ∈ dom vol
292	291	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑤) ∈ dom vol)
293	148	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ)
294	8	feqmptd 6945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)))
295	294, 7	eqeltrrd 2862	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
296	295	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
297	280, 292, 293, 296	iblss 26105	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
298	290, 297	chvarvv 2022	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
299	298	3ad2antr1 1207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ (𝐴(,)𝑢) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
300		ioombl 25866	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢(,)𝑤) ∈ dom vol
301	300	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ∈ dom vol)
302		fvexd 6892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ V)
303	295	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1)
304	146, 301, 302, 303	iblss 26105	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
305	304	3adantr3 1190	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ (𝑢(,)𝑤) ↦ (𝐹‘𝑡)) ∈ 𝐿1)
306	259, 261, 276, 284, 299, 305	itgsplitioo 26138	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ∫(𝐴(,)𝑤)(𝐹‘𝑡) d𝑡 = (∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
307	258, 306	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑤) = (∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
308		simpr1 1213	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑢 ∈ (𝐴[,]𝐵))
309		oveq2 7420	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 = 𝑢 → (𝐴(,)𝑥) = (𝐴(,)𝑢))
310		itgeq1 26073	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑢) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
311	309, 310	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑢 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
312		itgex 26071	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ V
313	311, 1, 312	fvmpt 6985	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐺‘𝑢) = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
314	308, 313	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝐺‘𝑢) = ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡)
315	307, 314	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) = ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡))
316		fvexd 6892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑢)) → (𝐹‘𝑡) ∈ V)
317	316, 298	itgcl 26084	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ ℂ)
318	317	adantrr 730	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 ∈ ℂ)
319		fvexd 6892	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ V)
320	319, 304	itgcl 26084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡 ∈ ℂ)
321	318, 320	pncan2d 11652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
322	321	3adantr3 1190	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡 + ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑢)(𝐹‘𝑡) d𝑡) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
323	315, 322	eqtrd 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
324	323	fveq2d 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) = (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
325		ftc1anc.t	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))))
326		df-ov 7415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑢(,)𝑤) = ((,)‘⟨𝑢, 𝑤⟩)
327		opelxpi 5688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))
328		ioof 13559	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
329		ffn 6701	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
330	328, 329	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (,) Fn (ℝ* × ℝ*)
331		iccssxr 13542	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴[,]𝐵) ⊆ ℝ*
332		xpss12 5666	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐴[,]𝐵) ⊆ ℝ* ∧ (𝐴[,]𝐵) ⊆ ℝ*) → ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*))
333	331, 331, 332	mp2an 705	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*)
334		fnfvima 7231	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((,) Fn (ℝ* × ℝ*) ∧ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) ⊆ (ℝ* × ℝ*) ∧ ⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵))) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
335	330, 333, 334	mp3an12 1480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑢, 𝑤⟩ ∈ ((𝐴[,]𝐵) × (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
336	327, 335	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((,)‘⟨𝑢, 𝑤⟩) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
337	326, 336	eqeltrid 2865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
338		itgeq1 26073	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑢(,)𝑤) → ∫𝑠(𝐹‘𝑡) d𝑡 = ∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡)
339	338	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑢(,)𝑤) → (abs‘∫𝑠(𝐹‘𝑡) d𝑡) = (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡))
340		eleq2 2850	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ 𝑠 ↔ 𝑡 ∈ (𝑢(,)𝑤)))
341	340	ifbid 4506	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑢(,)𝑤) → if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))
342	341	mpteq2dv 5199	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = (𝑢(,)𝑤) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))
343	342	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑠 = (𝑢(,)𝑤) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
344	339, 343	breq12d 5116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = (𝑢(,)𝑤) → ((abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)))))
345	344	rspccva 3576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((∀𝑠 ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))(abs‘∫𝑠(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝑠, (abs‘(𝐹‘𝑡)), 0))) ∧ (𝑢(,)𝑤) ∈ ((,) “ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
346	325, 337, 345	syl2an 608	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
347	346	3adantr3 1190	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
348	324, 347	eqbrtrd 5127	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
349	348	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))))
350		subcl 11537	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺‘𝑤) ∈ ℂ ∧ (𝐺‘𝑢) ∈ ℂ) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
351	124, 125, 350	syl2anr 609	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
352	351	anandis 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
353	352	abscld 15586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
354	353	rexrd 11340	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
355	354	3adantr3 1190	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
356	355	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
357	163	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
358	208	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → 𝑦 ∈ ℝ*)
359		xrlelttr 13266	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ* ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
360	356, 357, 358, 359	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
361	349, 360	mpand 708	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
362	251, 361	sylanl1 693	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) < 𝑦 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
363	362	adantr 486	. . . . . . . . . . . . . 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 16	. . . . . . . . . . . . 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 418	. . . . . . . . . . . 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 11830	. . . . . . . . . . 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 473	. . . . . . . . . 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 593	. . . . . . . . 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 3155	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
370		breq2 5107	. . . . . . . . 9 ⊢ (𝑧 = ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → ((abs‘(𝑤 − 𝑢)) < 𝑧 ↔ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )))))
371	370	rspceaimv 3583	. . . . . . . 8 ⊢ ((((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈ ℝ+ ∧ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
372	81, 369, 371	syl2anc 596	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
373		ralnex 3089	. . . . . . . . 9 ⊢ (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0)
374		nne 2960	. . . . . . . . . 10 ⊢ (¬ 𝑟 ≠ 0 ↔ 𝑟 = 0)
375	374	ralbii 3109	. . . . . . . . 9 ⊢ (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔) ¬ 𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
376	373, 375	bitr3i 280	. . . . . . . 8 ⊢ (¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 ↔ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)
377	16	ffnd 6702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 ∈ dom ∫1 → 𝑓 Fn ℝ)
378		fnfvelrn 7072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ran 𝑓)
379	377, 378	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ran 𝑓)
380		elun1 4128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑓‘𝑡) ∈ ran 𝑓 → (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
381	379, 380	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
382		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑟 = (𝑓‘𝑡) → (𝑟 = 0 ↔ (𝑓‘𝑡) = 0))
383	382	rspcva 3575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0)
384	381, 383	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0)
385	384	adantllr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑓‘𝑡) = 0)
386	19	ffnd 6702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 ∈ dom ∫1 → 𝑔 Fn ℝ)
387		fnfvelrn 7072	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ran 𝑔)
388	386, 387	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ran 𝑔)
389		elun2 4129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔‘𝑡) ∈ ran 𝑔 → (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
390	388, 389	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔))
391		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑟 = (𝑔‘𝑡) → (𝑟 = 0 ↔ (𝑔‘𝑡) = 0))
392	391	rspcva 3575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑔‘𝑡) = 0)
393	392	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = (i · 0))
394		it0e0 12550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (i · 0) = 0
395	393, 394	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0)
396	390, 395	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0)
397	396	adantlll 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (i · (𝑔‘𝑡)) = 0)
398	385, 397	oveq12d 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = (0 + 0))
399	398	an32s 665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = (0 + 0))
400		00id 11466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (0 + 0) = 0
401	399, 400	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = 0)
402	401	adantlll 731	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) = 0)
403	402	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0))
404		0cnd 11280	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ)
405	148, 404	ifclda 4518	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ)
406	405	subid1d 11639	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
407	406	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
408	403, 407	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))
409	408	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))
410		fvif 6893	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), (abs‘0))
411		abs0 15432	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (abs‘0) = 0
412		ifeq2 4487	. . . . . . . . . . . . . . . . . . . . . . 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 2784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (abs‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)
415	409, 414	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))
416	415	mpteq2dva 5198	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
417	416	fveq2d 6881	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
418	417	breq1d 5113	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)))
419	418	biimpd 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)))
420	419	ex 418	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0 → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))))
421	420	com23 87	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → (∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))))
422	421	imp32 424	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
423	422	anasss 472	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
424	423	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
425		1rp 13105	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ+
426	425	ne0ii 4290	. . . . . . . . . . . 12 ⊢ ℝ+ ≠ ∅
427	352	anassrs 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((𝐺‘𝑤) − (𝐺‘𝑢)) ∈ ℂ)
428	427	abscld 15586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
429	428	adantlrr 734	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
430	429	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ)
431		rpre 13110	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ)
432	431	rehalfcld 12574	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → (𝑦 / 2) ∈ ℝ)
433	432	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈ ℝ)
434	433	ad3antlr 744	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ)
435	431	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈ ℝ)
436	435	ad3antlr 744	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑦 ∈ ℝ)
437	430	rexrd 11340	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ∈ ℝ*)
438	156	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ (0[,]+∞))
439	153, 438	ifclda 4518	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
440	439	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ (0[,]+∞))
441	440	fmpttd 7107	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
442		itg2cl 26033	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
443	441, 442	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
444	443	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
445	434	rexrd 11340	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) ∈ ℝ*)
446	108, 107	oveqan12rd 7432	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → ((𝐺‘𝑎) − (𝐺‘𝑏)) = ((𝐺‘𝑤) − (𝐺‘𝑢)))
447	446	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → (abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) = (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))))
448	447	breq1d 5113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 = 𝑢 ∧ 𝑎 = 𝑤) → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))))
449	98, 97	oveqan12rd 7432	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → ((𝐺‘𝑎) − (𝐺‘𝑏)) = ((𝐺‘𝑢) − (𝐺‘𝑤)))
450	449	fveq2d 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → (abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) = (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))))
451	450	breq1d 5113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏 = 𝑤 ∧ 𝑎 = 𝑢) → ((abs‘((𝐺‘𝑎) − (𝐺‘𝑏))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))))
452	128	breq1d 5113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ↔ (abs‘((𝐺‘𝑢) − (𝐺‘𝑤))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))))
453	320	abscld 15586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ∈ ℝ)
454	453	rexrd 11340	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ∈ ℝ*)
455	443	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ*)
456	441	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)):ℝ⟶(0[,]+∞))
457		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((abs‘(𝐹‘𝑡)) = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
458		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 = if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0 ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
459	149	leidd 11863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)))
460		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((abs‘(𝐹‘𝑡)) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) → ((abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))))
461		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (0 = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) → (0 ≤ (abs‘(𝐹‘𝑡)) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡))))
462	460, 461	ifboth 4522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((abs‘(𝐹‘𝑡)) ≤ (abs‘(𝐹‘𝑡)) ∧ 0 ≤ (abs‘(𝐹‘𝑡))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))
463	459, 151, 462	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))
464	463	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ (abs‘(𝐹‘𝑡)))
465	146	ssneld 3933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (¬ 𝑡 ∈ 𝐷 → ¬ 𝑡 ∈ (𝑢(,)𝑤)))
466	465	imp 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ 𝐷) → ¬ 𝑡 ∈ (𝑢(,)𝑤))
467	225, 223	eqbrtrdi 5144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ 𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0)
468	466, 467	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ 𝐷) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ 0)
469	457, 458, 464, 468	ifbothda 4521	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))
470	469	ralrimivw 3159	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))
471	232, 233	ifex 4533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ V
472	471	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0) ∈ V)
473		eqidd 2762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
474	231, 235, 472, 239, 473	ofrfval2 7703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
475	474	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
476	470, 475	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0)) ∘r ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0)))
477		itg2le 26040	. . . . . . . . . . . . . . . . . . . . . . . . 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 1398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘(𝐹‘𝑡)), 0))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
479	454, 162, 455, 346, 478	xrletrd 13272	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘∫(𝑢(,)𝑤)(𝐹‘𝑡) d𝑡) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
480	479	3adantr3 1190	. . . . . . . . . . . . . . . . . . . . . 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 11830	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
483	482	anassrs 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
484	483	adantlrr 734	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
485	484	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))))
486		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2))
487	437, 444, 445, 485, 486	xrlelttrd 13270	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < (𝑦 / 2))
488		rphalflt 13132	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℝ+ → (𝑦 / 2) < 𝑦)
489	488	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) < 𝑦)
490	489	ad3antlr 744	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝑦 / 2) < 𝑦)
491	430, 434, 436, 487, 490	lttrd 11452	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)
492	491	a1d 26	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → ((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
493	492	ralrimiva 3155	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
494	493	ralrimivw 3159	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∀𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
495		r19.2z 4455	. . . . . . . . . . . 12 ⊢ ((ℝ+ ≠ ∅ ∧ ∀𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
496	426, 494, 495	sylancr 599	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(𝐹‘𝑡)), 0))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
497	424, 496	syldan 603	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0))) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
498	497	anassrs 473	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
499	498	anassrs 473	. . . . . . . 8 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∀𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 = 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
500	376, 499	sylan2b 606	. . . . . . 7 ⊢ (((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ¬ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
501	372, 500	pm2.61dan 825	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
502	501	ex 418	. . . . 5 ⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))
503	502	rexlimdvva 3220	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → (∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦)))
504	13, 503	mpd 16	. . 3 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
505	504	ralrimivva 3206	. 2 ⊢ (𝜑 → ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))
506		ssid 3953	. . 3 ⊢ ℂ ⊆ ℂ
507		elcncf2 25191	. . 3 ⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))))
508	117, 506, 507	sylancl 598	. 2 ⊢ (𝜑 → (𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ) ↔ (𝐺:(𝐴[,]𝐵)⟶ℂ ∧ ∀𝑢 ∈ (𝐴[,]𝐵)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (𝐴[,]𝐵)((abs‘(𝑤 − 𝑢)) < 𝑧 → (abs‘((𝐺‘𝑤) − (𝐺‘𝑢))) < 𝑦))))
509	9, 505, 508	mpbir2and 726	1 ⊢ (𝜑 → 𝐺 ∈ ((𝐴[,]𝐵)–cn→ℂ))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  Vcvv 3451   ∪ cun 3897   ⊆ wss 3899  ∅c0 4279  ifcif 4482  𝒫 cpw 4557  ⟨cop 4590   class class class wbr 5103   ↦ cmpt 5186   × cxp 5649  dom cdm 5651  ran crn 5652   “ cima 5654  Fun wfun 6525   Fn wfn 6526  ⟶wf 6527  ‘cfv 6531  (class class class)co 7412   ∘_r cofr 7681  Fincfn 8957  supcsup 9416  ℂcc 11179  ℝcr 11180  0cc0 11181  1c1 11182  ici 11183   + caddc 11184   · cmul 11186  +∞cpnf 11321  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325   − cmin 11522   / cdiv 11954  2c2 12378  ℝ⁺crp 13101  (,)cioo 13457  [,]cicc 13460  abscabs 15381  –cn→ccncf 25177  volcvol 25764  ∫₁citg1 25916  ∫₂citg2 25917  𝐿¹cibl 25918  ∫citg 25919

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-inf2 9626  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-addrcl 11242  ax-mulcl 11243  ax-mulrcl 11244  ax-mulcom 11245  ax-addass 11246  ax-mulass 11247  ax-distr 11248  ax-i2m1 11249  ax-1ne0 11250  ax-1rid 11251  ax-rnegex 11252  ax-rrecex 11253  ax-cnre 11254  ax-pre-lttri 11255  ax-pre-lttrn 11256  ax-pre-ltadd 11257  ax-pre-mulgt0 11258  ax-pre-sup 11259  ax-addf 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-symdif 4199  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-disj 5071  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7682  df-ofr 7683  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8460  df-2o 8461  df-er 8701  df-map 8833  df-pm 8834  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fi 9387  df-sup 9418  df-inf 9419  df-oi 9488  df-dju 9963  df-card 10001  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11524  df-neg 11525  df-div 11955  df-nn 12317  df-2 12386  df-3 12387  df-4 12388  df-n0 12588  df-z 12675  df-uz 12947  df-q 13057  df-rp 13102  df-xneg 13222  df-xadd 13223  df-xmul 13224  df-ioo 13461  df-ico 13463  df-icc 13464  df-fz 13621  df-fzo 13769  df-fl 13912  df-mod 13990  df-seq 14125  df-exp 14185  df-hash 14455  df-cj 15246  df-re 15247  df-im 15248  df-sqrt 15382  df-abs 15383  df-clim 15635  df-rlim 15636  df-sum 15834  df-rest 17573  df-topgen 17594  df-psmet 21650  df-xmet 21651  df-met 21652  df-bl 21653  df-mopn 21654  df-top 23192  df-topon 23209  df-bases 23244  df-cmp 23685  df-cncf 25179  df-ovol 25765  df-vol 25766  df-mbf 25920  df-itg1 25921  df-itg2 25922  df-ibl 25923  df-itg 25924  df-0p 25971

This theorem is used by:  ftc2nc  38588