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 )