Theorem diveq1bd

Description: If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 . Converse of diveq1d . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	diveq1bd.1	$$⊢\phi \to B\in ℂ$$
	diveq1bd.2	$$⊢\phi \to B\ne 0$$
	diveq1bd.3	$$⊢\phi \to A=B$$
Assertion	diveq1bd	$$⊢\phi \to \frac{A}{B}=1$$

Proof

Step	Hyp	Ref	Expression
1		diveq1bd.1	$$⊢\phi \to B\in ℂ$$
2		diveq1bd.2	$$⊢\phi \to B\ne 0$$
3		diveq1bd.3	$$⊢\phi \to A=B$$
4	3 1	eqeltrd	$$⊢\phi \to A\in ℂ$$
5	4 1 2	diveq1ad	$$⊢\phi \to \left(\frac{A}{B}=1\leftrightarrow A=B\right)$$
6	3 5	mpbird	$$⊢\phi \to \frac{A}{B}=1$$