Proof of Theorem ftc1lem5
Step | Hyp | Ref
| Expression |
1 | | ftc1.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | ftc1.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | iccssre 12255 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
4 | 1, 2, 3 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
5 | | ftc1.x1 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝐴[,]𝐵)) |
6 | 4, 5 | sseldd 3604 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) |
7 | | ioossicc 12259 |
. . . . . 6
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
8 | | ftc1.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ (𝐴(,)𝐵)) |
9 | 7, 8 | sseldi 3601 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) |
10 | 4, 9 | sseldd 3604 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ ℝ) |
11 | 6, 10 | lttri2d 10176 |
. . 3
⊢ (𝜑 → (𝑋 ≠ 𝐶 ↔ (𝑋 < 𝐶 ∨ 𝐶 < 𝑋))) |
12 | 11 | biimpa 501 |
. 2
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐶) → (𝑋 < 𝐶 ∨ 𝐶 < 𝑋)) |
13 | 5 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → 𝑋 ∈ (𝐴[,]𝐵)) |
14 | 6 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → 𝑋 ∈ ℝ) |
15 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → 𝑋 < 𝐶) |
16 | 14, 15 | ltned 10173 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → 𝑋 ≠ 𝐶) |
17 | | eldifsn 4317 |
. . . . . . . . 9
⊢ (𝑋 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↔ (𝑋 ∈ (𝐴[,]𝐵) ∧ 𝑋 ≠ 𝐶)) |
18 | 13, 16, 17 | sylanbrc 698 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → 𝑋 ∈ ((𝐴[,]𝐵) ∖ {𝐶})) |
19 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑋 → (𝐺‘𝑧) = (𝐺‘𝑋)) |
20 | 19 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑋 → ((𝐺‘𝑧) − (𝐺‘𝐶)) = ((𝐺‘𝑋) − (𝐺‘𝐶))) |
21 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑋 → (𝑧 − 𝐶) = (𝑋 − 𝐶)) |
22 | 20, 21 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑧 = 𝑋 → (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶)) = (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶))) |
23 | | ftc1.h |
. . . . . . . . 9
⊢ 𝐻 = (𝑧 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) ↦ (((𝐺‘𝑧) − (𝐺‘𝐶)) / (𝑧 − 𝐶))) |
24 | | ovex 6678 |
. . . . . . . . 9
⊢ (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶)) ∈ V |
25 | 22, 23, 24 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑋 ∈ ((𝐴[,]𝐵) ∖ {𝐶}) → (𝐻‘𝑋) = (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶))) |
26 | 18, 25 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (𝐻‘𝑋) = (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶))) |
27 | | ftc1.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) |
28 | | ftc1.le |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
29 | | ftc1.s |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) |
30 | | ftc1.d |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
31 | | ftc1.i |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
32 | | ftc1.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ ((𝐾 CnP 𝐿)‘𝐶)) |
33 | | ftc1.j |
. . . . . . . . . . . . 13
⊢ 𝐽 = (𝐿 ↾t
ℝ) |
34 | | ftc1.k |
. . . . . . . . . . . . 13
⊢ 𝐾 = (𝐿 ↾t 𝐷) |
35 | | ftc1.l |
. . . . . . . . . . . . 13
⊢ 𝐿 =
(TopOpen‘ℂfld) |
36 | 27, 1, 2, 28, 29, 30, 31, 8, 32, 33, 34, 35 | ftc1lem3 23801 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) |
37 | 27, 1, 2, 28, 29, 30, 31, 36 | ftc1lem2 23799 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺:(𝐴[,]𝐵)⟶ℂ) |
38 | 37, 5 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑋) ∈ ℂ) |
39 | 37, 9 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝐶) ∈ ℂ) |
40 | 38, 39 | subcld 10392 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐺‘𝑋) − (𝐺‘𝐶)) ∈ ℂ) |
41 | 40 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → ((𝐺‘𝑋) − (𝐺‘𝐶)) ∈ ℂ) |
42 | 6 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
43 | 10 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℂ) |
44 | 42, 43 | subcld 10392 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 − 𝐶) ∈ ℂ) |
45 | 44 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (𝑋 − 𝐶) ∈ ℂ) |
46 | 42, 43 | subeq0ad 10402 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑋 − 𝐶) = 0 ↔ 𝑋 = 𝐶)) |
47 | 46 | necon3bid 2838 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 − 𝐶) ≠ 0 ↔ 𝑋 ≠ 𝐶)) |
48 | 47 | biimpar 502 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐶) → (𝑋 − 𝐶) ≠ 0) |
49 | 16, 48 | syldan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (𝑋 − 𝐶) ≠ 0) |
50 | 41, 45, 49 | div2negd 10816 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (-((𝐺‘𝑋) − (𝐺‘𝐶)) / -(𝑋 − 𝐶)) = (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶))) |
51 | 38, 39 | negsubdi2d 10408 |
. . . . . . . . 9
⊢ (𝜑 → -((𝐺‘𝑋) − (𝐺‘𝐶)) = ((𝐺‘𝐶) − (𝐺‘𝑋))) |
52 | 42, 43 | negsubdi2d 10408 |
. . . . . . . . 9
⊢ (𝜑 → -(𝑋 − 𝐶) = (𝐶 − 𝑋)) |
53 | 51, 52 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝜑 → (-((𝐺‘𝑋) − (𝐺‘𝐶)) / -(𝑋 − 𝐶)) = (((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋))) |
54 | 53 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (-((𝐺‘𝑋) − (𝐺‘𝐶)) / -(𝑋 − 𝐶)) = (((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋))) |
55 | 26, 50, 54 | 3eqtr2d 2662 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (𝐻‘𝑋) = (((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋))) |
56 | 55 | oveq1d 6665 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → ((𝐻‘𝑋) − (𝐹‘𝐶)) = ((((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋)) − (𝐹‘𝐶))) |
57 | 56 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) = (abs‘((((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋)) − (𝐹‘𝐶)))) |
58 | | ftc1.e |
. . . . 5
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
59 | | ftc1.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
60 | | ftc1.fc |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((abs‘(𝑦 − 𝐶)) < 𝑅 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < 𝐸)) |
61 | | ftc1.x2 |
. . . . 5
⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) < 𝑅) |
62 | 43 | subidd 10380 |
. . . . . . 7
⊢ (𝜑 → (𝐶 − 𝐶) = 0) |
63 | 62 | abs00bd 14031 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐶 − 𝐶)) = 0) |
64 | 59 | rpgt0d 11875 |
. . . . . 6
⊢ (𝜑 → 0 < 𝑅) |
65 | 63, 64 | eqbrtrd 4675 |
. . . . 5
⊢ (𝜑 → (abs‘(𝐶 − 𝐶)) < 𝑅) |
66 | 27, 1, 2, 28, 29, 30, 31, 8, 32, 33, 34, 35, 23, 58, 59, 60, 5, 61, 9, 65 | ftc1lem4 23802 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (abs‘((((𝐺‘𝐶) − (𝐺‘𝑋)) / (𝐶 − 𝑋)) − (𝐹‘𝐶))) < 𝐸) |
67 | 57, 66 | eqbrtrd 4675 |
. . 3
⊢ ((𝜑 ∧ 𝑋 < 𝐶) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) < 𝐸) |
68 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → 𝑋 ∈ (𝐴[,]𝐵)) |
69 | 10 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → 𝐶 ∈ ℝ) |
70 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → 𝐶 < 𝑋) |
71 | 69, 70 | gtned 10172 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → 𝑋 ≠ 𝐶) |
72 | 68, 71, 17 | sylanbrc 698 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → 𝑋 ∈ ((𝐴[,]𝐵) ∖ {𝐶})) |
73 | 72, 25 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → (𝐻‘𝑋) = (((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶))) |
74 | 73 | oveq1d 6665 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → ((𝐻‘𝑋) − (𝐹‘𝐶)) = ((((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶)) − (𝐹‘𝐶))) |
75 | 74 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) = (abs‘((((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶)) − (𝐹‘𝐶)))) |
76 | 27, 1, 2, 28, 29, 30, 31, 8, 32, 33, 34, 35, 23, 58, 59, 60, 9, 65, 5, 61 | ftc1lem4 23802 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → (abs‘((((𝐺‘𝑋) − (𝐺‘𝐶)) / (𝑋 − 𝐶)) − (𝐹‘𝐶))) < 𝐸) |
77 | 75, 76 | eqbrtrd 4675 |
. . 3
⊢ ((𝜑 ∧ 𝐶 < 𝑋) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) < 𝐸) |
78 | 67, 77 | jaodan 826 |
. 2
⊢ ((𝜑 ∧ (𝑋 < 𝐶 ∨ 𝐶 < 𝑋)) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) < 𝐸) |
79 | 12, 78 | syldan 487 |
1
⊢ ((𝜑 ∧ 𝑋 ≠ 𝐶) → (abs‘((𝐻‘𝑋) − (𝐹‘𝐶))) < 𝐸) |