Step | Hyp | Ref
| Expression |
1 | | ulmcn.u |
. . 3
β’ (π β πΉ(βπ’βπ)πΊ) |
2 | | ulmcl 25756 |
. . 3
β’ (πΉ(βπ’βπ)πΊ β πΊ:πβΆβ) |
3 | 1, 2 | syl 17 |
. 2
β’ (π β πΊ:πβΆβ) |
4 | | ulmcn.z |
. . . . 5
β’ π =
(β€β₯βπ) |
5 | | ulmcn.m |
. . . . . 6
β’ (π β π β β€) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β π β
β€) |
7 | | ulmcn.f |
. . . . . . 7
β’ (π β πΉ:πβΆ(πβcnββ)) |
8 | | cncff 24272 |
. . . . . . . . 9
β’ (π₯ β (πβcnββ) β π₯:πβΆβ) |
9 | | cnex 11139 |
. . . . . . . . . 10
β’ β
β V |
10 | | cncfrss 24270 |
. . . . . . . . . . 11
β’ (π₯ β (πβcnββ) β π β β) |
11 | | ssexg 5285 |
. . . . . . . . . . 11
β’ ((π β β β§ β
β V) β π β
V) |
12 | 10, 9, 11 | sylancl 587 |
. . . . . . . . . 10
β’ (π₯ β (πβcnββ) β π β V) |
13 | | elmapg 8785 |
. . . . . . . . . 10
β’ ((β
β V β§ π β V)
β (π₯ β (β
βm π)
β π₯:πβΆβ)) |
14 | 9, 12, 13 | sylancr 588 |
. . . . . . . . 9
β’ (π₯ β (πβcnββ) β (π₯ β (β βm π) β π₯:πβΆβ)) |
15 | 8, 14 | mpbird 257 |
. . . . . . . 8
β’ (π₯ β (πβcnββ) β π₯ β (β βm π)) |
16 | 15 | ssriv 3953 |
. . . . . . 7
β’ (πβcnββ) β (β βm
π) |
17 | | fss 6690 |
. . . . . . 7
β’ ((πΉ:πβΆ(πβcnββ) β§ (πβcnββ) β (β βm
π)) β πΉ:πβΆ(β βm π)) |
18 | 7, 16, 17 | sylancl 587 |
. . . . . 6
β’ (π β πΉ:πβΆ(β βm π)) |
19 | 18 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β πΉ:πβΆ(β βm π)) |
20 | | eqidd 2738 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β β+)) β§ (π β π β§ π€ β π)) β ((πΉβπ)βπ€) = ((πΉβπ)βπ€)) |
21 | | eqidd 2738 |
. . . . 5
β’ (((π β§ (π₯ β π β§ π¦ β β+)) β§ π€ β π) β (πΊβπ€) = (πΊβπ€)) |
22 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β πΉ(βπ’βπ)πΊ) |
23 | | rphalfcl 12949 |
. . . . . . 7
β’ (π¦ β β+
β (π¦ / 2) β
β+) |
24 | 23 | ad2antll 728 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β (π¦ / 2) β
β+) |
25 | 24 | rphalfcld 12976 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β ((π¦ / 2) / 2) β
β+) |
26 | 4, 6, 19, 20, 21, 22, 25 | ulmi 25761 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β
βπ β π βπ β (β€β₯βπ)βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) |
27 | 4 | r19.2uz 15243 |
. . . . 5
β’
(βπ β
π βπ β
(β€β₯βπ)βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β βπ β π βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) |
28 | | simplrl 776 |
. . . . . . . 8
β’ (((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β π₯ β π) |
29 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π€ = π₯ β ((πΉβπ)βπ€) = ((πΉβπ)βπ₯)) |
30 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π€ = π₯ β (πΊβπ€) = (πΊβπ₯)) |
31 | 29, 30 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (π€ = π₯ β (((πΉβπ)βπ€) β (πΊβπ€)) = (((πΉβπ)βπ₯) β (πΊβπ₯))) |
32 | 31 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π€ = π₯ β (absβ(((πΉβπ)βπ€) β (πΊβπ€))) = (absβ(((πΉβπ)βπ₯) β (πΊβπ₯)))) |
33 | 32 | breq1d 5120 |
. . . . . . . . 9
β’ (π€ = π₯ β ((absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2))) |
34 | 33 | rspcv 3580 |
. . . . . . . 8
β’ (π₯ β π β (βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2))) |
35 | 28, 34 | syl 17 |
. . . . . . 7
β’ (((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β (βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2))) |
36 | 7 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β πΉ:πβΆ(πβcnββ)) |
37 | 36 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β (πΉβπ) β (πβcnββ)) |
38 | 24 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β (π¦ / 2) β
β+) |
39 | | cncfi 24273 |
. . . . . . . . . . 11
β’ (((πΉβπ) β (πβcnββ) β§ π₯ β π β§ (π¦ / 2) β β+) β
βπ§ β
β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2))) |
40 | 37, 28, 38, 39 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β βπ§ β β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2))) |
41 | 40 | ad2antrr 725 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β βπ§ β β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2))) |
42 | | r19.26 3115 |
. . . . . . . . . . . . 13
β’
(βπ€ β
π ((absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β§ ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2))) β (βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β§ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2)))) |
43 | 19 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β πΉ:πβΆ(β βm π)) |
44 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β π β π) |
45 | 43, 44 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (πΉβπ) β (β βm π)) |
46 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (πΉβπ):πβΆβ) |
48 | 28 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β π₯ β π) |
49 | 47, 48 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((πΉβπ)βπ₯) β β) |
50 | 3 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β πΊ:πβΆβ) |
51 | 50, 48 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (πΊβπ₯) β β) |
52 | 49, 51 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((πΉβπ)βπ₯) β (πΊβπ₯)) β β) |
53 | 52 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) β β) |
54 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΉβπ):πβΆβ β§ π€ β π) β ((πΉβπ)βπ€) β β) |
55 | 47, 54 | sylancom 589 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((πΉβπ)βπ€) β β) |
56 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΊ:πβΆβ β§ π€ β π) β (πΊβπ€) β β) |
57 | 50, 56 | sylancom 589 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (πΊβπ€) β β) |
58 | 55, 57 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((πΉβπ)βπ€) β (πΊβπ€)) β β) |
59 | 58 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ(((πΉβπ)βπ€) β (πΊβπ€))) β β) |
60 | 38 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (π¦ / 2) β
β+) |
61 | 60 | rphalfcld 12976 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((π¦ / 2) / 2) β
β+) |
62 | 61 | rpred 12964 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((π¦ / 2) / 2) β β) |
63 | | lt2add 11647 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) β β β§ (absβ(((πΉβπ)βπ€) β (πΊβπ€))) β β) β§ (((π¦ / 2) / 2) β β β§
((π¦ / 2) / 2) β
β)) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2) β§ (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) < (((π¦ / 2) / 2) + ((π¦ / 2) / 2)))) |
64 | 53, 59, 62, 62, 63 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2) β§ (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) < (((π¦ / 2) / 2) + ((π¦ / 2) / 2)))) |
65 | 60 | rpred 12964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (π¦ / 2) β β) |
66 | 65 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (π¦ / 2) β β) |
67 | 66 | 2halvesd 12406 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((π¦ / 2) / 2) + ((π¦ / 2) / 2)) = (π¦ / 2)) |
68 | 67 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) < (((π¦ / 2) / 2) + ((π¦ / 2) / 2)) β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) < (π¦ / 2))) |
69 | 53, 59 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) β β) |
70 | 55, 49 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((πΉβπ)βπ€) β ((πΉβπ)βπ₯)) β β) |
71 | 70 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) β β) |
72 | | lt2add 11647 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) β β β§ (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) β β) β§ ((π¦ / 2) β β β§
(π¦ / 2) β β))
β ((((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) < (π¦ / 2) β§ (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2)) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) < ((π¦ / 2) + (π¦ / 2)))) |
73 | 69, 71, 65, 65, 72 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) < (π¦ / 2) β§ (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2)) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) < ((π¦ / 2) + (π¦ / 2)))) |
74 | | rpre 12930 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π¦ β β+
β π¦ β
β) |
75 | 74 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β π¦ β
β) |
76 | 75 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β π¦ β β) |
77 | 76 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β π¦ β β) |
78 | 77 | 2halvesd 12406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((π¦ / 2) + (π¦ / 2)) = π¦) |
79 | 78 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) < ((π¦ / 2) + (π¦ / 2)) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) < π¦)) |
80 | 57, 51 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((πΊβπ€) β (πΊβπ₯)) β β) |
81 | 80 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ((πΊβπ€) β (πΊβπ₯))) β β) |
82 | 57, 49 | subcld 11519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((πΊβπ€) β ((πΉβπ)βπ₯)) β β) |
83 | 82 | abscld 15328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ((πΊβπ€) β ((πΉβπ)βπ₯))) β β) |
84 | 53, 83 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ((πΊβπ€) β ((πΉβπ)βπ₯)))) β β) |
85 | 69, 71 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) β β) |
86 | 57, 51, 49 | abs3difd 15352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ((πΊβπ€) β (πΊβπ₯))) β€ ((absβ((πΊβπ€) β ((πΉβπ)βπ₯))) + (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))))) |
87 | 83 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ((πΊβπ€) β ((πΉβπ)βπ₯))) β β) |
88 | 53 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) β β) |
89 | 87, 88 | addcomd 11364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((absβ((πΊβπ€) β ((πΉβπ)βπ₯))) + (absβ(((πΉβπ)βπ₯) β (πΊβπ₯)))) = ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ((πΊβπ€) β ((πΉβπ)βπ₯))))) |
90 | 86, 89 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ((πΊβπ€) β (πΊβπ₯))) β€ ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ((πΊβπ€) β ((πΉβπ)βπ₯))))) |
91 | 59, 71 | readdcld 11191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((absβ(((πΉβπ)βπ€) β (πΊβπ€))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) β β) |
92 | 57, 49, 55 | abs3difd 15352 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ((πΊβπ€) β ((πΉβπ)βπ₯))) β€ ((absβ((πΊβπ€) β ((πΉβπ)βπ€))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))))) |
93 | 57, 55 | abssubd 15345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ((πΊβπ€) β ((πΉβπ)βπ€))) = (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) |
94 | 93 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((absβ((πΊβπ€) β ((πΉβπ)βπ€))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) = ((absβ(((πΉβπ)βπ€) β (πΊβπ€))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))))) |
95 | 92, 94 | breqtrd 5136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ((πΊβπ€) β ((πΉβπ)βπ₯))) β€ ((absβ(((πΉβπ)βπ€) β (πΊβπ€))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))))) |
96 | 83, 91, 53, 95 | leadd2dd 11777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ((πΊβπ€) β ((πΉβπ)βπ₯)))) β€ ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + ((absβ(((πΉβπ)βπ€) β (πΊβπ€))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))))) |
97 | 59 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ(((πΉβπ)βπ€) β (πΊβπ€))) β β) |
98 | 71 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) β β) |
99 | 88, 97, 98 | addassd 11184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) = ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + ((absβ(((πΉβπ)βπ€) β (πΊβπ€))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))))) |
100 | 96, 99 | breqtrrd 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ((πΊβπ€) β ((πΉβπ)βπ₯)))) β€ (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))))) |
101 | 81, 84, 85, 90, 100 | letrd 11319 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (absβ((πΊβπ€) β (πΊβπ₯))) β€ (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))))) |
102 | | lelttr 11252 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((absβ((πΊβπ€) β (πΊβπ₯))) β β β§
(((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) β β β§ π¦ β β) β (((absβ((πΊβπ€) β (πΊβπ₯))) β€ (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) β§ (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) < π¦) β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)) |
103 | 81, 85, 76, 102 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((absβ((πΊβπ€) β (πΊβπ₯))) β€ (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) β§ (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) < π¦) β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)) |
104 | 101, 103 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) < π¦ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)) |
105 | 79, 104 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) + (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯)))) < ((π¦ / 2) + (π¦ / 2)) β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)) |
106 | 73, 105 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β ((((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) < (π¦ / 2) β§ (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2)) β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)) |
107 | 106 | expd 417 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) < (π¦ / 2) β ((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2) β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
108 | 68, 107 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) + (absβ(((πΉβπ)βπ€) β (πΊβπ€)))) < (((π¦ / 2) / 2) + ((π¦ / 2) / 2)) β ((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2) β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
109 | 64, 108 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β (((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2) β§ (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) β ((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2) β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
110 | 109 | expdimp 454 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ π€ β π) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β ((absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β ((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2) β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
111 | 110 | an32s 651 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β§ π€ β π) β ((absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β ((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2) β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
112 | 111 | imp 408 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β§ π€ β π) β§ (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) β ((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2) β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)) |
113 | 112 | imim2d 57 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β§ π€ β π) β§ (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) β (((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2)) β ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
114 | 113 | expimpd 455 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β§ π€ β π) β (((absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β§ ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2))) β ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
115 | 114 | ralimdva 3165 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β (βπ€ β π ((absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β§ ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2))) β βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
116 | 42, 115 | biimtrrid 242 |
. . . . . . . . . . . 12
β’ ((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β ((βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β§ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2))) β βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
117 | 116 | expdimp 454 |
. . . . . . . . . . 11
β’
(((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β§ βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) β (βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2)) β βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
118 | 117 | an32s 651 |
. . . . . . . . . 10
β’
(((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β (βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2)) β βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
119 | 118 | reximdv 3168 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β (βπ§ β β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ₯))) < (π¦ / 2)) β βπ§ β β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
120 | 41, 119 | mpd 15 |
. . . . . . . 8
β’
(((((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β§ βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2)) β§ (absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2)) β βπ§ β β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)) |
121 | 120 | exp31 421 |
. . . . . . 7
β’ (((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β (βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β ((absβ(((πΉβπ)βπ₯) β (πΊβπ₯))) < ((π¦ / 2) / 2) β βπ§ β β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)))) |
122 | 35, 121 | mpdd 43 |
. . . . . 6
β’ (((π β§ (π₯ β π β§ π¦ β β+)) β§ π β π) β (βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β βπ§ β β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
123 | 122 | rexlimdva 3153 |
. . . . 5
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β
(βπ β π βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β βπ§ β β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
124 | 27, 123 | syl5 34 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β
(βπ β π βπ β (β€β₯βπ)βπ€ β π (absβ(((πΉβπ)βπ€) β (πΊβπ€))) < ((π¦ / 2) / 2) β βπ§ β β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦))) |
125 | 26, 124 | mpd 15 |
. . 3
β’ ((π β§ (π₯ β π β§ π¦ β β+)) β
βπ§ β
β+ βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)) |
126 | 125 | ralrimivva 3198 |
. 2
β’ (π β βπ₯ β π βπ¦ β β+ βπ§ β β+
βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)) |
127 | | uzid 12785 |
. . . . . . 7
β’ (π β β€ β π β
(β€β₯βπ)) |
128 | 5, 127 | syl 17 |
. . . . . 6
β’ (π β π β (β€β₯βπ)) |
129 | 128, 4 | eleqtrrdi 2849 |
. . . . 5
β’ (π β π β π) |
130 | 7, 129 | ffvelcdmd 7041 |
. . . 4
β’ (π β (πΉβπ) β (πβcnββ)) |
131 | | cncfrss 24270 |
. . . 4
β’ ((πΉβπ) β (πβcnββ) β π β β) |
132 | 130, 131 | syl 17 |
. . 3
β’ (π β π β β) |
133 | | ssid 3971 |
. . 3
β’ β
β β |
134 | | elcncf2 24269 |
. . 3
β’ ((π β β β§ β
β β) β (πΊ
β (πβcnββ) β (πΊ:πβΆβ β§ βπ₯ β π βπ¦ β β+ βπ§ β β+
βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)))) |
135 | 132, 133,
134 | sylancl 587 |
. 2
β’ (π β (πΊ β (πβcnββ) β (πΊ:πβΆβ β§ βπ₯ β π βπ¦ β β+ βπ§ β β+
βπ€ β π ((absβ(π€ β π₯)) < π§ β (absβ((πΊβπ€) β (πΊβπ₯))) < π¦)))) |
136 | 3, 126, 135 | mpbir2and 712 |
1
β’ (π β πΊ β (πβcnββ)) |