I present this proof-in-Maple not just for its own sake, but because I think that it illustrates effective techniques for working with complicated algebraic numbers.

Proof of a complicated trigonometric / algebraic number identity

 

It is well known that for any integer p and positive integer q, cos(p*Pi/q)is an algebraic number. When q has prime factors larger than 3, an explicit presentation of that algebraic number can be quite complicated, and often involves imaginary numbers. Here we prove a remarkable purely real-number identity that holds between a group of these algebraic numbers when q = 19.

restart;

(The reason that I use lowercase pi in the following expression is explained below.)

LHS:=
   surd(cos(3*pi/19) + cos(5*pi/19) + cos(17*pi/19), 3) +
   surd(cos(pi/19) + cos(7*pi/19) + cos(11*pi/19), 3) +
   surd(cos(9*pi/19) + cos(13*pi/19) + cos(15*pi/19), 3)
;
RHS:= (
    1/2 -
    3*7^(1/3) +
    (3/2)*(-25+3*7^(2/3)+18*7^(1/3))^(1/3) +
    (3/2)*(-44+18*7^(1/3)+3*7^(2/3))^(1/3)
)^(1/3);

surd(cos((3/19)*pi)+cos((5/19)*pi)+cos((17/19)*pi), 3)+surd(cos((1/19)*pi)+cos((7/19)*pi)+cos((11/19)*pi), 3)+surd(cos((9/19)*pi)+cos((13/19)*pi)+cos((15/19)*pi), 3)

(1/2-3*7^(1/3)+(3/2)*(-25+3*7^(2/3)+18*7^(1/3))^(1/3)+(3/2)*(-44+18*7^(1/3)+3*7^(2/3))^(1/3))^(1/3)

The identity is

LHS = RHS:

This identity is quite remarkable for at least four reasons:

1. 

All the roots are cube roots (even though the cosines are the roots of a degree-9 polynomial, as we shall see).

2. 

All 9 roots of that polynomial are used.

3. 

All the numbers involved are real.

4. 

The only integer base of the cube roots is the small integer 7.

To prove the identity, we construct an exact integer polynomial whose roots give us the values of cosine in the identity. (The polynomial's roots are actually cos(k*Pi/(38))^(2), and they must be manipulated via the identity cos(2*x) = 2*cos(x)^2-1to get the values of cos((1/19)*k*Pi)that we want.)

algsubs(cos(x)^2= _Z, expand(cos(19*x))/cos(x));

262144*_Z^9-1245184*_Z^8+2490368*_Z^7-2723840*_Z^6+1770496*_Z^5-695552*_Z^4+160512*_Z^3-20064*_Z^2+1140*_Z-19

alias(P19= %):

Verify irreducibility:

factor(P19);

P19

Establish a correspondence between the roots of this polynomial and values of cos((1/19)*k*Pi), k odd.  Note the use of lowercase pi below to prevent simplifications that would otherwise be done by Maple's use of  the identity cos(Pi-x) = cos(x). For example, cos(11*Pi*(1/19))would become cos(8*Pi*(1/19)).

RootMap:= n-> cos((2*n-1)*pi/19) = 2*RootOf(P19, index= 10-n) - 1:

For example:

RootMap(5);

cos((9/19)*pi) = 2*RootOf(P19, index = 5)-1

Generate the substitutions that will be used on the left-hand side (LHS) of the identity.

Subs:= [seq](RootMap(k), k= 1..9):

Verify numerically that I've got the indexing in the right order.

(fnormal@evalf) ~ (eval((rhs-lhs) ~ (Subs), pi= Pi));

[0., -0., -0., -0., 0., 0., -0., -0., -0.]

Prove LHS - RHS = 0.

CodeTools:-Usage(evala(Normal(subs(Subs, LHS) - RHS)));

memory used=4.01GiB, alloc change=41.86MiB, cpu time=45.70s, real time=43.94s

0

 


Download identity19.mw


Please Wait...