ftc2re - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ftc2re		Structured version Visualization version GIF version

Theorem ftc2re 34761

Description: The Fundamental Theorem of Calculus, part two, for functions continuous on 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2021.)

**Hypotheses**
Ref	Expression
ftc2re.e	⊢ 𝐸 = (𝐶(,)𝐷)
ftc2re.a	⊢ (𝜑 → 𝐴 ∈ 𝐸)
ftc2re.b	⊢ (𝜑 → 𝐵 ∈ 𝐸)
ftc2re.le	⊢ (𝜑 → 𝐴 ≤ 𝐵)
ftc2re.f	⊢ (𝜑 → 𝐹:𝐸⟶ℂ)
ftc2re.1	⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ))

**Assertion**
Ref	Expression
ftc2re	⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))

Distinct variable groups: 𝑡,𝐴 𝑡,𝐵 𝑡,𝐹 𝜑,𝑡 Allowed substitution hints: 𝐶(𝑡) 𝐷(𝑡) 𝐸(𝑡)

Proof of Theorem ftc2re Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ftc2re.e	. . . . . 6 ⊢ 𝐸 = (𝐶(,)𝐷)
2		ioossre 13354	. . . . . 6 ⊢ (𝐶(,)𝐷) ⊆ ℝ
3	1, 2	eqsstri 3969	. . . . 5 ⊢ 𝐸 ⊆ ℝ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
5		ftc2re.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝐸)
6	4, 5	sseldd 3923	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
7		ftc2re.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝐸)
8	4, 7	sseldd 3923	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9		ftc2re.le	. . 3 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
10		ax-resscn 11089	. . . . . . 7 ⊢ ℝ ⊆ ℂ
11	10	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℂ)
12		ftc2re.f	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐸⟶ℂ)
13		iccssre 13376	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
14	6, 8, 13	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
15		eqid 2737	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
16		tgioo4 24783	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
17	15, 16	dvres 25891	. . . . . 6 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:𝐸⟶ℂ) ∧ (𝐸 ⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
18	11, 12, 4, 14, 17	syl22anc 839	. . . . 5 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
19		iccntr 24800	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
20	6, 8, 19	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
21	20	reseq2d 5939	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)))
22	18, 21	eqtrd 2772	. . . 4 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)))
23		ioossicc 13380	. . . . . . 7 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
24	23	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
25	1, 5, 7	fct2relem 34760	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸)
26	24, 25	sstrd 3933	. . . . 5 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐸)
27		ftc2re.1	. . . . 5 ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ))
28		rescncf 24877	. . . . 5 ⊢ ((𝐴(,)𝐵) ⊆ 𝐸 → ((ℝ D 𝐹) ∈ (𝐸–cn→ℂ) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)))
29	26, 27, 28	sylc 65	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
30	22, 29	eqeltrd 2837	. . 3 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
31		ioombl 25545	. . . . . . 7 ⊢ (𝐴(,)𝐵) ∈ dom vol
32	31	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol)
33		cnmbf 25639	. . . . . 6 ⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ MblFn)
34	32, 29, 33	syl2anc 585	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ MblFn)
35		dmres 5972	. . . . . . 7 ⊢ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = ((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹))
36	35	fveq2i 6838	. . . . . 6 ⊢ (vol‘dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) = (vol‘((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹)))
37		cncff 24873	. . . . . . . . . . . 12 ⊢ ((ℝ D 𝐹) ∈ (𝐸–cn→ℂ) → (ℝ D 𝐹):𝐸⟶ℂ)
38	27, 37	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹):𝐸⟶ℂ)
39	38	fdmd 6673	. . . . . . . . . 10 ⊢ (𝜑 → dom (ℝ D 𝐹) = 𝐸)
40	39	ineq2d 4161	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹)) = ((𝐴(,)𝐵) ∩ 𝐸))
41		dfss2 3908	. . . . . . . . . 10 ⊢ ((𝐴(,)𝐵) ⊆ 𝐸 ↔ ((𝐴(,)𝐵) ∩ 𝐸) = (𝐴(,)𝐵))
42	26, 41	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴(,)𝐵) ∩ 𝐸) = (𝐴(,)𝐵))
43	40, 42	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → ((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹)) = (𝐴(,)𝐵))
44	43	fveq2d 6839	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹))) = (vol‘(𝐴(,)𝐵)))
45		volioo 25549	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
46	6, 8, 9, 45	syl3anc 1374	. . . . . . . 8 ⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
47	8, 6	resubcld 11572	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
48	46, 47	eqeltrd 2837	. . . . . . 7 ⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
49	44, 48	eqeltrd 2837	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹))) ∈ ℝ)
50	36, 49	eqeltrid 2841	. . . . 5 ⊢ (𝜑 → (vol‘dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) ∈ ℝ)
51		rescncf 24877	. . . . . . . . 9 ⊢ ((𝐴[,]𝐵) ⊆ 𝐸 → ((ℝ D 𝐹) ∈ (𝐸–cn→ℂ) → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
52	25, 51	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D 𝐹) ∈ (𝐸–cn→ℂ) → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
53	27, 52	mpd 15	. . . . . . 7 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
54		cniccbdd 25441	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥)
55	6, 8, 53, 54	syl3anc 1374	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥)
56	35, 43	eqtrid 2784	. . . . . . . . . . 11 ⊢ (𝜑 → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (𝐴(,)𝐵))
57	56, 24	eqsstrd 3957	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
58		ssralv 3991	. . . . . . . . . 10 ⊢ (dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵) → (∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥))
59	57, 58	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥))
60	59	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥))
61	57	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
62	61	sselda 3922	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → 𝑦 ∈ (𝐴[,]𝐵))
63		fvres 6854	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝐴[,]𝐵) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦))
64	62, 63	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦))
65		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)))
66	56	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (𝐴(,)𝐵))
67	65, 66	eleqtrd 2839	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → 𝑦 ∈ (𝐴(,)𝐵))
68		fvres 6854	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦))
69	67, 68	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦))
70	64, 69	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦) = (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦))
71	70	fveq2d 6839	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) = (abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)))
72	71	breq1d 5096	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → ((abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 ↔ (abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥))
73	72	biimpd 229	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → ((abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → (abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥))
74	73	ralimdva 3150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥))
75	60, 74	syld 47	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥))
76	75	reximdva 3151	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥))
77	55, 76	mpd 15	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥)
78		bddibl 25820	. . . . 5 ⊢ ((((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ MblFn ∧ (vol‘dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ 𝐿¹)
79	34, 50, 77, 78	syl3anc 1374	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ 𝐿¹)
80	22, 79	eqeltrd 2837	. . 3 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈ 𝐿¹)
81		dvcn 25901	. . . . 5 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:𝐸⟶ℂ ∧ 𝐸 ⊆ ℝ) ∧ dom (ℝ D 𝐹) = 𝐸) → 𝐹 ∈ (𝐸–cn→ℂ))
82	11, 12, 4, 39, 81	syl31anc 1376	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝐸–cn→ℂ))
83		rescncf 24877	. . . . 5 ⊢ ((𝐴[,]𝐵) ⊆ 𝐸 → (𝐹 ∈ (𝐸–cn→ℂ) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
84	25, 83	syl 17	. . . 4 ⊢ (𝜑 → (𝐹 ∈ (𝐸–cn→ℂ) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
85	82, 84	mpd 15	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
86	6, 8, 9, 30, 80, 85	ftc2 26024	. 2 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)))
87	22	fveq1d 6837	. . . . 5 ⊢ (𝜑 → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡))
88		fvres 6854	. . . . 5 ⊢ (𝑡 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
89	87, 88	sylan9eq 2792	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
90	89	ralrimiva 3130	. . 3 ⊢ (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
91		itgeq2 25758	. . 3 ⊢ (∀𝑡 ∈ (𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡) → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
92	90, 91	syl 17	. 2 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
93	6	rexrd 11189	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
94	8	rexrd 11189	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
95		ubicc2 13412	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
96	93, 94, 9, 95	syl3anc 1374	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
97	96	fvresd 6855	. . 3 ⊢ (𝜑 → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) = (𝐹‘𝐵))
98		lbicc2 13411	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
99	93, 94, 9, 98	syl3anc 1374	. . . 4 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
100	99	fvresd 6855	. . 3 ⊢ (𝜑 → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴) = (𝐹‘𝐴))
101	97, 100	oveq12d 7379	. 2 ⊢ (𝜑 → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴)))
102	86, 92, 101	3eqtr3d 2780	1 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 ∩ cin 3889 ⊆ wss 3890 class class class wbr 5086 dom cdm 5625 ran crn 5626 ↾ cres 5627 ⟶wf 6489 ‘cfv 6493 (class class class)co 7361 ℂcc 11030 ℝcr 11031 ℝ^*cxr 11172 ≤ cle 11174 − cmin 11371 (,)cioo 13292 [,]cicc 13295 abscabs 15190 TopOpenctopn 17378 topGenctg 17394 ℂ_fldccnfld 21347 intcnt 22995 –cn→ccncf 24856 volcvol 25443 MblFncmbf 25594 𝐿¹cibl 25597 ∫citg 25598 D cdv 25843

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-inf2 9556 ax-cc 10351 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109 ax-pre-sup 11110 ax-addf 11111

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-symdif 4194 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-of 7625 df-ofr 7626 df-om 7812 df-1st 7936 df-2nd 7937 df-supp 8105 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-2o 8400 df-oadd 8403 df-omul 8404 df-er 8637 df-map 8769 df-pm 8770 df-ixp 8840 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-fsupp 9269 df-fi 9318 df-sup 9349 df-inf 9350 df-oi 9419 df-dju 9819 df-card 9857 df-acn 9860 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-div 11802 df-nn 12169 df-2 12238 df-3 12239 df-4 12240 df-5 12241 df-6 12242 df-7 12243 df-8 12244 df-9 12245 df-n0 12432 df-z 12519 df-dec 12639 df-uz 12783 df-q 12893 df-rp 12937 df-xneg 13057 df-xadd 13058 df-xmul 13059 df-ioo 13296 df-ioc 13297 df-ico 13298 df-icc 13299 df-fz 13456 df-fzo 13603 df-fl 13745 df-mod 13823 df-seq 13958 df-exp 14018 df-hash 14287 df-cj 15055 df-re 15056 df-im 15057 df-sqrt 15191 df-abs 15192 df-limsup 15427 df-clim 15444 df-rlim 15445 df-sum 15643 df-struct 17111 df-sets 17128 df-slot 17146 df-ndx 17158 df-base 17174 df-ress 17195 df-plusg 17227 df-mulr 17228 df-starv 17229 df-sca 17230 df-vsca 17231 df-ip 17232 df-tset 17233 df-ple 17234 df-ds 17236 df-unif 17237 df-hom 17238 df-cco 17239 df-rest 17379 df-topn 17380 df-0g 17398 df-gsum 17399 df-topgen 17400 df-pt 17401 df-prds 17404 df-xrs 17460 df-qtop 17465 df-imas 17466 df-xps 17468 df-mre 17542 df-mrc 17543 df-acs 17545 df-mgm 18602 df-sgrp 18681 df-mnd 18697 df-submnd 18746 df-mulg 19038 df-cntz 19286 df-cmn 19751 df-psmet 21339 df-xmet 21340 df-met 21341 df-bl 21342 df-mopn 21343 df-fbas 21344 df-fg 21345 df-cnfld 21348 df-top 22872 df-topon 22889 df-topsp 22911 df-bases 22924 df-cld 22997 df-ntr 22998 df-cls 22999 df-nei 23076 df-lp 23114 df-perf 23115 df-cn 23205 df-cnp 23206 df-haus 23293 df-cmp 23365 df-tx 23540 df-hmeo 23733 df-fil 23824 df-fm 23916 df-flim 23917 df-flf 23918 df-xms 24298 df-ms 24299 df-tms 24300 df-cncf 24858 df-ovol 25444 df-vol 25445 df-mbf 25599 df-itg1 25600 df-itg2 25601 df-ibl 25602 df-itg 25603 df-0p 25650 df-limc 25846 df-dv 25847

This theorem is referenced by: fdvposlt 34762 fdvposle 34764 itgexpif 34769

W3C validator