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 sseldi 
 |-  ( ( ( 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 ) )