let k be Nat; for x, y being Nat st x = (36 * k) + 14 & y = ((12 * k) + 5) * ((18 * k) + 7) holds
x,y satisfy_Sierpinski_problem_35
let x, y be Nat; ( x = (36 * k) + 14 & y = ((12 * k) + 5) * ((18 * k) + 7) implies x,y satisfy_Sierpinski_problem_35 )
assume that
A1:
x = (36 * k) + 14
and
A2:
y = ((12 * k) + 5) * ((18 * k) + 7)
; x,y satisfy_Sierpinski_problem_35
A3:
( x * (x + 1) = ((2 * 3) * ((12 * k) + 5)) * ((18 * k) + 7) & ((2 * 3) * ((12 * k) + 5)) * ((18 * k) + 7) = 6 * y )
by A1, A2;
y + 1 = 6 * ((((36 * k) * k) + (29 * k)) + 6)
by A2;
then
6 divides y + 1
;
hence
x * (x + 1) divides y * (y + 1)
by A2, A3, INT_4:7; NUMBER05:def 2 ( not x divides y & not x + 1 divides y & not x divides y + 1 & not x + 1 divides y + 1 )
A4:
x = 2 * ((18 * k) + 7)
by A1;
y = (2 * ((((108 * k) * k) + (87 * k)) + 17)) + 1
by A2;
hence
not x divides y
by A4; ( not x + 1 divides y & not x divides y + 1 & not x + 1 divides y + 1 )
A5:
x + 1 = 3 * ((12 * k) + 5)
by A1;
then A6:
3 divides x + 1
;
y = (3 * ((((72 * k) * k) + (58 * k)) + 11)) + 2
by A2;
hence
not x + 1 divides y
by A6, INT_2:9, NAT_4:9; ( not x divides y + 1 & not x + 1 divides y + 1 )
0 + 7 <= (18 * k) + 7
by XREAL_1:6;
then A7:
(18 * k) + 7 <> 1
;
A8:
(18 * k) + 7 divides x
by A4;
(18 * k) + 7 divides y
by A2;
then
not (18 * k) + 7 divides y + 1
by A7, NEWTON:39;
hence
not x divides y + 1
by A8, INT_2:9; not x + 1 divides y + 1
0 + 5 <= (12 * k) + 5
by XREAL_1:6;
then A9:
(12 * k) + 5 <> 1
;
A10:
(12 * k) + 5 divides x + 1
by A5;
(12 * k) + 5 divides y
by A2;
then
not (12 * k) + 5 divides y + 1
by A9, NEWTON:39;
hence
not x + 1 divides y + 1
by A10, INT_2:9; verum