---

Step * 1 1 1 1 1 of Lemma rsin-pi-over-4


1. r0 = (rcos((π/r(4)))^2 - rsin((π/r(4)))^2)
2. rcos((π/r(4)) + (π/r(4))) = rcos(π/2)
3. (rsin((π/r(4)))^2 + rsin((π/r(4)))^2) = r1
4. rcos((π/r(4)))^2 = rsin((π/r(4)))^2
⊢ rsin((π/r(4))) = (r1/rsqrt(r(2)))
BY
{ (InstLemma `rsqrt-unique` [⌜(r1/r(2))⌝;⌜rsin((π/r(4)))⌝]⋅ THEN Auto) }

1
.....wf..... 
1. r0 = (rcos((π/r(4)))^2 - rsin((π/r(4)))^2)
2. rcos((π/r(4)) + (π/r(4))) = rcos(π/2)
3. (rsin((π/r(4)))^2 + rsin((π/r(4)))^2) = r1
4. rcos((π/r(4)))^2 = rsin((π/r(4)))^2
⊢ rsin((π/r(4))) ∈ {x:ℝ| r0 ≤ x} 

2
.....antecedent..... 
1. r0 = (rcos((π/r(4)))^2 - rsin((π/r(4)))^2)
2. rcos((π/r(4)) + (π/r(4))) = rcos(π/2)
3. (rsin((π/r(4)))^2 + rsin((π/r(4)))^2) = r1
4. rcos((π/r(4)))^2 = rsin((π/r(4)))^2
⊢ (rsin((π/r(4))) * rsin((π/r(4)))) = (r1/r(2))

3
1. r0 = (rcos((π/r(4)))^2 - rsin((π/r(4)))^2)
2. rcos((π/r(4)) + (π/r(4))) = rcos(π/2)
3. (rsin((π/r(4)))^2 + rsin((π/r(4)))^2) = r1
4. rcos((π/r(4)))^2 = rsin((π/r(4)))^2
5. rsin((π/r(4))) = rsqrt((r1/r(2)))
⊢ rsin((π/r(4))) = (r1/rsqrt(r(2)))

---

Latex:

---

Latex:

1.  r0  =  (rcos((\mpi{}/r(4)))\^{}2  -  rsin((\mpi{}/r(4)))\^{}2)
2.  rcos((\mpi{}/r(4))  +  (\mpi{}/r(4)))  =  rcos(\mpi{}/2)
3.  (rsin((\mpi{}/r(4)))\^{}2  +  rsin((\mpi{}/r(4)))\^{}2)  =  r1
4.  rcos((\mpi{}/r(4)))\^{}2  =  rsin((\mpi{}/r(4)))\^{}2
\mvdash{}  rsin((\mpi{}/r(4)))  =  (r1/rsqrt(r(2)))


By

---

Latex:
(InstLemma  `rsqrt-unique`  [\mkleeneopen{}(r1/r(2))\mkleeneclose{};\mkleeneopen{}rsin((\mpi{}/r(4)))\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index