---

Step * of Lemma sine-rminus

∀x:ℝ. (sine(-(x)) = -(sine(x)))
BY
{ (Auto
   THEN (InstLemma `sine-is-limit` [⌜x⌝]⋅ THENA Auto)
   THEN (InstLemma `sine-is-limit` [⌜-(x)⌝]⋅ THENA Auto)
   THEN (RWO "rnexp-rminus" (-1) THENA Auto)
   THEN (Assert ∀i:ℕ. isOdd((2 * i) + 1) = tt BY
               (Auto
                THEN Unfold `isOdd` 0
                THEN ((RWO  "mod2-add1" 0 THENA Auto) THEN (RWO  "mod2-2n" 0 THENA Auto))
                THEN Reduce 0
                THEN Auto))
   THEN (RWO  "-1" (-2) THENA Auto)
   THEN Reduce -2
   THEN (InstLemma `series-sum-unique` [⌜λ2i.-1^i * (-(x^(2 * i) + 1))/((2 * i) + 1)!⌝]⋅ THENA Auto)
   THEN BHyp -1
   THEN Auto) }

1
1. x : ℝ
2. Σi.-1^i * (x^(2 * i) + 1)/((2 * i) + 1)! = sine(x)
3. Σi.-1^i * (-(x^(2 * i) + 1))/((2 * i) + 1)! = sine(-(x))
4. ∀i:ℕ. isOdd((2 * i) + 1) = tt
5. ∀[a,b:ℝ].
     (a = b) supposing 
        (Σn.-1^n * (-(x^(2 * n) + 1))/((2 * n) + 1)! = b and 
        Σn.-1^n * (-(x^(2 * n) + 1))/((2 * n) + 1)! = a)
⊢ Σn.-1^n * (-(x^(2 * n) + 1))/((2 * n) + 1)! = -(sine(x))

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  (sine(-(x))  =  -(sine(x)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `sine-is-limit`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `sine-is-limit`  [\mkleeneopen{}-(x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "rnexp-rminus"  (-1)  THENA  Auto)
  THEN  (Assert  \mforall{}i:\mBbbN{}.  isOdd((2  *  i)  +  1)  =  tt  BY
                          (Auto
                            THEN  Unfold  `isOdd`  0
                            THEN  ((RWO    "mod2-add1"  0  THENA  Auto)  THEN  (RWO    "mod2-2n"  0  THENA  Auto))
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  (RWO    "-1"  (-2)  THENA  Auto)
  THEN  Reduce  -2
  THEN  (InstLemma  `series-sum-unique`  [\mkleeneopen{}\mlambda{}\msubtwo{}i.-1\^{}i  *  (-(x\^{}(2  *  i)  +  1))/((2  *  i)  +  1)!\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1
  THEN  Auto)

---

Home Index