Nuprl Lemma : mul-assoced-one

x,y:ℤ.  (((x y) 1)  (x 1))


Proof




Definitions occuring in Statement :  assoced: b all: x:A. B[x] implies:  Q multiply: m natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q assoced: b and: P ∧ Q cand: c∧ B member: t ∈ T prop: uall: [x:A]. B[x] divides: a exists: x:A. B[x] guard: {T}
Lemmas referenced :  one_divs_any assoced_wf equal_wf divides_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin cut independent_pairFormation hypothesis lemma_by_obid dependent_functionElimination hypothesisEquality isectElimination multiplyEquality natural_numberEquality intEquality dependent_pairFormation independent_functionElimination

Latex:
\mforall{}x,y:\mBbbZ{}.    (((x  *  y)  \msim{}  1)  {}\mRightarrow{}  (x  \msim{}  1))



Date html generated: 2018_05_21-PM-01_05_57
Last ObjectModification: 2018_01_28-PM-02_02_05

Theory : num_thy_1


Home Index