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		simpll	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to A \in ℂ$
2		simprl	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to B \in ℂ$
3		simplr	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to A \neq 0$
4		simprr	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to B \neq 0$
5	1 2 3 4	subrecd	$⊢ ((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