Nuprl Rule : divideRemainderSum

H  ⊢ a = (((a ÷ b) * b) + (a rem b)) ∈ ℤ

  BY divideRemainderSum ()
  
  H  ⊢ if b=0 then False else True
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ


Definitions occuring in rule :  equal: s = t ∈ T,  add: n + m,  multiply: n * m,  divide: n ÷ m,  remainder: n rem m,  int_eq: if a=b then c else d,  natural_number: $n,  false: False,  true: True,  member: t ∈ T,  int: ℤ,  axiom: Ax
Latex:
H    \mvdash{}  a  =  (((a  \mdiv{}  b)  *  b)  +  (a  rem  b))

    BY  divideRemainderSum  ()
   
    H    \mvdash{}  if  b=0  then  False  else  True
    H    \mvdash{}  a  \mmember{}  \mBbbZ{}
    H    \mvdash{}  b  \mmember{}  \mBbbZ{}


Date html generated: 2019_06_20-PM-04_12_24
Last ObjectModification: 2018_09_08-AM-08_14_55

Theory : rules


Home Index