Step | Hyp | Ref
| Expression |
1 | | ftc2.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | rexrd 10089 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
3 | | ftc2.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | 3 | rexrd 10089 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
5 | | ftc2.le |
. . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
6 | | ubicc2 12289 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
7 | 2, 4, 5, 6 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
8 | | fvex 6201 |
. . . . . 6
⊢ ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) ∈ V |
9 | 8 | fvconst2 6469 |
. . . . 5
⊢ (𝐵 ∈ (𝐴[,]𝐵) → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)) |
10 | 7, 9 | syl 17 |
. . . 4
⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)) |
11 | | eqid 2622 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
12 | 11 | subcn 22669 |
. . . . . . . . 9
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → − ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
14 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) |
15 | | ssid 3624 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵) |
16 | 15 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴(,)𝐵)) |
17 | | ioossre 12235 |
. . . . . . . . . 10
⊢ (𝐴(,)𝐵) ⊆ ℝ |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
19 | | ftc2.i |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) ∈
𝐿1) |
20 | | ftc2.c |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
21 | | cncff 22696 |
. . . . . . . . . 10
⊢ ((ℝ
D 𝐹) ∈ ((𝐴(,)𝐵)–cn→ℂ) → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹):(𝐴(,)𝐵)⟶ℂ) |
23 | 14, 1, 3, 5, 16, 18, 19, 22 | ftc1a 23800 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
24 | | ftc2.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
25 | | cncff 22696 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(𝐴[,]𝐵)⟶ℂ) |
27 | 26 | feqmptd 6249 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) |
28 | 27, 24 | eqeltrrd 2702 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
29 | 11, 13, 23, 28 | cncfmpt2f 22717 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
30 | | ax-resscn 9993 |
. . . . . . . . . . 11
⊢ ℝ
⊆ ℂ |
31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ⊆
ℂ) |
32 | | iccssre 12255 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
33 | 1, 3, 32 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
34 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢ ((ℝ
D 𝐹)‘𝑡) ∈ V |
35 | 34 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝑥)) → ((ℝ D 𝐹)‘𝑡) ∈ V) |
36 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈ ℝ) |
37 | 36 | rexrd 10089 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐵 ∈
ℝ*) |
38 | | elicc2 12238 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
39 | 1, 3, 38 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↔ (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵))) |
40 | 39 | biimpa 501 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵)) |
41 | 40 | simp3d 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵) |
42 | | iooss2 12211 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℝ*
∧ 𝑥 ≤ 𝐵) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵)) |
43 | 37, 41, 42 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ⊆ (𝐴(,)𝐵)) |
44 | | ioombl 23333 |
. . . . . . . . . . . . . 14
⊢ (𝐴(,)𝑥) ∈ dom vol |
45 | 44 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐴(,)𝑥) ∈ dom vol) |
46 | 34 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V) |
47 | 22 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡))) |
48 | 47, 19 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈
𝐿1) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈
𝐿1) |
50 | 43, 45, 46, 49 | iblss 23571 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑡 ∈ (𝐴(,)𝑥) ↦ ((ℝ D 𝐹)‘𝑡)) ∈
𝐿1) |
51 | 35, 50 | itgcl 23550 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ) |
52 | 26 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
53 | 51, 52 | subcld 10392 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) ∈ ℂ) |
54 | 11 | tgioo2 22606 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
55 | | iccntr 22624 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
56 | 1, 3, 55 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
57 | 31, 33, 53, 54, 11, 56 | dvmptntr 23734 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))))) |
58 | | reelprrecn 10028 |
. . . . . . . . . . 11
⊢ ℝ
∈ {ℝ, ℂ} |
59 | 58 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
60 | | ioossicc 12259 |
. . . . . . . . . . . 12
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
61 | 60 | sseli 3599 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ (𝐴[,]𝐵)) |
62 | 61, 51 | sylan2 491 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ) |
63 | 22 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑥) ∈ ℂ) |
64 | 14, 1, 3, 5, 20, 19 | ftc1cn 23806 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D 𝐹)) |
65 | 31, 33, 51, 54, 11, 56 | dvmptntr 23734 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡))) |
66 | 22 | feqmptd 6249 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D 𝐹) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥))) |
67 | 64, 65, 66 | 3eqtr3d 2664 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥))) |
68 | 61, 52 | sylan2 491 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑥) ∈ ℂ) |
69 | 31, 33, 52, 54, 11, 56 | dvmptntr 23734 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥)))) |
70 | 27 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ D 𝐹) = (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥)))) |
71 | 70, 66 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥))) |
72 | 69, 71 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (𝐹‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑥))) |
73 | 59, 62, 63, 67, 68, 63, 72 | dvmptsub 23730 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥)))) |
74 | 63 | subidd 10380 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥)) = 0) |
75 | 74 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ (((ℝ D 𝐹)‘𝑥) − ((ℝ D 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)) |
76 | 57, 73, 75 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)) |
77 | | fconstmpt 5163 |
. . . . . . . 8
⊢ ((𝐴(,)𝐵) × {0}) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0) |
78 | 76, 77 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))) = ((𝐴(,)𝐵) × {0})) |
79 | 1, 3, 29, 78 | dveq0 23763 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = ((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})) |
80 | 79 | fveq1d 6193 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵)) |
81 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (𝐴(,)𝑥) = (𝐴(,)𝐵)) |
82 | | itgeq1 23539 |
. . . . . . . . 9
⊢ ((𝐴(,)𝑥) = (𝐴(,)𝐵) → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
83 | 81, 82 | syl 17 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
84 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
85 | 83, 84 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) |
86 | | eqid 2622 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥))) |
87 | | ovex 6678 |
. . . . . . 7
⊢
(∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) ∈ V |
88 | 85, 86, 87 | fvmpt 6282 |
. . . . . 6
⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) |
89 | 7, 88 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) |
90 | 80, 89 | eqtr3d 2658 |
. . . 4
⊢ (𝜑 → (((𝐴[,]𝐵) × {((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴)})‘𝐵) = (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) |
91 | | lbicc2 12288 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
92 | 2, 4, 5, 91 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
93 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = (𝐴(,)𝐴)) |
94 | | iooid 12203 |
. . . . . . . . . . 11
⊢ (𝐴(,)𝐴) = ∅ |
95 | 93, 94 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐴(,)𝑥) = ∅) |
96 | | itgeq1 23539 |
. . . . . . . . . 10
⊢ ((𝐴(,)𝑥) = ∅ → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡) |
97 | 95, 96 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = ∫∅((ℝ D 𝐹)‘𝑡) d𝑡) |
98 | | itg0 23546 |
. . . . . . . . 9
⊢
∫∅((ℝ D 𝐹)‘𝑡) d𝑡 = 0 |
99 | 97, 98 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 = 0) |
100 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
101 | 99, 100 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = (0 − (𝐹‘𝐴))) |
102 | | df-neg 10269 |
. . . . . . 7
⊢ -(𝐹‘𝐴) = (0 − (𝐹‘𝐴)) |
103 | 101, 102 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)) = -(𝐹‘𝐴)) |
104 | | negex 10279 |
. . . . . 6
⊢ -(𝐹‘𝐴) ∈ V |
105 | 103, 86, 104 | fvmpt 6282 |
. . . . 5
⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴)) |
106 | 92, 105 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝐴[,]𝐵) ↦ (∫(𝐴(,)𝑥)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝑥)))‘𝐴) = -(𝐹‘𝐴)) |
107 | 10, 90, 106 | 3eqtr3d 2664 |
. . 3
⊢ (𝜑 → (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵)) = -(𝐹‘𝐴)) |
108 | 107 | oveq2d 6666 |
. 2
⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ((𝐹‘𝐵) + -(𝐹‘𝐴))) |
109 | 26, 7 | ffvelrnd 6360 |
. . 3
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ) |
110 | 34 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D 𝐹)‘𝑡) ∈ V) |
111 | 110, 48 | itgcl 23550 |
. . 3
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 ∈ ℂ) |
112 | 109, 111 | pncan3d 10395 |
. 2
⊢ (𝜑 → ((𝐹‘𝐵) + (∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 − (𝐹‘𝐵))) = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
113 | 26, 92 | ffvelrnd 6360 |
. . 3
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℂ) |
114 | 109, 113 | negsubd 10398 |
. 2
⊢ (𝜑 → ((𝐹‘𝐵) + -(𝐹‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
115 | 108, 112,
114 | 3eqtr3d 2664 |
1
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |