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 𝑡 = ( ( 𝐹𝐵 ) − ( 𝐹𝐴 ) ) )