Step
*
1
of Lemma
zero-mul
1. x : ℤ
2. (0 * x) + x ~ x
⊢ 0 * x ~ 0
BY
{ ((Assert ((0 * x) + x) + (-x) ~ x + (-x) BY (EqCD THEN Trivial)) THEN (RWO "add-associates" (-1) THENA Auto)) }
1
1. x : ℤ
2. (0 * x) + x ~ x
3. (0 * x) + x + (-x) ~ x + (-x)
⊢ 0 * x ~ 0
Latex:
Latex:
1. x : \mBbbZ{}
2. (0 * x) + x \msim{} x
\mvdash{} 0 * x \msim{} 0
By
Latex:
((Assert ((0 * x) + x) + (-x) \msim{} x + (-x) BY
(EqCD THEN Trivial))
THEN (RWO "add-associates" (-1) THENA Auto)
)
Home
Index