Description: Lemma for ang180 . Since ang180lem1 shows that N is an integer and ang180lem2 shows that N is strictly between -u 2 and 1 , it follows that N e. { -u 1 , 0 } , and these two cases correspond to the two possible values for T . (Contributed by Mario Carneiro, 23-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ang.1 | |
|
ang180lem1.2 | |
||
ang180lem1.3 | |
||
Assertion | ang180lem3 | |