let m, n be positive Integer; :: thesis: ( n > 40 * m implies for A being finite set st A = { [x,y] where x, y is positive Integer : (3 * x) + (5 * y) = n } holds
card A > m )
assume A1: n > 40 * m ; :: thesis: for A being finite set st A = { [x,y] where x, y is positive Integer : (3 * x) + (5 * y) = n } holds
card A > m
let A be finite set ; :: thesis: ( A = { [x,y] where x, y is positive Integer : (3 * x) + (5 * y) = n } implies card A > m )
assume A2: A = { [x,y] where x, y is positive Integer : (3 * x) + (5 * y) = n } ; :: thesis: card A > m
reconsider M = m as positive Nat by TARSKI:1;
m >= 0 + 1 by NAT_1:13;
then A3: 40 * m >= 40 * 1 by XREAL_1:64;
then 40 * m > 7 by XXREAL_0:2;
then A4: n > 7 by A1, XXREAL_0:2;

now :: thesis: not n in {9,10,12,15}

assume n in {9,10,12,15} ; :: thesis: contradiction
then ( n = 9 or n = 10 or n = 12 or n = 15 ) by ENUMSET1:def 2;
hence contradiction by A1, A3, XXREAL_0:2; :: thesis: verum

end;

then consider x0, y0 being positive Integer such that
A5: (3 * x0) + (5 * y0) = n by A4, Th74;

now :: thesis: ( x0 <= 5 * m implies not y0 <= 5 * m )

assume ( x0 <= 5 * m & y0 <= 5 * m ) ; :: thesis: contradiction
then ( 3 * x0 <= 3 * (5 * m) & 5 * y0 <= 5 * (5 * m) ) by XREAL_1:64;
then n <= (15 * m) + (25 * m) by A5, XREAL_1:7;
hence contradiction by A1; :: thesis: verum

end;

per cases then ( x0 > 5 * m or y0 > 5 * m ) ;

suppose A6: x0 > 5 * m ; :: thesis: card A > m

deffunc H₁( Nat) -> set = x0 - (5 * $1);
deffunc H₂( Nat) -> set = y0 + (3 * $1);
deffunc H₃( Nat) -> object = [H₁($1),H₂($1)];
deffunc H₄( Nat) -> set = (3 * H₁($1)) + (5 * H₂($1));
set K = { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } ;
m + 1, { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } are_equipotent

proof

defpred S₁[ object , object ] means ex k being Nat st
( k = $1 & $2 = H₃(k) );
A7: for e being object st e in M + 1 holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in M + 1 implies ex u being object st S₁[e,u] )
assume e in M + 1 ; :: thesis: ex u being object st S₁[e,u]
then reconsider e = e as Nat ;
take H₃(e) ; :: thesis: S₁[e,H₃(e)]
take e ; :: thesis: ( e = e & H₃(e) = H₃(e) )
thus ( e = e & H₃(e) = H₃(e) ) ; :: thesis: verum

end;

consider f being Function such that
A8: dom f = M + 1 and
A9: for e being object st e in M + 1 holds
S₁[e,f . e] from CLASSES1:sch 1(A7);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = m + 1 & proj2 f = { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } )
thus f is one-to-one :: thesis: ( proj1 f = m + 1 & proj2 f = { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } )

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A10: x1 in dom f and
A11: x2 in dom f and
A12: f . x1 = f . x2 ; :: thesis: x1 = x2
consider k1 being Nat such that
A13: k1 = x1 and
A14: f . x1 = H₃(k1) by A8, A9, A10;
consider k2 being Nat such that
A15: k2 = x2 and
A16: f . x2 = H₃(k2) by A8, A9, A11;
H₁(k1) = H₁(k2) by A12, A14, A16, XTUPLE_0:1;
hence x1 = x2 by A13, A15; :: thesis: verum

end;

thus dom f = m + 1 by A8; :: thesis: proj2 f = { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) }
thus rng f c= { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } :: according to XBOOLE_0:def 10 :: thesis: { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } c= proj2 f

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng f or u in { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } )
assume u in rng f ; :: thesis: u in { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) }
then consider e being object such that
A17: e in dom f and
A18: f . e = u by FUNCT_1:def 3;
consider k being Nat such that
A19: k = e and
A20: f . e = H₃(k) by A8, A9, A17;
k in Segm (M + 1) by A8, A17, A19;
then k < M + 1 by NAT_1:44;
then A21: k <= m by NAT_1:13;
n = H₄(k) by A5;
hence u in { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } by A18, A20, A21; :: thesis: verum

end;

thus { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } c= rng f :: thesis: verum

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } or u in rng f )
assume u in { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } ; :: thesis: u in rng f
then consider k being Nat such that
A22: u = H₃(k) and
A23: k <= m and
( H₄(k) > 0 & n = H₄(k) ) ;
k < m + 1 by A23, NAT_1:13;
then A24: k in Segm (M + 1) by NAT_1:44;
then S₁[k,f . k] by A9;
hence u in rng f by A8, A22, A24, FUNCT_1:def 3; :: thesis: verum

end;

end;

then A25: card { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } = card (M + 1) by CARD_1:5;
then reconsider K = { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } as finite set ;
K c= A

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in K or q in A )
assume q in K ; :: thesis: q in A
then consider k being Nat such that
A26: q = H₃(k) and
A27: k <= m and
A28: ( H₄(k) > 0 & n = H₄(k) ) ;
5 * k <= 5 * m by A27, XREAL_1:64;
then H₁(k) > (5 * m) - (5 * m) by A6, XREAL_1:14;
hence q in A by A2, A26, A28; :: thesis: verum

end;

then card K <= card A by NAT_1:43;
hence m < card A by A25, XXREAL_0:2, NAT_1:16; :: thesis: verum

end;

suppose A29: y0 > 5 * m ; :: thesis: card A > m

deffunc H₁( Nat) -> set = x0 + (5 * $1);
deffunc H₂( Nat) -> set = y0 - (3 * $1);
deffunc H₃( Nat) -> object = [H₁($1),H₂($1)];
deffunc H₄( Nat) -> set = (3 * H₁($1)) + (5 * H₂($1));
set K = { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } ;
m + 1, { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } are_equipotent

proof

defpred S₁[ object , object ] means ex k being Nat st
( k = $1 & $2 = H₃(k) );
A30: for e being object st e in M + 1 holds
ex u being object st S₁[e,u]

proof

let e be object ; :: thesis: ( e in M + 1 implies ex u being object st S₁[e,u] )
assume e in M + 1 ; :: thesis: ex u being object st S₁[e,u]
then reconsider e = e as Nat ;
take H₃(e) ; :: thesis: S₁[e,H₃(e)]
take e ; :: thesis: ( e = e & H₃(e) = H₃(e) )
thus ( e = e & H₃(e) = H₃(e) ) ; :: thesis: verum

end;

consider f being Function such that
A31: dom f = M + 1 and
A32: for e being object st e in M + 1 holds
S₁[e,f . e] from CLASSES1:sch 1(A30);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = m + 1 & proj2 f = { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } )
thus f is one-to-one :: thesis: ( proj1 f = m + 1 & proj2 f = { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } )

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A33: x1 in dom f and
A34: x2 in dom f and
A35: f . x1 = f . x2 ; :: thesis: x1 = x2
consider k1 being Nat such that
A36: k1 = x1 and
A37: f . x1 = H₃(k1) by A31, A32, A33;
consider k2 being Nat such that
A38: k2 = x2 and
A39: f . x2 = H₃(k2) by A31, A32, A34;
H₁(k1) = H₁(k2) by A35, A37, A39, XTUPLE_0:1;
hence x1 = x2 by A36, A38; :: thesis: verum

end;

thus dom f = m + 1 by A31; :: thesis: proj2 f = { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) }
thus rng f c= { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } :: according to XBOOLE_0:def 10 :: thesis: { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } c= proj2 f

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng f or u in { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } )
assume u in rng f ; :: thesis: u in { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) }
then consider e being object such that
A40: e in dom f and
A41: f . e = u by FUNCT_1:def 3;
consider k being Nat such that
A42: k = e and
A43: f . e = H₃(k) by A31, A32, A40;
k in Segm (M + 1) by A31, A40, A42;
then k < M + 1 by NAT_1:44;
then A44: k <= m by NAT_1:13;
n = H₄(k) by A5;
hence u in { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } by A41, A43, A44; :: thesis: verum

end;

thus { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } c= rng f :: thesis: verum

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } or u in rng f )
assume u in { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } ; :: thesis: u in rng f
then consider k being Nat such that
A45: u = H₃(k) and
A46: k <= m and
( H₄(k) > 0 & n = H₄(k) ) ;
k < m + 1 by A46, NAT_1:13;
then A47: k in Segm (M + 1) by NAT_1:44;
then S₁[k,f . k] by A32;
hence u in rng f by A31, A45, A47, FUNCT_1:def 3; :: thesis: verum

end;

end;

then A48: card { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } = card (M + 1) by CARD_1:5;
then reconsider K = { H₃(k) where k is Nat : ( k <= m & H₄(k) > 0 & n = H₄(k) ) } as finite set ;
K c= A

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in K or q in A )
assume q in K ; :: thesis: q in A
then consider k being Nat such that
A49: q = H₃(k) and
A50: k <= m and
A51: ( H₄(k) > 0 & n = H₄(k) ) ;
3 * k <= 3 * m by A50, XREAL_1:64;
then H₂(k) > (5 * m) - (3 * m) by A29, XREAL_1:14;
then H₂(k) > 2 * m ;
hence q in A by A2, A49, A51; :: thesis: verum

end;

then card K <= card A by NAT_1:43;
hence m < card A by A48, XXREAL_0:2, NAT_1:16; :: thesis: verum

end;

end;