let a, b, c, d be Complex; :: thesis: ( b <> 0 & d <> 0 implies (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d) )
assume A1: b <> 0 ; :: thesis: ( not d <> 0 or (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d) )
assume A2: d <> 0 ; :: thesis: (a / b) - (c / d) = ((a * d) - (c * b)) / (b * d)
thus (a / b) - (c / d) = (a / b) + (- (c / d))
.= (a / b) + ((- c) / d) by Lm17
.= ((a * d) + ((- c) * b)) / (b * d) by A1, A2, Th116
.= ((a * d) - (c * b)) / (b * d) ; :: thesis: verum