---

Step * of Lemma rcos-nonneg-upto-half-pi

∀x:{x:ℝ| x ∈ [r0, π/2]} . (r0 ≤ rcos(x))
BY
{ (Auto
   THEN D 1
   THEN ((Unhide THEN Auto) THEN (Assert r0 < π/2 BY Auto))
   THEN BLemma `rleq-iff-all-rless`
   THEN Auto
   THEN (InstLemma `function-is-continuous` [⌜[r0, π/2]⌝;⌜λ2x.rcos(x)⌝]⋅
         THENA (Auto THEN RepUR ``iproper`` 0 THEN Auto THEN RWO "-1" 0 THEN Auto)
         )) }

1
1. x : ℝ
2. x ∈ [r0, π/2]
3. r0 < π/2
4. e : {e:ℝ| r0 < e} 
5. rcos(x) continuous for x ∈ [r0, π/2]
⊢ r0 ≤ (rcos(x) + e)

---

Latex:

---

Latex:
\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [r0,  \mpi{}/2]\}  .  (r0  \mleq{}  rcos(x))


By

---

Latex:
(Auto
  THEN  D  1
  THEN  ((Unhide  THEN  Auto)  THEN  (Assert  r0  <  \mpi{}/2  BY  Auto))
  THEN  BLemma  `rleq-iff-all-rless`
  THEN  Auto
  THEN  (InstLemma  `function-is-continuous`  [\mkleeneopen{}[r0,  \mpi{}/2]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(x)\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RepUR  ``iproper``  0  THEN  Auto  THEN  RWO  "-1"  0  THEN  Auto)
              ))

---

Home Index