Proof of Theorem ftc2ditglem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ≤ 𝐵) | 
| 2 | 1 | ditgpos 25891 | . 2
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) | 
| 3 |  | ftc2ditg.x | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 4 |  | ftc2ditg.y | . . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 5 |  | iccssre 13469 | . . . . . . 7
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ) | 
| 6 | 3, 4, 5 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑋[,]𝑌) ⊆ ℝ) | 
| 7 |  | ftc2ditg.a | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌)) | 
| 8 | 6, 7 | sseldd 3984 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 9 | 8 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈ ℝ) | 
| 10 |  | ftc2ditg.b | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌)) | 
| 11 | 6, 10 | sseldd 3984 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 12 | 11 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈ ℝ) | 
| 13 |  | ax-resscn 11212 | . . . . . . . 8
⊢ ℝ
⊆ ℂ | 
| 14 | 13 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ℝ ⊆
ℂ) | 
| 15 |  | ftc2ditg.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ)) | 
| 16 |  | cncff 24919 | . . . . . . . . 9
⊢ (𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ) → 𝐹:(𝑋[,]𝑌)⟶ℂ) | 
| 17 | 15, 16 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐹:(𝑋[,]𝑌)⟶ℂ) | 
| 18 | 17 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐹:(𝑋[,]𝑌)⟶ℂ) | 
| 19 | 6 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝑋[,]𝑌) ⊆ ℝ) | 
| 20 |  | iccssre 13469 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) | 
| 21 | 8, 11, 20 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) | 
| 22 | 21 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝐴[,]𝐵) ⊆ ℝ) | 
| 23 |  | eqid 2737 | . . . . . . . 8
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 24 |  | tgioo4 24826 | . . . . . . . 8
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 25 | 23, 24 | dvres 25946 | . . . . . . 7
⊢
(((ℝ ⊆ ℂ ∧ 𝐹:(𝑋[,]𝑌)⟶ℂ) ∧ ((𝑋[,]𝑌) ⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) | 
| 26 | 14, 18, 19, 22, 25 | syl22anc 839 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)))) | 
| 27 |  | iccntr 24843 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) | 
| 28 | 8, 11, 27 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 →
((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) | 
| 29 | 28 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) | 
| 30 | 29 | reseq2d 5997 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran
(,)))‘(𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) | 
| 31 | 26, 30 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵))) | 
| 32 | 3 | rexrd 11311 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈
ℝ*) | 
| 33 |  | elicc2 13452 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐴 ∈ (𝑋[,]𝑌) ↔ (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌))) | 
| 34 | 3, 4, 33 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ (𝑋[,]𝑌) ↔ (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌))) | 
| 35 | 7, 34 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝑋 ≤ 𝐴 ∧ 𝐴 ≤ 𝑌)) | 
| 36 | 35 | simp2d 1144 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ≤ 𝐴) | 
| 37 |  | iooss1 13422 | . . . . . . . . 9
⊢ ((𝑋 ∈ ℝ*
∧ 𝑋 ≤ 𝐴) → (𝐴(,)𝐵) ⊆ (𝑋(,)𝐵)) | 
| 38 | 32, 36, 37 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝑋(,)𝐵)) | 
| 39 | 4 | rexrd 11311 | . . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈
ℝ*) | 
| 40 |  | elicc2 13452 | . . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐵 ∈ (𝑋[,]𝑌) ↔ (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌))) | 
| 41 | 3, 4, 40 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ∈ (𝑋[,]𝑌) ↔ (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌))) | 
| 42 | 10, 41 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → (𝐵 ∈ ℝ ∧ 𝑋 ≤ 𝐵 ∧ 𝐵 ≤ 𝑌)) | 
| 43 | 42 | simp3d 1145 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ≤ 𝑌) | 
| 44 |  | iooss2 13423 | . . . . . . . . 9
⊢ ((𝑌 ∈ ℝ*
∧ 𝐵 ≤ 𝑌) → (𝑋(,)𝐵) ⊆ (𝑋(,)𝑌)) | 
| 45 | 39, 43, 44 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑋(,)𝐵) ⊆ (𝑋(,)𝑌)) | 
| 46 | 38, 45 | sstrd 3994 | . . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ (𝑋(,)𝑌)) | 
| 47 | 46 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝐴(,)𝐵) ⊆ (𝑋(,)𝑌)) | 
| 48 |  | ftc2ditg.c | . . . . . . 7
⊢ (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ)) | 
| 49 | 48 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ)) | 
| 50 |  | rescncf 24923 | . . . . . 6
⊢ ((𝐴(,)𝐵) ⊆ (𝑋(,)𝑌) → ((ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))) | 
| 51 | 47, 49, 50 | sylc 65 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 52 | 31, 51 | eqeltrd 2841 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈ ((𝐴(,)𝐵)–cn→ℂ)) | 
| 53 |  | cncff 24919 | . . . . . . . . . . 11
⊢ ((ℝ
D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (ℝ D 𝐹):(𝑋(,)𝑌)⟶ℂ) | 
| 54 | 48, 53 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (ℝ D 𝐹):(𝑋(,)𝑌)⟶ℂ) | 
| 55 | 54 | feqmptd 6977 | . . . . . . . . 9
⊢ (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡))) | 
| 56 | 55 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D 𝐹) = (𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡))) | 
| 57 | 56 | reseq1d 5996 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = ((𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ (𝐴(,)𝐵))) | 
| 58 | 47 | resmptd 6058 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ (𝐴(,)𝐵)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡))) | 
| 59 | 57, 58 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡))) | 
| 60 | 31, 59 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡))) | 
| 61 |  | ioombl 25600 | . . . . . . 7
⊢ (𝐴(,)𝐵) ∈ dom vol | 
| 62 | 61 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝐴(,)𝐵) ∈ dom vol) | 
| 63 |  | fvexd 6921 | . . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝑡 ∈ (𝑋(,)𝑌)) → ((ℝ D 𝐹)‘𝑡) ∈ V) | 
| 64 |  | ftc2ditg.i | . . . . . . . 8
⊢ (𝜑 → (ℝ D 𝐹) ∈
𝐿1) | 
| 65 | 64 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D 𝐹) ∈
𝐿1) | 
| 66 | 56, 65 | eqeltrrd 2842 | . . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)) ∈
𝐿1) | 
| 67 | 47, 62, 63, 66 | iblss 25840 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈
𝐿1) | 
| 68 | 60, 67 | eqeltrd 2841 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈
𝐿1) | 
| 69 |  | iccss2 13458 | . . . . . . 7
⊢ ((𝐴 ∈ (𝑋[,]𝑌) ∧ 𝐵 ∈ (𝑋[,]𝑌)) → (𝐴[,]𝐵) ⊆ (𝑋[,]𝑌)) | 
| 70 | 7, 10, 69 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (𝑋[,]𝑌)) | 
| 71 |  | rescncf 24923 | . . . . . 6
⊢ ((𝐴[,]𝐵) ⊆ (𝑋[,]𝑌) → (𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))) | 
| 72 | 70, 15, 71 | sylc 65 | . . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) | 
| 73 | 72 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) | 
| 74 | 9, 12, 1, 52, 68, 73 | ftc2 26085 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴))) | 
| 75 | 31 | fveq1d 6908 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡)) | 
| 76 |  | fvres 6925 | . . . . 5
⊢ (𝑡 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡) = ((ℝ D 𝐹)‘𝑡)) | 
| 77 | 75, 76 | sylan9eq 2797 | . . . 4
⊢ (((𝜑 ∧ 𝐴 ≤ 𝐵) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡)) | 
| 78 | 77 | itgeq2dv 25817 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡) | 
| 79 | 9 | rexrd 11311 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐴 ∈
ℝ*) | 
| 80 | 12 | rexrd 11311 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → 𝐵 ∈
ℝ*) | 
| 81 |  | ubicc2 13505 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) | 
| 82 |  | lbicc2 13504 | . . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) | 
| 83 |  | fvres 6925 | . . . . . 6
⊢ (𝐵 ∈ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) = (𝐹‘𝐵)) | 
| 84 |  | fvres 6925 | . . . . . 6
⊢ (𝐴 ∈ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴) = (𝐹‘𝐴)) | 
| 85 | 83, 84 | oveqan12d 7450 | . . . . 5
⊢ ((𝐵 ∈ (𝐴[,]𝐵) ∧ 𝐴 ∈ (𝐴[,]𝐵)) → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) | 
| 86 | 81, 82, 85 | syl2anc 584 | . . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) | 
| 87 | 79, 80, 1, 86 | syl3anc 1373 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹‘𝐵) − (𝐹‘𝐴))) | 
| 88 | 74, 78, 87 | 3eqtr3d 2785 | . 2
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) | 
| 89 | 2, 88 | eqtrd 2777 | 1
⊢ ((𝜑 ∧ 𝐴 ≤ 𝐵) → ⨜[𝐴 → 𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹‘𝐵) − (𝐹‘𝐴))) |