---

Step * 1 of Lemma rroot-regularity-lemma

.....assertion..... 
∀[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))))
BY
{ Auto }

1
1. k : {2...}
2. n : ℕ+
3. m : ℕ+
4. a : ℤ
5. b : ℤ
6. c : ℤ
7. d : ℤ
8. a ≤ b
9. (m ≤ a) ∨ ((a = 0 ∈ ℤ) ∧ (c = 0 ∈ ℤ))
10. (n ≤ b) ∨ ((b = 0 ∈ ℤ) ∧ (d = 0 ∈ ℤ))
11. a^k ≤ c
12. c < a + m^k
13. b^k ≤ d
14. d < b + n^k
15. |c - d| ≤ (2^k * (n^k + m^k))
⊢ |a - b| ≤ (2 * (n + m))

---

Latex:

---

Latex:
.....assertion..... 
\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))))


By

---

Latex:
Auto

---

Home Index