Theorem divcan8d

Description: A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	divcan8d.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	divcan8d.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	divcan8d.a0	⊢ ( 𝜑 → 𝐴 ≠ 0 )
	divcan8d.b0	⊢ ( 𝜑 → 𝐵 ≠ 0 )
Assertion	divcan8d	⊢ ( 𝜑 → ( 𝐵 / ( 𝐴 · 𝐵 ) ) = ( 1 / 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		divcan8d.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		divcan8d.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		divcan8d.a0	⊢ ( 𝜑 → 𝐴 ≠ 0 )
4		divcan8d.b0	⊢ ( 𝜑 → 𝐵 ≠ 0 )
5	1 2	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℂ )
6	1 2 3 4	mulne0d	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ≠ 0 )
7	1 2 6	mulne0bbd	⊢ ( 𝜑 → 𝐵 ≠ 0 )
8	2 5 2 6 7	divcan7d	⊢ ( 𝜑 → ( ( 𝐵 / 𝐵 ) / ( ( 𝐴 · 𝐵 ) / 𝐵 ) ) = ( 𝐵 / ( 𝐴 · 𝐵 ) ) )
9	8	eqcomd	⊢ ( 𝜑 → ( 𝐵 / ( 𝐴 · 𝐵 ) ) = ( ( 𝐵 / 𝐵 ) / ( ( 𝐴 · 𝐵 ) / 𝐵 ) ) )
10	2 4	dividd	⊢ ( 𝜑 → ( 𝐵 / 𝐵 ) = 1 )
11	1 2 4	divcan4d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) / 𝐵 ) = 𝐴 )
12	10 11	oveq12d	⊢ ( 𝜑 → ( ( 𝐵 / 𝐵 ) / ( ( 𝐴 · 𝐵 ) / 𝐵 ) ) = ( 1 / 𝐴 ) )
13		eqidd	⊢ ( 𝜑 → ( 1 / 𝐴 ) = ( 1 / 𝐴 ) )
14	9 12 13	3eqtrd	⊢ ( 𝜑 → ( 𝐵 / ( 𝐴 · 𝐵 ) ) = ( 1 / 𝐴 ) )