Step | Hyp | Ref
| Expression |
1 | | eldmg 5859 |
. . . 4
β’ (πΉ β dom
(βπ’βπ) β (πΉ β dom
(βπ’βπ) β βπ πΉ(βπ’βπ)π)) |
2 | 1 | ibi 267 |
. . 3
β’ (πΉ β dom
(βπ’βπ) β βπ πΉ(βπ’βπ)π) |
3 | | ulmcau.z |
. . . . . . . 8
β’ π =
(β€β₯βπ) |
4 | | ulmcau.m |
. . . . . . . . 9
β’ (π β π β β€) |
5 | 4 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β π β
β€) |
6 | | ulmcau.f |
. . . . . . . . 9
β’ (π β πΉ:πβΆ(β βm π)) |
7 | 6 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β πΉ:πβΆ(β βm π)) |
8 | | eqidd 2738 |
. . . . . . . 8
β’ ((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ (π β π β§ π§ β π)) β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
9 | | eqidd 2738 |
. . . . . . . 8
β’ ((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π§ β π) β (πβπ§) = (πβπ§)) |
10 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β πΉ(βπ’βπ)π) |
11 | | rphalfcl 12949 |
. . . . . . . . 9
β’ (π₯ β β+
β (π₯ / 2) β
β+) |
12 | 11 | adantl 483 |
. . . . . . . 8
β’ (((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β (π₯ / 2) β
β+) |
13 | 3, 5, 7, 8, 9, 10,
12 | ulmi 25761 |
. . . . . . 7
β’ (((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2)) |
14 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β π β π) |
15 | 14, 3 | eleqtrdi 2848 |
. . . . . . . . . 10
β’ ((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β π β (β€β₯βπ)) |
16 | | eluzelz 12780 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β π β β€) |
17 | | uzid 12785 |
. . . . . . . . . 10
β’ (π β β€ β π β
(β€β₯βπ)) |
18 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΉβπ) = (πΉβπ)) |
19 | 18 | fveq1d 6849 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
20 | 19 | fvoveq1d 7384 |
. . . . . . . . . . . . 13
β’ (π = π β (absβ(((πΉβπ)βπ§) β (πβπ§))) = (absβ(((πΉβπ)βπ§) β (πβπ§)))) |
21 | 20 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (π = π β ((absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2))) |
22 | 21 | ralbidv 3175 |
. . . . . . . . . . 11
β’ (π = π β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2))) |
23 | 22 | rspcv 3580 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2))) |
24 | 15, 16, 17, 23 | 4syl 19 |
. . . . . . . . 9
β’ ((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2))) |
25 | | r19.26 3115 |
. . . . . . . . . . . . . . 15
β’
(βπ§ β
π ((absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β§ (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2))) |
26 | 7 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β (πΉβπ) β (β βm π)) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β (β βm π)) |
28 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ):πβΆβ) |
30 | 29 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β ((πΉβπ)βπ§) β β) |
31 | | ulmcl 25756 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΉ(βπ’βπ)π β π:πβΆβ) |
32 | 31 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β π:πβΆβ) |
33 | 32 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β (πβπ§) β β) |
34 | 30, 33 | abssubd 15345 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β (absβ(((πΉβπ)βπ§) β (πβπ§))) = (absβ((πβπ§) β ((πΉβπ)βπ§)))) |
35 | 34 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β ((absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β (absβ((πβπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
36 | 35 | biimpd 228 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β ((absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β (absβ((πβπ§) β ((πΉβπ)βπ§))) < (π₯ / 2))) |
37 | 3 | uztrn2 12789 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
38 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΉ:πβΆ(β βm π) β§ π β π) β (πΉβπ) β (β βm π)) |
39 | 7, 37, 38 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ (π β π β§ π β (β€β₯βπ))) β (πΉβπ) β (β βm π)) |
40 | 39 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β (β βm π)) |
41 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ):πβΆβ) |
43 | 42 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β ((πΉβπ)βπ§) β β) |
44 | | rpre 12930 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β β+
β π₯ β
β) |
45 | 44 | ad4antlr 732 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β π₯ β β) |
46 | | abs3lem 15230 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((πΉβπ)βπ§) β β β§ ((πΉβπ)βπ§) β β) β§ ((πβπ§) β β β§ π₯ β β)) β
(((absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β§ (absβ((πβπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
47 | 43, 30, 33, 45, 46 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β (((absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β§ (absβ((πβπ§) β ((πΉβπ)βπ§))) < (π₯ / 2)) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
48 | 36, 47 | sylan2d 606 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β (((absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β§ (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2)) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
49 | 48 | ancomsd 467 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ π§ β π) β (((absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β§ (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2)) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
50 | 49 | ralimdva 3165 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β (βπ§ β π ((absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β§ (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2)) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
51 | 25, 50 | biimtrrid 242 |
. . . . . . . . . . . . . 14
β’
(((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β ((βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2)) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
52 | 51 | expdimp 454 |
. . . . . . . . . . . . 13
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ π β (β€β₯βπ)) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
53 | 52 | an32s 651 |
. . . . . . . . . . . 12
β’
((((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2)) β§ π β (β€β₯βπ)) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
54 | 53 | ralimdva 3165 |
. . . . . . . . . . 11
β’
(((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β§ βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2)) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
55 | 54 | ex 414 |
. . . . . . . . . 10
β’ ((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯))) |
56 | 55 | com23 86 |
. . . . . . . . 9
β’ ((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β (βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯))) |
57 | 24, 56 | mpdd 43 |
. . . . . . . 8
β’ ((((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β§ π β π) β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
58 | 57 | reximdva 3166 |
. . . . . . 7
β’ (((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β
(βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β (πβπ§))) < (π₯ / 2) β βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
59 | 13, 58 | mpd 15 |
. . . . . 6
β’ (((π β§ πΉ(βπ’βπ)π) β§ π₯ β β+) β
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) |
60 | 59 | ralrimiva 3144 |
. . . . 5
β’ ((π β§ πΉ(βπ’βπ)π) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) |
61 | 60 | ex 414 |
. . . 4
β’ (π β (πΉ(βπ’βπ)π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
62 | 61 | exlimdv 1937 |
. . 3
β’ (π β (βπ πΉ(βπ’βπ)π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
63 | 2, 62 | syl5 34 |
. 2
β’ (π β (πΉ β dom
(βπ’βπ) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
64 | | ulmrel 25753 |
. . . 4
β’ Rel
(βπ’βπ) |
65 | | ulmcau.s |
. . . . . . . . . 10
β’ (π β π β π) |
66 | 3, 4, 65, 6 | ulmcaulem 25769 |
. . . . . . . . 9
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |
67 | 66 | biimpa 478 |
. . . . . . . 8
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) |
68 | | rphalfcl 12949 |
. . . . . . . 8
β’ (π β β+
β (π / 2) β
β+) |
69 | | breq2 5114 |
. . . . . . . . . . . . 13
β’ (π₯ = (π / 2) β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
70 | 69 | ralbidv 3175 |
. . . . . . . . . . . 12
β’ (π₯ = (π / 2) β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
71 | 70 | 2ralbidv 3213 |
. . . . . . . . . . 11
β’ (π₯ = (π / 2) β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
72 | 71 | rexbidv 3176 |
. . . . . . . . . 10
β’ (π₯ = (π / 2) β (βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
73 | | ralcom 3275 |
. . . . . . . . . . . . . 14
β’
(βπ€ β
π βπ β
(β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ β (β€β₯βπ)βπ€ β π (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2)) |
74 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
75 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = π§ β ((πΉβπ)βπ€) = ((πΉβπ)βπ§)) |
76 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = π§ β ((πΉβπ)βπ€) = ((πΉβπ)βπ§)) |
77 | 75, 76 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ = π§ β (((πΉβπ)βπ€) β ((πΉβπ)βπ€)) = (((πΉβπ)βπ§) β ((πΉβπ)βπ§))) |
78 | 77 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = π§ β (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) = (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§)))) |
79 | 78 | breq1d 5120 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = π§ β ((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
80 | 79 | cbvralvw 3228 |
. . . . . . . . . . . . . . . 16
β’
(βπ€ β
π (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2)) |
81 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (πΉβπ) = (πΉβπ)) |
82 | 81 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
83 | 82 | fvoveq1d 7384 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) = (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§)))) |
84 | 83 | breq1d 5120 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2) β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
85 | 84 | ralbidv 3175 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
86 | 80, 85 | bitrid 283 |
. . . . . . . . . . . . . . 15
β’ (π = π β (βπ€ β π (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
87 | 74, 86 | raleqbidv 3322 |
. . . . . . . . . . . . . 14
β’ (π = π β (βπ β (β€β₯βπ)βπ€ β π (absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
88 | 73, 87 | bitrid 283 |
. . . . . . . . . . . . 13
β’ (π = π β (βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
89 | 88 | cbvralvw 3228 |
. . . . . . . . . . . 12
β’
(βπ β
(β€β₯βπ)βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2)) |
90 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
91 | 90 | raleqdv 3316 |
. . . . . . . . . . . 12
β’ (π = π β (βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
92 | 89, 91 | bitrid 283 |
. . . . . . . . . . 11
β’ (π = π β (βπ β (β€β₯βπ)βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2))) |
93 | 92 | cbvrexvw 3229 |
. . . . . . . . . 10
β’
(βπ β
π βπ β
(β€β₯βπ)βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < (π / 2)) |
94 | 72, 93 | bitr4di 289 |
. . . . . . . . 9
β’ (π₯ = (π / 2) β (βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β π βπ β (β€β₯βπ)βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2))) |
95 | 94 | rspccva 3583 |
. . . . . . . 8
β’
((βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β§ (π / 2) β β+) β
βπ β π βπ β (β€β₯βπ)βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2)) |
96 | 67, 68, 95 | syl2an 597 |
. . . . . . 7
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β
βπ β π βπ β (β€β₯βπ)βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2)) |
97 | 3 | uztrn2 12789 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
98 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(β€β₯βπ) = (β€β₯βπ) |
99 | | eluzelz 12780 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯βπ) β π β β€) |
100 | 99, 3 | eleq2s 2856 |
. . . . . . . . . . . . . . 15
β’ (π β π β π β β€) |
101 | 100 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β π β β€) |
102 | 68 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β (π / 2) β
β+) |
103 | 102 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β (π / 2) β
β+) |
104 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β π β π) |
105 | 3 | uztrn2 12789 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
106 | 104, 105 | sylan 581 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β π β π) |
107 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΉβπ) = (πΉβπ)) |
108 | 107 | fveq1d 6849 |
. . . . . . . . . . . . . . . 16
β’ (π = π β ((πΉβπ)βπ€) = ((πΉβπ)βπ€)) |
109 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ (π β π β¦ ((πΉβπ)βπ€)) = (π β π β¦ ((πΉβπ)βπ€)) |
110 | | fvex 6860 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ)βπ€) β V |
111 | 108, 109,
110 | fvmpt 6953 |
. . . . . . . . . . . . . . 15
β’ (π β π β ((π β π β¦ ((πΉβπ)βπ€))βπ) = ((πΉβπ)βπ€)) |
112 | 106, 111 | syl 17 |
. . . . . . . . . . . . . 14
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β ((π β π β¦ ((πΉβπ)βπ€))βπ) = ((πΉβπ)βπ€)) |
113 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β πΉ:πβΆ(β βm π)) |
114 | 113 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β π) β (πΉβπ) β (β βm π)) |
115 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β π) β (πΉβπ):πβΆβ) |
117 | 116 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β π) β§ π¦ β π) β ((πΉβπ)βπ¦) β β) |
118 | 117 | an32s 651 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π¦ β π) β§ π β π) β ((πΉβπ)βπ¦) β β) |
119 | 118 | fmpttd 7068 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π¦ β π) β (π β π β¦ ((πΉβπ)βπ¦)):πβΆβ) |
120 | 119 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π¦ β π) β§ π β π) β ((π β π β¦ ((πΉβπ)βπ¦))βπ) β β) |
121 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π§ = π¦ β ((πΉβπ)βπ§) = ((πΉβπ)βπ¦)) |
122 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π§ = π¦ β ((πΉβπ)βπ§) = ((πΉβπ)βπ¦)) |
123 | 121, 122 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π§ = π¦ β (((πΉβπ)βπ§) β ((πΉβπ)βπ§)) = (((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) |
124 | 123 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ = π¦ β (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) = (absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦)))) |
125 | 124 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ = π¦ β ((absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β (absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯)) |
126 | 125 | rspcv 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ β π β (βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β (absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯)) |
127 | 126 | ralimdv 3167 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ β π β (βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯)) |
128 | 127 | reximdv 3168 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ β π β (βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯)) |
129 | 128 | ralimdv 3167 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β π β (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯)) |
130 | 129 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β§ π¦ β π) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯) |
131 | 130 | adantll 713 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π¦ β π) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯) |
132 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π β ((π β π β¦ ((πΉβπ)βπ¦))βπ) = ((π β π β¦ ((πΉβπ)βπ¦))βπ)) |
133 | 132 | fvoveq1d 7384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β (absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) = (absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ)))) |
134 | 133 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π β ((absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β (absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π)) |
135 | 134 | cbvralvw 3228 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
(β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β βπ β (β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π) |
136 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β ((π β π β¦ ((πΉβπ)βπ¦))βπ) = ((π β π β¦ ((πΉβπ)βπ¦))βπ)) |
137 | 136 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = π β (((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ)) = (((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) |
138 | 137 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β (absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) = (absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ)))) |
139 | 138 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π β ((absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β (absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π)) |
140 | 90, 139 | raleqbidv 3322 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = π β (βπ β (β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β βπ β (β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π)) |
141 | 135, 140 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π β (βπ β (β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β βπ β (β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π)) |
142 | 141 | cbvrexvw 3229 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ β
π βπ β
(β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β βπ β π βπ β (β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π) |
143 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π β (πΉβπ) = (πΉβπ)) |
144 | 143 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β ((πΉβπ)βπ¦) = ((πΉβπ)βπ¦)) |
145 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β π β¦ ((πΉβπ)βπ¦)) = (π β π β¦ ((πΉβπ)βπ¦)) |
146 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πΉβπ)βπ¦) β V |
147 | 144, 145,
146 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β ((π β π β¦ ((πΉβπ)βπ¦))βπ) = ((πΉβπ)βπ¦)) |
148 | 37, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β π β§ π β (β€β₯βπ)) β ((π β π β¦ ((πΉβπ)βπ¦))βπ) = ((πΉβπ)βπ¦)) |
149 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π β (πΉβπ) = (πΉβπ)) |
150 | 149 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β ((πΉβπ)βπ¦) = ((πΉβπ)βπ¦)) |
151 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πΉβπ)βπ¦) β V |
152 | 150, 145,
151 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β ((π β π β¦ ((πΉβπ)βπ¦))βπ) = ((πΉβπ)βπ¦)) |
153 | 152 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β π β§ π β (β€β₯βπ)) β ((π β π β¦ ((πΉβπ)βπ¦))βπ) = ((πΉβπ)βπ¦)) |
154 | 148, 153 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β π β§ π β (β€β₯βπ)) β (((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ)) = (((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) |
155 | 154 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β π β§ π β (β€β₯βπ)) β (absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) = (absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦)))) |
156 | 155 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β π β§ π β (β€β₯βπ)) β ((absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β (absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π)) |
157 | 156 | ralbidva 3173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β (βπ β (β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π)) |
158 | 157 | rexbiia 3096 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ β
π βπ β
(β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π) |
159 | 142, 158 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ β
π βπ β
(β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π) |
160 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π₯ β ((absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π β (absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯)) |
161 | 160 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π₯ β (βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π β βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯)) |
162 | 161 | rexbidv 3176 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π₯ β (βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π β βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯)) |
163 | 159, 162 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π₯ β (βπ β π βπ β (β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯)) |
164 | 163 | cbvralvw 3228 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
β+ βπ β π βπ β (β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ¦) β ((πΉβπ)βπ¦))) < π₯) |
165 | 131, 164 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π¦ β π) β βπ β β+ βπ β π βπ β (β€β₯βπ)(absβ(((π β π β¦ ((πΉβπ)βπ¦))βπ) β ((π β π β¦ ((πΉβπ)βπ¦))βπ))) < π) |
166 | 3 | fvexi 6861 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π β V |
167 | 166 | mptex 7178 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β¦ ((πΉβπ)βπ¦)) β V |
168 | 167 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π¦ β π) β (π β π β¦ ((πΉβπ)βπ¦)) β V) |
169 | 3, 120, 165, 168 | caucvg 15570 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π¦ β π) β (π β π β¦ ((πΉβπ)βπ¦)) β dom β ) |
170 | 169 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β βπ¦ β π (π β π β¦ ((πΉβπ)βπ¦)) β dom β ) |
171 | 170 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β βπ¦ β π (π β π β¦ ((πΉβπ)βπ¦)) β dom β ) |
172 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π€ β ((πΉβπ)βπ¦) = ((πΉβπ)βπ€)) |
173 | 172 | mpteq2dv 5212 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π€ β (π β π β¦ ((πΉβπ)βπ¦)) = (π β π β¦ ((πΉβπ)βπ€))) |
174 | 173 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π€ β ((π β π β¦ ((πΉβπ)βπ¦)) β dom β β (π β π β¦ ((πΉβπ)βπ€)) β dom β )) |
175 | 174 | rspccva 3583 |
. . . . . . . . . . . . . . . 16
β’
((βπ¦ β
π (π β π β¦ ((πΉβπ)βπ¦)) β dom β β§ π€ β π) β (π β π β¦ ((πΉβπ)βπ€)) β dom β ) |
176 | 171, 175 | sylan 581 |
. . . . . . . . . . . . . . 15
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β (π β π β¦ ((πΉβπ)βπ€)) β dom β ) |
177 | | climdm 15443 |
. . . . . . . . . . . . . . 15
β’ ((π β π β¦ ((πΉβπ)βπ€)) β dom β β (π β π β¦ ((πΉβπ)βπ€)) β ( β β(π β π β¦ ((πΉβπ)βπ€)))) |
178 | 176, 177 | sylib 217 |
. . . . . . . . . . . . . 14
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β (π β π β¦ ((πΉβπ)βπ€)) β ( β β(π β π β¦ ((πΉβπ)βπ€)))) |
179 | 98, 101, 103, 112, 178 | climi2 15400 |
. . . . . . . . . . . . 13
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β βπ£ β (β€β₯βπ)βπ β (β€β₯βπ£)(absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2)) |
180 | 98 | r19.29uz 15242 |
. . . . . . . . . . . . . . 15
β’
((βπ β
(β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β§ βπ£ β (β€β₯βπ)βπ β (β€β₯βπ£)(absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2)) β βπ£ β (β€β₯βπ)βπ β (β€β₯βπ£)((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β§ (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2))) |
181 | 98 | r19.2uz 15243 |
. . . . . . . . . . . . . . 15
β’
(βπ£ β
(β€β₯βπ)βπ β (β€β₯βπ£)((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β§ (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2)) β βπ β (β€β₯βπ)((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β§ (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2))) |
182 | 180, 181 | syl 17 |
. . . . . . . . . . . . . 14
β’
((βπ β
(β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β§ βπ£ β (β€β₯βπ)βπ β (β€β₯βπ£)(absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2)) β βπ β (β€β₯βπ)((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β§ (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2))) |
183 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β πΉ:πβΆ(β βm π)) |
184 | 183 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β (πΉβπ) β (β βm π)) |
185 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β (πΉβπ):πβΆβ) |
187 | 186 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β ((πΉβπ)βπ€) β β) |
188 | 187 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ€) β β) |
189 | | climcl 15388 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β π β¦ ((πΉβπ)βπ€)) β ( β β(π β π β¦ ((πΉβπ)βπ€))) β ( β β(π β π β¦ ((πΉβπ)βπ€))) β β) |
190 | 178, 189 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β ( β β(π β π β¦ ((πΉβπ)βπ€))) β β) |
191 | 190 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β ( β
β(π β π β¦ ((πΉβπ)βπ€))) β β) |
192 | 6 | ad5antr 733 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β πΉ:πβΆ(β βm π)) |
193 | 192, 106 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β (πΉβπ) β (β βm π)) |
194 | | elmapi 8794 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
195 | 193, 194 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β (πΉβπ):πβΆβ) |
196 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β π€ β π) |
197 | 195, 196 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β ((πΉβπ)βπ€) β β) |
198 | | rpre 12930 |
. . . . . . . . . . . . . . . . 17
β’ (π β β+
β π β
β) |
199 | 198 | ad4antlr 732 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β π β β) |
200 | | abs3lem 15230 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉβπ)βπ€) β β β§ ( β
β(π β π β¦ ((πΉβπ)βπ€))) β β) β§ (((πΉβπ)βπ€) β β β§ π β β)) β
(((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β§ (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2)) β (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
201 | 188, 191,
197, 199, 200 | syl22anc 838 |
. . . . . . . . . . . . . . 15
β’
((((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β§ π β (β€β₯βπ)) β (((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β§ (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2)) β (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
202 | 201 | rexlimdva 3153 |
. . . . . . . . . . . . . 14
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β (βπ β (β€β₯βπ)((absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β§ (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2)) β (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
203 | 182, 202 | syl5 34 |
. . . . . . . . . . . . 13
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β ((βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β§ βπ£ β (β€β₯βπ)βπ β (β€β₯βπ£)(absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < (π / 2)) β (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
204 | 179, 203 | mpan2d 693 |
. . . . . . . . . . . 12
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π€ β π) β (βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
205 | 204 | ralimdva 3165 |
. . . . . . . . . . 11
β’ ((((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β (βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ€ β π (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
206 | 97, 205 | sylan2 594 |
. . . . . . . . . 10
β’ ((((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ (π β π β§ π β (β€β₯βπ))) β (βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ€ β π (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
207 | 206 | anassrs 469 |
. . . . . . . . 9
β’
(((((π β§
βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β§ π β (β€β₯βπ)) β (βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ€ β π (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
208 | 207 | ralimdva 3165 |
. . . . . . . 8
β’ ((((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β§ π β π) β (βπ β (β€β₯βπ)βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ β (β€β₯βπ)βπ€ β π (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
209 | 208 | reximdva 3166 |
. . . . . . 7
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β
(βπ β π βπ β (β€β₯βπ)βπ€ β π βπ β (β€β₯βπ)(absβ(((πΉβπ)βπ€) β ((πΉβπ)βπ€))) < (π / 2) β βπ β π βπ β (β€β₯βπ)βπ€ β π (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
210 | 96, 209 | mpd 15 |
. . . . . 6
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π β β+) β
βπ β π βπ β (β€β₯βπ)βπ€ β π (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π) |
211 | 210 | ralrimiva 3144 |
. . . . 5
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β βπ β β+ βπ β π βπ β (β€β₯βπ)βπ€ β π (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π) |
212 | 4 | adantr 482 |
. . . . . 6
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β π β β€) |
213 | | eqidd 2738 |
. . . . . 6
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ (π β π β§ π€ β π)) β ((πΉβπ)βπ€) = ((πΉβπ)βπ€)) |
214 | 173 | fveq2d 6851 |
. . . . . . . 8
β’ (π¦ = π€ β ( β β(π β π β¦ ((πΉβπ)βπ¦))) = ( β β(π β π β¦ ((πΉβπ)βπ€)))) |
215 | | eqid 2737 |
. . . . . . . 8
β’ (π¦ β π β¦ ( β β(π β π β¦ ((πΉβπ)βπ¦)))) = (π¦ β π β¦ ( β β(π β π β¦ ((πΉβπ)βπ¦)))) |
216 | | fvex 6860 |
. . . . . . . 8
β’ ( β
β(π β π β¦ ((πΉβπ)βπ€))) β V |
217 | 214, 215,
216 | fvmpt 6953 |
. . . . . . 7
β’ (π€ β π β ((π¦ β π β¦ ( β β(π β π β¦ ((πΉβπ)βπ¦))))βπ€) = ( β β(π β π β¦ ((πΉβπ)βπ€)))) |
218 | 217 | adantl 483 |
. . . . . 6
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π€ β π) β ((π¦ β π β¦ ( β β(π β π β¦ ((πΉβπ)βπ¦))))βπ€) = ( β β(π β π β¦ ((πΉβπ)βπ€)))) |
219 | | climdm 15443 |
. . . . . . . . 9
β’ ((π β π β¦ ((πΉβπ)βπ¦)) β dom β β (π β π β¦ ((πΉβπ)βπ¦)) β ( β β(π β π β¦ ((πΉβπ)βπ¦)))) |
220 | 169, 219 | sylib 217 |
. . . . . . . 8
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π¦ β π) β (π β π β¦ ((πΉβπ)βπ¦)) β ( β β(π β π β¦ ((πΉβπ)βπ¦)))) |
221 | | climcl 15388 |
. . . . . . . 8
β’ ((π β π β¦ ((πΉβπ)βπ¦)) β ( β β(π β π β¦ ((πΉβπ)βπ¦))) β ( β β(π β π β¦ ((πΉβπ)βπ¦))) β β) |
222 | 220, 221 | syl 17 |
. . . . . . 7
β’ (((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β§ π¦ β π) β ( β β(π β π β¦ ((πΉβπ)βπ¦))) β β) |
223 | 222 | fmpttd 7068 |
. . . . . 6
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β (π¦ β π β¦ ( β β(π β π β¦ ((πΉβπ)βπ¦)))):πβΆβ) |
224 | 65 | adantr 482 |
. . . . . 6
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β π β π) |
225 | 3, 212, 113, 213, 218, 223, 224 | ulm2 25760 |
. . . . 5
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β (πΉ(βπ’βπ)(π¦ β π β¦ ( β β(π β π β¦ ((πΉβπ)βπ¦)))) β βπ β β+ βπ β π βπ β (β€β₯βπ)βπ€ β π (absβ(((πΉβπ)βπ€) β ( β β(π β π β¦ ((πΉβπ)βπ€))))) < π)) |
226 | 211, 225 | mpbird 257 |
. . . 4
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β πΉ(βπ’βπ)(π¦ β π β¦ ( β β(π β π β¦ ((πΉβπ)βπ¦))))) |
227 | | releldm 5904 |
. . . 4
β’ ((Rel
(βπ’βπ) β§ πΉ(βπ’βπ)(π¦ β π β¦ ( β β(π β π β¦ ((πΉβπ)βπ¦))))) β πΉ β dom
(βπ’βπ)) |
228 | 64, 226, 227 | sylancr 588 |
. . 3
β’ ((π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯) β πΉ β dom
(βπ’βπ)) |
229 | 228 | ex 414 |
. 2
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯ β πΉ β dom
(βπ’βπ))) |
230 | 63, 229 | impbid 211 |
1
β’ (π β (πΉ β dom
(βπ’βπ) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)βπ§ β π (absβ(((πΉβπ)βπ§) β ((πΉβπ)βπ§))) < π₯)) |