let n be Nat; :: thesis: ( n < 8 & card (PrimeDivisors n) = 1 & card (PrimeDivisors (n + 1)) = 1 & n is not mersenne Prime implies n + 1 is fermat Prime )
assume n < 8 ; :: thesis: ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime )
then n < 7 + 1 ;
then n <= 7 by NAT_1:13;
then not not n = 0 & ... & not n = 7 ;
per cases then ( n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5 or n = 6 or n = 7 ) ;
suppose n = 0 ; :: thesis: ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime )
hence ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime ) by Fer0; :: thesis: verum
end;
suppose n = 1 ; :: thesis: ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime )
hence ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime ) by Fer1; :: thesis: verum
end;
suppose n = 2 ; :: thesis: ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime )
hence ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime ) by Fer2; :: thesis: verum
end;
suppose n = 3 ; :: thesis: ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime )
hence ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime ) by Fer3; :: thesis: verum
end;
suppose n = 4 ; :: thesis: ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime )
hence ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime ) by Fer4; :: thesis: verum
end;
suppose n = 5 ; :: thesis: ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime )
hence ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime ) by Fer5; :: thesis: verum
end;
suppose n = 6 ; :: thesis: ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime )
hence ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime ) by Fer6; :: thesis: verum
end;
suppose n = 7 ; :: thesis: ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime )
hence ( not card (PrimeDivisors n) = 1 or not card (PrimeDivisors (n + 1)) = 1 or n is mersenne Prime or n + 1 is fermat Prime ) by Fer7; :: thesis: verum
end;
end;