let a, b, c be Nat; :: thesis: ( (a ^2) + (b ^2) = c ^2 & a,b,c form_an_AP implies ex i being Integer st
( a = 3 * i & b = 4 * i & c = 5 * i ) )
assume A1: ( (a ^2) + (b ^2) = c ^2 & a,b,c form_an_AP ) ; :: thesis: ex i being Integer st
( a = 3 * i & b = 4 * i & c = 5 * i )
set r = b - a;

per cases ( b <> 0 or b = 0 ) ;

suppose A2: b <> 0 ; :: thesis: ex i being Integer st
( a = 3 * i & b = 4 * i & c = 5 * i )

((b - (b - a)) ^2) + (b ^2) = (b + (b - a)) ^2 by A1;
then b = ((4 * (b - a)) * b) / b by A2, XCMPLX_1:89;
then A4: b = 4 * (b - a) by A2, XCMPLX_1:89;
then B1: a = 3 * (b - a) ;
B2: c = 5 * (b - a) by A4, A1;
reconsider rr = b - a as Integer ;
take rr ; :: thesis: ( a = 3 * rr & b = 4 * rr & c = 5 * rr )
thus ( a = 3 * rr & b = 4 * rr & c = 5 * rr ) by B1, B2; :: thesis: verum

end;

suppose C1: b = 0 ; :: thesis: ex i being Integer st
( a = 3 * i & b = 4 * i & c = 5 * i )

take i = 0 ; :: thesis: ( a = 3 * i & b = 4 * i & c = 5 * i )
thus ( a = 3 * i & b = 4 * i & c = 5 * i ) by C1, A1; :: thesis: verum

end;

end;