---

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

.....assertion..... 
1. k : {2...}
2. n : ℕ+
3. m : ℕ+
4. a : ℤ
5. b : ℤ
6. c : ℤ
7. d : ℤ
8. a ≤ b
9. m ≤ a
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
17. ((2 * n) + m) + a + m^k < b^k
⊢ ((2 * n) + (3 * m)^k - 2 * m^k) + c < ((2 * n) + m) + a + m^k
BY
{ ((Subst' (2 * n) + (3 * m) ~ ((2 * n) + m) + (2 * m) 0 THENA Auto)
   THEN (RWO "binomial-int" 0 THENA Auto)
   THEN (RW (AddrC [2] (LemmaC `sum_split_first`)) 0 THENA Auto)
   THEN Reduce 0
   THEN (Subst' choose(k;0) ~ 1 0 THENA (RecUnfold `choose` 0 THEN Reduce 0 THEN Auto))
   THEN (Subst' k - 0 ~ k 0 THENA Auto)) }

1
1. k : {2...}
2. n : ℕ+
3. m : ℕ+
4. a : ℤ
5. b : ℤ
6. c : ℤ
7. d : ℤ
8. a ≤ b
9. m ≤ a
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
17. ((2 * n) + m) + a + m^k < b^k
⊢ (Σ(choose(k;i) * (2 * n) + m^i * 2 * m^k - i | i < k + 1) - 2 * m^k) + c < (1 * 1 * a + m^k)
+ Σ(choose(k;i + 1) * (2 * n) + m^i + 1 * a + m^k - i + 1 | i < (k + 1) - 1)

---

Latex:

---

Latex:
.....assertion..... 
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
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))
16.  ((2  *  n)  +  m)  +  a  +  m  <  b
17.  ((2  *  n)  +  m)  +  a  +  m\^{}k  <  b\^{}k
\mvdash{}  ((2  *  n)  +  (3  *  m)\^{}k  -  2  *  m\^{}k)  +  c  <  ((2  *  n)  +  m)  +  a  +  m\^{}k


By

---

Latex:
((Subst'  (2  *  n)  +  (3  *  m)  \msim{}  ((2  *  n)  +  m)  +  (2  *  m)  0  THENA  Auto)
  THEN  (RWO  "binomial-int"  0  THENA  Auto)
  THEN  (RW  (AddrC  [2]  (LemmaC  `sum\_split\_first`))  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst'  choose(k;0)  \msim{}  1  0  THENA  (RecUnfold  `choose`  0  THEN  Reduce  0  THEN  Auto))
  THEN  (Subst'  k  -  0  \msim{}  k  0  THENA  Auto))

---

Home Index