Step
*
2
2
1
of Lemma
rcos-nonneg
1. x : {x:ℝ| x ∈ [-(π/2), π/2]}
2. x < (r1/r(1000))
3. x < r0
⊢ r0 ≤ rcos(-(x))
BY
{ ((BLemma `rcos-nonneg-upto-half-pi` THEN Auto)
THEN DSetVars
THEN All Reduce
THEN MemTypeCD
THEN Auto
THEN nRAdd ⌜x⌝ 0⋅
THEN Auto) }
Latex:
Latex:
1. x : \{x:\mBbbR{}| x \mmember{} [-(\mpi{}/2), \mpi{}/2]\}
2. x < (r1/r(1000))
3. x < r0
\mvdash{} r0 \mleq{} rcos(-(x))
By
Latex:
((BLemma `rcos-nonneg-upto-half-pi` THEN Auto)
THEN DSetVars
THEN All Reduce
THEN MemTypeCD
THEN Auto
THEN nRAdd \mkleeneopen{}x\mkleeneclose{} 0\mcdot{}
THEN Auto)
Home
Index