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 = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
signsw.w 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⟩ }
Assertion signswch ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) → ( ( 𝑋 𝑌 ) ≠ 𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) )

Proof

Step Hyp Ref Expression
1 signsw.p = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
2 signsw.w 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ 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 ( 𝑋 ∈ { - 1 , 1 } → 𝑋 ∈ { - 1 , 0 , 1 } )
9 1 signspval ( ( 𝑋 ∈ { - 1 , 0 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) → ( 𝑋 𝑌 ) = if ( 𝑌 = 0 , 𝑋 , 𝑌 ) )
10 8 9 sylan ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) → ( 𝑋 𝑌 ) = if ( 𝑌 = 0 , 𝑋 , 𝑌 ) )
11 10 neeq1d ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) → ( ( 𝑋 𝑌 ) ≠ 𝑋 ↔ if ( 𝑌 = 0 , 𝑋 , 𝑌 ) ≠ 𝑋 ) )
12 neeq1 ( 𝑋 = if ( 𝑌 = 0 , 𝑋 , 𝑌 ) → ( 𝑋𝑋 ↔ if ( 𝑌 = 0 , 𝑋 , 𝑌 ) ≠ 𝑋 ) )
13 12 bibi1d ( 𝑋 = if ( 𝑌 = 0 , 𝑋 , 𝑌 ) → ( ( 𝑋𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) ↔ ( if ( 𝑌 = 0 , 𝑋 , 𝑌 ) ≠ 𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) ) )
14 neeq1 ( 𝑌 = if ( 𝑌 = 0 , 𝑋 , 𝑌 ) → ( 𝑌𝑋 ↔ if ( 𝑌 = 0 , 𝑋 , 𝑌 ) ≠ 𝑋 ) )
15 14 bibi1d ( 𝑌 = if ( 𝑌 = 0 , 𝑋 , 𝑌 ) → ( ( 𝑌𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) ↔ ( if ( 𝑌 = 0 , 𝑋 , 𝑌 ) ≠ 𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) ) )
16 neirr ¬ 𝑋𝑋
17 16 a1i ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ 𝑌 = 0 ) → ¬ 𝑋𝑋 )
18 0re 0 ∈ ℝ
19 18 ltnri ¬ 0 < 0
20 simpr ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ 𝑌 = 0 ) → 𝑌 = 0 )
21 20 oveq2d ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ 𝑌 = 0 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 · 0 ) )
22 neg1cn - 1 ∈ ℂ
23 ax-1cn 1 ∈ ℂ
24 prssi ( ( - 1 ∈ ℂ ∧ 1 ∈ ℂ ) → { - 1 , 1 } ⊆ ℂ )
25 22 23 24 mp2an { - 1 , 1 } ⊆ ℂ
26 simpll ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ 𝑌 = 0 ) → 𝑋 ∈ { - 1 , 1 } )
27 25 26 sselid ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ 𝑌 = 0 ) → 𝑋 ∈ ℂ )
28 27 mul01d ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ 𝑌 = 0 ) → ( 𝑋 · 0 ) = 0 )
29 21 28 eqtrd ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ 𝑌 = 0 ) → ( 𝑋 · 𝑌 ) = 0 )
30 29 breq1d ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ 𝑌 = 0 ) → ( ( 𝑋 · 𝑌 ) < 0 ↔ 0 < 0 ) )
31 19 30 mtbiri ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ 𝑌 = 0 ) → ¬ ( 𝑋 · 𝑌 ) < 0 )
32 17 31 2falsed ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ 𝑌 = 0 ) → ( 𝑋𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) )
33 simplr ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ ¬ 𝑌 = 0 ) → 𝑌 ∈ { - 1 , 0 , 1 } )
34 tpcomb { - 1 , 0 , 1 } = { - 1 , 1 , 0 }
35 33 34 eleqtrdi ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ ¬ 𝑌 = 0 ) → 𝑌 ∈ { - 1 , 1 , 0 } )
36 simpr ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ ¬ 𝑌 = 0 ) → ¬ 𝑌 = 0 )
37 36 neqned ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ ¬ 𝑌 = 0 ) → 𝑌 ≠ 0 )
38 35 37 jca ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ ¬ 𝑌 = 0 ) → ( 𝑌 ∈ { - 1 , 1 , 0 } ∧ 𝑌 ≠ 0 ) )
39 eldifsn ( 𝑌 ∈ ( { - 1 , 1 , 0 } ∖ { 0 } ) ↔ ( 𝑌 ∈ { - 1 , 1 , 0 } ∧ 𝑌 ≠ 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 ( 𝑌 ∈ ( { - 1 , 1 , 0 } ∖ { 0 } ) ↔ 𝑌 ∈ { - 1 , 1 } )
45 39 44 bitr3i ( ( 𝑌 ∈ { - 1 , 1 , 0 } ∧ 𝑌 ≠ 0 ) ↔ 𝑌 ∈ { - 1 , 1 } )
46 38 45 sylib ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ ¬ 𝑌 = 0 ) → 𝑌 ∈ { - 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 ( 𝑌 = - 1 → ( 𝑌 ≠ - 1 ↔ - 1 ≠ - 1 ) )
57 oveq2 ( 𝑌 = - 1 → ( - 1 · 𝑌 ) = ( - 1 · - 1 ) )
58 57 breq1d ( 𝑌 = - 1 → ( ( - 1 · 𝑌 ) < 0 ↔ ( - 1 · - 1 ) < 0 ) )
59 56 58 bibi12d ( 𝑌 = - 1 → ( ( 𝑌 ≠ - 1 ↔ ( - 1 · 𝑌 ) < 0 ) ↔ ( - 1 ≠ - 1 ↔ ( - 1 · - 1 ) < 0 ) ) )
60 55 59 mpbiri ( 𝑌 = - 1 → ( 𝑌 ≠ - 1 ↔ ( - 1 · 𝑌 ) < 0 ) )
61 60 adantl ( ( 𝑌 ∈ { - 1 , 1 } ∧ 𝑌 = - 1 ) → ( 𝑌 ≠ - 1 ↔ ( - 1 · 𝑌 ) < 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 ( 𝑌 = 1 → ( 𝑌 ≠ - 1 ↔ 1 ≠ - 1 ) )
72 oveq2 ( 𝑌 = 1 → ( - 1 · 𝑌 ) = ( - 1 · 1 ) )
73 72 breq1d ( 𝑌 = 1 → ( ( - 1 · 𝑌 ) < 0 ↔ ( - 1 · 1 ) < 0 ) )
74 71 73 bibi12d ( 𝑌 = 1 → ( ( 𝑌 ≠ - 1 ↔ ( - 1 · 𝑌 ) < 0 ) ↔ ( 1 ≠ - 1 ↔ ( - 1 · 1 ) < 0 ) ) )
75 70 74 mpbiri ( 𝑌 = 1 → ( 𝑌 ≠ - 1 ↔ ( - 1 · 𝑌 ) < 0 ) )
76 75 adantl ( ( 𝑌 ∈ { - 1 , 1 } ∧ 𝑌 = 1 ) → ( 𝑌 ≠ - 1 ↔ ( - 1 · 𝑌 ) < 0 ) )
77 elpri ( 𝑌 ∈ { - 1 , 1 } → ( 𝑌 = - 1 ∨ 𝑌 = 1 ) )
78 61 76 77 mpjaodan ( 𝑌 ∈ { - 1 , 1 } → ( 𝑌 ≠ - 1 ↔ ( - 1 · 𝑌 ) < 0 ) )
79 78 adantr ( ( 𝑌 ∈ { - 1 , 1 } ∧ 𝑋 = - 1 ) → ( 𝑌 ≠ - 1 ↔ ( - 1 · 𝑌 ) < 0 ) )
80 neeq2 ( 𝑋 = - 1 → ( 𝑌𝑋𝑌 ≠ - 1 ) )
81 oveq1 ( 𝑋 = - 1 → ( 𝑋 · 𝑌 ) = ( - 1 · 𝑌 ) )
82 81 breq1d ( 𝑋 = - 1 → ( ( 𝑋 · 𝑌 ) < 0 ↔ ( - 1 · 𝑌 ) < 0 ) )
83 80 82 bibi12d ( 𝑋 = - 1 → ( ( 𝑌𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) ↔ ( 𝑌 ≠ - 1 ↔ ( - 1 · 𝑌 ) < 0 ) ) )
84 83 adantl ( ( 𝑌 ∈ { - 1 , 1 } ∧ 𝑋 = - 1 ) → ( ( 𝑌𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) ↔ ( 𝑌 ≠ - 1 ↔ ( - 1 · 𝑌 ) < 0 ) ) )
85 79 84 mpbird ( ( 𝑌 ∈ { - 1 , 1 } ∧ 𝑋 = - 1 ) → ( 𝑌𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) )
86 46 85 sylan ( ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ ¬ 𝑌 = 0 ) ∧ 𝑋 = - 1 ) → ( 𝑌𝑋 ↔ ( 𝑋 · 𝑌 ) < 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 ( 𝑌 = - 1 → ( 𝑌 ≠ 1 ↔ - 1 ≠ 1 ) )
93 oveq2 ( 𝑌 = - 1 → ( 1 · 𝑌 ) = ( 1 · - 1 ) )
94 93 breq1d ( 𝑌 = - 1 → ( ( 1 · 𝑌 ) < 0 ↔ ( 1 · - 1 ) < 0 ) )
95 92 94 bibi12d ( 𝑌 = - 1 → ( ( 𝑌 ≠ 1 ↔ ( 1 · 𝑌 ) < 0 ) ↔ ( - 1 ≠ 1 ↔ ( 1 · - 1 ) < 0 ) ) )
96 91 95 mpbiri ( 𝑌 = - 1 → ( 𝑌 ≠ 1 ↔ ( 1 · 𝑌 ) < 0 ) )
97 96 adantl ( ( 𝑌 ∈ { - 1 , 1 } ∧ 𝑌 = - 1 ) → ( 𝑌 ≠ 1 ↔ ( 1 · 𝑌 ) < 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 ( 𝑌 = 1 → ( 𝑌 ≠ 1 ↔ 1 ≠ 1 ) )
104 oveq2 ( 𝑌 = 1 → ( 1 · 𝑌 ) = ( 1 · 1 ) )
105 104 breq1d ( 𝑌 = 1 → ( ( 1 · 𝑌 ) < 0 ↔ ( 1 · 1 ) < 0 ) )
106 103 105 bibi12d ( 𝑌 = 1 → ( ( 𝑌 ≠ 1 ↔ ( 1 · 𝑌 ) < 0 ) ↔ ( 1 ≠ 1 ↔ ( 1 · 1 ) < 0 ) ) )
107 102 106 mpbiri ( 𝑌 = 1 → ( 𝑌 ≠ 1 ↔ ( 1 · 𝑌 ) < 0 ) )
108 107 adantl ( ( 𝑌 ∈ { - 1 , 1 } ∧ 𝑌 = 1 ) → ( 𝑌 ≠ 1 ↔ ( 1 · 𝑌 ) < 0 ) )
109 97 108 77 mpjaodan ( 𝑌 ∈ { - 1 , 1 } → ( 𝑌 ≠ 1 ↔ ( 1 · 𝑌 ) < 0 ) )
110 109 adantr ( ( 𝑌 ∈ { - 1 , 1 } ∧ 𝑋 = 1 ) → ( 𝑌 ≠ 1 ↔ ( 1 · 𝑌 ) < 0 ) )
111 neeq2 ( 𝑋 = 1 → ( 𝑌𝑋𝑌 ≠ 1 ) )
112 oveq1 ( 𝑋 = 1 → ( 𝑋 · 𝑌 ) = ( 1 · 𝑌 ) )
113 112 breq1d ( 𝑋 = 1 → ( ( 𝑋 · 𝑌 ) < 0 ↔ ( 1 · 𝑌 ) < 0 ) )
114 111 113 bibi12d ( 𝑋 = 1 → ( ( 𝑌𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) ↔ ( 𝑌 ≠ 1 ↔ ( 1 · 𝑌 ) < 0 ) ) )
115 114 adantl ( ( 𝑌 ∈ { - 1 , 1 } ∧ 𝑋 = 1 ) → ( ( 𝑌𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) ↔ ( 𝑌 ≠ 1 ↔ ( 1 · 𝑌 ) < 0 ) ) )
116 110 115 mpbird ( ( 𝑌 ∈ { - 1 , 1 } ∧ 𝑋 = 1 ) → ( 𝑌𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) )
117 46 116 sylan ( ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ ¬ 𝑌 = 0 ) ∧ 𝑋 = 1 ) → ( 𝑌𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) )
118 elpri ( 𝑋 ∈ { - 1 , 1 } → ( 𝑋 = - 1 ∨ 𝑋 = 1 ) )
119 118 ad2antrr ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ ¬ 𝑌 = 0 ) → ( 𝑋 = - 1 ∨ 𝑋 = 1 ) )
120 86 117 119 mpjaodan ( ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) ∧ ¬ 𝑌 = 0 ) → ( 𝑌𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) )
121 13 15 32 120 ifbothda ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) → ( if ( 𝑌 = 0 , 𝑋 , 𝑌 ) ≠ 𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) )
122 11 121 bitrd ( ( 𝑋 ∈ { - 1 , 1 } ∧ 𝑌 ∈ { - 1 , 0 , 1 } ) → ( ( 𝑋 𝑌 ) ≠ 𝑋 ↔ ( 𝑋 · 𝑌 ) < 0 ) )