Step | Hyp | Ref
| Expression |
1 | | breq2 5114 |
. . . . . 6
β’ (π₯ = π€ β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€)) |
2 | 1 | ralbidv 3175 |
. . . . 5
β’ (π₯ = π€ β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€)) |
3 | 2 | rexralbidv 3215 |
. . . 4
β’ (π₯ = π€ β (βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€)) |
4 | 3 | cbvralvw 3228 |
. . 3
β’
(βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ€ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€) |
5 | | rphalfcl 12949 |
. . . . . . 7
β’ (π₯ β β+
β (π₯ / 2) β
β+) |
6 | | breq2 5114 |
. . . . . . . . . 10
β’ (π€ = (π₯ / 2) β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€ β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
7 | 6 | ralbidv 3175 |
. . . . . . . . 9
β’ (π€ = (π₯ / 2) β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€ β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
8 | 7 | rexralbidv 3215 |
. . . . . . . 8
β’ (π€ = (π₯ / 2) β (βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€ β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
9 | 8 | rspcv 3580 |
. . . . . . 7
β’ ((π₯ / 2) β β+
β (βπ€ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€ β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
10 | 5, 9 | syl 17 |
. . . . . 6
β’ (π₯ β β+
β (βπ€ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€ β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
11 | 10 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(βπ€ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€ β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
12 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβπ) = (πΉβπ)) |
13 | 12 | fveq1d 6849 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
14 | 13 | fvoveq1d 7384 |
. . . . . . . . . . 11
β’ (π = π β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) = (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§)))) |
15 | 14 | breq1d 5120 |
. . . . . . . . . 10
β’ (π = π β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
16 | 15 | ralbidv 3175 |
. . . . . . . . 9
β’ (π = π β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
17 | 16 | cbvralvw 3228 |
. . . . . . . 8
β’
(βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) |
18 | 17 | biimpi 215 |
. . . . . . 7
β’
(βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) |
19 | | uzss 12793 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯βπ) β (β€β₯βπ) β
(β€β₯βπ)) |
20 | 19 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β
(β€β₯βπ) β (β€β₯βπ)) |
21 | | ssralv 4015 |
. . . . . . . . . . . . . 14
β’
((β€β₯βπ) β (β€β₯βπ) β (βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
23 | | r19.26 3115 |
. . . . . . . . . . . . . . . . 17
β’
(βπ§ β
π ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β§ (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
24 | | ulmcau.f |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β πΉ:πβΆ(β βm π)) |
25 | 24 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π₯ β β+) β πΉ:πβΆ(β βm π)) |
26 | 25 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β πΉ:πβΆ(β βm π)) |
27 | | ulmcau.z |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ π =
(β€β₯βπ) |
28 | 27 | uztrn2 12789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
29 | 28 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
30 | 27 | uztrn2 12789 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
31 | 29, 30 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β π β π) |
32 | 26, 31 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (πΉβπ) β (β βm π)) |
33 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (πΉβπ):πβΆβ) |
35 | 34 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β ((πΉβπ)βπ§) β β) |
36 | 25 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β β+) β§ π β π) β (πΉβπ) β (β βm π)) |
37 | 36 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (πΉβπ) β (β βm π)) |
38 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (πΉβπ):πβΆβ) |
40 | 39 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β ((πΉβπ)βπ§) β β) |
41 | 35, 40 | abssubd 15345 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) = (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§)))) |
42 | 41 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
43 | 42 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
44 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ:πβΆ(β βm π) β§ π β π) β (πΉβπ) β (β βm π)) |
45 | 25, 28, 44 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) β (β βm π)) |
46 | 45 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β (β βm π)) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (πΉβπ) β (β βm π)) |
48 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (πΉβπ):πβΆβ) |
50 | 49 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β ((πΉβπ)βπ§) β β) |
51 | | rpre 12930 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π₯ β β+
β π₯ β
β) |
52 | 51 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β β+) β§ π β π) β π₯ β β) |
53 | 52 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β π₯ β β) |
54 | | abs3lem 15230 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((πΉβπ)βπ§) β β β§ ((πΉβπ)βπ§) β β) β§ (((πΉβπ)βπ§) β β β§ π₯ β β)) β
(((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β§ (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
55 | 50, 35, 40, 53, 54 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β (((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β§ (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
56 | 43, 55 | sylan2d 606 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ π§ β π) β (((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β§ (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
57 | 56 | ralimdva 3165 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β (βπ§ β π ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β§ (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
58 | 23, 57 | biimtrrid 242 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β ((βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
59 | 58 | expdimp 454 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ π β (β€β₯βπ)) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
60 | 59 | an32s 651 |
. . . . . . . . . . . . . 14
β’
((((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β§ π β (β€β₯βπ)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
61 | 60 | ralimdva 3165 |
. . . . . . . . . . . . 13
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
62 | 22, 61 | syld 47 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
63 | 62 | impancom 453 |
. . . . . . . . . . 11
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ π β (β€β₯βπ)) β§ βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
64 | 63 | an32s 651 |
. . . . . . . . . 10
β’
(((((π β§ π₯ β β+)
β§ π β π) β§ βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β§ π β (β€β₯βπ)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
65 | 64 | ralimdva 3165 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β π) β§ βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
66 | 65 | ex 414 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯))) |
67 | 66 | com23 86 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯))) |
68 | 18, 67 | mpdi 45 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
69 | 68 | reximdva 3166 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π₯ / 2) β βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
70 | 11, 69 | syld 47 |
. . . 4
β’ ((π β§ π₯ β β+) β
(βπ€ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€ β βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
71 | 70 | ralrimdva 3152 |
. . 3
β’ (π β (βπ€ β β+
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π€ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
72 | 4, 71 | biimtrid 241 |
. 2
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
73 | | eluzelz 12780 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β π β β€) |
74 | 73, 27 | eleq2s 2856 |
. . . . . . . 8
β’ (π β π β π β β€) |
75 | | uzid 12785 |
. . . . . . . 8
β’ (π β β€ β π β
(β€β₯βπ)) |
76 | 74, 75 | syl 17 |
. . . . . . 7
β’ (π β π β π β (β€β₯βπ)) |
77 | 76 | adantl 483 |
. . . . . 6
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
78 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
79 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πΉβπ) = (πΉβπ)) |
80 | 79 | fveq1d 6849 |
. . . . . . . . . . 11
β’ (π = π β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
81 | 80 | fvoveq1d 7384 |
. . . . . . . . . 10
β’ (π = π β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) = (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§)))) |
82 | 81 | breq1d 5120 |
. . . . . . . . 9
β’ (π = π β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
83 | 82 | ralbidv 3175 |
. . . . . . . 8
β’ (π = π β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
84 | 78, 83 | raleqbidv 3322 |
. . . . . . 7
β’ (π = π β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
85 | 84 | rspcv 3580 |
. . . . . 6
β’ (π β
(β€β₯βπ) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
86 | 77, 85 | syl 17 |
. . . . 5
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
87 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πΉβπ) = (πΉβπ)) |
88 | 87 | fveq1d 6849 |
. . . . . . . . . . 11
β’ (π = π β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
89 | 88 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = π β (((πΉβπ)βπ§) β ((πΉβπ)βπ§)) = (((πΉβπ)βπ§) β ((πΉβπ)βπ§))) |
90 | 89 | fveq2d 6851 |
. . . . . . . . 9
β’ (π = π β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) = (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§)))) |
91 | 90 | breq1d 5120 |
. . . . . . . 8
β’ (π = π β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
92 | 91 | ralbidv 3175 |
. . . . . . 7
β’ (π = π β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
93 | 92 | cbvralvw 3228 |
. . . . . 6
β’
(βπ β
(β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) |
94 | 24 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (πΉβπ) β (β βm π)) |
95 | 94 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β (β βm π)) |
96 | 95, 38 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ):πβΆβ) |
97 | 96 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β ((πΉβπ)βπ§) β β) |
98 | 24, 28, 44 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) β (β βm π)) |
99 | 98 | anassrs 469 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β (β βm π)) |
100 | 99, 48 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ):πβΆβ) |
101 | 100 | ffvelcdmda 7040 |
. . . . . . . . . 10
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β ((πΉβπ)βπ§) β β) |
102 | 97, 101 | abssubd 15345 |
. . . . . . . . 9
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) = (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§)))) |
103 | 102 | breq1d 5120 |
. . . . . . . 8
β’ ((((π β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
104 | 103 | ralbidva 3173 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
105 | 104 | ralbidva 3173 |
. . . . . 6
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
106 | 93, 105 | bitrid 283 |
. . . . 5
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
107 | 86, 106 | sylibd 238 |
. . . 4
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
108 | 107 | reximdva 3166 |
. . 3
β’ (π β (βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
109 | 108 | ralimdv 3167 |
. 2
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
110 | 72, 109 | impbid 211 |
1
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |