---

Step * 2 of Lemma rroot-regularity-lemma


1. ∀[k:{2...}]. ∀[n,m:ℕ+]. ∀[a,b,c,d:ℤ].
     ((a ≤ b)
     ⇒ ((m ≤ a) ∨ ((a = 0 ∈ ℤ) ∧ (c = 0 ∈ ℤ)))
     ⇒ ((n ≤ b) ∨ ((b = 0 ∈ ℤ) ∧ (d = 0 ∈ ℤ)))
     ⇒ (a^k ≤ c)
     ⇒ c < a + m^k
     ⇒ (b^k ≤ d)
     ⇒ d < b + n^k
     ⇒ (|c - d| ≤ (2^k * (n^k + m^k)))
     ⇒ (|a - b| ≤ (2 * (n + m))))
⊢ ∀[k:{2...}]. ∀[n,m:ℕ+]. ∀[a,b,c,d:ℤ].
    (((m ≤ a) ∨ ((a = 0 ∈ ℤ) ∧ (c = 0 ∈ ℤ)))
    ⇒ ((n ≤ b) ∨ ((b = 0 ∈ ℤ) ∧ (d = 0 ∈ ℤ)))
    ⇒ (a^k ≤ c)
    ⇒ c < a + m^k
    ⇒ (b^k ≤ d)
    ⇒ d < b + n^k
    ⇒ (|c - d| ≤ (2^k * (n^k + m^k)))
    ⇒ (|a - b| ≤ (2 * (n + m))))
BY
{ (Auto
   THEN Decide ⌜a ≤ b⌝⋅
   THEN Auto
   THEN (InstHyp [⌜k⌝;⌜m⌝;⌜n⌝;⌜b⌝;⌜a⌝;⌜d⌝;⌜c⌝] 1⋅ THENA Auto)
   THEN RWO "absval-diff-symmetry" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}[k:\{2...\}].  \mforall{}[n,m:\mBbbN{}\msupplus{}].  \mforall{}[a,b,c,d:\mBbbZ{}].
          ((a  \mleq{}  b)
          {}\mRightarrow{}  ((m  \mleq{}  a)  \mvee{}  ((a  =  0)  \mwedge{}  (c  =  0)))
          {}\mRightarrow{}  ((n  \mleq{}  b)  \mvee{}  ((b  =  0)  \mwedge{}  (d  =  0)))
          {}\mRightarrow{}  (a\^{}k  \mleq{}  c)
          {}\mRightarrow{}  c  <  a  +  m\^{}k
          {}\mRightarrow{}  (b\^{}k  \mleq{}  d)
          {}\mRightarrow{}  d  <  b  +  n\^{}k
          {}\mRightarrow{}  (|c  -  d|  \mleq{}  (2\^{}k  *  (n\^{}k  +  m\^{}k)))
          {}\mRightarrow{}  (|a  -  b|  \mleq{}  (2  *  (n  +  m))))
\mvdash{}  \mforall{}[k:\{2...\}].  \mforall{}[n,m:\mBbbN{}\msupplus{}].  \mforall{}[a,b,c,d:\mBbbZ{}].
        (((m  \mleq{}  a)  \mvee{}  ((a  =  0)  \mwedge{}  (c  =  0)))
        {}\mRightarrow{}  ((n  \mleq{}  b)  \mvee{}  ((b  =  0)  \mwedge{}  (d  =  0)))
        {}\mRightarrow{}  (a\^{}k  \mleq{}  c)
        {}\mRightarrow{}  c  <  a  +  m\^{}k
        {}\mRightarrow{}  (b\^{}k  \mleq{}  d)
        {}\mRightarrow{}  d  <  b  +  n\^{}k
        {}\mRightarrow{}  (|c  -  d|  \mleq{}  (2\^{}k  *  (n\^{}k  +  m\^{}k)))
        {}\mRightarrow{}  (|a  -  b|  \mleq{}  (2  *  (n  +  m))))


By

---

Latex:
(Auto
  THEN  Decide  \mkleeneopen{}a  \mleq{}  b\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  1\mcdot{}  THENA  Auto)
  THEN  RWO  "absval-diff-symmetry"  0
  THEN  Auto)

---

Home Index