Step | Hyp | Ref
| Expression |
1 | | ulmbdd.z |
. . 3
β’ π =
(β€β₯βπ) |
2 | | ulmbdd.m |
. . 3
β’ (π β π β β€) |
3 | | ulmbdd.f |
. . 3
β’ (π β πΉ:πβΆ(β βm π)) |
4 | | eqidd 2738 |
. . 3
β’ ((π β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
5 | | eqidd 2738 |
. . 3
β’ ((π β§ π§ β π) β (πΊβπ§) = (πΊβπ§)) |
6 | | ulmbdd.u |
. . 3
β’ (π β πΉ(βπ’βπ)πΊ) |
7 | | 1rp 12926 |
. . . 4
β’ 1 β
β+ |
8 | 7 | a1i 11 |
. . 3
β’ (π β 1 β
β+) |
9 | 1, 2, 3, 4, 5, 6, 8 | ulmi 25761 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1) |
10 | 1 | r19.2uz 15243 |
. . 3
β’
(βπ β
π βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1 β βπ β π βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1) |
11 | | ulmbdd.b |
. . . . . 6
β’ ((π β§ π β π) β βπ₯ β β βπ§ β π (absβ((πΉβπ)βπ§)) β€ π₯) |
12 | | r19.26 3115 |
. . . . . . . . 9
β’
(βπ§ β
π ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1) β (βπ§ β π (absβ((πΉβπ)βπ§)) β€ π₯ β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1)) |
13 | | peano2re 11335 |
. . . . . . . . . . 11
β’ (π₯ β β β (π₯ + 1) β
β) |
14 | 13 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π₯ β β) β (π₯ + 1) β β) |
15 | | ulmcl 25756 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) |
16 | 6, 15 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β πΊ:πβΆβ) |
17 | 16 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β πΊ:πβΆβ) |
18 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β π§ β π) |
19 | 17, 18 | ffvelcdmd 7041 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (πΊβπ§) β β) |
20 | 19 | abscld 15328 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ(πΊβπ§)) β β) |
21 | 3 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β πΉ:πβΆ(β βm π)) |
22 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β π β π) |
23 | 21, 22 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (πΉβπ) β (β βm π)) |
24 | | elmapi 8794 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (πΉβπ):πβΆβ) |
26 | 25, 18 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β ((πΉβπ)βπ§) β β) |
27 | 26 | abscld 15328 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ((πΉβπ)βπ§)) β β) |
28 | 19, 26 | subcld 11519 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β ((πΊβπ§) β ((πΉβπ)βπ§)) β β) |
29 | 28 | abscld 15328 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ((πΊβπ§) β ((πΉβπ)βπ§))) β β) |
30 | 27, 29 | readdcld 11191 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β ((absβ((πΉβπ)βπ§)) + (absβ((πΊβπ§) β ((πΉβπ)βπ§)))) β β) |
31 | 14 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (π₯ + 1) β β) |
32 | 26, 19 | pncan3d 11522 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (((πΉβπ)βπ§) + ((πΊβπ§) β ((πΉβπ)βπ§))) = (πΊβπ§)) |
33 | 32 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ(((πΉβπ)βπ§) + ((πΊβπ§) β ((πΉβπ)βπ§)))) = (absβ(πΊβπ§))) |
34 | 26, 28 | abstrid 15348 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ(((πΉβπ)βπ§) + ((πΊβπ§) β ((πΉβπ)βπ§)))) β€ ((absβ((πΉβπ)βπ§)) + (absβ((πΊβπ§) β ((πΉβπ)βπ§))))) |
35 | 33, 34 | eqbrtrrd 5134 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ(πΊβπ§)) β€ ((absβ((πΉβπ)βπ§)) + (absβ((πΊβπ§) β ((πΉβπ)βπ§))))) |
36 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β π₯ β β) |
37 | | 1re 11162 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β 1 β
β) |
39 | | simprrl 780 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ((πΉβπ)βπ§)) β€ π₯) |
40 | 19, 26 | abssubd 15345 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ((πΊβπ§) β ((πΉβπ)βπ§))) = (absβ(((πΉβπ)βπ§) β (πΊβπ§)))) |
41 | | simprrr 781 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1) |
42 | 40, 41 | eqbrtrd 5132 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ((πΊβπ§) β ((πΉβπ)βπ§))) < 1) |
43 | | ltle 11250 |
. . . . . . . . . . . . . . . 16
β’
(((absβ((πΊβπ§) β ((πΉβπ)βπ§))) β β β§ 1 β β)
β ((absβ((πΊβπ§) β ((πΉβπ)βπ§))) < 1 β (absβ((πΊβπ§) β ((πΉβπ)βπ§))) β€ 1)) |
44 | 29, 37, 43 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β ((absβ((πΊβπ§) β ((πΉβπ)βπ§))) < 1 β (absβ((πΊβπ§) β ((πΉβπ)βπ§))) β€ 1)) |
45 | 42, 44 | mpd 15 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ((πΊβπ§) β ((πΉβπ)βπ§))) β€ 1) |
46 | 27, 29, 36, 38, 39, 45 | le2addd 11781 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β ((absβ((πΉβπ)βπ§)) + (absβ((πΊβπ§) β ((πΉβπ)βπ§)))) β€ (π₯ + 1)) |
47 | 20, 30, 31, 35, 46 | letrd 11319 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π) β§ π₯ β β) β§ (π§ β π β§ ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1))) β (absβ(πΊβπ§)) β€ (π₯ + 1)) |
48 | 47 | expr 458 |
. . . . . . . . . . 11
β’ ((((π β§ π β π) β§ π₯ β β) β§ π§ β π) β (((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1) β (absβ(πΊβπ§)) β€ (π₯ + 1))) |
49 | 48 | ralimdva 3165 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π₯ β β) β (βπ§ β π ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1) β βπ§ β π (absβ(πΊβπ§)) β€ (π₯ + 1))) |
50 | | brralrspcev 5170 |
. . . . . . . . . 10
β’ (((π₯ + 1) β β β§
βπ§ β π (absβ(πΊβπ§)) β€ (π₯ + 1)) β βπ¦ β β βπ§ β π (absβ(πΊβπ§)) β€ π¦) |
51 | 14, 49, 50 | syl6an 683 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π₯ β β) β (βπ§ β π ((absβ((πΉβπ)βπ§)) β€ π₯ β§ (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1) β βπ¦ β β βπ§ β π (absβ(πΊβπ§)) β€ π¦)) |
52 | 12, 51 | biimtrrid 242 |
. . . . . . . 8
β’ (((π β§ π β π) β§ π₯ β β) β ((βπ§ β π (absβ((πΉβπ)βπ§)) β€ π₯ β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1) β βπ¦ β β βπ§ β π (absβ(πΊβπ§)) β€ π¦)) |
53 | 52 | expd 417 |
. . . . . . 7
β’ (((π β§ π β π) β§ π₯ β β) β (βπ§ β π (absβ((πΉβπ)βπ§)) β€ π₯ β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1 β βπ¦ β β βπ§ β π (absβ(πΊβπ§)) β€ π¦))) |
54 | 53 | rexlimdva 3153 |
. . . . . 6
β’ ((π β§ π β π) β (βπ₯ β β βπ§ β π (absβ((πΉβπ)βπ§)) β€ π₯ β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1 β βπ¦ β β βπ§ β π (absβ(πΊβπ§)) β€ π¦))) |
55 | 11, 54 | mpd 15 |
. . . . 5
β’ ((π β§ π β π) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1 β βπ¦ β β βπ§ β π (absβ(πΊβπ§)) β€ π¦)) |
56 | | breq2 5114 |
. . . . . . 7
β’ (π¦ = π₯ β ((absβ(πΊβπ§)) β€ π¦ β (absβ(πΊβπ§)) β€ π₯)) |
57 | 56 | ralbidv 3175 |
. . . . . 6
β’ (π¦ = π₯ β (βπ§ β π (absβ(πΊβπ§)) β€ π¦ β βπ§ β π (absβ(πΊβπ§)) β€ π₯)) |
58 | 57 | cbvrexvw 3229 |
. . . . 5
β’
(βπ¦ β
β βπ§ β
π (absβ(πΊβπ§)) β€ π¦ β βπ₯ β β βπ§ β π (absβ(πΊβπ§)) β€ π₯) |
59 | 55, 58 | syl6ib 251 |
. . . 4
β’ ((π β§ π β π) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1 β βπ₯ β β βπ§ β π (absβ(πΊβπ§)) β€ π₯)) |
60 | 59 | rexlimdva 3153 |
. . 3
β’ (π β (βπ β π βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1 β βπ₯ β β βπ§ β π (absβ(πΊβπ§)) β€ π₯)) |
61 | 10, 60 | syl5 34 |
. 2
β’ (π β (βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πΊβπ§))) < 1 β βπ₯ β β βπ§ β π (absβ(πΊβπ§)) β€ π₯)) |
62 | 9, 61 | mpd 15 |
1
β’ (π β βπ₯ β β βπ§ β π (absβ(πΊβπ§)) β€ π₯) |