let p, q, r be Prime; :: thesis: ( p = 127 & q = 3697 & r = 5227 implies p * (p + 1),q * (q + 1),r * (r + 1) form_an_AP )
assume A1: ( p = 127 & q = 3697 & r = 5227 ) ; :: thesis: p * (p + 1),q * (q + 1),r * (r + 1) form_an_AP
then A3: q * (q + 1) = 13671506 ;
T1: Triangle 127 = (127 * (127 + 1)) / 2 by NUMPOLY1:19
.= 8128 ;
T2: Triangle 3697 = (3697 * (3697 + 1)) / 2 by NUMPOLY1:19
.= 6835753 ;
(q * (q + 1)) - (p * (p + 1)) = (r * (r + 1)) - (q * (q + 1)) by A1;
hence p * (p + 1),q * (q + 1),r * (r + 1) form_an_AP by NUMBER06:def 9; :: thesis: verum