Theorem sqdivid

Description: The square of a nonzero number divided by itself yields the number itself. (Contributed by AV, 19-Jul-2021)

	Ref	Expression
Assertion	sqdivid	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{A^2}{A}=A$$

Proof

Step	Hyp	Ref	Expression
1		sqval	$$⊢A\in ℂ\to A^2=AA$$
2	1	adantr	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to A^2=AA$$
3	2	oveq1d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{A^2}{A}=\frac{AA}{A}$$
4		divcan3	$$⊢\left(A\in ℂ\wedge A\in ℂ\wedge A\ne 0\right)\to \frac{AA}{A}=A$$
5	4	3anidm12	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{AA}{A}=A$$
6	3 5	eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{A^2}{A}=A$$