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

Metamath Proof Explorer

Theorem rdiv

Description: Right-division. (Contributed by BJ, 6-Jun-2019)

Ref Expression
Hypotheses ldiv.a ⊢ φ → A ∈ ℂ
ldiv.b ⊢ φ → B ∈ ℂ
ldiv.c ⊢ φ → C ∈ ℂ
rdiv.an0 ⊢ φ → A ≠ 0
Assertion rdiv ⊢ φ → A ⁢ B = C ↔ B = C A

Proof

Step Hyp Ref Expression
1 ldiv.a ⊢ φ → A ∈ ℂ
2 ldiv.b ⊢ φ → B ∈ ℂ
3 ldiv.c ⊢ φ → C ∈ ℂ
4 rdiv.an0 ⊢ φ → A ≠ 0
5 1 2 mulcomd ⊢ φ → A ⁢ B = B ⁢ A
6 5 eqeq1d ⊢ φ → A ⁢ B = C ↔ B ⁢ A = C
7 2 1 3 4 ldiv ⊢ φ → B ⁢ A = C ↔ B = C A
8 6 7 bitrd ⊢ φ → A ⁢ B = C ↔ B = C A