Step | Hyp | Ref
| Expression |
1 | | limcrcl 14130 |
. . . . 5
β’ (π’ β (πΉ limβ π΅) β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΅ β β)) |
2 | 1 | simp3d 1011 |
. . . 4
β’ (π’ β (πΉ limβ π΅) β π΅ β β) |
3 | 2 | a1i 9 |
. . 3
β’ (π β (π’ β (πΉ limβ π΅) β π΅ β β)) |
4 | | limcrcl 14130 |
. . . . 5
β’ (π’ β ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}) limβ π΅) β ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}):dom (πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βΆβ β§ dom (πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}) β β β§ π΅ β β)) |
5 | 4 | simp3d 1011 |
. . . 4
β’ (π’ β ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}) limβ π΅) β π΅ β β) |
6 | 5 | a1i 9 |
. . 3
β’ (π β (π’ β ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}) limβ π΅) β π΅ β β)) |
7 | | breq1 4007 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π§ β (π₯ # π΅ β π§ # π΅)) |
8 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π΅ β β) β§ π§ β π΄) β§ π§ # π΅) β π§ β π΄) |
9 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π΅ β β) β§ π§ β π΄) β§ π§ # π΅) β π§ # π΅) |
10 | 7, 8, 9 | elrabd 2896 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π΅ β β) β§ π§ β π΄) β§ π§ # π΅) β π§ β {π₯ β π΄ β£ π₯ # π΅}) |
11 | | fvres 5540 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β {π₯ β π΄ β£ π₯ # π΅} β ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) = (πΉβπ§)) |
12 | 11 | eqcomd 2183 |
. . . . . . . . . . . . . . . 16
β’ (π§ β {π₯ β π΄ β£ π₯ # π΅} β (πΉβπ§) = ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§)) |
13 | 10, 12 | syl 14 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π΅ β β) β§ π§ β π΄) β§ π§ # π΅) β (πΉβπ§) = ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§)) |
14 | 13 | fvoveq1d 5897 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π΅ β β) β§ π§ β π΄) β§ π§ # π΅) β (absβ((πΉβπ§) β π’)) = (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’))) |
15 | 14 | breq1d 4014 |
. . . . . . . . . . . . 13
β’ ((((π β§ π΅ β β) β§ π§ β π΄) β§ π§ # π΅) β ((absβ((πΉβπ§) β π’)) < π β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π)) |
16 | 15 | imbi2d 230 |
. . . . . . . . . . . 12
β’ ((((π β§ π΅ β β) β§ π§ β π΄) β§ π§ # π΅) β (((absβ(π§ β π΅)) < π β (absβ((πΉβπ§) β π’)) < π) β ((absβ(π§ β π΅)) < π β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π))) |
17 | 16 | pm5.74da 443 |
. . . . . . . . . . 11
β’ (((π β§ π΅ β β) β§ π§ β π΄) β ((π§ # π΅ β ((absβ(π§ β π΅)) < π β (absβ((πΉβπ§) β π’)) < π)) β (π§ # π΅ β ((absβ(π§ β π΅)) < π β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π)))) |
18 | | impexp 263 |
. . . . . . . . . . 11
β’ (((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π’)) < π) β (π§ # π΅ β ((absβ(π§ β π΅)) < π β (absβ((πΉβπ§) β π’)) < π))) |
19 | | impexp 263 |
. . . . . . . . . . . . 13
β’ (((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π) β (π§ # π΅ β ((absβ(π§ β π΅)) < π β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π))) |
20 | 19 | imbi2i 226 |
. . . . . . . . . . . 12
β’ ((π§ # π΅ β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π)) β (π§ # π΅ β (π§ # π΅ β ((absβ(π§ β π΅)) < π β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π)))) |
21 | | pm5.4 249 |
. . . . . . . . . . . 12
β’ ((π§ # π΅ β (π§ # π΅ β ((absβ(π§ β π΅)) < π β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π))) β (π§ # π΅ β ((absβ(π§ β π΅)) < π β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π))) |
22 | 20, 21 | bitri 184 |
. . . . . . . . . . 11
β’ ((π§ # π΅ β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π)) β (π§ # π΅ β ((absβ(π§ β π΅)) < π β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π))) |
23 | 17, 18, 22 | 3bitr4g 223 |
. . . . . . . . . 10
β’ (((π β§ π΅ β β) β§ π§ β π΄) β (((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π’)) < π) β (π§ # π΅ β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π)))) |
24 | 23 | ralbidva 2473 |
. . . . . . . . 9
β’ ((π β§ π΅ β β) β (βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π’)) < π) β βπ§ β π΄ (π§ # π΅ β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π)))) |
25 | 7 | ralrab 2899 |
. . . . . . . . 9
β’
(βπ§ β
{π₯ β π΄ β£ π₯ # π΅} ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π) β βπ§ β π΄ (π§ # π΅ β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π))) |
26 | 24, 25 | bitr4di 198 |
. . . . . . . 8
β’ ((π β§ π΅ β β) β (βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π’)) < π) β βπ§ β {π₯ β π΄ β£ π₯ # π΅} ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π))) |
27 | 26 | rexbidv 2478 |
. . . . . . 7
β’ ((π β§ π΅ β β) β (βπ β β+
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π’)) < π) β βπ β β+ βπ§ β {π₯ β π΄ β£ π₯ # π΅} ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π))) |
28 | 27 | ralbidv 2477 |
. . . . . 6
β’ ((π β§ π΅ β β) β (βπ β β+
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π’)) < π) β βπ β β+ βπ β β+
βπ§ β {π₯ β π΄ β£ π₯ # π΅} ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π))) |
29 | 28 | anbi2d 464 |
. . . . 5
β’ ((π β§ π΅ β β) β ((π’ β β β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π’)) < π)) β (π’ β β β§ βπ β β+
βπ β
β+ βπ§ β {π₯ β π΄ β£ π₯ # π΅} ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π)))) |
30 | | limccl.f |
. . . . . . 7
β’ (π β πΉ:π΄βΆβ) |
31 | 30 | adantr 276 |
. . . . . 6
β’ ((π β§ π΅ β β) β πΉ:π΄βΆβ) |
32 | | limcdifap.a |
. . . . . . 7
β’ (π β π΄ β β) |
33 | 32 | adantr 276 |
. . . . . 6
β’ ((π β§ π΅ β β) β π΄ β β) |
34 | | simpr 110 |
. . . . . 6
β’ ((π β§ π΅ β β) β π΅ β β) |
35 | 31, 33, 34 | ellimc3ap 14133 |
. . . . 5
β’ ((π β§ π΅ β β) β (π’ β (πΉ limβ π΅) β (π’ β β β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π’)) < π)))) |
36 | | ssrab2 3241 |
. . . . . . 7
β’ {π₯ β π΄ β£ π₯ # π΅} β π΄ |
37 | | fssres 5392 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ {π₯ β π΄ β£ π₯ # π΅} β π΄) β (πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}):{π₯ β π΄ β£ π₯ # π΅}βΆβ) |
38 | 31, 36, 37 | sylancl 413 |
. . . . . 6
β’ ((π β§ π΅ β β) β (πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}):{π₯ β π΄ β£ π₯ # π΅}βΆβ) |
39 | 36, 33 | sstrid 3167 |
. . . . . 6
β’ ((π β§ π΅ β β) β {π₯ β π΄ β£ π₯ # π΅} β β) |
40 | 38, 39, 34 | ellimc3ap 14133 |
. . . . 5
β’ ((π β§ π΅ β β) β (π’ β ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}) limβ π΅) β (π’ β β β§ βπ β β+
βπ β
β+ βπ§ β {π₯ β π΄ β£ π₯ # π΅} ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ(((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅})βπ§) β π’)) < π)))) |
41 | 29, 35, 40 | 3bitr4d 220 |
. . . 4
β’ ((π β§ π΅ β β) β (π’ β (πΉ limβ π΅) β π’ β ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}) limβ π΅))) |
42 | 41 | ex 115 |
. . 3
β’ (π β (π΅ β β β (π’ β (πΉ limβ π΅) β π’ β ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}) limβ π΅)))) |
43 | 3, 6, 42 | pm5.21ndd 705 |
. 2
β’ (π β (π’ β (πΉ limβ π΅) β π’ β ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}) limβ π΅))) |
44 | 43 | eqrdv 2175 |
1
β’ (π β (πΉ limβ π΅) = ((πΉ βΎ {π₯ β π΄ β£ π₯ # π΅}) limβ π΅)) |