This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subrecd

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

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

Proof

Step Hyp Ref Expression
1 subrecd.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 subrecd.2 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 subrecd.3 ⊢ ( 𝜑 → 𝐴 ≠ 0 )
4 subrecd.4 ⊢ ( 𝜑 → 𝐵 ≠ 0 )
5 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
6 5 1 5 2 3 4 divsubdivd ⊢ ( 𝜑 → ( ( 1 / 𝐴 ) − ( 1 / 𝐵 ) ) = ( ( ( 1 · 𝐵 ) − ( 1 · 𝐴 ) ) / ( 𝐴 · 𝐵 ) ) )
7 2 mullidd ⊢ ( 𝜑 → ( 1 · 𝐵 ) = 𝐵 )
8 1 mullidd ⊢ ( 𝜑 → ( 1 · 𝐴 ) = 𝐴 )
9 7 8 oveq12d ⊢ ( 𝜑 → ( ( 1 · 𝐵 ) − ( 1 · 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
10 9 oveq1d ⊢ ( 𝜑 → ( ( ( 1 · 𝐵 ) − ( 1 · 𝐴 ) ) / ( 𝐴 · 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐴 · 𝐵 ) ) )
11 6 10 eqtrd ⊢ ( 𝜑 → ( ( 1 / 𝐴 ) − ( 1 / 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐴 · 𝐵 ) ) )