Step * 1 1 1 1 1 1 1 of Lemma rroot-abs-property


1. {2...}
2. i ≠ 0
3. {2...}
4. : ℕ+
5. : ℕ
6. 2^(i 1) b ∈ ℕ
7. : ℕ+
8. n^i k ∈ ℕ+
9. : ℕ
10. : ℕ
11. |(n A) B| ≤ (2 (k n))
12. : ℕ
13. R^i ≤ (b A)
14. A < (R 1)^i
15. |R| ≤ ((2 n) C)
⊢ |(R^i ÷ n^i 1) B| ≤ ((i C^(i 1)) 5)
BY
((RWO "exp-fastexp<THENA Auto)
   THEN (Assert 0 < (2 n)^(i 1) BY
               (BLemma `exp-positive` THEN Auto))
   THEN (Assert ⌜|k| k⌝⋅ THENA ((RWO  "absval_unfold" THENA Auto) THEN AutoSplit))
   THEN Mul ⌜k⌝ 0⋅
   THEN RevHypSubst' (-1) 0
   THEN (RWO "absval_mul<THENA Auto)) }

1
1. {2...}
2. i ≠ 0
3. {2...}
4. : ℕ+
5. : ℕ
6. 2^(i 1) b ∈ ℕ
7. : ℕ+
8. n^i k ∈ ℕ+
9. : ℕ
10. : ℕ
11. |(n A) B| ≤ (2 (k n))
12. : ℕ
13. R^i ≤ (b A)
14. A < (R 1)^i
15. |R| ≤ ((2 n) C)
16. 0 < (2 n)^(i 1)
17. |k| k
⊢ |k ((R^i ÷ (2 n)^(i 1)) B)| ≤ (|k| ((i C^(i 1)) 5))


Latex:


Latex:

1.  i  :  \{2...\}
2.  i  \mneq{}  0
3.  C  :  \{2...\}
4.  n  :  \mBbbN{}\msupplus{}
5.  b  :  \mBbbN{}
6.  2\^{}(i  -  1)  =  b
7.  k  :  \mBbbN{}\msupplus{}
8.  n\^{}i  =  k
9.  A  :  \mBbbN{}
10.  B  :  \mBbbN{}
11.  |(n  *  A)  -  k  *  B|  \mleq{}  (2  *  (k  +  n))
12.  R  :  \mBbbN{}
13.  R\^{}i  \mleq{}  (b  *  A)
14.  b  *  A  <  (R  +  1)\^{}i
15.  |R|  \mleq{}  ((2  *  n)  *  C)
\mvdash{}  |(R\^{}i  \mdiv{}  2  *  n\^{}i  -  1)  -  B|  \mleq{}  ((i  *  b  *  C\^{}(i  -  1))  +  5)


By


Latex:
((RWO  "exp-fastexp<"  0  THENA  Auto)
  THEN  (Assert  0  <  (2  *  n)\^{}(i  -  1)  BY
                          (BLemma  `exp-positive`  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}|k|  \msim{}  k\mkleeneclose{}\mcdot{}  THENA  ((RWO    "absval\_unfold"  0  THENA  Auto)  THEN  AutoSplit))
  THEN  Mul  \mkleeneopen{}k\mkleeneclose{}  0\mcdot{}
  THEN  RevHypSubst'  (-1)  0
  THEN  (RWO  "absval\_mul<"  0  THENA  Auto))




Home Index