Theorem div11

Description: One-to-one relationship for division. (Contributed by NM, 20-Apr-2006) (Proof shortened by Mario Carneiro, 27-May-2016) (Proof shortened by SN, 9-Jul-2025)

	Ref	Expression
Assertion	div11	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) = ( 𝐵 / 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		divcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐵 / 𝐶 ) ∈ ℂ )
2	1	3expb	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐵 / 𝐶 ) ∈ ℂ )
3	2	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐵 / 𝐶 ) ∈ ℂ )
4		divmul3	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 / 𝐶 ) ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) = ( 𝐵 / 𝐶 ) ↔ 𝐴 = ( ( 𝐵 / 𝐶 ) · 𝐶 ) ) )
5	3 4	syld3an2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) = ( 𝐵 / 𝐶 ) ↔ 𝐴 = ( ( 𝐵 / 𝐶 ) · 𝐶 ) ) )
6		divcan1	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( ( 𝐵 / 𝐶 ) · 𝐶 ) = 𝐵 )
7	6	3expb	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐵 / 𝐶 ) · 𝐶 ) = 𝐵 )
8	7	3adant1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐵 / 𝐶 ) · 𝐶 ) = 𝐵 )
9	8	eqeq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 = ( ( 𝐵 / 𝐶 ) · 𝐶 ) ↔ 𝐴 = 𝐵 ) )
10	5 9	bitrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) = ( 𝐵 / 𝐶 ) ↔ 𝐴 = 𝐵 ) )