Metamath Proof Explorer


Theorem signswch

Description: The zero-skipping operation changes value when the operands change signs. (Contributed by Thierry Arnoux, 9-Oct-2018)

Ref Expression
Hypotheses signsw.p
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
signsw.w
|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
Assertion signswch
|- ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( ( X .+^ Y ) =/= X <-> ( X x. Y ) < 0 ) )

Proof

Step Hyp Ref Expression
1 signsw.p
 |-  .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
2 signsw.w
 |-  W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
3 df-pr
 |-  { -u 1 , 1 } = ( { -u 1 } u. { 1 } )
4 snsstp1
 |-  { -u 1 } C_ { -u 1 , 0 , 1 }
5 snsstp3
 |-  { 1 } C_ { -u 1 , 0 , 1 }
6 4 5 unssi
 |-  ( { -u 1 } u. { 1 } ) C_ { -u 1 , 0 , 1 }
7 3 6 eqsstri
 |-  { -u 1 , 1 } C_ { -u 1 , 0 , 1 }
8 7 sseli
 |-  ( X e. { -u 1 , 1 } -> X e. { -u 1 , 0 , 1 } )
9 1 signspval
 |-  ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( X .+^ Y ) = if ( Y = 0 , X , Y ) )
10 8 9 sylan
 |-  ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( X .+^ Y ) = if ( Y = 0 , X , Y ) )
11 10 neeq1d
 |-  ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( ( X .+^ Y ) =/= X <-> if ( Y = 0 , X , Y ) =/= X ) )
12 neeq1
 |-  ( X = if ( Y = 0 , X , Y ) -> ( X =/= X <-> if ( Y = 0 , X , Y ) =/= X ) )
13 12 bibi1d
 |-  ( X = if ( Y = 0 , X , Y ) -> ( ( X =/= X <-> ( X x. Y ) < 0 ) <-> ( if ( Y = 0 , X , Y ) =/= X <-> ( X x. Y ) < 0 ) ) )
14 neeq1
 |-  ( Y = if ( Y = 0 , X , Y ) -> ( Y =/= X <-> if ( Y = 0 , X , Y ) =/= X ) )
15 14 bibi1d
 |-  ( Y = if ( Y = 0 , X , Y ) -> ( ( Y =/= X <-> ( X x. Y ) < 0 ) <-> ( if ( Y = 0 , X , Y ) =/= X <-> ( X x. Y ) < 0 ) ) )
16 neirr
 |-  -. X =/= X
17 16 a1i
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y = 0 ) -> -. X =/= X )
18 0re
 |-  0 e. RR
19 18 ltnri
 |-  -. 0 < 0
20 simpr
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y = 0 ) -> Y = 0 )
21 20 oveq2d
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y = 0 ) -> ( X x. Y ) = ( X x. 0 ) )
22 neg1cn
 |-  -u 1 e. CC
23 ax-1cn
 |-  1 e. CC
24 prssi
 |-  ( ( -u 1 e. CC /\ 1 e. CC ) -> { -u 1 , 1 } C_ CC )
25 22 23 24 mp2an
 |-  { -u 1 , 1 } C_ CC
26 simpll
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y = 0 ) -> X e. { -u 1 , 1 } )
27 25 26 sselid
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y = 0 ) -> X e. CC )
28 27 mul01d
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y = 0 ) -> ( X x. 0 ) = 0 )
29 21 28 eqtrd
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y = 0 ) -> ( X x. Y ) = 0 )
30 29 breq1d
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y = 0 ) -> ( ( X x. Y ) < 0 <-> 0 < 0 ) )
31 19 30 mtbiri
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y = 0 ) -> -. ( X x. Y ) < 0 )
32 17 31 2falsed
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y = 0 ) -> ( X =/= X <-> ( X x. Y ) < 0 ) )
33 simplr
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ -. Y = 0 ) -> Y e. { -u 1 , 0 , 1 } )
34 tpcomb
 |-  { -u 1 , 0 , 1 } = { -u 1 , 1 , 0 }
35 33 34 eleqtrdi
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ -. Y = 0 ) -> Y e. { -u 1 , 1 , 0 } )
36 simpr
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ -. Y = 0 ) -> -. Y = 0 )
37 36 neqned
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ -. Y = 0 ) -> Y =/= 0 )
38 35 37 jca
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ -. Y = 0 ) -> ( Y e. { -u 1 , 1 , 0 } /\ Y =/= 0 ) )
39 eldifsn
 |-  ( Y e. ( { -u 1 , 1 , 0 } \ { 0 } ) <-> ( Y e. { -u 1 , 1 , 0 } /\ Y =/= 0 ) )
40 neg1ne0
 |-  -u 1 =/= 0
41 ax-1ne0
 |-  1 =/= 0
42 diftpsn3
 |-  ( ( -u 1 =/= 0 /\ 1 =/= 0 ) -> ( { -u 1 , 1 , 0 } \ { 0 } ) = { -u 1 , 1 } )
43 40 41 42 mp2an
 |-  ( { -u 1 , 1 , 0 } \ { 0 } ) = { -u 1 , 1 }
44 43 eleq2i
 |-  ( Y e. ( { -u 1 , 1 , 0 } \ { 0 } ) <-> Y e. { -u 1 , 1 } )
45 39 44 bitr3i
 |-  ( ( Y e. { -u 1 , 1 , 0 } /\ Y =/= 0 ) <-> Y e. { -u 1 , 1 } )
46 38 45 sylib
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ -. Y = 0 ) -> Y e. { -u 1 , 1 } )
47 neirr
 |-  -. -u 1 =/= -u 1
48 0le1
 |-  0 <_ 1
49 1re
 |-  1 e. RR
50 18 49 lenlti
 |-  ( 0 <_ 1 <-> -. 1 < 0 )
51 48 50 mpbi
 |-  -. 1 < 0
52 neg1mulneg1e1
 |-  ( -u 1 x. -u 1 ) = 1
53 52 breq1i
 |-  ( ( -u 1 x. -u 1 ) < 0 <-> 1 < 0 )
54 51 53 mtbir
 |-  -. ( -u 1 x. -u 1 ) < 0
55 47 54 2false
 |-  ( -u 1 =/= -u 1 <-> ( -u 1 x. -u 1 ) < 0 )
56 neeq1
 |-  ( Y = -u 1 -> ( Y =/= -u 1 <-> -u 1 =/= -u 1 ) )
57 oveq2
 |-  ( Y = -u 1 -> ( -u 1 x. Y ) = ( -u 1 x. -u 1 ) )
58 57 breq1d
 |-  ( Y = -u 1 -> ( ( -u 1 x. Y ) < 0 <-> ( -u 1 x. -u 1 ) < 0 ) )
59 56 58 bibi12d
 |-  ( Y = -u 1 -> ( ( Y =/= -u 1 <-> ( -u 1 x. Y ) < 0 ) <-> ( -u 1 =/= -u 1 <-> ( -u 1 x. -u 1 ) < 0 ) ) )
60 55 59 mpbiri
 |-  ( Y = -u 1 -> ( Y =/= -u 1 <-> ( -u 1 x. Y ) < 0 ) )
61 60 adantl
 |-  ( ( Y e. { -u 1 , 1 } /\ Y = -u 1 ) -> ( Y =/= -u 1 <-> ( -u 1 x. Y ) < 0 ) )
62 neg1rr
 |-  -u 1 e. RR
63 neg1lt0
 |-  -u 1 < 0
64 0lt1
 |-  0 < 1
65 62 18 49 lttri
 |-  ( ( -u 1 < 0 /\ 0 < 1 ) -> -u 1 < 1 )
66 63 64 65 mp2an
 |-  -u 1 < 1
67 62 66 gtneii
 |-  1 =/= -u 1
68 22 mulid1i
 |-  ( -u 1 x. 1 ) = -u 1
69 68 63 eqbrtri
 |-  ( -u 1 x. 1 ) < 0
70 67 69 2th
 |-  ( 1 =/= -u 1 <-> ( -u 1 x. 1 ) < 0 )
71 neeq1
 |-  ( Y = 1 -> ( Y =/= -u 1 <-> 1 =/= -u 1 ) )
72 oveq2
 |-  ( Y = 1 -> ( -u 1 x. Y ) = ( -u 1 x. 1 ) )
73 72 breq1d
 |-  ( Y = 1 -> ( ( -u 1 x. Y ) < 0 <-> ( -u 1 x. 1 ) < 0 ) )
74 71 73 bibi12d
 |-  ( Y = 1 -> ( ( Y =/= -u 1 <-> ( -u 1 x. Y ) < 0 ) <-> ( 1 =/= -u 1 <-> ( -u 1 x. 1 ) < 0 ) ) )
75 70 74 mpbiri
 |-  ( Y = 1 -> ( Y =/= -u 1 <-> ( -u 1 x. Y ) < 0 ) )
76 75 adantl
 |-  ( ( Y e. { -u 1 , 1 } /\ Y = 1 ) -> ( Y =/= -u 1 <-> ( -u 1 x. Y ) < 0 ) )
77 elpri
 |-  ( Y e. { -u 1 , 1 } -> ( Y = -u 1 \/ Y = 1 ) )
78 61 76 77 mpjaodan
 |-  ( Y e. { -u 1 , 1 } -> ( Y =/= -u 1 <-> ( -u 1 x. Y ) < 0 ) )
79 78 adantr
 |-  ( ( Y e. { -u 1 , 1 } /\ X = -u 1 ) -> ( Y =/= -u 1 <-> ( -u 1 x. Y ) < 0 ) )
80 neeq2
 |-  ( X = -u 1 -> ( Y =/= X <-> Y =/= -u 1 ) )
81 oveq1
 |-  ( X = -u 1 -> ( X x. Y ) = ( -u 1 x. Y ) )
82 81 breq1d
 |-  ( X = -u 1 -> ( ( X x. Y ) < 0 <-> ( -u 1 x. Y ) < 0 ) )
83 80 82 bibi12d
 |-  ( X = -u 1 -> ( ( Y =/= X <-> ( X x. Y ) < 0 ) <-> ( Y =/= -u 1 <-> ( -u 1 x. Y ) < 0 ) ) )
84 83 adantl
 |-  ( ( Y e. { -u 1 , 1 } /\ X = -u 1 ) -> ( ( Y =/= X <-> ( X x. Y ) < 0 ) <-> ( Y =/= -u 1 <-> ( -u 1 x. Y ) < 0 ) ) )
85 79 84 mpbird
 |-  ( ( Y e. { -u 1 , 1 } /\ X = -u 1 ) -> ( Y =/= X <-> ( X x. Y ) < 0 ) )
86 46 85 sylan
 |-  ( ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ -. Y = 0 ) /\ X = -u 1 ) -> ( Y =/= X <-> ( X x. Y ) < 0 ) )
87 67 necomi
 |-  -u 1 =/= 1
88 22 23 mulcomi
 |-  ( -u 1 x. 1 ) = ( 1 x. -u 1 )
89 88 breq1i
 |-  ( ( -u 1 x. 1 ) < 0 <-> ( 1 x. -u 1 ) < 0 )
90 69 89 mpbi
 |-  ( 1 x. -u 1 ) < 0
91 87 90 2th
 |-  ( -u 1 =/= 1 <-> ( 1 x. -u 1 ) < 0 )
92 neeq1
 |-  ( Y = -u 1 -> ( Y =/= 1 <-> -u 1 =/= 1 ) )
93 oveq2
 |-  ( Y = -u 1 -> ( 1 x. Y ) = ( 1 x. -u 1 ) )
94 93 breq1d
 |-  ( Y = -u 1 -> ( ( 1 x. Y ) < 0 <-> ( 1 x. -u 1 ) < 0 ) )
95 92 94 bibi12d
 |-  ( Y = -u 1 -> ( ( Y =/= 1 <-> ( 1 x. Y ) < 0 ) <-> ( -u 1 =/= 1 <-> ( 1 x. -u 1 ) < 0 ) ) )
96 91 95 mpbiri
 |-  ( Y = -u 1 -> ( Y =/= 1 <-> ( 1 x. Y ) < 0 ) )
97 96 adantl
 |-  ( ( Y e. { -u 1 , 1 } /\ Y = -u 1 ) -> ( Y =/= 1 <-> ( 1 x. Y ) < 0 ) )
98 neirr
 |-  -. 1 =/= 1
99 23 mulid1i
 |-  ( 1 x. 1 ) = 1
100 99 breq1i
 |-  ( ( 1 x. 1 ) < 0 <-> 1 < 0 )
101 51 100 mtbir
 |-  -. ( 1 x. 1 ) < 0
102 98 101 2false
 |-  ( 1 =/= 1 <-> ( 1 x. 1 ) < 0 )
103 neeq1
 |-  ( Y = 1 -> ( Y =/= 1 <-> 1 =/= 1 ) )
104 oveq2
 |-  ( Y = 1 -> ( 1 x. Y ) = ( 1 x. 1 ) )
105 104 breq1d
 |-  ( Y = 1 -> ( ( 1 x. Y ) < 0 <-> ( 1 x. 1 ) < 0 ) )
106 103 105 bibi12d
 |-  ( Y = 1 -> ( ( Y =/= 1 <-> ( 1 x. Y ) < 0 ) <-> ( 1 =/= 1 <-> ( 1 x. 1 ) < 0 ) ) )
107 102 106 mpbiri
 |-  ( Y = 1 -> ( Y =/= 1 <-> ( 1 x. Y ) < 0 ) )
108 107 adantl
 |-  ( ( Y e. { -u 1 , 1 } /\ Y = 1 ) -> ( Y =/= 1 <-> ( 1 x. Y ) < 0 ) )
109 97 108 77 mpjaodan
 |-  ( Y e. { -u 1 , 1 } -> ( Y =/= 1 <-> ( 1 x. Y ) < 0 ) )
110 109 adantr
 |-  ( ( Y e. { -u 1 , 1 } /\ X = 1 ) -> ( Y =/= 1 <-> ( 1 x. Y ) < 0 ) )
111 neeq2
 |-  ( X = 1 -> ( Y =/= X <-> Y =/= 1 ) )
112 oveq1
 |-  ( X = 1 -> ( X x. Y ) = ( 1 x. Y ) )
113 112 breq1d
 |-  ( X = 1 -> ( ( X x. Y ) < 0 <-> ( 1 x. Y ) < 0 ) )
114 111 113 bibi12d
 |-  ( X = 1 -> ( ( Y =/= X <-> ( X x. Y ) < 0 ) <-> ( Y =/= 1 <-> ( 1 x. Y ) < 0 ) ) )
115 114 adantl
 |-  ( ( Y e. { -u 1 , 1 } /\ X = 1 ) -> ( ( Y =/= X <-> ( X x. Y ) < 0 ) <-> ( Y =/= 1 <-> ( 1 x. Y ) < 0 ) ) )
116 110 115 mpbird
 |-  ( ( Y e. { -u 1 , 1 } /\ X = 1 ) -> ( Y =/= X <-> ( X x. Y ) < 0 ) )
117 46 116 sylan
 |-  ( ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ -. Y = 0 ) /\ X = 1 ) -> ( Y =/= X <-> ( X x. Y ) < 0 ) )
118 elpri
 |-  ( X e. { -u 1 , 1 } -> ( X = -u 1 \/ X = 1 ) )
119 118 ad2antrr
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ -. Y = 0 ) -> ( X = -u 1 \/ X = 1 ) )
120 86 117 119 mpjaodan
 |-  ( ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ -. Y = 0 ) -> ( Y =/= X <-> ( X x. Y ) < 0 ) )
121 13 15 32 120 ifbothda
 |-  ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( if ( Y = 0 , X , Y ) =/= X <-> ( X x. Y ) < 0 ) )
122 11 121 bitrd
 |-  ( ( X e. { -u 1 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( ( X .+^ Y ) =/= X <-> ( X x. Y ) < 0 ) )