Step | Hyp | Ref
| Expression |
1 | | aalioulem2.a |
. . 3
β’ π = (degβπΉ) |
2 | | aalioulem2.b |
. . 3
β’ (π β πΉ β
(Polyββ€)) |
3 | | aalioulem2.c |
. . 3
β’ (π β π β β) |
4 | | aalioulem2.d |
. . 3
β’ (π β π΄ β β) |
5 | | aalioulem3.e |
. . 3
β’ (π β (πΉβπ΄) = 0) |
6 | 1, 2, 3, 4, 5 | aalioulem3 25710 |
. 2
β’ (π β βπ₯ β β+ βπ β β
((absβ(π΄ β
π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π)))) |
7 | | simp2l 1200 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β π β β€) |
8 | | simp2r 1201 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β π β β) |
9 | | znq 12884 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π β β) β (π / π) β β) |
10 | 7, 8, 9 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π / π) β β) |
11 | | qre 12885 |
. . . . . . . . . 10
β’ ((π / π) β β β (π / π) β β) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π / π) β β) |
13 | | simp3r 1203 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (absβ(π΄ β (π / π))) β€ 1) |
14 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π = (π / π) β (π΄ β π) = (π΄ β (π / π))) |
15 | 14 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π = (π / π) β (absβ(π΄ β π)) = (absβ(π΄ β (π / π)))) |
16 | 15 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (π = (π / π) β ((absβ(π΄ β π)) β€ 1 β (absβ(π΄ β (π / π))) β€ 1)) |
17 | | 2fveq3 6852 |
. . . . . . . . . . . . . 14
β’ (π = (π / π) β (absβ(πΉβπ)) = (absβ(πΉβ(π / π)))) |
18 | 17 | oveq2d 7378 |
. . . . . . . . . . . . 13
β’ (π = (π / π) β (π₯ Β· (absβ(πΉβπ))) = (π₯ Β· (absβ(πΉβ(π / π))))) |
19 | 18, 15 | breq12d 5123 |
. . . . . . . . . . . 12
β’ (π = (π / π) β ((π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π)) β (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π))))) |
20 | 16, 19 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = (π / π) β (((absβ(π΄ β π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π))) β ((absβ(π΄ β (π / π))) β€ 1 β (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))))) |
21 | 20 | rspcv 3580 |
. . . . . . . . . 10
β’ ((π / π) β β β (βπ β β
((absβ(π΄ β
π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π))) β ((absβ(π΄ β (π / π))) β€ 1 β (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))))) |
22 | 21 | com23 86 |
. . . . . . . . 9
β’ ((π / π) β β β ((absβ(π΄ β (π / π))) β€ 1 β (βπ β β ((absβ(π΄ β π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π))) β (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))))) |
23 | 12, 13, 22 | sylc 65 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (βπ β β
((absβ(π΄ β
π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π))) β (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π))))) |
24 | | simp1r 1199 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β π₯ β β+) |
25 | 8 | nnrpd 12962 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β π β β+) |
26 | | simp1l 1198 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β π) |
27 | 26, 3 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β π β β) |
28 | 27 | nnzd 12533 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β π β β€) |
29 | 25, 28 | rpexpcld 14157 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (πβπ) β
β+) |
30 | 24, 29 | rpdivcld 12981 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π₯ / (πβπ)) β
β+) |
31 | 30 | rpred 12964 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π₯ / (πβπ)) β β) |
32 | 31 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β§ (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))) β (π₯ / (πβπ)) β β) |
33 | 24 | rpred 12964 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β π₯ β β) |
34 | 26, 2 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β πΉ β
(Polyββ€)) |
35 | | plyf 25575 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β (Polyββ€)
β πΉ:ββΆβ) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β πΉ:ββΆβ) |
37 | 12 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π / π) β β) |
38 | 36, 37 | ffvelcdmd 7041 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (πΉβ(π / π)) β β) |
39 | 38 | abscld 15328 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (absβ(πΉβ(π / π))) β β) |
40 | 33, 39 | remulcld 11192 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π₯ Β· (absβ(πΉβ(π / π)))) β β) |
41 | 40 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β§ (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))) β (π₯ Β· (absβ(πΉβ(π / π)))) β β) |
42 | 26, 4 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β π΄ β β) |
43 | 42, 12 | resubcld 11590 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π΄ β (π / π)) β β) |
44 | 43 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π΄ β (π / π)) β β) |
45 | 44 | abscld 15328 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (absβ(π΄ β (π / π))) β β) |
46 | 45 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β§ (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))) β (absβ(π΄ β (π / π))) β β) |
47 | 24 | rpcnd 12966 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β π₯ β β) |
48 | 29 | rpcnd 12966 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (πβπ) β β) |
49 | 29 | rpne0d 12969 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (πβπ) β 0) |
50 | 47, 48, 49 | divrecd 11941 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π₯ / (πβπ)) = (π₯ Β· (1 / (πβπ)))) |
51 | 48, 38 | absmuld 15346 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (absβ((πβπ) Β· (πΉβ(π / π)))) = ((absβ(πβπ)) Β· (absβ(πΉβ(π / π))))) |
52 | 29 | rpred 12964 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (πβπ) β β) |
53 | 29 | rpge0d 12968 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β 0 β€ (πβπ)) |
54 | 52, 53 | absidd 15314 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (absβ(πβπ)) = (πβπ)) |
55 | 54 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β ((absβ(πβπ)) Β· (absβ(πΉβ(π / π)))) = ((πβπ) Β· (absβ(πΉβ(π / π))))) |
56 | 51, 55 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (absβ((πβπ) Β· (πΉβ(π / π)))) = ((πβπ) Β· (absβ(πΉβ(π / π))))) |
57 | 48, 38 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β ((πβπ) Β· (πΉβ(π / π))) = ((πΉβ(π / π)) Β· (πβπ))) |
58 | 1 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πβπ) = (πβ(degβπΉ)) |
59 | 58 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉβ(π / π)) Β· (πβπ)) = ((πΉβ(π / π)) Β· (πβ(degβπΉ))) |
60 | 57, 59 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β ((πβπ) Β· (πΉβ(π / π))) = ((πΉβ(π / π)) Β· (πβ(degβπΉ)))) |
61 | 34, 7, 8 | aalioulem1 25708 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β ((πΉβ(π / π)) Β· (πβ(degβπΉ))) β β€) |
62 | 60, 61 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β ((πβπ) Β· (πΉβ(π / π))) β β€) |
63 | | simp3l 1202 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (πΉβ(π / π)) β 0) |
64 | 48, 38, 49, 63 | mulne0d 11814 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β ((πβπ) Β· (πΉβ(π / π))) β 0) |
65 | | nnabscl 15217 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πβπ) Β· (πΉβ(π / π))) β β€ β§ ((πβπ) Β· (πΉβ(π / π))) β 0) β (absβ((πβπ) Β· (πΉβ(π / π)))) β β) |
66 | 62, 64, 65 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (absβ((πβπ) Β· (πΉβ(π / π)))) β β) |
67 | 56, 66 | eqeltrrd 2839 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β ((πβπ) Β· (absβ(πΉβ(π / π)))) β β) |
68 | 67 | nnge1d 12208 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β 1 β€ ((πβπ) Β· (absβ(πΉβ(π / π))))) |
69 | | 1red 11163 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β 1 β
β) |
70 | 69, 39, 29 | ledivmuld 13017 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β ((1 / (πβπ)) β€ (absβ(πΉβ(π / π))) β 1 β€ ((πβπ) Β· (absβ(πΉβ(π / π)))))) |
71 | 68, 70 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (1 / (πβπ)) β€ (absβ(πΉβ(π / π)))) |
72 | 29 | rprecred 12975 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (1 / (πβπ)) β β) |
73 | 72, 39, 24 | lemul2d 13008 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β ((1 / (πβπ)) β€ (absβ(πΉβ(π / π))) β (π₯ Β· (1 / (πβπ))) β€ (π₯ Β· (absβ(πΉβ(π / π)))))) |
74 | 71, 73 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π₯ Β· (1 / (πβπ))) β€ (π₯ Β· (absβ(πΉβ(π / π))))) |
75 | 50, 74 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (π₯ / (πβπ)) β€ (π₯ Β· (absβ(πΉβ(π / π))))) |
76 | 75 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β§ (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))) β (π₯ / (πβπ)) β€ (π₯ Β· (absβ(πΉβ(π / π))))) |
77 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β§ (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))) β (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))) |
78 | 32, 41, 46, 76, 77 | letrd 11319 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β§ (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))) β (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))) |
79 | 78 | olcd 873 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β§ (π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π)))) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
80 | 79 | ex 414 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β ((π₯ Β· (absβ(πΉβ(π / π)))) β€ (absβ(π΄ β (π / π))) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
81 | 23, 80 | syld 47 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β) β§ ((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1)) β (βπ β β
((absβ(π΄ β
π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π))) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
82 | 81 | 3exp 1120 |
. . . . . 6
β’ ((π β§ π₯ β β+) β ((π β β€ β§ π β β) β (((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1) β (βπ β β
((absβ(π΄ β
π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π))) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))))) |
83 | 82 | com34 91 |
. . . . 5
β’ ((π β§ π₯ β β+) β ((π β β€ β§ π β β) β
(βπ β β
((absβ(π΄ β
π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π))) β (((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))))) |
84 | 83 | com23 86 |
. . . 4
β’ ((π β§ π₯ β β+) β
(βπ β β
((absβ(π΄ β
π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π))) β ((π β β€ β§ π β β) β (((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))))) |
85 | 84 | ralrimdvv 3199 |
. . 3
β’ ((π β§ π₯ β β+) β
(βπ β β
((absβ(π΄ β
π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π))) β βπ β β€ βπ β β (((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))))) |
86 | 85 | reximdva 3166 |
. 2
β’ (π β (βπ₯ β β+ βπ β β
((absβ(π΄ β
π)) β€ 1 β (π₯ Β· (absβ(πΉβπ))) β€ (absβ(π΄ β π))) β βπ₯ β β+ βπ β β€ βπ β β (((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))))) |
87 | 6, 86 | mpd 15 |
1
β’ (π β βπ₯ β β+ βπ β β€ βπ β β (((πΉβ(π / π)) β 0 β§ (absβ(π΄ β (π / π))) β€ 1) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |