ddcan

Description: Cancellation in a double division. (Contributed by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	ddcan	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to \frac{A}{\frac{A}{B}} = 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		simprr	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to B \neq 0$
4		divcan1	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to (\frac{A}{B}) B = A$
5	1 2 3 4	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to (\frac{A}{B}) B = A$
6		divcl	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} \in ℂ$
7	1 2 3 6	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to \frac{A}{B} \in ℂ$
8		divne0	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to \frac{A}{B} \neq 0$
9		divmul	$⊢ (A \in ℂ \land B \in ℂ \land (\frac{A}{B} \in ℂ \land \frac{A}{B} \neq 0)) \to (\frac{A}{\frac{A}{B}} = B \leftrightarrow (\frac{A}{B}) B = A)$
10	1 2 7 8 9	syl112anc	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to (\frac{A}{\frac{A}{B}} = B \leftrightarrow (\frac{A}{B}) B = A)$
11	5 10	mpbird	$⊢ ((A \in ℂ \land A \neq 0) \land (B \in ℂ \land B \neq 0)) \to \frac{A}{\frac{A}{B}} = B$

Metamath Proof Explorer