---

Step * of Lemma small-eqmod-odd

∀m:ℕ+. ((↑isOdd(m)) ⇒ (∀a:ℤ. ∃b:ℤ. (2 * |b| < m ∧ (b ≡ a mod m))))
BY
{ (Auto
   THEN (InstLemma `small-eqmod` [⌜m⌝;⌜a⌝]⋅ THENA Auto)
   THEN ParallelLast
   THEN Auto
   THEN SupposeNot
   THEN (Assert m = (2 * |b|) ∈ ℤ BY
               Auto)
   THEN ((FLemma `odd-implies` [2] THENM (ExRepD THEN D -2)) THENA Auto)
   THEN HypSubst' (-3) 0) }

1
1. m : ℕ+
2. ↑isOdd(m)
3. a : ℤ
4. b : ℤ
5. (2 * |b|) ≤ m
6. b ≡ a mod m
7. ¬2 * |b| < m
8. m = (2 * |b|) ∈ ℤ
9. ↑isEven(m - 1)
10. ↑isEven(m + 1)
⊢ ↑isEven(2 * |b|)

---

Latex:

---

Latex:
\mforall{}m:\mBbbN{}\msupplus{}.  ((\muparrow{}isOdd(m))  {}\mRightarrow{}  (\mforall{}a:\mBbbZ{}.  \mexists{}b:\mBbbZ{}.  (2  *  |b|  <  m  \mwedge{}  (b  \mequiv{}  a  mod  m))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `small-eqmod`  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto
  THEN  SupposeNot
  THEN  (Assert  m  =  (2  *  |b|)  BY
                          Auto)
  THEN  ((FLemma  `odd-implies`  [2]  THENM  (ExRepD  THEN  D  -2))  THENA  Auto)
  THEN  HypSubst'  (-3)  0)

---

Home Index