Proof of Theorem ftc1lem5
| Step | Hyp | Ref
| Expression |
| 1 | | ftc1.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 2 | | ftc1.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 3 | | iccssre 13469 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
| 4 | 1, 2, 3 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
| 5 | | ftc1.x1 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) |
| 6 | 4, 5 | sseldd 3984 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 7 | | ioossicc 13473 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
| 8 | | ftc1.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) |
| 9 | 7, 8 | sselid 3981 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) |
| 10 | 4, 9 | sseldd 3984 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 11 | 6, 10 | lttri2d 11400 |
. . 3
⊢ (𝜑 → (𝑋 ≠ 𝐶 ↔ (𝑋 < 𝐶 ∨ 𝐶 < 𝑋))) |
| 12 | 11 | biimpa 476 |
. 2
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐶) → (𝑋 < 𝐶 ∨ 𝐶 < 𝑋)) |
| 13 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → 𝑋 ∈ (𝐴[,]𝐵)) |
| 14 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → 𝑋 ∈ ℝ) |
| 15 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → 𝑋 < 𝐶) |
| 16 | 14, 15 | ltned 11397 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → 𝑋 ≠ 𝐶) |
| 17 | | eldifsn 4786 |
. . . . . . . 8
⊢ (𝑋 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↔ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑋 ≠ 𝐶)) |
| 18 | 13, 16, 17 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → 𝑋 ∈ ((𝐴[,]𝐵) ∖ {𝐶})) |
| 19 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑋 → (𝐺‘𝑧) = (𝐺‘𝑋)) |
| 20 | 19 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑧 = 𝑋 → ((𝐺‘𝑧) − (𝐺‘𝐶)) = ((𝐺‘𝑋) − (𝐺‘𝐶))) |
| 21 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑧 = 𝑋 → (𝑧 − 𝐶) = (𝑋 − 𝐶)) |
| 22 | 20, 21 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑧 = 𝑋 → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) = (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶))) |
| 23 | | ftc1.h |
. . . . . . . 8
⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) |
| 24 | | ovex 7464 |
. . . . . . . 8
⊢ (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶)) ∈ V |
| 25 | 22, 23, 24 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑋 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) → (𝐻‘𝑋) = (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶))) |
| 26 | 18, 25 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (𝐻‘𝑋) = (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶))) |
| 27 | | ftc1.g |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) |
| 28 | | ftc1.le |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 29 | | ftc1.s |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) |
| 30 | | ftc1.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
| 31 | | ftc1.i |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
| 32 | | ftc1.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) |
| 33 | | ftc1.j |
. . . . . . . . . . . 12
⊢ 𝐽 = (𝐿 ↾t
ℝ) |
| 34 | | ftc1.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (𝐿 ↾t 𝐷) |
| 35 | | ftc1.l |
. . . . . . . . . . . 12
⊢ 𝐿 =
(TopOpen‘ℂfld) |
| 36 | 27, 1, 2, 28, 29, 30, 31, 8, 32, 33, 34, 35 | ftc1lem3 26079 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) |
| 37 | 27, 1, 2, 28, 29, 30, 31, 36 | ftc1lem2 26077 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
| 38 | 37, 5 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝑋) ∈ ℂ) |
| 39 | 37, 9 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ) |
| 40 | 38, 39 | subcld 11620 |
. . . . . . . 8
⊢ (𝜑 → ((𝐺‘𝑋) − (𝐺‘𝐶)) ∈ ℂ) |
| 41 | 40 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → ((𝐺‘𝑋) − (𝐺‘𝐶)) ∈ ℂ) |
| 42 | 6 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℂ) |
| 43 | 10 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 44 | 42, 43 | subcld 11620 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 − 𝐶) ∈ ℂ) |
| 45 | 44 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (𝑋 − 𝐶) ∈ ℂ) |
| 46 | 42, 43 | subeq0ad 11630 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 − 𝐶) = 0 ↔ 𝑋 = 𝐶)) |
| 47 | 46 | necon3bid 2985 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 − 𝐶) ≠ 0 ↔ 𝑋 ≠ 𝐶)) |
| 48 | 47 | biimpar 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐶) → (𝑋 − 𝐶) ≠ 0) |
| 49 | 16, 48 | syldan 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (𝑋 − 𝐶) ≠ 0) |
| 50 | 41, 45, 49 | div2negd 12058 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (-((𝐺‘𝑋) − (𝐺‘𝐶)) / -(𝑋 − 𝐶)) = (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶))) |
| 51 | 38, 39 | negsubdi2d 11636 |
. . . . . . . 8
⊢ (𝜑 → -((𝐺‘𝑋) − (𝐺‘𝐶)) = ((𝐺‘𝐶) − (𝐺‘𝑋))) |
| 52 | 42, 43 | negsubdi2d 11636 |
. . . . . . . 8
⊢ (𝜑 → -(𝑋 − 𝐶) = (𝐶 − 𝑋)) |
| 53 | 51, 52 | oveq12d 7449 |
. . . . . . 7
⊢ (𝜑 → (-((𝐺‘𝑋) − (𝐺‘𝐶)) / -(𝑋 − 𝐶)) = (((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋))) |
| 54 | 53 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (-((𝐺‘𝑋) − (𝐺‘𝐶)) / -(𝑋 − 𝐶)) = (((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋))) |
| 55 | 26, 50, 54 | 3eqtr2d 2783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (𝐻‘𝑋) = (((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋))) |
| 56 | 55 | fvoveq1d 7453 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) = (abs‘((((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋)) − (𝐹‘𝐶)))) |
| 57 | | ftc1.e |
. . . . 5
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 58 | | ftc1.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
| 59 | | ftc1.fc |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((abs‘(𝑦 − 𝐶)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝐸)) |
| 60 | | ftc1.x2 |
. . . . 5
⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) < 𝑅) |
| 61 | 43 | subidd 11608 |
. . . . . . 7
⊢ (𝜑 → (𝐶 − 𝐶) = 0) |
| 62 | 61 | abs00bd 15330 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐶 − 𝐶)) = 0) |
| 63 | 58 | rpgt0d 13080 |
. . . . . 6
⊢ (𝜑 → 0 < 𝑅) |
| 64 | 62, 63 | eqbrtrd 5165 |
. . . . 5
⊢ (𝜑 → (abs‘(𝐶 − 𝐶)) < 𝑅) |
| 65 | 27, 1, 2, 28, 29, 30, 31, 8, 32, 33, 34, 35, 23, 57, 58, 59, 5, 60, 9, 64 | ftc1lem4 26080 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (abs‘((((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋)) − (𝐹‘𝐶))) < 𝐸) |
| 66 | 56, 65 | eqbrtrd 5165 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) < 𝐸) |
| 67 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → 𝑋 ∈ (𝐴[,]𝐵)) |
| 68 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → 𝐶 ∈ ℝ) |
| 69 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → 𝐶 < 𝑋) |
| 70 | 68, 69 | gtned 11396 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → 𝑋 ≠ 𝐶) |
| 71 | 67, 70, 17 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → 𝑋 ∈ ((𝐴[,]𝐵) ∖ {𝐶})) |
| 72 | 71, 25 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → (𝐻‘𝑋) = (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶))) |
| 73 | 72 | fvoveq1d 7453 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) = (abs‘((((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶)) − (𝐹‘𝐶)))) |
| 74 | 27, 1, 2, 28, 29, 30, 31, 8, 32, 33, 34, 35, 23, 57, 58, 59, 9, 64, 5, 60 | ftc1lem4 26080 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → (abs‘((((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶)) − (𝐹‘𝐶))) < 𝐸) |
| 75 | 73, 74 | eqbrtrd 5165 |
. . 3
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) < 𝐸) |
| 76 | 66, 75 | jaodan 960 |
. 2
⊢ ((𝜑 ∧ (𝑋 < 𝐶 ∨ 𝐶 < 𝑋)) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) < 𝐸) |
| 77 | 12, 76 | syldan 591 |
1
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐶) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) < 𝐸) |