This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )