---

Step * 2 1 1 1 of Lemma rroot-abs_wf


1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
5. n : ℕ+
6. m : ℕ+
7. k : ℕ+
8. n^i = k ∈ ℕ+
9. j : ℕ+
10. m^i = j ∈ ℕ+
11. 0 ≤ (|x| k)
12. 0 ≤ (|x| j)
⊢ |(m * iroot(i;b * (|x| k))) - n * iroot(i;b * (|x| j))| ≤ (2 * (n + m))
BY
{ TACTIC:(InstLemma `rroot-regularity-lemma` 
          [⌜i⌝;⌜n⌝;⌜m⌝
          ;⌜m * iroot(i;b * (|x| k))⌝
          ;⌜n * iroot(i;b * (|x| j))⌝
          ; ⌜j * b * (|x| k)⌝
          ; ⌜k * b * (|x| j)⌝
          ]⋅
          THEN Auto
          ) }

1
.....antecedent..... 
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
5. n : ℕ+
6. m : ℕ+
7. k : ℕ+
8. n^i = k ∈ ℕ+
9. j : ℕ+
10. m^i = j ∈ ℕ+
11. 0 ≤ (|x| k)
12. 0 ≤ (|x| j)
⊢ (m ≤ (m * iroot(i;b * (|x| k)))) ∨ (((m * iroot(i;b * (|x| k))) = 0 ∈ ℤ) ∧ ((j * b * (|x| k)) = 0 ∈ ℤ))

2
.....antecedent..... 
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
5. n : ℕ+
6. m : ℕ+
7. k : ℕ+
8. n^i = k ∈ ℕ+
9. j : ℕ+
10. m^i = j ∈ ℕ+
11. 0 ≤ (|x| k)
12. 0 ≤ (|x| j)
⊢ (n ≤ (n * iroot(i;b * (|x| j)))) ∨ (((n * iroot(i;b * (|x| j))) = 0 ∈ ℤ) ∧ ((k * b * (|x| j)) = 0 ∈ ℤ))

3
.....antecedent..... 
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
5. n : ℕ+
6. m : ℕ+
7. k : ℕ+
8. n^i = k ∈ ℕ+
9. j : ℕ+
10. m^i = j ∈ ℕ+
11. 0 ≤ (|x| k)
12. 0 ≤ (|x| j)
⊢ (m * iroot(i;b * (|x| k)))^i ≤ (j * b * (|x| k))

4
.....antecedent..... 
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
5. n : ℕ+
6. m : ℕ+
7. k : ℕ+
8. n^i = k ∈ ℕ+
9. j : ℕ+
10. m^i = j ∈ ℕ+
11. 0 ≤ (|x| k)
12. 0 ≤ (|x| j)
⊢ j * b * (|x| k) < ((m * iroot(i;b * (|x| k))) + m)^i

5
.....antecedent..... 
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
5. n : ℕ+
6. m : ℕ+
7. k : ℕ+
8. n^i = k ∈ ℕ+
9. j : ℕ+
10. m^i = j ∈ ℕ+
11. 0 ≤ (|x| k)
12. 0 ≤ (|x| j)
⊢ (n * iroot(i;b * (|x| j)))^i ≤ (k * b * (|x| j))

6
.....antecedent..... 
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
5. n : ℕ+
6. m : ℕ+
7. k : ℕ+
8. n^i = k ∈ ℕ+
9. j : ℕ+
10. m^i = j ∈ ℕ+
11. 0 ≤ (|x| k)
12. 0 ≤ (|x| j)
⊢ k * b * (|x| j) < ((n * iroot(i;b * (|x| j))) + n)^i

7
.....antecedent..... 
1. i : {2...}
2. x : ℝ
3. b : ℕ
4. 2^(i - 1) = b ∈ ℕ
5. n : ℕ+
6. m : ℕ+
7. k : ℕ+
8. n^i = k ∈ ℕ+
9. j : ℕ+
10. m^i = j ∈ ℕ+
11. 0 ≤ (|x| k)
12. 0 ≤ (|x| j)
⊢ |(j * b * (|x| k)) - k * b * (|x| j)| ≤ (2^i * (n^i + m^i))

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  x  :  \mBbbR{}
3.  b  :  \mBbbN{}
4.  2\^{}(i  -  1)  =  b
5.  n  :  \mBbbN{}\msupplus{}
6.  m  :  \mBbbN{}\msupplus{}
7.  k  :  \mBbbN{}\msupplus{}
8.  n\^{}i  =  k
9.  j  :  \mBbbN{}\msupplus{}
10.  m\^{}i  =  j
11.  0  \mleq{}  (|x|  k)
12.  0  \mleq{}  (|x|  j)
\mvdash{}  |(m  *  iroot(i;b  *  (|x|  k)))  -  n  *  iroot(i;b  *  (|x|  j))|  \mleq{}  (2  *  (n  +  m))


By

---

Latex:
TACTIC:(InstLemma  `rroot-regularity-lemma` 
                [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}
                ;\mkleeneopen{}m  *  iroot(i;b  *  (|x|  k))\mkleeneclose{}
                ;\mkleeneopen{}n  *  iroot(i;b  *  (|x|  j))\mkleeneclose{}
                ;  \mkleeneopen{}j  *  b  *  (|x|  k)\mkleeneclose{}
                ;  \mkleeneopen{}k  *  b  *  (|x|  j)\mkleeneclose{}
                ]\mcdot{}
                THEN  Auto
                )

---

Home Index