Metamath Proof Explorer

Theorem ftc2re

Description: The Fundamental Theorem of Calculus, part two, for functions continuous on D . (Contributed by Thierry Arnoux, 1-Dec-2021)

Ref Expression
Hypotheses ftc2re.e ⊢ 𝐸 = ( 𝐶 (,) 𝐷 )
ftc2re.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
ftc2re.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
ftc2re.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ftc2re.f ⊢ ( 𝜑 → 𝐹 : 𝐸 ⟶ ℂ )
ftc2re.1 ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℂ ) )
Assertion ftc2re ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ftc2re.e ⊢ 𝐸 = ( 𝐶 (,) 𝐷 )
2 ftc2re.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐸 )
3 ftc2re.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐸 )
4 ftc2re.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 ftc2re.f ⊢ ( 𝜑 → 𝐹 : 𝐸 ⟶ ℂ )
6 ftc2re.1 ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℂ ) )
7 ioossre ⊢ ( 𝐶 (,) 𝐷 ) ⊆ ℝ
8 1 7 eqsstri ⊢ 𝐸 ⊆ ℝ
9 8 a1i ⊢ ( 𝜑 → 𝐸 ⊆ ℝ )
10 9 2 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
11 9 3 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
12 ax-resscn ⊢ ℝ ⊆ ℂ
13 12 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
14 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
15 10 11 14 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
16 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
17 16 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
18 16 17 dvres ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : 𝐸 ⟶ ℂ ) ∧ ( 𝐸 ⊆ ℝ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
19 13 5 9 15 18 syl22anc ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) )
20 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
21 10 11 20 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
22 21 reseq2d ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) )
23 19 22 eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) )
24 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
25 24 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
26 1 2 3 fct2relem ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐸 )
27 25 26 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐸 )
28 rescncf ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ 𝐸 → ( ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℂ ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) )
29 27 6 28 sylc ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
30 23 29 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
31 ioombl ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
32 31 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
33 cnmbf ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∈ dom vol ∧ ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ MblFn )
34 32 29 33 syl2anc ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ MblFn )
35 dmres ⊢ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( ( 𝐴 (,) 𝐵 ) ∩ dom ( ℝ D 𝐹 ) )
36 35 fveq2i ⊢ ( vol ‘ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) = ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∩ dom ( ℝ D 𝐹 ) ) )
37 cncff ⊢ ( ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℂ ) → ( ℝ D 𝐹 ) : 𝐸 ⟶ ℂ )
38 6 37 syl ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : 𝐸 ⟶ ℂ )
39 38 fdmd ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = 𝐸 )
40 39 ineq2d ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∩ dom ( ℝ D 𝐹 ) ) = ( ( 𝐴 (,) 𝐵 ) ∩ 𝐸 ) )
41 df-ss ⊢ ( ( 𝐴 (,) 𝐵 ) ⊆ 𝐸 ↔ ( ( 𝐴 (,) 𝐵 ) ∩ 𝐸 ) = ( 𝐴 (,) 𝐵 ) )
42 27 41 sylib ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∩ 𝐸 ) = ( 𝐴 (,) 𝐵 ) )
43 40 42 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∩ dom ( ℝ D 𝐹 ) ) = ( 𝐴 (,) 𝐵 ) )
44 43 fveq2d ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∩ dom ( ℝ D 𝐹 ) ) ) = ( vol ‘ ( 𝐴 (,) 𝐵 ) ) )
45 volioo ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
46 10 11 4 45 syl3anc ⊢ ( 𝜑 → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
47 11 10 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
48 46 47 eqeltrd ⊢ ( 𝜑 → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )
49 44 48 eqeltrd ⊢ ( 𝜑 → ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∩ dom ( ℝ D 𝐹 ) ) ) ∈ ℝ )
50 36 49 eqeltrid ⊢ ( 𝜑 → ( vol ‘ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) ∈ ℝ )
51 rescncf ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐸 → ( ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℂ ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) )
52 26 51 syl ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ∈ ( 𝐸 –cn→ ℂ ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) )
53 6 52 mpd ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
54 cniccbdd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 )
55 10 11 53 54 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 )
56 35 43 syl5eq ⊢ ( 𝜑 → dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
57 56 25 eqsstrd ⊢ ( 𝜑 → dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
58 ssralv ⊢ ( dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 → ∀ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) )
59 57 58 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 → ∀ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 → ∀ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) )
61 57 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
62 61 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
63 fvres ⊢ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ 𝑦 ) )
64 62 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ 𝑦 ) )
65 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) → 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) )
66 56 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) → dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
67 65 66 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) → 𝑦 ∈ ( 𝐴 (,) 𝐵 ) )
68 fvres ⊢ ( 𝑦 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ 𝑦 ) )
69 67 68 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) = ( ( ℝ D 𝐹 ) ‘ 𝑦 ) )
70 64 69 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) = ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) )
71 70 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) → ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) = ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) )
72 71 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) → ( ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 ↔ ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) )
73 72 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) → ( ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 → ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) )
74 73 ralimdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 → ∀ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) )
75 60 74 syld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 → ∀ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) )
76 75 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) )
77 55 76 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 )
78 bddibl ⊢ ( ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ MblFn ∧ ( vol ‘ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ( abs ‘ ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑦 ) ) ≤ 𝑥 ) → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ 𝐿1 )
79 34 50 77 78 syl3anc ⊢ ( 𝜑 → ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ∈ 𝐿1 )
80 23 79 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ∈ 𝐿1 )
81 dvcn ⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : 𝐸 ⟶ ℂ ∧ 𝐸 ⊆ ℝ ) ∧ dom ( ℝ D 𝐹 ) = 𝐸 ) → 𝐹 ∈ ( 𝐸 –cn→ ℂ ) )
82 13 5 9 39 81 syl31anc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 –cn→ ℂ ) )
83 rescncf ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐸 → ( 𝐹 ∈ ( 𝐸 –cn→ ℂ ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) )
84 26 83 syl ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐸 –cn→ ℂ ) → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) )
85 82 84 mpd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
86 10 11 4 30 80 85 ftc2 ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) d 𝑡 = ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) )
87 23 fveq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) = ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑡 ) )
88 fvres ⊢ ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) → ( ( ( ℝ D 𝐹 ) ↾ ( 𝐴 (,) 𝐵 ) ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
89 87 88 sylan9eq ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
90 89 ralrimiva ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
91 itgeq2 ⊢ ( ∀ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
92 90 91 syl ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
93 10 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
94 11 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
95 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
96 93 94 4 95 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
97 96 fvresd ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
98 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
99 93 94 4 98 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
100 99 fvresd ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
101 97 100 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐵 ) − ( ( 𝐹 ↾ ( 𝐴 [,] 𝐵 ) ) ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
102 86 92 101 3eqtr3d ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )