# Metamath Proof Explorer

## Theorem subrec

Description: Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jul-2015)

Ref Expression
Assertion subrec ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \left(\frac{1}{{A}}\right)-\left(\frac{1}{{B}}\right)=\frac{{B}-{A}}{{A}{B}}$

### Proof

Step Hyp Ref Expression
1 1cnd ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to 1\in ℂ$
2 simpll ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to {A}\in ℂ$
3 simprl ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to {B}\in ℂ$
4 simplr ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to {A}\ne 0$
5 simprr ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to {B}\ne 0$
6 1 2 1 3 4 5 divsubdivd ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \left(\frac{1}{{A}}\right)-\left(\frac{1}{{B}}\right)=\frac{1{B}-1{A}}{{A}{B}}$
7 3 mulid2d ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to 1{B}={B}$
8 2 mulid2d ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to 1{A}={A}$
9 7 8 oveq12d ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to 1{B}-1{A}={B}-{A}$
10 9 oveq1d ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \frac{1{B}-1{A}}{{A}{B}}=\frac{{B}-{A}}{{A}{B}}$
11 6 10 eqtrd ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \left(\frac{1}{{A}}\right)-\left(\frac{1}{{B}}\right)=\frac{{B}-{A}}{{A}{B}}$