Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  recexsr Structured version   Visualization version   GIF version

Theorem recexsr 10523
 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.)
Assertion
Ref Expression
recexsr ((𝐴R𝐴 ≠ 0R) → ∃𝑥R (𝐴 ·R 𝑥) = 1R)
Distinct variable group:   𝑥,𝐴

Proof of Theorem recexsr
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 sqgt0sr 10522 . 2 ((𝐴R𝐴 ≠ 0R) → 0R <R (𝐴 ·R 𝐴))
2 mulclsr 10500 . . . . 5 ((𝐴R𝑦R) → (𝐴 ·R 𝑦) ∈ R)
3 mulasssr 10506 . . . . . . 7 ((𝐴 ·R 𝐴) ·R 𝑦) = (𝐴 ·R (𝐴 ·R 𝑦))
43eqeq1i 2826 . . . . . 6 (((𝐴 ·R 𝐴) ·R 𝑦) = 1R ↔ (𝐴 ·R (𝐴 ·R 𝑦)) = 1R)
5 oveq2 7158 . . . . . . . 8 (𝑥 = (𝐴 ·R 𝑦) → (𝐴 ·R 𝑥) = (𝐴 ·R (𝐴 ·R 𝑦)))
65eqeq1d 2823 . . . . . . 7 (𝑥 = (𝐴 ·R 𝑦) → ((𝐴 ·R 𝑥) = 1R ↔ (𝐴 ·R (𝐴 ·R 𝑦)) = 1R))
76rspcev 3623 . . . . . 6 (((𝐴 ·R 𝑦) ∈ R ∧ (𝐴 ·R (𝐴 ·R 𝑦)) = 1R) → ∃𝑥R (𝐴 ·R 𝑥) = 1R)
84, 7sylan2b 595 . . . . 5 (((𝐴 ·R 𝑦) ∈ R ∧ ((𝐴 ·R 𝐴) ·R 𝑦) = 1R) → ∃𝑥R (𝐴 ·R 𝑥) = 1R)
92, 8sylan 582 . . . 4 (((𝐴R𝑦R) ∧ ((𝐴 ·R 𝐴) ·R 𝑦) = 1R) → ∃𝑥R (𝐴 ·R 𝑥) = 1R)
109rexlimdva2 3287 . . 3 (𝐴R → (∃𝑦R ((𝐴 ·R 𝐴) ·R 𝑦) = 1R → ∃𝑥R (𝐴 ·R 𝑥) = 1R))
11 recexsrlem 10519 . . 3 (0R <R (𝐴 ·R 𝐴) → ∃𝑦R ((𝐴 ·R 𝐴) ·R 𝑦) = 1R)
1210, 11impel 508 . 2 ((𝐴R ∧ 0R <R (𝐴 ·R 𝐴)) → ∃𝑥R (𝐴 ·R 𝑥) = 1R)
131, 12syldan 593 1 ((𝐴R𝐴 ≠ 0R) → ∃𝑥R (𝐴 ·R 𝑥) = 1R)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∃wrex 3139   class class class wbr 5059  (class class class)co 7150  Rcnr 10281  0Rc0r 10282  1Rc1r 10283   ·R cmr 10286
 Copyright terms: Public domain W3C validator