Theorem ftc1lem4

Description: Lemma for ftc1 . (Contributed by Mario Carneiro, 31-Aug-2014)

	Ref	Expression
Hypotheses	ftc1.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
	ftc1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ftc1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ftc1.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ftc1.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
	ftc1.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
	ftc1.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
	ftc1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
	ftc1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) )
	ftc1.j	⊢ 𝐽 = ( 𝐿 ↾t ℝ )
	ftc1.k	⊢ 𝐾 = ( 𝐿 ↾t 𝐷 )
	ftc1.l	⊢ 𝐿 = ( TopOpen ‘ ℂfld )
	ftc1.h	⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
	ftc1.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	ftc1.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
	ftc1.fc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
	ftc1.x1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
	ftc1.x2	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐶 ) ) < 𝑅 )
	ftc1.y1	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
	ftc1.y2	⊢ ( 𝜑 → ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑅 )
Assertion	ftc1lem4	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		ftc1.g	⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2		ftc1.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3		ftc1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		ftc1.le	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5		ftc1.s	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
6		ftc1.d	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
7		ftc1.i	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
8		ftc1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
9		ftc1.f	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐾 CnP 𝐿 ) ‘ 𝐶 ) )
10		ftc1.j	⊢ 𝐽 = ( 𝐿 ↾t ℝ )
11		ftc1.k	⊢ 𝐾 = ( 𝐿 ↾t 𝐷 )
12		ftc1.l	⊢ 𝐿 = ( TopOpen ‘ ℂfld )
13		ftc1.h	⊢ 𝐻 = ( 𝑧 ∈ ( ( 𝐴 [,] 𝐵 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
14		ftc1.e	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
15		ftc1.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
16		ftc1.fc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
17		ftc1.x1	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
18		ftc1.x2	⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 𝐶 ) ) < 𝑅 )
19		ftc1.y1	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
20		ftc1.y2	⊢ ( 𝜑 → ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑅 )
21		ovexd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ∈ V )
22	2	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
23		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
24	2 3 23	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
25	17 24	mpbid	⊢ ( 𝜑 → ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) )
26	25	simp2d	⊢ ( 𝜑 → 𝐴 ≤ 𝑋 )
27		iooss1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ) → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝑌 ) )
28	22 26 27	syl2anc	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝑌 ) )
29	3	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
30		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) ) )
31	2 3 30	syl2anc	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) ) )
32	19 31	mpbid	⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) )
33	32	simp3d	⊢ ( 𝜑 → 𝑌 ≤ 𝐵 )
34		iooss2	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑌 ≤ 𝐵 ) → ( 𝐴 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
35	29 33 34	syl2anc	⊢ ( 𝜑 → ( 𝐴 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
36	28 35	sstrd	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
37	36 5	sstrd	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ 𝐷 )
38	37	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 ∈ 𝐷 )
39	1 2 3 4 5 6 7 8 9 10 11 12	ftc1lem3	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
40	39	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
41	38 40	syldan	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
42		ioombl	⊢ ( 𝑋 (,) 𝑌 ) ∈ dom vol
43	42	a1i	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ∈ dom vol )
44		fvexd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
45	39	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) )
46	45 7	eqeltrrd	⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
47	37 43 44 46	iblss	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
48	5 8	sseldd	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
49	39 48	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
50	49	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
51		fconstmpt	⊢ ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝐶 ) } ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) )
52		mblvol	⊢ ( ( 𝑋 (,) 𝑌 ) ∈ dom vol → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) )
53	42 52	ax-mp	⊢ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( vol* ‘ ( 𝑋 (,) 𝑌 ) )
54		ioossicc	⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 )
55	54	a1i	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) )
56		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
57	2 3 56	syl2anc	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
58	57 17	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
59	57 19	sseldd	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
60		iccmbl	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 [,] 𝑌 ) ∈ dom vol )
61	58 59 60	syl2anc	⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ∈ dom vol )
62		mblss	⊢ ( ( 𝑋 [,] 𝑌 ) ∈ dom vol → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
63	61 62	syl	⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
64		mblvol	⊢ ( ( 𝑋 [,] 𝑌 ) ∈ dom vol → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) = ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) )
65	61 64	syl	⊢ ( 𝜑 → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) = ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) )
66		iccvolcl	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
67	58 59 66	syl2anc	⊢ ( 𝜑 → ( vol ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
68	65 67	eqeltrrd	⊢ ( 𝜑 → ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ )
69		ovolsscl	⊢ ( ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) ∧ ( 𝑋 [,] 𝑌 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑋 [,] 𝑌 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
70	55 63 68 69	syl3anc	⊢ ( 𝜑 → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
71	53 70	eqeltrid	⊢ ( 𝜑 → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ )
72		iblconst	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐶 ) ∈ ℂ ) → ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝐶 ) } ) ∈ 𝐿1 )
73	43 71 49 72	syl3anc	⊢ ( 𝜑 → ( ( 𝑋 (,) 𝑌 ) × { ( 𝐹 ‘ 𝐶 ) } ) ∈ 𝐿1 )
74	51 73	eqeltrrid	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) ∈ 𝐿1 )
75	41 47 50 74	iblsub	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ∈ 𝐿1 )
76	21 75	itgcl	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ∈ ℂ )
77	76	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ∈ ℂ )
78	59 58	resubcld	⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℝ )
79	78	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ∈ ℝ )
80	79	recnd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ∈ ℂ )
81	58 59	posdifd	⊢ ( 𝜑 → ( 𝑋 < 𝑌 ↔ 0 < ( 𝑌 − 𝑋 ) ) )
82	81	biimpa	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( 𝑌 − 𝑋 ) )
83	82	gt0ne0d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑌 − 𝑋 ) ≠ 0 )
84	77 80 83	divcld	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ∈ ℂ )
85	49	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
86		ltle	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) )
87	58 59 86	syl2anc	⊢ ( 𝜑 → ( 𝑋 < 𝑌 → 𝑋 ≤ 𝑌 ) )
88	87	imp	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 ≤ 𝑌 )
89	1 2 3 4 5 6 7 39 17 19	ftc1lem1	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
90	88 89	syldan	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
91	41 50	npcand	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) + ( 𝐹 ‘ 𝐶 ) ) = ( 𝐹 ‘ 𝑡 ) )
92	91	itgeq2dv	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) + ( 𝐹 ‘ 𝐶 ) ) d 𝑡 = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
93	41 50	subcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ∈ ℂ )
94	93 75 50 74	itgadd	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) + ( 𝐹 ‘ 𝐶 ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 ) )
95	92 94	eqtr3d	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 ) )
96	95	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 ) )
97		itgconst	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐶 ) ∈ ℂ ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 = ( ( 𝐹 ‘ 𝐶 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
98	43 71 49 97	syl3anc	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 = ( ( 𝐹 ‘ 𝐶 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
99	98	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 = ( ( 𝐹 ‘ 𝐶 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
100	58	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑋 ∈ ℝ )
101	59	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝑌 ∈ ℝ )
102		ovolioo	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌 ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
103	100 101 88 102	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( vol* ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
104	53 103	eqtrid	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( vol ‘ ( 𝑋 (,) 𝑌 ) ) = ( 𝑌 − 𝑋 ) )
105	104	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ‘ 𝐶 ) · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) = ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) )
106	99 105	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 = ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) )
107	106	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝐶 ) d 𝑡 ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) ) )
108	90 96 107	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) ) )
109	108	oveq1d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) ) / ( 𝑌 − 𝑋 ) ) )
110	85 80	mulcld	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) ∈ ℂ )
111	77 110 80 83	divdird	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 + ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) )
112	85 80 83	divcan4d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( 𝐹 ‘ 𝐶 ) )
113	112	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( ( ( 𝐹 ‘ 𝐶 ) · ( 𝑌 − 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( 𝐹 ‘ 𝐶 ) ) )
114	109 111 113	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) = ( ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) + ( 𝐹 ‘ 𝐶 ) ) )
115	84 85 114	mvrraddd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) = ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) )
116	115	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( abs ‘ ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ) )
117	77 80 83	absdivd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 / ( 𝑌 − 𝑋 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( abs ‘ ( 𝑌 − 𝑋 ) ) ) )
118		0re	⊢ 0 ∈ ℝ
119		ltle	⊢ ( ( 0 ∈ ℝ ∧ ( 𝑌 − 𝑋 ) ∈ ℝ ) → ( 0 < ( 𝑌 − 𝑋 ) → 0 ≤ ( 𝑌 − 𝑋 ) ) )
120	118 79 119	sylancr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 0 < ( 𝑌 − 𝑋 ) → 0 ≤ ( 𝑌 − 𝑋 ) ) )
121	82 120	mpd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 ≤ ( 𝑌 − 𝑋 ) )
122	79 121	absidd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( 𝑌 − 𝑋 ) ) = ( 𝑌 − 𝑋 ) )
123	122	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( abs ‘ ( 𝑌 − 𝑋 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) )
124	116 117 123	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) )
125	76	abscld	⊢ ( 𝜑 → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ∈ ℝ )
126	125	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ∈ ℝ )
127	93	abscld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ∈ ℝ )
128	21 75	iblabs	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ∈ 𝐿1 )
129	127 128	itgrecl	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ∈ ℝ )
130	129	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ∈ ℝ )
131	14	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
132	78 131	remulcld	⊢ ( 𝜑 → ( ( 𝑌 − 𝑋 ) · 𝐸 ) ∈ ℝ )
133	132	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( 𝑌 − 𝑋 ) · 𝐸 ) ∈ ℝ )
134	93 75	itgabs	⊢ ( 𝜑 → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ≤ ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 )
135	134	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ≤ ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 )
136	82 104	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( vol ‘ ( 𝑋 (,) 𝑌 ) ) )
137	131	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐸 ∈ ℝ )
138		fconstmpt	⊢ ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) = ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 )
139	131	recnd	⊢ ( 𝜑 → 𝐸 ∈ ℂ )
140		iblconst	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ 𝐸 ∈ ℂ ) → ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) ∈ 𝐿1 )
141	43 71 139 140	syl3anc	⊢ ( 𝜑 → ( ( 𝑋 (,) 𝑌 ) × { 𝐸 } ) ∈ 𝐿1 )
142	138 141	eqeltrrid	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐸 ) ∈ 𝐿1 )
143	137 142 127 128	iblsub	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ) ∈ 𝐿1 )
144	143	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ) ∈ 𝐿1 )
145	6 48	sseldd	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
146	15	rpred	⊢ ( 𝜑 → 𝑅 ∈ ℝ )
147	145 146	resubcld	⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) ∈ ℝ )
148	147	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐶 − 𝑅 ) ∈ ℝ )
149	58	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑋 ∈ ℝ )
150	37 6	sstrd	⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ℝ )
151	150	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 ∈ ℝ )
152	58 145 146	absdifltd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑋 − 𝐶 ) ) < 𝑅 ↔ ( ( 𝐶 − 𝑅 ) < 𝑋 ∧ 𝑋 < ( 𝐶 + 𝑅 ) ) ) )
153	18 152	mpbid	⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) < 𝑋 ∧ 𝑋 < ( 𝐶 + 𝑅 ) ) )
154	153	simpld	⊢ ( 𝜑 → ( 𝐶 − 𝑅 ) < 𝑋 )
155	154	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐶 − 𝑅 ) < 𝑋 )
156		eliooord	⊢ ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) → ( 𝑋 < 𝑡 ∧ 𝑡 < 𝑌 ) )
157	156	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝑋 < 𝑡 ∧ 𝑡 < 𝑌 ) )
158	157	simpld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑋 < 𝑡 )
159	148 149 151 155 158	lttrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐶 − 𝑅 ) < 𝑡 )
160	59	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑌 ∈ ℝ )
161	145 146	readdcld	⊢ ( 𝜑 → ( 𝐶 + 𝑅 ) ∈ ℝ )
162	161	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐶 + 𝑅 ) ∈ ℝ )
163	157	simprd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 < 𝑌 )
164	59 145 146	absdifltd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝑌 − 𝐶 ) ) < 𝑅 ↔ ( ( 𝐶 − 𝑅 ) < 𝑌 ∧ 𝑌 < ( 𝐶 + 𝑅 ) ) ) )
165	20 164	mpbid	⊢ ( 𝜑 → ( ( 𝐶 − 𝑅 ) < 𝑌 ∧ 𝑌 < ( 𝐶 + 𝑅 ) ) )
166	165	simprd	⊢ ( 𝜑 → 𝑌 < ( 𝐶 + 𝑅 ) )
167	166	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑌 < ( 𝐶 + 𝑅 ) )
168	151 160 162 163 167	lttrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 < ( 𝐶 + 𝑅 ) )
169	145	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐶 ∈ ℝ )
170	146	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑅 ∈ ℝ )
171	151 169 170	absdifltd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( 𝑡 − 𝐶 ) ) < 𝑅 ↔ ( ( 𝐶 − 𝑅 ) < 𝑡 ∧ 𝑡 < ( 𝐶 + 𝑅 ) ) ) )
172	159 168 171	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( 𝑡 − 𝐶 ) ) < 𝑅 )
173		fvoveq1	⊢ ( 𝑦 = 𝑡 → ( abs ‘ ( 𝑦 − 𝐶 ) ) = ( abs ‘ ( 𝑡 − 𝐶 ) ) )
174	173	breq1d	⊢ ( 𝑦 = 𝑡 → ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 ↔ ( abs ‘ ( 𝑡 − 𝐶 ) ) < 𝑅 ) )
175	174	imbrov2fvoveq	⊢ ( 𝑦 = 𝑡 → ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) ↔ ( ( abs ‘ ( 𝑡 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) ) )
176	16	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
177	176	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
178	175 177 38	rspcdva	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( 𝑡 − 𝐶 ) ) < 𝑅 → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ) )
179	172 178	mpd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )
180		difrp	⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ∈ ℝ ∧ 𝐸 ∈ ℝ ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ↔ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ∈ ℝ+ ) )
181	127 137 180	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 ↔ ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ∈ ℝ+ ) )
182	179 181	mpbid	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ∈ ℝ+ )
183	182	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝑌 ) ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) ∈ ℝ+ )
184	136 144 183	itggt0	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) d 𝑡 )
185	137 142 127 128	itgsub	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) )
186	185	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) d 𝑡 = ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) )
187		itgconst	⊢ ( ( ( 𝑋 (,) 𝑌 ) ∈ dom vol ∧ ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ∈ ℝ ∧ 𝐸 ∈ ℂ ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
188	43 71 139 187	syl3anc	⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
189	188	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) )
190	104	oveq2d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐸 · ( vol ‘ ( 𝑋 (,) 𝑌 ) ) ) = ( 𝐸 · ( 𝑌 − 𝑋 ) ) )
191	78	recnd	⊢ ( 𝜑 → ( 𝑌 − 𝑋 ) ∈ ℂ )
192	139 191	mulcomd	⊢ ( 𝜑 → ( 𝐸 · ( 𝑌 − 𝑋 ) ) = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
193	192	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( 𝐸 · ( 𝑌 − 𝑋 ) ) = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
194	189 190 193	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 = ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
195	194	oveq1d	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ∫ ( 𝑋 (,) 𝑌 ) 𝐸 d 𝑡 − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) = ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) )
196	186 195	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐸 − ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) d 𝑡 = ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) )
197	184 196	breqtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) )
198	129 132	posdifd	⊢ ( 𝜑 → ( ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ↔ 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) ) )
199	198	biimpar	⊢ ( ( 𝜑 ∧ 0 < ( ( ( 𝑌 − 𝑋 ) · 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 ) ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
200	197 199	syldan	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ∫ ( 𝑋 (,) 𝑌 ) ( abs ‘ ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) ) d 𝑡 < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
201	126 130 133 135 200	lelttrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) )
202	77	abscld	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ∈ ℝ )
203	131	adantr	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → 𝐸 ∈ ℝ )
204		ltdivmul	⊢ ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) ∈ ℝ ∧ 𝐸 ∈ ℝ ∧ ( ( 𝑌 − 𝑋 ) ∈ ℝ ∧ 0 < ( 𝑌 − 𝑋 ) ) ) → ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 ↔ ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ) )
205	202 203 79 82 204	syl112anc	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 ↔ ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) < ( ( 𝑌 − 𝑋 ) · 𝐸 ) ) )
206	201 205	mpbird	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( ( abs ‘ ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐹 ‘ 𝑡 ) − ( 𝐹 ‘ 𝐶 ) ) d 𝑡 ) / ( 𝑌 − 𝑋 ) ) < 𝐸 )
207	124 206	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑋 < 𝑌 ) → ( abs ‘ ( ( ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) / ( 𝑌 − 𝑋 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) < 𝐸 )