let n be Nat; :: thesis: ( n is even & n > 8 implies n satisfies_Sierpinski_problem_48 )
assume that
A1: n is even and
A2: n > 8 ; :: thesis: n satisfies_Sierpinski_problem_48
consider k being Nat such that
A3: ( 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;
( (6 * k) + 1 = (2 * (3 * k)) + 1 & (6 * k) + 3 = (2 * ((3 * k) + 1)) + 1 & (6 * k) + 5 = (2 * ((3 * k) + 2)) + 1 ) ;

per cases then ( n = 6 * k or n = (6 * k) + 2 or n = (6 * k) + 4 ) by A1, A3;

suppose A4: n = 6 * k ; :: thesis: n satisfies_Sierpinski_problem_48

then A5: (6 * k) - 5 > 8 - 5 by A2, XREAL_1:9;
then (6 * k) - 5 > 3 ;
then reconsider c = (6 * (k - 1)) + 1 as Element of NAT by INT_1:3;
take a = 2; :: 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 = 3; :: thesis: ex c being Nat st
( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
take c ; :: thesis: ( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
thus n = (a + b) + c by A4; :: thesis: ( a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
thus a > 1 ; :: thesis: ( b > 1 & c > 1 & a,b,c are_mutually_coprime )
thus b > 1 ; :: thesis: ( c > 1 & a,b,c are_mutually_coprime )
thus c > 1 by A5, XXREAL_0:2; :: thesis: a,b,c are_mutually_coprime
thus a,b are_coprime by XPRIMES1:2, XPRIMES1:3, INT_2:30; :: according to NUMBER03:def 1 :: thesis: ( a,c are_coprime & b,c are_coprime )
2 divides 2 * (3 * (k - 1)) ;
hence a,c are_coprime by Th5; :: thesis: b,c are_coprime
3 divides 3 * (2 * (k - 1)) ;
hence b,c are_coprime by Th5; :: thesis: verum

end;

suppose A6: n = (6 * k) + 2 ; :: thesis: n satisfies_Sierpinski_problem_48

then A7: ((6 * k) + 2) - 7 > 8 - 7 by A2, XREAL_1:9;
then reconsider c = (6 * (k - 1)) + 1 as Element of NAT by INT_1:3;
take a = 3; :: 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 = 4; :: thesis: ex c being Nat st
( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
take c ; :: thesis: ( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
thus n = (a + b) + c by A6; :: thesis: ( a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
thus a > 1 ; :: thesis: ( b > 1 & c > 1 & a,b,c are_mutually_coprime )
thus b > 1 ; :: thesis: ( c > 1 & a,b,c are_mutually_coprime )
thus c > 1 by A7; :: thesis: a,b,c are_mutually_coprime
4 = 3 + 1 ;
hence a,b are_coprime by Th5; :: according to NUMBER03:def 1 :: thesis: ( a,c are_coprime & b,c are_coprime )
3 divides 3 * (2 * (k - 1)) ;
hence a,c are_coprime by Th5; :: thesis: b,c are_coprime
A8: 1 divides b by INT_2:12;
A9: 1 divides c by INT_2:12;
for d being Nat st d divides b & d divides c holds
d divides 1

proof

let d be Nat; :: thesis: ( d divides b & d divides c implies d divides 1 )
assume that
A10: d divides b and
A11: d divides c ; :: thesis: d divides 1
A12: 4 = 2 * 2 ;
A13: c = (2 * (3 * (k - 1))) + 1 ;
( d = 1 or d = 2 or d = 4 ) by A10, NUMBER05:21;
hence d divides 1 by A11, A12, A13; :: thesis: verum

end;

hence b,c are_coprime by A8, A9, NAT_D:def 5; :: thesis: verum

end;

suppose A14: n = (6 * k) + 4 ; :: thesis: n satisfies_Sierpinski_problem_48

then A15: ((6 * k) + 4) - 5 > 8 - 5 by A2, XREAL_1:9;
then (6 * k) - 1 > 3 ;
then reconsider c = (6 * k) - 1 as Element of NAT by INT_1:3;
take a = 2; :: 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 = 3; :: thesis: ex c being Nat st
( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
take c ; :: thesis: ( n = (a + b) + c & a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
thus n = (a + b) + c by A14; :: thesis: ( a > 1 & b > 1 & c > 1 & a,b,c are_mutually_coprime )
thus a > 1 ; :: thesis: ( b > 1 & c > 1 & a,b,c are_mutually_coprime )
thus b > 1 ; :: thesis: ( c > 1 & a,b,c are_mutually_coprime )
thus c > 1 by A15, XXREAL_0:2; :: thesis: a,b,c are_mutually_coprime
thus a,b are_coprime by XPRIMES1:2, XPRIMES1:3, INT_2:30; :: according to NUMBER03:def 1 :: thesis: ( a,c are_coprime & b,c are_coprime )
2 divides 2 * (3 * k) ;
hence a,c are_coprime by Th6; :: thesis: b,c are_coprime
3 divides 3 * (2 * k) ;
hence b,c are_coprime by Th6; :: thesis: verum

end;

end;