---

Step * of Lemma mul-distributes

∀[x,y,z:Top].  (x * (y + z) ~ (x * y) + (x * z))
BY
{ TACTIC:Assert ⌜∀x,y,z:ℤ.  ((x * (y + z)) = ((x * y) + (x * z)) ∈ ℤ)⌝⋅ }

1
.....assertion..... 
∀x,y,z:ℤ.  ((x * (y + z)) = ((x * y) + (x * z)) ∈ ℤ)

2
1. ∀x,y,z:ℤ.  ((x * (y + z)) = ((x * y) + (x * z)) ∈ ℤ)
⊢ ∀[x,y,z:Top].  (x * (y + z) ~ (x * y) + (x * z))

---

Latex:

---

Latex:
\mforall{}[x,y,z:Top].    (x  *  (y  +  z)  \msim{}  (x  *  y)  +  (x  *  z))


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}x,y,z:\mBbbZ{}.    ((x  *  (y  +  z))  =  ((x  *  y)  +  (x  *  z)))\mkleeneclose{}\mcdot{}

---

Home Index