Theorem dividi

Description: A number divided by itself is one. (Contributed by NM, 9-Feb-1995)

	Ref	Expression
Hypotheses	divclz.1	⊢ 𝐴 ∈ ℂ
	reccl.2	⊢ 𝐴 ≠ 0
Assertion	dividi	⊢ ( 𝐴 / 𝐴 ) = 1

Proof

Step	Hyp	Ref	Expression
1		divclz.1	⊢ 𝐴 ∈ ℂ
2		reccl.2	⊢ 𝐴 ≠ 0
3		divid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 / 𝐴 ) = 1 )
4	1 2 3	mp2an	⊢ ( 𝐴 / 𝐴 ) = 1