let x, y, z be Nat; ( y = (5 * x) + 2 & z = (7 * x) + 3 implies ( x * (x + 1),y * (y + 1),z * (z + 1) form_an_AP & x < y & y < z ) )
assume A1:
( y = (5 * x) + 2 & z = (7 * x) + 3 )
; ( x * (x + 1),y * (y + 1),z * (z + 1) form_an_AP & x < y & y < z )
t0:
1 * x <= 5 * x
by XREAL_1:64;
TT:
(5 * x) + 0 < (5 * x) + 2
by XREAL_1:8;
5 * x <= 7 * x
by XREAL_1:64;
hence
( x * (x + 1),y * (y + 1),z * (z + 1) form_an_AP & x < y & y < z )
by TT, A1, XREAL_1:8, t0, XXREAL_0:2; verum