Step | Hyp | Ref
| Expression |
1 | | rlimf 15389 |
. . . . . 6
β’ (πΉ βπ
π΄ β πΉ:dom πΉβΆβ) |
2 | 1 | ffvelcdmda 7036 |
. . . . 5
β’ ((πΉ βπ
π΄ β§ π§ β dom πΉ) β (πΉβπ§) β β) |
3 | 2 | ralrimiva 3140 |
. . . 4
β’ (πΉ βπ
π΄ β βπ§ β dom πΉ(πΉβπ§) β β) |
4 | | 1rp 12924 |
. . . . 5
β’ 1 β
β+ |
5 | 4 | a1i 11 |
. . . 4
β’ (πΉ βπ
π΄ β 1 β
β+) |
6 | 1 | feqmptd 6911 |
. . . . 5
β’ (πΉ βπ
π΄ β πΉ = (π§ β dom πΉ β¦ (πΉβπ§))) |
7 | | id 22 |
. . . . 5
β’ (πΉ βπ
π΄ β πΉ βπ π΄) |
8 | 6, 7 | eqbrtrrd 5130 |
. . . 4
β’ (πΉ βπ
π΄ β (π§ β dom πΉ β¦ (πΉβπ§)) βπ π΄) |
9 | 3, 5, 8 | rlimi 15401 |
. . 3
β’ (πΉ βπ
π΄ β βπ¦ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < 1)) |
10 | | rlimcl 15391 |
. . . . . . . 8
β’ (πΉ βπ
π΄ β π΄ β β) |
11 | 10 | adantr 482 |
. . . . . . 7
β’ ((πΉ βπ
π΄ β§ π¦ β β) β π΄ β β) |
12 | 11 | abscld 15327 |
. . . . . 6
β’ ((πΉ βπ
π΄ β§ π¦ β β) β (absβπ΄) β
β) |
13 | | peano2re 11333 |
. . . . . 6
β’
((absβπ΄)
β β β ((absβπ΄) + 1) β β) |
14 | 12, 13 | syl 17 |
. . . . 5
β’ ((πΉ βπ
π΄ β§ π¦ β β) β ((absβπ΄) + 1) β
β) |
15 | 2 | adantlr 714 |
. . . . . . . . . . 11
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β (πΉβπ§) β β) |
16 | 11 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β π΄ β β) |
17 | 15, 16 | abs2difd 15348 |
. . . . . . . . . 10
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β ((absβ(πΉβπ§)) β (absβπ΄)) β€ (absβ((πΉβπ§) β π΄))) |
18 | 15 | abscld 15327 |
. . . . . . . . . . . 12
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β (absβ(πΉβπ§)) β β) |
19 | 12 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β (absβπ΄) β β) |
20 | 18, 19 | resubcld 11588 |
. . . . . . . . . . 11
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β ((absβ(πΉβπ§)) β (absβπ΄)) β β) |
21 | 15, 16 | subcld 11517 |
. . . . . . . . . . . 12
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β ((πΉβπ§) β π΄) β β) |
22 | 21 | abscld 15327 |
. . . . . . . . . . 11
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β (absβ((πΉβπ§) β π΄)) β β) |
23 | | 1red 11161 |
. . . . . . . . . . 11
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β 1 β β) |
24 | | lelttr 11250 |
. . . . . . . . . . 11
β’
((((absβ(πΉβπ§)) β (absβπ΄)) β β β§ (absβ((πΉβπ§) β π΄)) β β β§ 1 β β)
β ((((absβ(πΉβπ§)) β (absβπ΄)) β€ (absβ((πΉβπ§) β π΄)) β§ (absβ((πΉβπ§) β π΄)) < 1) β ((absβ(πΉβπ§)) β (absβπ΄)) < 1)) |
25 | 20, 22, 23, 24 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β ((((absβ(πΉβπ§)) β (absβπ΄)) β€ (absβ((πΉβπ§) β π΄)) β§ (absβ((πΉβπ§) β π΄)) < 1) β ((absβ(πΉβπ§)) β (absβπ΄)) < 1)) |
26 | 17, 25 | mpand 694 |
. . . . . . . . 9
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β ((absβ((πΉβπ§) β π΄)) < 1 β ((absβ(πΉβπ§)) β (absβπ΄)) < 1)) |
27 | 18, 19, 23 | ltsubadd2d 11758 |
. . . . . . . . 9
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β (((absβ(πΉβπ§)) β (absβπ΄)) < 1 β (absβ(πΉβπ§)) < ((absβπ΄) + 1))) |
28 | 26, 27 | sylibd 238 |
. . . . . . . 8
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β ((absβ((πΉβπ§) β π΄)) < 1 β (absβ(πΉβπ§)) < ((absβπ΄) + 1))) |
29 | 14 | adantr 482 |
. . . . . . . . 9
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β ((absβπ΄) + 1) β β) |
30 | | ltle 11248 |
. . . . . . . . 9
β’
(((absβ(πΉβπ§)) β β β§ ((absβπ΄) + 1) β β) β
((absβ(πΉβπ§)) < ((absβπ΄) + 1) β (absβ(πΉβπ§)) β€ ((absβπ΄) + 1))) |
31 | 18, 29, 30 | syl2anc 585 |
. . . . . . . 8
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β ((absβ(πΉβπ§)) < ((absβπ΄) + 1) β (absβ(πΉβπ§)) β€ ((absβπ΄) + 1))) |
32 | 28, 31 | syld 47 |
. . . . . . 7
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β ((absβ((πΉβπ§) β π΄)) < 1 β (absβ(πΉβπ§)) β€ ((absβπ΄) + 1))) |
33 | 32 | imim2d 57 |
. . . . . 6
β’ (((πΉ βπ
π΄ β§ π¦ β β) β§ π§ β dom πΉ) β ((π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < 1) β (π¦ β€ π§ β (absβ(πΉβπ§)) β€ ((absβπ΄) + 1)))) |
34 | 33 | ralimdva 3161 |
. . . . 5
β’ ((πΉ βπ
π΄ β§ π¦ β β) β (βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < 1) β βπ§ β dom πΉ(π¦ β€ π§ β (absβ(πΉβπ§)) β€ ((absβπ΄) + 1)))) |
35 | | breq2 5110 |
. . . . . . . 8
β’ (π€ = ((absβπ΄) + 1) β ((absβ(πΉβπ§)) β€ π€ β (absβ(πΉβπ§)) β€ ((absβπ΄) + 1))) |
36 | 35 | imbi2d 341 |
. . . . . . 7
β’ (π€ = ((absβπ΄) + 1) β ((π¦ β€ π§ β (absβ(πΉβπ§)) β€ π€) β (π¦ β€ π§ β (absβ(πΉβπ§)) β€ ((absβπ΄) + 1)))) |
37 | 36 | ralbidv 3171 |
. . . . . 6
β’ (π€ = ((absβπ΄) + 1) β (βπ§ β dom πΉ(π¦ β€ π§ β (absβ(πΉβπ§)) β€ π€) β βπ§ β dom πΉ(π¦ β€ π§ β (absβ(πΉβπ§)) β€ ((absβπ΄) + 1)))) |
38 | 37 | rspcev 3580 |
. . . . 5
β’
((((absβπ΄) +
1) β β β§ βπ§ β dom πΉ(π¦ β€ π§ β (absβ(πΉβπ§)) β€ ((absβπ΄) + 1))) β βπ€ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ(πΉβπ§)) β€ π€)) |
39 | 14, 34, 38 | syl6an 683 |
. . . 4
β’ ((πΉ βπ
π΄ β§ π¦ β β) β (βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < 1) β βπ€ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ(πΉβπ§)) β€ π€))) |
40 | 39 | reximdva 3162 |
. . 3
β’ (πΉ βπ
π΄ β (βπ¦ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ((πΉβπ§) β π΄)) < 1) β βπ¦ β β βπ€ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ(πΉβπ§)) β€ π€))) |
41 | 9, 40 | mpd 15 |
. 2
β’ (πΉ βπ
π΄ β βπ¦ β β βπ€ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ(πΉβπ§)) β€ π€)) |
42 | | rlimss 15390 |
. . 3
β’ (πΉ βπ
π΄ β dom πΉ β
β) |
43 | | elo12 15415 |
. . 3
β’ ((πΉ:dom πΉβΆβ β§ dom πΉ β β) β (πΉ β π(1) β βπ¦ β β βπ€ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ(πΉβπ§)) β€ π€))) |
44 | 1, 42, 43 | syl2anc 585 |
. 2
β’ (πΉ βπ
π΄ β (πΉ β π(1) β βπ¦ β β βπ€ β β βπ§ β dom πΉ(π¦ β€ π§ β (absβ(πΉβπ§)) β€ π€))) |
45 | 41, 44 | mpbird 257 |
1
β’ (πΉ βπ
π΄ β πΉ β π(1)) |