Step | Hyp | Ref
| Expression |
1 | | ftc2.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
3 | | ftc2.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | 3 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
5 | | ftc2.le |
. . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
6 | | ubicc2 12160 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
7 | 2, 4, 5, 6 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
8 | | fvex 6113 |
. . . . . 6
⊢ ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) ∈ V |
9 | 8 | fvconst2 6374 |
. . . . 5
⊢ (𝐵 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)) |
10 | 7, 9 | syl 17 |
. . . 4
⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)) |
11 | | eqid 2610 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
12 | 11 | subcn 22477 |
. . . . . . . . 9
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → − ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
14 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) |
15 | | ssid 3587 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵) |
16 | 15 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)) |
17 | | ioossre 12106 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ ℝ |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
19 | | ftc2.i |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) ∈
𝐿1) |
20 | | ftc2.c |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
21 | | cncff 22504 |
. . . . . . . . . 10
⊢ ((ℝ
D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
23 | 14, 1, 3, 5, 16, 18, 19, 22 | ftc1a 23604 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
24 | | ftc2.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
25 | | cncff 22504 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
27 | 26 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) |
28 | 27, 24 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
29 | 11, 13, 23, 28 | cncfmpt2f 22525 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
30 | | ax-resscn 9872 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) |
32 | | iccssre 12126 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
33 | 1, 3, 32 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
34 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ ((ℝ
D 𝐹)‘𝑡) ∈ V |
35 | 34 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑥)) → ((ℝ D 𝐹)‘𝑡) ∈ V) |
36 | 3 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
37 | 36 | rexrd 9968 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈
ℝ*) |
38 | | elicc2 12109 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
39 | 1, 3, 38 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
40 | 39 | biimpa 500 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
41 | 40 | simp3d 1068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵) |
42 | | iooss2 12082 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ*
∧ 𝑥 ≤ 𝐵) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵)) |
43 | 37, 41, 42 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵)) |
44 | | ioombl 23140 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝑥) ∈ dom vol |
45 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ∈ dom vol) |
46 | 34 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V) |
47 | 22 | feqmptd 6159 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡))) |
48 | 47, 19 | eqeltrrd 2689 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈
𝐿1) |
49 | 48 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈
𝐿1) |
50 | 43, 45, 46, 49 | iblss 23377 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑥) ↦ ((ℝ D 𝐹)‘𝑡)) ∈
𝐿1) |
51 | 35, 50 | itgcl 23356 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ) |
52 | 26 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
53 | 51, 52 | subcld 10271 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) ∈ ℂ) |
54 | 11 | tgioo2 22414 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
55 | | iccntr 22432 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
56 | 1, 3, 55 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
57 | 31, 33, 53, 54, 11, 56 | dvmptntr 23540 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))))) |
58 | | reelprrecn 9907 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
59 | 58 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
60 | | ioossicc 12130 |
. . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
61 | 60 | sseli 3564 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ (𝐴[,]𝐵)) |
62 | 61, 51 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ) |
63 | 22 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
64 | 14, 1, 3, 5, 20, 19 | ftc1cn 23610 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D 𝐹)) |
65 | 31, 33, 51, 54, 11, 56 | dvmptntr 23540 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡))) |
66 | 22 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D 𝐹) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥))) |
67 | 64, 65, 66 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥))) |
68 | 61, 52 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
69 | 31, 33, 52, 54, 11, 56 | dvmptntr 23540 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)))) |
70 | 27 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))) |
71 | 70, 66 | eqtr3d 2646 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥))) |
72 | 69, 71 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥))) |
73 | 59, 62, 63, 67, 68, 63, 72 | dvmptsub 23536 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥)))) |
74 | 63 | subidd 10259 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥)) = 0) |
75 | 74 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)) |
76 | 57, 73, 75 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)) |
77 | | fconstmpt 5085 |
. . . . . . . 8
⊢ ((𝐴(,)𝐵) × {0}) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0) |
78 | 76, 77 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = ((𝐴(,)𝐵) × {0})) |
79 | 1, 3, 29, 78 | dveq0 23567 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = ((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})) |
80 | 79 | fveq1d 6105 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵)) |
81 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (𝐴(,)𝑥) = (𝐴(,)𝐵)) |
82 | | itgeq1 23345 |
. . . . . . . . 9
⊢ ((𝐴(,)𝑥) = (𝐴(,)𝐵) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
83 | 81, 82 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
84 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
85 | 83, 84 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) |
86 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) |
87 | | ovex 6577 |
. . . . . . 7
⊢
(∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) ∈ V |
88 | 85, 86, 87 | fvmpt 6191 |
. . . . . 6
⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) |
89 | 7, 88 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) |
90 | 80, 89 | eqtr3d 2646 |
. . . 4
⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) |
91 | | lbicc2 12159 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
92 | 2, 4, 5, 91 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
93 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = (𝐴(,)𝐴)) |
94 | | iooid 12074 |
. . . . . . . . . . 11
⊢ (𝐴(,)𝐴) = ∅ |
95 | 93, 94 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = ∅) |
96 | | itgeq1 23345 |
. . . . . . . . . 10
⊢ ((𝐴(,)𝑥) = ∅ → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡) |
97 | 95, 96 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡) |
98 | | itg0 23352 |
. . . . . . . . 9
⊢
∫∅((ℝ D 𝐹)‘𝑡) d𝑡 = 0 |
99 | 97, 98 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = 0) |
100 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
101 | 99, 100 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (0 − (𝐹‘𝐴))) |
102 | | df-neg 10148 |
. . . . . . 7
⊢ -(𝐹‘𝐴) = (0 − (𝐹‘𝐴)) |
103 | 101, 102 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = -(𝐹‘𝐴)) |
104 | | negex 10158 |
. . . . . 6
⊢ -(𝐹‘𝐴) ∈ V |
105 | 103, 86, 104 | fvmpt 6191 |
. . . . 5
⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴)) |
106 | 92, 105 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴)) |
107 | 10, 90, 106 | 3eqtr3d 2652 |
. . 3
⊢ (𝜑 → (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) = -(𝐹‘𝐴)) |
108 | 107 | oveq2d 6565 |
. 2
⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ((𝐹‘𝐵) + -(𝐹‘𝐴))) |
109 | 26, 7 | ffvelrnd 6268 |
. . 3
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ) |
110 | 34 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V) |
111 | 110, 48 | itgcl 23356 |
. . 3
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ) |
112 | 109, 111 | pncan3d 10274 |
. 2
⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
113 | 26, 92 | ffvelrnd 6268 |
. . 3
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ) |
114 | 109, 113 | negsubd 10277 |
. 2
⊢ (𝜑 → ((𝐹‘𝐵) + -(𝐹‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
115 | 108, 112,
114 | 3eqtr3d 2652 |
1
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |