---

Step * of Lemma rtan_one_one

∀x,y:{x:ℝ| x ∈ (-(π/2), π/2)} .  x = y supposing rtan(x) = rtan(y)
BY
{ (Auto
   THEN (StableCases ⌜x ≠ y⌝⋅ THENA Auto)
   THEN ((FLemma `not-rneq` [-1] THEN Auto) ORELSE (D -1 THEN FLemma `rtan_functionality_wrt_rless` [-1] THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  (-(\mpi{}/2),  \mpi{}/2)\}  .    x  =  y  supposing  rtan(x)  =  rtan(y)


By

---

Latex:
(Auto
  THEN  (StableCases  \mkleeneopen{}x  \mneq{}  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((FLemma  `not-rneq`  [-1]  THEN  Auto)
  ORELSE  (D  -1  THEN  FLemma  `rtan\_functionality\_wrt\_rless`  [-1]  THEN  Auto)
  ))

---

Home Index