Nuprl Lemma : remainder_wf

[a:ℕ]. ∀[n:ℕ+].  (a rem n ∈ ℕ)


Proof




Definitions occuring in Statement :  nat_plus: + nat: uall: [x:A]. B[x] member: t ∈ T remainder: rem m
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: subtype_rel: A ⊆B and: P ∧ Q
Lemmas referenced :  remainder_wfa nat_plus_inc_int_nzero rem_bounds_1 istype-le nat_plus_wf istype-nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut Error :dependent_set_memberEquality_alt,  extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis applyEquality sqequalRule productElimination natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry Error :universeIsType,  Error :isect_memberEquality_alt,  Error :isectIsTypeImplies,  Error :inhabitedIsType

Latex:
\mforall{}[a:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    (a  rem  n  \mmember{}  \mBbbN{})



Date html generated: 2019_06_20-PM-02_12_29
Last ObjectModification: 2019_06_20-PM-02_08_52

Theory : int_2


Home Index