Theorem divval

Description: Value of division: if A and B are complex numbers with B nonzero, then ( A / B ) is the (unique) complex number such that ( B x. x ) = A . (Contributed by NM, 8-May-1999) (Revised by Mario Carneiro, 17-Feb-2014)

	Ref	Expression
Assertion	divval	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \frac{A}{B}=\left(\iota x\in ℂ|Bx=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$$⊢B\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(B\in ℂ\wedge B\ne 0\right)$$
2		eqeq2	$$⊢z=A\to \left(yx=z\leftrightarrow yx=A\right)$$
3	2	riotabidv	$$⊢z=A\to \left(\iota x\in ℂ|yx=z\right)=\left(\iota x\in ℂ|yx=A\right)$$
4		oveq1	$$⊢y=B\to yx=Bx$$
5	4	eqeq1d	$$⊢y=B\to \left(yx=A\leftrightarrow Bx=A\right)$$
6	5	riotabidv	$$⊢y=B\to \left(\iota x\in ℂ|yx=A\right)=\left(\iota x\in ℂ|Bx=A\right)$$
7		df-div	$$⊢÷=\left(z\in ℂ,y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\left(\iota x\in ℂ|yx=z\right)\right)$$
8		riotaex	$$⊢\left(\iota x\in ℂ|Bx=A\right)\in \mathrm{V}$$
9	3 6 7 8	ovmpo	$$⊢\left(A\in ℂ\wedge B\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to \frac{A}{B}=\left(\iota x\in ℂ|Bx=A\right)$$
10	1 9	sylan2br	$$⊢\left(A\in ℂ\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\to \frac{A}{B}=\left(\iota x\in ℂ|Bx=A\right)$$
11	10	3impb	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \frac{A}{B}=\left(\iota x\in ℂ|Bx=A\right)$$