__My simplest theorem__

__Theorem__ Any natural number that has a divisor greater than itself equals zero.

__Proof__ We observe for any natural `n`, `d`, `q`

`n` = `d`∙`q` ∧ `d` > `n`

= { Leibniz }

`n` = `d`∙`q` ∧ `d` > `d`∙`q`

= { `d` > 0 }

`n` = `d`∙`q` ∧ 1 > `q`

= { `q` is natural }

`n` = `d`∙`q` ∧ `q` = 0

⇒ { Leibniz }

`n` = 0

( End of Proof )

At least twice —EWD1088 & EWD1170— I had used that 0 is the only natural number with infinitely many divisors —e.g. 2^{k} for any `k`— but I never took the trouble to prove it, and that probably explains why I missed the above.

Austin, 10 February 1996

prof. dr. Edsger W.Dijkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712-1188

USA

transcribed by Tristam Brelstaff

modified