let n be positive Integer; :: thesis: ( ( n <= 7 or n in {9,10,12,15} ) iff for x, y being positive Integer holds not (3 * x) + (5 * y) = n )
thus ( ( n <= 7 or n in {9,10,12,15} ) implies for x, y being positive Integer holds not (3 * x) + (5 * y) = n ) :: thesis: ( ex x, y being positive Integer st (3 * x) + (5 * y) = n or n <= 7 or n in {9,10,12,15} )
proof
assume A1: ( n <= 7 or n in {9,10,12,15} ) ; :: thesis: for x, y being positive Integer holds not (3 * x) + (5 * y) = n
given x, y being positive Integer such that A2: (3 * x) + (5 * y) = n ; :: thesis: contradiction
x >= 0 + 1 by NAT_1:13;
then A3: 3 * x >= 3 * 1 by XREAL_1:64;
y >= 0 + 1 by NAT_1:13;
then A4: 5 * y >= 5 * 1 by XREAL_1:64;
per cases ( n <= 7 or n in {9,10,12,15} ) by A1;
suppose A5: n <= 7 ; :: thesis: contradiction
(3 * x) + (5 * y) >= 3 + 5 by A3, A4, XREAL_1:7;
hence contradiction by A2, A5, XXREAL_0:2; :: thesis: verum
end;
suppose n in {9,10,12,15} ; :: thesis: contradiction
per cases then ( n = 3 * 3 or n = 3 * 4 or n = 3 * 5 or n = 5 * 2 ) by ENUMSET1:def 2;
suppose A6: ( n = 3 * 3 or n = 3 * 4 or n = 3 * 5 ) ; :: thesis: contradiction
then A7: 3 divides n ;
3 divides 3 * x ;
then A8: 3 divides n - (3 * x) by A7, INT_5:1;
5 divides 5 * y ;
then 3 * 5 divides 5 * y by A2, A8, XPRIMES1:3, XPRIMES1:5, INT_2:30, PEPIN:4;
then ( 9 - (3 * x) >= 15 or 12 - (3 * x) >= 15 or 15 - (3 * x) >= 15 ) by A2, A6, INT_2:27;
then ( 3 * x <= 9 - 15 or 3 * x <= 12 - 15 or 3 * x <= 15 - 15 ) by XREAL_1:11;
hence contradiction by A3, XXREAL_0:2; :: thesis: verum
end;
end;
end;
end;
end;
assume A12: for x, y being positive Integer holds (3 * x) + (5 * y) <> n ; :: thesis: ( n <= 7 or n in {9,10,12,15} )
assume A13: n > 7 ; :: thesis: n in {9,10,12,15}
assume A14: not n in {9,10,12,15} ; :: thesis: contradiction
n is Nat by TARSKI:1;
then consider k being Nat such that
A15: ( n = 3 * k or n = (3 * k) + 1 or n = (3 * k) + 2 ) by NUMBER02:23;
per cases ( n = 3 * k or n = (3 * k) + 1 or n = (3 * k) + 2 ) by A15;
suppose A16: n = 3 * k ; :: thesis: contradiction
set x = k - 5;
set y = 3;
A17: now :: thesis: not k - 5 <= 0
assume k - 5 <= 0 ; :: thesis: contradiction
then k <= 0 + 5 by XREAL_1:20;
then 3 * k <= 3 * 5 by XREAL_1:64;
then A18: not not n = 0 & ... & not n = 15 by A16;
A19: (3 * k) mod 3 = 0 by NAT_D:13;
( ((2 * 3) + 2) mod 3 = 2 mod 3 & ((3 * 3) + 2) mod 3 = 2 mod 3 & ((4 * 3) + 1) mod 3 = 1 mod 3 & ((4 * 3) + 2) mod 3 = 2 mod 3 ) by NAT_D:21;
hence contradiction by A13, A14, A16, A18, A19, NAT_D:24, ENUMSET1:def 2; :: thesis: verum
end;
(3 * (k - 5)) + (5 * 3) = n by A16;
hence contradiction by A12, A17; :: thesis: verum
end;
suppose A20: n = (3 * k) + 1 ; :: thesis: contradiction
set x = k - 3;
set y = 2;
A21: now :: thesis: not k - 3 <= 0
assume k - 3 <= 0 ; :: thesis: contradiction
then k <= 0 + 3 by XREAL_1:20;
then 3 * k <= 3 * 3 by XREAL_1:64;
then (3 * k) + 1 <= (3 * 3) + 1 by XREAL_1:6;
then A22: not not n = 0 & ... & not n = 10 by A20;
A23: ((3 * k) + 1) mod 3 = 1 mod 3 by NAT_D:21
.= 1 by NAT_D:24 ;
((2 * 3) + 2) mod 3 = 2 mod 3 by NAT_D:21;
hence contradiction by A13, A14, A20, A22, A23, NAT_D:24, ENUMSET1:def 2; :: thesis: verum
end;
(3 * (k - 3)) + (5 * 2) = n by A20;
hence contradiction by A12, A21; :: thesis: verum
end;
suppose A24: n = (3 * k) + 2 ; :: thesis: contradiction
set x = k - 1;
set y = 1;
A25: now :: thesis: not k - 1 <= 0
assume k - 1 <= 0 ; :: thesis: contradiction
then k <= 0 + 1 by XREAL_1:20;
then 3 * k <= 3 * 1 by XREAL_1:64;
then (3 * k) + 2 <= (3 * 1) + 2 by XREAL_1:6;
then not not n = 0 & ... & not n = 5 by A24;
hence contradiction by A13; :: thesis: verum
end;
(3 * (k - 1)) + (5 * 1) = n by A24;
hence contradiction by A12, A25; :: thesis: verum
end;
end;