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

Metamath Proof Explorer

Theorem recexsr

Description: The reciprocal of a nonzero signed real exists. Part of Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 15-May-1996) (New usage is discouraged.)

Ref Expression
Assertion recexsr ⊢ A ∈ 𝑹 ∧ A ≠ 0 𝑹 → ∃ x ∈ 𝑹 A ⋅ 𝑹 x = 1 𝑹

Proof

Step Hyp Ref Expression
1 sqgt0sr ⊢ A ∈ 𝑹 ∧ A ≠ 0 𝑹 → 0 𝑹 < 𝑹 A ⋅ 𝑹 A
2 mulclsr ⊢ A ∈ 𝑹 ∧ y ∈ 𝑹 → A ⋅ 𝑹 y ∈ 𝑹
3 mulasssr ⊢ A ⋅ 𝑹 A ⋅ 𝑹 y = A ⋅ 𝑹 A ⋅ 𝑹 y
4 3 eqeq1i ⊢ A ⋅ 𝑹 A ⋅ 𝑹 y = 1 𝑹 ↔ A ⋅ 𝑹 A ⋅ 𝑹 y = 1 𝑹
5 oveq2 ⊢ x = A ⋅ 𝑹 y → A ⋅ 𝑹 x = A ⋅ 𝑹 A ⋅ 𝑹 y
6 5 eqeq1d ⊢ x = A ⋅ 𝑹 y → A ⋅ 𝑹 x = 1 𝑹 ↔ A ⋅ 𝑹 A ⋅ 𝑹 y = 1 𝑹
7 6 rspcev ⊢ A ⋅ 𝑹 y ∈ 𝑹 ∧ A ⋅ 𝑹 A ⋅ 𝑹 y = 1 𝑹 → ∃ x ∈ 𝑹 A ⋅ 𝑹 x = 1 𝑹
8 4 7 sylan2b ⊢ A ⋅ 𝑹 y ∈ 𝑹 ∧ A ⋅ 𝑹 A ⋅ 𝑹 y = 1 𝑹 → ∃ x ∈ 𝑹 A ⋅ 𝑹 x = 1 𝑹
9 2 8 sylan ⊢ A ∈ 𝑹 ∧ y ∈ 𝑹 ∧ A ⋅ 𝑹 A ⋅ 𝑹 y = 1 𝑹 → ∃ x ∈ 𝑹 A ⋅ 𝑹 x = 1 𝑹
10 9 rexlimdva2 ⊢ A ∈ 𝑹 → ∃ y ∈ 𝑹 A ⋅ 𝑹 A ⋅ 𝑹 y = 1 𝑹 → ∃ x ∈ 𝑹 A ⋅ 𝑹 x = 1 𝑹
11 recexsrlem ⊢ 0 𝑹 < 𝑹 A ⋅ 𝑹 A → ∃ y ∈ 𝑹 A ⋅ 𝑹 A ⋅ 𝑹 y = 1 𝑹
12 10 11 impel ⊢ A ∈ 𝑹 ∧ 0 𝑹 < 𝑹 A ⋅ 𝑹 A → ∃ x ∈ 𝑹 A ⋅ 𝑹 x = 1 𝑹
13 1 12 syldan ⊢ A ∈ 𝑹 ∧ A ≠ 0 𝑹 → ∃ x ∈ 𝑹 A ⋅ 𝑹 x = 1 𝑹