Metamath Proof Explorer


Theorem subreci

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

Ref Expression
Hypotheses subreci.1 ⊢ A ∈ ℂ
subreci.2 ⊢ B ∈ ℂ
subreci.3 ⊢ A ≠ 0
subreci.4 ⊢ B ≠ 0
Assertion subreci ⊢ 1 A − 1 B = B − A A ⁢ B

Proof

Step Hyp Ref Expression
1 subreci.1 ⊢ A ∈ ℂ
2 subreci.2 ⊢ B ∈ ℂ
3 subreci.3 ⊢ A ≠ 0
4 subreci.4 ⊢ B ≠ 0
5 subrec ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → 1 A − 1 B = B − A A ⁢ B
6 1 3 2 4 5 mp4an ⊢ 1 A − 1 B = B − A A ⁢ B