---

Step * 1 of Lemma rroot-odd-2-regular


1. b : ℕ
2. i : {2...}
3. x : ℝ
4. n : ℕ+
5. m : ℕ+
6. |(m * eval k = n^i in eval z = |x| k in   iroot(i;b * z)) - n * eval k = m^i in eval z = |x| k in   iroot(i;b * z)| 
   ≤ (2 * (n + m))
7. 2^(i - 1) = b ∈ ℕ
⊢ |(m * eval k = n^i in eval z = x k in   if z <z 0 then -iroot(i;b * (-z)) else iroot(i;b * z) fi ) - n
  * eval k = m^i in
    eval z = x k in
      if z <z 0 then -iroot(i;b * (-z)) else iroot(i;b * z) fi | ≤ (4 * (n + m))
BY
{ (((GenConcl ⌜n^i = k ∈ ℕ+⌝⋅
     THENA (Auto THEN (InstLemma `exp_preserves_lt` [⌜i⌝;⌜0⌝;⌜n⌝]⋅ THENA Auto) THEN RWO "exp-zero" (-1) THEN Auto)
     )
    THEN PromoteHyp (-2) 1
    THEN HypSubst' (-1) (-3)
    THEN (GenConcl ⌜m^i = j ∈ ℕ+⌝⋅
          THENA (Auto THEN (InstLemma `exp_preserves_lt` [⌜i⌝;⌜0⌝;⌜m⌝]⋅ THENA Auto) THEN RWO "exp-zero" (-1) THEN Auto)
          )
    THEN PromoteHyp (-2) 1
    THEN HypSubst' (-1) (-4))
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN RepeatFor 2 ((CallByValueReduce (-4) THENA Auto))) }

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

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}
2.  i  :  \{2...\}
3.  x  :  \mBbbR{}
4.  n  :  \mBbbN{}\msupplus{}
5.  m  :  \mBbbN{}\msupplus{}
6.  |(m  *  eval  k  =  n\^{}i  in  eval  z  =  |x|  k  in      iroot(i;b  *  z))  -  n
      *  eval  k  =  m\^{}i  in
          eval  z  =  |x|  k  in
              iroot(i;b  *  z)|  \mleq{}  (2  *  (n  +  m))
7.  2\^{}(i  -  1)  =  b
\mvdash{}  |(m
    *  eval  k  =  n\^{}i  in
        eval  z  =  x  k  in
            if  z  <z  0  then  -iroot(i;b  *  (-z))  else  iroot(i;b  *  z)  fi  )  -  n
    *  eval  k  =  m\^{}i  in
        eval  z  =  x  k  in
            if  z  <z  0  then  -iroot(i;b  *  (-z))  else  iroot(i;b  *  z)  fi  |  \mleq{}  (4  *  (n  +  m))


By

---

Latex:
(((GenConcl  \mkleeneopen{}n\^{}i  =  k\mkleeneclose{}\mcdot{}
      THENA  (Auto
                    THEN  (InstLemma  `exp\_preserves\_lt`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                    THEN  RWO  "exp-zero"  (-1)
                    THEN  Auto)
      )
    THEN  PromoteHyp  (-2)  1
    THEN  HypSubst'  (-1)  (-3)
    THEN  (GenConcl  \mkleeneopen{}m\^{}i  =  j\mkleeneclose{}\mcdot{}
                THENA  (Auto
                              THEN  (InstLemma  `exp\_preserves\_lt`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  RWO  "exp-zero"  (-1)
                              THEN  Auto)
                )
    THEN  PromoteHyp  (-2)  1
    THEN  HypSubst'  (-1)  (-4))
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  RepeatFor  2  ((CallByValueReduce  (-4)  THENA  Auto)))

---

Home Index