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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
ldiv.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
ldiv.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
ldiv.bn0 ⊢ ( 𝜑 → 𝐵 ≠ 0 )
Assertion ldiv ( 𝜑 → ( ( 𝐴 · 𝐵 ) = 𝐶 ↔ 𝐴 = ( 𝐶 / 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ldiv.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 ldiv.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 ldiv.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4 ldiv.bn0 ⊢ ( 𝜑 → 𝐵 ≠ 0 )
5 oveq1 ⊢ ( ( 𝐴 · 𝐵 ) = 𝐶 → ( ( 𝐴 · 𝐵 ) / 𝐵 ) = ( 𝐶 / 𝐵 ) )
6 1 2 4 divcan4d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) / 𝐵 ) = 𝐴 )
7 6 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) / 𝐵 ) = ( 𝐶 / 𝐵 ) ↔ 𝐴 = ( 𝐶 / 𝐵 ) ) )
8 5 7 imbitrid ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) = 𝐶 → 𝐴 = ( 𝐶 / 𝐵 ) ) )
9 oveq1 ⊢ ( 𝐴 = ( 𝐶 / 𝐵 ) → ( 𝐴 · 𝐵 ) = ( ( 𝐶 / 𝐵 ) · 𝐵 ) )
10 3 2 4 divcan1d ⊢ ( 𝜑 → ( ( 𝐶 / 𝐵 ) · 𝐵 ) = 𝐶 )
11 10 eqeq2d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) = ( ( 𝐶 / 𝐵 ) · 𝐵 ) ↔ ( 𝐴 · 𝐵 ) = 𝐶 ) )
12 9 11 imbitrid ⊢ ( 𝜑 → ( 𝐴 = ( 𝐶 / 𝐵 ) → ( 𝐴 · 𝐵 ) = 𝐶 ) )
13 8 12 impbid ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) = 𝐶 ↔ 𝐴 = ( 𝐶 / 𝐵 ) ) )