Theorem divid

Description: A number divided by itself is one. (Contributed by NM, 1-Aug-2004) (Proof shortened by SN, 9-Jul-2025)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A=A$$
2		diveq1	$$⊢\left(A\in ℂ\wedge A\in ℂ\wedge A\ne 0\right)\to \left(\frac{A}{A}=1\leftrightarrow A=A\right)$$
3	1 2	mpbiri	$$⊢\left(A\in ℂ\wedge A\in ℂ\wedge A\ne 0\right)\to \frac{A}{A}=1$$
4	3	3anidm12	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{A}{A}=1$$