Lm1:
for n being even Nat holds (- 1) |^ n = 1
Lm2:
for n being odd Nat holds (- 1) |^ n = - 1
Lm3:
for a being Nat
for b being Integer st a divides b holds
a gcd b = a
Lm4:
for a being Integer
for p being Prime holds Lege (a,p) = Leg (a,p)
Lm5:
1 is odd
Lm6:
3 is Proth
Lm7:
9 is Proth
TT:
( not Fermat 5 is prime & 641 divides Fermat 5 )