let a, b, c, d be Complex; ( b <> 0 & d <> 0 implies (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) )
assume A1:
b <> 0
; ( not d <> 0 or (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) )
assume
d <> 0
; (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
hence (a / b) + (c / d) =
((a * d) / (b * d)) + (c / d)
by Lm10
.=
((a * d) / (b * d)) + ((c * b) / (b * d))
by A1, Lm10
.=
((a * d) + (c * b)) / (b * d)
by Th62
;
verum