Metamath Proof Explorer

Theorem ftc2

Description: The Fundamental Theorem of Calculus, part two. If F is a function continuous on [ A , B ] and continuously differentiable on ( A , B ) , then the integral of the derivative of F is equal to F ( B ) - F ( A ) . This is part of Metamath 100 proof #15. (Contributed by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses ftc2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ftc2.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ftc2.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ftc2.c ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
ftc2.i ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ 𝐿1 )
ftc2.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
Assertion ftc2 ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 ftc2.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ftc2.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ftc2.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 ftc2.c ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
5 ftc2.i ⊢ ( 𝜑 → ( ℝ D 𝐹 ) ∈ 𝐿1 )
6 ftc2.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
7 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
8 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
9 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
10 7 8 3 9 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
11 fvex ⊢ ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) ∈ V
12 11 fvconst2 ⊢ ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) → ( ( ( 𝐴 [,] 𝐵 ) × { ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) } ) ‘ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) )
13 10 12 syl ⊢ ( 𝜑 → ( ( ( 𝐴 [,] 𝐵 ) × { ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) } ) ‘ 𝐵 ) = ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) )
14 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
15 14 subcn ⊢ − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
16 15 a1i ⊢ ( 𝜑 → − ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
17 eqid ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
18 ssidd ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
19 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
20 19 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
21 cncff ⊢ ( ( ℝ D 𝐹 ) ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
22 4 21 syl ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
23 17 1 2 3 18 20 5 22 ftc1a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
24 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
25 6 24 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
26 25 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
27 26 6 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
28 14 16 23 27 cncfmpt2f ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
29 ax-resscn ⊢ ℝ ⊆ ℂ
30 29 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
31 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
32 1 2 31 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
33 fvex ⊢ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V
34 33 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑥 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V )
35 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
36 35 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ* )
37 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
38 1 2 37 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
39 38 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
40 39 simp3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ≤ 𝐵 )
41 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑥 ≤ 𝐵 ) → ( 𝐴 (,) 𝑥 ) ⊆ ( 𝐴 (,) 𝐵 ) )
42 36 40 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑥 ) ⊆ ( 𝐴 (,) 𝐵 ) )
43 ioombl ⊢ ( 𝐴 (,) 𝑥 ) ∈ dom vol
44 43 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 (,) 𝑥 ) ∈ dom vol )
45 33 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V )
46 22 feqmptd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
47 46 5 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿1 )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿1 )
49 42 44 45 48 iblss ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑥 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ∈ 𝐿1 )
50 34 49 itgcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ∈ ℂ )
51 25 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
52 50 51 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
53 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
54 iccntr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
55 1 2 54 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐴 (,) 𝐵 ) )
56 30 32 52 53 14 55 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ) )
57 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
58 57 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
59 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
60 59 sseli ⊢ ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
61 60 50 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ∈ ℂ )
62 22 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
63 17 1 2 3 4 5 ftc1cn ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) = ( ℝ D 𝐹 ) )
64 30 32 50 53 14 55 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) )
65 22 feqmptd ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
66 63 64 65 3eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
67 60 51 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
68 30 32 51 53 14 55 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
69 26 oveq2d ⊢ ( 𝜑 → ( ℝ D 𝐹 ) = ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
70 69 65 eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
71 68 70 eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
72 58 61 62 66 67 62 71 dvmptsub ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
73 62 subidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = 0 )
74 73 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( ℝ D 𝐹 ) ‘ 𝑥 ) − ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
75 56 72 74 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 ) )
76 fconstmpt ⊢ ( ( 𝐴 (,) 𝐵 ) × { 0 } ) = ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 0 )
77 75 76 eqtr4di ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ( 𝐴 (,) 𝐵 ) × { 0 } ) )
78 1 2 28 77 dveq0 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) = ( ( 𝐴 [,] 𝐵 ) × { ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) } ) )
79 78 fveq1d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐵 ) = ( ( ( 𝐴 [,] 𝐵 ) × { ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) } ) ‘ 𝐵 ) )
80 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝐵 ) )
81 itgeq1 ⊢ ( ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝐵 ) → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
82 80 81 syl ⊢ ( 𝑥 = 𝐵 → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
83 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
84 82 83 oveq12d ⊢ ( 𝑥 = 𝐵 → ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) = ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) )
85 eqid ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) )
86 ovex ⊢ ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) ∈ V
87 84 85 86 fvmpt ⊢ ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐵 ) = ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) )
88 10 87 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐵 ) = ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) )
89 79 88 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐴 [,] 𝐵 ) × { ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) } ) ‘ 𝐵 ) = ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) )
90 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
91 7 8 3 90 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
92 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝐴 ) )
93 iooid ⊢ ( 𝐴 (,) 𝐴 ) = ∅
94 92 93 eqtrdi ⊢ ( 𝑥 = 𝐴 → ( 𝐴 (,) 𝑥 ) = ∅ )
95 itgeq1 ⊢ ( ( 𝐴 (,) 𝑥 ) = ∅ → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ∫ ∅ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
96 94 95 syl ⊢ ( 𝑥 = 𝐴 → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ∫ ∅ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
97 itg0 ⊢ ∫ ∅ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = 0
98 96 97 eqtrdi ⊢ ( 𝑥 = 𝐴 → ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = 0 )
99 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
100 98 99 oveq12d ⊢ ( 𝑥 = 𝐴 → ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) = ( 0 − ( 𝐹 ‘ 𝐴 ) ) )
101 df-neg ⊢ - ( 𝐹 ‘ 𝐴 ) = ( 0 − ( 𝐹 ‘ 𝐴 ) )
102 100 101 eqtr4di ⊢ ( 𝑥 = 𝐴 → ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) = - ( 𝐹 ‘ 𝐴 ) )
103 negex ⊢ - ( 𝐹 ‘ 𝐴 ) ∈ V
104 102 85 103 fvmpt ⊢ ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) = - ( 𝐹 ‘ 𝐴 ) )
105 91 104 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ∫ ( 𝐴 (,) 𝑥 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝐴 ) = - ( 𝐹 ‘ 𝐴 ) )
106 13 89 105 3eqtr3d ⊢ ( 𝜑 → ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) = - ( 𝐹 ‘ 𝐴 ) )
107 106 oveq2d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) + ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) ) = ( ( 𝐹 ‘ 𝐵 ) + - ( 𝐹 ‘ 𝐴 ) ) )
108 25 10 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
109 33 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ∈ V )
110 109 47 itgcl ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 ∈ ℂ )
111 108 110 pncan3d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) + ( ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 − ( 𝐹 ‘ 𝐵 ) ) ) = ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 )
112 25 91 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
113 108 112 negsubd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) + - ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )
114 107 111 113 3eqtr3d ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) ( ( ℝ D 𝐹 ) ‘ 𝑡 ) d 𝑡 = ( ( 𝐹 ‘ 𝐵 ) − ( 𝐹 ‘ 𝐴 ) ) )