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 ⊢ φ → A ∈ ℝ
receqid.2 ⊢ φ → A ≠ 0
Assertion receqid ⊢ φ → 1 A = A ↔ A = 1

Proof

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