Theorem rerecrecd

Description: A number is equal to the reciprocal of its reciprocal. (Contributed by SN, 2-Apr-2026)

	Ref	Expression
Hypotheses	sn-rereccld.a	$$⊢\phi \to A\in ℝ$$
	sn-rereccld.z	$$⊢\phi \to A\ne 0$$
Assertion	rerecrecd	$$⊢\phi \to 1{/}_{ℝ}\left(1{/}_{ℝ}A\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		sn-rereccld.a	$$⊢\phi \to A\in ℝ$$
2		sn-rereccld.z	$$⊢\phi \to A\ne 0$$
3	1 2	rerecid2d	$$⊢\phi \to \left(1{/}_{ℝ}A\right)A=1$$
4		1red	$$⊢\phi \to 1\in ℝ$$
5	1 2	sn-rereccld	$$⊢\phi \to 1{/}_{ℝ}A\in ℝ$$
6	1 2	rerecne0d	$$⊢\phi \to 1{/}_{ℝ}A\ne 0$$
7	4 1 5 6	redivmuld	$$⊢\phi \to \left(1{/}_{ℝ}\left(1{/}_{ℝ}A\right)=A\leftrightarrow \left(1{/}_{ℝ}A\right)A=1\right)$$
8	3 7	mpbird	$$⊢\phi \to 1{/}_{ℝ}\left(1{/}_{ℝ}A\right)=A$$