let a, b, c be Real; :: thesis: ( a > 0 & b >= 0 & c >= 0 & b < a & c < a implies for i being Integer st b = c + (a * i) holds
b = c )
assume that
A1: a > 0 and
A2: b >= 0 and
A3: c >= 0 and
A4: b < a and
A5: c < a ; :: thesis: for i being Integer st b = c + (a * i) holds
b = c
A6: 0 + a <= c + a by A3, XREAL_1:7;
let i be Integer; :: thesis: ( b = c + (a * i) implies b = c )
assume A7: b = c + (a * i) ; :: thesis: b = c

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

suppose i < 0 ; :: thesis: b = c

then i <= - 1 by INT_1:8;
then a * i <= a * (- 1) by A1, XREAL_1:64;
then c + (a * i) <= c - a by XREAL_1:7;
hence b = c by A2, A5, A7, XREAL_1:49; :: thesis: verum

end;

suppose i = 0 ; :: thesis: b = c

hence b = c by A7; :: thesis: verum

end;

suppose i > 0 ; :: thesis: b = c

then 0 + 1 <= i by INT_1:7;
then a * i >= a by A1, XREAL_1:151;
then c + (a * i) >= c + a by XREAL_1:7;
hence b = c by A4, A7, A6, XXREAL_0:2; :: thesis: verum

end;

end;