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