---

Step * 1 of Lemma two-mul

.....assertion..... 
∀[x:ℤ]. (x + x ~ 2 * x)
BY
{ ((UnivCD THENA Auto) THEN Subst' 2 ~ 1 + 1 0) }

1
.....equality..... 
1. x : ℤ
⊢ 2 ~ 1 + 1

2
1. x : ℤ
⊢ x + x ~ (1 + 1) * x

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}[x:\mBbbZ{}].  (x  +  x  \msim{}  2  *  x)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Subst'  2  \msim{}  1  +  1  0)

---

Home Index