This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to B \in ℂ$
	diveq1bd.2	$⊢ φ \to B \neq 0$
	diveq1bd.3	$⊢ φ \to A = B$
Assertion	diveq1bd	$⊢ φ \to \frac{A}{B} = 1$

Proof

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