Theorem sn-redividd

Description: A number divided by itself is 1. (Contributed by SN, 2-Apr-2026)

	Ref	Expression
Hypotheses	sn-rediv0d.a	|- ( ph -> A e. RR )
	sn-rediv0d.z	|- ( ph -> A =/= 0 )
Assertion	sn-redividd	|- ( ph -> ( A /R A ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		sn-rediv0d.a	|- ( ph -> A e. RR )
2		sn-rediv0d.z	|- ( ph -> A =/= 0 )
3		eqidd	|- ( ph -> A = A )
4	1 1 2	rediveq1d	|- ( ph -> ( ( A /R A ) = 1 <-> A = A ) )
5	3 4	mpbird	|- ( ph -> ( A /R A ) = 1 )