let n be Nat; ( not n satisfies_Sierpinski_problem_86 or ( n - 1 is prime & ex x, y being Prime st
( x <> y & n + 1 = x * y ) ) or ( n + 1 is prime & ex x, y being Prime st
( x <> y & n - 1 = x * y ) ) )
assume
n satisfies_Sierpinski_problem_86
; ( ( n - 1 is prime & ex x, y being Prime st
( x <> y & n + 1 = x * y ) ) or ( n + 1 is prime & ex x, y being Prime st
( x <> y & n - 1 = x * y ) ) )
then consider a, b, c being Prime such that
A1:
a,b,c are_mutually_distinct
and
A2:
(a * b) * c = (n |^ 2) - 1
;
A3:
n |^ 2 = n ^2
by WSIERP_1:1;
then A4:
(a * b) * c = (n - 1) * (n + 1)
by A2;
c divides (a * b) * c
;
then A5:
( c divides n - 1 or c divides n + 1 )
by A4, INT_5:7;
A6:
c > 1
by INT_2:def 4;
A7:
(a * b) * c = (b * c) * a
;
A8:
(a * b) * c = (a * c) * b
;
A9:
now not 1 > nassume
1
> n
;
contradictionthen
n = 0
by NAT_1:14;
hence
contradiction
by A2;
verum end;