---

Step * of Lemma rsine_wf

∀[x:ℝ]. (rsine(x) ∈ {y:ℝ| y = rsin(x)} )
BY
{ (Auto
   THEN Unfold `rsine` 0
   THEN (GenConclTerm ⌜reduce-halfpi(x)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RenameVar `n' (-1)
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (GenConcl ⌜2 * MachinPi4() = p ∈ {p:ℝ| p = π/2} ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN (D -2 THEN D -1 THEN (Assert |x - r(n) * p| ≤ r(2) BY (RWO  "-1" 0 THEN Auto)))
   THEN (RWO "int-rmul-req<" (-1) THENA Auto)
   THEN DupHyp (-1)
   THEN (RWO "rabs-rleq-iff" (-1) THENA Auto)
   THEN MemTypeCD
   THEN Auto) }

1
1. x : ℝ
2. n : ℤ
3. |x - r(n) * π/2| ≤ r(2)
4. p : ℝ
5. p = π/2
6. |x - n * p| ≤ r(2)
7. -(r(2)) ≤ (x - n * p)
8. (x - n * p) ≤ r(2)
⊢ if (n mod 4 =z 0) then sine-medium(x - n * p)
if (n mod 4 =z 2) then -(sine-medium(x - n * p))
if (n mod 4 =z 1) then cosine-medium(x - n * p)
else -(cosine-medium(x - n * p))
fi 
= rsin(x)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (rsine(x)  \mmember{}  \{y:\mBbbR{}|  y  =  rsin(x)\}  )


By

---

Latex:
(Auto
  THEN  Unfold  `rsine`  0
  THEN  (GenConclTerm  \mkleeneopen{}reduce-halfpi(x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RenameVar  `n'  (-1)
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}2  *  MachinPi4()  =  p\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (D  -2  THEN  D  -1  THEN  (Assert  |x  -  r(n)  *  p|  \mleq{}  r(2)  BY  (RWO    "-1"  0  THEN  Auto)))
  THEN  (RWO  "int-rmul-req<"  (-1)  THENA  Auto)
  THEN  DupHyp  (-1)
  THEN  (RWO  "rabs-rleq-iff"  (-1)  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index