Flyspeck/lemma-1-7

From MathWeb

Jump to: navigation, search

Twelf 

 lemma-1-7 : |- cos X <> zero 
            -> |- cos Y <> zero
            -> |- cos (X + Y) <> zero
            -> |- tan(X + Y) == (tan X + tan Y) / (one - tan X * tan Y).

LaTeX

If \cos(x)\ne 0, \cos(y)\ne 0, and \cos(x+y)\ne 0 then

\tan(x+y)=\frac{\tan(x)+\tan(y)}{1-\tan(x)\tan(y)}

Annotations

Retrieved from "http://www.mathweb.org/wiki/Flyspeck/lemma-1-7"
Facts about Flyspeck/lemma-1-7RDF feed
Uses symbolFlyspeck/lemma-1-7  +, Flyspeck/ bar-  +, Flyspeck/cos  +, Flyspeck/ lt gt  +, Flyspeck/zero  +, Flyspeck/ plus  +, Flyspeck/tan  +, Flyspeck/==  +, Flyspeck//  +, Flyspeck/one  +, Flyspeck/-  +, and Flyspeck/*  +
Written inTwelf  +, and LaTeX  +
Personal tools
MathWeb
Structures