Step | Hyp | Ref
| Expression |
1 | | nfcv 2317 |
. . . . . 6
β’
β²π€π· |
2 | | nfcsb1v 3088 |
. . . . . 6
β’
β²π§β¦π€ / π§β¦π· |
3 | | csbeq1a 3064 |
. . . . . 6
β’ (π§ = π€ β π· = β¦π€ / π§β¦π·) |
4 | 1, 2, 3 | cbvmpt 4093 |
. . . . 5
β’ (π§ β π΄ β¦ π·) = (π€ β π΄ β¦ β¦π€ / π§β¦π·) |
5 | 4 | a1i 9 |
. . . 4
β’ (π β (π§ β π΄ β¦ π·) = (π€ β π΄ β¦ β¦π€ / π§β¦π·)) |
6 | 5 | oveq1d 5880 |
. . 3
β’ (π β ((π§ β π΄ β¦ π·) limβ π΅) = ((π€ β π΄ β¦ β¦π€ / π§β¦π·) limβ π΅)) |
7 | 6 | eleq2d 2245 |
. 2
β’ (π β (πΆ β ((π§ β π΄ β¦ π·) limβ π΅) β πΆ β ((π€ β π΄ β¦ β¦π€ / π§β¦π·) limβ π΅))) |
8 | | limcmpted.f |
. . . . 5
β’ ((π β§ π§ β π΄) β π· β β) |
9 | 8 | fmpttd 5663 |
. . . 4
β’ (π β (π§ β π΄ β¦ π·):π΄βΆβ) |
10 | 4 | feq1i 5350 |
. . . 4
β’ ((π§ β π΄ β¦ π·):π΄βΆβ β (π€ β π΄ β¦ β¦π€ / π§β¦π·):π΄βΆβ) |
11 | 9, 10 | sylib 122 |
. . 3
β’ (π β (π€ β π΄ β¦ β¦π€ / π§β¦π·):π΄βΆβ) |
12 | | limcmpted.a |
. . 3
β’ (π β π΄ β β) |
13 | | limcmpted.b |
. . 3
β’ (π β π΅ β β) |
14 | | nfcv 2317 |
. . . 4
β’
β²π§π΄ |
15 | 14, 2 | nfmpt 4090 |
. . 3
β’
β²π§(π€ β π΄ β¦ β¦π€ / π§β¦π·) |
16 | 11, 12, 13, 15 | ellimc3apf 13622 |
. 2
β’ (π β (πΆ β ((π€ β π΄ β¦ β¦π€ / π§β¦π·) limβ π΅) β (πΆ β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(((π€ β π΄ β¦ β¦π€ / π§β¦π·)βπ§) β πΆ)) < π₯)))) |
17 | | eqid 2175 |
. . . . . . . . . 10
β’ (π€ β π΄ β¦ β¦π€ / π§β¦π·) = (π€ β π΄ β¦ β¦π€ / π§β¦π·) |
18 | | eqcom 2177 |
. . . . . . . . . . 11
β’ (π§ = π€ β π€ = π§) |
19 | | eqcom 2177 |
. . . . . . . . . . 11
β’ (π· = β¦π€ / π§β¦π· β β¦π€ / π§β¦π· = π·) |
20 | 3, 18, 19 | 3imtr3i 200 |
. . . . . . . . . 10
β’ (π€ = π§ β β¦π€ / π§β¦π· = π·) |
21 | | simpr 110 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β π§ β π΄) |
22 | 17, 20, 21, 8 | fvmptd3 5601 |
. . . . . . . . 9
β’ ((π β§ π§ β π΄) β ((π€ β π΄ β¦ β¦π€ / π§β¦π·)βπ§) = π·) |
23 | 22 | fvoveq1d 5887 |
. . . . . . . 8
β’ ((π β§ π§ β π΄) β (absβ(((π€ β π΄ β¦ β¦π€ / π§β¦π·)βπ§) β πΆ)) = (absβ(π· β πΆ))) |
24 | 23 | breq1d 4008 |
. . . . . . 7
β’ ((π β§ π§ β π΄) β ((absβ(((π€ β π΄ β¦ β¦π€ / π§β¦π·)βπ§) β πΆ)) < π₯ β (absβ(π· β πΆ)) < π₯)) |
25 | 24 | imbi2d 230 |
. . . . . 6
β’ ((π β§ π§ β π΄) β (((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(((π€ β π΄ β¦ β¦π€ / π§β¦π·)βπ§) β πΆ)) < π₯) β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(π· β πΆ)) < π₯))) |
26 | 25 | ralbidva 2471 |
. . . . 5
β’ (π β (βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(((π€ β π΄ β¦ β¦π€ / π§β¦π·)βπ§) β πΆ)) < π₯) β βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(π· β πΆ)) < π₯))) |
27 | 26 | rexbidv 2476 |
. . . 4
β’ (π β (βπ¦ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(((π€ β π΄ β¦ β¦π€ / π§β¦π·)βπ§) β πΆ)) < π₯) β βπ¦ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(π· β πΆ)) < π₯))) |
28 | 27 | ralbidv 2475 |
. . 3
β’ (π β (βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(((π€ β π΄ β¦ β¦π€ / π§β¦π·)βπ§) β πΆ)) < π₯) β βπ₯ β β+ βπ¦ β β+
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(π· β πΆ)) < π₯))) |
29 | 28 | anbi2d 464 |
. 2
β’ (π β ((πΆ β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(((π€ β π΄ β¦ β¦π€ / π§β¦π·)βπ§) β πΆ)) < π₯)) β (πΆ β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(π· β πΆ)) < π₯)))) |
30 | 7, 16, 29 | 3bitrd 214 |
1
β’ (π β (πΆ β ((π§ β π΄ β¦ π·) limβ π΅) β (πΆ β β β§ βπ₯ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π¦) β (absβ(π· β πΆ)) < π₯)))) |