Proof of Theorem ftc1lem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ftc1lem1.y | . . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝐴[,]𝐵)) | 
| 2 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑥 = 𝑌 → (𝐴(,)𝑥) = (𝐴(,)𝑌)) | 
| 3 |  | itgeq1 25809 | . . . . . . . 8
⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑌) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑌)(𝐹‘𝑡) d𝑡) | 
| 4 | 2, 3 | syl 17 | . . . . . . 7
⊢ (𝑥 = 𝑌 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑌)(𝐹‘𝑡) d𝑡) | 
| 5 |  | ftc1.g | . . . . . . 7
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) | 
| 6 |  | itgex 25806 | . . . . . . 7
⊢
∫(𝐴(,)𝑌)(𝐹‘𝑡) d𝑡 ∈ V | 
| 7 | 4, 5, 6 | fvmpt 7015 | . . . . . 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 13470 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) | 
| 14 | 10, 12, 13 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) | 
| 15 | 14, 1 | sseldd 3983 | . . . . . 6
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 16 | 15 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → 𝑌 ∈ ℝ) | 
| 17 |  | ftc1lem1.x | . . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) | 
| 18 | 14, 17 | sseldd 3983 | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 19 | 18 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → 𝑋 ∈ ℝ) | 
| 20 |  | elicc2 13453 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))) | 
| 21 | 10, 12, 20 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 ∈ (𝐴[,]𝐵) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵))) | 
| 22 | 17, 21 | mpbid 232 | . . . . . . . 8
⊢ (𝜑 → (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵)) | 
| 23 | 22 | simp2d 1143 | . . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝑋) | 
| 24 | 23 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → 𝐴 ≤ 𝑋) | 
| 25 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → 𝑋 ≤ 𝑌) | 
| 26 |  | elicc2 13453 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋 ∈ (𝐴[,]𝑌) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌))) | 
| 27 | 10, 15, 26 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝑋 ∈ (𝐴[,]𝑌) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌))) | 
| 28 | 27 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → (𝑋 ∈ (𝐴[,]𝑌) ↔ (𝑋 ∈ ℝ ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌))) | 
| 29 | 19, 24, 25, 28 | mpbir3and 1342 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → 𝑋 ∈ (𝐴[,]𝑌)) | 
| 30 | 12 | rexrd 11312 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈
ℝ*) | 
| 31 |  | elicc2 13453 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑌 ∈ (𝐴[,]𝐵) ↔ (𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵))) | 
| 32 | 10, 12, 31 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ∈ (𝐴[,]𝐵) ↔ (𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵))) | 
| 33 | 1, 32 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝐴 ≤ 𝑌 ∧ 𝑌 ≤ 𝐵)) | 
| 34 | 33 | simp3d 1144 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ≤ 𝐵) | 
| 35 |  | iooss2 13424 | . . . . . . . . . 10
⊢ ((𝐵 ∈ ℝ*
∧ 𝑌 ≤ 𝐵) → (𝐴(,)𝑌) ⊆ (𝐴(,)𝐵)) | 
| 36 | 30, 34, 35 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝑌) ⊆ (𝐴(,)𝐵)) | 
| 37 |  | ftc1.s | . . . . . . . . 9
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) | 
| 38 | 36, 37 | sstrd 3993 | . . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝑌) ⊆ 𝐷) | 
| 39 | 38 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → (𝐴(,)𝑌) ⊆ 𝐷) | 
| 40 | 39 | sselda 3982 | . . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≤ 𝑌) ∧ 𝑡 ∈ (𝐴(,)𝑌)) → 𝑡 ∈ 𝐷) | 
| 41 |  | ftc1a.f | . . . . . . . 8
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) | 
| 42 | 41 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) | 
| 43 | 42 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ 𝑋 ≤ 𝑌) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) | 
| 44 | 40, 43 | syldan 591 | . . . . 5
⊢ (((𝜑 ∧ 𝑋 ≤ 𝑌) ∧ 𝑡 ∈ (𝐴(,)𝑌)) → (𝐹‘𝑡) ∈ ℂ) | 
| 45 | 22 | simp3d 1144 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ≤ 𝐵) | 
| 46 |  | iooss2 13424 | . . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝑋 ≤ 𝐵) → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵)) | 
| 47 | 30, 45, 46 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐴(,)𝑋) ⊆ (𝐴(,)𝐵)) | 
| 48 | 47, 37 | sstrd 3993 | . . . . . . 7
⊢ (𝜑 → (𝐴(,)𝑋) ⊆ 𝐷) | 
| 49 |  | ioombl 25601 | . . . . . . . 8
⊢ (𝐴(,)𝑋) ∈ dom vol | 
| 50 | 49 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (𝐴(,)𝑋) ∈ dom vol) | 
| 51 |  | fvexd 6920 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ V) | 
| 52 | 41 | feqmptd 6976 | . . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) | 
| 53 |  | ftc1.i | . . . . . . . 8
⊢ (𝜑 → 𝐹 ∈
𝐿1) | 
| 54 | 52, 53 | eqeltrrd 2841 | . . . . . . 7
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) | 
| 55 | 48, 50, 51, 54 | iblss 25841 | . . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑡)) ∈
𝐿1) | 
| 56 | 55 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → (𝑡 ∈ (𝐴(,)𝑋) ↦ (𝐹‘𝑡)) ∈
𝐿1) | 
| 57 | 10 | rexrd 11312 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ*) | 
| 58 |  | iooss1 13423 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ*
∧ 𝐴 ≤ 𝑋) → (𝑋(,)𝑌) ⊆ (𝐴(,)𝑌)) | 
| 59 | 57, 23, 58 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝐴(,)𝑌)) | 
| 60 | 59, 36 | sstrd 3993 | . . . . . . . 8
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ (𝐴(,)𝐵)) | 
| 61 | 60, 37 | sstrd 3993 | . . . . . . 7
⊢ (𝜑 → (𝑋(,)𝑌) ⊆ 𝐷) | 
| 62 |  | ioombl 25601 | . . . . . . . 8
⊢ (𝑋(,)𝑌) ∈ dom vol | 
| 63 | 62 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (𝑋(,)𝑌) ∈ dom vol) | 
| 64 | 61, 63, 51, 54 | iblss 25841 | . . . . . 6
⊢ (𝜑 → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑡)) ∈
𝐿1) | 
| 65 | 64 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → (𝑡 ∈ (𝑋(,)𝑌) ↦ (𝐹‘𝑡)) ∈
𝐿1) | 
| 66 | 11, 16, 29, 44, 56, 65 | itgsplitioo 25874 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ∫(𝐴(,)𝑌)(𝐹‘𝑡) d𝑡 = (∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡 + ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡)) | 
| 67 | 9, 66 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → (𝐺‘𝑌) = (∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡 + ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡)) | 
| 68 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐴(,)𝑥) = (𝐴(,)𝑋)) | 
| 69 |  | itgeq1 25809 | . . . . . . 7
⊢ ((𝐴(,)𝑥) = (𝐴(,)𝑋) → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡) | 
| 70 | 68, 69 | syl 17 | . . . . . 6
⊢ (𝑥 = 𝑋 → ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡 = ∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡) | 
| 71 |  | itgex 25806 | . . . . . 6
⊢
∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡 ∈ V | 
| 72 | 70, 5, 71 | fvmpt 7015 | . . . . 5
⊢ (𝑋 ∈ (𝐴[,]𝐵) → (𝐺‘𝑋) = ∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡) | 
| 73 | 17, 72 | syl 17 | . . . 4
⊢ (𝜑 → (𝐺‘𝑋) = ∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡) | 
| 74 | 73 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → (𝐺‘𝑋) = ∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡) | 
| 75 | 67, 74 | oveq12d 7450 | . 2
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ((∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡 + ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡)) | 
| 76 |  | fvexd 6920 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝐴(,)𝑋)) → (𝐹‘𝑡) ∈ V) | 
| 77 | 76, 55 | itgcl 25820 | . . . 4
⊢ (𝜑 → ∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡 ∈ ℂ) | 
| 78 | 61 | sselda 3982 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → 𝑡 ∈ 𝐷) | 
| 79 | 78, 42 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑋(,)𝑌)) → (𝐹‘𝑡) ∈ ℂ) | 
| 80 | 79, 64 | itgcl 25820 | . . . 4
⊢ (𝜑 → ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡 ∈ ℂ) | 
| 81 | 77, 80 | pncan2d 11623 | . . 3
⊢ (𝜑 → ((∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡 + ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡) | 
| 82 | 81 | adantr 480 | . 2
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ((∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡 + ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡) − ∫(𝐴(,)𝑋)(𝐹‘𝑡) d𝑡) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡) | 
| 83 | 75, 82 | eqtrd 2776 | 1
⊢ ((𝜑 ∧ 𝑋 ≤ 𝑌) → ((𝐺‘𝑌) − (𝐺‘𝑋)) = ∫(𝑋(,)𝑌)(𝐹‘𝑡) d𝑡) |