Metamath Proof Explorer

Theorem subrec

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

Ref Expression
Assertion subrec ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐴 ) − ( 1 / 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐴 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 1cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 1 ∈ ℂ )
2 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℂ )
3 simprl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℂ )
4 simplr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 𝐴 ≠ 0 )
5 simprr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
6 1 2 1 3 4 5 divsubdivd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐴 ) − ( 1 / 𝐵 ) ) = ( ( ( 1 · 𝐵 ) − ( 1 · 𝐴 ) ) / ( 𝐴 · 𝐵 ) ) )
7 3 mulid2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 1 · 𝐵 ) = 𝐵 )
8 2 mulid2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 1 · 𝐴 ) = 𝐴 )
9 7 8 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 · 𝐵 ) − ( 1 · 𝐴 ) ) = ( 𝐵 − 𝐴 ) )
10 9 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 1 · 𝐵 ) − ( 1 · 𝐴 ) ) / ( 𝐴 · 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐴 · 𝐵 ) ) )
11 6 10 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( 1 / 𝐴 ) − ( 1 / 𝐵 ) ) = ( ( 𝐵 − 𝐴 ) / ( 𝐴 · 𝐵 ) ) )