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 ( ( 𝐴 ∈ R ∧ 𝐴 ≠ 0R ) → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R )

Proof

Step Hyp Ref Expression
1 sqgt0sr ⊢ ( ( 𝐴 ∈ R ∧ 𝐴 ≠ 0R ) → 0R <R ( 𝐴 ·R 𝐴 ) )
2 mulclsr ⊢ ( ( 𝐴 ∈ R ∧ 𝑦 ∈ R ) → ( 𝐴 ·R 𝑦 ) ∈ R )
3 mulasssr ⊢ ( ( 𝐴 ·R 𝐴 ) ·R 𝑦 ) = ( 𝐴 ·R ( 𝐴 ·R 𝑦 ) )
4 3 eqeq1i ⊢ ( ( ( 𝐴 ·R 𝐴 ) ·R 𝑦 ) = 1R ↔ ( 𝐴 ·R ( 𝐴 ·R 𝑦 ) ) = 1R )
5 oveq2 ⊢ ( 𝑥 = ( 𝐴 ·R 𝑦 ) → ( 𝐴 ·R 𝑥 ) = ( 𝐴 ·R ( 𝐴 ·R 𝑦 ) ) )
6 5 eqeq1d ⊢ ( 𝑥 = ( 𝐴 ·R 𝑦 ) → ( ( 𝐴 ·R 𝑥 ) = 1R ↔ ( 𝐴 ·R ( 𝐴 ·R 𝑦 ) ) = 1R ) )
7 6 rspcev ⊢ ( ( ( 𝐴 ·R 𝑦 ) ∈ R ∧ ( 𝐴 ·R ( 𝐴 ·R 𝑦 ) ) = 1R ) → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R )
8 4 7 sylan2b ⊢ ( ( ( 𝐴 ·R 𝑦 ) ∈ R ∧ ( ( 𝐴 ·R 𝐴 ) ·R 𝑦 ) = 1R ) → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R )
9 2 8 sylan ⊢ ( ( ( 𝐴 ∈ R ∧ 𝑦 ∈ R ) ∧ ( ( 𝐴 ·R 𝐴 ) ·R 𝑦 ) = 1R ) → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R )
10 9 rexlimdva2 ⊢ ( 𝐴 ∈ R → ( ∃ 𝑦 ∈ R ( ( 𝐴 ·R 𝐴 ) ·R 𝑦 ) = 1R → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R ) )
11 recexsrlem ⊢ ( 0R <R ( 𝐴 ·R 𝐴 ) → ∃ 𝑦 ∈ R ( ( 𝐴 ·R 𝐴 ) ·R 𝑦 ) = 1R )
12 10 11 impel ⊢ ( ( 𝐴 ∈ R ∧ 0R <R ( 𝐴 ·R 𝐴 ) ) → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R )
13 1 12 syldan ⊢ ( ( 𝐴 ∈ R ∧ 𝐴 ≠ 0R ) → ∃ 𝑥 ∈ R ( 𝐴 ·R 𝑥 ) = 1R )