Exercices on polynomials

  • Formalisation of the algebraic part of a simple proof that PI is irrational described in:
  • http://projecteuclid.org/download/pdf_1/euclid.bams/1183510788

Parameters definitions:

  • Let n na nb be natural numbers
  • Suppose nb is a non zero nat: nb != 0
  • Define the corresponding rationals a , b
  • Define pi as a/b.

Definition of the polynomials:

  • Look at the f definition: the factorial, the coercion nat :> R (as a Ring), etc...
  • Define F:{poly rat} using bigop.

Prove that:

  • b is non zero rational.

Prove that:

  • (a - bX) has a size of 2

Prove that:

  • the lead_coef of (a - bX) is -b.

Prove that:

  • the size of (a-X)^n is n.+1

Prove that:

  • Exponent and composition of polynomials combine:

Prove that:

  • f's small coefficients are zero

Prove that:

  • f/n! as integral coefficients

Prove that:

the f^`(i) (x) have integral values for x = 0

Deduce that:

F (0) has an integral value

Then prove

  • the symmetry argument f(x) = f(pi -x).


  • the symmetry for the derivative

Deduce that

  • F(pi) is an integer

if you have time

  • you can prove the equality F^`(2) + F = f
  • that is needed by the analytic part of the Niven proof

save script