---

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


1. x : ℝ
2. i : ℕ@i
3. v : ℝ@i
4. v1 : ℝ@i
5. r0 < v1
6. r0 < v
7. (v * x * x) ≤ v1
8. v ≠ r0
9. v1 ≠ r0
⊢ (x^2 * (i + 1) * v) ≤ (x^2 * i * v1)
BY
{ ((RWO "rnexp-mul<" 0 THENA Auto')
   THEN (Assert x^2 = (x * x) BY
               ((RWO "rpower-two" 0 THEN Reduce 0) THEN Auto))
   THEN RWO "-1" 0
   THEN Auto
   THEN MoveToConcl (-4)⋅
   THEN (GenConcl⌜(x * x) = y ∈ {r:ℝ| r0 ≤ r} ⌝⋅ THENA (Auto THEN InstLemma `square-nonneg` [⌜x⌝]⋅ THEN Auto)))⋅ }

1
1. x : ℝ
2. i : ℕ@i
3. v : ℝ@i
4. v1 : ℝ@i
5. r0 < v1
6. r0 < v
7. v ≠ r0
8. v1 ≠ r0
9. x^2 = (x * x)
10. y : {r:ℝ| r0 ≤ r} @i
11. (x * x) = y ∈ {r:ℝ| r0 ≤ r} 
⊢ ((v * y) ≤ v1) ⇒ ((y^i + 1 * v) ≤ (y^i * v1))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  i  :  \mBbbN{}@i
3.  v  :  \mBbbR{}@i
4.  v1  :  \mBbbR{}@i
5.  r0  <  v1
6.  r0  <  v
7.  (v  *  x  *  x)  \mleq{}  v1
8.  v  \mneq{}  r0
9.  v1  \mneq{}  r0
\mvdash{}  (x\^{}2  *  (i  +  1)  *  v)  \mleq{}  (x\^{}2  *  i  *  v1)


By

---

Latex:
((RWO  "rnexp-mul<"  0  THENA  Auto')
  THEN  (Assert  x\^{}2  =  (x  *  x)  BY
                          ((RWO  "rpower-two"  0  THEN  Reduce  0)  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  MoveToConcl  (-4)\mcdot{}
  THEN  (GenConcl\mkleeneopen{}(x  *  x)  =  y\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  InstLemma  `square-nonneg`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)))\mcdot{}

---

Home Index