Theorem subrecd

Description: Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017)

	Ref	Expression
Hypotheses	subrecd.1	|- ( ph -> A e. CC )
	subrecd.2	|- ( ph -> B e. CC )
	subrecd.3	|- ( ph -> A =/= 0 )
	subrecd.4	|- ( ph -> B =/= 0 )
Assertion	subrecd	|- ( ph -> ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		subrecd.1	|- ( ph -> A e. CC )
2		subrecd.2	|- ( ph -> B e. CC )
3		subrecd.3	|- ( ph -> A =/= 0 )
4		subrecd.4	|- ( ph -> B =/= 0 )
5		1cnd	|- ( ph -> 1 e. CC )
6	5 1 5 2 3 4	divsubdivd	|- ( ph -> ( ( 1 / A ) - ( 1 / B ) ) = ( ( ( 1 x. B ) - ( 1 x. A ) ) / ( A x. B ) ) )
7	2	mullidd	|- ( ph -> ( 1 x. B ) = B )
8	1	mullidd	|- ( ph -> ( 1 x. A ) = A )
9	7 8	oveq12d	|- ( ph -> ( ( 1 x. B ) - ( 1 x. A ) ) = ( B - A ) )
10	9	oveq1d	|- ( ph -> ( ( ( 1 x. B ) - ( 1 x. A ) ) / ( A x. B ) ) = ( ( B - A ) / ( A x. B ) ) )
11	6 10	eqtrd	|- ( ph -> ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) ) )