---

Step * of Lemma rcos-nonzero-on

rcos(x)≠r0 for x ∈ (-(π/2), π/2)
BY
{ (InstLemma `second-deriv-implies-nonzero-on` [⌜(-(π/2), π/2)⌝;⌜λ2x.rcos(x)⌝;⌜λ2x.-(rsin(x))⌝;⌜λ2x.-(rcos(x))⌝]⋅
   THEN Auto
   ) }

1
.....antecedent..... 
d(rcos(x))/dx = λx.-(rsin(x)) on (-(π/2), π/2)

2
.....antecedent..... 
d(-(rsin(x)))/dx = λx.-(rcos(x)) on (-(π/2), π/2)

3
.....antecedent..... 
((∀x:{a:ℝ| a ∈ (-(π/2), π/2)} . (-(rcos(x)) ≤ r0)) ∧ (∀x:ℝ. ((x ∈ (-(π/2), π/2)) ⇒ (r0 < rcos(x)))))
∨ ((∀x:{a:ℝ| a ∈ (-(π/2), π/2)} . (r0 ≤ -(rcos(x)))) ∧ (∀x:ℝ. ((x ∈ (-(π/2), π/2)) ⇒ (rcos(x) < r0))))

---

Latex:

---

Latex:
rcos(x)\mneq{}r0  for  x  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)


By

---

Latex:
(InstLemma  `second-deriv-implies-nonzero-on`  [\mkleeneopen{}(-(\mpi{}/2),  \mpi{}/2)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.-(rsin(x))\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}x.-(rcos(x))\mkleeneclose{}]\mcdot{}
  THEN  Auto
  )

---

Home Index