Theorem divrec2

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

	Ref	Expression
Assertion	divrec2	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \frac{A}{B}=\left(\frac{1}{B}\right)A$$

Proof

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