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

Metamath Proof Explorer

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 / 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐴 · 𝐵 ) )