---

Step * 1 2 1 of Lemma modulus_base_neg


1. m : ℕ+
2. a : {-m..0-}
3. (0 ≥ (a rem m) ) ∧ ((a rem m) > (-m))
4. (a ÷ m) ≤ 0
5. a = (((a ÷ m) * m) + (a rem m)) ∈ ℤ
6. ¬((a ÷ m) = 0 ∈ ℤ)
7. (a ÷ m) ≤ (-1)
⊢ if (a rem m) < (0)  then m + (a rem m)  else (a rem m) = (m + a) ∈ ℕ
BY
{ (Mul ⌜m⌝ (-1)⋅ THENA Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Mul  \mkleeneopen{}m\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)

---

Home Index