Metamath Proof Explorer

Theorem itgparts

Description: Integration by parts. If B ( x ) is the derivative of A ( x ) and D ( x ) is the derivative of C ( x ) , and E = ( A x. B ) ( X ) and F = ( A x. B ) ( Y ) , then under suitable integrability and differentiability assumptions, the integral of A x. D from X to Y is equal to F - E minus the integral of B x. C . (Contributed by Mario Carneiro, 3-Sep-2014)

Ref Expression
Hypotheses itgparts.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
itgparts.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
itgparts.le ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
itgparts.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
itgparts.c ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
itgparts.b ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
itgparts.d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
itgparts.ad ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐴 · 𝐷 ) ) ∈ 𝐿1 )
itgparts.bc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐵 · 𝐶 ) ) ∈ 𝐿1 )
itgparts.da ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
itgparts.dc ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) )
itgparts.e ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐴 · 𝐶 ) = 𝐸 )
itgparts.f ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝐴 · 𝐶 ) = 𝐹 )
Assertion itgparts ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐴 · 𝐷 ) d 𝑥 = ( ( 𝐹 − 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( 𝐵 · 𝐶 ) d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 itgparts.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2 itgparts.y ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3 itgparts.le ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
4 itgparts.a ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
5 itgparts.c ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
6 itgparts.b ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
7 itgparts.d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
8 itgparts.ad ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐴 · 𝐷 ) ) ∈ 𝐿1 )
9 itgparts.bc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐵 · 𝐶 ) ) ∈ 𝐿1 )
10 itgparts.da ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
11 itgparts.dc ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) )
12 itgparts.e ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐴 · 𝐶 ) = 𝐸 )
13 itgparts.f ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝐴 · 𝐶 ) = 𝐹 )
14 cncff ⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
15 6 14 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
16 15 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐵 ∈ ℂ )
17 ioossicc ⊢ ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 )
18 17 sseli ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) → 𝑥 ∈ ( 𝑋 [,] 𝑌 ) )
19 cncff ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
20 5 19 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
21 20 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐶 ∈ ℂ )
22 18 21 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐶 ∈ ℂ )
23 16 22 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
24 23 9 itgcl ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐵 · 𝐶 ) d 𝑥 ∈ ℂ )
25 cncff ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
26 4 25 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ℂ )
27 26 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → 𝐴 ∈ ℂ )
28 18 27 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐴 ∈ ℂ )
29 cncff ⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
30 7 29 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) : ( 𝑋 (,) 𝑌 ) ⟶ ℂ )
31 30 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝐷 ∈ ℂ )
32 28 31 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
33 32 8 itgcl ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐴 · 𝐷 ) d 𝑥 ∈ ℂ )
34 24 33 pncan2d ⊢ ( 𝜑 → ( ( ∫ ( 𝑋 (,) 𝑌 ) ( 𝐵 · 𝐶 ) d 𝑥 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐴 · 𝐷 ) d 𝑥 ) − ∫ ( 𝑋 (,) 𝑌 ) ( 𝐵 · 𝐶 ) d 𝑥 ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐴 · 𝐷 ) d 𝑥 )
35 23 9 32 8 itgadd ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) d 𝑥 = ( ∫ ( 𝑋 (,) 𝑌 ) ( 𝐵 · 𝐶 ) d 𝑥 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐴 · 𝐷 ) d 𝑥 ) )
36 fveq2 ⊢ ( 𝑥 = 𝑡 → ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑥 ) = ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑡 ) )
37 nfcv ⊢ Ⅎ 𝑡 ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑥 )
38 nfcv ⊢ Ⅎ 𝑥 ℝ
39 nfcv ⊢ Ⅎ 𝑥 D
40 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) )
41 38 39 40 nfov ⊢ Ⅎ 𝑥 ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) )
42 nfcv ⊢ Ⅎ 𝑥 𝑡
43 41 42 nffv ⊢ Ⅎ 𝑥 ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑡 )
44 36 37 43 cbvitg ⊢ ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑡 ) d 𝑡
45 ax-resscn ⊢ ℝ ⊆ ℂ
46 45 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
47 iccssre ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
48 1 2 47 syl2anc ⊢ ( 𝜑 → ( 𝑋 [,] 𝑌 ) ⊆ ℝ )
49 27 21 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
50 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
51 50 tgioo2 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
52 iccntr ⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) = ( 𝑋 (,) 𝑌 ) )
53 1 2 52 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝑋 [,] 𝑌 ) ) = ( 𝑋 (,) 𝑌 ) )
54 46 48 49 51 50 53 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) = ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) )
55 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
56 55 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
57 46 48 27 51 50 53 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐴 ) ) )
58 57 10 eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
59 46 48 21 51 50 53 dvmptntr ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ) = ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) ) )
60 59 11 eqtr3d ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐷 ) )
61 56 28 16 58 22 31 60 dvmptmul ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) )
62 31 28 mulcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐷 · 𝐴 ) = ( 𝐴 · 𝐷 ) )
63 62 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) = ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) )
64 63 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ) )
65 54 61 64 3eqtrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ) )
66 50 addcn ⊢ + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
67 66 a1i ⊢ ( 𝜑 → + ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
68 resmpt ⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) )
69 17 68 ax-mp ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 )
70 rescncf ⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) )
71 17 5 70 mpsyl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐶 ) ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
72 69 71 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐶 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
73 6 72 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐵 · 𝐶 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
74 resmpt ⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐴 ) )
75 17 74 ax-mp ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ↾ ( 𝑋 (,) 𝑌 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐴 )
76 rescncf ⊢ ( ( 𝑋 (,) 𝑌 ) ⊆ ( 𝑋 [,] 𝑌 ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ) )
77 17 4 76 mpsyl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ↾ ( 𝑋 (,) 𝑌 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
78 75 77 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
79 78 7 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐴 · 𝐷 ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
80 50 67 73 79 cncfmpt2f ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
81 65 80 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ∈ ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) )
82 23 9 32 8 ibladd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ) ∈ 𝐿1 )
83 65 82 eqeltrd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ∈ 𝐿1 )
84 4 5 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ℂ ) )
85 1 2 3 81 83 84 ftc2 ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑡 ) d 𝑡 = ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑌 ) − ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑋 ) ) )
86 44 85 syl5eq ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑥 ) d 𝑥 = ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑌 ) − ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑋 ) ) )
87 65 fveq1d ⊢ ( 𝜑 → ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ) ‘ 𝑥 ) )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ) ‘ 𝑥 ) )
89 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑥 ∈ ( 𝑋 (,) 𝑌 ) )
90 ovex ⊢ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ∈ V
91 eqid ⊢ ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) )
92 91 fvmpt2 ⊢ ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ∧ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ∈ V ) → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ) ‘ 𝑥 ) = ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) )
93 89 90 92 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) ) ‘ 𝑥 ) = ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) )
94 88 93 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ) → ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑥 ) = ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) )
95 94 itgeq2dv ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) d 𝑥 )
96 1 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
97 2 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
98 ubicc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
99 96 97 3 98 syl3anc ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
100 ovex ⊢ ( 𝐴 · 𝐶 ) ∈ V
101 100 csbex ⊢ ⦋ 𝑌 / 𝑥 ⦌ ( 𝐴 · 𝐶 ) ∈ V
102 eqid ⊢ ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) )
103 102 fvmpts ⊢ ( ( 𝑌 ∈ ( 𝑋 [,] 𝑌 ) ∧ ⦋ 𝑌 / 𝑥 ⦌ ( 𝐴 · 𝐶 ) ∈ V ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑌 ) = ⦋ 𝑌 / 𝑥 ⦌ ( 𝐴 · 𝐶 ) )
104 99 101 103 sylancl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑌 ) = ⦋ 𝑌 / 𝑥 ⦌ ( 𝐴 · 𝐶 ) )
105 2 13 csbied ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ ( 𝐴 · 𝐶 ) = 𝐹 )
106 104 105 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑌 ) = 𝐹 )
107 lbicc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) )
108 96 97 3 107 syl3anc ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 [,] 𝑌 ) )
109 100 csbex ⊢ ⦋ 𝑋 / 𝑥 ⦌ ( 𝐴 · 𝐶 ) ∈ V
110 102 fvmpts ⊢ ( ( 𝑋 ∈ ( 𝑋 [,] 𝑌 ) ∧ ⦋ 𝑋 / 𝑥 ⦌ ( 𝐴 · 𝐶 ) ∈ V ) → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑋 ) = ⦋ 𝑋 / 𝑥 ⦌ ( 𝐴 · 𝐶 ) )
111 108 109 110 sylancl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑋 ) = ⦋ 𝑋 / 𝑥 ⦌ ( 𝐴 · 𝐶 ) )
112 1 12 csbied ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ ( 𝐴 · 𝐶 ) = 𝐸 )
113 111 112 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑋 ) = 𝐸 )
114 106 113 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑌 ) − ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ ( 𝐴 · 𝐶 ) ) ‘ 𝑋 ) ) = ( 𝐹 − 𝐸 ) )
115 86 95 114 3eqtr3d ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( ( 𝐵 · 𝐶 ) + ( 𝐴 · 𝐷 ) ) d 𝑥 = ( 𝐹 − 𝐸 ) )
116 35 115 eqtr3d ⊢ ( 𝜑 → ( ∫ ( 𝑋 (,) 𝑌 ) ( 𝐵 · 𝐶 ) d 𝑥 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐴 · 𝐷 ) d 𝑥 ) = ( 𝐹 − 𝐸 ) )
117 116 oveq1d ⊢ ( 𝜑 → ( ( ∫ ( 𝑋 (,) 𝑌 ) ( 𝐵 · 𝐶 ) d 𝑥 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐴 · 𝐷 ) d 𝑥 ) − ∫ ( 𝑋 (,) 𝑌 ) ( 𝐵 · 𝐶 ) d 𝑥 ) = ( ( 𝐹 − 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( 𝐵 · 𝐶 ) d 𝑥 ) )
118 34 117 eqtr3d ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐴 · 𝐷 ) d 𝑥 = ( ( 𝐹 − 𝐸 ) − ∫ ( 𝑋 (,) 𝑌 ) ( 𝐵 · 𝐶 ) d 𝑥 ) )