---

Step * of Lemma rsin-nonneg

∀x:{x:ℝ| x ∈ [r0, π]} . (r0 ≤ rsin(x))
BY
{ (Auto THEN InstLemma `rcos-nonneg` [⌜x - π/2⌝]⋅ THEN Auto) }

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  InstLemma  `rcos-nonneg`  [\mkleeneopen{}x  -  \mpi{}/2\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index