let n be Nat; :: thesis: ( n > 7 implies ex m being Nat ex p, q being Prime st
( p <> q & ( m = n or m = n + 1 or m = n + 2 ) & p divides m & q divides m ) )
assume A1: n > 7 ; :: thesis: ex m being Nat ex p, q being Prime st
( p <> q & ( m = n or m = n + 1 or m = n + 2 ) & p divides m & q divides m )
assume A2: for m being Nat
for p, q being Prime holds
( not p <> q or ( not m = n & not m = n + 1 & not m = n + 2 ) or not p divides m or not q divides m ) ; :: thesis: contradiction
then ( not 2 divides n or not 3 divides n ) by XPRIMES1:2, XPRIMES1:3;
then A3: not 2 * 3 divides n by NUMBER04:3;
( not 2 divides n + 1 or not 3 divides n + 1 ) by A2, XPRIMES1:2, XPRIMES1:3;
then A4: not 2 * 3 divides n + 1 by NUMBER04:3;
( not 2 divides n + 2 or not 3 divides n + 2 ) by A2, XPRIMES1:2, XPRIMES1:3;
then A5: not 2 * 3 divides n + 2 by NUMBER04:3;
consider k being Nat such that
A6: ( n = 6 * k or n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 ) by NUMBER02:26;
A7: n is having_exactly_one_prime_divisor
proof
consider p being Element of NAT such that
A8: p is prime and
A9: p divides n by A1, XXREAL_0:2, INT_2:31;
reconsider p = p as Prime by A8;
take p ; :: according to NUMBER08:def 6 :: thesis: ( p divides n & ( for r being Prime st r <> p holds
not r divides n ) )
thus ( p divides n & ( for r being Prime st r <> p holds
not r divides n ) ) by A2, A9; :: thesis: verum
end;
A10: n + 1 is having_exactly_one_prime_divisor
proof
n + 1 > n + 0 by XREAL_1:8;
then n + 1 > 7 by A1, XXREAL_0:2;
then consider p being Element of NAT such that
A11: p is prime and
A12: p divides n + 1 by INT_2:31, XXREAL_0:2;
reconsider p = p as Prime by A11;
take p ; :: according to NUMBER08:def 6 :: thesis: ( p divides n + 1 & ( for r being Prime st r <> p holds
not r divides n + 1 ) )
thus ( p divides n + 1 & ( for r being Prime st r <> p holds
not r divides n + 1 ) ) by A2, A12; :: thesis: verum
end;
A13: n + 2 is having_exactly_one_prime_divisor
proof
n + 2 > n + 0 by XREAL_1:8;
then n + 2 > 7 by A1, XXREAL_0:2;
then consider p being Element of NAT such that
A14: p is prime and
A15: p divides n + 2 by INT_2:31, XXREAL_0:2;
reconsider p = p as Prime by A14;
take p ; :: according to NUMBER08:def 6 :: thesis: ( p divides n + 2 & ( for r being Prime st r <> p holds
not r divides n + 2 ) )
thus ( p divides n + 2 & ( for r being Prime st r <> p holds
not r divides n + 2 ) ) by A2, A15; :: thesis: verum
end;
per cases ( n = 6 * k or n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 ) by A6;
suppose n = 6 * k ; :: thesis: contradiction
hence contradiction by A3; :: thesis: verum
end;
suppose A16: n = (6 * k) + 1 ; :: thesis: contradiction
consider m being non zero Nat such that
A17: n + 1 = (the_only_divisor_of (n + 1)) |^ m by A10, Th78;
n + 1 = 2 * ((3 * k) + 1) by A16;
then 2 divides n + 1 ;
then A18: the_only_divisor_of (n + 1) = 2 by A10, Def7, XPRIMES1:2;
consider s being non zero Nat such that
A19: n + 2 = (the_only_divisor_of (n + 2)) |^ s by A13, Th78;
n + 2 = 3 * ((2 * k) + 1) by A16;
then 3 divides n + 2 ;
then A20: the_only_divisor_of (n + 2) = 3 by A13, Def7, XPRIMES1:3;
A21: now :: thesis: not m <= 3
assume m <= 3 ; :: thesis: contradiction
then n + 1 <= 7 + 1 by A17, A18, Lm12, PREPOWER:93;
hence contradiction by A1, XREAL_1:8; :: thesis: verum
end;
(3 |^ s) - (2 |^ m) = 1 by A17, A19, A18, A20;
then ( ( s = m & m = 1 ) or ( s = 2 & m = 3 ) ) by Th73;
hence contradiction by A21; :: thesis: verum
end;
suppose A22: n = (6 * k) + 2 ; :: thesis: contradiction
consider m being non zero Nat such that
A23: n = (the_only_divisor_of n) |^ m by A7, Th78;
n = 2 * ((3 * k) + 1) by A22;
then 2 divides n ;
then A24: the_only_divisor_of n = 2 by A7, Def7, XPRIMES1:2;
consider s being non zero Nat such that
A25: n + 1 = (the_only_divisor_of (n + 1)) |^ s by A10, Th78;
n + 1 = 3 * ((2 * k) + 1) by A22;
then 3 divides n + 1 ;
then A26: the_only_divisor_of (n + 1) = 3 by A10, Def7, XPRIMES1:3;
(3 |^ s) - (2 |^ m) = 1 by A23, A25, A24, A26;
then ( ( s = m & m = 1 ) or ( s = 2 & m = 3 ) ) by Th73;
hence contradiction by A27; :: thesis: verum
end;
suppose A30: n = (6 * k) + 3 ; :: thesis: contradiction
consider s being non zero Nat such that
A31: n = (the_only_divisor_of n) |^ s by A7, Th78;
n = 3 * ((2 * k) + 1) by A30;
then 3 divides n ;
then A32: the_only_divisor_of n = 3 by A7, Def7, XPRIMES1:3;
consider m being non zero Nat such that
A33: n + 1 = (the_only_divisor_of (n + 1)) |^ m by A10, Th78;
n + 1 = 2 * ((3 * k) + 2) by A30;
then 2 divides n + 1 ;
then A34: the_only_divisor_of (n + 1) = 2 by A10, Def7, XPRIMES1:2;
A35: now :: thesis: not m <= 3
assume m <= 3 ; :: thesis: contradiction
then n + 1 <= 7 + 1 by A33, A34, Lm12, PREPOWER:93;
hence contradiction by A1, XREAL_1:8; :: thesis: verum
end;
(2 |^ m) - (3 |^ s) = 1 by A33, A31, A34, A32;
then ( s = 1 & m = 2 ) by Th67;
hence contradiction by A35; :: thesis: verum
end;
suppose n = (6 * k) + 4 ; :: thesis: contradiction
then n + 2 = 6 * (k + 1) ;
hence contradiction by A5; :: thesis: verum
end;
suppose n = (6 * k) + 5 ; :: thesis: contradiction
then n + 1 = 6 * (k + 1) ;
hence contradiction by A4; :: thesis: verum
end;
end;