---

Step * of Lemma rsin-first-req-1

∀x:ℝ. ((r0 ≤ x) ⇒ (rsin(x) = r1) ⇒ (π/2 ≤ x))
BY
{ (Auto
   THEN ((BLemma `rleq-iff-not-rless` THENM D 0) THENA Auto)
   THEN (InstLemma `rcos-positive-before-half-pi` [⌜x⌝]⋅ THENA Auto)) }

1
1. x : ℝ
2. r0 ≤ x
3. rsin(x) = r1
4. x < π/2
5. r0 < rcos(x)
⊢ False

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  ((r0  \mleq{}  x)  {}\mRightarrow{}  (rsin(x)  =  r1)  {}\mRightarrow{}  (\mpi{}/2  \mleq{}  x))


By

---

Latex:
(Auto
  THEN  ((BLemma  `rleq-iff-not-rless`  THENM  D  0)  THENA  Auto)
  THEN  (InstLemma  `rcos-positive-before-half-pi`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index