---

Step * of Lemma div_absval_bound

∀[M:ℕ+]. ∀[z:ℤ]. ∀[n:ℕ].  |z ÷ M| ≤ n supposing |z| ≤ (n * M)
BY
{ (Auto
   THEN (CaseNat 0 `n'
         THENL [((Assert |z| ≤ 0 BY
                        Auto)
                 THEN (RWO "absval_le_zero" (-1) THENA Auto)
                 THEN HypSubst' (-1) 0
                 THEN Subst' 0 ÷ M ~ 0 0
                 THEN Auto)
               ; ((Assert 1 ≤ n BY Auto) THEN Mul ⌜M⌝ (-1)⋅)]
        )
   ) }

1
1. M : ℕ+
2. z : ℤ
3. n : ℕ
4. |z| ≤ (n * M)
5. ¬(n = 0 ∈ ℤ)
6. 1 ≤ n
7. (M * 1) ≤ (M * n)
⊢ |z ÷ M| ≤ n

---

Latex:

---

Latex:
\mforall{}[M:\mBbbN{}\msupplus{}].  \mforall{}[z:\mBbbZ{}].  \mforall{}[n:\mBbbN{}].    |z  \mdiv{}  M|  \mleq{}  n  supposing  |z|  \mleq{}  (n  *  M)


By

---

Latex:
(Auto
  THEN  (CaseNat  0  `n'
              THENL  [((Assert  |z|  \mleq{}  0  BY
                                            Auto)
                              THEN  (RWO  "absval\_le\_zero"  (-1)  THENA  Auto)
                              THEN  HypSubst'  (-1)  0
                              THEN  Subst'  0  \mdiv{}  M  \msim{}  0  0
                              THEN  Auto)
                          ;  ((Assert  1  \mleq{}  n  BY  Auto)  THEN  Mul  \mkleeneopen{}M\mkleeneclose{}  (-1)\mcdot{})]
            )
  )

---

Home Index