Nuprl Rule : remainderBounds2
H  ⊢ if (-b) < (a rem b)  then True  else False
  BY remainderBounds2 ()
  
  H  ⊢ if (a) < (0)  then True  else False
  H  ⊢ if (0) < (b)  then True  else False
  H  ⊢ a ∈ ℤ
  H  ⊢ b ∈ ℤ
Definitions occuring in rule : 
minus: -n
, 
remainder: n rem m
, 
less: if (a) < (b)  then c  else d
, 
natural_number: $n
, 
true: True
, 
false: False
, 
member: t ∈ T
, 
int: ℤ
, 
axiom: Ax
Latex:
H    \mvdash{}  if  (-b)  <  (a  rem  b)    then  True    else  False
    BY  remainderBounds2  ()
   
    H    \mvdash{}  if  (a)  <  (0)    then  True    else  False
    H    \mvdash{}  if  (0)  <  (b)    then  True    else  False
    H    \mvdash{}  a  \mmember{}  \mBbbZ{}
    H    \mvdash{}  b  \mmember{}  \mBbbZ{}
Date html generated:
2019_06_20-PM-04_12_23
Last ObjectModification:
2018_08_20-AM-11_34_06
Theory : rules
Home
Index