From van IJzeren's correspondence to my aunt and uncle (EWD1317)

From van IJzeren's correspondence to my aunt and uncle

Browsing through letters sent to my late aunt dr H.A. van Herk-Kluyver, I found the following theorem and proof in a letter from my late brother-in-law mr dr J.van IJzeren. The theorem is surprising but not interesting; this note is devoted to its proof because it is an elementary and very convincing illustration of the use of the device of the General Solution (which I promoted in EWD1155).

The proof uses two theorems.

(0) A Pythagorean triple that is relatively prime, can be written as p² – q², 2pq, p² + q² (See EWD1172.)

(1) For prime p, n^p – n is a multiple of p. (Known as "Fermat's Little Theorem", see EWD740.)

The theorem to be proved here —as said: surprising but not interesting— is

(2) For any Pythagorean triple, i.e. with a² + b² = c², there is a multiple of 7 among (a), (b), (a−b), (a+b).

*		*
	*

Proof Because of a² + b² = c², any factor shared by 2 of the numbers is shared by the 3rd, and hence we can restrict ourselves to a, b, c that are relatively prime. We shall do so in what follows.

With ⊑ denoting "divides" and p,q providing (see (0)) the parameters for the General Solution of a² + b² = c², we observe

  7 ⊑ a ∨ 7 ⊑ b ∨ 7 ⊑ a-b ∨ 7 ⊑ a+b
≡   { algebra, prime.7 }
  7 ⊑ ab(a² – b²)
≡   { a := p² – q², b := 2pq }
  7 ⊑ 2(p² – q²)pq(p⁴ - 2p²q² + q⁴ – 4p²q²)
≡   { ¬ 7 ⊑ 2, prime.7, algebra }
  7 ⊑ pq(p² – q²) (p⁴ - 6p²q² + q⁴)
≡   { modulo calculus }
  7 ⊑ pq(p² – q²) (p⁴ + p²q² + q⁴)
≡   { algebra }
  7 ⊑ pq(p⁶ – q⁶)
≡   { algebra }
  7 ⊑ p⁷q – pq⁷
≡   { Fermat's Little Theorem, modulo calculus, prime.7 }
  7 ⊑ pq – pq
≡   { 7 ⊑ 0 }
  true.

I don't think I could have proved this theorem without the introduction of p and q.

Austin, 11 January 2002

prof.dr. Edsger W. Dijkstra
Department of Computer Sciences
The University of Texas at Austin
Austin, TX 78712 – 1188 USA