let b, c be Nat; :: thesis: for r being Real st b <> 0 & c <> 0 holds
((r * b) + c) / b > r
let r be Real; :: thesis: ( b <> 0 & c <> 0 implies ((r * b) + c) / b > r )
assume that
A1: b <> 0 and
A2: c <> 0 ; :: thesis: ((r * b) + c) / b > r
A3: ((r * b) + c) / b = ((r * b) / b) + (c / b)
.= r + (c / b) by A1, XCMPLX_1:89 ;
r + (c / b) > r + 0 by A1, A2, XREAL_1:8;
hence ((r * b) + c) / b > r by A3; :: thesis: verum