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 ⊢ φ → A ∈ ℂ
subrecd.2 ⊢ φ → B ∈ ℂ
subrecd.3 ⊢ φ → A ≠ 0
subrecd.4 ⊢ φ → B ≠ 0
Assertion subrecd ⊢ φ → 1 A − 1 B = B − A A ⁢ B

Proof

Step Hyp Ref Expression
1 subrecd.1 ⊢ φ → A ∈ ℂ
2 subrecd.2 ⊢ φ → B ∈ ℂ
3 subrecd.3 ⊢ φ → A ≠ 0
4 subrecd.4 ⊢ φ → B ≠ 0
5 1cnd ⊢ φ → 1 ∈ ℂ
6 5 1 5 2 3 4 divsubdivd ⊢ φ → 1 A − 1 B = 1 ⁢ B − 1 ⁢ A A ⁢ B
7 2 mullidd ⊢ φ → 1 ⁢ B = B
8 1 mullidd ⊢ φ → 1 ⁢ A = A
9 7 8 oveq12d ⊢ φ → 1 ⁢ B − 1 ⁢ A = B − A
10 9 oveq1d ⊢ φ → 1 ⁢ B − 1 ⁢ A A ⁢ B = B − A A ⁢ B
11 6 10 eqtrd ⊢ φ → 1 A − 1 B = B − A A ⁢ B