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 35338

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 13578	. . . . . 6 ⊢ (𝐶(,)𝐷) ⊆ ℝ
3	1, 2	eqsstri 3959	. . . . 5 ⊢ 𝐸 ⊆ ℝ
4	3	a1i 11	. . . 4 ⊢ (𝜑 → 𝐸 ⊆ ℝ)
5		ftc2re.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝐸)
6	4, 5	sseldd 3914	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
7		ftc2re.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝐸)
8	4, 7	sseldd 3914	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
9		ftc2re.le	. . 3 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
10		ax-resscn 11296	. . . . . . 7 ⊢ ℝ ⊆ ℂ
11	10	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ ⊆ ℂ)
12		ftc2re.f	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐸⟶ℂ)
13		iccssre 13600	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
14	6, 8, 13	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
15		eqid 2763	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
16		tgioo4 25179	. . . . . . 7 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
17	15, 16	dvres 26286	. . . . . 6 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:𝐸⟶ℂ) ∧ (𝐸 ⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
18	11, 12, 4, 14, 17	syl22anc 852	. . . . 5 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
19		iccntr 25196	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
20	6, 8, 19	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
21	20	reseq2d 5986	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)))
22	18, 21	eqtrd 2798	. . . 4 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)))
23		ioossicc 13604	. . . . . . 7 ⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)
24	23	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵))
25	1, 5, 7	fct2relem 35337	. . . . . 6 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸)
26	24, 25	sstrd 3923	. . . . 5 ⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐸)
27		ftc2re.1	. . . . 5 ⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ))
28		rescncf 25273	. . . . 5 ⊢ ((𝐴(,)𝐵) ⊆ 𝐸 → ((ℝ D 𝐹) ∈ (𝐸–cn→ℂ) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)))
29	26, 27, 28	sylc 66	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
30	22, 29	eqeltrd 2864	. . 3 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
31		ioombl 25941	. . . . . . 7 ⊢ (𝐴(,)𝐵) ∈ dom vol
32	31	a1i 11	. . . . . 6 ⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol)
33		cnmbf 26035	. . . . . 6 ⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ MblFn)
34	32, 29, 33	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ MblFn)
35		dmres 6020	. . . . . . 7 ⊢ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = ((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹))
36	35	fveq2i 6919	. . . . . 6 ⊢ (vol‘dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) = (vol‘((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹)))
37		cncff 25269	. . . . . . . . . . . 12 ⊢ ((ℝ D 𝐹) ∈ (𝐸–cn→ℂ) → (ℝ D 𝐹):𝐸⟶ℂ)
38	27, 37	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (ℝ D 𝐹):𝐸⟶ℂ)
39	38	fdmd 6750	. . . . . . . . . 10 ⊢ (𝜑 → dom (ℝ D 𝐹) = 𝐸)
40	39	ineq2d 4120	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹)) = ((𝐴(,)𝐵) ∩ 𝐸))
41		dfss2 4097	. . . . . . . . . 10 ⊢ ((𝐴(,)𝐵) ⊆ 𝐸 ↔ ((𝐴(,)𝐵) ∩ 𝐸) = (𝐴(,)𝐵))
42	26, 41	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴(,)𝐵) ∩ 𝐸) = (𝐴(,)𝐵))
43	40, 42	eqtrd 2798	. . . . . . . 8 ⊢ (𝜑 → ((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹)) = (𝐴(,)𝐵))
44	43	fveq2d 6920	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹))) = (vol‘(𝐴(,)𝐵)))
45		volioo 25945	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
46	6, 8, 9, 45	syl3anc 1399	. . . . . . . 8 ⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴))
47	8, 6	resubcld 11783	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
48	46, 47	eqeltrd 2864	. . . . . . 7 ⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ)
49	44, 48	eqeltrd 2864	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹))) ∈ ℝ)
50	36, 49	eqeltrid 2868	. . . . 5 ⊢ (𝜑 → (vol‘dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) ∈ ℝ)
51		rescncf 25273	. . . . . . . . 9 ⊢ ((𝐴[,]𝐵) ⊆ 𝐸 → ((ℝ D 𝐹) ∈ (𝐸–cn→ℂ) → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
52	25, 51	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((ℝ D 𝐹) ∈ (𝐸–cn→ℂ) → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
53	27, 52	mpd 16	. . . . . . 7 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
54		cniccbdd 25837	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ((ℝ D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥)
55	6, 8, 53, 54	syl3anc 1399	. . . . . 6 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥)
56	35, 43	eqtrid 2810	. . . . . . . . . . 11 ⊢ (𝜑 → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (𝐴(,)𝐵))
57	56, 24	eqsstrd 3947	. . . . . . . . . 10 ⊢ (𝜑 → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
58		ssralv 3982	. . . . . . . . . 10 ⊢ (dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵) → (∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥))
59	57, 58	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥))
60	59	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥))
61	57	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵))
62	61	sselda 3913	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → 𝑦 ∈ (𝐴[,]𝐵))
63		fvres 6935	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝐴[,]𝐵) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦))
64	62, 63	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦))
65		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)))
66	56	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (𝐴(,)𝐵))
67	65, 66	eleqtrd 2866	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → 𝑦 ∈ (𝐴(,)𝐵))
68		fvres 6935	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦))
69	67, 68	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦))
70	64, 69	eqtr4d 2801	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦) = (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦))
71	70	fveq2d 6920	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) = (abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)))
72	71	breq1d 5118	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → ((abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 ↔ (abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥))
73	72	biimpd 232	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → ((abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → (abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥))
74	73	ralimdva 3178	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥))
75	60, 74	syld 48	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥))
76	75	reximdva 3179	. . . . . 6 ⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥))
77	55, 76	mpd 16	. . . . 5 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥)
78		bddibl 26215	. . . . 5 ⊢ ((((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ MblFn ∧ (vol‘dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ 𝐿¹)
79	34, 50, 77, 78	syl3anc 1399	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ 𝐿¹)
80	22, 79	eqeltrd 2864	. . 3 ⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈ 𝐿¹)
81		dvcn 26296	. . . . 5 ⊢ (((ℝ ⊆ ℂ ∧ 𝐹:𝐸⟶ℂ ∧ 𝐸 ⊆ ℝ) ∧ dom (ℝ D 𝐹) = 𝐸) → 𝐹 ∈ (𝐸–cn→ℂ))
82	11, 12, 4, 39, 81	syl31anc 1401	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝐸–cn→ℂ))
83		rescncf 25273	. . . . 5 ⊢ ((𝐴[,]𝐵) ⊆ 𝐸 → (𝐹 ∈ (𝐸–cn→ℂ) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
84	25, 83	syl 18	. . . 4 ⊢ (𝜑 → (𝐹 ∈ (𝐸–cn→ℂ) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
85	82, 84	mpd 16	. . 3 ⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
86	6, 8, 9, 30, 80, 85	ftc2 26419	. 2 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)))
87	22	fveq1d 6918	. . . . 5 ⊢ (𝜑 → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡))
88		fvres 6935	. . . . 5 ⊢ (𝑡 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
89	87, 88	sylan9eq 2818	. . . 4 ⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
90	89	ralrimiva 3158	. . 3 ⊢ (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
91		itgeq2 26153	. . 3 ⊢ (∀𝑡 ∈ (𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡) → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
92	90, 91	syl 18	. 2 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
93	6	rexrd 11398	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
94	8	rexrd 11398	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ ℝ^*)
95		ubicc2 13636	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
96	93, 94, 9, 95	syl3anc 1399	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵))
97	96	fvresd 6936	. . 3 ⊢ (𝜑 → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) = (𝐹‘𝐵))
98		lbicc2 13635	. . . . 5 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
99	93, 94, 9, 98	syl3anc 1399	. . . 4 ⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵))
100	99	fvresd 6936	. . 3 ⊢ (𝜑 → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴) = (𝐹‘𝐴))
101	97, 100	oveq12d 7469	. 2 ⊢ (𝜑 → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴)))
102	86, 92, 101	3eqtr3d 2806	1 ⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ∀wral 3080 ∃wrex 3090 ⊆ wss 3900 ∩ cin 4092 class class class wbr 5108 dom cdm 5658 ran crn 5659 ↾ cres 5660 ⟶wf 6562 ‘cfv 6566 (class class class)co 7451 ℂcc 11237 ℝcr 11238 ℝ^*cxr 11381 ≤ cle 11383 − cmin 11580 (,)cioo 13516 [,]cicc 13519 abscabs 15444 TopOpenctopn 17642 topGenctg 17658 ℂ_fldccnfld 21729 intcnt 23390 –cn→ccncf 25252 volcvol 25839 MblFncmbf 25990 𝐿¹cibl 25993 ∫citg 25994 D cdv 26238

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-inf2 9679 ax-cc 10552 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317 ax-addf 11318

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-symdif 4201 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-disj 5076 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7725 df-ofr 7726 df-om 7912 df-1st 8035 df-2nd 8036 df-supp 8215 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-oadd 8518 df-omul 8519 df-er 8755 df-map 8887 df-pm 8888 df-ixp 8964 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-fsupp 9392 df-fi 9440 df-sup 9471 df-inf 9472 df-oi 9541 df-dju 10019 df-card 10057 df-acn 10060 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-z 12734 df-dec 12855 df-uz 13006 df-q 13116 df-rp 13161 df-xneg 13281 df-xadd 13282 df-xmul 13283 df-ioo 13520 df-ioc 13521 df-ico 13522 df-icc 13523 df-fz 13680 df-fzo 13829 df-fl 13972 df-mod 14050 df-seq 14185 df-exp 14245 df-hash 14516 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-limsup 15682 df-clim 15699 df-rlim 15700 df-sum 15898 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-starv 17488 df-sca 17489 df-vsca 17490 df-ip 17491 df-tset 17492 df-ple 17493 df-ds 17495 df-unif 17496 df-hom 17497 df-cco 17498 df-euf 17499 df-rest 17643 df-topn 17644 df-0g 17662 df-gsum 17663 df-topgen 17664 df-pt 17665 df-prds 17668 df-xrs 17724 df-qtop 17729 df-imas 17730 df-xps 17732 df-mre 17806 df-mrc 17807 df-acs 17809 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-submnd 19029 df-mulg 19328 df-cntz 19582 df-cmn 20047 df-psmet 21721 df-xmet 21722 df-met 21723 df-bl 21724 df-mopn 21725 df-fbas 21726 df-fg 21727 df-cnfld 21730 df-top 23267 df-topon 23284 df-topsp 23306 df-bases 23319 df-cld 23392 df-ntr 23393 df-cls 23394 df-nei 23471 df-lp 23509 df-perf 23510 df-cn 23600 df-cnp 23601 df-haus 23688 df-cmp 23760 df-tx 23936 df-hmeo 24129 df-fil 24220 df-fm 24312 df-flim 24313 df-flf 24314 df-xms 24694 df-ms 24695 df-tms 24696 df-cncf 25254 df-ovol 25840 df-vol 25841 df-mbf 25995 df-itg1 25996 df-itg2 25997 df-ibl 25998 df-itg 25999 df-0p 26046 df-limc 26241 df-dv 26242

This theorem is used by: fdvposlt 35339 fdvposle 35341 itgexpif 35346

W3C validator