given a, b, c being Nat such that A1:
17 = (a + b) + c
and
A2:
a > 1
and
A3:
b > 1
and
A4:
c > 1
and
A5:
a,b,c are_mutually_coprime
; NUMBER07:def 1 contradiction
A6:
17 = (2 * 8) + 1
;
then
a is odd
by A1, A5, Th7;
then A7:
( a = 3 or a = 5 or a = 7 or a = 9 or a = 11 or a = 13 )
by A1, A2, A3, A4, Lm4, Lm3;
b is odd
by A1, A5, A6, Th7;
then A8:
( b = 3 or b = 5 or b = 7 or b = 9 or b = 11 or b = 13 )
by A1, A2, A3, A4, Lm4, Lm3;
A9:
c is odd
by A1, A5, A6, Th7;
(a + b) + c = (c + a) + b
;
then A10:
( c = 3 or c = 5 or c = 7 or c = 9 or c = 11 or c = 13 )
by A1, A2, A3, A4, A9, Lm4, Lm3;
not 3,3 * 3 are_coprime
by Th1;
hence
contradiction
by A1, A5, A7, A8, A10, EULER_1:1; verum