---

Step * 1 2 1 of Lemma rcos-seq-converges

.....assertion..... 
1. ∀n:ℕ+. ((rcos-seq(n + 1) - rcos-seq(n)) ≤ ((r1/r(3164556962025316455)) * (rcos-seq(n) - rcos-seq(n - 1))))
⊢ (r(3164556962025316455) * (rcos-seq(1) - rcos-seq(0))/r(3164556962025316455 - 1)) < (r1/r(1000000000))
BY
{ ((D 0 With ⌜10^10⌝  THENA Auto)
   THEN (Subst' (r(3164556962025316455) * (rcos-seq(1) - rcos-seq(0))/r(3164556962025316455 - 1)) 10^10 ~ 15 0
         THENA Refine `computeAll` []
         )
   ) }

1
1. ∀n:ℕ+. ((rcos-seq(n + 1) - rcos-seq(n)) ≤ ((r1/r(3164556962025316455)) * (rcos-seq(n) - rcos-seq(n - 1))))
⊢ 15 + 4 < (r1/r(1000000000)) 10^10

---

Latex:

---

Latex:
.....assertion..... 
1.  \mforall{}n:\mBbbN{}\msupplus{}
          ((rcos-seq(n  +  1)  -  rcos-seq(n))  \mleq{}  ((r1/r(3164556962025316455))
          *  (rcos-seq(n)  -  rcos-seq(n  -  1))))
\mvdash{}  (r(3164556962025316455)  *  (rcos-seq(1)  -  rcos-seq(0))/r(3164556962025316455 
-  1))  <  (r1/r(1000000000))


By

---

Latex:
((D  0  With  \mkleeneopen{}10\^{}10\mkleeneclose{}    THENA  Auto)
  THEN  (Subst'  (r(3164556962025316455)  *  (rcos-seq(1)  -  rcos-seq(0))/r(3164556962025316455  -  1)) 
                            10\^{}10  \msim{}  15  0
              THENA  Refine  `computeAll`  []
              )
  )

---

Home Index