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 ∈ − 1 0 1 , b ∈ − 1 0 1 ⟼ if b = 0 a b
signsw.w ⊢ W = Base ndx − 1 0 1 + ndx ⨣ ˙
Assertion signswch ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 → X ⨣ ˙ Y ≠ X ↔ X ⁢ Y < 0

Proof

Step Hyp Ref Expression
1 signsw.p ⊢ ⨣ ˙ = a ∈ − 1 0 1 , b ∈ − 1 0 1 ⟼ if b = 0 a b
2 signsw.w ⊢ W = Base ndx − 1 0 1 + ndx ⨣ ˙
3 df-pr ⊢ − 1 1 = − 1 ∪ 1
4 snsstp1 ⊢ − 1 ⊆ − 1 0 1
5 snsstp3 ⊢ 1 ⊆ − 1 0 1
6 4 5 unssi ⊢ − 1 ∪ 1 ⊆ − 1 0 1
7 3 6 eqsstri ⊢ − 1 1 ⊆ − 1 0 1
8 7 sseli ⊢ X ∈ − 1 1 → X ∈ − 1 0 1
9 1 signspval ⊢ X ∈ − 1 0 1 ∧ Y ∈ − 1 0 1 → X ⨣ ˙ Y = if Y = 0 X Y
10 8 9 sylan ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 → X ⨣ ˙ Y = if Y = 0 X Y
11 10 neeq1d ⊢ X ∈ − 1 1 ∧ Y ∈ − 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 ⁢ Y < 0 ↔ if Y = 0 X Y ≠ 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 ⁢ Y < 0 ↔ if Y = 0 X Y ≠ X ↔ X ⁢ Y < 0
16 neirr ⊢ ¬ X ≠ X
17 16 a1i ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ Y = 0 → ¬ X ≠ X
18 0re ⊢ 0 ∈ ℝ
19 18 ltnri ⊢ ¬ 0 < 0
20 simpr ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ Y = 0 → Y = 0
21 20 oveq2d ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ Y = 0 → X ⁢ Y = X ⋅ 0
22 neg1cn ⊢ − 1 ∈ ℂ
23 ax-1cn ⊢ 1 ∈ ℂ
24 prssi ⊢ − 1 ∈ ℂ ∧ 1 ∈ ℂ → − 1 1 ⊆ ℂ
25 22 23 24 mp2an ⊢ − 1 1 ⊆ ℂ
26 simpll ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ Y = 0 → X ∈ − 1 1
27 25 26 sseldi ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ Y = 0 → X ∈ ℂ
28 27 mul01d ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ Y = 0 → X ⋅ 0 = 0
29 21 28 eqtrd ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ Y = 0 → X ⁢ Y = 0
30 29 breq1d ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ Y = 0 → X ⁢ Y < 0 ↔ 0 < 0
31 19 30 mtbiri ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ Y = 0 → ¬ X ⁢ Y < 0
32 17 31 2falsed ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ Y = 0 → X ≠ X ↔ X ⁢ Y < 0
33 simplr ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ ¬ Y = 0 → Y ∈ − 1 0 1
34 tpcomb ⊢ − 1 0 1 = − 1 1 0
35 33 34 eleqtrdi ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ ¬ Y = 0 → Y ∈ − 1 1 0
36 simpr ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ ¬ Y = 0 → ¬ Y = 0
37 36 neqned ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ ¬ Y = 0 → Y ≠ 0
38 35 37 jca ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ ¬ Y = 0 → Y ∈ − 1 1 0 ∧ Y ≠ 0
39 eldifsn ⊢ Y ∈ − 1 1 0 ∖ 0 ↔ Y ∈ − 1 1 0 ∧ Y ≠ 0
40 neg1ne0 ⊢ − 1 ≠ 0
41 ax-1ne0 ⊢ 1 ≠ 0
42 diftpsn3 ⊢ − 1 ≠ 0 ∧ 1 ≠ 0 → − 1 1 0 ∖ 0 = − 1 1
43 40 41 42 mp2an ⊢ − 1 1 0 ∖ 0 = − 1 1
44 43 eleq2i ⊢ Y ∈ − 1 1 0 ∖ 0 ↔ Y ∈ − 1 1
45 39 44 bitr3i ⊢ Y ∈ − 1 1 0 ∧ Y ≠ 0 ↔ Y ∈ − 1 1
46 38 45 sylib ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ ¬ Y = 0 → Y ∈ − 1 1
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 ∈ − 1 1 ∧ 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 mulid1i ⊢ -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 ∈ − 1 1 ∧ Y = 1 → Y ≠ − 1 ↔ -1 ⁢ Y < 0
77 elpri ⊢ Y ∈ − 1 1 → Y = − 1 ∨ Y = 1
78 61 76 77 mpjaodan ⊢ Y ∈ − 1 1 → Y ≠ − 1 ↔ -1 ⁢ Y < 0
79 78 adantr ⊢ Y ∈ − 1 1 ∧ 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 ∈ − 1 1 ∧ X = − 1 → Y ≠ X ↔ X ⁢ Y < 0 ↔ Y ≠ − 1 ↔ -1 ⁢ Y < 0
85 79 84 mpbird ⊢ Y ∈ − 1 1 ∧ X = − 1 → Y ≠ X ↔ X ⁢ Y < 0
86 46 85 sylan ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ ¬ 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 ∈ − 1 1 ∧ Y = − 1 → Y ≠ 1 ↔ 1 ⁢ Y < 0
98 neirr ⊢ ¬ 1 ≠ 1
99 23 mulid1i ⊢ 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 ∈ − 1 1 ∧ Y = 1 → Y ≠ 1 ↔ 1 ⁢ Y < 0
109 97 108 77 mpjaodan ⊢ Y ∈ − 1 1 → Y ≠ 1 ↔ 1 ⁢ Y < 0
110 109 adantr ⊢ Y ∈ − 1 1 ∧ 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 ∈ − 1 1 ∧ X = 1 → Y ≠ X ↔ X ⁢ Y < 0 ↔ Y ≠ 1 ↔ 1 ⁢ Y < 0
116 110 115 mpbird ⊢ Y ∈ − 1 1 ∧ X = 1 → Y ≠ X ↔ X ⁢ Y < 0
117 46 116 sylan ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ ¬ Y = 0 ∧ X = 1 → Y ≠ X ↔ X ⁢ Y < 0
118 elpri ⊢ X ∈ − 1 1 → X = − 1 ∨ X = 1
119 118 ad2antrr ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ ¬ Y = 0 → X = − 1 ∨ X = 1
120 86 117 119 mpjaodan ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 ∧ ¬ Y = 0 → Y ≠ X ↔ X ⁢ Y < 0
121 13 15 32 120 ifbothda ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 → if Y = 0 X Y ≠ X ↔ X ⁢ Y < 0
122 11 121 bitrd ⊢ X ∈ − 1 1 ∧ Y ∈ − 1 0 1 → X ⨣ ˙ Y ≠ X ↔ X ⁢ Y < 0