This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Real and complex numbers - basic operations Division diveq1ad
Description: The quotient of two complex numbers is one iff they are equal.
Deduction form of diveq1 . Generalization of diveq1d .
(Contributed by David Moews , 28-Feb-2017)
Ref
Expression
Hypotheses
div1d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
divcld.2 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
divcld.3 ⊢ ( 𝜑 → 𝐵 ≠ 0 )
Assertion
diveq1ad ⊢ ( 𝜑 → ( ( 𝐴 / 𝐵 ) = 1 ↔ 𝐴 = 𝐵 ) )
Proof
Step
Hyp
Ref
Expression
1
div1d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2
divcld.2 ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3
divcld.3 ⊢ ( 𝜑 → 𝐵 ≠ 0 )
4
diveq1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) = 1 ↔ 𝐴 = 𝐵 ) )
5
1 2 3 4
syl3anc ⊢ ( 𝜑 → ( ( 𝐴 / 𝐵 ) = 1 ↔ 𝐴 = 𝐵 ) )