let n be Nat; :: thesis: ( n > 17 implies n satisfies_Sierpinski_problem_48 )
assume A1: n > 17 ; :: thesis: n satisfies_Sierpinski_problem_48
per cases ( n is even or n is odd ) ;
suppose A2: n is even ; :: thesis: n satisfies_Sierpinski_problem_48
n > 8 by A1, XXREAL_0:2;
hence n satisfies_Sierpinski_problem_48 by A2, Th41; :: thesis: verum
end;
suppose A3: n is odd ; :: thesis: n satisfies_Sierpinski_problem_48
consider k being Nat such that
A4: not not n = (12 * k) + 0 & ... & not n = (12 * k) + (12 - 1) by NUMBER02:22;
consider i being Nat such that
A5: ( 0 <= i & i <= 11 ) and
A6: n = (12 * k) + i by A4;
A7: not not i = 0 & ... & not i = 11 by A5;
A8: now :: thesis: not 9 divides (6 * k) - 1
assume 9 divides (6 * k) - 1 ; :: thesis: contradiction
then consider z being Integer such that
A9: (6 * k) - 1 = 9 * z ;
3 divides 3 * ((2 * k) - (3 * z)) ;
hence contradiction by A9, NAT_D:7; :: thesis: verum
end;
A10: now :: thesis: not 9 divides (6 * k) + 1
assume 9 divides (6 * k) + 1 ; :: thesis: contradiction
then consider z being Integer such that
A11: (6 * k) + 1 = 9 * z ;
3 divides 3 * ((3 * z) - (2 * k)) ;
hence contradiction by A11, NAT_D:7; :: thesis: verum
end;
( (12 * k) + 0 = 2 * (6 * k) & (12 * k) + 2 = 2 * ((6 * k) + 1) & (12 * k) + 4 = 2 * ((6 * k) + 2) & (12 * k) + 6 = 2 * ((6 * k) + 3) & (12 * k) + 8 = 2 * ((6 * k) + 4) & (12 * k) + 10 = 2 * ((6 * k) + 5) ) ;
per cases then ( n = (12 * k) + 1 or n = (12 * k) + 3 or n = (12 * k) + 5 or n = (12 * k) + 7 or n = (12 * k) + 9 or n = (12 * k) + 11 ) by A3, A6, A7;
suppose A12: n = (12 * k) + 1 ; :: thesis: n satisfies_Sierpinski_problem_48
then ((12 * k) + 1) - 1 > 17 - 1 by A1, XREAL_1:9;
then (12 * k) / 12 > 16 / 12 by XREAL_1:97;
then A13: k > 1 by XXREAL_0:2;
then A14: 6 * k > 6 * 1 by XREAL_1:68;
k - 1 > 1 - 1 by A13, XREAL_1:9;
then k - 1 >= 0 + 1 by INT_1:7;
then 6 * (k - 1) >= 6 * 1 by XREAL_1:64;
then A15: (6 * (k - 1)) - 1 >= 6 - 1 by XREAL_1:9;
then reconsider a = (6 * (k - 1)) - 1 as Element of NAT by INT_1:3;
A16: (6 * k) - 1 > 6 - 1 by A14, XREAL_1:9;
then reconsider b = (6 * (k - 1)) + 5 as Element of NAT by INT_1:3;
set c = 9;
take a ; :: according to NUMBER07:def 1 :: thesis: ex b, c being Nat st
( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
take b ; :: thesis: ex c being Nat st
( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
take 9 ; :: thesis: ( n = (a + b) + 9 & a > 1 & b > 1 & 9 > 1 & a,b,9 are_mutually_coprime )
thus n = (a + b) + 9 by A12; :: thesis: ( a > 1 & b > 1 & 9 > 1 & a,b,9 are_mutually_coprime )
thus a > 1 by A15, XXREAL_0:2; :: thesis: ( b > 1 & 9 > 1 & a,b,9 are_mutually_coprime )
thus b > 1 by A16, XXREAL_0:2; :: thesis: ( 9 > 1 & a,b,9 are_mutually_coprime )
thus 9 > 1 ; :: thesis: a,b,9 are_mutually_coprime
A17: 1 divides a by INT_2:12;
A18: 1 divides b by INT_2:12;
A19: 1 divides 9 by INT_2:12;
for d being Nat st d divides a & d divides b holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides a & d divides b implies d divides 1 )
assume that
A20: d divides a and
A21: d divides b ; :: thesis: d divides 1
A22: d divides b - a by A20, A21, INT_5:1;
A23: ( 3 divides 3 * (2 * (k - 1)) & 6 divides 6 * (k - 1) ) ;
( d = 1 or d = 2 or d = 3 or d = 6 ) by A22, Th10;
hence d divides 1 by A20, A23, Th4; :: thesis: verum
end;
hence a,b are_coprime by A17, A18, NAT_D:def 5; :: according to NUMBER03:def 1 :: thesis: ( a,9 are_coprime & b,9 are_coprime )
for d being Nat st d divides a & d divides 9 holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides a & d divides 9 implies d divides 1 )
assume that
A24: d divides a and
A25: d divides 9 ; :: thesis: d divides 1
A26: 3 divides 3 * (2 * (k - 1)) ;
A27: now :: thesis: not 9 divides (6 * k) - 7
assume 9 divides (6 * k) - 7 ; :: thesis: contradiction
then consider z being Integer such that
A28: (6 * k) - 7 = 9 * z ;
A29: 3 divides 3 * ((2 * k) - (3 * z)) ;
((2 * 3) + 1) mod 3 = 1 mod 3 by NAT_D:21
.= 1 by NAT_D:24 ;
hence contradiction by A28, A29, INT_1:62; :: thesis: verum
end;
( d = 1 or d = 3 or d = 9 ) by A25, Th11;
hence d divides 1 by A24, A26, A27, Th4; :: thesis: verum
end;
hence a,9 are_coprime by A17, A19, NAT_D:def 5; :: thesis: b,9 are_coprime
for d being Nat st d divides b & d divides 9 holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides b & d divides 9 implies d divides 1 )
assume that
A30: d divides b and
A31: d divides 9 ; :: thesis: d divides 1
A32: 3 divides 3 * (2 * k) ;
( d = 1 or d = 3 or d = 9 ) by A31, Th11;
hence d divides 1 by A30, A32, A8, Th4; :: thesis: verum
end;
hence b,9 are_coprime by A18, A19, NAT_D:def 5; :: thesis: verum
end;
suppose A33: n = (12 * k) + 3 ; :: thesis: n satisfies_Sierpinski_problem_48
then ((12 * k) + 3) - 3 > 17 - 3 by A1, XREAL_1:9;
then (12 * k) / 12 > ((1 * 12) + 2) / 12 by XREAL_1:97;
then k > 1 by XXREAL_0:2;
then A34: 6 * k > 6 * 1 by XREAL_1:68;
then A35: (6 * k) - 1 > 6 - 1 by XREAL_1:9;
then reconsider a = (6 * k) - 1 as Element of NAT by INT_1:3;
set b = (6 * k) + 1;
set c = 3;
take a ; :: according to NUMBER07:def 1 :: thesis: ex b, c being Nat st
( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
take (6 * k) + 1 ; :: thesis: ex c being Nat st
( n = (a + ((6 * k) + 1)) + c & a > 1 & (6 * k) + 1 > 1 & c > 1 & a,(6 * k) + 1,c are_mutually_coprime )
take 3 ; :: thesis: ( n = (a + ((6 * k) + 1)) + 3 & a > 1 & (6 * k) + 1 > 1 & 3 > 1 & a,(6 * k) + 1,3 are_mutually_coprime )
thus n = (a + ((6 * k) + 1)) + 3 by A33; :: thesis: ( a > 1 & (6 * k) + 1 > 1 & 3 > 1 & a,(6 * k) + 1,3 are_mutually_coprime )
thus a > 1 by A35, XXREAL_0:2; :: thesis: ( (6 * k) + 1 > 1 & 3 > 1 & a,(6 * k) + 1,3 are_mutually_coprime )
(6 * k) + 1 > 6 + 1 by A34, XREAL_1:6;
hence (6 * k) + 1 > 1 by XXREAL_0:2; :: thesis: ( 3 > 1 & a,(6 * k) + 1,3 are_mutually_coprime )
thus 3 > 1 ; :: thesis: a,(6 * k) + 1,3 are_mutually_coprime
A36: ( 1 divides a & 1 divides (6 * k) + 1 ) by INT_2:12;
for d being Nat st d divides a & d divides (6 * k) + 1 holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides a & d divides (6 * k) + 1 implies d divides 1 )
assume that
A37: d divides a and
A38: d divides (6 * k) + 1 ; :: thesis: d divides 1
A39: a = (2 * (3 * k)) - 1 ;
d divides ((6 * k) + 1) - a by A37, A38, INT_5:1;
then ( d = 1 or d = 2 ) by Th9;
hence d divides 1 by A37, A39; :: thesis: verum
end;
hence a,(6 * k) + 1 are_coprime by A36, NAT_D:def 5; :: according to NUMBER03:def 1 :: thesis: ( a,3 are_coprime & (6 * k) + 1,3 are_coprime )
A40: 3 divides 3 * (2 * k) ;
hence a,3 are_coprime by Th6; :: thesis: (6 * k) + 1,3 are_coprime
thus (6 * k) + 1,3 are_coprime by A40, Th5; :: thesis: verum
end;
suppose A41: n = (12 * k) + 5 ; :: thesis: n satisfies_Sierpinski_problem_48
then ((12 * k) + 5) - 5 > 17 - 5 by A1, XREAL_1:9;
then (12 * k) / 12 > 12 / 12 by XREAL_1:97;
then A42: 6 * k > 6 * 1 by XREAL_1:68;
then A43: (6 * k) - 5 > 6 - 5 by XREAL_1:9;
then reconsider a = (6 * k) - 5 as Element of NAT by INT_1:3, XXREAL_0:2;
set b = (6 * k) + 1;
set c = 9;
take a ; :: according to NUMBER07:def 1 :: thesis: ex b, c being Nat st
( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
take (6 * k) + 1 ; :: thesis: ex c being Nat st
( n = (a + ((6 * k) + 1)) + c & a > 1 & (6 * k) + 1 > 1 & c > 1 & a,(6 * k) + 1,c are_mutually_coprime )
take 9 ; :: thesis: ( n = (a + ((6 * k) + 1)) + 9 & a > 1 & (6 * k) + 1 > 1 & 9 > 1 & a,(6 * k) + 1,9 are_mutually_coprime )
thus n = (a + ((6 * k) + 1)) + 9 by A41; :: thesis: ( a > 1 & (6 * k) + 1 > 1 & 9 > 1 & a,(6 * k) + 1,9 are_mutually_coprime )
thus a > 1 by A43; :: thesis: ( (6 * k) + 1 > 1 & 9 > 1 & a,(6 * k) + 1,9 are_mutually_coprime )
(6 * k) + 1 > 6 + 1 by A42, XREAL_1:8;
hence (6 * k) + 1 > 1 by XXREAL_0:2; :: thesis: ( 9 > 1 & a,(6 * k) + 1,9 are_mutually_coprime )
thus 9 > 1 ; :: thesis: a,(6 * k) + 1,9 are_mutually_coprime
A44: 1 divides a by INT_2:12;
A45: 1 divides (6 * k) + 1 by INT_2:12;
A46: 1 divides 9 by INT_2:12;
for d being Nat st d divides a & d divides (6 * k) + 1 holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides a & d divides (6 * k) + 1 implies d divides 1 )
assume that
A47: d divides a and
A48: d divides (6 * k) + 1 ; :: thesis: d divides 1
A49: ( 3 divides 3 * (2 * k) & 6 divides 6 * k ) ;
d divides ((6 * k) + 1) - a by A47, A48, INT_5:1;
then ( d = 1 or d = 2 or d = 3 or d = 6 ) by Th10;
hence d divides 1 by A48, A49, Th3; :: thesis: verum
end;
hence a,(6 * k) + 1 are_coprime by A44, A45, NAT_D:def 5; :: according to NUMBER03:def 1 :: thesis: ( a,9 are_coprime & (6 * k) + 1,9 are_coprime )
for d being Nat st d divides a & d divides 9 holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides a & d divides 9 implies d divides 1 )
assume that
A50: d divides a and
A51: d divides 9 ; :: thesis: d divides 1
A52: 3 divides 3 * (2 * (k - 1)) ;
A53: (6 * k) - 5 = (6 * (k - 1)) + 1 ;
A54: now :: thesis: not 9 divides (6 * k) - 5
assume 9 divides (6 * k) - 5 ; :: thesis: contradiction
then consider z being Integer such that
A55: (6 * k) - 5 = 9 * z ;
A56: 3 divides 3 * ((2 * k) - (3 * z)) ;
((1 * 3) + 2) mod 3 = 2 mod 3 by NAT_D:21
.= 2 by NAT_D:24 ;
hence contradiction by A55, A56, INT_1:62; :: thesis: verum
end;
( d = 1 or d = 3 or d = 9 ) by A51, Th11;
hence d divides 1 by A50, A52, A53, A54, Th3; :: thesis: verum
end;
hence a,9 are_coprime by A44, A46, NAT_D:def 5; :: thesis: (6 * k) + 1,9 are_coprime
for d being Nat st d divides (6 * k) + 1 & d divides 9 holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides (6 * k) + 1 & d divides 9 implies d divides 1 )
assume that
A57: d divides (6 * k) + 1 and
A58: d divides 9 ; :: thesis: d divides 1
A59: 3 divides 3 * (2 * k) ;
( d = 1 or d = 3 or d = 9 ) by A58, Th11;
hence d divides 1 by A57, A59, A10, Th3; :: thesis: verum
end;
hence (6 * k) + 1,9 are_coprime by A45, A46, NAT_D:def 5; :: thesis: verum
end;
suppose A60: n = (12 * k) + 7 ; :: thesis: n satisfies_Sierpinski_problem_48
set a = ((6 * k) + 6) - 1;
((12 * k) + 7) - 7 > 17 - 7 by A1, A60, XREAL_1:9;
then (12 * k) / 12 > 10 / 12 by XREAL_1:97;
then A61: k >= 0 + 1 by NAT_1:13;
then reconsider b = (6 * k) - 1 as Element of NAT by INT_1:3;
set c = 3;
take ((6 * k) + 6) - 1 ; :: according to NUMBER07:def 1 :: thesis: ex b, c being Nat st
( n = ((((6 * k) + 6) - 1) + b) + c & ((6 * k) + 6) - 1 > 1 & b > 1 & c > 1 & ((6 * k) + 6) - 1,b,c are_mutually_coprime )
take b ; :: thesis: ex c being Nat st
( n = ((((6 * k) + 6) - 1) + b) + c & ((6 * k) + 6) - 1 > 1 & b > 1 & c > 1 & ((6 * k) + 6) - 1,b,c are_mutually_coprime )
take 3 ; :: thesis: ( n = ((((6 * k) + 6) - 1) + b) + 3 & ((6 * k) + 6) - 1 > 1 & b > 1 & 3 > 1 & ((6 * k) + 6) - 1,b,3 are_mutually_coprime )
thus n = ((((6 * k) + 6) - 1) + b) + 3 by A60; :: thesis: ( ((6 * k) + 6) - 1 > 1 & b > 1 & 3 > 1 & ((6 * k) + 6) - 1,b,3 are_mutually_coprime )
A62: 6 * k >= 6 * 1 by A61, XREAL_1:64;
then (6 * k) + 5 >= 6 + 5 by XREAL_1:6;
hence ((6 * k) + 6) - 1 > 1 by XXREAL_0:2; :: thesis: ( b > 1 & 3 > 1 & ((6 * k) + 6) - 1,b,3 are_mutually_coprime )
(6 * k) - 1 >= 6 - 1 by A62, XREAL_1:9;
hence b > 1 by XXREAL_0:2; :: thesis: ( 3 > 1 & ((6 * k) + 6) - 1,b,3 are_mutually_coprime )
thus 3 > 1 ; :: thesis: ((6 * k) + 6) - 1,b,3 are_mutually_coprime
A63: 1 divides ((6 * k) + 6) - 1 by INT_2:12;
A64: 1 divides b by INT_2:12;
for d being Nat st d divides ((6 * k) + 6) - 1 & d divides b holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides ((6 * k) + 6) - 1 & d divides b implies d divides 1 )
assume that
A65: d divides ((6 * k) + 6) - 1 and
A66: d divides b ; :: thesis: d divides 1
A67: ( 3 divides 3 * (2 * k) & 6 divides 6 * k ) ;
d divides (((6 * k) + 6) - 1) - b by A65, A66, INT_5:1;
then ( d = 1 or d = 2 or d = 3 or d = 6 ) by Th10;
hence d divides 1 by A66, A67, Th4; :: thesis: verum
end;
hence ((6 * k) + 6) - 1,b are_coprime by A63, A64, NAT_D:def 5; :: according to NUMBER03:def 1 :: thesis: ( ((6 * k) + 6) - 1,3 are_coprime & b,3 are_coprime )
3 divides 3 * (2 * (k + 1)) ;
hence ((6 * k) + 6) - 1,3 are_coprime by Th6; :: thesis: b,3 are_coprime
3 divides 3 * (2 * k) ;
hence b,3 are_coprime by Th6; :: thesis: verum
end;
suppose A68: n = (12 * k) + 9 ; :: thesis: n satisfies_Sierpinski_problem_48
then ((12 * k) + 9) - 9 > 17 - 9 by A1, XREAL_1:9;
then A69: (12 * k) / 12 > 8 / 12 by XREAL_1:97;
then reconsider a = (6 * k) - 1 as Element of NAT by INT_1:3;
set b = (6 * k) + 1;
set c = 9;
take a ; :: according to NUMBER07:def 1 :: thesis: ex b, c being Nat st
( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
take (6 * k) + 1 ; :: thesis: ex c being Nat st
( n = (a + ((6 * k) + 1)) + c & a > 1 & (6 * k) + 1 > 1 & c > 1 & a,(6 * k) + 1,c are_mutually_coprime )
take 9 ; :: thesis: ( n = (a + ((6 * k) + 1)) + 9 & a > 1 & (6 * k) + 1 > 1 & 9 > 1 & a,(6 * k) + 1,9 are_mutually_coprime )
thus n = (a + ((6 * k) + 1)) + 9 by A68; :: thesis: ( a > 1 & (6 * k) + 1 > 1 & 9 > 1 & a,(6 * k) + 1,9 are_mutually_coprime )
k >= 0 + 1 by A69, NAT_1:13;
then A70: 6 * k >= 6 * 1 by XREAL_1:64;
then (6 * k) - 1 >= 6 - 1 by XREAL_1:9;
hence a > 1 by XXREAL_0:2; :: thesis: ( (6 * k) + 1 > 1 & 9 > 1 & a,(6 * k) + 1,9 are_mutually_coprime )
(6 * k) + 1 >= 6 + 1 by A70, XREAL_1:6;
hence (6 * k) + 1 > 1 by XXREAL_0:2; :: thesis: ( 9 > 1 & a,(6 * k) + 1,9 are_mutually_coprime )
thus 9 > 1 ; :: thesis: a,(6 * k) + 1,9 are_mutually_coprime
A71: 1 divides a by INT_2:12;
A72: 1 divides (6 * k) + 1 by INT_2:12;
A73: 1 divides 9 by INT_2:12;
for d being Nat st d divides a & d divides (6 * k) + 1 holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides a & d divides (6 * k) + 1 implies d divides 1 )
assume that
A74: d divides a and
A75: d divides (6 * k) + 1 ; :: thesis: d divides 1
A76: a = (2 * (3 * k)) - 1 ;
d divides ((6 * k) + 1) - a by A74, A75, INT_5:1;
then ( d = 1 or d = 2 ) by Th9;
hence d divides 1 by A74, A76; :: thesis: verum
end;
hence a,(6 * k) + 1 are_coprime by A71, A72, NAT_D:def 5; :: according to NUMBER03:def 1 :: thesis: ( a,9 are_coprime & (6 * k) + 1,9 are_coprime )
for d being Nat st d divides a & d divides 9 holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides a & d divides 9 implies d divides 1 )
assume that
A77: d divides a and
A78: d divides 9 ; :: thesis: d divides 1
A79: 3 divides 3 * (2 * k) ;
( d = 1 or d = 3 or d = 9 ) by A78, Th11;
hence d divides 1 by A8, A77, A79, Th4; :: thesis: verum
end;
hence a,9 are_coprime by A71, A73, NAT_D:def 5; :: thesis: (6 * k) + 1,9 are_coprime
for d being Nat st d divides (6 * k) + 1 & d divides 9 holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides (6 * k) + 1 & d divides 9 implies d divides 1 )
assume that
A80: d divides (6 * k) + 1 and
A81: d divides 9 ; :: thesis: d divides 1
A82: 3 divides 3 * (2 * k) ;
( d = 1 or d = 3 or d = 9 ) by A81, Th11;
hence d divides 1 by A10, A80, A82, Th3; :: thesis: verum
end;
hence (6 * k) + 1,9 are_coprime by A72, A73, NAT_D:def 5; :: thesis: verum
end;
suppose A83: n = (12 * k) + 11 ; :: thesis: n satisfies_Sierpinski_problem_48
set a = (6 * k) + 1;
set b = ((6 * k) + 6) + 1;
set c = 3;
take (6 * k) + 1 ; :: according to NUMBER07:def 1 :: thesis: ex b, c being Nat st
( n = (((6 * k) + 1) + b) + c & (6 * k) + 1 > 1 & b > 1 & c > 1 & (6 * k) + 1,b,c are_mutually_coprime )
take ((6 * k) + 6) + 1 ; :: thesis: ex c being Nat st
( n = (((6 * k) + 1) + (((6 * k) + 6) + 1)) + c & (6 * k) + 1 > 1 & ((6 * k) + 6) + 1 > 1 & c > 1 & (6 * k) + 1,((6 * k) + 6) + 1,c are_mutually_coprime )
take 3 ; :: thesis: ( n = (((6 * k) + 1) + (((6 * k) + 6) + 1)) + 3 & (6 * k) + 1 > 1 & ((6 * k) + 6) + 1 > 1 & 3 > 1 & (6 * k) + 1,((6 * k) + 6) + 1,3 are_mutually_coprime )
thus n = (((6 * k) + 1) + (((6 * k) + 6) + 1)) + 3 by A83; :: thesis: ( (6 * k) + 1 > 1 & ((6 * k) + 6) + 1 > 1 & 3 > 1 & (6 * k) + 1,((6 * k) + 6) + 1,3 are_mutually_coprime )
((12 * k) + 11) - 11 > 17 - 11 by A1, A83, XREAL_1:9;
then (12 * k) / 12 > 6 / 12 by XREAL_1:97;
then k >= 0 + 1 by NAT_1:13;
then A84: 6 * k >= 6 * 1 by XREAL_1:64;
then (6 * k) + 1 >= 6 + 1 by XREAL_1:6;
hence (6 * k) + 1 > 1 by XXREAL_0:2; :: thesis: ( ((6 * k) + 6) + 1 > 1 & 3 > 1 & (6 * k) + 1,((6 * k) + 6) + 1,3 are_mutually_coprime )
(6 * k) + 7 >= 6 + 7 by A84, XREAL_1:6;
hence ((6 * k) + 6) + 1 > 1 by XXREAL_0:2; :: thesis: ( 3 > 1 & (6 * k) + 1,((6 * k) + 6) + 1,3 are_mutually_coprime )
thus 3 > 1 ; :: thesis: (6 * k) + 1,((6 * k) + 6) + 1,3 are_mutually_coprime
A85: 1 divides (6 * k) + 1 by INT_2:12;
A86: 1 divides ((6 * k) + 6) + 1 by INT_2:12;
for d being Nat st d divides (6 * k) + 1 & d divides ((6 * k) + 6) + 1 holds
d divides 1
proof
let d be Nat; :: thesis: ( d divides (6 * k) + 1 & d divides ((6 * k) + 6) + 1 implies d divides 1 )
assume that
A87: d divides (6 * k) + 1 and
A88: d divides ((6 * k) + 6) + 1 ; :: thesis: d divides 1
A89: ( 3 divides 3 * (2 * k) & 6 divides 6 * k ) ;
d divides (((6 * k) + 6) + 1) - ((6 * k) + 1) by A87, A88, INT_5:1;
then ( d = 1 or d = 2 or d = 3 or d = 6 ) by Th10;
hence d divides 1 by A87, A89, Th3; :: thesis: verum
end;
hence (6 * k) + 1,((6 * k) + 6) + 1 are_coprime by A85, A86, NAT_D:def 5; :: according to NUMBER03:def 1 :: thesis: ( (6 * k) + 1,3 are_coprime & ((6 * k) + 6) + 1,3 are_coprime )
3 divides 3 * (2 * k) ;
hence (6 * k) + 1,3 are_coprime by Th5; :: thesis: ((6 * k) + 6) + 1,3 are_coprime
3 divides 3 * ((2 * k) + 2) ;
hence ((6 * k) + 6) + 1,3 are_coprime by Th5; :: thesis: verum
end;
end;
end;
end;