Metamath Proof Explorer

Theorem diveq1

Description: Equality in terms of unit ratio. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion diveq1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 1 ↔ A = B

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 divmul2 ⊢ A ∈ ℂ ∧ 1 ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 1 ↔ A = B ⋅ 1
3 1 2 mp3an2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 1 ↔ A = B ⋅ 1
4 3 3impb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 1 ↔ A = B ⋅ 1
5 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ
6 5 mulridd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⋅ 1 = B
7 6 eqeq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A = B ⋅ 1 ↔ A = B
8 4 7 bitrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 1 ↔ A = B