---

Step * of Lemma mul-minus-2

∀x,y:Top.  (x * (-y) ~ -(x * y))
BY
{ ((Intros THEN SqEqualTopToBase) THEN SqReasoning) }

1
1. y : Base
2. x : Base
3. (x * (-y))↓
4. x ∈ ℤ
5. -y ∈ ℤ
6. (-y)↓
7. y ∈ ℤ
⊢ x * (-y) ≤ -(x * y)

2
1. y : Base
2. x : Base
3. is-exception(x * (-y))
4. x ∈ ℤ
5. is-exception(-y)
6. is-exception(y)
⊢ x * (-y) ≤ -(x * y)

3
1. y : Base
2. x : Base
3. (-(x * y))↓
4. x * y ∈ ℤ
5. (x * y)↓
6. x ∈ ℤ
7. y ∈ ℤ
⊢ -(x * y) ≤ x * (-y)

4
1. y : Base
2. x : Base
3. is-exception(-(x * y))
4. is-exception(x * y)
5. x ∈ ℤ
6. is-exception(y)
⊢ -(x * y) ≤ x * (-y)

---

Latex:

---

Latex:
\mforall{}x,y:Top.    (x  *  (-y)  \msim{}  -(x  *  y))


By

---

Latex:
((Intros  THEN  SqEqualTopToBase)  THEN  SqReasoning)

---

Home Index