---

Step * of Lemma rsin-positive

∀x:{x:ℝ| x ∈ (r0, π)} . (r0 < rsin(x))
BY
{ (Auto THEN InstLemma `rcos-positive` [⌜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  <  rsin(x))


By

---

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

---

Home Index