Step | Hyp | Ref
| Expression |
1 | | ftc1.g |
. . . 4
β’ πΊ = (π₯ β (π΄[,]π΅) β¦ β«(π΄(,)π₯)(πΉβπ‘) dπ‘) |
2 | | ftc1.a |
. . . 4
β’ (π β π΄ β β) |
3 | | ftc1.b |
. . . 4
β’ (π β π΅ β β) |
4 | | ftc1.le |
. . . 4
β’ (π β π΄ β€ π΅) |
5 | | ftc1.s |
. . . 4
β’ (π β (π΄(,)π΅) β π·) |
6 | | ftc1.d |
. . . 4
β’ (π β π· β β) |
7 | | ftc1.i |
. . . 4
β’ (π β πΉ β
πΏ1) |
8 | | ftc1.c |
. . . 4
β’ (π β πΆ β (π΄(,)π΅)) |
9 | | ftc1.f |
. . . 4
β’ (π β πΉ β ((πΎ CnP πΏ)βπΆ)) |
10 | | ftc1.j |
. . . 4
β’ π½ = (πΏ βΎt
β) |
11 | | ftc1.k |
. . . 4
β’ πΎ = (πΏ βΎt π·) |
12 | | ftc1.l |
. . . 4
β’ πΏ =
(TopOpenββfld) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12 | ftc1lem3 25425 |
. . 3
β’ (π β πΉ:π·βΆβ) |
14 | 5, 8 | sseldd 3949 |
. . 3
β’ (π β πΆ β π·) |
15 | 13, 14 | ffvelcdmd 7040 |
. 2
β’ (π β (πΉβπΆ) β β) |
16 | | cnxmet 24159 |
. . . . . 6
β’ (abs
β β ) β (βMetββ) |
17 | | ax-resscn 11116 |
. . . . . . . 8
β’ β
β β |
18 | 6, 17 | sstrdi 3960 |
. . . . . . 7
β’ (π β π· β β) |
19 | 18 | adantr 482 |
. . . . . 6
β’ ((π β§ π€ β β+) β π· β
β) |
20 | | xmetres2 23737 |
. . . . . 6
β’ (((abs
β β ) β (βMetββ) β§ π· β β) β ((abs β
β ) βΎ (π·
Γ π·)) β
(βMetβπ·)) |
21 | 16, 19, 20 | sylancr 588 |
. . . . 5
β’ ((π β§ π€ β β+) β ((abs
β β ) βΎ (π· Γ π·)) β (βMetβπ·)) |
22 | 16 | a1i 11 |
. . . . 5
β’ ((π β§ π€ β β+) β (abs
β β ) β (βMetββ)) |
23 | | eqid 2733 |
. . . . . . . . . . . 12
β’ ((abs
β β ) βΎ (π· Γ π·)) = ((abs β β ) βΎ (π· Γ π·)) |
24 | 12 | cnfldtopn 24168 |
. . . . . . . . . . . 12
β’ πΏ = (MetOpenβ(abs β
β )) |
25 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(MetOpenβ((abs β β ) βΎ (π· Γ π·))) = (MetOpenβ((abs β β )
βΎ (π· Γ π·))) |
26 | 23, 24, 25 | metrest 23903 |
. . . . . . . . . . 11
β’ (((abs
β β ) β (βMetββ) β§ π· β β) β (πΏ βΎt π·) = (MetOpenβ((abs β β )
βΎ (π· Γ π·)))) |
27 | 16, 18, 26 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (πΏ βΎt π·) = (MetOpenβ((abs β β )
βΎ (π· Γ π·)))) |
28 | 11, 27 | eqtrid 2785 |
. . . . . . . . 9
β’ (π β πΎ = (MetOpenβ((abs β β )
βΎ (π· Γ π·)))) |
29 | 28 | oveq1d 7376 |
. . . . . . . 8
β’ (π β (πΎ CnP πΏ) = ((MetOpenβ((abs β β )
βΎ (π· Γ π·))) CnP πΏ)) |
30 | 29 | fveq1d 6848 |
. . . . . . 7
β’ (π β ((πΎ CnP πΏ)βπΆ) = (((MetOpenβ((abs β β )
βΎ (π· Γ π·))) CnP πΏ)βπΆ)) |
31 | 9, 30 | eleqtrd 2836 |
. . . . . 6
β’ (π β πΉ β (((MetOpenβ((abs β
β ) βΎ (π·
Γ π·))) CnP πΏ)βπΆ)) |
32 | 31 | adantr 482 |
. . . . 5
β’ ((π β§ π€ β β+) β πΉ β (((MetOpenβ((abs
β β ) βΎ (π· Γ π·))) CnP πΏ)βπΆ)) |
33 | | simpr 486 |
. . . . 5
β’ ((π β§ π€ β β+) β π€ β
β+) |
34 | 25, 24 | metcnpi2 23924 |
. . . . 5
β’ (((((abs
β β ) βΎ (π· Γ π·)) β (βMetβπ·) β§ (abs β β )
β (βMetββ)) β§ (πΉ β (((MetOpenβ((abs β
β ) βΎ (π·
Γ π·))) CnP πΏ)βπΆ) β§ π€ β β+)) β
βπ£ β
β+ βπ¦ β π· ((π¦((abs β β ) βΎ (π· Γ π·))πΆ) < π£ β ((πΉβπ¦)(abs β β )(πΉβπΆ)) < π€)) |
35 | 21, 22, 32, 33, 34 | syl22anc 838 |
. . . 4
β’ ((π β§ π€ β β+) β
βπ£ β
β+ βπ¦ β π· ((π¦((abs β β ) βΎ (π· Γ π·))πΆ) < π£ β ((πΉβπ¦)(abs β β )(πΉβπΆ)) < π€)) |
36 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β π¦ β π·) |
37 | 14 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β πΆ β π·) |
38 | 36, 37 | ovresd 7525 |
. . . . . . . . . . 11
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β (π¦((abs β β ) βΎ (π· Γ π·))πΆ) = (π¦(abs β β )πΆ)) |
39 | 18 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π€ β β+ β§ π£ β β+))
β π· β
β) |
40 | 39 | sselda 3948 |
. . . . . . . . . . . 12
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β π¦ β β) |
41 | | iccssre 13355 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
42 | 2, 3, 41 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄[,]π΅) β β) |
43 | 42, 17 | sstrdi 3960 |
. . . . . . . . . . . . . 14
β’ (π β (π΄[,]π΅) β β) |
44 | | ioossicc 13359 |
. . . . . . . . . . . . . . 15
β’ (π΄(,)π΅) β (π΄[,]π΅) |
45 | 44, 8 | sselid 3946 |
. . . . . . . . . . . . . 14
β’ (π β πΆ β (π΄[,]π΅)) |
46 | 43, 45 | sseldd 3949 |
. . . . . . . . . . . . 13
β’ (π β πΆ β β) |
47 | 46 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β πΆ β β) |
48 | | eqid 2733 |
. . . . . . . . . . . . 13
β’ (abs
β β ) = (abs β β ) |
49 | 48 | cnmetdval 24157 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ πΆ β β) β (π¦(abs β β )πΆ) = (absβ(π¦ β πΆ))) |
50 | 40, 47, 49 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β (π¦(abs β β )πΆ) = (absβ(π¦ β πΆ))) |
51 | 38, 50 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β (π¦((abs β β ) βΎ (π· Γ π·))πΆ) = (absβ(π¦ β πΆ))) |
52 | 51 | breq1d 5119 |
. . . . . . . . 9
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β ((π¦((abs β β ) βΎ (π· Γ π·))πΆ) < π£ β (absβ(π¦ β πΆ)) < π£)) |
53 | 13 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π€ β β+ β§ π£ β β+))
β πΉ:π·βΆβ) |
54 | 53 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β (πΉβπ¦) β β) |
55 | 15 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β (πΉβπΆ) β β) |
56 | 48 | cnmetdval 24157 |
. . . . . . . . . . 11
β’ (((πΉβπ¦) β β β§ (πΉβπΆ) β β) β ((πΉβπ¦)(abs β β )(πΉβπΆ)) = (absβ((πΉβπ¦) β (πΉβπΆ)))) |
57 | 54, 55, 56 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β ((πΉβπ¦)(abs β β )(πΉβπΆ)) = (absβ((πΉβπ¦) β (πΉβπΆ)))) |
58 | 57 | breq1d 5119 |
. . . . . . . . 9
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β (((πΉβπ¦)(abs β β )(πΉβπΆ)) < π€ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) |
59 | 52, 58 | imbi12d 345 |
. . . . . . . 8
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π¦ β π·) β (((π¦((abs β β ) βΎ (π· Γ π·))πΆ) < π£ β ((πΉβπ¦)(abs β β )(πΉβπΆ)) < π€) β ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€))) |
60 | 59 | ralbidva 3169 |
. . . . . . 7
β’ ((π β§ (π€ β β+ β§ π£ β β+))
β (βπ¦ β
π· ((π¦((abs β β ) βΎ (π· Γ π·))πΆ) < π£ β ((πΉβπ¦)(abs β β )(πΉβπΆ)) < π€) β βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€))) |
61 | | simprll 778 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β π β ((π΄[,]π΅) β {πΆ})) |
62 | | eldifsni 4754 |
. . . . . . . . . . . . 13
β’ (π β ((π΄[,]π΅) β {πΆ}) β π β πΆ) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β π β πΆ) |
64 | 2 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β π΄ β β) |
65 | 3 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β π΅ β β) |
66 | 4 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β π΄ β€ π΅) |
67 | 5 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β (π΄(,)π΅) β π·) |
68 | 6 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β π· β β) |
69 | 7 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β πΉ β
πΏ1) |
70 | 8 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β πΆ β (π΄(,)π΅)) |
71 | 9 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β πΉ β ((πΎ CnP πΏ)βπΆ)) |
72 | | ftc1.h |
. . . . . . . . . . . . 13
β’ π» = (π§ β ((π΄[,]π΅) β {πΆ}) β¦ (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ))) |
73 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β π€ β β+) |
74 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β π£ β β+) |
75 | | simprlr 779 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) |
76 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π’ β (absβ(π¦ β πΆ)) = (absβ(π’ β πΆ))) |
77 | 76 | breq1d 5119 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π’ β ((absβ(π¦ β πΆ)) < π£ β (absβ(π’ β πΆ)) < π£)) |
78 | 77 | imbrov2fvoveq 7386 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π’ β (((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€) β ((absβ(π’ β πΆ)) < π£ β (absβ((πΉβπ’) β (πΉβπΆ))) < π€))) |
79 | 78 | rspccva 3582 |
. . . . . . . . . . . . . 14
β’
((βπ¦ β
π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€) β§ π’ β π·) β ((absβ(π’ β πΆ)) < π£ β (absβ((πΉβπ’) β (πΉβπΆ))) < π€)) |
80 | 75, 79 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β§ π’ β π·) β ((absβ(π’ β πΆ)) < π£ β (absβ((πΉβπ’) β (πΉβπΆ))) < π€)) |
81 | 61 | eldifad 3926 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β π β (π΄[,]π΅)) |
82 | | simprr 772 |
. . . . . . . . . . . . 13
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β (absβ(π β πΆ)) < π£) |
83 | 1, 64, 65, 66, 67, 68, 69, 70, 71, 10, 11, 12, 72, 73, 74, 80, 81, 82 | ftc1lem5 25427 |
. . . . . . . . . . . 12
β’ ((((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β§ π β πΆ) β (absβ((π»βπ ) β (πΉβπΆ))) < π€) |
84 | 63, 83 | mpdan 686 |
. . . . . . . . . . 11
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ ((π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€)) β§ (absβ(π β πΆ)) < π£)) β (absβ((π»βπ ) β (πΉβπΆ))) < π€) |
85 | 84 | expr 458 |
. . . . . . . . . 10
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ (π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€))) β ((absβ(π β πΆ)) < π£ β (absβ((π»βπ ) β (πΉβπΆ))) < π€)) |
86 | 85 | adantld 492 |
. . . . . . . . 9
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ (π β ((π΄[,]π΅) β {πΆ}) β§ βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€))) β ((π β πΆ β§ (absβ(π β πΆ)) < π£) β (absβ((π»βπ ) β (πΉβπΆ))) < π€)) |
87 | 86 | expr 458 |
. . . . . . . 8
β’ (((π β§ (π€ β β+ β§ π£ β β+))
β§ π β ((π΄[,]π΅) β {πΆ})) β (βπ¦ β π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€) β ((π β πΆ β§ (absβ(π β πΆ)) < π£) β (absβ((π»βπ ) β (πΉβπΆ))) < π€))) |
88 | 87 | ralrimdva 3148 |
. . . . . . 7
β’ ((π β§ (π€ β β+ β§ π£ β β+))
β (βπ¦ β
π· ((absβ(π¦ β πΆ)) < π£ β (absβ((πΉβπ¦) β (πΉβπΆ))) < π€) β βπ β ((π΄[,]π΅) β {πΆ})((π β πΆ β§ (absβ(π β πΆ)) < π£) β (absβ((π»βπ ) β (πΉβπΆ))) < π€))) |
89 | 60, 88 | sylbid 239 |
. . . . . 6
β’ ((π β§ (π€ β β+ β§ π£ β β+))
β (βπ¦ β
π· ((π¦((abs β β ) βΎ (π· Γ π·))πΆ) < π£ β ((πΉβπ¦)(abs β β )(πΉβπΆ)) < π€) β βπ β ((π΄[,]π΅) β {πΆ})((π β πΆ β§ (absβ(π β πΆ)) < π£) β (absβ((π»βπ ) β (πΉβπΆ))) < π€))) |
90 | 89 | anassrs 469 |
. . . . 5
β’ (((π β§ π€ β β+) β§ π£ β β+)
β (βπ¦ β
π· ((π¦((abs β β ) βΎ (π· Γ π·))πΆ) < π£ β ((πΉβπ¦)(abs β β )(πΉβπΆ)) < π€) β βπ β ((π΄[,]π΅) β {πΆ})((π β πΆ β§ (absβ(π β πΆ)) < π£) β (absβ((π»βπ ) β (πΉβπΆ))) < π€))) |
91 | 90 | reximdva 3162 |
. . . 4
β’ ((π β§ π€ β β+) β
(βπ£ β
β+ βπ¦ β π· ((π¦((abs β β ) βΎ (π· Γ π·))πΆ) < π£ β ((πΉβπ¦)(abs β β )(πΉβπΆ)) < π€) β βπ£ β β+ βπ β ((π΄[,]π΅) β {πΆ})((π β πΆ β§ (absβ(π β πΆ)) < π£) β (absβ((π»βπ ) β (πΉβπΆ))) < π€))) |
92 | 35, 91 | mpd 15 |
. . 3
β’ ((π β§ π€ β β+) β
βπ£ β
β+ βπ β ((π΄[,]π΅) β {πΆ})((π β πΆ β§ (absβ(π β πΆ)) < π£) β (absβ((π»βπ ) β (πΉβπΆ))) < π€)) |
93 | 92 | ralrimiva 3140 |
. 2
β’ (π β βπ€ β β+ βπ£ β β+
βπ β ((π΄[,]π΅) β {πΆ})((π β πΆ β§ (absβ(π β πΆ)) < π£) β (absβ((π»βπ ) β (πΉβπΆ))) < π€)) |
94 | 1, 2, 3, 4, 5, 6, 7, 13 | ftc1lem2 25423 |
. . . . 5
β’ (π β πΊ:(π΄[,]π΅)βΆβ) |
95 | 94, 43, 45 | dvlem 25283 |
. . . 4
β’ ((π β§ π§ β ((π΄[,]π΅) β {πΆ})) β (((πΊβπ§) β (πΊβπΆ)) / (π§ β πΆ)) β β) |
96 | 95, 72 | fmptd 7066 |
. . 3
β’ (π β π»:((π΄[,]π΅) β {πΆ})βΆβ) |
97 | 43 | ssdifssd 4106 |
. . 3
β’ (π β ((π΄[,]π΅) β {πΆ}) β β) |
98 | 96, 97, 46 | ellimc3 25266 |
. 2
β’ (π β ((πΉβπΆ) β (π» limβ πΆ) β ((πΉβπΆ) β β β§ βπ€ β β+
βπ£ β
β+ βπ β ((π΄[,]π΅) β {πΆ})((π β πΆ β§ (absβ(π β πΆ)) < π£) β (absβ((π»βπ ) β (πΉβπΆ))) < π€)))) |
99 | 15, 93, 98 | mpbir2and 712 |
1
β’ (π β (πΉβπΆ) β (π» limβ πΆ)) |