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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	receqid.2	⊢ ( 𝜑 → 𝐴 ≠ 0 )
Assertion	receqid	⊢ ( 𝜑 → ( ( 1 / 𝐴 ) = 𝐴 ↔ ( abs ‘ 𝐴 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		receqid.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		receqid.2	⊢ ( 𝜑 → 𝐴 ≠ 0 )
3	1	absred	⊢ ( 𝜑 → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 ↑ 2 ) ) )
4		sqrt1	⊢ ( √ ‘ 1 ) = 1
5	4	a1i	⊢ ( 𝜑 → ( √ ‘ 1 ) = 1 )
6	5	eqcomd	⊢ ( 𝜑 → 1 = ( √ ‘ 1 ) )
7	3 6	eqeq12d	⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) = 1 ↔ ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( √ ‘ 1 ) ) )
8	1	resqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℝ )
9	1	sqge0d	⊢ ( 𝜑 → 0 ≤ ( 𝐴 ↑ 2 ) )
10		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
11		0le1	⊢ 0 ≤ 1
12	11	a1i	⊢ ( 𝜑 → 0 ≤ 1 )
13		sqrt11	⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 ↑ 2 ) ) ∧ ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ) → ( ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( √ ‘ 1 ) ↔ ( 𝐴 ↑ 2 ) = 1 ) )
14	8 9 10 12 13	syl22anc	⊢ ( 𝜑 → ( ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( √ ‘ 1 ) ↔ ( 𝐴 ↑ 2 ) = 1 ) )
15	8	recnd	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
16		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
17	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
18		div11	⊢ ( ( ( 𝐴 ↑ 2 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( ( 𝐴 ↑ 2 ) / 𝐴 ) = ( 1 / 𝐴 ) ↔ ( 𝐴 ↑ 2 ) = 1 ) )
19	15 16 17 2 18	syl112anc	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) / 𝐴 ) = ( 1 / 𝐴 ) ↔ ( 𝐴 ↑ 2 ) = 1 ) )
20		sqdivid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 ↑ 2 ) / 𝐴 ) = 𝐴 )
21	17 2 20	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) / 𝐴 ) = 𝐴 )
22	21	eqeq1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) / 𝐴 ) = ( 1 / 𝐴 ) ↔ 𝐴 = ( 1 / 𝐴 ) ) )
23	14 19 22	3bitr2rd	⊢ ( 𝜑 → ( 𝐴 = ( 1 / 𝐴 ) ↔ ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( √ ‘ 1 ) ) )
24		eqcom	⊢ ( 𝐴 = ( 1 / 𝐴 ) ↔ ( 1 / 𝐴 ) = 𝐴 )
25	24	a1i	⊢ ( 𝜑 → ( 𝐴 = ( 1 / 𝐴 ) ↔ ( 1 / 𝐴 ) = 𝐴 ) )
26	7 23 25	3bitr2rd	⊢ ( 𝜑 → ( ( 1 / 𝐴 ) = 𝐴 ↔ ( abs ‘ 𝐴 ) = 1 ) )