Nuprl Lemma : div_rem_sum

[a:ℤ]. ∀[n:ℤ-o].  (a (((a ÷ n) n) (a rem n)) ∈ ℤ)


Proof




Definitions occuring in Statement :  int_nzero: -o uall: [x:A]. B[x] remainder: rem m divide: n ÷ m multiply: m add: m 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:
Lemmas referenced :  int_nzero_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality axiomEquality because_Cache intEquality divideRemainderSum setElimination rename lambdaFormation independent_functionElimination voidElimination natural_numberEquality

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (a  =  (((a  \mdiv{}  n)  *  n)  +  (a  rem  n)))



Date html generated: 2016_05_13-PM-03_33_17
Last ObjectModification: 2015_12_26-AM-09_44_45

Theory : arithmetic


Home Index