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

Metamath Proof Explorer

Theorem ldiv

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

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

Proof

Step Hyp Ref Expression
1 ldiv.a ⊢ φ → A ∈ ℂ
2 ldiv.b ⊢ φ → B ∈ ℂ
3 ldiv.c ⊢ φ → C ∈ ℂ
4 ldiv.bn0 ⊢ φ → B ≠ 0
5 oveq1 ⊢ A ⁢ B = C → A ⁢ B B = C B
6 1 2 4 divcan4d ⊢ φ → A ⁢ B B = A
7 6 eqeq1d ⊢ φ → A ⁢ B B = C B ↔ A = C B
8 5 7 imbitrid ⊢ φ → A ⁢ B = C → A = C B
9 oveq1 ⊢ A = C B → A ⁢ B = C B ⁢ B
10 3 2 4 divcan1d ⊢ φ → C B ⁢ B = C
11 10 eqeq2d ⊢ φ → A ⁢ B = C B ⁢ B ↔ A ⁢ B = C
12 9 11 imbitrid ⊢ φ → A = C B → A ⁢ B = C
13 8 12 impbid ⊢ φ → A ⁢ B = C ↔ A = C B