This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ftc1lem1

Description: Lemma for ftc1a and ftc1 . (Contributed by Mario Carneiro, 31-Aug-2014)

Ref Expression
Hypotheses ftc1.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
ftc1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ftc1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ftc1.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ftc1.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
ftc1.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
ftc1.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
ftc1a.f ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
ftc1lem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
ftc1lem1.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
Assertion ftc1lem1 ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )

Proof

Step Hyp Ref Expression
1 ftc1.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2 ftc1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ftc1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 ftc1.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 ftc1.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
6 ftc1.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
7 ftc1.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
8 ftc1a.f ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
9 ftc1lem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )
10 ftc1lem1.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 [,] 𝐵 ) )
11 oveq2 ⊢ ( 𝑥 = 𝑌 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑌 ) )
12 itgeq1 ⊢ ( ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑌 ) → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
13 11 12 syl ⊢ ( 𝑥 = 𝑌 → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
14 itgex ⊢ ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ V
15 13 1 14 fvmpt ⊢ ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐺 ‘ 𝑌 ) = ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
16 10 15 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝐺 ‘ 𝑌 ) = ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
18 2 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝐴 ∈ ℝ )
19 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
20 2 3 19 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
21 20 10 sseldd ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ ℝ )
23 20 9 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ ℝ )
25 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
26 2 3 25 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
27 9 26 mpbid ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) )
28 27 simp2d ⊢ ( 𝜑 → 𝐴 ≤ 𝑋 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝐴 ≤ 𝑋 )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 )
31 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( 𝑋 ∈ ( 𝐴 [,] 𝑌 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) )
32 2 21 31 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 [,] 𝑌 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ∈ ( 𝐴 [,] 𝑌 ) ↔ ( 𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) ) )
34 24 29 30 33 mpbir3and ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ ( 𝐴 [,] 𝑌 ) )
35 3 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
36 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) ) )
37 2 3 36 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) ) )
38 10 37 mpbid ⊢ ( 𝜑 → ( 𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵 ) )
39 38 simp3d ⊢ ( 𝜑 → 𝑌 ≤ 𝐵 )
40 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑌 ≤ 𝐵 ) → ( 𝐴 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
41 35 39 40 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
42 41 5 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝑌 ) ⊆ 𝐷 )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝐴 (,) 𝑌 ) ⊆ 𝐷 )
44 43 sselda ⊢ ( ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑌 ) ) → 𝑡 ∈ 𝐷 )
45 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
47 44 46 syldan ⊢ ( ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) ∧ 𝑡 ∈ ( 𝐴 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
48 27 simp3d ⊢ ( 𝜑 → 𝑋 ≤ 𝐵 )
49 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑋 ≤ 𝐵 ) → ( 𝐴 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
50 35 48 49 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝑋 ) ⊆ ( 𝐴 (,) 𝐵 ) )
51 50 5 sstrd ⊢ ( 𝜑 → ( 𝐴 (,) 𝑋 ) ⊆ 𝐷 )
52 ioombl ⊢ ( 𝐴 (,) 𝑋 ) ∈ dom vol
53 52 a1i ⊢ ( 𝜑 → ( 𝐴 (,) 𝑋 ) ∈ dom vol )
54 fvexd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
55 8 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) )
56 55 7 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
57 51 53 54 56 iblss ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑡 ∈ ( 𝐴 (,) 𝑋 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
59 2 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
60 iooss1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ) → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝑌 ) )
61 59 28 60 syl2anc ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝑌 ) )
62 61 41 sstrd ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ ( 𝐴 (,) 𝐵 ) )
63 62 5 sstrd ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ⊆ 𝐷 )
64 ioombl ⊢ ( 𝑋 (,) 𝑌 ) ∈ dom vol
65 64 a1i ⊢ ( 𝜑 → ( 𝑋 (,) 𝑌 ) ∈ dom vol )
66 63 65 54 56 iblss ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
68 18 22 34 47 58 67 itgsplitioo ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ∫ ( 𝐴 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ( ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) )
69 17 68 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝐺 ‘ 𝑌 ) = ( ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) )
70 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑋 ) )
71 itgeq1 ⊢ ( ( 𝐴 (,) 𝑥 ) = ( 𝐴 (,) 𝑋 ) → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
72 70 71 syl ⊢ ( 𝑥 = 𝑋 → ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 = ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
73 itgex ⊢ ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ V
74 72 1 73 fvmpt ⊢ ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝐺 ‘ 𝑋 ) = ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
75 9 74 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
76 75 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝐺 ‘ 𝑋 ) = ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
77 69 76 oveq12d ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ( ( ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) )
78 fvexd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 (,) 𝑋 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
79 78 57 itgcl ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ ℂ )
80 63 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → 𝑡 ∈ 𝐷 )
81 80 45 syldan ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑋 (,) 𝑌 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
82 81 66 itgcl ⊢ ( 𝜑 → ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ ℂ )
83 79 82 pncan2d ⊢ ( 𝜑 → ( ( ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
84 83 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 + ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) − ∫ ( 𝐴 (,) 𝑋 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
85 77 84 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ∫ ( 𝑋 (,) 𝑌 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )