---

Step * of Lemma derivative-rtan

d(rtan(x))/dx = λx.(r1/rcos(x)^2) on (-(π/2), π/2)
BY
{ (InstLemma `rcos-positive` []
   THEN (InstLemma `derivative-rdiv` [⌜(-(π/2), π/2)⌝;⌜λ2x.rsin(x)⌝;⌜λ2x.rcos(x)⌝;⌜λ2x.rcos(x)⌝;⌜λ2x.-(rsin(x))⌝]⋅
         THENA Auto
         )
   ) }

1
.....antecedent..... 
1. ∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (r0 < rcos(x))
⊢ d(rsin(x))/dx = λx.rcos(x) on (-(π/2), π/2)

2
.....antecedent..... 
1. ∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (r0 < rcos(x))
⊢ d(rcos(x))/dx = λx.-(rsin(x)) on (-(π/2), π/2)

3
1. ∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (r0 < rcos(x))
2. d((rsin(x)/rcos(x)))/dx = λx.((rcos(x) * rcos(x)) - rsin(x) * -(rsin(x))/rcos(x) * rcos(x)) on (-(π/2), π/2)
⊢ d(rtan(x))/dx = λx.(r1/rcos(x)^2) on (-(π/2), π/2)

---

Latex:

---

Latex:
d(rtan(x))/dx  =  \mlambda{}x.(r1/rcos(x)\^{}2)  on  (-(\mpi{}/2),  \mpi{}/2)


By

---

Latex:
(InstLemma  `rcos-positive`  []
  THEN  (InstLemma  `derivative-rdiv`  [\mkleeneopen{}(-(\mpi{}/2),  \mpi{}/2)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rsin(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(x)\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}x.-(rsin(x))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  )

---

Home Index