---

Step * 1 1 1 of Lemma rroot-regularity-lemma


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))
⊢ (b - a) ≤ (2 * (n + m))
BY
{ ( Decide ⌜((2 * n) + m) + a + m < b⌝⋅ THENA 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))
16. ((2 * n) + m) + a + m < b
⊢ (b - a) ≤ (2 * (n + m))

2
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))
16. ¬((2 * n) + m) + a + m < b
⊢ (b - a) ≤ (2 * (n + m))

---

Latex:

---

Latex:

1.  k  :  \{2...\}
2.  n  :  \mBbbN{}\msupplus{}
3.  m  :  \mBbbN{}\msupplus{}
4.  a  :  \mBbbZ{}
5.  b  :  \mBbbZ{}
6.  c  :  \mBbbZ{}
7.  d  :  \mBbbZ{}
8.  a  \mleq{}  b
9.  (m  \mleq{}  a)  \mvee{}  ((a  =  0)  \mwedge{}  (c  =  0))
10.  (n  \mleq{}  b)  \mvee{}  ((b  =  0)  \mwedge{}  (d  =  0))
11.  a\^{}k  \mleq{}  c
12.  c  <  a  +  m\^{}k
13.  b\^{}k  \mleq{}  d
14.  d  <  b  +  n\^{}k
15.  |c  -  d|  \mleq{}  (2\^{}k  *  (n\^{}k  +  m\^{}k))
\mvdash{}  (b  -  a)  \mleq{}  (2  *  (n  +  m))


By

---

Latex:
(  Decide  \mkleeneopen{}((2  *  n)  +  m)  +  a  +  m  <  b\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index