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	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	diveq1bd.2	⊢ ( 𝜑 → 𝐵 ≠ 0 )
	diveq1bd.3	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	diveq1bd	⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		diveq1bd.1	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
2		diveq1bd.2	⊢ ( 𝜑 → 𝐵 ≠ 0 )
3		diveq1bd.3	⊢ ( 𝜑 → 𝐴 = 𝐵 )
4	3 1	eqeltrd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
5	4 1 2	diveq1ad	⊢ ( 𝜑 → ( ( 𝐴 / 𝐵 ) = 1 ↔ 𝐴 = 𝐵 ) )
6	3 5	mpbird	⊢ ( 𝜑 → ( 𝐴 / 𝐵 ) = 1 )