Step | Hyp | Ref
| Expression |
1 | | df-pr 4632 |
. . . . . 6
β’ {-1, 1} =
({-1} βͺ {1}) |
2 | | snsstp1 4820 |
. . . . . . 7
β’ {-1}
β {-1, 0, 1} |
3 | | snsstp3 4822 |
. . . . . . 7
β’ {1}
β {-1, 0, 1} |
4 | 2, 3 | unssi 4186 |
. . . . . 6
β’ ({-1}
βͺ {1}) β {-1, 0, 1} |
5 | 1, 4 | eqsstri 4017 |
. . . . 5
β’ {-1, 1}
β {-1, 0, 1} |
6 | 5 | sseli 3979 |
. . . 4
β’ (π β {-1, 1} β π β {-1, 0,
1}) |
7 | | signsw.p |
. . . . 5
⒠⨣ =
(π β {-1, 0, 1}, π β {-1, 0, 1} β¦
if(π = 0, π, π)) |
8 | 7 | signspval 33563 |
. . . 4
β’ ((π β {-1, 0, 1} β§ π β {-1, 0, 1}) β
(π ⨣ π) = if(π = 0, π, π)) |
9 | 6, 8 | sylan 581 |
. . 3
β’ ((π β {-1, 1} β§ π β {-1, 0, 1}) β
(π ⨣ π) = if(π = 0, π, π)) |
10 | 9 | neeq1d 3001 |
. 2
β’ ((π β {-1, 1} β§ π β {-1, 0, 1}) β
((π ⨣ π) β π β if(π = 0, π, π) β π)) |
11 | | neeq1 3004 |
. . . 4
β’ (π = if(π = 0, π, π) β (π β π β if(π = 0, π, π) β π)) |
12 | 11 | bibi1d 344 |
. . 3
β’ (π = if(π = 0, π, π) β ((π β π β (π Β· π) < 0) β (if(π = 0, π, π) β π β (π Β· π) < 0))) |
13 | | neeq1 3004 |
. . . 4
β’ (π = if(π = 0, π, π) β (π β π β if(π = 0, π, π) β π)) |
14 | 13 | bibi1d 344 |
. . 3
β’ (π = if(π = 0, π, π) β ((π β π β (π Β· π) < 0) β (if(π = 0, π, π) β π β (π Β· π) < 0))) |
15 | | neirr 2950 |
. . . . 5
β’ Β¬
π β π |
16 | 15 | a1i 11 |
. . . 4
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ π = 0) β Β¬ π β π) |
17 | | 0re 11216 |
. . . . . 6
β’ 0 β
β |
18 | 17 | ltnri 11323 |
. . . . 5
β’ Β¬ 0
< 0 |
19 | | simpr 486 |
. . . . . . . 8
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ π = 0) β π = 0) |
20 | 19 | oveq2d 7425 |
. . . . . . 7
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ π = 0) β (π Β· π) = (π Β· 0)) |
21 | | neg1cn 12326 |
. . . . . . . . . 10
β’ -1 β
β |
22 | | ax-1cn 11168 |
. . . . . . . . . 10
β’ 1 β
β |
23 | | prssi 4825 |
. . . . . . . . . 10
β’ ((-1
β β β§ 1 β β) β {-1, 1} β
β) |
24 | 21, 22, 23 | mp2an 691 |
. . . . . . . . 9
β’ {-1, 1}
β β |
25 | | simpll 766 |
. . . . . . . . 9
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ π = 0) β π β {-1, 1}) |
26 | 24, 25 | sselid 3981 |
. . . . . . . 8
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ π = 0) β π β β) |
27 | 26 | mul01d 11413 |
. . . . . . 7
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ π = 0) β (π Β· 0) = 0) |
28 | 20, 27 | eqtrd 2773 |
. . . . . 6
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ π = 0) β (π Β· π) = 0) |
29 | 28 | breq1d 5159 |
. . . . 5
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ π = 0) β ((π Β· π) < 0 β 0 < 0)) |
30 | 18, 29 | mtbiri 327 |
. . . 4
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ π = 0) β Β¬ (π Β· π) < 0) |
31 | 16, 30 | 2falsed 377 |
. . 3
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ π = 0) β (π β π β (π Β· π) < 0)) |
32 | | simplr 768 |
. . . . . . . 8
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ Β¬
π = 0) β π β {-1, 0,
1}) |
33 | | tpcomb 4756 |
. . . . . . . 8
β’ {-1, 0,
1} = {-1, 1, 0} |
34 | 32, 33 | eleqtrdi 2844 |
. . . . . . 7
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ Β¬
π = 0) β π β {-1, 1,
0}) |
35 | | simpr 486 |
. . . . . . . 8
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ Β¬
π = 0) β Β¬ π = 0) |
36 | 35 | neqned 2948 |
. . . . . . 7
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ Β¬
π = 0) β π β 0) |
37 | 34, 36 | jca 513 |
. . . . . 6
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ Β¬
π = 0) β (π β {-1, 1, 0} β§ π β 0)) |
38 | | eldifsn 4791 |
. . . . . . 7
β’ (π β ({-1, 1, 0} β {0})
β (π β {-1, 1, 0}
β§ π β
0)) |
39 | | neg1ne0 12328 |
. . . . . . . . 9
β’ -1 β
0 |
40 | | ax-1ne0 11179 |
. . . . . . . . 9
β’ 1 β
0 |
41 | | diftpsn3 4806 |
. . . . . . . . 9
β’ ((-1 β
0 β§ 1 β 0) β ({-1, 1, 0} β {0}) = {-1, 1}) |
42 | 39, 40, 41 | mp2an 691 |
. . . . . . . 8
β’ ({-1, 1,
0} β {0}) = {-1, 1} |
43 | 42 | eleq2i 2826 |
. . . . . . 7
β’ (π β ({-1, 1, 0} β {0})
β π β {-1,
1}) |
44 | 38, 43 | bitr3i 277 |
. . . . . 6
β’ ((π β {-1, 1, 0} β§ π β 0) β π β {-1,
1}) |
45 | 37, 44 | sylib 217 |
. . . . 5
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ Β¬
π = 0) β π β {-1,
1}) |
46 | | neirr 2950 |
. . . . . . . . . . 11
β’ Β¬ -1
β -1 |
47 | | 0le1 11737 |
. . . . . . . . . . . . 13
β’ 0 β€
1 |
48 | | 1re 11214 |
. . . . . . . . . . . . . 14
β’ 1 β
β |
49 | 17, 48 | lenlti 11334 |
. . . . . . . . . . . . 13
β’ (0 β€ 1
β Β¬ 1 < 0) |
50 | 47, 49 | mpbi 229 |
. . . . . . . . . . . 12
β’ Β¬ 1
< 0 |
51 | | neg1mulneg1e1 12425 |
. . . . . . . . . . . . 13
β’ (-1
Β· -1) = 1 |
52 | 51 | breq1i 5156 |
. . . . . . . . . . . 12
β’ ((-1
Β· -1) < 0 β 1 < 0) |
53 | 50, 52 | mtbir 323 |
. . . . . . . . . . 11
β’ Β¬
(-1 Β· -1) < 0 |
54 | 46, 53 | 2false 376 |
. . . . . . . . . 10
β’ (-1 β
-1 β (-1 Β· -1) < 0) |
55 | | neeq1 3004 |
. . . . . . . . . . 11
β’ (π = -1 β (π β -1 β -1 β
-1)) |
56 | | oveq2 7417 |
. . . . . . . . . . . 12
β’ (π = -1 β (-1 Β· π) = (-1 Β·
-1)) |
57 | 56 | breq1d 5159 |
. . . . . . . . . . 11
β’ (π = -1 β ((-1 Β· π) < 0 β (-1 Β· -1)
< 0)) |
58 | 55, 57 | bibi12d 346 |
. . . . . . . . . 10
β’ (π = -1 β ((π β -1 β (-1 Β· π) < 0) β (-1 β -1
β (-1 Β· -1) < 0))) |
59 | 54, 58 | mpbiri 258 |
. . . . . . . . 9
β’ (π = -1 β (π β -1 β (-1 Β· π) < 0)) |
60 | 59 | adantl 483 |
. . . . . . . 8
β’ ((π β {-1, 1} β§ π = -1) β (π β -1 β (-1 Β· π) < 0)) |
61 | | neg1rr 12327 |
. . . . . . . . . . . 12
β’ -1 β
β |
62 | | neg1lt0 12329 |
. . . . . . . . . . . . 13
β’ -1 <
0 |
63 | | 0lt1 11736 |
. . . . . . . . . . . . 13
β’ 0 <
1 |
64 | 61, 17, 48 | lttri 11340 |
. . . . . . . . . . . . 13
β’ ((-1 <
0 β§ 0 < 1) β -1 < 1) |
65 | 62, 63, 64 | mp2an 691 |
. . . . . . . . . . . 12
β’ -1 <
1 |
66 | 61, 65 | gtneii 11326 |
. . . . . . . . . . 11
β’ 1 β
-1 |
67 | 21 | mulridi 11218 |
. . . . . . . . . . . 12
β’ (-1
Β· 1) = -1 |
68 | 67, 62 | eqbrtri 5170 |
. . . . . . . . . . 11
β’ (-1
Β· 1) < 0 |
69 | 66, 68 | 2th 264 |
. . . . . . . . . 10
β’ (1 β
-1 β (-1 Β· 1) < 0) |
70 | | neeq1 3004 |
. . . . . . . . . . 11
β’ (π = 1 β (π β -1 β 1 β -1)) |
71 | | oveq2 7417 |
. . . . . . . . . . . 12
β’ (π = 1 β (-1 Β· π) = (-1 Β·
1)) |
72 | 71 | breq1d 5159 |
. . . . . . . . . . 11
β’ (π = 1 β ((-1 Β· π) < 0 β (-1 Β· 1)
< 0)) |
73 | 70, 72 | bibi12d 346 |
. . . . . . . . . 10
β’ (π = 1 β ((π β -1 β (-1 Β· π) < 0) β (1 β -1
β (-1 Β· 1) < 0))) |
74 | 69, 73 | mpbiri 258 |
. . . . . . . . 9
β’ (π = 1 β (π β -1 β (-1 Β· π) < 0)) |
75 | 74 | adantl 483 |
. . . . . . . 8
β’ ((π β {-1, 1} β§ π = 1) β (π β -1 β (-1 Β· π) < 0)) |
76 | | elpri 4651 |
. . . . . . . 8
β’ (π β {-1, 1} β (π = -1 β¨ π = 1)) |
77 | 60, 75, 76 | mpjaodan 958 |
. . . . . . 7
β’ (π β {-1, 1} β (π β -1 β (-1 Β·
π) <
0)) |
78 | 77 | adantr 482 |
. . . . . 6
β’ ((π β {-1, 1} β§ π = -1) β (π β -1 β (-1 Β· π) < 0)) |
79 | | neeq2 3005 |
. . . . . . . 8
β’ (π = -1 β (π β π β π β -1)) |
80 | | oveq1 7416 |
. . . . . . . . 9
β’ (π = -1 β (π Β· π) = (-1 Β· π)) |
81 | 80 | breq1d 5159 |
. . . . . . . 8
β’ (π = -1 β ((π Β· π) < 0 β (-1 Β· π) < 0)) |
82 | 79, 81 | bibi12d 346 |
. . . . . . 7
β’ (π = -1 β ((π β π β (π Β· π) < 0) β (π β -1 β (-1 Β· π) < 0))) |
83 | 82 | adantl 483 |
. . . . . 6
β’ ((π β {-1, 1} β§ π = -1) β ((π β π β (π Β· π) < 0) β (π β -1 β (-1 Β· π) < 0))) |
84 | 78, 83 | mpbird 257 |
. . . . 5
β’ ((π β {-1, 1} β§ π = -1) β (π β π β (π Β· π) < 0)) |
85 | 45, 84 | sylan 581 |
. . . 4
β’ ((((π β {-1, 1} β§ π β {-1, 0, 1}) β§ Β¬
π = 0) β§ π = -1) β (π β π β (π Β· π) < 0)) |
86 | 66 | necomi 2996 |
. . . . . . . . . . 11
β’ -1 β
1 |
87 | 21, 22 | mulcomi 11222 |
. . . . . . . . . . . . 13
β’ (-1
Β· 1) = (1 Β· -1) |
88 | 87 | breq1i 5156 |
. . . . . . . . . . . 12
β’ ((-1
Β· 1) < 0 β (1 Β· -1) < 0) |
89 | 68, 88 | mpbi 229 |
. . . . . . . . . . 11
β’ (1
Β· -1) < 0 |
90 | 86, 89 | 2th 264 |
. . . . . . . . . 10
β’ (-1 β
1 β (1 Β· -1) < 0) |
91 | | neeq1 3004 |
. . . . . . . . . . 11
β’ (π = -1 β (π β 1 β -1 β 1)) |
92 | | oveq2 7417 |
. . . . . . . . . . . 12
β’ (π = -1 β (1 Β· π) = (1 Β·
-1)) |
93 | 92 | breq1d 5159 |
. . . . . . . . . . 11
β’ (π = -1 β ((1 Β· π) < 0 β (1 Β· -1)
< 0)) |
94 | 91, 93 | bibi12d 346 |
. . . . . . . . . 10
β’ (π = -1 β ((π β 1 β (1 Β· π) < 0) β (-1 β 1 β (1
Β· -1) < 0))) |
95 | 90, 94 | mpbiri 258 |
. . . . . . . . 9
β’ (π = -1 β (π β 1 β (1 Β· π) < 0)) |
96 | 95 | adantl 483 |
. . . . . . . 8
β’ ((π β {-1, 1} β§ π = -1) β (π β 1 β (1 Β· π) < 0)) |
97 | | neirr 2950 |
. . . . . . . . . . 11
β’ Β¬ 1
β 1 |
98 | 22 | mulridi 11218 |
. . . . . . . . . . . . 13
β’ (1
Β· 1) = 1 |
99 | 98 | breq1i 5156 |
. . . . . . . . . . . 12
β’ ((1
Β· 1) < 0 β 1 < 0) |
100 | 50, 99 | mtbir 323 |
. . . . . . . . . . 11
β’ Β¬ (1
Β· 1) < 0 |
101 | 97, 100 | 2false 376 |
. . . . . . . . . 10
β’ (1 β 1
β (1 Β· 1) < 0) |
102 | | neeq1 3004 |
. . . . . . . . . . 11
β’ (π = 1 β (π β 1 β 1 β 1)) |
103 | | oveq2 7417 |
. . . . . . . . . . . 12
β’ (π = 1 β (1 Β· π) = (1 Β·
1)) |
104 | 103 | breq1d 5159 |
. . . . . . . . . . 11
β’ (π = 1 β ((1 Β· π) < 0 β (1 Β· 1)
< 0)) |
105 | 102, 104 | bibi12d 346 |
. . . . . . . . . 10
β’ (π = 1 β ((π β 1 β (1 Β· π) < 0) β (1 β 1 β (1
Β· 1) < 0))) |
106 | 101, 105 | mpbiri 258 |
. . . . . . . . 9
β’ (π = 1 β (π β 1 β (1 Β· π) < 0)) |
107 | 106 | adantl 483 |
. . . . . . . 8
β’ ((π β {-1, 1} β§ π = 1) β (π β 1 β (1 Β· π) < 0)) |
108 | 96, 107, 76 | mpjaodan 958 |
. . . . . . 7
β’ (π β {-1, 1} β (π β 1 β (1 Β· π) < 0)) |
109 | 108 | adantr 482 |
. . . . . 6
β’ ((π β {-1, 1} β§ π = 1) β (π β 1 β (1 Β· π) < 0)) |
110 | | neeq2 3005 |
. . . . . . . 8
β’ (π = 1 β (π β π β π β 1)) |
111 | | oveq1 7416 |
. . . . . . . . 9
β’ (π = 1 β (π Β· π) = (1 Β· π)) |
112 | 111 | breq1d 5159 |
. . . . . . . 8
β’ (π = 1 β ((π Β· π) < 0 β (1 Β· π) < 0)) |
113 | 110, 112 | bibi12d 346 |
. . . . . . 7
β’ (π = 1 β ((π β π β (π Β· π) < 0) β (π β 1 β (1 Β· π) < 0))) |
114 | 113 | adantl 483 |
. . . . . 6
β’ ((π β {-1, 1} β§ π = 1) β ((π β π β (π Β· π) < 0) β (π β 1 β (1 Β· π) < 0))) |
115 | 109, 114 | mpbird 257 |
. . . . 5
β’ ((π β {-1, 1} β§ π = 1) β (π β π β (π Β· π) < 0)) |
116 | 45, 115 | sylan 581 |
. . . 4
β’ ((((π β {-1, 1} β§ π β {-1, 0, 1}) β§ Β¬
π = 0) β§ π = 1) β (π β π β (π Β· π) < 0)) |
117 | | elpri 4651 |
. . . . 5
β’ (π β {-1, 1} β (π = -1 β¨ π = 1)) |
118 | 117 | ad2antrr 725 |
. . . 4
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ Β¬
π = 0) β (π = -1 β¨ π = 1)) |
119 | 85, 116, 118 | mpjaodan 958 |
. . 3
β’ (((π β {-1, 1} β§ π β {-1, 0, 1}) β§ Β¬
π = 0) β (π β π β (π Β· π) < 0)) |
120 | 12, 14, 31, 119 | ifbothda 4567 |
. 2
β’ ((π β {-1, 1} β§ π β {-1, 0, 1}) β
(if(π = 0, π, π) β π β (π Β· π) < 0)) |
121 | 10, 120 | bitrd 279 |
1
β’ ((π β {-1, 1} β§ π β {-1, 0, 1}) β
((π ⨣ π) β π β (π Β· π) < 0)) |