---

Step * 2 1 1 1 1 1 of Lemma close-reals-iff


1. k : ℕ+
2. n : ℕ+
3. v : ℤ
4. (|v| * k) ≤ ((4 * k) + (2 * 4 * n))
⊢ (4 * |v ÷ 4|) ≤ (4 * (((2 * n * 1) ÷ k) + 4))
BY
{ (Assert (4 * |v ÷ 4|) ≤ (|v| + 3) BY
         ((InstLemma `div_rem_sum` [⌜v⌝;⌜4⌝]⋅ THENA Auto)
          THEN (Assert |(v ÷ 4) * 4| = |v - v rem 4| ∈ ℤ BY
                      (EqCD THEN Auto))
          THEN (RWO "absval_mul" (-1) THENA Auto)
          THEN (Subst' |4| ~ 4 -1 THENA Auto)
          THEN ((Assert |v - v rem 4| ≤ (|v| + 3) BY
                       ((InstLemma `int-triangle-inequality` [⌜v⌝;⌜-(v rem 4)⌝]⋅ THENA Auto)
                        THEN (RWO "absval-minus" (-1) THENA Auto)
                        THEN ((Assert |v rem 4| ≤ 3 BY
                                     ((InstLemma `rem_bounds_z` [⌜v⌝;⌜4⌝]⋅ THENA Auto)
                                      THEN Subst' |4| ~ 4 -1
                                      THEN Auto))
                        THENM ((RWO "-1" (-2) THENA Auto) THEN NthHypSq (-2) THEN Auto)
                        )))
          THENM Auto
          ))) }

1
1. k : ℕ+
2. n : ℕ+
3. v : ℤ
4. (|v| * k) ≤ ((4 * k) + (2 * 4 * n))
5. (4 * |v ÷ 4|) ≤ (|v| + 3)
⊢ (4 * |v ÷ 4|) ≤ (4 * (((2 * n * 1) ÷ k) + 4))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  n  :  \mBbbN{}\msupplus{}
3.  v  :  \mBbbZ{}
4.  (|v|  *  k)  \mleq{}  ((4  *  k)  +  (2  *  4  *  n))
\mvdash{}  (4  *  |v  \mdiv{}  4|)  \mleq{}  (4  *  (((2  *  n  *  1)  \mdiv{}  k)  +  4))


By

---

Latex:
(Assert  (4  *  |v  \mdiv{}  4|)  \mleq{}  (|v|  +  3)  BY
              ((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}4\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (Assert  |(v  \mdiv{}  4)  *  4|  =  |v  -  v  rem  4|  BY
                                        (EqCD  THEN  Auto))
                THEN  (RWO  "absval\_mul"  (-1)  THENA  Auto)
                THEN  (Subst'  |4|  \msim{}  4  -1  THENA  Auto)
                THEN  ((Assert  |v  -  v  rem  4|  \mleq{}  (|v|  +  3)  BY
                                          ((InstLemma  `int-triangle-inequality`  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}-(v  rem  4)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                            THEN  (RWO  "absval-minus"  (-1)  THENA  Auto)
                                            THEN  ((Assert  |v  rem  4|  \mleq{}  3  BY
                                                                      ((InstLemma  `rem\_bounds\_z`  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}4\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                                                        THEN  Subst'  |4|  \msim{}  4  -1
                                                                        THEN  Auto))
                                            THENM  ((RWO  "-1"  (-2)  THENA  Auto)  THEN  NthHypSq  (-2)  THEN  Auto)
                                            )))
                THENM  Auto
                )))

---

Home Index