Step | Hyp | Ref
| Expression |
1 | | 1rp 12919 |
. . . . . . 7
β’ 1 β
β+ |
2 | | snssi 4768 |
. . . . . . 7
β’ (1 β
β+ β {1} β β+) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
β’ {1}
β β+ |
4 | | ssrab2 4037 |
. . . . . 6
β’ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))} β
β+ |
5 | 3, 4 | unssi 4145 |
. . . . 5
β’ ({1}
βͺ {π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}) β
β+ |
6 | | ltso 11235 |
. . . . . . 7
β’ < Or
β |
7 | 6 | a1i 11 |
. . . . . 6
β’ (π β < Or
β) |
8 | | snfi 8988 |
. . . . . . 7
β’ {1}
β Fin |
9 | | aalioulem2.b |
. . . . . . . . . . 11
β’ (π β πΉ β
(Polyββ€)) |
10 | | aalioulem2.c |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
11 | 10 | nnne0d 12203 |
. . . . . . . . . . . . 13
β’ (π β π β 0) |
12 | | aalioulem2.a |
. . . . . . . . . . . . . 14
β’ π = (degβπΉ) |
13 | 12 | eqcomi 2745 |
. . . . . . . . . . . . 13
β’
(degβπΉ) =
π |
14 | | dgr0 25623 |
. . . . . . . . . . . . 13
β’
(degβ0π) = 0 |
15 | 11, 13, 14 | 3netr4g 3023 |
. . . . . . . . . . . 12
β’ (π β (degβπΉ) β
(degβ0π)) |
16 | | fveq2 6842 |
. . . . . . . . . . . . 13
β’ (πΉ = 0π β
(degβπΉ) =
(degβ0π)) |
17 | 16 | necon3i 2976 |
. . . . . . . . . . . 12
β’
((degβπΉ) β
(degβ0π) β πΉ β
0π) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ β
0π) |
19 | | eqid 2736 |
. . . . . . . . . . . 12
β’ (β‘πΉ β {0}) = (β‘πΉ β {0}) |
20 | 19 | fta1 25668 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyββ€)
β§ πΉ β
0π) β ((β‘πΉ β {0}) β Fin β§
(β―β(β‘πΉ β {0})) β€ (degβπΉ))) |
21 | 9, 18, 20 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β ((β‘πΉ β {0}) β Fin β§
(β―β(β‘πΉ β {0})) β€ (degβπΉ))) |
22 | 21 | simpld 495 |
. . . . . . . . 9
β’ (π β (β‘πΉ β {0}) β Fin) |
23 | | abrexfi 9296 |
. . . . . . . . 9
β’ ((β‘πΉ β {0}) β Fin β {π β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))} β Fin) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ (π β {π β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))} β Fin) |
25 | | rabssab 4043 |
. . . . . . . 8
β’ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))} β {π β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))} |
26 | | ssfi 9117 |
. . . . . . . 8
β’ (({π β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))} β Fin β§ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))} β {π β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}) β {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))} β Fin) |
27 | 24, 25, 26 | sylancl 586 |
. . . . . . 7
β’ (π β {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))} β Fin) |
28 | | unfi 9116 |
. . . . . . 7
β’ (({1}
β Fin β§ {π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))} β Fin) β ({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}) β Fin) |
29 | 8, 27, 28 | sylancr 587 |
. . . . . 6
β’ (π β ({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}) β Fin) |
30 | | 1ex 11151 |
. . . . . . . . 9
β’ 1 β
V |
31 | 30 | snid 4622 |
. . . . . . . 8
β’ 1 β
{1} |
32 | | elun1 4136 |
. . . . . . . 8
β’ (1 β
{1} β 1 β ({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))})) |
33 | | ne0i 4294 |
. . . . . . . 8
β’ (1 β
({1} βͺ {π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}) β ({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}) β β
) |
34 | 31, 32, 33 | mp2b 10 |
. . . . . . 7
β’ ({1}
βͺ {π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}) β β
|
35 | 34 | a1i 11 |
. . . . . 6
β’ (π β ({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}) β β
) |
36 | | rpssre 12922 |
. . . . . . . 8
β’
β+ β β |
37 | 5, 36 | sstri 3953 |
. . . . . . 7
β’ ({1}
βͺ {π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}) β β |
38 | 37 | a1i 11 |
. . . . . 6
β’ (π β ({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}) β β) |
39 | | fiinfcl 9437 |
. . . . . 6
β’ (( <
Or β β§ (({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}) β Fin β§ ({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}) β β
β§ ({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}) β β)) β inf(({1} βͺ
{π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β ({1} βͺ
{π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))})) |
40 | 7, 29, 35, 38, 39 | syl13anc 1372 |
. . . . 5
β’ (π β inf(({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β ({1} βͺ
{π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))})) |
41 | 5, 40 | sselid 3942 |
. . . 4
β’ (π β inf(({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β
β+) |
42 | | 0re 11157 |
. . . . . . . . . . 11
β’ 0 β
β |
43 | | rpge0 12928 |
. . . . . . . . . . . 12
β’ (π β β+
β 0 β€ π) |
44 | 43 | rgen 3066 |
. . . . . . . . . . 11
β’
βπ β
β+ 0 β€ π |
45 | | breq1 5108 |
. . . . . . . . . . . . 13
β’ (π = 0 β (π β€ π β 0 β€ π)) |
46 | 45 | ralbidv 3174 |
. . . . . . . . . . . 12
β’ (π = 0 β (βπ β β+
π β€ π β βπ β β+ 0 β€ π)) |
47 | 46 | rspcev 3581 |
. . . . . . . . . . 11
β’ ((0
β β β§ βπ β β+ 0 β€ π) β βπ β β βπ β β+
π β€ π) |
48 | 42, 44, 47 | mp2an 690 |
. . . . . . . . . 10
β’
βπ β
β βπ β
β+ π β€
π |
49 | | ssralv 4010 |
. . . . . . . . . . . 12
β’ (({1}
βͺ {π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}) β β+ β
(βπ β
β+ π β€
π β βπ β ({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))})π β€ π)) |
50 | 5, 49 | ax-mp 5 |
. . . . . . . . . . 11
β’
(βπ β
β+ π β€
π β βπ β ({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))})π β€ π) |
51 | 50 | reximi 3087 |
. . . . . . . . . 10
β’
(βπ β
β βπ β
β+ π β€
π β βπ β β βπ β ({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))})π β€ π) |
52 | 48, 51 | ax-mp 5 |
. . . . . . . . 9
β’
βπ β
β βπ β
({1} βͺ {π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))})π β€ π |
53 | | eqeq1 2740 |
. . . . . . . . . . . 12
β’ (π = (absβ(π΄ β π)) β (π = (absβ(π΄ β π)) β (absβ(π΄ β π)) = (absβ(π΄ β π)))) |
54 | 53 | rexbidv 3175 |
. . . . . . . . . . 11
β’ (π = (absβ(π΄ β π)) β (βπ β (β‘πΉ β {0})π = (absβ(π΄ β π)) β βπ β (β‘πΉ β {0})(absβ(π΄ β π)) = (absβ(π΄ β π)))) |
55 | | aalioulem2.d |
. . . . . . . . . . . . . . 15
β’ (π β π΄ β β) |
56 | 55 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β π΄ β β) |
57 | | simplr 767 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β π β β) |
58 | 56, 57 | resubcld 11583 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β (π΄ β π) β β) |
59 | 58 | recnd 11183 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β (π΄ β π) β β) |
60 | 55 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (πΉβπ) = 0) β π΄ β β) |
61 | 60 | recnd 11183 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (πΉβπ) = 0) β π΄ β β) |
62 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (πΉβπ) = 0) β π β β) |
63 | 62 | recnd 11183 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (πΉβπ) = 0) β π β β) |
64 | 61, 63 | subeq0ad 11522 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (πΉβπ) = 0) β ((π΄ β π) = 0 β π΄ = π)) |
65 | 64 | necon3abid 2980 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ (πΉβπ) = 0) β ((π΄ β π) β 0 β Β¬ π΄ = π)) |
66 | 65 | biimprd 247 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (πΉβπ) = 0) β (Β¬ π΄ = π β (π΄ β π) β 0)) |
67 | 66 | impr 455 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β (π΄ β π) β 0) |
68 | 59, 67 | absrpcld 15333 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β (absβ(π΄ β π)) β
β+) |
69 | 57 | recnd 11183 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β π β β) |
70 | | simprl 769 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β (πΉβπ) = 0) |
71 | | plyf 25559 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ β (Polyββ€)
β πΉ:ββΆβ) |
72 | 9, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β πΉ:ββΆβ) |
73 | 72 | ffnd 6669 |
. . . . . . . . . . . . . . 15
β’ (π β πΉ Fn β) |
74 | 73 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β πΉ Fn β) |
75 | | fniniseg 7010 |
. . . . . . . . . . . . . 14
β’ (πΉ Fn β β (π β (β‘πΉ β {0}) β (π β β β§ (πΉβπ) = 0))) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β (π β (β‘πΉ β {0}) β (π β β β§ (πΉβπ) = 0))) |
77 | 69, 70, 76 | mpbir2and 711 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β π β (β‘πΉ β {0})) |
78 | | eqid 2736 |
. . . . . . . . . . . 12
β’
(absβ(π΄
β π)) =
(absβ(π΄ β π)) |
79 | | oveq2 7365 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄ β π) = (π΄ β π)) |
80 | 79 | fveq2d 6846 |
. . . . . . . . . . . . 13
β’ (π = π β (absβ(π΄ β π)) = (absβ(π΄ β π))) |
81 | 80 | rspceeqv 3595 |
. . . . . . . . . . . 12
β’ ((π β (β‘πΉ β {0}) β§ (absβ(π΄ β π)) = (absβ(π΄ β π))) β βπ β (β‘πΉ β {0})(absβ(π΄ β π)) = (absβ(π΄ β π))) |
82 | 77, 78, 81 | sylancl 586 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β βπ β (β‘πΉ β {0})(absβ(π΄ β π)) = (absβ(π΄ β π))) |
83 | 54, 68, 82 | elrabd 3647 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β (absβ(π΄ β π)) β {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}) |
84 | | elun2 4137 |
. . . . . . . . . 10
β’
((absβ(π΄
β π)) β {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))} β (absβ(π΄ β π)) β ({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))})) |
85 | 83, 84 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β (absβ(π΄ β π)) β ({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))})) |
86 | | infrelb 12140 |
. . . . . . . . 9
β’ ((({1}
βͺ {π β
β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}) β β β§ βπ β β βπ β ({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))})π β€ π β§ (absβ(π΄ β π)) β ({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))})) β inf(({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π))) |
87 | 37, 52, 85, 86 | mp3an12i 1465 |
. . . . . . . 8
β’ (((π β§ π β β) β§ ((πΉβπ) = 0 β§ Β¬ π΄ = π)) β inf(({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π))) |
88 | 87 | expr 457 |
. . . . . . 7
β’ (((π β§ π β β) β§ (πΉβπ) = 0) β (Β¬ π΄ = π β inf(({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π)))) |
89 | 88 | orrd 861 |
. . . . . 6
β’ (((π β§ π β β) β§ (πΉβπ) = 0) β (π΄ = π β¨ inf(({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π)))) |
90 | 89 | ex 413 |
. . . . 5
β’ ((π β§ π β β) β ((πΉβπ) = 0 β (π΄ = π β¨ inf(({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π))))) |
91 | 90 | ralrimiva 3143 |
. . . 4
β’ (π β βπ β β ((πΉβπ) = 0 β (π΄ = π β¨ inf(({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π))))) |
92 | | breq1 5108 |
. . . . . . . 8
β’ (π₯ = inf(({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β (π₯ β€ (absβ(π΄ β π)) β inf(({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π)))) |
93 | 92 | orbi2d 914 |
. . . . . . 7
β’ (π₯ = inf(({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β ((π΄ = π β¨ π₯ β€ (absβ(π΄ β π))) β (π΄ = π β¨ inf(({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π))))) |
94 | 93 | imbi2d 340 |
. . . . . 6
β’ (π₯ = inf(({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β (((πΉβπ) = 0 β (π΄ = π β¨ π₯ β€ (absβ(π΄ β π)))) β ((πΉβπ) = 0 β (π΄ = π β¨ inf(({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π)))))) |
95 | 94 | ralbidv 3174 |
. . . . 5
β’ (π₯ = inf(({1} βͺ {π β β+
β£ βπ β
(β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β (βπ β β ((πΉβπ) = 0 β (π΄ = π β¨ π₯ β€ (absβ(π΄ β π)))) β βπ β β ((πΉβπ) = 0 β (π΄ = π β¨ inf(({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π)))))) |
96 | 95 | rspcev 3581 |
. . . 4
β’
((inf(({1} βͺ {π
β β+ β£ βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β
β+ β§ βπ β β ((πΉβπ) = 0 β (π΄ = π β¨ inf(({1} βͺ {π β β+ β£
βπ β (β‘πΉ β {0})π = (absβ(π΄ β π))}), β, < ) β€ (absβ(π΄ β π))))) β βπ₯ β β+ βπ β β ((πΉβπ) = 0 β (π΄ = π β¨ π₯ β€ (absβ(π΄ β π))))) |
97 | 41, 91, 96 | syl2anc 584 |
. . 3
β’ (π β βπ₯ β β+ βπ β β ((πΉβπ) = 0 β (π΄ = π β¨ π₯ β€ (absβ(π΄ β π))))) |
98 | | fveqeq2 6851 |
. . . . . . . 8
β’ (π = (π / π) β ((πΉβπ) = 0 β (πΉβ(π / π)) = 0)) |
99 | | eqeq2 2748 |
. . . . . . . . 9
β’ (π = (π / π) β (π΄ = π β π΄ = (π / π))) |
100 | | oveq2 7365 |
. . . . . . . . . . 11
β’ (π = (π / π) β (π΄ β π) = (π΄ β (π / π))) |
101 | 100 | fveq2d 6846 |
. . . . . . . . . 10
β’ (π = (π / π) β (absβ(π΄ β π)) = (absβ(π΄ β (π / π)))) |
102 | 101 | breq2d 5117 |
. . . . . . . . 9
β’ (π = (π / π) β (π₯ β€ (absβ(π΄ β π)) β π₯ β€ (absβ(π΄ β (π / π))))) |
103 | 99, 102 | orbi12d 917 |
. . . . . . . 8
β’ (π = (π / π) β ((π΄ = π β¨ π₯ β€ (absβ(π΄ β π))) β (π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π)))))) |
104 | 98, 103 | imbi12d 344 |
. . . . . . 7
β’ (π = (π / π) β (((πΉβπ) = 0 β (π΄ = π β¨ π₯ β€ (absβ(π΄ β π)))) β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π))))))) |
105 | 104 | rspcv 3577 |
. . . . . 6
β’ ((π / π) β β β (βπ β β ((πΉβπ) = 0 β (π΄ = π β¨ π₯ β€ (absβ(π΄ β π)))) β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π))))))) |
106 | | znq 12877 |
. . . . . . 7
β’ ((π β β€ β§ π β β) β (π / π) β β) |
107 | | qre 12878 |
. . . . . . 7
β’ ((π / π) β β β (π / π) β β) |
108 | 106, 107 | syl 17 |
. . . . . 6
β’ ((π β β€ β§ π β β) β (π / π) β β) |
109 | 105, 108 | syl11 33 |
. . . . 5
β’
(βπ β
β ((πΉβπ) = 0 β (π΄ = π β¨ π₯ β€ (absβ(π΄ β π)))) β ((π β β€ β§ π β β) β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π))))))) |
110 | 109 | ralrimivv 3195 |
. . . 4
β’
(βπ β
β ((πΉβπ) = 0 β (π΄ = π β¨ π₯ β€ (absβ(π΄ β π)))) β βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π)))))) |
111 | 110 | reximi 3087 |
. . 3
β’
(βπ₯ β
β+ βπ β β ((πΉβπ) = 0 β (π΄ = π β¨ π₯ β€ (absβ(π΄ β π)))) β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π)))))) |
112 | 97, 111 | syl 17 |
. 2
β’ (π β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π)))))) |
113 | | simplr 767 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β π₯ β
β+) |
114 | | simprr 771 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β π β
β) |
115 | 10 | nnnn0d 12473 |
. . . . . . . . . . . . . 14
β’ (π β π β
β0) |
116 | 115 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β π β
β0) |
117 | 114, 116 | nnexpcld 14148 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (πβπ) β β) |
118 | 117 | nnrpd 12955 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (πβπ) β
β+) |
119 | 113, 118 | rpdivcld 12974 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (π₯ / (πβπ)) β
β+) |
120 | 119 | rpred 12957 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (π₯ / (πβπ)) β β) |
121 | 120 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β§ π₯ β€ (absβ(π΄ β (π / π)))) β (π₯ / (πβπ)) β β) |
122 | | simpllr 774 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β§ π₯ β€ (absβ(π΄ β (π / π)))) β π₯ β β+) |
123 | 122 | rpred 12957 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β§ π₯ β€ (absβ(π΄ β (π / π)))) β π₯ β β) |
124 | 55 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β π΄ β
β) |
125 | 108 | adantl 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (π / π) β β) |
126 | 124, 125 | resubcld 11583 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (π΄ β (π / π)) β β) |
127 | 126 | recnd 11183 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (π΄ β (π / π)) β β) |
128 | 127 | abscld 15321 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β
(absβ(π΄ β
(π / π))) β β) |
129 | 128 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β§ π₯ β€ (absβ(π΄ β (π / π)))) β (absβ(π΄ β (π / π))) β β) |
130 | | rpre 12923 |
. . . . . . . . . . 11
β’ (π₯ β β+
β π₯ β
β) |
131 | 130 | ad2antlr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β π₯ β
β) |
132 | 113 | rpcnne0d 12966 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (π₯ β β β§ π₯ β 0)) |
133 | | divid 11842 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π₯ β 0) β (π₯ / π₯) = 1) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (π₯ / π₯) = 1) |
135 | 117 | nnge1d 12201 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β 1 β€
(πβπ)) |
136 | 134, 135 | eqbrtrd 5127 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (π₯ / π₯) β€ (πβπ)) |
137 | 131, 113,
118, 136 | lediv23d 13025 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (π₯ / (πβπ)) β€ π₯) |
138 | 137 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β§ π₯ β€ (absβ(π΄ β (π / π)))) β (π₯ / (πβπ)) β€ π₯) |
139 | | simpr 485 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β§ π₯ β€ (absβ(π΄ β (π / π)))) β π₯ β€ (absβ(π΄ β (π / π)))) |
140 | 121, 123,
129, 138, 139 | letrd 11312 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β§ π₯ β€ (absβ(π΄ β (π / π)))) β (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))) |
141 | 140 | ex 413 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β (π₯ β€ (absβ(π΄ β (π / π))) β (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))) |
142 | 141 | orim2d 965 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β ((π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π)))) β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |
143 | 142 | imim2d 57 |
. . . 4
β’ (((π β§ π₯ β β+) β§ (π β β€ β§ π β β)) β
(((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π))))) β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))))) |
144 | 143 | ralimdvva 3201 |
. . 3
β’ ((π β§ π₯ β β+) β
(βπ β β€
βπ β β
((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π))))) β βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))))) |
145 | 144 | reximdva 3165 |
. 2
β’ (π β (βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ π₯ β€ (absβ(π΄ β (π / π))))) β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π))))))) |
146 | 112, 145 | mpd 15 |
1
β’ (π β βπ₯ β β+ βπ β β€ βπ β β ((πΉβ(π / π)) = 0 β (π΄ = (π / π) β¨ (π₯ / (πβπ)) β€ (absβ(π΄ β (π / π)))))) |