Theorem receqid

Description: Real numbers equal to their own reciprocal have absolute value 1 . (Contributed by Thierry Arnoux, 9-Nov-2025)

	Ref	Expression
Hypotheses	receqid.1	$$⊢\phi \to A\in ℝ$$
	receqid.2	$$⊢\phi \to A\ne 0$$
Assertion	receqid	$$⊢\phi \to \left(\frac{1}{A}=A\leftrightarrow \left|A\right|=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		receqid.1	$$⊢\phi \to A\in ℝ$$
2		receqid.2	$$⊢\phi \to A\ne 0$$
3	1	absred	$$⊢\phi \to \left|A\right|=\sqrt{A^2}$$
4		sqrt1	$$⊢\sqrt{1}=1$$
5	4	a1i	$$⊢\phi \to \sqrt{1}=1$$
6	5	eqcomd	$$⊢\phi \to 1=\sqrt{1}$$
7	3 6	eqeq12d	$$⊢\phi \to \left(\left|A\right|=1\leftrightarrow \sqrt{A^2}=\sqrt{1}\right)$$
8	1	resqcld	$$⊢\phi \to A^2\in ℝ$$
9	1	sqge0d	$$⊢\phi \to 0\le A^2$$
10		1red	$$⊢\phi \to 1\in ℝ$$
11		0le1	$$⊢0\le 1$$
12	11	a1i	$$⊢\phi \to 0\le 1$$
13		sqrt11	$$⊢\left(\left(A^2\in ℝ\wedge 0\le A^2\right)\wedge \left(1\in ℝ\wedge 0\le 1\right)\right)\to \left(\sqrt{A^2}=\sqrt{1}\leftrightarrow A^2=1\right)$$
14	8 9 10 12 13	syl22anc	$$⊢\phi \to \left(\sqrt{A^2}=\sqrt{1}\leftrightarrow A^2=1\right)$$
15	8	recnd	$$⊢\phi \to A^2\in ℂ$$
16		1cnd	$$⊢\phi \to 1\in ℂ$$
17	1	recnd	$$⊢\phi \to A\in ℂ$$
18		div11	$$⊢\left(A^2\in ℂ\wedge 1\in ℂ\wedge \left(A\in ℂ\wedge A\ne 0\right)\right)\to \left(\frac{A^2}{A}=\frac{1}{A}\leftrightarrow A^2=1\right)$$
19	15 16 17 2 18	syl112anc	$$⊢\phi \to \left(\frac{A^2}{A}=\frac{1}{A}\leftrightarrow A^2=1\right)$$
20		sqdivid	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{A^2}{A}=A$$
21	17 2 20	syl2anc	$$⊢\phi \to \frac{A^2}{A}=A$$
22	21	eqeq1d	$$⊢\phi \to \left(\frac{A^2}{A}=\frac{1}{A}\leftrightarrow A=\frac{1}{A}\right)$$
23	14 19 22	3bitr2rd	$$⊢\phi \to \left(A=\frac{1}{A}\leftrightarrow \sqrt{A^2}=\sqrt{1}\right)$$
24		eqcom	$$⊢A=\frac{1}{A}\leftrightarrow \frac{1}{A}=A$$
25	24	a1i	$$⊢\phi \to \left(A=\frac{1}{A}\leftrightarrow \frac{1}{A}=A\right)$$
26	7 23 25	3bitr2rd	$$⊢\phi \to \left(\frac{1}{A}=A\leftrightarrow \left|A\right|=1\right)$$