Theorem ftc1cnnclem

Description: Lemma for ftc1cnnc ; cf. ftc1lem4 . The stronger assumptions of ftc1cn are exploited to make use of weaker theorems. (Contributed by Brendan Leahy, 19-Nov-2017)

	Ref	Expression
Hypotheses	ftc1cnnc.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
	ftc1cnnc.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ftc1cnnc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ftc1cnnc.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ftc1cnnc.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
	ftc1cnnc.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
	ftc1cnnclem.c	⊢ ( 𝜑 → 𝑐 ∈ ( 𝐴 (,) 𝐵 ) )
	ftc1cnnclem.h	⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) )
	ftc1cnnclem.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	ftc1cnnclem.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
	ftc1cnnclem.fc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) )
	ftc1cnnclem.x1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
	ftc1cnnclem.x2	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝑐 ) ) < 𝑅 )
	ftc1cnnclem.y1	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
	ftc1cnnclem.y2	⊢ ( 𝜑 → ( abs ‘ ( 𝑌 − 𝑐 ) ) < 𝑅 )
Assertion	ftc1cnnclem	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		ftc1cnnc.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2		ftc1cnnc.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3		ftc1cnnc.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		ftc1cnnc.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5		ftc1cnnc.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
6		ftc1cnnc.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
7		ftc1cnnclem.c	⊢ ( 𝜑 → 𝑐 ∈ ( 𝐴 (,) 𝐵 ) )
8		ftc1cnnclem.h	⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝑐 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑐 ) ) / ( 𝑧 − 𝑐 ) ) )
9		ftc1cnnclem.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
10		ftc1cnnclem.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
11		ftc1cnnclem.fc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) )
12		ftc1cnnclem.x1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
13		ftc1cnnclem.x2	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝑐 ) ) < 𝑅 )
14		ftc1cnnclem.y1	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
15		ftc1cnnclem.y2	⊢ ( 𝜑 → ( abs ‘ ( 𝑌 − 𝑐 ) ) < 𝑅 )
16		ovexd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ∈ V )
17	2	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
18	3	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
19		elicc1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
20	19	biimpa	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑋 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) )
21	20	simp2d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ 𝑋 )
22	17 18 12 21	syl21anc	⊢ ( 𝜑 → 𝐴 ≤ 𝑋 )
23		iccleub	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑌 ≤ 𝐵 )
24	17 18 14 23	syl3anc	⊢ ( 𝜑 → 𝑌 ≤ 𝐵 )
25		ioossioo	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝑋 ∧ 𝑌 ≤ 𝐵 ) ) → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
26	17 18 22 24 25	syl22anc	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
27	26	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 ∈ ( 𝐴 (,) 𝐵 ) )
28		cncff	⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
29	5 28	syl	⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
30	29	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
31	27 30	syldan	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
32		ioombl	⊢ ( 𝑋 (,) 𝑌 ) ∈ dom vol
33	32	a1i	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ∈ dom vol )
34		fvexd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
35	29	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑡 ) ) )
36	35 6	eqeltrrd	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
37	26 33 34 36	iblss	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
38	29 7	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
40		fconstmpt	⊢ ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝑐 ) } ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑐 ) )
41		mblvol	⊢ ( ( 𝑋 (,) 𝑌 ) ∈ dom vol → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) )
42	32 41	ax-mp	⊢ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( vol* ‘ ( 𝑋 (,) 𝑌 ) )
43		ioossicc	⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 )
44	43	a1i	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) )
45		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
46	2 3 45	syl2anc	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
47	46 12	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
48	46 14	sseldd	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
49		iccmbl	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 [,] 𝑌 ) ∈ dom vol )
50	47 48 49	syl2anc	⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ∈ dom vol )
51		mblss	⊢ ( ( 𝑋 [,] 𝑌 ) ∈ dom vol → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
52	50 51	syl	⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
53		mblvol	⊢ ( ( 𝑋 [,] 𝑌 ) ∈ dom vol → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) = ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) )
54	50 53	syl	⊢ ( 𝜑 → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) = ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) )
55		iccvolcl	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
56	47 48 55	syl2anc	⊢ ( 𝜑 → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
57	54 56	eqeltrrd	⊢ ( 𝜑 → ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
58		ovolsscl	⊢ ( ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) ∧ ( 𝑋 [,] 𝑌 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
59	44 52 57 58	syl3anc	⊢ ( 𝜑 → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
60	42 59	eqeltrid	⊢ ( 𝜑 → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
61		iblconst	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℂ ) → ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝑐 ) } ) ∈ 𝐿1 )
62	33 60 38 61	syl3anc	⊢ ( 𝜑 → ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝑐 ) } ) ∈ 𝐿1 )
63	40 62	eqeltrrid	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑐 ) ) ∈ 𝐿1 )
64		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
65	64	subcn	⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
66	65	a1i	⊢ ( 𝜑 → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
67	29 26	feqresmpt	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) )
68		rescncf	⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) → ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) )
69	26 5 68	sylc	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
70	67 69	eqeltrrd	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
71		ioossre	⊢ ( 𝑋 (,) 𝑌 ) ⊆ ℝ
72		ax-resscn	⊢ ℝ ⊆ ℂ
73	71 72	sstri	⊢ ( 𝑋 (,) 𝑌 ) ⊆ ℂ
74		ssid	⊢ ℂ ⊆ ℂ
75		cncfmptc	⊢ ( ( ( 𝐹 ‘ 𝑐 ) ∈ ℂ ∧ ( 𝑋 (,) 𝑌 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑐 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
76	73 74 75	mp3an23	⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ ℂ → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑐 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
77	38 76	syl	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑐 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
78	64 66 70 77	cncfmpt2f	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
79		cnmbf	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ MblFn )
80	32 78 79	sylancr	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ MblFn )
81	31 37 39 63 80	iblsubnc	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ 𝐿1 )
82	16 81	itgcl	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ∈ ℂ )
83	82	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ∈ ℂ )
84	48 47	resubcld	⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℝ )
85	84	recnd	⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℂ )
86	85	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ∈ ℂ )
87	47 48	posdifd	⊢ ( 𝜑 → ( 𝑋 < 𝑌 ↔ 0 < ( 𝑌 − 𝑋 ) ) )
88	87	biimpa	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( 𝑌 − 𝑋 ) )
89	88	gt0ne0d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ≠ 0 )
90	83 86 89	divcld	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ∈ ℂ )
91	38	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
92		ltle	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) )
93	47 48 92	syl2anc	⊢ ( 𝜑 → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) )
94	93	imp	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 ≤ 𝑌 )
95		ssidd	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
96		ioossre	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
97	96	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
98	1 2 3 4 95 97 6 29 12 14	ftc1lem1	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
99	94 98	syldan	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
100	31 39	npcand	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) = ( 𝐹 ‘ 𝑡 ) )
101	100	itgeq2dv	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) d 𝑡 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
102	31 39	subcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ∈ ℂ )
103	100	mpteq2dva	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) )
104	103 67	eqtr4d	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) ) = ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) )
105		iblmbf	⊢ ( 𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn )
106	6 105	syl	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
107		mbfres	⊢ ( ( 𝐹 ∈ MblFn ∧ ( 𝑋 (,) 𝑌 ) ∈ dom vol ) → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ MblFn )
108	106 32 107	sylancl	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑋 (,) 𝑌 ) ) ∈ MblFn )
109	104 108	eqeltrd	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) ) ∈ MblFn )
110	102 81 39 63 109	itgaddnc	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) + ( 𝐹 ‘ 𝑐 ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 ) )
111	101 110	eqtr3d	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 ) )
112	111	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 ) )
113		itgconst	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑐 ) ∈ ℂ ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 = ( ( 𝐹 ‘ 𝑐 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
114	33 60 38 113	syl3anc	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 = ( ( 𝐹 ‘ 𝑐 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
115	114	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 = ( ( 𝐹 ‘ 𝑐 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
116	47	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ ℝ )
117	48	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ ℝ )
118		ovolioo	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
119	116 117 94 118	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
120	42 119	eqtrid	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
121	120	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ‘ 𝑐 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) = ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) )
122	115 121	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 = ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) )
123	122	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑐 ) d 𝑡 ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) ) )
124	99 112 123	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) ) )
125	124	oveq1d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) ) / ( 𝑌 − 𝑋 ) ) )
126	91 86	mulcld	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) ∈ ℂ )
127	83 126 86 89	divdird	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) )
128	91 86 89	divcan4d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( 𝐹 ‘ 𝑐 ) )
129	128	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( ( ( 𝐹 ‘ 𝑐 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( 𝐹 ‘ 𝑐 ) ) )
130	125 127 129	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( 𝐹 ‘ 𝑐 ) ) )
131	90 91 130	mvrraddd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝑐 ) ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) )
132	131	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) = ( abs ‘ ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ) )
133	83 86 89	absdivd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( abs ‘ ( 𝑌 − 𝑋 ) ) ) )
134	84	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ∈ ℝ )
135		0re	⊢ 0 ∈ ℝ
136		ltle	⊢ ( ( 0 ∈ ℝ ∧ ( 𝑌 − 𝑋 ) ∈ ℝ ) → ( 0 < ( 𝑌 − 𝑋 ) → 0 ≤ ( 𝑌 − 𝑋 ) ) )
137	135 134 136	sylancr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 0 < ( 𝑌 − 𝑋 ) → 0 ≤ ( 𝑌 − 𝑋 ) ) )
138	88 137	mpd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 ≤ ( 𝑌 − 𝑋 ) )
139	134 138	absidd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( 𝑌 − 𝑋 ) ) = ( 𝑌 − 𝑋 ) )
140	139	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( abs ‘ ( 𝑌 − 𝑋 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) )
141	132 133 140	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) )
142	83	abscld	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ∈ ℝ )
143	102	abscld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ ℝ )
144		cncfss	⊢ ( ( ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ ) )
145	72 74 144	mp2an	⊢ ( ℂ –cn→ ℝ ) ⊆ ( ℂ –cn→ ℂ )
146		abscncf	⊢ abs ∈ ( ℂ –cn→ ℝ )
147	145 146	sselii	⊢ abs ∈ ( ℂ –cn→ ℂ )
148	147	a1i	⊢ ( 𝜑 → abs ∈ ( ℂ –cn→ ℂ ) )
149	148 78	cncfmpt1f	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
150		cnmbf	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ MblFn )
151	32 149 150	sylancr	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ MblFn )
152	16 81 151	iblabsnc	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ 𝐿1 )
153	143 152	itgrecl	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ∈ ℝ )
154	153	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ∈ ℝ )
155	9	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
156	84 155	remulcld	⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) · 𝐸 ) ∈ ℝ )
157	156	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝑌 − 𝑋 ) · 𝐸 ) ∈ ℝ )
158	82	cjcld	⊢ ( 𝜑 → ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ∈ ℂ )
159		cncfmptc	⊢ ( ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ∈ ℂ ∧ ( 𝑋 (,) 𝑌 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
160	73 74 159	mp3an23	⊢ ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ∈ ℂ → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
161	158 160	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
162		nfcv	⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) )
163		nfcsb1v	⊢ Ⅎ 𝑡 ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) )
164		csbeq1a	⊢ ( 𝑡 = 𝑥 → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) = ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) )
165	162 163 164	cbvmpt	⊢ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) )
166	165 78	eqeltrrid	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
167	161 166	mulcncf	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) · ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
168		cnmbf	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) · ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) · ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ MblFn )
169	32 167 168	sylancr	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( ∗ ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) · ⦋ 𝑥 / 𝑡 ⦌ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ MblFn )
170	102 81 151 169	itgabsnc	⊢ ( 𝜑 → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ≤ ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 )
171	170	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ≤ ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 )
172		simpr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 < 𝑌 )
173	155	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐸 ∈ ℝ )
174		fconstmpt	⊢ ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 )
175	9	rpcnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
176		iblconst	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ 𝐸 ∈ ℂ ) → ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) ∈ 𝐿1 )
177	33 60 175 176	syl3anc	⊢ ( 𝜑 → ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) ∈ 𝐿1 )
178	174 177	eqeltrrid	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 )
179		cncfmptc	⊢ ( ( 𝐸 ∈ ℂ ∧ ( 𝑋 (,) 𝑌 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
180	73 74 179	mp3an23	⊢ ( 𝐸 ∈ ℂ → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
181	175 180	syl	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
182	64 66 181 149	cncfmpt2f	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
183		cnmbf	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ MblFn )
184	32 182 183	sylancr	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ MblFn )
185	173 178 143 152 184	iblsubnc	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ 𝐿1 )
186	185	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ 𝐿1 )
187	11	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) )
188	187	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) )
189	96 7	sselid	⊢ ( 𝜑 → 𝑐 ∈ ℝ )
190	10	rpred	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
191	189 190	resubcld	⊢ ( 𝜑 → ( 𝑐 − 𝑅 ) ∈ ℝ )
192	191	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑐 − 𝑅 ) ∈ ℝ )
193	47	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑋 ∈ ℝ )
194		elioore	⊢ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) → 𝑡 ∈ ℝ )
195	194	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 ∈ ℝ )
196	47 189 190	absdifltd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝑐 ) ) < 𝑅 ↔ ( ( 𝑐 − 𝑅 ) < 𝑋 ∧ 𝑋 < ( 𝑐 + 𝑅 ) ) ) )
197	13 196	mpbid	⊢ ( 𝜑 → ( ( 𝑐 − 𝑅 ) < 𝑋 ∧ 𝑋 < ( 𝑐 + 𝑅 ) ) )
198	197	simpld	⊢ ( 𝜑 → ( 𝑐 − 𝑅 ) < 𝑋 )
199	198	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑐 − 𝑅 ) < 𝑋 )
200		eliooord	⊢ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) → ( 𝑋 < 𝑡 ∧ 𝑡 < 𝑌 ) )
201	200	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑋 < 𝑡 ∧ 𝑡 < 𝑌 ) )
202	201	simpld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑋 < 𝑡 )
203	192 193 195 199 202	lttrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑐 − 𝑅 ) < 𝑡 )
204	48	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑌 ∈ ℝ )
205	189 190	readdcld	⊢ ( 𝜑 → ( 𝑐 + 𝑅 ) ∈ ℝ )
206	205	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑐 + 𝑅 ) ∈ ℝ )
207	201	simprd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 < 𝑌 )
208	48 189 190	absdifltd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑌 − 𝑐 ) ) < 𝑅 ↔ ( ( 𝑐 − 𝑅 ) < 𝑌 ∧ 𝑌 < ( 𝑐 + 𝑅 ) ) ) )
209	15 208	mpbid	⊢ ( 𝜑 → ( ( 𝑐 − 𝑅 ) < 𝑌 ∧ 𝑌 < ( 𝑐 + 𝑅 ) ) )
210	209	simprd	⊢ ( 𝜑 → 𝑌 < ( 𝑐 + 𝑅 ) )
211	210	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑌 < ( 𝑐 + 𝑅 ) )
212	195 204 206 207 211	lttrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 < ( 𝑐 + 𝑅 ) )
213	189	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑐 ∈ ℝ )
214	190	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑅 ∈ ℝ )
215	195 213 214	absdifltd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( 𝑡 − 𝑐 ) ) < 𝑅 ↔ ( ( 𝑐 − 𝑅 ) < 𝑡 ∧ 𝑡 < ( 𝑐 + 𝑅 ) ) ) )
216	203 212 215	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( 𝑡 − 𝑐 ) ) < 𝑅 )
217		fvoveq1	⊢ ( 𝑦 = 𝑡 → ( abs ‘ ( 𝑦 − 𝑐 ) ) = ( abs ‘ ( 𝑡 − 𝑐 ) ) )
218	217	breq1d	⊢ ( 𝑦 = 𝑡 → ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 ↔ ( abs ‘ ( 𝑡 − 𝑐 ) ) < 𝑅 ) )
219	218	imbrov2fvoveq	⊢ ( 𝑦 = 𝑡 → ( ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) ↔ ( ( abs ‘ ( 𝑡 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) ) )
220	219	rspcv	⊢ ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) → ( ( abs ‘ ( 𝑡 − 𝑐 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ) ) )
221	27 188 216 220	syl3c	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 )
222		difrp	⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ∈ ℝ ∧ 𝐸 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ↔ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ℝ+ ) )
223	143 173 222	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 ↔ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ℝ+ ) )
224	221 223	mpbid	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ℝ+ )
225	224	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ∈ ℝ+ )
226	182	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
227	172 186 225 226	itggt0cn	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) d 𝑡 )
228	173 178 143 152 184	itgsubnc	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) )
229	228	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) )
230		itgconst	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ 𝐸 ∈ ℂ ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
231	33 60 175 230	syl3anc	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
232	231	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
233	120	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) = ( 𝐸 · ( 𝑌 − 𝑋 ) ) )
234	175 85	mulcomd	⊢ ( 𝜑 → ( 𝐸 · ( 𝑌 − 𝑋 ) ) = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
235	234	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐸 · ( 𝑌 − 𝑋 ) ) = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
236	232 233 235	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
237	236	oveq1d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) = ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) )
238	229 237	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) ) d 𝑡 = ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) )
239	227 238	breqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) )
240	153 156	posdifd	⊢ ( 𝜑 → ( ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ↔ 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) ) )
241	240	biimpar	⊢ ( ( 𝜑 ∧ 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 ) ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
242	239 241	syldan	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
243	142 154 157 171 242	lelttrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
244	155	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝐸 ∈ ℝ )
245		ltdivmul	⊢ ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) ∈ ℝ ∧ 𝐸 ∈ ℝ ∧ ( ( 𝑌 − 𝑋 ) ∈ ℝ ∧ 0 < ( 𝑌 − 𝑋 ) ) ) → ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 ↔ ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ) )
246	142 244 134 88 245	syl112anc	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 ↔ ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ) )
247	243 246	mpbird	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝑐 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 )
248	141 247	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝑐 ) ) ) < 𝐸 )