Proof of Theorem ftc2ditglem
Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐵) |
2 | 1 | ditgpos 24608 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
3 | | ftc2ditg.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℝ) |
4 | | ftc2ditg.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℝ) |
5 | | iccssre 12904 |
. . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ) |
6 | 3, 4, 5 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) |
7 | | ftc2ditg.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) |
8 | 6, 7 | sseldd 3879 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
9 | 8 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ) |
10 | | ftc2ditg.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) |
11 | 6, 10 | sseldd 3879 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
12 | 11 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ) |
13 | | ax-resscn 10673 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ℝ ⊆
ℂ) |
15 | | ftc2ditg.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ)) |
16 | | cncff 23646 |
. . . . . . . . 9
⊢ (𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ) → 𝐹:(𝑋[,]𝑌)⟶ℂ) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(𝑋[,]𝑌)⟶ℂ) |
18 | 17 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐹:(𝑋[,]𝑌)⟶ℂ) |
19 | 6 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝑋[,]𝑌) ⊆ ℝ) |
20 | | iccssre 12904 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
21 | 8, 11, 20 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
22 | 21 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝐴[,]𝐵) ⊆ ℝ) |
23 | | eqid 2738 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
24 | 23 | tgioo2 23556 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
25 | 23, 24 | dvres 24663 |
. . . . . . 7
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝑋[,]𝑌)⟶ℂ) ∧ ((𝑋[,]𝑌) ⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
26 | 14, 18, 19, 22, 25 | syl22anc 838 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) |
27 | | iccntr 23574 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
28 | 8, 11, 27 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
29 | 28 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) |
30 | 29 | reseq2d 5826 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) |
31 | 26, 30 | eqtrd 2773 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) |
32 | 3 | rexrd 10770 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
33 | | elicc2 12887 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐴 ∈ (𝑋[,]𝑌) ↔ (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌))) |
34 | 3, 4, 33 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ (𝑋[,]𝑌) ↔ (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌))) |
35 | 7, 34 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌)) |
36 | 35 | simp2d 1144 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≤ 𝐴) |
37 | | iooss1 12857 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℝ*
∧ 𝑋 ≤ 𝐴) → (𝐴(,)𝐵) ⊆ (𝑋(,)𝐵)) |
38 | 32, 36, 37 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝑋(,)𝐵)) |
39 | 4 | rexrd 10770 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈
ℝ*) |
40 | | elicc2 12887 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐵 ∈ (𝑋[,]𝑌) ↔ (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌))) |
41 | 3, 4, 40 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ∈ (𝑋[,]𝑌) ↔ (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌))) |
42 | 10, 41 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌)) |
43 | 42 | simp3d 1145 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ≤ 𝑌) |
44 | | iooss2 12858 |
. . . . . . . . 9
⊢ ((𝑌 ∈ ℝ*
∧ 𝐵 ≤ 𝑌) → (𝑋(,)𝐵) ⊆ (𝑋(,)𝑌)) |
45 | 39, 43, 44 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (𝑋(,)𝐵) ⊆ (𝑋(,)𝑌)) |
46 | 38, 45 | sstrd 3888 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝑋(,)𝑌)) |
47 | 46 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝐴(,)𝐵) ⊆ (𝑋(,)𝑌)) |
48 | | ftc2ditg.c |
. . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
49 | 48 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ)) |
50 | | rescncf 23650 |
. . . . . 6
⊢ ((𝐴(,)𝐵) ⊆ (𝑋(,)𝑌) → ((ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))) |
51 | 47, 49, 50 | sylc 65 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
52 | 31, 51 | eqeltrd 2833 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) |
53 | | cncff 23646 |
. . . . . . . . . . 11
⊢ ((ℝ
D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (ℝ D 𝐹):(𝑋(,)𝑌)⟶ℂ) |
54 | 48, 53 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐹):(𝑋(,)𝑌)⟶ℂ) |
55 | 54 | feqmptd 6738 |
. . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡))) |
56 | 55 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D 𝐹) = (𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡))) |
57 | 56 | reseq1d 5825 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = ((𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ (𝐴(,)𝐵))) |
58 | 47 | resmptd 5883 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ (𝐴(,)𝐵)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡))) |
59 | 57, 58 | eqtrd 2773 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡))) |
60 | 31, 59 | eqtrd 2773 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡))) |
61 | | ioombl 24318 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol |
62 | 61 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝐴(,)𝐵) ∈ dom vol) |
63 | | fvexd 6690 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝑡 ∈ (𝑋(,)𝑌)) → ((ℝ D 𝐹)‘𝑡) ∈ V) |
64 | | ftc2ditg.i |
. . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹) ∈
𝐿1) |
65 | 64 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D 𝐹) ∈
𝐿1) |
66 | 56, 65 | eqeltrrd 2834 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)) ∈
𝐿1) |
67 | 47, 62, 63, 66 | iblss 24557 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈
𝐿1) |
68 | 60, 67 | eqeltrd 2833 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈
𝐿1) |
69 | | iccss2 12893 |
. . . . . . 7
⊢ ((𝐴 ∈ (𝑋[,]𝑌) ∧ 𝐵 ∈ (𝑋[,]𝑌)) → (𝐴[,]𝐵) ⊆ (𝑋[,]𝑌)) |
70 | 7, 10, 69 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (𝑋[,]𝑌)) |
71 | | rescncf 23650 |
. . . . . 6
⊢ ((𝐴[,]𝐵) ⊆ (𝑋[,]𝑌) → (𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) |
72 | 70, 15, 71 | sylc 65 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
73 | 72 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) |
74 | 9, 12, 1, 52, 68, 73 | ftc2 24796 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴))) |
75 | 31 | fveq1d 6677 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡)) |
76 | | fvres 6694 |
. . . . 5
⊢ (𝑡 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡) = ((ℝ D 𝐹)‘𝑡)) |
77 | 75, 76 | sylan9eq 2793 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡)) |
78 | 77 | itgeq2dv 24534 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) |
79 | 9 | rexrd 10770 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈
ℝ*) |
80 | 12 | rexrd 10770 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈
ℝ*) |
81 | | ubicc2 12940 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
82 | | lbicc2 12939 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
83 | | fvres 6694 |
. . . . . 6
⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) = (𝐹‘𝐵)) |
84 | | fvres 6694 |
. . . . . 6
⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴) = (𝐹‘𝐴)) |
85 | 83, 84 | oveqan12d 7190 |
. . . . 5
⊢ ((𝐵 ∈ (𝐴[,]𝐵) ∧ 𝐴 ∈ (𝐴[,]𝐵)) → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
86 | 81, 82, 85 | syl2anc 587 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
87 | 79, 80, 1, 86 | syl3anc 1372 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
88 | 74, 78, 87 | 3eqtr3d 2781 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |
89 | 2, 88 | eqtrd 2773 |
1
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |