Step | Hyp | Ref
| Expression |
1 | | ftc1.a |
. . . . . 6
β’ (π β π΄ β β) |
2 | | ftc1.b |
. . . . . 6
β’ (π β π΅ β β) |
3 | | iccssre 13355 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
4 | 1, 2, 3 | syl2anc 585 |
. . . . 5
β’ (π β (π΄[,]π΅) β β) |
5 | | ftc1.x1 |
. . . . 5
β’ (π β π β (π΄[,]π΅)) |
6 | 4, 5 | sseldd 3949 |
. . . 4
β’ (π β π β β) |
7 | | ioossicc 13359 |
. . . . . 6
β’ (π΄(,)π΅) β (π΄[,]π΅) |
8 | | ftc1.c |
. . . . . 6
β’ (π β πΆ β (π΄(,)π΅)) |
9 | 7, 8 | sselid 3946 |
. . . . 5
β’ (π β πΆ β (π΄[,]π΅)) |
10 | 4, 9 | sseldd 3949 |
. . . 4
β’ (π β πΆ β β) |
11 | 6, 10 | lttri2d 11302 |
. . 3
β’ (π β (π β πΆ β (π < πΆ β¨ πΆ < π))) |
12 | 11 | biimpa 478 |
. 2
β’ ((π β§ π β πΆ) β (π < πΆ β¨ πΆ < π)) |
13 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π < πΆ) β π β (π΄[,]π΅)) |
14 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π < πΆ) β π β β) |
15 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π < πΆ) β π < πΆ) |
16 | 14, 15 | ltned 11299 |
. . . . . . . 8
β’ ((π β§ π < πΆ) β π β πΆ) |
17 | | eldifsn 4751 |
. . . . . . . 8
β’ (π β ((π΄[,]π΅) β {πΆ}) β (π β (π΄[,]π΅) β§ π β πΆ)) |
18 | 13, 16, 17 | sylanbrc 584 |
. . . . . . 7
β’ ((π β§ π < πΆ) β π β ((π΄[,]π΅) β {πΆ})) |
19 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π§ = π β (πΊβπ§) = (πΊβπ)) |
20 | 19 | oveq1d 7376 |
. . . . . . . . 9
β’ (π§ = π β ((πΊβπ§) β (πΊβπΆ)) = ((πΊβπ) β (πΊβπΆ))) |
21 | | oveq1 7368 |
. . . . . . . . 9
β’ (π§ = π β (π§ β πΆ) = (π β πΆ)) |
22 | 20, 21 | oveq12d 7379 |
. . . . . . . 8
β’ (π§ = π β (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)) = (((πΊβπ) β (πΊβπΆ)) / (π β πΆ))) |
23 | | ftc1.h |
. . . . . . . 8
β’ π» = (π§ β ((π΄[,]π΅) β {πΆ}) β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) |
24 | | ovex 7394 |
. . . . . . . 8
β’ (((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β V |
25 | 22, 23, 24 | fvmpt 6952 |
. . . . . . 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 25425 |
. . . . . . . . . . 11
β’ (π β πΉ:π·βΆβ) |
37 | 27, 1, 2, 28, 29, 30, 31, 36 | ftc1lem2 25423 |
. . . . . . . . . 10
β’ (π β πΊ:(π΄[,]π΅)βΆβ) |
38 | 37, 5 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ (π β (πΊβπ) β β) |
39 | 37, 9 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ (π β (πΊβπΆ) β β) |
40 | 38, 39 | subcld 11520 |
. . . . . . . 8
β’ (π β ((πΊβπ) β (πΊβπΆ)) β β) |
41 | 40 | adantr 482 |
. . . . . . 7
β’ ((π β§ π < πΆ) β ((πΊβπ) β (πΊβπΆ)) β β) |
42 | 6 | recnd 11191 |
. . . . . . . . 9
β’ (π β π β β) |
43 | 10 | recnd 11191 |
. . . . . . . . 9
β’ (π β πΆ β β) |
44 | 42, 43 | subcld 11520 |
. . . . . . . 8
β’ (π β (π β πΆ) β β) |
45 | 44 | adantr 482 |
. . . . . . 7
β’ ((π β§ π < πΆ) β (π β πΆ) β β) |
46 | 42, 43 | subeq0ad 11530 |
. . . . . . . . . 10
β’ (π β ((π β πΆ) = 0 β π = πΆ)) |
47 | 46 | necon3bid 2985 |
. . . . . . . . 9
β’ (π β ((π β πΆ) β 0 β π β πΆ)) |
48 | 47 | biimpar 479 |
. . . . . . . 8
β’ ((π β§ π β πΆ) β (π β πΆ) β 0) |
49 | 16, 48 | syldan 592 |
. . . . . . 7
β’ ((π β§ π < πΆ) β (π β πΆ) β 0) |
50 | 41, 45, 49 | div2negd 11954 |
. . . . . 6
β’ ((π β§ π < πΆ) β (-((πΊβπ) β (πΊβπΆ)) / -(π β πΆ)) = (((πΊβπ) β (πΊβπΆ)) / (π β πΆ))) |
51 | 38, 39 | negsubdi2d 11536 |
. . . . . . . 8
β’ (π β -((πΊβπ) β (πΊβπΆ)) = ((πΊβπΆ) β (πΊβπ))) |
52 | 42, 43 | negsubdi2d 11536 |
. . . . . . . 8
β’ (π β -(π β πΆ) = (πΆ β π)) |
53 | 51, 52 | oveq12d 7379 |
. . . . . . 7
β’ (π β (-((πΊβπ) β (πΊβπΆ)) / -(π β πΆ)) = (((πΊβπΆ) β (πΊβπ)) / (πΆ β π))) |
54 | 53 | adantr 482 |
. . . . . 6
β’ ((π β§ π < πΆ) β (-((πΊβπ) β (πΊβπΆ)) / -(π β πΆ)) = (((πΊβπΆ) β (πΊβπ)) / (πΆ β π))) |
55 | 26, 50, 54 | 3eqtr2d 2779 |
. . . . 5
β’ ((π β§ π < πΆ) β (π»βπ) = (((πΊβπΆ) β (πΊβπ)) / (πΆ β π))) |
56 | 55 | fvoveq1d 7383 |
. . . 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 11508 |
. . . . . . 7
β’ (π β (πΆ β πΆ) = 0) |
62 | 61 | abs00bd 15185 |
. . . . . 6
β’ (π β (absβ(πΆ β πΆ)) = 0) |
63 | 58 | rpgt0d 12968 |
. . . . . 6
β’ (π β 0 < π
) |
64 | 62, 63 | eqbrtrd 5131 |
. . . . 5
β’ (π β (absβ(πΆ β πΆ)) < π
) |
65 | 27, 1, 2, 28, 29, 30, 31, 8, 32, 33, 34, 35, 23, 57, 58, 59, 5, 60, 9, 64 | ftc1lem4 25426 |
. . . 4
β’ ((π β§ π < πΆ) β (absβ((((πΊβπΆ) β (πΊβπ)) / (πΆ β π)) β (πΉβπΆ))) < πΈ) |
66 | 56, 65 | eqbrtrd 5131 |
. . 3
β’ ((π β§ π < πΆ) β (absβ((π»βπ) β (πΉβπΆ))) < πΈ) |
67 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΆ < π) β π β (π΄[,]π΅)) |
68 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΆ < π) β πΆ β β) |
69 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ πΆ < π) β πΆ < π) |
70 | 68, 69 | gtned 11298 |
. . . . . . 7
β’ ((π β§ πΆ < π) β π β πΆ) |
71 | 67, 70, 17 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ πΆ < π) β π β ((π΄[,]π΅) β {πΆ})) |
72 | 71, 25 | syl 17 |
. . . . 5
β’ ((π β§ πΆ < π) β (π»βπ) = (((πΊβπ) β (πΊβπΆ)) / (π β πΆ))) |
73 | 72 | fvoveq1d 7383 |
. . . 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 25426 |
. . . 4
β’ ((π β§ πΆ < π) β (absβ((((πΊβπ) β (πΊβπΆ)) / (π β πΆ)) β (πΉβπΆ))) < πΈ) |
75 | 73, 74 | eqbrtrd 5131 |
. . 3
β’ ((π β§ πΆ < π) β (absβ((π»βπ) β (πΉβπΆ))) < πΈ) |
76 | 66, 75 | jaodan 957 |
. 2
β’ ((π β§ (π < πΆ β¨ πΆ < π)) β (absβ((π»βπ) β (πΉβπΆ))) < πΈ) |
77 | 12, 76 | syldan 592 |
1
β’ ((π β§ π β πΆ) β (absβ((π»βπ) β (πΉβπΆ))) < πΈ) |