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 sseldi ⊢ ( ( ( 𝑋 ∈ { - 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 ) )