Step | Hyp | Ref
| Expression |
1 | | limccoap.d |
. . . 4
β’ (π β π· β ((π¦ β {π€ β π΅ β£ π€ # πΆ} β¦ π) limβ πΆ)) |
2 | | apsscn 8604 |
. . . . . 6
β’ {π€ β π΅ β£ π€ # πΆ} β β |
3 | 2 | a1i 9 |
. . . . 5
β’ (π β {π€ β π΅ β£ π€ # πΆ} β β) |
4 | | limcrcl 14130 |
. . . . . . 7
β’ (π· β ((π¦ β {π€ β π΅ β£ π€ # πΆ} β¦ π) limβ πΆ) β ((π¦ β {π€ β π΅ β£ π€ # πΆ} β¦ π):dom (π¦ β {π€ β π΅ β£ π€ # πΆ} β¦ π)βΆβ β§ dom (π¦ β {π€ β π΅ β£ π€ # πΆ} β¦ π) β β β§ πΆ β β)) |
5 | 1, 4 | syl 14 |
. . . . . 6
β’ (π β ((π¦ β {π€ β π΅ β£ π€ # πΆ} β¦ π):dom (π¦ β {π€ β π΅ β£ π€ # πΆ} β¦ π)βΆβ β§ dom (π¦ β {π€ β π΅ β£ π€ # πΆ} β¦ π) β β β§ πΆ β β)) |
6 | 5 | simp3d 1011 |
. . . . 5
β’ (π β πΆ β β) |
7 | | limccoap.s |
. . . . 5
β’ ((π β§ π¦ β {π€ β π΅ β£ π€ # πΆ}) β π β β) |
8 | 3, 6, 7 | limcmpted 14135 |
. . . 4
β’ (π β (π· β ((π¦ β {π€ β π΅ β£ π€ # πΆ} β¦ π) limβ πΆ) β (π· β β β§ βπ β β+
βπ β
β+ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)))) |
9 | 1, 8 | mpbid 147 |
. . 3
β’ (π β (π· β β β§ βπ β β+
βπ β
β+ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π))) |
10 | 9 | simpld 112 |
. 2
β’ (π β π· β β) |
11 | 9 | simprd 114 |
. . 3
β’ (π β βπ β β+ βπ β β+
βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) |
12 | | breq2 4008 |
. . . . . . . . . 10
β’ (π£ = π β ((absβ(π
β πΆ)) < π£ β (absβ(π
β πΆ)) < π)) |
13 | 12 | imbi2d 230 |
. . . . . . . . 9
β’ (π£ = π β (((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π£) β ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π))) |
14 | 13 | rexralbidv 2503 |
. . . . . . . 8
β’ (π£ = π β (βπ’ β β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π£) β βπ’ β β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π))) |
15 | | limccoap.c |
. . . . . . . . . . 11
β’ (π β πΆ β ((π₯ β {π€ β π΄ β£ π€ # π} β¦ π
) limβ π)) |
16 | | apsscn 8604 |
. . . . . . . . . . . . 13
β’ {π€ β π΄ β£ π€ # π} β β |
17 | 16 | a1i 9 |
. . . . . . . . . . . 12
β’ (π β {π€ β π΄ β£ π€ # π} β β) |
18 | | limcrcl 14130 |
. . . . . . . . . . . . . 14
β’ (πΆ β ((π₯ β {π€ β π΄ β£ π€ # π} β¦ π
) limβ π) β ((π₯ β {π€ β π΄ β£ π€ # π} β¦ π
):dom (π₯ β {π€ β π΄ β£ π€ # π} β¦ π
)βΆβ β§ dom (π₯ β {π€ β π΄ β£ π€ # π} β¦ π
) β β β§ π β β)) |
19 | 15, 18 | syl 14 |
. . . . . . . . . . . . 13
β’ (π β ((π₯ β {π€ β π΄ β£ π€ # π} β¦ π
):dom (π₯ β {π€ β π΄ β£ π€ # π} β¦ π
)βΆβ β§ dom (π₯ β {π€ β π΄ β£ π€ # π} β¦ π
) β β β§ π β β)) |
20 | 19 | simp3d 1011 |
. . . . . . . . . . . 12
β’ (π β π β β) |
21 | | limccoap.r |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β {π€ β π΄ β£ π€ # π}) β π
β {π€ β π΅ β£ π€ # πΆ}) |
22 | 2, 21 | sselid 3154 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β {π€ β π΄ β£ π€ # π}) β π
β β) |
23 | 17, 20, 22 | limcmpted 14135 |
. . . . . . . . . . 11
β’ (π β (πΆ β ((π₯ β {π€ β π΄ β£ π€ # π} β¦ π
) limβ π) β (πΆ β β β§ βπ£ β β+
βπ’ β
β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π£)))) |
24 | 15, 23 | mpbid 147 |
. . . . . . . . . 10
β’ (π β (πΆ β β β§ βπ£ β β+
βπ’ β
β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π£))) |
25 | 24 | simprd 114 |
. . . . . . . . 9
β’ (π β βπ£ β β+ βπ’ β β+
βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π£)) |
26 | 25 | ad2antrr 488 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ π β β+)
β βπ£ β
β+ βπ’ β β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π£)) |
27 | | simpr 110 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ π β β+)
β π β
β+) |
28 | 14, 26, 27 | rspcdva 2847 |
. . . . . . 7
β’ (((π β§ π β β+) β§ π β β+)
β βπ’ β
β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π)) |
29 | 28 | adantr 276 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π β β+)
β§ βπ¦ β
{π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β βπ’ β β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π)) |
30 | | simp-5l 543 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β§ π’ β β+) β§ π₯ β {π€ β π΄ β£ π€ # π}) β π) |
31 | 30, 21 | sylancom 420 |
. . . . . . . . . . . 12
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β§ π’ β β+) β§ π₯ β {π€ β π΄ β£ π€ # π}) β π
β {π€ β π΅ β£ π€ # πΆ}) |
32 | | breq1 4007 |
. . . . . . . . . . . . 13
β’ (π€ = π
β (π€ # πΆ β π
# πΆ)) |
33 | 32 | elrab 2894 |
. . . . . . . . . . . 12
β’ (π
β {π€ β π΅ β£ π€ # πΆ} β (π
β π΅ β§ π
# πΆ)) |
34 | 31, 33 | sylib 122 |
. . . . . . . . . . 11
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β§ π’ β β+) β§ π₯ β {π€ β π΄ β£ π€ # π}) β (π
β π΅ β§ π
# πΆ)) |
35 | 34 | simprd 114 |
. . . . . . . . . 10
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β§ π’ β β+) β§ π₯ β {π€ β π΄ β£ π€ # π}) β π
# πΆ) |
36 | | breq1 4007 |
. . . . . . . . . . . . 13
β’ (π¦ = π
β (π¦ # πΆ β π
# πΆ)) |
37 | | fvoveq1 5898 |
. . . . . . . . . . . . . 14
β’ (π¦ = π
β (absβ(π¦ β πΆ)) = (absβ(π
β πΆ))) |
38 | 37 | breq1d 4014 |
. . . . . . . . . . . . 13
β’ (π¦ = π
β ((absβ(π¦ β πΆ)) < π β (absβ(π
β πΆ)) < π)) |
39 | 36, 38 | anbi12d 473 |
. . . . . . . . . . . 12
β’ (π¦ = π
β ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (π
# πΆ β§ (absβ(π
β πΆ)) < π))) |
40 | | limcco.1 |
. . . . . . . . . . . . . 14
β’ (π¦ = π
β π = π) |
41 | 40 | fvoveq1d 5897 |
. . . . . . . . . . . . 13
β’ (π¦ = π
β (absβ(π β π·)) = (absβ(π β π·))) |
42 | 41 | breq1d 4014 |
. . . . . . . . . . . 12
β’ (π¦ = π
β ((absβ(π β π·)) < π β (absβ(π β π·)) < π)) |
43 | 39, 42 | imbi12d 234 |
. . . . . . . . . . 11
β’ (π¦ = π
β (((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π) β ((π
# πΆ β§ (absβ(π
β πΆ)) < π) β (absβ(π β π·)) < π))) |
44 | | simpllr 534 |
. . . . . . . . . . 11
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β§ π’ β β+) β§ π₯ β {π€ β π΄ β£ π€ # π}) β βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) |
45 | 43, 44, 31 | rspcdva 2847 |
. . . . . . . . . 10
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β§ π’ β β+) β§ π₯ β {π€ β π΄ β£ π€ # π}) β ((π
# πΆ β§ (absβ(π
β πΆ)) < π) β (absβ(π β π·)) < π)) |
46 | 35, 45 | mpand 429 |
. . . . . . . . 9
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β§ π’ β β+) β§ π₯ β {π€ β π΄ β£ π€ # π}) β ((absβ(π
β πΆ)) < π β (absβ(π β π·)) < π)) |
47 | 46 | imim2d 54 |
. . . . . . . 8
β’
((((((π β§ π β β+)
β§ π β
β+) β§ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β§ π’ β β+) β§ π₯ β {π€ β π΄ β£ π€ # π}) β (((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π) β ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π β π·)) < π))) |
48 | 47 | ralimdva 2544 |
. . . . . . 7
β’
(((((π β§ π β β+)
β§ π β
β+) β§ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β§ π’ β β+) β
(βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π) β βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π β π·)) < π))) |
49 | 48 | reximdva 2579 |
. . . . . 6
β’ ((((π β§ π β β+) β§ π β β+)
β§ βπ¦ β
{π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β (βπ’ β β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π
β πΆ)) < π) β βπ’ β β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π β π·)) < π))) |
50 | 29, 49 | mpd 13 |
. . . . 5
β’ ((((π β§ π β β+) β§ π β β+)
β§ βπ¦ β
{π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π)) β βπ’ β β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π β π·)) < π)) |
51 | 50 | rexlimdva2 2597 |
. . . 4
β’ ((π β§ π β β+) β
(βπ β
β+ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π) β βπ’ β β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π β π·)) < π))) |
52 | 51 | ralimdva 2544 |
. . 3
β’ (π β (βπ β β+
βπ β
β+ βπ¦ β {π€ β π΅ β£ π€ # πΆ} ((π¦ # πΆ β§ (absβ(π¦ β πΆ)) < π) β (absβ(π β π·)) < π) β βπ β β+ βπ’ β β+
βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π β π·)) < π))) |
53 | 11, 52 | mpd 13 |
. 2
β’ (π β βπ β β+ βπ’ β β+
βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π β π·)) < π)) |
54 | 40 | eleq1d 2246 |
. . . 4
β’ (π¦ = π
β (π β β β π β β)) |
55 | 7 | ralrimiva 2550 |
. . . . 5
β’ (π β βπ¦ β {π€ β π΅ β£ π€ # πΆ}π β β) |
56 | 55 | adantr 276 |
. . . 4
β’ ((π β§ π₯ β {π€ β π΄ β£ π€ # π}) β βπ¦ β {π€ β π΅ β£ π€ # πΆ}π β β) |
57 | 54, 56, 21 | rspcdva 2847 |
. . 3
β’ ((π β§ π₯ β {π€ β π΄ β£ π€ # π}) β π β β) |
58 | 17, 20, 57 | limcmpted 14135 |
. 2
β’ (π β (π· β ((π₯ β {π€ β π΄ β£ π€ # π} β¦ π) limβ π) β (π· β β β§ βπ β β+
βπ’ β
β+ βπ₯ β {π€ β π΄ β£ π€ # π} ((π₯ # π β§ (absβ(π₯ β π)) < π’) β (absβ(π β π·)) < π)))) |
59 | 10, 53, 58 | mpbir2and 944 |
1
β’ (π β π· β ((π₯ β {π€ β π΄ β£ π€ # π} β¦ π) limβ π)) |