ftc1cnnclem - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ftc1cnnclem		Structured version Visualization version GIF version

Theorem ftc1cnnclem 33815

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

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

**Assertion**
Ref	Expression
ftc1cnnclem	⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝑐))) < 𝐸)

Distinct variable groups: 𝑥,𝑦,𝑧,𝑡,𝐴 𝑥,𝐵,𝑦,𝑧,𝑡 𝑥,𝐹,𝑦,𝑧,𝑡 𝜑,𝑥,𝑦,𝑧,𝑡 𝑦,𝐺,𝑧 𝑥,𝑐,𝑦,𝑧,𝑡 𝑥,𝑋,𝑧,𝑡 𝑦,𝐸,𝑡 𝑦,𝐻 𝑥,𝑌,𝑡 𝑦,𝑅 Allowed substitution hints: 𝜑(𝑐) 𝐴(𝑐) 𝐵(𝑐) 𝑅(𝑥,𝑧,𝑡,𝑐) 𝐸(𝑥,𝑧,𝑐) 𝐹(𝑐) 𝐺(𝑥,𝑡,𝑐) 𝐻(𝑥,𝑧,𝑡,𝑐) 𝑋(𝑦,𝑐) 𝑌(𝑦,𝑧,𝑐)

**Proof of Theorem ftc1cnnclem**
Step	Hyp	Ref	Expression
1		ftc1cnnc.a	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ftc1cnnc.b	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		iccssre 12460	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
4	1, 2, 3	syl2anc 573	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
5		ftc1cnnclem.x1	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵))
6	4, 5	sseldd 3753	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ ℝ)
7		ftc1cnnclem.y1	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵))
8	4, 7	sseldd 3753	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ ℝ)
9		ltle 10332	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌))
10	6, 8, 9	syl2anc 573	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 < 𝑌 → 𝑋 ≤ 𝑌))
11	10	imp 393	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 𝑋 ≤ 𝑌)
12		ftc1cnnc.g	. . . . . . . . . . 11 ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡)
13		ftc1cnnc.le	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
14		ssid 3773	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)
15	14	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵))
16		ioossre 12440	. . . . . . . . . . . 12 ⊢ (𝐴(,)𝐵) ⊆ ℝ
17	16	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ)
18		ftc1cnnc.i	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ 𝐿¹)
19		ftc1cnnc.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ))
20		cncff 22916	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → 𝐹:(𝐴(,)𝐵)⟶ℂ)
21	19, 20	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:(𝐴(,)𝐵)⟶ℂ)
22	12, 1, 2, 13, 15, 17, 18, 21, 5, 7	ftc1lem1 24018	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡)
23	11, 22	syldan 579	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡)
24	1	rexrd 10295	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
25	2	rexrd 10295	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
26		elicc1 12424	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ^ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵)))
27	26	biimpa 462	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^) ∧ 𝑋 ∈ (𝐴[,]𝐵)) → (𝑋 ∈ ℝ^ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))
28	27	simp2d 1137	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ 𝑋 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑋)
29	24, 25, 5, 28	syl21anc 1475	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐴 ≤ 𝑋)
30		iccleub 12434	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑌 ∈ (𝐴[,]𝐵)) → 𝑌 ≤ 𝐵)
31	24, 25, 7, 30	syl3anc 1476	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ≤ 𝐵)
32		ioossioo 12471	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^*) ∧ (𝐴 ≤ 𝑋 ∧ 𝑌 ≤ 𝐵)) → (𝑋(,)𝑌) ⊆ (𝐴(,)𝐵))
33	24, 25, 29, 31, 32	syl22anc 1477	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝐴(,)𝐵))
34	33	sselda 3752	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑡 ∈ (𝐴(,)𝐵))
35	21	ffvelrnda 6504	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑡) ∈ ℂ)
36	34, 35	syldan 579	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (𝐹‘𝑡) ∈ ℂ)
37		ftc1cnnclem.c	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑐 ∈ (𝐴(,)𝐵))
38	21, 37	ffvelrnd 6505	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹‘𝑐) ∈ ℂ)
39	38	adantr 466	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (𝐹‘𝑐) ∈ ℂ)
40	36, 39	npcand 10602	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (((𝐹‘𝑡) − (𝐹‘𝑐)) + (𝐹‘𝑐)) = (𝐹‘𝑡))
41	40	itgeq2dv 23768	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(((𝐹‘𝑡) − (𝐹‘𝑐)) + (𝐹‘𝑐)) d𝑡 = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡)
42	36, 39	subcld 10598	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → ((𝐹‘𝑡) − (𝐹‘𝑐)) ∈ ℂ)
43		ioombl 23553	. . . . . . . . . . . . . . 15 ⊢ (𝑋(,)𝑌) ∈ dom vol
44	43	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol)
45		fvexd 6346	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑡) ∈ V)
46	21	feqmptd 6393	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑡)))
47	46, 18	eqeltrrd 2851	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑡)) ∈ 𝐿¹)
48	33, 44, 45, 47	iblss 23791	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑡)) ∈ 𝐿¹)
49		fconstmpt 5302	. . . . . . . . . . . . . 14 ⊢ ((𝑋(,)𝑌) × {(𝐹‘𝑐)}) = (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑐))
50		mblvol 23518	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋(,)𝑌) ∈ dom vol → (vol‘(𝑋(,)𝑌)) = (vol*‘(𝑋(,)𝑌)))
51	43, 50	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (vol‘(𝑋(,)𝑌)) = (vol*‘(𝑋(,)𝑌))
52		ioossicc 12464	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌)
53	52	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝑋[,]𝑌))
54		iccmbl 23554	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ∈ dom vol)
55	6, 8, 54	syl2anc 573	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋[,]𝑌) ∈ dom vol)
56		mblss 23519	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑋[,]𝑌) ∈ dom vol → (𝑋[,]𝑌) ⊆ ℝ)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
58		mblvol 23518	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋[,]𝑌) ∈ dom vol → (vol‘(𝑋[,]𝑌)) = (vol*‘(𝑋[,]𝑌)))
59	55, 58	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (vol‘(𝑋[,]𝑌)) = (vol*‘(𝑋[,]𝑌)))
60		iccvolcl 23555	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (vol‘(𝑋[,]𝑌)) ∈ ℝ)
61	6, 8, 60	syl2anc 573	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (vol‘(𝑋[,]𝑌)) ∈ ℝ)
62	59, 61	eqeltrrd 2851	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (vol*‘(𝑋[,]𝑌)) ∈ ℝ)
63		ovolsscl 23474	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋(,)𝑌) ⊆ (𝑋[,]𝑌) ∧ (𝑋[,]𝑌) ⊆ ℝ ∧ (vol‘(𝑋[,]𝑌)) ∈ ℝ) → (vol‘(𝑋(,)𝑌)) ∈ ℝ)
64	53, 57, 62, 63	syl3anc 1476	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (vol*‘(𝑋(,)𝑌)) ∈ ℝ)
65	51, 64	syl5eqel 2854	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (vol‘(𝑋(,)𝑌)) ∈ ℝ)
66		iblconst 23804	. . . . . . . . . . . . . . 15 ⊢ (((𝑋(,)𝑌) ∈ dom vol ∧ (vol‘(𝑋(,)𝑌)) ∈ ℝ ∧ (𝐹‘𝑐) ∈ ℂ) → ((𝑋(,)𝑌) × {(𝐹‘𝑐)}) ∈ 𝐿¹)
67	44, 65, 38, 66	syl3anc 1476	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋(,)𝑌) × {(𝐹‘𝑐)}) ∈ 𝐿¹)
68	49, 67	syl5eqelr 2855	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑐)) ∈ 𝐿¹)
69		eqid 2771	. . . . . . . . . . . . . . 15 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
70	69	subcn 22889	. . . . . . . . . . . . . . . 16 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
71	70	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
72	21, 33	feqresmpt 6394	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) = (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑡)))
73		rescncf 22920	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑋(,)𝑌) ⊆ (𝐴(,)𝐵) → (𝐹 ∈ ((𝐴(,)𝐵)–cn→ℂ) → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ)))
74	33, 19, 73	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
75	72, 74	eqeltrrd 2851	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑡)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
76		ioossre 12440	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋(,)𝑌) ⊆ ℝ
77		ax-resscn 10199	. . . . . . . . . . . . . . . . . 18 ⊢ ℝ ⊆ ℂ
78	76, 77	sstri 3761	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋(,)𝑌) ⊆ ℂ
79		ssid 3773	. . . . . . . . . . . . . . . . 17 ⊢ ℂ ⊆ ℂ
80		cncfmptc 22934	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑐) ∈ ℂ ∧ (𝑋(,)𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑐)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
81	78, 79, 80	mp3an23 1564	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑐) ∈ ℂ → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑐)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
82	38, 81	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑐)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
83	69, 71, 75, 82	cncfmpt2f 22937	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ ((𝐹‘𝑡) − (𝐹‘𝑐))) ∈ ((𝑋(,)𝑌)–cn→ℂ))
84		cnmbf 23646	. . . . . . . . . . . . . 14 ⊢ (((𝑋(,)𝑌) ∈ dom vol ∧ (𝑡 ∈ (𝑋(,)𝑌) ↦ ((𝐹‘𝑡) − (𝐹‘𝑐))) ∈ ((𝑋(,)𝑌)–cn→ℂ)) → (𝑡 ∈ (𝑋(,)𝑌) ↦ ((𝐹‘𝑡) − (𝐹‘𝑐))) ∈ MblFn)
85	43, 83, 84	sylancr 575	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ ((𝐹‘𝑡) − (𝐹‘𝑐))) ∈ MblFn)
86	36, 48, 39, 68, 85	iblsubnc 33803	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ ((𝐹‘𝑡) − (𝐹‘𝑐))) ∈ 𝐿¹)
87	40	mpteq2dva 4879	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (((𝐹‘𝑡) − (𝐹‘𝑐)) + (𝐹‘𝑐))) = (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑡)))
88	87, 72	eqtr4d 2808	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (((𝐹‘𝑡) − (𝐹‘𝑐)) + (𝐹‘𝑐))) = (𝐹 ↾ (𝑋(,)𝑌)))
89		iblmbf 23754	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ 𝐿¹ → 𝐹 ∈ MblFn)
90	18, 89	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ MblFn)
91		mbfres 23631	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ MblFn ∧ (𝑋(,)𝑌) ∈ dom vol) → (𝐹 ↾ (𝑋(,)𝑌)) ∈ MblFn)
92	90, 43, 91	sylancl 574	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾ (𝑋(,)𝑌)) ∈ MblFn)
93	88, 92	eqeltrd 2850	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (((𝐹‘𝑡) − (𝐹‘𝑐)) + (𝐹‘𝑐))) ∈ MblFn)
94	42, 86, 39, 68, 93	itgaddnc 33802	. . . . . . . . . . 11 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(((𝐹‘𝑡) − (𝐹‘𝑐)) + (𝐹‘𝑐)) d𝑡 = (∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 + ∫(𝑋(,)𝑌)(𝐹‘𝑐) d𝑡))
95	41, 94	eqtr3d 2807	. . . . . . . . . 10 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡 = (∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 + ∫(𝑋(,)𝑌)(𝐹‘𝑐) d𝑡))
96	95	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡 = (∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 + ∫(𝑋(,)𝑌)(𝐹‘𝑐) d𝑡))
97		itgconst 23805	. . . . . . . . . . . . 13 ⊢ (((𝑋(,)𝑌) ∈ dom vol ∧ (vol‘(𝑋(,)𝑌)) ∈ ℝ ∧ (𝐹‘𝑐) ∈ ℂ) → ∫(𝑋(,)𝑌)(𝐹‘𝑐) d𝑡 = ((𝐹‘𝑐) · (vol‘(𝑋(,)𝑌))))
98	44, 65, 38, 97	syl3anc 1476	. . . . . . . . . . . 12 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐹‘𝑐) d𝑡 = ((𝐹‘𝑐) · (vol‘(𝑋(,)𝑌))))
99	98	adantr 466	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ∫(𝑋(,)𝑌)(𝐹‘𝑐) d𝑡 = ((𝐹‘𝑐) · (vol‘(𝑋(,)𝑌))))
100	6	adantr 466	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 𝑋 ∈ ℝ)
101	8	adantr 466	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 𝑌 ∈ ℝ)
102		ovolioo 23556	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ∧ 𝑋 ≤ 𝑌) → (vol*‘(𝑋(,)𝑌)) = (𝑌 − 𝑋))
103	100, 101, 11, 102	syl3anc 1476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (vol*‘(𝑋(,)𝑌)) = (𝑌 − 𝑋))
104	51, 103	syl5eq 2817	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (vol‘(𝑋(,)𝑌)) = (𝑌 − 𝑋))
105	104	oveq2d 6812	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((𝐹‘𝑐) · (vol‘(𝑋(,)𝑌))) = ((𝐹‘𝑐) · (𝑌 − 𝑋)))
106	99, 105	eqtrd 2805	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ∫(𝑋(,)𝑌)(𝐹‘𝑐) d𝑡 = ((𝐹‘𝑐) · (𝑌 − 𝑋)))
107	106	oveq2d 6812	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 + ∫(𝑋(,)𝑌)(𝐹‘𝑐) d𝑡) = (∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 + ((𝐹‘𝑐) · (𝑌 − 𝑋))))
108	23, 96, 107	3eqtrd 2809	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = (∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 + ((𝐹‘𝑐) · (𝑌 − 𝑋))))
109	108	oveq1d 6811	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) = ((∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 + ((𝐹‘𝑐) · (𝑌 − 𝑋))) / (𝑌 − 𝑋)))
110		ovexd 6829	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → ((𝐹‘𝑡) − (𝐹‘𝑐)) ∈ V)
111	110, 86	itgcl 23770	. . . . . . . . 9 ⊢ (𝜑 → ∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 ∈ ℂ)
112	111	adantr 466	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 ∈ ℂ)
113	38	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (𝐹‘𝑐) ∈ ℂ)
114	8, 6	resubcld 10664	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℝ)
115	114	recnd 10274	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℂ)
116	115	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (𝑌 − 𝑋) ∈ ℂ)
117	113, 116	mulcld 10266	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((𝐹‘𝑐) · (𝑌 − 𝑋)) ∈ ℂ)
118	6, 8	posdifd 10820	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 < 𝑌 ↔ 0 < (𝑌 − 𝑋)))
119	118	biimpa 462	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 0 < (𝑌 − 𝑋))
120	119	gt0ne0d 10798	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (𝑌 − 𝑋) ≠ 0)
121	112, 117, 116, 120	divdird 11045	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 + ((𝐹‘𝑐) · (𝑌 − 𝑋))) / (𝑌 − 𝑋)) = ((∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋)) + (((𝐹‘𝑐) · (𝑌 − 𝑋)) / (𝑌 − 𝑋))))
122	113, 116, 120	divcan4d 11013	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (((𝐹‘𝑐) · (𝑌 − 𝑋)) / (𝑌 − 𝑋)) = (𝐹‘𝑐))
123	122	oveq2d 6812	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋)) + (((𝐹‘𝑐) · (𝑌 − 𝑋)) / (𝑌 − 𝑋))) = ((∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋)) + (𝐹‘𝑐)))
124	109, 121, 123	3eqtrd 2809	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) = ((∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋)) + (𝐹‘𝑐)))
125	124	oveq1d 6811	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝑐)) = (((∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋)) + (𝐹‘𝑐)) − (𝐹‘𝑐)))
126	112, 116, 120	divcld 11007	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋)) ∈ ℂ)
127	126, 113	pncand 10599	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (((∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋)) + (𝐹‘𝑐)) − (𝐹‘𝑐)) = (∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋)))
128	125, 127	eqtrd 2805	. . . 4 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝑐)) = (∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋)))
129	128	fveq2d 6337	. . 3 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝑐))) = (abs‘(∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋))))
130	112, 116, 120	absdivd 14402	. . 3 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘(∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡 / (𝑌 − 𝑋))) = ((abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) / (abs‘(𝑌 − 𝑋))))
131	114	adantr 466	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (𝑌 − 𝑋) ∈ ℝ)
132		0re 10246	. . . . . . 7 ⊢ 0 ∈ ℝ
133		ltle 10332	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ (𝑌 − 𝑋) ∈ ℝ) → (0 < (𝑌 − 𝑋) → 0 ≤ (𝑌 − 𝑋)))
134	132, 131, 133	sylancr 575	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (0 < (𝑌 − 𝑋) → 0 ≤ (𝑌 − 𝑋)))
135	119, 134	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 0 ≤ (𝑌 − 𝑋))
136	131, 135	absidd 14369	. . . 4 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘(𝑌 − 𝑋)) = (𝑌 − 𝑋))
137	136	oveq2d 6812	. . 3 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) / (abs‘(𝑌 − 𝑋))) = ((abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) / (𝑌 − 𝑋)))
138	129, 130, 137	3eqtrd 2809	. 2 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝑐))) = ((abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) / (𝑌 − 𝑋)))
139	112	abscld 14383	. . . 4 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) ∈ ℝ)
140	42	abscld 14383	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) ∈ ℝ)
141		cncfss 22922	. . . . . . . . . . . 12 ⊢ ((ℝ ⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ))
142	77, 79, 141	mp2an 672	. . . . . . . . . . 11 ⊢ (ℂ–cn→ℝ) ⊆ (ℂ–cn→ℂ)
143		abscncf 22924	. . . . . . . . . . 11 ⊢ abs ∈ (ℂ–cn→ℝ)
144	142, 143	sselii 3749	. . . . . . . . . 10 ⊢ abs ∈ (ℂ–cn→ℂ)
145	144	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → abs ∈ (ℂ–cn→ℂ))
146	145, 83	cncfmpt1f 22936	. . . . . . . 8 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ ((𝑋(,)𝑌)–cn→ℂ))
147		cnmbf 23646	. . . . . . . 8 ⊢ (((𝑋(,)𝑌) ∈ dom vol ∧ (𝑡 ∈ (𝑋(,)𝑌) ↦ (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ ((𝑋(,)𝑌)–cn→ℂ)) → (𝑡 ∈ (𝑋(,)𝑌) ↦ (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ MblFn)
148	43, 146, 147	sylancr 575	. . . . . . 7 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ MblFn)
149	110, 86, 148	iblabsnc 33806	. . . . . 6 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ 𝐿¹)
150	140, 149	itgrecl 23784	. . . . 5 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡 ∈ ℝ)
151	150	adantr 466	. . . 4 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡 ∈ ℝ)
152		ftc1cnnclem.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
153	152	rpred 12075	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ)
154	114, 153	remulcld 10276	. . . . 5 ⊢ (𝜑 → ((𝑌 − 𝑋) · 𝐸) ∈ ℝ)
155	154	adantr 466	. . . 4 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((𝑌 − 𝑋) · 𝐸) ∈ ℝ)
156	111	cjcld 14144	. . . . . . . . 9 ⊢ (𝜑 → (∗‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) ∈ ℂ)
157		cncfmptc 22934	. . . . . . . . . 10 ⊢ (((∗‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) ∈ ℂ ∧ (𝑋(,)𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝑋(,)𝑌) ↦ (∗‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
158	78, 79, 157	mp3an23 1564	. . . . . . . . 9 ⊢ ((∗‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) ∈ ℂ → (𝑥 ∈ (𝑋(,)𝑌) ↦ (∗‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
159	156, 158	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ (∗‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡)) ∈ ((𝑋(,)𝑌)–cn→ℂ))
160		nfcv 2913	. . . . . . . . . 10 ⊢ Ⅎ𝑥((𝐹‘𝑡) − (𝐹‘𝑐))
161		nfcsb1v 3698	. . . . . . . . . 10 ⊢ Ⅎ𝑡⦋𝑥 / 𝑡⦌((𝐹‘𝑡) − (𝐹‘𝑐))
162		csbeq1a 3691	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → ((𝐹‘𝑡) − (𝐹‘𝑐)) = ⦋𝑥 / 𝑡⦌((𝐹‘𝑡) − (𝐹‘𝑐)))
163	160, 161, 162	cbvmpt 4884	. . . . . . . . 9 ⊢ (𝑡 ∈ (𝑋(,)𝑌) ↦ ((𝐹‘𝑡) − (𝐹‘𝑐))) = (𝑥 ∈ (𝑋(,)𝑌) ↦ ⦋𝑥 / 𝑡⦌((𝐹‘𝑡) − (𝐹‘𝑐)))
164	163, 83	syl5eqelr 2855	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ ⦋𝑥 / 𝑡⦌((𝐹‘𝑡) − (𝐹‘𝑐))) ∈ ((𝑋(,)𝑌)–cn→ℂ))
165	159, 164	mulcncf 23434	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ ((∗‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) · ⦋𝑥 / 𝑡⦌((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ ((𝑋(,)𝑌)–cn→ℂ))
166		cnmbf 23646	. . . . . . 7 ⊢ (((𝑋(,)𝑌) ∈ dom vol ∧ (𝑥 ∈ (𝑋(,)𝑌) ↦ ((∗‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) · ⦋𝑥 / 𝑡⦌((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ ((𝑋(,)𝑌)–cn→ℂ)) → (𝑥 ∈ (𝑋(,)𝑌) ↦ ((∗‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) · ⦋𝑥 / 𝑡⦌((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ MblFn)
167	43, 165, 166	sylancr 575	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ ((∗‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) · ⦋𝑥 / 𝑡⦌((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ MblFn)
168	42, 86, 148, 167	itgabsnc 33811	. . . . 5 ⊢ (𝜑 → (abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) ≤ ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡)
169	168	adantr 466	. . . 4 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) ≤ ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡)
170		simpr 471	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 𝑋 < 𝑌)
171	153	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝐸 ∈ ℝ)
172		fconstmpt 5302	. . . . . . . . . 10 ⊢ ((𝑋(,)𝑌) × {𝐸}) = (𝑡 ∈ (𝑋(,)𝑌) ↦ 𝐸)
173	152	rpcnd 12077	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℂ)
174		iblconst 23804	. . . . . . . . . . 11 ⊢ (((𝑋(,)𝑌) ∈ dom vol ∧ (vol‘(𝑋(,)𝑌)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ((𝑋(,)𝑌) × {𝐸}) ∈ 𝐿¹)
175	44, 65, 173, 174	syl3anc 1476	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑋(,)𝑌) × {𝐸}) ∈ 𝐿¹)
176	172, 175	syl5eqelr 2855	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ 𝐿¹)
177		cncfmptc 22934	. . . . . . . . . . . . 13 ⊢ ((𝐸 ∈ ℂ ∧ (𝑋(,)𝑌) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑡 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ))
178	78, 79, 177	mp3an23 1564	. . . . . . . . . . . 12 ⊢ (𝐸 ∈ ℂ → (𝑡 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ))
179	173, 178	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ 𝐸) ∈ ((𝑋(,)𝑌)–cn→ℂ))
180	69, 71, 179, 146	cncfmpt2f 22937	. . . . . . . . . 10 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))))) ∈ ((𝑋(,)𝑌)–cn→ℂ))
181		cnmbf 23646	. . . . . . . . . 10 ⊢ (((𝑋(,)𝑌) ∈ dom vol ∧ (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))))) ∈ ((𝑋(,)𝑌)–cn→ℂ)) → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))))) ∈ MblFn)
182	43, 180, 181	sylancr 575	. . . . . . . . 9 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))))) ∈ MblFn)
183	171, 176, 140, 149, 182	iblsubnc 33803	. . . . . . . 8 ⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))))) ∈ 𝐿¹)
184	183	adantr 466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))))) ∈ 𝐿¹)
185		ftc1cnnclem.fc	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴(,)𝐵)) → ((abs‘(𝑦 − 𝑐)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝐸))
186	185	ralrimiva 3115	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑦 ∈ (𝐴(,)𝐵)((abs‘(𝑦 − 𝑐)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝐸))
187	186	adantr 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → ∀𝑦 ∈ (𝐴(,)𝐵)((abs‘(𝑦 − 𝑐)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝐸))
188	16, 37	sseldi 3750	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑐 ∈ ℝ)
189		ftc1cnnclem.r	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 ∈ ℝ⁺)
190	189	rpred 12075	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ ℝ)
191	188, 190	resubcld 10664	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑐 − 𝑅) ∈ ℝ)
192	191	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (𝑐 − 𝑅) ∈ ℝ)
193	6	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑋 ∈ ℝ)
194		elioore 12410	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (𝑋(,)𝑌) → 𝑡 ∈ ℝ)
195	194	adantl 467	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑡 ∈ ℝ)
196		ftc1cnnclem.x2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝑋 − 𝑐)) < 𝑅)
197	6, 188, 190	absdifltd 14380	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘(𝑋 − 𝑐)) < 𝑅 ↔ ((𝑐 − 𝑅) < 𝑋 ∧ 𝑋 < (𝑐 + 𝑅))))
198	196, 197	mpbid 222	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑐 − 𝑅) < 𝑋 ∧ 𝑋 < (𝑐 + 𝑅)))
199	198	simpld 482	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑐 − 𝑅) < 𝑋)
200	199	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (𝑐 − 𝑅) < 𝑋)
201		eliooord 12438	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ (𝑋(,)𝑌) → (𝑋 < 𝑡 ∧ 𝑡 < 𝑌))
202	201	adantl 467	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (𝑋 < 𝑡 ∧ 𝑡 < 𝑌))
203	202	simpld 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑋 < 𝑡)
204	192, 193, 195, 200, 203	lttrd 10404	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (𝑐 − 𝑅) < 𝑡)
205	8	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑌 ∈ ℝ)
206	188, 190	readdcld 10275	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑐 + 𝑅) ∈ ℝ)
207	206	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (𝑐 + 𝑅) ∈ ℝ)
208	202	simprd 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑡 < 𝑌)
209		ftc1cnnclem.y2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (abs‘(𝑌 − 𝑐)) < 𝑅)
210	8, 188, 190	absdifltd 14380	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘(𝑌 − 𝑐)) < 𝑅 ↔ ((𝑐 − 𝑅) < 𝑌 ∧ 𝑌 < (𝑐 + 𝑅))))
211	209, 210	mpbid 222	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑐 − 𝑅) < 𝑌 ∧ 𝑌 < (𝑐 + 𝑅)))
212	211	simprd 483	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 < (𝑐 + 𝑅))
213	212	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑌 < (𝑐 + 𝑅))
214	195, 205, 207, 208, 213	lttrd 10404	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑡 < (𝑐 + 𝑅))
215	188	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑐 ∈ ℝ)
216	190	adantr 466	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑅 ∈ ℝ)
217	195, 215, 216	absdifltd 14380	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → ((abs‘(𝑡 − 𝑐)) < 𝑅 ↔ ((𝑐 − 𝑅) < 𝑡 ∧ 𝑡 < (𝑐 + 𝑅))))
218	204, 214, 217	mpbir2and 692	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (abs‘(𝑡 − 𝑐)) < 𝑅)
219		fvoveq1 6819	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑡 → (abs‘(𝑦 − 𝑐)) = (abs‘(𝑡 − 𝑐)))
220	219	breq1d 4797	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑡 → ((abs‘(𝑦 − 𝑐)) < 𝑅 ↔ (abs‘(𝑡 − 𝑐)) < 𝑅))
221		fveq2 6333	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑡 → (𝐹‘𝑦) = (𝐹‘𝑡))
222	221	fvoveq1d 6818	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑡 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) = (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))))
223	222	breq1d 4797	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑡 → ((abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝐸 ↔ (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) < 𝐸))
224	220, 223	imbi12d 333	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑡 → (((abs‘(𝑦 − 𝑐)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝐸) ↔ ((abs‘(𝑡 − 𝑐)) < 𝑅 → (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) < 𝐸)))
225	224	rspcv 3456	. . . . . . . . . 10 ⊢ (𝑡 ∈ (𝐴(,)𝐵) → (∀𝑦 ∈ (𝐴(,)𝐵)((abs‘(𝑦 − 𝑐)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝑐))) < 𝐸) → ((abs‘(𝑡 − 𝑐)) < 𝑅 → (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) < 𝐸)))
226	34, 187, 218, 225	syl3c 66	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) < 𝐸)
227		difrp 12071	. . . . . . . . . 10 ⊢ (((abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) < 𝐸 ↔ (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ ℝ⁺))
228	140, 171, 227	syl2anc 573	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → ((abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) < 𝐸 ↔ (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ ℝ⁺))
229	226, 228	mpbid 222	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ ℝ⁺)
230	229	adantlr 694	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑋 < 𝑌) ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) ∈ ℝ⁺)
231	180	adantr 466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐))))) ∈ ((𝑋(,)𝑌)–cn→ℂ))
232	170, 184, 230, 231	itggt0cn 33814	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 0 < ∫(𝑋(,)𝑌)(𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) d𝑡)
233	171, 176, 140, 149, 182	itgsubnc 33804	. . . . . . . 8 ⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) d𝑡 = (∫(𝑋(,)𝑌)𝐸 d𝑡 − ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡))
234	233	adantr 466	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ∫(𝑋(,)𝑌)(𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) d𝑡 = (∫(𝑋(,)𝑌)𝐸 d𝑡 − ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡))
235		itgconst 23805	. . . . . . . . . . 11 ⊢ (((𝑋(,)𝑌) ∈ dom vol ∧ (vol‘(𝑋(,)𝑌)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝑋(,)𝑌)𝐸 d𝑡 = (𝐸 · (vol‘(𝑋(,)𝑌))))
236	44, 65, 173, 235	syl3anc 1476	. . . . . . . . . 10 ⊢ (𝜑 → ∫(𝑋(,)𝑌)𝐸 d𝑡 = (𝐸 · (vol‘(𝑋(,)𝑌))))
237	236	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ∫(𝑋(,)𝑌)𝐸 d𝑡 = (𝐸 · (vol‘(𝑋(,)𝑌))))
238	104	oveq2d 6812	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (𝐸 · (vol‘(𝑋(,)𝑌))) = (𝐸 · (𝑌 − 𝑋)))
239	173, 115	mulcomd 10267	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · (𝑌 − 𝑋)) = ((𝑌 − 𝑋) · 𝐸))
240	239	adantr 466	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (𝐸 · (𝑌 − 𝑋)) = ((𝑌 − 𝑋) · 𝐸))
241	237, 238, 240	3eqtrd 2809	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ∫(𝑋(,)𝑌)𝐸 d𝑡 = ((𝑌 − 𝑋) · 𝐸))
242	241	oveq1d 6811	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (∫(𝑋(,)𝑌)𝐸 d𝑡 − ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡) = (((𝑌 − 𝑋) · 𝐸) − ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡))
243	234, 242	eqtrd 2805	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ∫(𝑋(,)𝑌)(𝐸 − (abs‘((𝐹‘𝑡) − (𝐹‘𝑐)))) d𝑡 = (((𝑌 − 𝑋) · 𝐸) − ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡))
244	232, 243	breqtrd 4813	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 0 < (((𝑌 − 𝑋) · 𝐸) − ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡))
245	150, 154	posdifd 10820	. . . . . 6 ⊢ (𝜑 → (∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡 < ((𝑌 − 𝑋) · 𝐸) ↔ 0 < (((𝑌 − 𝑋) · 𝐸) − ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡)))
246	245	biimpar 463	. . . . 5 ⊢ ((𝜑 ∧ 0 < (((𝑌 − 𝑋) · 𝐸) − ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡)) → ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡 < ((𝑌 − 𝑋) · 𝐸))
247	244, 246	syldan 579	. . . 4 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ∫(𝑋(,)𝑌)(abs‘((𝐹‘𝑡) − (𝐹‘𝑐))) d𝑡 < ((𝑌 − 𝑋) · 𝐸))
248	139, 151, 155, 169, 247	lelttrd 10401	. . 3 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) < ((𝑌 − 𝑋) · 𝐸))
249	153	adantr 466	. . . 4 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → 𝐸 ∈ ℝ)
250		ltdivmul 11104	. . . 4 ⊢ (((abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) ∈ ℝ ∧ 𝐸 ∈ ℝ ∧ ((𝑌 − 𝑋) ∈ ℝ ∧ 0 < (𝑌 − 𝑋))) → (((abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) / (𝑌 − 𝑋)) < 𝐸 ↔ (abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) < ((𝑌 − 𝑋) · 𝐸)))
251	139, 249, 131, 119, 250	syl112anc 1480	. . 3 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (((abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) / (𝑌 − 𝑋)) < 𝐸 ↔ (abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) < ((𝑌 − 𝑋) · 𝐸)))
252	248, 251	mpbird 247	. 2 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → ((abs‘∫(𝑋(,)𝑌)((𝐹‘𝑡) − (𝐹‘𝑐)) d𝑡) / (𝑌 − 𝑋)) < 𝐸)
253	138, 252	eqbrtrd 4809	1 ⊢ ((𝜑 ∧ 𝑋 < 𝑌) → (abs‘((((𝐺‘𝑌) − (𝐺‘𝑋)) / (𝑌 − 𝑋)) − (𝐹‘𝑐))) < 𝐸)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 ∧ w3a 1071 = wceq 1631 ∈ wcel 2145 ∀wral 3061 Vcvv 3351 ⦋csb 3682 ∖ cdif 3720 ⊆ wss 3723 {csn 4317 class class class wbr 4787 ↦ cmpt 4864 × cxp 5248 dom cdm 5250 ↾ cres 5252 ⟶wf 6026 ‘cfv 6030 (class class class)co 6796 ℂcc 10140 ℝcr 10141 0cc0 10142 + caddc 10145 · cmul 10147 ℝ^*cxr 10279 < clt 10280 ≤ cle 10281 − cmin 10472 / cdiv 10890 ℝ⁺crp 12035 (,)cioo 12380 [,]cicc 12383 ∗ccj 14044 abscabs 14182 TopOpenctopn 16290 ℂ_fldccnfld 19961 Cn ccn 21249 ×_t ctx 21584 –cn→ccncf 22899 vol*covol 23450 volcvol 23451 MblFncmbf 23602 𝐿¹cibl 23605 ∫citg 23606

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4905 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7100 ax-inf2 8706 ax-cnex 10198 ax-resscn 10199 ax-1cn 10200 ax-icn 10201 ax-addcl 10202 ax-addrcl 10203 ax-mulcl 10204 ax-mulrcl 10205 ax-mulcom 10206 ax-addass 10207 ax-mulass 10208 ax-distr 10209 ax-i2m1 10210 ax-1ne0 10211 ax-1rid 10212 ax-rnegex 10213 ax-rrecex 10214 ax-cnre 10215 ax-pre-lttri 10216 ax-pre-lttrn 10217 ax-pre-ltadd 10218 ax-pre-mulgt0 10219 ax-pre-sup 10220 ax-addf 10221 ax-mulf 10222

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-fal 1637 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4576 df-int 4613 df-iun 4657 df-iin 4658 df-disj 4756 df-br 4788 df-opab 4848 df-mpt 4865 df-tr 4888 df-id 5158 df-eprel 5163 df-po 5171 df-so 5172 df-fr 5209 df-se 5210 df-we 5211 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-pred 5822 df-ord 5868 df-on 5869 df-lim 5870 df-suc 5871 df-iota 5993 df-fun 6032 df-fn 6033 df-f 6034 df-f1 6035 df-fo 6036 df-f1o 6037 df-fv 6038 df-isom 6039 df-riota 6757 df-ov 6799 df-oprab 6800 df-mpt2 6801 df-of 7048 df-ofr 7049 df-om 7217 df-1st 7319 df-2nd 7320 df-supp 7451 df-wrecs 7563 df-recs 7625 df-rdg 7663 df-1o 7717 df-2o 7718 df-oadd 7721 df-omul 7722 df-er 7900 df-map 8015 df-pm 8016 df-ixp 8067 df-en 8114 df-dom 8115 df-sdom 8116 df-fin 8117 df-fsupp 8436 df-fi 8477 df-sup 8508 df-inf 8509 df-oi 8575 df-card 8969 df-acn 8972 df-cda 9196 df-pnf 10282 df-mnf 10283 df-xr 10284 df-ltxr 10285 df-le 10286 df-sub 10474 df-neg 10475 df-div 10891 df-nn 11227 df-2 11285 df-3 11286 df-4 11287 df-5 11288 df-6 11289 df-7 11290 df-8 11291 df-9 11292 df-n0 11500 df-z 11585 df-dec 11701 df-uz 11894 df-q 11997 df-rp 12036 df-xneg 12151 df-xadd 12152 df-xmul 12153 df-ioo 12384 df-ico 12386 df-icc 12387 df-fz 12534 df-fzo 12674 df-fl 12801 df-mod 12877 df-seq 13009 df-exp 13068 df-hash 13322 df-cj 14047 df-re 14048 df-im 14049 df-sqrt 14183 df-abs 14184 df-clim 14427 df-rlim 14428 df-sum 14625 df-struct 16066 df-ndx 16067 df-slot 16068 df-base 16070 df-sets 16071 df-ress 16072 df-plusg 16162 df-mulr 16163 df-starv 16164 df-sca 16165 df-vsca 16166 df-ip 16167 df-tset 16168 df-ple 16169 df-ds 16172 df-unif 16173 df-hom 16174 df-cco 16175 df-rest 16291 df-topn 16292 df-0g 16310 df-gsum 16311 df-topgen 16312 df-pt 16313 df-prds 16316 df-xrs 16370 df-qtop 16375 df-imas 16376 df-xps 16378 df-mre 16454 df-mrc 16455 df-acs 16457 df-mgm 17450 df-sgrp 17492 df-mnd 17503 df-submnd 17544 df-mulg 17749 df-cntz 17957 df-cmn 18402 df-psmet 19953 df-xmet 19954 df-met 19955 df-bl 19956 df-mopn 19957 df-cnfld 19962 df-top 20919 df-topon 20936 df-topsp 20958 df-bases 20971 df-cn 21252 df-cnp 21253 df-cmp 21411 df-tx 21586 df-hmeo 21779 df-xms 22345 df-ms 22346 df-tms 22347 df-cncf 22901 df-ovol 23452 df-vol 23453 df-mbf 23607 df-itg1 23608 df-itg2 23609 df-ibl 23610 df-itg 23611 df-0p 23657

This theorem is referenced by: ftc1cnnc 33816

W3C validator