let n be Nat; :: thesis: ( n > 6 implies ex a, b being Nat st
( a > 1 & b > 1 & n = a + b & a,b are_coprime ) )
assume A1: n > 6 ; :: thesis: ex a, b being Nat st
( a > 1 & b > 1 & n = a + b & a,b are_coprime )

per cases ( n is odd or n is even ) ;

suppose A2: n is odd ; :: thesis: ex a, b being Nat st
( a > 1 & b > 1 & n = a + b & a,b are_coprime )

2 = 2 * 1 ;
then reconsider a = 2 as even Nat ;
reconsider b = n - a as Element of NAT by A1, XXREAL_0:2, INT_1:5;
take a ; :: thesis: ex b being Nat st
( a > 1 & b > 1 & n = a + b & a,b are_coprime )
take b ; :: thesis: ( a > 1 & b > 1 & n = a + b & a,b are_coprime )
thus a > 1 ; :: thesis: ( b > 1 & n = a + b & a,b are_coprime )
n - a > 6 - a by A1, XREAL_1:14;
hence b > 1 by XXREAL_0:2; :: thesis: ( n = a + b & a,b are_coprime )
thus n = a + b ; :: thesis: a,b are_coprime
2 = 2 |^ 1 ;
hence a,b are_coprime by A2, NAT_5:3; :: thesis: verum

end;

suppose A3: n is even ; :: thesis: ex a, b being Nat st
( a > 1 & b > 1 & n = a + b & a,b are_coprime )

consider k being Nat such that
A4: ( n = 4 * k or n = (4 * k) + 1 or n = (4 * k) + 2 or n = (4 * k) + 3 ) by NUMBER02:24;
( (4 * k) + 1 = (2 * (2 * k)) + 1 & (4 * k) + 3 = (2 * ((2 * k) + 1)) + 1 ) ;

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

suppose A5: n = 4 * k ; :: thesis: ex a, b being Nat st
( a > 1 & b > 1 & n = a + b & a,b are_coprime )

A6: now :: thesis: not 1 >= k

assume 1 >= k ; :: thesis: contradiction
then ( k = 0 or k = 1 ) by NAT_1:25;
hence contradiction by A1, A5; :: thesis: verum

end;

then A7: 2 * 1 < 2 * k by XREAL_1:68;
then reconsider a = (2 * k) - 1 as odd Element of NAT by INT_1:5, XXREAL_0:2;
reconsider b = (2 * k) + 1 as odd Element of NAT ;
take a ; :: thesis: ex b being Nat st
( a > 1 & b > 1 & n = a + b & a,b are_coprime )
take b ; :: thesis: ( a > 1 & b > 1 & n = a + b & a,b are_coprime )
(2 * k) - 1 > 2 - 1 by A7, XREAL_1:9;
hence a > 1 ; :: thesis: ( b > 1 & n = a + b & a,b are_coprime )
1 + 0 < (2 * k) + 1 by A6, XREAL_1:8;
hence b > 1 ; :: thesis: ( n = a + b & a,b are_coprime )
thus n = a + b by A5; :: thesis: a,b are_coprime
b - a = 2 ;
hence a,b are_coprime by NUMBER03:31; :: thesis: verum

end;

suppose A8: n = (4 * k) + 2 ; :: thesis: ex a, b being Nat st
( a > 1 & b > 1 & n = a + b & a,b are_coprime )

reconsider a = ((2 * k) + 2) + 1 as Nat ;
(4 * k) + 2 > 4 + 2 by A1, A8;
then 2 * (2 * k) > 2 * (2 * 1) by XREAL_1:6;
then A9: 2 * k > 2 * 1 by XREAL_1:64;
then A10: 1 <= 2 * k by XXREAL_0:2;
then reconsider b = (2 * k) - 1 as Element of NAT by INT_1:5;
take a ; :: thesis: ex b being Nat st
( a > 1 & b > 1 & n = a + b & a,b are_coprime )
take b ; :: thesis: ( a > 1 & b > 1 & n = a + b & a,b are_coprime )
(2 * k) + 3 > (2 * k) + 0 by XREAL_1:8;
hence a > 1 by A10, XXREAL_0:2; :: thesis: ( b > 1 & n = a + b & a,b are_coprime )
(2 * k) - 1 > (1 + 1) - 1 by A9, XREAL_1:9;
hence b > 1 ; :: thesis: ( n = a + b & a,b are_coprime )
thus n = a + b by A8; :: thesis: a,b are_coprime
A11: ( 1 divides a & 1 divides b ) 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
A12: d divides a and
A13: d divides b ; :: thesis: d divides 1
d divides a - b by A12, A13, INT_5:1;
then ( d = 1 or d = 2 * 1 or d = 2 * 2 ) by Th21;
hence d divides 1 by A12; :: thesis: verum

end;

hence a gcd b = 1 by A11, NAT_D:def 5; :: according to INT_2:def 3 :: thesis: verum

end;

end;

end;

end;