Description: Lemma for ang180 . Show that the "revolution number" N is an integer, using efeq1 to show that since the product of the three arguments A , 1 / ( 1 - A ) , ( A - 1 ) / A is -u 1 , the sum of the logarithms must be an integer multiple of 2pi i away from _pi _i = log ( -u 1 ) . (Contributed by Mario Carneiro, 23-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ang.1 | |
|
ang180lem1.2 | |
||
ang180lem1.3 | |
||
Assertion | ang180lem1 | |