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	|- ( ph -> A e. RR )
	receqid.2	|- ( ph -> A =/= 0 )
Assertion	receqid	|- ( ph -> ( ( 1 / A ) = A <-> ( abs ` A ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		receqid.1	|- ( ph -> A e. RR )
2		receqid.2	|- ( ph -> A =/= 0 )
3	1	absred	|- ( ph -> ( abs ` A ) = ( sqrt ` ( A ^ 2 ) ) )
4		sqrt1	|- ( sqrt ` 1 ) = 1
5	4	a1i	|- ( ph -> ( sqrt ` 1 ) = 1 )
6	5	eqcomd	|- ( ph -> 1 = ( sqrt ` 1 ) )
7	3 6	eqeq12d	|- ( ph -> ( ( abs ` A ) = 1 <-> ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 1 ) ) )
8	1	resqcld	|- ( ph -> ( A ^ 2 ) e. RR )
9	1	sqge0d	|- ( ph -> 0 <_ ( A ^ 2 ) )
10		1red	|- ( ph -> 1 e. RR )
11		0le1	|- 0 <_ 1
12	11	a1i	|- ( ph -> 0 <_ 1 )
13		sqrt11	|- ( ( ( ( A ^ 2 ) e. RR /\ 0 <_ ( A ^ 2 ) ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 1 ) <-> ( A ^ 2 ) = 1 ) )
14	8 9 10 12 13	syl22anc	|- ( ph -> ( ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 1 ) <-> ( A ^ 2 ) = 1 ) )
15	8	recnd	|- ( ph -> ( A ^ 2 ) e. CC )
16		1cnd	|- ( ph -> 1 e. CC )
17	1	recnd	|- ( ph -> A e. CC )
18		div11	|- ( ( ( A ^ 2 ) e. CC /\ 1 e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( ( A ^ 2 ) / A ) = ( 1 / A ) <-> ( A ^ 2 ) = 1 ) )
19	15 16 17 2 18	syl112anc	|- ( ph -> ( ( ( A ^ 2 ) / A ) = ( 1 / A ) <-> ( A ^ 2 ) = 1 ) )
20		sqdivid	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( A ^ 2 ) / A ) = A )
21	17 2 20	syl2anc	|- ( ph -> ( ( A ^ 2 ) / A ) = A )
22	21	eqeq1d	|- ( ph -> ( ( ( A ^ 2 ) / A ) = ( 1 / A ) <-> A = ( 1 / A ) ) )
23	14 19 22	3bitr2rd	|- ( ph -> ( A = ( 1 / A ) <-> ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` 1 ) ) )
24		eqcom	|- ( A = ( 1 / A ) <-> ( 1 / A ) = A )
25	24	a1i	|- ( ph -> ( A = ( 1 / A ) <-> ( 1 / A ) = A ) )
26	7 23 25	3bitr2rd	|- ( ph -> ( ( 1 / A ) = A <-> ( abs ` A ) = 1 ) )