let a be Integer; :: thesis: for b being non zero Integer
for c being negative Integer holds [\(a / (b * c))/] = [\([\(- (a / b))/] / (- c))/]
let b be non zero Integer; :: thesis: for c being negative Integer holds [\(a / (b * c))/] = [\([\(- (a / b))/] / (- c))/]
let c be negative Integer; :: thesis: [\(a / (b * c))/] = [\([\(- (a / b))/] / (- c))/]
- c in NAT by INT_1:3;
then reconsider k = - c as Nat ;
[\([\(- (a / b))/] / (- c))/] = [\([\((- a) / b)/] / k)/]
.= [\((- a) / (b * k))/] by N227
.= [\((- a) / (- (b * c)))/]
.= [\(a / (b * c))/] by XCMPLX_1:191 ;
hence [\(a / (b * c))/] = [\([\(- (a / b))/] / (- c))/] ; :: thesis: verum