Step | Hyp | Ref
| Expression |
1 | | ellimcabssub0.c |
. . . 4
β’ (π β πΆ β β) |
2 | | 0cnd 11149 |
. . . 4
β’ (π β 0 β
β) |
3 | 1, 2 | 2thd 265 |
. . 3
β’ (π β (πΆ β β β 0 β
β)) |
4 | | ellimcabssub0.b |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΄) β π΅ β β) |
5 | 1 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β π΄) β πΆ β β) |
6 | 4, 5 | subcld 11513 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β (π΅ β πΆ) β β) |
7 | | ellimcabssub0.g |
. . . . . . . . . . . . 13
β’ πΊ = (π₯ β π΄ β¦ (π΅ β πΆ)) |
8 | 6, 7 | fmptd 7063 |
. . . . . . . . . . . 12
β’ (π β πΊ:π΄βΆβ) |
9 | 8 | ffvelcdmda 7036 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β (πΊβπ§) β β) |
10 | 9 | subid1d 11502 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β ((πΊβπ§) β 0) = (πΊβπ§)) |
11 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β π§ β π΄) |
12 | | csbov1g 7403 |
. . . . . . . . . . . . 13
β’ (π§ β V β
β¦π§ / π₯β¦(π΅ β πΆ) = (β¦π§ / π₯β¦π΅ β πΆ)) |
13 | 12 | elv 3452 |
. . . . . . . . . . . 12
β’
β¦π§ /
π₯β¦(π΅ β πΆ) = (β¦π§ / π₯β¦π΅ β πΆ) |
14 | | sban 2084 |
. . . . . . . . . . . . . . . . 17
β’ ([π§ / π₯](π β§ π₯ β π΄) β ([π§ / π₯]π β§ [π§ / π₯]π₯ β π΄)) |
15 | | nfv 1918 |
. . . . . . . . . . . . . . . . . . 19
β’
β²π₯π |
16 | 15 | sbf 2263 |
. . . . . . . . . . . . . . . . . 18
β’ ([π§ / π₯]π β π) |
17 | | clelsb1 2865 |
. . . . . . . . . . . . . . . . . 18
β’ ([π§ / π₯]π₯ β π΄ β π§ β π΄) |
18 | 16, 17 | anbi12i 628 |
. . . . . . . . . . . . . . . . 17
β’ (([π§ / π₯]π β§ [π§ / π₯]π₯ β π΄) β (π β§ π§ β π΄)) |
19 | 14, 18 | bitri 275 |
. . . . . . . . . . . . . . . 16
β’ ([π§ / π₯](π β§ π₯ β π΄) β (π β§ π§ β π΄)) |
20 | 4 | nfth 1804 |
. . . . . . . . . . . . . . . . . 18
β’
β²π₯((π β§ π₯ β π΄) β π΅ β β) |
21 | 20 | sbf 2263 |
. . . . . . . . . . . . . . . . 17
β’ ([π§ / π₯]((π β§ π₯ β π΄) β π΅ β β) β ((π β§ π₯ β π΄) β π΅ β β)) |
22 | | sbim 2300 |
. . . . . . . . . . . . . . . . 17
β’ ([π§ / π₯]((π β§ π₯ β π΄) β π΅ β β) β ([π§ / π₯](π β§ π₯ β π΄) β [π§ / π₯]π΅ β β)) |
23 | 21, 22 | sylbb1 236 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π΄) β π΅ β β) β ([π§ / π₯](π β§ π₯ β π΄) β [π§ / π₯]π΅ β β)) |
24 | 19, 23 | biimtrrid 242 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π΄) β π΅ β β) β ((π β§ π§ β π΄) β [π§ / π₯]π΅ β β)) |
25 | 4, 24 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ ((π β§ π§ β π΄) β [π§ / π₯]π΅ β β) |
26 | | sbsbc 3744 |
. . . . . . . . . . . . . . 15
β’ ([π§ / π₯]π΅ β β β [π§ / π₯]π΅ β β) |
27 | | sbcel1g 4374 |
. . . . . . . . . . . . . . . 16
β’ (π§ β V β ([π§ / π₯]π΅ β β β β¦π§ / π₯β¦π΅ β β)) |
28 | 27 | elv 3452 |
. . . . . . . . . . . . . . 15
β’
([π§ / π₯]π΅ β β β β¦π§ / π₯β¦π΅ β β) |
29 | 26, 28 | bitri 275 |
. . . . . . . . . . . . . 14
β’ ([π§ / π₯]π΅ β β β β¦π§ / π₯β¦π΅ β β) |
30 | 25, 29 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π΄) β β¦π§ / π₯β¦π΅ β β) |
31 | 1 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β π΄) β πΆ β β) |
32 | 30, 31 | subcld 11513 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π΄) β (β¦π§ / π₯β¦π΅ β πΆ) β β) |
33 | 13, 32 | eqeltrid 2842 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β β¦π§ / π₯β¦(π΅ β πΆ) β β) |
34 | 7 | fvmpts 6952 |
. . . . . . . . . . 11
β’ ((π§ β π΄ β§ β¦π§ / π₯β¦(π΅ β πΆ) β β) β (πΊβπ§) = β¦π§ / π₯β¦(π΅ β πΆ)) |
35 | 11, 33, 34 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β (πΊβπ§) = β¦π§ / π₯β¦(π΅ β πΆ)) |
36 | | ellimcabssub0.f |
. . . . . . . . . . . . . 14
β’ πΉ = (π₯ β π΄ β¦ π΅) |
37 | 36 | fvmpts 6952 |
. . . . . . . . . . . . 13
β’ ((π§ β π΄ β§ β¦π§ / π₯β¦π΅ β β) β (πΉβπ§) = β¦π§ / π₯β¦π΅) |
38 | 11, 30, 37 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β π΄) β (πΉβπ§) = β¦π§ / π₯β¦π΅) |
39 | 38 | oveq1d 7373 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β ((πΉβπ§) β πΆ) = (β¦π§ / π₯β¦π΅ β πΆ)) |
40 | 13, 39 | eqtr4id 2796 |
. . . . . . . . . 10
β’ ((π β§ π§ β π΄) β β¦π§ / π₯β¦(π΅ β πΆ) = ((πΉβπ§) β πΆ)) |
41 | 10, 35, 40 | 3eqtrrd 2782 |
. . . . . . . . 9
β’ ((π β§ π§ β π΄) β ((πΉβπ§) β πΆ) = ((πΊβπ§) β 0)) |
42 | 41 | fveq2d 6847 |
. . . . . . . 8
β’ ((π β§ π§ β π΄) β (absβ((πΉβπ§) β πΆ)) = (absβ((πΊβπ§) β 0))) |
43 | 42 | breq1d 5116 |
. . . . . . 7
β’ ((π β§ π§ β π΄) β ((absβ((πΉβπ§) β πΆ)) < π¦ β (absβ((πΊβπ§) β 0)) < π¦)) |
44 | 43 | imbi2d 341 |
. . . . . 6
β’ ((π β§ π§ β π΄) β (((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΉβπ§) β πΆ)) < π¦) β ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΊβπ§) β 0)) < π¦))) |
45 | 44 | ralbidva 3173 |
. . . . 5
β’ (π β (βπ§ β π΄ ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΉβπ§) β πΆ)) < π¦) β βπ§ β π΄ ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΊβπ§) β 0)) < π¦))) |
46 | 45 | rexbidv 3176 |
. . . 4
β’ (π β (βπ€ β β+ βπ§ β π΄ ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΉβπ§) β πΆ)) < π¦) β βπ€ β β+ βπ§ β π΄ ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΊβπ§) β 0)) < π¦))) |
47 | 46 | ralbidv 3175 |
. . 3
β’ (π β (βπ¦ β β+
βπ€ β
β+ βπ§ β π΄ ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΉβπ§) β πΆ)) < π¦) β βπ¦ β β+ βπ€ β β+
βπ§ β π΄ ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΊβπ§) β 0)) < π¦))) |
48 | 3, 47 | anbi12d 632 |
. 2
β’ (π β ((πΆ β β β§ βπ¦ β β+
βπ€ β
β+ βπ§ β π΄ ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΉβπ§) β πΆ)) < π¦)) β (0 β β β§
βπ¦ β
β+ βπ€ β β+ βπ§ β π΄ ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΊβπ§) β 0)) < π¦)))) |
49 | 4, 36 | fmptd 7063 |
. . 3
β’ (π β πΉ:π΄βΆβ) |
50 | | ellimcabssub0.a |
. . 3
β’ (π β π΄ β β) |
51 | | ellimcabssub0.p |
. . 3
β’ (π β π· β β) |
52 | 49, 50, 51 | ellimc3 25246 |
. 2
β’ (π β (πΆ β (πΉ limβ π·) β (πΆ β β β§ βπ¦ β β+
βπ€ β
β+ βπ§ β π΄ ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΉβπ§) β πΆ)) < π¦)))) |
53 | 8, 50, 51 | ellimc3 25246 |
. 2
β’ (π β (0 β (πΊ limβ π·) β (0 β β β§
βπ¦ β
β+ βπ€ β β+ βπ§ β π΄ ((π§ β π· β§ (absβ(π§ β π·)) < π€) β (absβ((πΊβπ§) β 0)) < π¦)))) |
54 | 48, 52, 53 | 3bitr4d 311 |
1
β’ (π β (πΆ β (πΉ limβ π·) β 0 β (πΊ limβ π·))) |