subrec

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

		Ref	Expression
	Assertion	subrec	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to (\frac{1}{A}) - (\frac{1}{B}) = \frac{B - A}{A B}$

Step	Hyp	Ref	Expression
1		1cnd	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to 1 \in ℂ$
2		simpll	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to A \in ℂ$
3		simprl	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to B \in ℂ$
4		simplr	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to A \neq 0$
5		simprr	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to B \neq 0$
6	1 2 1 3 4 5	divsubdivd	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to (\frac{1}{A}) - (\frac{1}{B}) = \frac{1 B - 1 A}{A B}$
7	3	mulid2d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to 1 B = B$
8	2	mulid2d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to 1 A = A$
9	7 8	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to 1 B - 1 A = B - A$
10	9	oveq1d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to \frac{1 B - 1 A}{A B} = \frac{B - A}{A B}$
11	6 10	eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to (\frac{1}{A}) - (\frac{1}{B}) = \frac{B - A}{A B}$

Metamath Proof Explorer