assume Mersenne n = 0 ; :: according to ORDINAL1:def 14 :: thesis: contradiction
then log (2,(2 to_power n)) = 0 by POWER:51;
then n * (log (2,2)) = 0 by POWER:55;
then n * 1 = 0 by POWER:52;
hence contradiction ; :: thesis: verum