---

Step * of Lemma rcos-nonpositive

∀x:{x:ℝ| x ∈ [π/2, π + π/2]} . (rcos(x) ≤ r0)
BY
{ (Auto
   THEN (InstLemma `rcos-nonneg` [⌜x - π⌝]⋅
         THENA (D 1
                THEN MemTypeCD
                THEN Auto
                THEN All Reduce
                THEN Auto
                THEN nRAdd ⌜π⌝ 0⋅
                THEN Auto
                THEN Unfold `pi` 0
                THEN (RWO "int-rmul-req" 0 THENA Auto)
                THEN nRNorm 0
                THEN Auto)
         )
   ) }

1
1. x : {x:ℝ| x ∈ [π/2, π + π/2]} 
2. r0 ≤ rcos(x - π)
⊢ rcos(x) ≤ r0

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `rcos-nonneg`  [\mkleeneopen{}x  -  \mpi{}\mkleeneclose{}]\mcdot{}
              THENA  (D  1
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  All  Reduce
                            THEN  Auto
                            THEN  nRAdd  \mkleeneopen{}\mpi{}\mkleeneclose{}  0\mcdot{}
                            THEN  Auto
                            THEN  Unfold  `pi`  0
                            THEN  (RWO  "int-rmul-req"  0  THENA  Auto)
                            THEN  nRNorm  0
                            THEN  Auto)
              )
  )

---

Home Index