---

Step * 1 1 1 1 2 1 1 of Lemma cosine-exists


1. x : ℝ
2. ∀n:ℕ. (r0 ≤ (x^2 * n/r((2 * n)!)))
3. b : ℕ
4. |x| ≤ r(b)
5. i : ℕ@i
6. b ÷ 2 < i
7. (x * x) ≤ (r((2 * (i + 1))!)/r((2 * i)!))
8. r0 ≤ (x^2 * i/r((2 * i)!))
⊢ (x^2 * (i + 1)/r((2 * (i + 1))!)) ≤ (x^2 * i/r((2 * i)!))
BY
{ (Thin (-1)
   THEN MoveToConcl (-1)
   THEN (Assert r0 < r((2 * (i + 1))!) BY
               Auto)
   THEN (Assert r0 < r((2 * i)!) BY
               Auto)
   THEN (MoveToConcl (-1) THEN (GenConclAtAddrType ⌜ℝ⌝ [1;2] ⋅ THENA Auto) THEN Thin (-1))
   THEN MoveToConcl (-2)
   THEN (GenConclAtAddrType ⌜ℝ⌝ [1;2] ⋅ THENA Auto)
   THEN All Thin)⋅ }

1
1. x : ℝ
2. i : ℕ@i
3. v : ℝ@i
4. v1 : ℝ@i
⊢ (r0 < v1) ⇒ (r0 < v) ⇒ ((x * x) ≤ (v1/v)) ⇒ ((x^2 * (i + 1)/v1) ≤ (x^2 * i/v))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  \mforall{}n:\mBbbN{}.  (r0  \mleq{}  (x\^{}2  *  n/r((2  *  n)!)))
3.  b  :  \mBbbN{}
4.  |x|  \mleq{}  r(b)
5.  i  :  \mBbbN{}@i
6.  b  \mdiv{}  2  <  i
7.  (x  *  x)  \mleq{}  (r((2  *  (i  +  1))!)/r((2  *  i)!))
8.  r0  \mleq{}  (x\^{}2  *  i/r((2  *  i)!))
\mvdash{}  (x\^{}2  *  (i  +  1)/r((2  *  (i  +  1))!))  \mleq{}  (x\^{}2  *  i/r((2  *  i)!))


By

---

Latex:
(Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (Assert  r0  <  r((2  *  (i  +  1))!)  BY
                          Auto)
  THEN  (Assert  r0  <  r((2  *  i)!)  BY
                          Auto)
  THEN  (MoveToConcl  (-1)  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;2]  \mcdot{}  THENA  Auto)  THEN  Thin  (-1))
  THEN  MoveToConcl  (-2)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;2]  \mcdot{}  THENA  Auto)
  THEN  All  Thin)\mcdot{}

---

Home Index