Step | Hyp | Ref
| Expression |
1 | | breq2 5153 |
. . . 4
β’ (π₯ = π
β ((absβ(π΅ β πΆ)) < π₯ β (absβ(π΅ β πΆ)) < π
)) |
2 | 1 | imbi2d 341 |
. . 3
β’ (π₯ = π
β ((π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯) β (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π
))) |
3 | 2 | rexralbidv 3221 |
. 2
β’ (π₯ = π
β (βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯) β βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π
))) |
4 | | rlimi.3 |
. . 3
β’ (π β (π§ β π΄ β¦ π΅) βπ πΆ) |
5 | | rlimf 15445 |
. . . . . . 7
β’ ((π§ β π΄ β¦ π΅) βπ πΆ β (π§ β π΄ β¦ π΅):dom (π§ β π΄ β¦ π΅)βΆβ) |
6 | 4, 5 | syl 17 |
. . . . . 6
β’ (π β (π§ β π΄ β¦ π΅):dom (π§ β π΄ β¦ π΅)βΆβ) |
7 | | rlimi.1 |
. . . . . . . . 9
β’ (π β βπ§ β π΄ π΅ β π) |
8 | | eqid 2733 |
. . . . . . . . . 10
β’ (π§ β π΄ β¦ π΅) = (π§ β π΄ β¦ π΅) |
9 | 8 | fmpt 7110 |
. . . . . . . . 9
β’
(βπ§ β
π΄ π΅ β π β (π§ β π΄ β¦ π΅):π΄βΆπ) |
10 | 7, 9 | sylib 217 |
. . . . . . . 8
β’ (π β (π§ β π΄ β¦ π΅):π΄βΆπ) |
11 | 10 | fdmd 6729 |
. . . . . . 7
β’ (π β dom (π§ β π΄ β¦ π΅) = π΄) |
12 | 11 | feq2d 6704 |
. . . . . 6
β’ (π β ((π§ β π΄ β¦ π΅):dom (π§ β π΄ β¦ π΅)βΆβ β (π§ β π΄ β¦ π΅):π΄βΆβ)) |
13 | 6, 12 | mpbid 231 |
. . . . 5
β’ (π β (π§ β π΄ β¦ π΅):π΄βΆβ) |
14 | 8 | fmpt 7110 |
. . . . 5
β’
(βπ§ β
π΄ π΅ β β β (π§ β π΄ β¦ π΅):π΄βΆβ) |
15 | 13, 14 | sylibr 233 |
. . . 4
β’ (π β βπ§ β π΄ π΅ β β) |
16 | | rlimss 15446 |
. . . . . 6
β’ ((π§ β π΄ β¦ π΅) βπ πΆ β dom (π§ β π΄ β¦ π΅) β β) |
17 | 4, 16 | syl 17 |
. . . . 5
β’ (π β dom (π§ β π΄ β¦ π΅) β β) |
18 | 11, 17 | eqsstrrd 4022 |
. . . 4
β’ (π β π΄ β β) |
19 | | rlimcl 15447 |
. . . . 5
β’ ((π§ β π΄ β¦ π΅) βπ πΆ β πΆ β β) |
20 | 4, 19 | syl 17 |
. . . 4
β’ (π β πΆ β β) |
21 | 15, 18, 20 | rlim2 15440 |
. . 3
β’ (π β ((π§ β π΄ β¦ π΅) βπ πΆ β βπ₯ β β+
βπ¦ β β
βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯))) |
22 | 4, 21 | mpbid 231 |
. 2
β’ (π β βπ₯ β β+ βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π₯)) |
23 | | rlimi.2 |
. 2
β’ (π β π
β
β+) |
24 | 3, 22, 23 | rspcdva 3614 |
1
β’ (π β βπ¦ β β βπ§ β π΄ (π¦ β€ π§ β (absβ(π΅ β πΆ)) < π
)) |