Step * 1 1 1 of Lemma modulus_base_neg


1. : ℕ+
2. {-m..0-}
3. (0 ≥ (a rem m) ) ∧ ((a rem m) > (-m))
4. 0 ≤ 0
5. ((0 m) (a rem m)) ∈ ℤ
6. (a ÷ m) 0 ∈ ℤ
⊢ if (a rem m) < (0)  then (a rem m)  else (a rem m) (m a) ∈ ℕ
BY
AutoSplit }


Latex:


Latex:

1.  m  :  \mBbbN{}\msupplus{}
2.  a  :  \{-m..0\msupminus{}\}
3.  (0  \mgeq{}  (a  rem  m)  )  \mwedge{}  ((a  rem  m)  >  (-m))
4.  0  \mleq{}  0
5.  a  =  ((0  *  m)  +  (a  rem  m))
6.  (a  \mdiv{}  m)  =  0
\mvdash{}  if  (a  rem  m)  <  (0)    then  m  +  (a  rem  m)    else  (a  rem  m)  =  (m  +  a)


By


Latex:
AutoSplit




Home Index