Proof of Theorem signswch
| Step | Hyp | Ref
| Expression |
| 1 | | df-pr 4629 |
. . . . . 6
⊢ {-1, 1} =
({-1} ∪ {1}) |
| 2 | | snsstp1 4816 |
. . . . . . 7
⊢ {-1}
⊆ {-1, 0, 1} |
| 3 | | snsstp3 4818 |
. . . . . . 7
⊢ {1}
⊆ {-1, 0, 1} |
| 4 | 2, 3 | unssi 4191 |
. . . . . 6
⊢ ({-1}
∪ {1}) ⊆ {-1, 0, 1} |
| 5 | 1, 4 | eqsstri 4030 |
. . . . 5
⊢ {-1, 1}
⊆ {-1, 0, 1} |
| 6 | 5 | sseli 3979 |
. . . 4
⊢ (𝑋 ∈ {-1, 1} → 𝑋 ∈ {-1, 0,
1}) |
| 7 | | signsw.p |
. . . . 5
⊢ ⨣ =
(𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦
if(𝑏 = 0, 𝑎, 𝑏)) |
| 8 | 7 | signspval 34567 |
. . . 4
⊢ ((𝑋 ∈ {-1, 0, 1} ∧ 𝑌 ∈ {-1, 0, 1}) →
(𝑋 ⨣ 𝑌) = if(𝑌 = 0, 𝑋, 𝑌)) |
| 9 | 6, 8 | sylan 580 |
. . 3
⊢ ((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) →
(𝑋 ⨣ 𝑌) = if(𝑌 = 0, 𝑋, 𝑌)) |
| 10 | 9 | neeq1d 3000 |
. 2
⊢ ((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) →
((𝑋 ⨣ 𝑌) ≠ 𝑋 ↔ if(𝑌 = 0, 𝑋, 𝑌) ≠ 𝑋)) |
| 11 | | neeq1 3003 |
. . . 4
⊢ (𝑋 = if(𝑌 = 0, 𝑋, 𝑌) → (𝑋 ≠ 𝑋 ↔ if(𝑌 = 0, 𝑋, 𝑌) ≠ 𝑋)) |
| 12 | 11 | bibi1d 343 |
. . 3
⊢ (𝑋 = if(𝑌 = 0, 𝑋, 𝑌) → ((𝑋 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0) ↔ (if(𝑌 = 0, 𝑋, 𝑌) ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0))) |
| 13 | | neeq1 3003 |
. . . 4
⊢ (𝑌 = if(𝑌 = 0, 𝑋, 𝑌) → (𝑌 ≠ 𝑋 ↔ if(𝑌 = 0, 𝑋, 𝑌) ≠ 𝑋)) |
| 14 | 13 | bibi1d 343 |
. . 3
⊢ (𝑌 = if(𝑌 = 0, 𝑋, 𝑌) → ((𝑌 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0) ↔ (if(𝑌 = 0, 𝑋, 𝑌) ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0))) |
| 15 | | neirr 2949 |
. . . . 5
⊢ ¬
𝑋 ≠ 𝑋 |
| 16 | 15 | a1i 11 |
. . . 4
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 = 0) → ¬ 𝑋 ≠ 𝑋) |
| 17 | | 0re 11263 |
. . . . . 6
⊢ 0 ∈
ℝ |
| 18 | 17 | ltnri 11370 |
. . . . 5
⊢ ¬ 0
< 0 |
| 19 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 = 0) → 𝑌 = 0) |
| 20 | 19 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 = 0) → (𝑋 · 𝑌) = (𝑋 · 0)) |
| 21 | | neg1cn 12380 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
| 22 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 23 | | prssi 4821 |
. . . . . . . . . 10
⊢ ((-1
∈ ℂ ∧ 1 ∈ ℂ) → {-1, 1} ⊆
ℂ) |
| 24 | 21, 22, 23 | mp2an 692 |
. . . . . . . . 9
⊢ {-1, 1}
⊆ ℂ |
| 25 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 = 0) → 𝑋 ∈ {-1, 1}) |
| 26 | 24, 25 | sselid 3981 |
. . . . . . . 8
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 = 0) → 𝑋 ∈ ℂ) |
| 27 | 26 | mul01d 11460 |
. . . . . . 7
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 = 0) → (𝑋 · 0) = 0) |
| 28 | 20, 27 | eqtrd 2777 |
. . . . . 6
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 = 0) → (𝑋 · 𝑌) = 0) |
| 29 | 28 | breq1d 5153 |
. . . . 5
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 = 0) → ((𝑋 · 𝑌) < 0 ↔ 0 < 0)) |
| 30 | 18, 29 | mtbiri 327 |
. . . 4
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 = 0) → ¬ (𝑋 · 𝑌) < 0) |
| 31 | 16, 30 | 2falsed 376 |
. . 3
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ 𝑌 = 0) → (𝑋 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0)) |
| 32 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ ¬
𝑌 = 0) → 𝑌 ∈ {-1, 0,
1}) |
| 33 | | tpcomb 4751 |
. . . . . . . 8
⊢ {-1, 0,
1} = {-1, 1, 0} |
| 34 | 32, 33 | eleqtrdi 2851 |
. . . . . . 7
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ ¬
𝑌 = 0) → 𝑌 ∈ {-1, 1,
0}) |
| 35 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ ¬
𝑌 = 0) → ¬ 𝑌 = 0) |
| 36 | 35 | neqned 2947 |
. . . . . . 7
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ ¬
𝑌 = 0) → 𝑌 ≠ 0) |
| 37 | 34, 36 | jca 511 |
. . . . . 6
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ ¬
𝑌 = 0) → (𝑌 ∈ {-1, 1, 0} ∧ 𝑌 ≠ 0)) |
| 38 | | eldifsn 4786 |
. . . . . . 7
⊢ (𝑌 ∈ ({-1, 1, 0} ∖ {0})
↔ (𝑌 ∈ {-1, 1, 0}
∧ 𝑌 ≠
0)) |
| 39 | | neg1ne0 12382 |
. . . . . . . . 9
⊢ -1 ≠
0 |
| 40 | | ax-1ne0 11224 |
. . . . . . . . 9
⊢ 1 ≠
0 |
| 41 | | diftpsn3 4802 |
. . . . . . . . 9
⊢ ((-1 ≠
0 ∧ 1 ≠ 0) → ({-1, 1, 0} ∖ {0}) = {-1, 1}) |
| 42 | 39, 40, 41 | mp2an 692 |
. . . . . . . 8
⊢ ({-1, 1,
0} ∖ {0}) = {-1, 1} |
| 43 | 42 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑌 ∈ ({-1, 1, 0} ∖ {0})
↔ 𝑌 ∈ {-1,
1}) |
| 44 | 38, 43 | bitr3i 277 |
. . . . . 6
⊢ ((𝑌 ∈ {-1, 1, 0} ∧ 𝑌 ≠ 0) ↔ 𝑌 ∈ {-1,
1}) |
| 45 | 37, 44 | sylib 218 |
. . . . 5
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ ¬
𝑌 = 0) → 𝑌 ∈ {-1,
1}) |
| 46 | | neirr 2949 |
. . . . . . . . . . 11
⊢ ¬ -1
≠ -1 |
| 47 | | 0le1 11786 |
. . . . . . . . . . . . 13
⊢ 0 ≤
1 |
| 48 | | 1re 11261 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
| 49 | 17, 48 | lenlti 11381 |
. . . . . . . . . . . . 13
⊢ (0 ≤ 1
↔ ¬ 1 < 0) |
| 50 | 47, 49 | mpbi 230 |
. . . . . . . . . . . 12
⊢ ¬ 1
< 0 |
| 51 | | neg1mulneg1e1 12479 |
. . . . . . . . . . . . 13
⊢ (-1
· -1) = 1 |
| 52 | 51 | breq1i 5150 |
. . . . . . . . . . . 12
⊢ ((-1
· -1) < 0 ↔ 1 < 0) |
| 53 | 50, 52 | mtbir 323 |
. . . . . . . . . . 11
⊢ ¬
(-1 · -1) < 0 |
| 54 | 46, 53 | 2false 375 |
. . . . . . . . . 10
⊢ (-1 ≠
-1 ↔ (-1 · -1) < 0) |
| 55 | | neeq1 3003 |
. . . . . . . . . . 11
⊢ (𝑌 = -1 → (𝑌 ≠ -1 ↔ -1 ≠
-1)) |
| 56 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑌 = -1 → (-1 · 𝑌) = (-1 ·
-1)) |
| 57 | 56 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑌 = -1 → ((-1 · 𝑌) < 0 ↔ (-1 · -1)
< 0)) |
| 58 | 55, 57 | bibi12d 345 |
. . . . . . . . . 10
⊢ (𝑌 = -1 → ((𝑌 ≠ -1 ↔ (-1 · 𝑌) < 0) ↔ (-1 ≠ -1
↔ (-1 · -1) < 0))) |
| 59 | 54, 58 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑌 = -1 → (𝑌 ≠ -1 ↔ (-1 · 𝑌) < 0)) |
| 60 | 59 | adantl 481 |
. . . . . . . 8
⊢ ((𝑌 ∈ {-1, 1} ∧ 𝑌 = -1) → (𝑌 ≠ -1 ↔ (-1 · 𝑌) < 0)) |
| 61 | | neg1rr 12381 |
. . . . . . . . . . . 12
⊢ -1 ∈
ℝ |
| 62 | | neg1lt0 12383 |
. . . . . . . . . . . . 13
⊢ -1 <
0 |
| 63 | | 0lt1 11785 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
| 64 | 61, 17, 48 | lttri 11387 |
. . . . . . . . . . . . 13
⊢ ((-1 <
0 ∧ 0 < 1) → -1 < 1) |
| 65 | 62, 63, 64 | mp2an 692 |
. . . . . . . . . . . 12
⊢ -1 <
1 |
| 66 | 61, 65 | gtneii 11373 |
. . . . . . . . . . 11
⊢ 1 ≠
-1 |
| 67 | 21 | mulridi 11265 |
. . . . . . . . . . . 12
⊢ (-1
· 1) = -1 |
| 68 | 67, 62 | eqbrtri 5164 |
. . . . . . . . . . 11
⊢ (-1
· 1) < 0 |
| 69 | 66, 68 | 2th 264 |
. . . . . . . . . 10
⊢ (1 ≠
-1 ↔ (-1 · 1) < 0) |
| 70 | | neeq1 3003 |
. . . . . . . . . . 11
⊢ (𝑌 = 1 → (𝑌 ≠ -1 ↔ 1 ≠ -1)) |
| 71 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑌 = 1 → (-1 · 𝑌) = (-1 ·
1)) |
| 72 | 71 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑌 = 1 → ((-1 · 𝑌) < 0 ↔ (-1 · 1)
< 0)) |
| 73 | 70, 72 | bibi12d 345 |
. . . . . . . . . 10
⊢ (𝑌 = 1 → ((𝑌 ≠ -1 ↔ (-1 · 𝑌) < 0) ↔ (1 ≠ -1
↔ (-1 · 1) < 0))) |
| 74 | 69, 73 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑌 = 1 → (𝑌 ≠ -1 ↔ (-1 · 𝑌) < 0)) |
| 75 | 74 | adantl 481 |
. . . . . . . 8
⊢ ((𝑌 ∈ {-1, 1} ∧ 𝑌 = 1) → (𝑌 ≠ -1 ↔ (-1 · 𝑌) < 0)) |
| 76 | | elpri 4649 |
. . . . . . . 8
⊢ (𝑌 ∈ {-1, 1} → (𝑌 = -1 ∨ 𝑌 = 1)) |
| 77 | 60, 75, 76 | mpjaodan 961 |
. . . . . . 7
⊢ (𝑌 ∈ {-1, 1} → (𝑌 ≠ -1 ↔ (-1 ·
𝑌) <
0)) |
| 78 | 77 | adantr 480 |
. . . . . 6
⊢ ((𝑌 ∈ {-1, 1} ∧ 𝑋 = -1) → (𝑌 ≠ -1 ↔ (-1 · 𝑌) < 0)) |
| 79 | | neeq2 3004 |
. . . . . . . 8
⊢ (𝑋 = -1 → (𝑌 ≠ 𝑋 ↔ 𝑌 ≠ -1)) |
| 80 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑋 = -1 → (𝑋 · 𝑌) = (-1 · 𝑌)) |
| 81 | 80 | breq1d 5153 |
. . . . . . . 8
⊢ (𝑋 = -1 → ((𝑋 · 𝑌) < 0 ↔ (-1 · 𝑌) < 0)) |
| 82 | 79, 81 | bibi12d 345 |
. . . . . . 7
⊢ (𝑋 = -1 → ((𝑌 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0) ↔ (𝑌 ≠ -1 ↔ (-1 · 𝑌) < 0))) |
| 83 | 82 | adantl 481 |
. . . . . 6
⊢ ((𝑌 ∈ {-1, 1} ∧ 𝑋 = -1) → ((𝑌 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0) ↔ (𝑌 ≠ -1 ↔ (-1 · 𝑌) < 0))) |
| 84 | 78, 83 | mpbird 257 |
. . . . 5
⊢ ((𝑌 ∈ {-1, 1} ∧ 𝑋 = -1) → (𝑌 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0)) |
| 85 | 45, 84 | sylan 580 |
. . . 4
⊢ ((((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ ¬
𝑌 = 0) ∧ 𝑋 = -1) → (𝑌 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0)) |
| 86 | 66 | necomi 2995 |
. . . . . . . . . . 11
⊢ -1 ≠
1 |
| 87 | 21, 22 | mulcomi 11269 |
. . . . . . . . . . . . 13
⊢ (-1
· 1) = (1 · -1) |
| 88 | 87 | breq1i 5150 |
. . . . . . . . . . . 12
⊢ ((-1
· 1) < 0 ↔ (1 · -1) < 0) |
| 89 | 68, 88 | mpbi 230 |
. . . . . . . . . . 11
⊢ (1
· -1) < 0 |
| 90 | 86, 89 | 2th 264 |
. . . . . . . . . 10
⊢ (-1 ≠
1 ↔ (1 · -1) < 0) |
| 91 | | neeq1 3003 |
. . . . . . . . . . 11
⊢ (𝑌 = -1 → (𝑌 ≠ 1 ↔ -1 ≠ 1)) |
| 92 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑌 = -1 → (1 · 𝑌) = (1 ·
-1)) |
| 93 | 92 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑌 = -1 → ((1 · 𝑌) < 0 ↔ (1 · -1)
< 0)) |
| 94 | 91, 93 | bibi12d 345 |
. . . . . . . . . 10
⊢ (𝑌 = -1 → ((𝑌 ≠ 1 ↔ (1 · 𝑌) < 0) ↔ (-1 ≠ 1 ↔ (1
· -1) < 0))) |
| 95 | 90, 94 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑌 = -1 → (𝑌 ≠ 1 ↔ (1 · 𝑌) < 0)) |
| 96 | 95 | adantl 481 |
. . . . . . . 8
⊢ ((𝑌 ∈ {-1, 1} ∧ 𝑌 = -1) → (𝑌 ≠ 1 ↔ (1 · 𝑌) < 0)) |
| 97 | | neirr 2949 |
. . . . . . . . . . 11
⊢ ¬ 1
≠ 1 |
| 98 | 22 | mulridi 11265 |
. . . . . . . . . . . . 13
⊢ (1
· 1) = 1 |
| 99 | 98 | breq1i 5150 |
. . . . . . . . . . . 12
⊢ ((1
· 1) < 0 ↔ 1 < 0) |
| 100 | 50, 99 | mtbir 323 |
. . . . . . . . . . 11
⊢ ¬ (1
· 1) < 0 |
| 101 | 97, 100 | 2false 375 |
. . . . . . . . . 10
⊢ (1 ≠ 1
↔ (1 · 1) < 0) |
| 102 | | neeq1 3003 |
. . . . . . . . . . 11
⊢ (𝑌 = 1 → (𝑌 ≠ 1 ↔ 1 ≠ 1)) |
| 103 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑌 = 1 → (1 · 𝑌) = (1 ·
1)) |
| 104 | 103 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑌 = 1 → ((1 · 𝑌) < 0 ↔ (1 · 1)
< 0)) |
| 105 | 102, 104 | bibi12d 345 |
. . . . . . . . . 10
⊢ (𝑌 = 1 → ((𝑌 ≠ 1 ↔ (1 · 𝑌) < 0) ↔ (1 ≠ 1 ↔ (1
· 1) < 0))) |
| 106 | 101, 105 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑌 = 1 → (𝑌 ≠ 1 ↔ (1 · 𝑌) < 0)) |
| 107 | 106 | adantl 481 |
. . . . . . . 8
⊢ ((𝑌 ∈ {-1, 1} ∧ 𝑌 = 1) → (𝑌 ≠ 1 ↔ (1 · 𝑌) < 0)) |
| 108 | 96, 107, 76 | mpjaodan 961 |
. . . . . . 7
⊢ (𝑌 ∈ {-1, 1} → (𝑌 ≠ 1 ↔ (1 · 𝑌) < 0)) |
| 109 | 108 | adantr 480 |
. . . . . 6
⊢ ((𝑌 ∈ {-1, 1} ∧ 𝑋 = 1) → (𝑌 ≠ 1 ↔ (1 · 𝑌) < 0)) |
| 110 | | neeq2 3004 |
. . . . . . . 8
⊢ (𝑋 = 1 → (𝑌 ≠ 𝑋 ↔ 𝑌 ≠ 1)) |
| 111 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑋 = 1 → (𝑋 · 𝑌) = (1 · 𝑌)) |
| 112 | 111 | breq1d 5153 |
. . . . . . . 8
⊢ (𝑋 = 1 → ((𝑋 · 𝑌) < 0 ↔ (1 · 𝑌) < 0)) |
| 113 | 110, 112 | bibi12d 345 |
. . . . . . 7
⊢ (𝑋 = 1 → ((𝑌 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0) ↔ (𝑌 ≠ 1 ↔ (1 · 𝑌) < 0))) |
| 114 | 113 | adantl 481 |
. . . . . 6
⊢ ((𝑌 ∈ {-1, 1} ∧ 𝑋 = 1) → ((𝑌 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0) ↔ (𝑌 ≠ 1 ↔ (1 · 𝑌) < 0))) |
| 115 | 109, 114 | mpbird 257 |
. . . . 5
⊢ ((𝑌 ∈ {-1, 1} ∧ 𝑋 = 1) → (𝑌 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0)) |
| 116 | 45, 115 | sylan 580 |
. . . 4
⊢ ((((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ ¬
𝑌 = 0) ∧ 𝑋 = 1) → (𝑌 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0)) |
| 117 | | elpri 4649 |
. . . . 5
⊢ (𝑋 ∈ {-1, 1} → (𝑋 = -1 ∨ 𝑋 = 1)) |
| 118 | 117 | ad2antrr 726 |
. . . 4
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ ¬
𝑌 = 0) → (𝑋 = -1 ∨ 𝑋 = 1)) |
| 119 | 85, 116, 118 | mpjaodan 961 |
. . 3
⊢ (((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) ∧ ¬
𝑌 = 0) → (𝑌 ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0)) |
| 120 | 12, 14, 31, 119 | ifbothda 4564 |
. 2
⊢ ((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) →
(if(𝑌 = 0, 𝑋, 𝑌) ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0)) |
| 121 | 10, 120 | bitrd 279 |
1
⊢ ((𝑋 ∈ {-1, 1} ∧ 𝑌 ∈ {-1, 0, 1}) →
((𝑋 ⨣ 𝑌) ≠ 𝑋 ↔ (𝑋 · 𝑌) < 0)) |