Step | Hyp | Ref
| Expression |
1 | | aalioulem2.a |
. . . 4
β’ π = (degβπΉ) |
2 | | aalioulem2.b |
. . . 4
β’ (π β πΉ β
(Polyββ€)) |
3 | | aalioulem2.c |
. . . 4
β’ (π β π β β) |
4 | | aalioulem2.d |
. . . 4
β’ (π β π΄ β β) |
5 | 1, 2, 3, 4 | aalioulem2 25709 |
. . 3
β’ (π β βπ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
6 | | aalioulem3.e |
. . . 4
β’ (π β (πΉβπ΄) = 0) |
7 | 1, 2, 3, 4, 6 | aalioulem5 25712 |
. . 3
β’ (π β βπ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
8 | | reeanv 3220 |
. . 3
β’
(βπ β
β+ βπ β β+ (βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) β (βπ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ βπ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))))) |
9 | 5, 7, 8 | sylanbrc 584 |
. 2
β’ (π β βπ β β+ βπ β β+
(βπ β β€
βπ β β
((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))))) |
10 | | r19.26-2 3136 |
. . . 4
β’
(βπ β
β€ βπ β
β (((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) β (βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))))) |
11 | | ifcl 4536 |
. . . . . 6
β’ ((π β β+
β§ π β
β+) β if(π β€ π, π, π) β
β+) |
12 | 11 | adantl 483 |
. . . . 5
β’ ((π β§ (π β β+ β§ π β β+))
β if(π β€ π, π, π) β
β+) |
13 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (πΉβ(π / π)) = 0) β (πΉβ(π / π)) = 0) |
14 | 11 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β if(π β€ π, π, π) β
β+) |
15 | | nnrp 12933 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β+) |
16 | 15 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β π β
β+) |
17 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β π β
β) |
18 | 17 | nnzd 12533 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β π β
β€) |
19 | 16, 18 | rpexpcld 14157 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (πβπ) β
β+) |
20 | 14, 19 | rpdivcld 12981 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (if(π β€ π, π, π) / (πβπ)) β
β+) |
21 | 20 | rpred 12964 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (if(π β€ π, π, π) / (πβπ)) β β) |
22 | | simplrl 776 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β π β
β+) |
23 | 22, 19 | rpdivcld 12981 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (π / (πβπ)) β
β+) |
24 | 23 | rpred 12964 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (π / (πβπ)) β β) |
25 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β π΄ β
β) |
26 | | znq 12884 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β€ β§ π β β) β (π / π) β β) |
27 | | qre 12885 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π / π) β β β (π / π) β β) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β) β (π / π) β β) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (π / π) β
β) |
30 | 25, 29 | resubcld 11590 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (π΄ β (π / π)) β β) |
31 | 30 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (π΄ β (π / π)) β β) |
32 | 31 | abscld 15328 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (absβ(π΄
β (π / π))) β
β) |
33 | 21, 24, 32 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β ((if(π β€ π, π, π) / (πβπ)) β β β§ (π / (πβπ)) β β β§ (absβ(π΄ β (π / π))) β β)) |
34 | 33 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))) β ((if(π β€ π, π, π) / (πβπ)) β β β§ (π / (πβπ)) β β β§ (absβ(π΄ β (π / π))) β β)) |
35 | 14 | rpred 12964 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β if(π β€ π, π, π) β β) |
36 | 22 | rpred 12964 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β π β
β) |
37 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β π β
β+) |
38 | 37 | rpred 12964 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β π β
β) |
39 | | min1 13115 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β) β if(π β€ π, π, π) β€ π) |
40 | 36, 38, 39 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β if(π β€ π, π, π) β€ π) |
41 | 35, 36, 19, 40 | lediv1dd 13022 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (if(π β€ π, π, π) / (πβπ)) β€ (π / (πβπ))) |
42 | 41 | anim1i 616 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))) β ((if(π β€ π, π, π) / (πβπ)) β€ (π / (πβπ)) β§ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
43 | | letr 11256 |
. . . . . . . . . . . . 13
β’
(((if(π β€ π, π, π) / (πβπ)) β β β§ (π / (πβπ)) β β β§ (absβ(π΄ β (π / π))) β β) β (((if(π β€ π, π, π) / (πβπ)) β€ (π / (πβπ)) β§ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))) β (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
44 | 34, 42, 43 | sylc 65 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))) β (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))) |
45 | 44 | ex 414 |
. . . . . . . . . . 11
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β ((π / (πβπ)) β€ (absβ(π΄ β (π / π))) β (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
46 | 45 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (πΉβ(π / π)) = 0) β ((π / (πβπ)) β€ (absβ(π΄ β (π / π))) β (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
47 | 46 | orim2d 966 |
. . . . . . . . 9
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (πΉβ(π / π)) = 0) β ((π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))) β (π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
48 | 13, 47 | embantd 59 |
. . . . . . . 8
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (πΉβ(π / π)) = 0) β (((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β (π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
49 | 48 | adantrd 493 |
. . . . . . 7
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (πΉβ(π / π)) = 0) β ((((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) β (π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
50 | | simpr 486 |
. . . . . . . . 9
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (πΉβ(π / π)) β 0) β (πΉβ(π / π)) β 0) |
51 | 37, 19 | rpdivcld 12981 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (π / (πβπ)) β
β+) |
52 | 51 | rpred 12964 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (π / (πβπ)) β β) |
53 | 21, 52, 32 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β ((if(π β€ π, π, π) / (πβπ)) β β β§ (π / (πβπ)) β β β§ (absβ(π΄ β (π / π))) β β)) |
54 | 53 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))) β ((if(π β€ π, π, π) / (πβπ)) β β β§ (π / (πβπ)) β β β§ (absβ(π΄ β (π / π))) β β)) |
55 | | min2 13116 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β) β if(π β€ π, π, π) β€ π) |
56 | 36, 38, 55 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β if(π β€ π, π, π) β€ π) |
57 | 35, 38, 19, 56 | lediv1dd 13022 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β (if(π β€ π, π, π) / (πβπ)) β€ (π / (πβπ))) |
58 | 57 | anim1i 616 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))) β ((if(π β€ π, π, π) / (πβπ)) β€ (π / (πβπ)) β§ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
59 | | letr 11256 |
. . . . . . . . . . . . 13
β’
(((if(π β€ π, π, π) / (πβπ)) β β β§ (π / (πβπ)) β β β§ (absβ(π΄ β (π / π))) β β) β (((if(π β€ π, π, π) / (πβπ)) β€ (π / (πβπ)) β§ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))) β (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
60 | 54, 58, 59 | sylc 65 |
. . . . . . . . . . . 12
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))) β (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))) |
61 | 60 | ex 414 |
. . . . . . . . . . 11
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β ((π / (πβπ)) β€ (absβ(π΄ β (π / π))) β (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
62 | 61 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (πΉβ(π / π)) β 0) β ((π / (πβπ)) β€ (absβ(π΄ β (π / π))) β (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
63 | 62 | orim2d 966 |
. . . . . . . . 9
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (πΉβ(π / π)) β 0) β ((π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))) β (π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
64 | 50, 63 | embantd 59 |
. . . . . . . 8
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (πΉβ(π / π)) β 0) β (((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β (π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
65 | 64 | adantld 492 |
. . . . . . 7
β’ ((((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β§ (πΉβ(π / π)) β 0) β ((((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) β (π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
66 | 49, 65 | pm2.61dane 3033 |
. . . . . 6
β’ (((π β§ (π β β+ β§ π β β+))
β§ (π β β€
β§ π β β))
β ((((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) β (π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
67 | 66 | ralimdvva 3202 |
. . . . 5
β’ ((π β§ (π β β+ β§ π β β+))
β (βπ β
β€ βπ β
β (((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) β βπ β β€ βπ β β (π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
68 | | oveq1 7369 |
. . . . . . . . 9
β’ (π₯ = if(π β€ π, π, π) β (π₯ / (πβπ)) = (if(π β€ π, π, π) / (πβπ))) |
69 | 68 | breq1d 5120 |
. . . . . . . 8
β’ (π₯ = if(π β€ π, π, π) β ((π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))) β (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
70 | 69 | orbi2d 915 |
. . . . . . 7
β’ (π₯ = if(π β€ π, π, π) β ((π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))) β (π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
71 | 70 | 2ralbidv 3213 |
. . . . . 6
β’ (π₯ = if(π β€ π, π, π) β (βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))) β βπ β β€ βπ β β (π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
72 | 71 | rspcev 3584 |
. . . . 5
β’
((if(π β€ π, π, π) β β+ β§
βπ β β€
βπ β β
(π΄ = (π / π) β¨ (if(π β€ π, π, π) / (πβπ)) β€ (absβ(π΄ β (π / π))))) β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
73 | 12, 67, 72 | syl6an 683 |
. . . 4
β’ ((π β§ (π β β+ β§ π β β+))
β (βπ β
β€ βπ β
β (((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
74 | 10, 73 | biimtrrid 242 |
. . 3
β’ ((π β§ (π β β+ β§ π β β+))
β ((βπ β
β€ βπ β
β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
75 | 74 | rexlimdvva 3206 |
. 2
β’ (π β (βπ β β+ βπ β β+
(βπ β β€
βπ β β
((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π))))) β§ βπ β β€ βπ β β ((πΉβ(π / π)) β 0 β (π΄ = (π / π) β¨ (π / (πβπ)) β€ (absβ(π΄ β (π / π)))))) β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
76 | 9, 75 | mpd 15 |
1
β’ (π β βπ₯ β β+ βπ β β€ βπ β β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))) |