Theorem subreci

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

	Ref	Expression
Hypotheses	subreci.1	⊢ 𝐴 ∈ ℂ
	subreci.2	⊢ 𝐵 ∈ ℂ
	subreci.3	⊢ 𝐴 ≠ 0
	subreci.4	⊢ 𝐵 ≠ 0
Assertion	subreci	⊢ ( ( 1 / 𝐴 ) − ( 1 / 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐴 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		subreci.1	⊢ 𝐴 ∈ ℂ
2		subreci.2	⊢ 𝐵 ∈ ℂ
3		subreci.3	⊢ 𝐴 ≠ 0
4		subreci.4	⊢ 𝐵 ≠ 0
5		subrec	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐴 ) − ( 1 / 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐴 · 𝐵 ) ) )
6	1 3 2 4 5	mp4an	⊢ ( ( 1 / 𝐴 ) − ( 1 / 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐴 · 𝐵 ) )