| Step | Hyp | Ref
| Expression |
| 1 | | ftc2re.e |
. . . . . 6
⊢ 𝐸 = (𝐶(,)𝐷) |
| 2 | | ioossre 13448 |
. . . . . 6
⊢ (𝐶(,)𝐷) ⊆ ℝ |
| 3 | 1, 2 | eqsstri 4030 |
. . . . 5
⊢ 𝐸 ⊆
ℝ |
| 4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐸 ⊆ ℝ) |
| 5 | | ftc2re.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝐸) |
| 6 | 4, 5 | sseldd 3984 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 7 | | ftc2re.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝐸) |
| 8 | 4, 7 | sseldd 3984 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 9 | | ftc2re.le |
. . 3
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 10 | | ax-resscn 11212 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
| 11 | 10 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
| 12 | | ftc2re.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐸⟶ℂ) |
| 13 | | iccssre 13469 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
| 14 | 6, 8, 13 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
| 15 | | eqid 2737 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 16 | | tgioo4 24826 |
. . . . . . 7
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 17 | 15, 16 | dvres 25946 |
. . . . . 6
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:𝐸⟶ℂ) ∧ (𝐸 ⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
| 18 | 11, 12, 4, 14, 17 | syl22anc 839 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
| 19 | | iccntr 24843 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
| 20 | 6, 8, 19 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
| 21 | 20 | reseq2d 5997 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹) ↾
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) |
| 22 | 18, 21 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) |
| 23 | | ioossicc 13473 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
| 24 | 23 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵)) |
| 25 | 1, 5, 7 | fct2relem 34612 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐸) |
| 26 | 24, 25 | sstrd 3994 |
. . . . 5
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐸) |
| 27 | | ftc2re.1 |
. . . . 5
⊢ (𝜑 → (ℝ D 𝐹) ∈ (𝐸–cn→ℂ)) |
| 28 | | rescncf 24923 |
. . . . 5
⊢ ((𝐴(,)𝐵) ⊆ 𝐸 → ((ℝ D 𝐹) ∈ (𝐸–cn→ℂ) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))) |
| 29 | 26, 27, 28 | sylc 65 |
. . . 4
⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 30 | 22, 29 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
| 31 | | ioombl 25600 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
| 32 | 31 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ dom vol) |
| 33 | | cnmbf 25694 |
. . . . . 6
⊢ (((𝐴(,)𝐵) ∈ dom vol ∧ ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ MblFn) |
| 34 | 32, 29, 33 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ MblFn) |
| 35 | | dmres 6030 |
. . . . . . 7
⊢ dom
((ℝ D 𝐹) ↾
(𝐴(,)𝐵)) = ((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹)) |
| 36 | 35 | fveq2i 6909 |
. . . . . 6
⊢
(vol‘dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) = (vol‘((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹))) |
| 37 | | cncff 24919 |
. . . . . . . . . . . 12
⊢ ((ℝ
D 𝐹) ∈ (𝐸–cn→ℂ) → (ℝ D 𝐹):𝐸⟶ℂ) |
| 38 | 27, 37 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℝ D 𝐹):𝐸⟶ℂ) |
| 39 | 38 | fdmd 6746 |
. . . . . . . . . 10
⊢ (𝜑 → dom (ℝ D 𝐹) = 𝐸) |
| 40 | 39 | ineq2d 4220 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹)) = ((𝐴(,)𝐵) ∩ 𝐸)) |
| 41 | | dfss2 3969 |
. . . . . . . . . 10
⊢ ((𝐴(,)𝐵) ⊆ 𝐸 ↔ ((𝐴(,)𝐵) ∩ 𝐸) = (𝐴(,)𝐵)) |
| 42 | 26, 41 | sylib 218 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴(,)𝐵) ∩ 𝐸) = (𝐴(,)𝐵)) |
| 43 | 40, 42 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹)) = (𝐴(,)𝐵)) |
| 44 | 43 | fveq2d 6910 |
. . . . . . 7
⊢ (𝜑 → (vol‘((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹))) = (vol‘(𝐴(,)𝐵))) |
| 45 | | volioo 25604 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
| 46 | 6, 8, 9, 45 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) = (𝐵 − 𝐴)) |
| 47 | 8, 6 | resubcld 11691 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
| 48 | 46, 47 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → (vol‘(𝐴(,)𝐵)) ∈ ℝ) |
| 49 | 44, 48 | eqeltrd 2841 |
. . . . . 6
⊢ (𝜑 → (vol‘((𝐴(,)𝐵) ∩ dom (ℝ D 𝐹))) ∈ ℝ) |
| 50 | 36, 49 | eqeltrid 2845 |
. . . . 5
⊢ (𝜑 → (vol‘dom ((ℝ D
𝐹) ↾ (𝐴(,)𝐵))) ∈ ℝ) |
| 51 | | rescncf 24923 |
. . . . . . . . 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 25496 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ((ℝ
D 𝐹) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥) |
| 55 | 6, 8, 53, 54 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥) |
| 56 | 35, 43 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (𝜑 → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (𝐴(,)𝐵)) |
| 57 | 56, 24 | eqsstrd 4018 |
. . . . . . . . . 10
⊢ (𝜑 → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ⊆ (𝐴[,]𝐵)) |
| 58 | | ssralv 4052 |
. . . . . . . . . 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 3983 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → 𝑦 ∈ (𝐴[,]𝐵)) |
| 63 | | fvres 6925 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐴[,]𝐵) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦)) |
| 64 | 62, 63 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦)) |
| 65 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) |
| 66 | 56 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (𝐴(,)𝐵)) |
| 67 | 65, 66 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → 𝑦 ∈ (𝐴(,)𝐵)) |
| 68 | | fvres 6925 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦)) |
| 69 | 67, 68 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦) = ((ℝ D 𝐹)‘𝑦)) |
| 70 | 64, 69 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦) = (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) |
| 71 | 70 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → (abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) = (abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦))) |
| 72 | 71 | breq1d 5153 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → ((abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 ↔ (abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥)) |
| 73 | 72 | biimpd 229 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) → ((abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → (abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥)) |
| 74 | 73 | ralimdva 3167 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥)) |
| 75 | 60, 74 | syld 47 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥)) |
| 76 | 75 | reximdva 3168 |
. . . . . 6
⊢ (𝜑 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(((ℝ D 𝐹) ↾ (𝐴[,]𝐵))‘𝑦)) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥)) |
| 77 | 55, 76 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥) |
| 78 | | bddibl 25875 |
. . . . 5
⊢
((((ℝ D 𝐹)
↾ (𝐴(,)𝐵)) ∈ MblFn ∧
(vol‘dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))(abs‘(((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑦)) ≤ 𝑥) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈
𝐿1) |
| 79 | 34, 50, 77, 78 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈
𝐿1) |
| 80 | 22, 79 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈
𝐿1) |
| 81 | | dvcn 25957 |
. . . . 5
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:𝐸⟶ℂ ∧ 𝐸 ⊆ ℝ) ∧ dom (ℝ D 𝐹) = 𝐸) → 𝐹 ∈ (𝐸–cn→ℂ)) |
| 82 | 11, 12, 4, 39, 81 | syl31anc 1375 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐸–cn→ℂ)) |
| 83 | | rescncf 24923 |
. . . . 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 26085 |
. 2
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴))) |
| 87 | 22 | fveq1d 6908 |
. . . . 5
⊢ (𝜑 → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡)) |
| 88 | | fvres 6925 |
. . . . 5
⊢ (𝑡 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡) = ((ℝ D 𝐹)‘𝑡)) |
| 89 | 87, 88 | sylan9eq 2797 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡)) |
| 90 | 89 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑡 ∈ (𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡)) |
| 91 | | itgeq2 25813 |
. . 3
⊢
(∀𝑡 ∈
(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡) → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
| 92 | 90, 91 | syl 17 |
. 2
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
| 93 | 6 | rexrd 11311 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 94 | 8 | rexrd 11311 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 95 | | ubicc2 13505 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
| 96 | 93, 94, 9, 95 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
| 97 | 96 | fvresd 6926 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) = (𝐹‘𝐵)) |
| 98 | | lbicc2 13504 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
| 99 | 93, 94, 9, 98 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
| 100 | 99 | fvresd 6926 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴) = (𝐹‘𝐴)) |
| 101 | 97, 100 | oveq12d 7449 |
. 2
⊢ (𝜑 → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
| 102 | 86, 92, 101 | 3eqtr3d 2785 |
1
⊢ (𝜑 → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |