---

Step * of Lemma mul-minus-1

∀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. (-x)↓
7. x ∈ ℤ
⊢ (-x) * y ≤ -(x * y)

2
1. y : Base
2. x : Base
3. is-exception((-x) * y)
4. -x ∈ ℤ
5. is-exception(y)
6. (-x)↓
7. x ∈ ℤ
⊢ (-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