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∈−101,b∈−101⟼ifb=0ab
signsw.w ⊢W=Basendx−101+ndx⨣˙
Assertion signswch ⊢X∈−11∧Y∈−101→X⨣˙Y≠X↔X⁢Y<0

Proof

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