---

Step * of Lemma rsin-reduce-half-pi

∀[n:ℤ]. ∀[x:ℝ].
  (rsin(x - n * π/2)
  = if (n mod 4 =z 0) then rsin(x)
    if (n mod 4 =z 2) then -(rsin(x))
    if (n mod 4 =z 1) then -(rcos(x))
    else rcos(x)
    fi )
BY
{ (Auto
   THEN (InstLemma `mod_bounds` [⌜n⌝;⌜4⌝]⋅ THENA Auto)
   THEN (InstLemma `mod-eqmod` [⌜n⌝;⌜4⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜(n mod 4) = i ∈ ℕ4⌝⋅ THENA Auto)
   THEN All Thin
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN IntSegCases 3
   THEN Reduce 0) }

1
1. n : ℤ
2. x : ℝ
3. i : ℤ
4. c : ℤ
5. (i - n) = (4 * c) ∈ ℤ
6. i = 0 ∈ ℤ
⊢ rsin(x - n * π/2) = rsin(x)

2
1. n : ℤ
2. x : ℝ
3. i : ℤ
4. c : ℤ
5. (i - n) = (4 * c) ∈ ℤ
6. i = 1 ∈ ℤ
⊢ rsin(x - n * π/2) = -(rcos(x))

3
1. n : ℤ
2. x : ℝ
3. i : ℤ
4. c : ℤ
5. (i - n) = (4 * c) ∈ ℤ
6. i = 2 ∈ ℤ
⊢ rsin(x - n * π/2) = -(rsin(x))

4
1. n : ℤ
2. x : ℝ
3. i : ℤ
4. c : ℤ
5. (i - n) = (4 * c) ∈ ℤ
6. i = 3 ∈ ℤ
⊢ rsin(x - n * π/2) = rcos(x)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[x:\mBbbR{}].
    (rsin(x  -  n  *  \mpi{}/2)
    =  if  (n  mod  4  =\msubz{}  0)  then  rsin(x)
        if  (n  mod  4  =\msubz{}  2)  then  -(rsin(x))
        if  (n  mod  4  =\msubz{}  1)  then  -(rcos(x))
        else  rcos(x)
        fi  )


By

---

Latex:
(Auto
  THEN  (InstLemma  `mod\_bounds`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}4\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `mod-eqmod`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}4\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}(n  mod  4)  =  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  IntSegCases  3
  THEN  Reduce  0)

---

Home Index