Step | Hyp | Ref
| Expression |
1 | | idlimc.x |
. 2
β’ (π β π β β) |
2 | | simpr 486 |
. . . 4
β’ ((π β§ π€ β β+) β π€ β
β+) |
3 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β π₯ β π΄) |
4 | | idlimc.f |
. . . . . . . . . . . . . 14
β’ πΉ = (π₯ β π΄ β¦ π₯) |
5 | 4 | fvmpt2 6918 |
. . . . . . . . . . . . 13
β’ ((π₯ β π΄ β§ π₯ β π΄) β (πΉβπ₯) = π₯) |
6 | 3, 3, 5 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) = π₯) |
7 | 6 | fvoveq1d 7329 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (absβ((πΉβπ₯) β π)) = (absβ(π₯ β π))) |
8 | 7 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π΄) β§ (absβ(π₯ β π)) < π€) β (absβ((πΉβπ₯) β π)) = (absβ(π₯ β π))) |
9 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π΄) β§ (absβ(π₯ β π)) < π€) β (absβ(π₯ β π)) < π€) |
10 | 8, 9 | eqbrtrd 5103 |
. . . . . . . . 9
β’ (((π β§ π₯ β π΄) β§ (absβ(π₯ β π)) < π€) β (absβ((πΉβπ₯) β π)) < π€) |
11 | 10 | adantrl 714 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ (π₯ β π β§ (absβ(π₯ β π)) < π€)) β (absβ((πΉβπ₯) β π)) < π€) |
12 | 11 | ex 414 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β ((π₯ β π β§ (absβ(π₯ β π)) < π€) β (absβ((πΉβπ₯) β π)) < π€)) |
13 | 12 | adantlr 713 |
. . . . . 6
β’ (((π β§ π€ β β+) β§ π₯ β π΄) β ((π₯ β π β§ (absβ(π₯ β π)) < π€) β (absβ((πΉβπ₯) β π)) < π€)) |
14 | 13 | ralrimiva 3140 |
. . . . 5
β’ ((π β§ π€ β β+) β
βπ₯ β π΄ ((π₯ β π β§ (absβ(π₯ β π)) < π€) β (absβ((πΉβπ₯) β π)) < π€)) |
15 | | nfcv 2905 |
. . . . . . . . 9
β’
β²π§π₯ |
16 | | nfcv 2905 |
. . . . . . . . 9
β’
β²π§π |
17 | 15, 16 | nfne 3043 |
. . . . . . . 8
β’
β²π§ π₯ β π |
18 | | nfv 1915 |
. . . . . . . 8
β’
β²π§(absβ(π₯ β π)) < π€ |
19 | 17, 18 | nfan 1900 |
. . . . . . 7
β’
β²π§(π₯ β π β§ (absβ(π₯ β π)) < π€) |
20 | | nfv 1915 |
. . . . . . 7
β’
β²π§(absβ((πΉβπ₯) β π)) < π€ |
21 | 19, 20 | nfim 1897 |
. . . . . 6
β’
β²π§((π₯ β π β§ (absβ(π₯ β π)) < π€) β (absβ((πΉβπ₯) β π)) < π€) |
22 | | nfv 1915 |
. . . . . . 7
β’
β²π₯(π§ β π β§ (absβ(π§ β π)) < π€) |
23 | | nfcv 2905 |
. . . . . . . . 9
β’
β²π₯abs |
24 | | nfmpt1 5189 |
. . . . . . . . . . . 12
β’
β²π₯(π₯ β π΄ β¦ π₯) |
25 | 4, 24 | nfcxfr 2903 |
. . . . . . . . . . 11
β’
β²π₯πΉ |
26 | | nfcv 2905 |
. . . . . . . . . . 11
β’
β²π₯π§ |
27 | 25, 26 | nffv 6814 |
. . . . . . . . . 10
β’
β²π₯(πΉβπ§) |
28 | | nfcv 2905 |
. . . . . . . . . 10
β’
β²π₯
β |
29 | | nfcv 2905 |
. . . . . . . . . 10
β’
β²π₯π |
30 | 27, 28, 29 | nfov 7337 |
. . . . . . . . 9
β’
β²π₯((πΉβπ§) β π) |
31 | 23, 30 | nffv 6814 |
. . . . . . . 8
β’
β²π₯(absβ((πΉβπ§) β π)) |
32 | | nfcv 2905 |
. . . . . . . 8
β’
β²π₯
< |
33 | | nfcv 2905 |
. . . . . . . 8
β’
β²π₯π€ |
34 | 31, 32, 33 | nfbr 5128 |
. . . . . . 7
β’
β²π₯(absβ((πΉβπ§) β π)) < π€ |
35 | 22, 34 | nfim 1897 |
. . . . . 6
β’
β²π₯((π§ β π β§ (absβ(π§ β π)) < π€) β (absβ((πΉβπ§) β π)) < π€) |
36 | | neeq1 3004 |
. . . . . . . 8
β’ (π₯ = π§ β (π₯ β π β π§ β π)) |
37 | | fvoveq1 7330 |
. . . . . . . . 9
β’ (π₯ = π§ β (absβ(π₯ β π)) = (absβ(π§ β π))) |
38 | 37 | breq1d 5091 |
. . . . . . . 8
β’ (π₯ = π§ β ((absβ(π₯ β π)) < π€ β (absβ(π§ β π)) < π€)) |
39 | 36, 38 | anbi12d 632 |
. . . . . . 7
β’ (π₯ = π§ β ((π₯ β π β§ (absβ(π₯ β π)) < π€) β (π§ β π β§ (absβ(π§ β π)) < π€))) |
40 | 39 | imbrov2fvoveq 7332 |
. . . . . 6
β’ (π₯ = π§ β (((π₯ β π β§ (absβ(π₯ β π)) < π€) β (absβ((πΉβπ₯) β π)) < π€) β ((π§ β π β§ (absβ(π§ β π)) < π€) β (absβ((πΉβπ§) β π)) < π€))) |
41 | 21, 35, 40 | cbvralw 3385 |
. . . . 5
β’
(βπ₯ β
π΄ ((π₯ β π β§ (absβ(π₯ β π)) < π€) β (absβ((πΉβπ₯) β π)) < π€) β βπ§ β π΄ ((π§ β π β§ (absβ(π§ β π)) < π€) β (absβ((πΉβπ§) β π)) < π€)) |
42 | 14, 41 | sylib 217 |
. . . 4
β’ ((π β§ π€ β β+) β
βπ§ β π΄ ((π§ β π β§ (absβ(π§ β π)) < π€) β (absβ((πΉβπ§) β π)) < π€)) |
43 | | brimralrspcev 5142 |
. . . 4
β’ ((π€ β β+
β§ βπ§ β
π΄ ((π§ β π β§ (absβ(π§ β π)) < π€) β (absβ((πΉβπ§) β π)) < π€)) β βπ¦ β β+ βπ§ β π΄ ((π§ β π β§ (absβ(π§ β π)) < π¦) β (absβ((πΉβπ§) β π)) < π€)) |
44 | 2, 42, 43 | syl2anc 585 |
. . 3
β’ ((π β§ π€ β β+) β
βπ¦ β
β+ βπ§ β π΄ ((π§ β π β§ (absβ(π§ β π)) < π¦) β (absβ((πΉβπ§) β π)) < π€)) |
45 | 44 | ralrimiva 3140 |
. 2
β’ (π β βπ€ β β+ βπ¦ β β+
βπ§ β π΄ ((π§ β π β§ (absβ(π§ β π)) < π¦) β (absβ((πΉβπ§) β π)) < π€)) |
46 | | idlimc.a |
. . . . 5
β’ (π β π΄ β β) |
47 | 46 | sselda 3926 |
. . . 4
β’ ((π β§ π₯ β π΄) β π₯ β β) |
48 | 47, 4 | fmptd 7020 |
. . 3
β’ (π β πΉ:π΄βΆβ) |
49 | 48, 46, 1 | ellimc3 25088 |
. 2
β’ (π β (π β (πΉ limβ π) β (π β β β§ βπ€ β β+
βπ¦ β
β+ βπ§ β π΄ ((π§ β π β§ (absβ(π§ β π)) < π¦) β (absβ((πΉβπ§) β π)) < π€)))) |
50 | 1, 45, 49 | mpbir2and 711 |
1
β’ (π β π β (πΉ limβ π)) |