---

Step * 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)) ∈ ℤ
⊢ if (a rem m) < (0)  then m + (a rem m)  else (a rem m) = (m + a) ∈ ℕ
BY
{ (Decide ⌜(a ÷ m) = 0 ∈ ℤ⌝⋅ 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 ∈ ℤ
⊢ if (a rem m) < (0)  then m + (a rem m)  else (a rem m) = (m + a) ∈ ℕ

2
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 ∈ ℤ)
⊢ 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))
\mvdash{}  if  (a  rem  m)  <  (0)    then  m  +  (a  rem  m)    else  (a  rem  m)  =  (m  +  a)


By

---

Latex:
(Decide  \mkleeneopen{}(a  \mdiv{}  m)  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index