### Nuprl Lemma : rem-exact

[g:ℤ-o]. ∀[v:ℤ].  ((g rem g) 0 ∈ ℤ)

Proof

Definitions occuring in Statement :  int_nzero: -o uall: [x:A]. B[x] remainder: rem m multiply: m natural_number: \$n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int_nzero: -o nequal: a ≠ b ∈  not: ¬A implies:  Q false: False prop: true: True top: Top squash: T uimplies: supposing a subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin multiplyEquality setElimination rename hypothesisEquality hypothesis intEquality sqequalRule isect_memberEquality axiomEquality because_Cache divideEquality equalityTransitivity equalitySymmetry lambdaFormation independent_functionElimination voidElimination natural_numberEquality remainderEquality addEquality voidEquality minusEquality applyEquality lambdaEquality imageElimination universeEquality independent_isectElimination imageMemberEquality baseClosed productElimination

Latex:
\mforall{}[g:\mBbbZ{}\msupminus{}\msupzero{}].  \mforall{}[v:\mBbbZ{}].    ((g  *  v  rem  g)  =  0)

Date html generated: 2017_04_14-AM-07_20_11
Last ObjectModification: 2017_02_27-PM-02_53_43

Theory : arithmetic

Home Index