divcan6

Description: Cancellation of inverted fractions. (Contributed by NM, 28-Dec-2007)

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

Step	Hyp	Ref	Expression
1		recdiv	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to \frac{1}{\frac{A}{B}} = \frac{B}{A}$
2	1	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to (\frac{A}{B}) (\frac{1}{\frac{A}{B}}) = (\frac{A}{B}) (\frac{B}{A})$
3		divcl	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} \in ℂ$
4	3	3expb	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{A}{B} \in ℂ$
5	4	adantlr	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to \frac{A}{B} \in ℂ$
6		divne0	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to \frac{A}{B} \neq 0$
7		recid	$⊢ (\frac{A}{B} \in ℂ \land \frac{A}{B} \neq 0) \to (\frac{A}{B}) (\frac{1}{\frac{A}{B}}) = 1$
8	5 6 7	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to (\frac{A}{B}) (\frac{1}{\frac{A}{B}}) = 1$
9	2 8	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to (\frac{A}{B}) (\frac{B}{A}) = 1$

Metamath Proof Explorer