---

Step * 1 2 1 1 1 1 of Lemma radd_rcos-Taylor


1. b : ℝ
2. e : {e:ℝ| r0 < e} 
3. c : ℝ
4. rmin(π/2(slower);b) ≤ c
5. c ≤ rmax(π/2(slower);b)
6. z : ℝ
7. |r(2)| = r(2)
8. r0 < |r(2)|
⊢ (|b + -(c)^2| * |rsin(c)|) ≤ |-(π/2(slower)) + b|^2
BY
{ (RWO "rmul_comm" 0 THENA Auto) }

1
1. b : ℝ
2. e : {e:ℝ| r0 < e} 
3. c : ℝ
4. rmin(π/2(slower);b) ≤ c
5. c ≤ rmax(π/2(slower);b)
6. z : ℝ
7. |r(2)| = r(2)
8. r0 < |r(2)|
⊢ (|rsin(c)| * |b + -(c)^2|) ≤ |-(π/2(slower)) + b|^2

---

Latex:

---

Latex:

1.  b  :  \mBbbR{}
2.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
3.  c  :  \mBbbR{}
4.  rmin(\mpi{}/2(slower);b)  \mleq{}  c
5.  c  \mleq{}  rmax(\mpi{}/2(slower);b)
6.  z  :  \mBbbR{}
7.  |r(2)|  =  r(2)
8.  r0  <  |r(2)|
\mvdash{}  (|b  +  -(c)\^{}2|  *  |rsin(c)|)  \mleq{}  |-(\mpi{}/2(slower))  +  b|\^{}2


By

---

Latex:
(RWO  "rmul\_comm"  0  THENA  Auto)

---

Home Index