divrec2

Description: Relationship between division and reciprocal. (Contributed by NM, 7-Feb-2006)

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

Step	Hyp	Ref	Expression
1		divrec	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} = A (\frac{1}{B})$
2		simp1	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to A \in ℂ$
3		reccl	$⊢ (B \in ℂ \land B \neq 0) \to \frac{1}{B} \in ℂ$
4	3	3adant1	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{1}{B} \in ℂ$
5	2 4	mulcomd	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to A (\frac{1}{B}) = (\frac{1}{B}) A$
6	1 5	eqtrd	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} = (\frac{1}{B}) A$

Metamath Proof Explorer