Theorem divadddivi

Description: Addition of two ratios. Theorem I.13 of Apostol p. 18. (Contributed by NM, 21-Feb-1995)

	Ref	Expression
Hypotheses	divclz.1	|- A e. CC
	divclz.2	|- B e. CC
	divmulz.3	|- C e. CC
	divmuldiv.4	|- D e. CC
	divmuldiv.5	|- B =/= 0
	divmuldiv.6	|- D =/= 0
Assertion	divadddivi	|- ( ( A / B ) + ( C / D ) ) = ( ( ( A x. D ) + ( C x. B ) ) / ( B x. D ) )

Proof

Step	Hyp	Ref	Expression
1		divclz.1	|- A e. CC
2		divclz.2	|- B e. CC
3		divmulz.3	|- C e. CC
4		divmuldiv.4	|- D e. CC
5		divmuldiv.5	|- B =/= 0
6		divmuldiv.6	|- D =/= 0
7	2 5	pm3.2i	|- ( B e. CC /\ B =/= 0 )
8	4 6	pm3.2i	|- ( D e. CC /\ D =/= 0 )
9		divadddiv	|- ( ( ( A e. CC /\ C e. CC ) /\ ( ( B e. CC /\ B =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / B ) + ( C / D ) ) = ( ( ( A x. D ) + ( C x. B ) ) / ( B x. D ) ) )
10	1 3 7 8 9	mp4an	|- ( ( A / B ) + ( C / D ) ) = ( ( ( A x. D ) + ( C x. B ) ) / ( B x. D ) )