theorem Th57: :: PEPIN:57

for n being Nat st n <> 0 holds
3, Fermat n are_coprime