Step * of Lemma mul-associates

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

1
.....assertion..... 
x,y,z:ℤ.  (((x y) z) (x z) ∈ ℤ)

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


Latex:


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


By


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




Home Index