---

Step * 1 of Lemma poly-approx-property


1. k : ℕ
2. a : ℕ ⟶ ℝ
3. x : ℝ
4. ∀[xM:ℤ]. ∀[M:ℕ+]. ∀[n:ℕ].
     ((|x| ≤ (r1/r(4)))
     ⇒ 1-approx(x;M;xM)
     ⇒ k + 1-approx(Σ{(a (n + i)) * x^i | 0≤i≤k};M;poly-approx-aux(a;x;xM;M;n;k)))
5. N : ℕ+
6. |x| ≤ (r1/r(4))
7. B : ℕ+
8. (2 * (k + 1)) = B ∈ ℕ+
9. M : ℕ+
10. (B * N) = M ∈ ℕ+
11. xM : ℤ
12. (x M) = xM ∈ ℤ
13. 1-approx(x;M;xM)
⊢ 1-approx(Σ{(a i) * x^i | 0≤i≤k};N;eval z = poly-approx-aux(a;x;xM;M;0;k) in
                                    z ÷ B)
BY
{ ((InstHyp [⌜xM⌝;⌜M⌝;⌜0⌝] 4⋅ THENA Auto)
   THEN (Assert Σ{(a (0 + i)) * x^i | 0≤i≤k} = Σ{(a i) * x^i | 0≤i≤k} BY
               (BLemma `rsum_functionality` THEN Auto THEN D 0 THEN Auto THEN Subst' 0 + i ~ i 0 THEN Auto))
   THEN (RWO "-1" (-2) THENA Auto)
   THEN MoveToConcl (-2)
   THEN (GenConcl ⌜poly-approx-aux(a;x;xM;M;0;k) = z ∈ ℤ⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN GenConclTerm ⌜Σ{(a i) * x^i | 0≤i≤k}⌝⋅
   THEN Auto) }

1
1. k : ℕ
2. a : ℕ ⟶ ℝ
3. x : ℝ
4. ∀[xM:ℤ]. ∀[M:ℕ+]. ∀[n:ℕ].
     ((|x| ≤ (r1/r(4)))
     ⇒ 1-approx(x;M;xM)
     ⇒ k + 1-approx(Σ{(a (n + i)) * x^i | 0≤i≤k};M;poly-approx-aux(a;x;xM;M;n;k)))
5. N : ℕ+
6. |x| ≤ (r1/r(4))
7. B : ℕ+
8. (2 * (k + 1)) = B ∈ ℕ+
9. M : ℕ+
10. (B * N) = M ∈ ℕ+
11. xM : ℤ
12. (x M) = xM ∈ ℤ
13. 1-approx(x;M;xM)
14. Σ{(a (0 + i)) * x^i | 0≤i≤k} = Σ{(a i) * x^i | 0≤i≤k}
15. z : ℤ
16. poly-approx-aux(a;x;xM;M;0;k) = z ∈ ℤ
17. v : ℝ
18. Σ{(a i) * x^i | 0≤i≤k} = v ∈ ℝ
19. k + 1-approx(v;M;z)
⊢ 1-approx(v;N;z ÷ B)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  x  :  \mBbbR{}
4.  \mforall{}[xM:\mBbbZ{}].  \mforall{}[M:\mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbN{}].
          ((|x|  \mleq{}  (r1/r(4)))
          {}\mRightarrow{}  1-approx(x;M;xM)
          {}\mRightarrow{}  k  +  1-approx(\mSigma{}\{(a  (n  +  i))  *  x\^{}i  |  0\mleq{}i\mleq{}k\};M;poly-approx-aux(a;x;xM;M;n;k)))
5.  N  :  \mBbbN{}\msupplus{}
6.  |x|  \mleq{}  (r1/r(4))
7.  B  :  \mBbbN{}\msupplus{}
8.  (2  *  (k  +  1))  =  B
9.  M  :  \mBbbN{}\msupplus{}
10.  (B  *  N)  =  M
11.  xM  :  \mBbbZ{}
12.  (x  M)  =  xM
13.  1-approx(x;M;xM)
\mvdash{}  1-approx(\mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}k\};N;eval  z  =  poly-approx-aux(a;x;xM;M;0;k)  in
                                                                        z  \mdiv{}  B)


By

---

Latex:
((InstHyp  [\mkleeneopen{}xM\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  (Assert  \mSigma{}\{(a  (0  +  i))  *  x\^{}i  |  0\mleq{}i\mleq{}k\}  =  \mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}k\}  BY
                          (BLemma  `rsum\_functionality`
                            THEN  Auto
                            THEN  D  0
                            THEN  Auto
                            THEN  Subst'  0  +  i  \msim{}  i  0
                            THEN  Auto))
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  (GenConcl  \mkleeneopen{}poly-approx-aux(a;x;xM;M;0;k)  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  GenConclTerm  \mkleeneopen{}\mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}k\}\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index