# mathlib3documentation

mathlib-archive / imo.imo1969_q1

# IMO 1969 Q1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Prove that there are infinitely many natural numbers $a$ with the following property: the number $z = n^4 + a$ is not prime for any natural number $n$.

good_nats is the set of natural numbers satisfying the condition in the problem statement, namely the a : ℕ such that n^4 + a is not prime for any n : ℕ.

Equations

The key to the solution is that you can factor $z$ into the product of two polynomials, if $a = 4*m^4$. This is Sophie Germain's identity, called pow_four_add_four_mul_pow_four in mathlib.

theorem imo1969_q1.factorization {m n : } :
((n - m) ^ 2 + m ^ 2) * ((n + m) ^ 2 + m ^ 2) = n ^ 4 + 4 * m ^ 4

To show that the product is not prime, we need to show each of the factors is at least 2, which nlinarith can solve since they are each expressed as a sum of squares.

theorem imo1969_q1.left_factor_large {m : } (n : ) (h : 1 < m) :
1 < (n - m) ^ 2 + m ^ 2
theorem imo1969_q1.right_factor_large {m : } (n : ) (h : 1 < m) :
1 < (n + m) ^ 2 + m ^ 2

The factorization is over the integers, but we need the nonprimality over the natural numbers.

theorem imo1969_q1.int_large {m : } (h : 1 < m) :
theorem imo1969_q1.not_prime_of_int_mul' {m n : } {c : } (hm : 1 < m) (hn : 1 < n) (hc : m * n = c) :
theorem imo1969_q1.polynomial_not_prime {m : } (h1 : 1 < m) (n : ) :
¬nat.prime (n ^ 4 + 4 * m ^ 4)

Every natural number of the form n^4 + 4*m^4 is not prime.

def imo1969_q1.a_choice (b : ) :

We define $a_{choice}(b) := 4*(2+b)^4$, so that we can take $m = 2+b$ in polynomial_not_prime.

Equations

a_choice is a strictly monotone function; this is easily proven by chaining together lemmas in the strict_mono namespace.

theorem imo1969_q1  :
{a : | (n : ), ¬nat.prime (n ^ 4 + a)}.infinite

We conclude by using the fact that a_choice is an injective function from the natural numbers to the set good_nats.