Step | Hyp | Ref
| Expression |
1 | | ftalem3.5 |
. . . 4
β’ π· = {π¦ β β β£ (absβπ¦) β€ π
} |
2 | 1 | ssrab3 4081 |
. . 3
β’ π· β
β |
3 | | ftalem3.6 |
. . . . . . . 8
β’ π½ =
(TopOpenββfld) |
4 | 3 | cnfldtopon 24299 |
. . . . . . 7
β’ π½ β
(TopOnββ) |
5 | | resttopon 22665 |
. . . . . . 7
β’ ((π½ β (TopOnββ)
β§ π· β β)
β (π½
βΎt π·)
β (TopOnβπ·)) |
6 | 4, 2, 5 | mp2an 691 |
. . . . . 6
β’ (π½ βΎt π·) β (TopOnβπ·) |
7 | 6 | toponunii 22418 |
. . . . 5
β’ π· = βͺ
(π½ βΎt
π·) |
8 | | eqid 2733 |
. . . . 5
β’
(topGenβran (,)) = (topGenβran (,)) |
9 | | cnxmet 24289 |
. . . . . . . 8
β’ (abs
β β ) β (βMetββ) |
10 | 9 | a1i 11 |
. . . . . . 7
β’ (π β (abs β β )
β (βMetββ)) |
11 | | 0cn 11206 |
. . . . . . . 8
β’ 0 β
β |
12 | 11 | a1i 11 |
. . . . . . 7
β’ (π β 0 β
β) |
13 | | ftalem3.7 |
. . . . . . . 8
β’ (π β π
β
β+) |
14 | 13 | rpxrd 13017 |
. . . . . . 7
β’ (π β π
β
β*) |
15 | 3 | cnfldtopn 24298 |
. . . . . . . 8
β’ π½ = (MetOpenβ(abs β
β )) |
16 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (abs
β β ) = (abs β β ) |
17 | 16 | cnmetdval 24287 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ π¦
β β) β (0(abs β β )π¦) = (absβ(0 β π¦))) |
18 | 11, 17 | mpan 689 |
. . . . . . . . . . . 12
β’ (π¦ β β β (0(abs
β β )π¦) =
(absβ(0 β π¦))) |
19 | | df-neg 11447 |
. . . . . . . . . . . . . 14
β’ -π¦ = (0 β π¦) |
20 | 19 | fveq2i 6895 |
. . . . . . . . . . . . 13
β’
(absβ-π¦) =
(absβ(0 β π¦)) |
21 | | absneg 15224 |
. . . . . . . . . . . . 13
β’ (π¦ β β β
(absβ-π¦) =
(absβπ¦)) |
22 | 20, 21 | eqtr3id 2787 |
. . . . . . . . . . . 12
β’ (π¦ β β β
(absβ(0 β π¦)) =
(absβπ¦)) |
23 | 18, 22 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π¦ β β β (0(abs
β β )π¦) =
(absβπ¦)) |
24 | 23 | breq1d 5159 |
. . . . . . . . . 10
β’ (π¦ β β β ((0(abs
β β )π¦) β€
π
β (absβπ¦) β€ π
)) |
25 | 24 | rabbiia 3437 |
. . . . . . . . 9
β’ {π¦ β β β£ (0(abs
β β )π¦) β€
π
} = {π¦ β β β£ (absβπ¦) β€ π
} |
26 | 1, 25 | eqtr4i 2764 |
. . . . . . . 8
β’ π· = {π¦ β β β£ (0(abs β
β )π¦) β€ π
} |
27 | 15, 26 | blcld 24014 |
. . . . . . 7
β’ (((abs
β β ) β (βMetββ) β§ 0 β β
β§ π
β
β*) β π· β (Clsdβπ½)) |
28 | 10, 12, 14, 27 | syl3anc 1372 |
. . . . . 6
β’ (π β π· β (Clsdβπ½)) |
29 | 13 | rpred 13016 |
. . . . . . 7
β’ (π β π
β β) |
30 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (absβπ¦) = (absβπ₯)) |
31 | 30 | breq1d 5159 |
. . . . . . . . . 10
β’ (π¦ = π₯ β ((absβπ¦) β€ π
β (absβπ₯) β€ π
)) |
32 | 31, 1 | elrab2 3687 |
. . . . . . . . 9
β’ (π₯ β π· β (π₯ β β β§ (absβπ₯) β€ π
)) |
33 | 32 | simprbi 498 |
. . . . . . . 8
β’ (π₯ β π· β (absβπ₯) β€ π
) |
34 | 33 | rgen 3064 |
. . . . . . 7
β’
βπ₯ β
π· (absβπ₯) β€ π
|
35 | | brralrspcev 5209 |
. . . . . . 7
β’ ((π
β β β§
βπ₯ β π· (absβπ₯) β€ π
) β βπ β β βπ₯ β π· (absβπ₯) β€ π ) |
36 | 29, 34, 35 | sylancl 587 |
. . . . . 6
β’ (π β βπ β β βπ₯ β π· (absβπ₯) β€ π ) |
37 | | eqid 2733 |
. . . . . . . 8
β’ (π½ βΎt π·) = (π½ βΎt π·) |
38 | 3, 37 | cnheibor 24471 |
. . . . . . 7
β’ (π· β β β ((π½ βΎt π·) β Comp β (π· β (Clsdβπ½) β§ βπ β β βπ₯ β π· (absβπ₯) β€ π ))) |
39 | 2, 38 | ax-mp 5 |
. . . . . 6
β’ ((π½ βΎt π·) β Comp β (π· β (Clsdβπ½) β§ βπ β β βπ₯ β π· (absβπ₯) β€ π )) |
40 | 28, 36, 39 | sylanbrc 584 |
. . . . 5
β’ (π β (π½ βΎt π·) β Comp) |
41 | | ftalem.3 |
. . . . . . . . 9
β’ (π β πΉ β (Polyβπ)) |
42 | | plycn 25775 |
. . . . . . . . 9
β’ (πΉ β (Polyβπ) β πΉ β (ββcnββ)) |
43 | 41, 42 | syl 17 |
. . . . . . . 8
β’ (π β πΉ β (ββcnββ)) |
44 | | abscncf 24417 |
. . . . . . . . 9
β’ abs
β (ββcnββ) |
45 | 44 | a1i 11 |
. . . . . . . 8
β’ (π β abs β
(ββcnββ)) |
46 | 43, 45 | cncfco 24423 |
. . . . . . 7
β’ (π β (abs β πΉ) β (ββcnββ)) |
47 | | ssid 4005 |
. . . . . . . 8
β’ β
β β |
48 | | ax-resscn 11167 |
. . . . . . . 8
β’ β
β β |
49 | 4 | toponrestid 22423 |
. . . . . . . . 9
β’ π½ = (π½ βΎt
β) |
50 | 3 | tgioo2 24319 |
. . . . . . . . 9
β’
(topGenβran (,)) = (π½ βΎt
β) |
51 | 3, 49, 50 | cncfcn 24426 |
. . . . . . . 8
β’ ((β
β β β§ β β β) β (ββcnββ) = (π½ Cn (topGenβran
(,)))) |
52 | 47, 48, 51 | mp2an 691 |
. . . . . . 7
β’
(ββcnββ) =
(π½ Cn (topGenβran
(,))) |
53 | 46, 52 | eleqtrdi 2844 |
. . . . . 6
β’ (π β (abs β πΉ) β (π½ Cn (topGenβran
(,)))) |
54 | 4 | toponunii 22418 |
. . . . . . 7
β’ β =
βͺ π½ |
55 | 54 | cnrest 22789 |
. . . . . 6
β’ (((abs
β πΉ) β (π½ Cn (topGenβran (,)))
β§ π· β β)
β ((abs β πΉ)
βΎ π·) β ((π½ βΎt π·) Cn (topGenβran
(,)))) |
56 | 53, 2, 55 | sylancl 587 |
. . . . 5
β’ (π β ((abs β πΉ) βΎ π·) β ((π½ βΎt π·) Cn (topGenβran
(,)))) |
57 | 13 | rpge0d 13020 |
. . . . . . 7
β’ (π β 0 β€ π
) |
58 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π¦ = 0 β (absβπ¦) =
(absβ0)) |
59 | | abs0 15232 |
. . . . . . . . . 10
β’
(absβ0) = 0 |
60 | 58, 59 | eqtrdi 2789 |
. . . . . . . . 9
β’ (π¦ = 0 β (absβπ¦) = 0) |
61 | 60 | breq1d 5159 |
. . . . . . . 8
β’ (π¦ = 0 β ((absβπ¦) β€ π
β 0 β€ π
)) |
62 | 61, 1 | elrab2 3687 |
. . . . . . 7
β’ (0 β
π· β (0 β β
β§ 0 β€ π
)) |
63 | 12, 57, 62 | sylanbrc 584 |
. . . . . 6
β’ (π β 0 β π·) |
64 | 63 | ne0d 4336 |
. . . . 5
β’ (π β π· β β
) |
65 | 7, 8, 40, 56, 64 | evth2 24476 |
. . . 4
β’ (π β βπ§ β π· βπ₯ β π· (((abs β πΉ) βΎ π·)βπ§) β€ (((abs β πΉ) βΎ π·)βπ₯)) |
66 | | fvres 6911 |
. . . . . . . . 9
β’ (π§ β π· β (((abs β πΉ) βΎ π·)βπ§) = ((abs β πΉ)βπ§)) |
67 | 66 | ad2antlr 726 |
. . . . . . . 8
β’ (((π β§ π§ β π·) β§ π₯ β π·) β (((abs β πΉ) βΎ π·)βπ§) = ((abs β πΉ)βπ§)) |
68 | | plyf 25712 |
. . . . . . . . . . 11
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
69 | 41, 68 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆβ) |
70 | 69 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π§ β π·) β§ π₯ β π·) β πΉ:ββΆβ) |
71 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π§ β π·) β§ π₯ β π·) β π§ β π·) |
72 | 2, 71 | sselid 3981 |
. . . . . . . . 9
β’ (((π β§ π§ β π·) β§ π₯ β π·) β π§ β β) |
73 | | fvco3 6991 |
. . . . . . . . 9
β’ ((πΉ:ββΆβ β§
π§ β β) β
((abs β πΉ)βπ§) = (absβ(πΉβπ§))) |
74 | 70, 72, 73 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π§ β π·) β§ π₯ β π·) β ((abs β πΉ)βπ§) = (absβ(πΉβπ§))) |
75 | 67, 74 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π§ β π·) β§ π₯ β π·) β (((abs β πΉ) βΎ π·)βπ§) = (absβ(πΉβπ§))) |
76 | | fvres 6911 |
. . . . . . . . 9
β’ (π₯ β π· β (((abs β πΉ) βΎ π·)βπ₯) = ((abs β πΉ)βπ₯)) |
77 | 76 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π§ β π·) β§ π₯ β π·) β (((abs β πΉ) βΎ π·)βπ₯) = ((abs β πΉ)βπ₯)) |
78 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π§ β π·) β§ π₯ β π·) β π₯ β π·) |
79 | 2, 78 | sselid 3981 |
. . . . . . . . 9
β’ (((π β§ π§ β π·) β§ π₯ β π·) β π₯ β β) |
80 | | fvco3 6991 |
. . . . . . . . 9
β’ ((πΉ:ββΆβ β§
π₯ β β) β
((abs β πΉ)βπ₯) = (absβ(πΉβπ₯))) |
81 | 70, 79, 80 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π§ β π·) β§ π₯ β π·) β ((abs β πΉ)βπ₯) = (absβ(πΉβπ₯))) |
82 | 77, 81 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π§ β π·) β§ π₯ β π·) β (((abs β πΉ) βΎ π·)βπ₯) = (absβ(πΉβπ₯))) |
83 | 75, 82 | breq12d 5162 |
. . . . . 6
β’ (((π β§ π§ β π·) β§ π₯ β π·) β ((((abs β πΉ) βΎ π·)βπ§) β€ (((abs β πΉ) βΎ π·)βπ₯) β (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
84 | 83 | ralbidva 3176 |
. . . . 5
β’ ((π β§ π§ β π·) β (βπ₯ β π· (((abs β πΉ) βΎ π·)βπ§) β€ (((abs β πΉ) βΎ π·)βπ₯) β βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
85 | 84 | rexbidva 3177 |
. . . 4
β’ (π β (βπ§ β π· βπ₯ β π· (((abs β πΉ) βΎ π·)βπ§) β€ (((abs β πΉ) βΎ π·)βπ₯) β βπ§ β π· βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
86 | 65, 85 | mpbid 231 |
. . 3
β’ (π β βπ§ β π· βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯))) |
87 | | ssrexv 4052 |
. . 3
β’ (π· β β β
(βπ§ β π· βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β βπ§ β β βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
88 | 2, 86, 87 | mpsyl 68 |
. 2
β’ (π β βπ§ β β βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯))) |
89 | 63 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β β) β 0 β π·) |
90 | | 2fveq3 6897 |
. . . . . . . . 9
β’ (π₯ = 0 β (absβ(πΉβπ₯)) = (absβ(πΉβ0))) |
91 | 90 | breq2d 5161 |
. . . . . . . 8
β’ (π₯ = 0 β ((absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β (absβ(πΉβπ§)) β€ (absβ(πΉβ0)))) |
92 | 91 | rspcv 3609 |
. . . . . . 7
β’ (0 β
π· β (βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β (absβ(πΉβπ§)) β€ (absβ(πΉβ0)))) |
93 | 89, 92 | syl 17 |
. . . . . 6
β’ ((π β§ π§ β β) β (βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β (absβ(πΉβπ§)) β€ (absβ(πΉβ0)))) |
94 | 69 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β πΉ:ββΆβ) |
95 | | ffvelcdm 7084 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆβ β§ 0
β β) β (πΉβ0) β β) |
96 | 94, 11, 95 | sylancl 587 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (πΉβ0) β β) |
97 | 96 | abscld 15383 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (absβ(πΉβ0)) β β) |
98 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β π₯ β (β β π·)) |
99 | 98 | eldifad 3961 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β π₯ β β) |
100 | 94, 99 | ffvelcdmd 7088 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (πΉβπ₯) β β) |
101 | 100 | abscld 15383 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (absβ(πΉβπ₯)) β β) |
102 | | ftalem3.8 |
. . . . . . . . . . 11
β’ (π β βπ₯ β β (π
< (absβπ₯) β (absβ(πΉβ0)) < (absβ(πΉβπ₯)))) |
103 | 102 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β βπ₯ β β (π
< (absβπ₯) β (absβ(πΉβ0)) < (absβ(πΉβπ₯)))) |
104 | 98 | eldifbd 3962 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β Β¬ π₯ β π·) |
105 | 32 | baib 537 |
. . . . . . . . . . . . 13
β’ (π₯ β β β (π₯ β π· β (absβπ₯) β€ π
)) |
106 | 99, 105 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (π₯ β π· β (absβπ₯) β€ π
)) |
107 | 104, 106 | mtbid 324 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β Β¬ (absβπ₯) β€ π
) |
108 | 29 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β π
β β) |
109 | 99 | abscld 15383 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (absβπ₯) β β) |
110 | 108, 109 | ltnled 11361 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (π
< (absβπ₯) β Β¬ (absβπ₯) β€ π
)) |
111 | 107, 110 | mpbird 257 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β π
< (absβπ₯)) |
112 | | rsp 3245 |
. . . . . . . . . 10
β’
(βπ₯ β
β (π
<
(absβπ₯) β
(absβ(πΉβ0))
< (absβ(πΉβπ₯))) β (π₯ β β β (π
< (absβπ₯) β (absβ(πΉβ0)) < (absβ(πΉβπ₯))))) |
113 | 103, 99, 111, 112 | syl3c 66 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (absβ(πΉβ0)) < (absβ(πΉβπ₯))) |
114 | 97, 101, 113 | ltled 11362 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (absβ(πΉβ0)) β€ (absβ(πΉβπ₯))) |
115 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β π§ β β) |
116 | 94, 115 | ffvelcdmd 7088 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (πΉβπ§) β β) |
117 | 116 | abscld 15383 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (absβ(πΉβπ§)) β β) |
118 | | letr 11308 |
. . . . . . . . 9
β’
(((absβ(πΉβπ§)) β β β§ (absβ(πΉβ0)) β β β§
(absβ(πΉβπ₯)) β β) β
(((absβ(πΉβπ§)) β€ (absβ(πΉβ0)) β§
(absβ(πΉβ0))
β€ (absβ(πΉβπ₯))) β (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
119 | 117, 97, 101, 118 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β (((absβ(πΉβπ§)) β€ (absβ(πΉβ0)) β§ (absβ(πΉβ0)) β€
(absβ(πΉβπ₯))) β (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
120 | 114, 119 | mpan2d 693 |
. . . . . . 7
β’ (((π β§ π§ β β) β§ π₯ β (β β π·)) β ((absβ(πΉβπ§)) β€ (absβ(πΉβ0)) β (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
121 | 120 | ralrimdva 3155 |
. . . . . 6
β’ ((π β§ π§ β β) β ((absβ(πΉβπ§)) β€ (absβ(πΉβ0)) β βπ₯ β (β β π·)(absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
122 | 93, 121 | syld 47 |
. . . . 5
β’ ((π β§ π§ β β) β (βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β βπ₯ β (β β π·)(absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
123 | 122 | ancld 552 |
. . . 4
β’ ((π β§ π§ β β) β (βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β (βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β§ βπ₯ β (β β π·)(absβ(πΉβπ§)) β€ (absβ(πΉβπ₯))))) |
124 | | ralunb 4192 |
. . . . 5
β’
(βπ₯ β
(π· βͺ (β β
π·))(absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β (βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β§ βπ₯ β (β β π·)(absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
125 | | undif2 4477 |
. . . . . . 7
β’ (π· βͺ (β β π·)) = (π· βͺ β) |
126 | | ssequn1 4181 |
. . . . . . . 8
β’ (π· β β β (π· βͺ β) =
β) |
127 | 2, 126 | mpbi 229 |
. . . . . . 7
β’ (π· βͺ β) =
β |
128 | 125, 127 | eqtri 2761 |
. . . . . 6
β’ (π· βͺ (β β π·)) = β |
129 | 128 | raleqi 3324 |
. . . . 5
β’
(βπ₯ β
(π· βͺ (β β
π·))(absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β βπ₯ β β (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯))) |
130 | 124, 129 | bitr3i 277 |
. . . 4
β’
((βπ₯ β
π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β§ βπ₯ β (β β π·)(absβ(πΉβπ§)) β€ (absβ(πΉβπ₯))) β βπ₯ β β (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯))) |
131 | 123, 130 | imbitrdi 250 |
. . 3
β’ ((π β§ π§ β β) β (βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β βπ₯ β β (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
132 | 131 | reximdva 3169 |
. 2
β’ (π β (βπ§ β β βπ₯ β π· (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)) β βπ§ β β βπ₯ β β (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯)))) |
133 | 88, 132 | mpd 15 |
1
β’ (π β βπ§ β β βπ₯ β β (absβ(πΉβπ§)) β€ (absβ(πΉβπ₯))) |