Flyspeck/lemma-1-11

Twelf

 lemma-1-11 : |- ~ one <= Y 
             -> |- Y <= one 
             -> |- sin(arccos Y) == sqrt(one - sqr Y).

If $y\in[-1,1]$ , then $\sin(\arccos(y)) = \sqrt{1-y^2}$ .

This lemma was proven by Michael, using Isabelle. (Proof object)

Uses symbol	Flyspeck/lemma-1-11 +, Flyspeck/ bar- +, Flyspeck/ til +, Flyspeck/one +, Flyspeck/ lt= +, Flyspeck/sin +, Flyspeck/arccos +, Flyspeck/== +, Flyspeck/sqrt +, Flyspeck/- +, and Flyspeck/sqr +
Written in	Twelf +, and LaTeX +