Theorem xrecex

Description: Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016)

	Ref	Expression
Assertion	xrecex	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 ·e 𝑥 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		ax-rrecex	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 )
2		rexmul	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐴 ·e 𝑥 ) = ( 𝐴 · 𝑥 ) )
3	2	eqeq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 ·e 𝑥 ) = 1 ↔ ( 𝐴 · 𝑥 ) = 1 ) )
4	3	ex	⊢ ( 𝐴 ∈ ℝ → ( 𝑥 ∈ ℝ → ( ( 𝐴 ·e 𝑥 ) = 1 ↔ ( 𝐴 · 𝑥 ) = 1 ) ) )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℝ → ( ( 𝐴 ·e 𝑥 ) = 1 ↔ ( 𝐴 · 𝑥 ) = 1 ) ) )
6	5	pm5.32d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ( 𝑥 ∈ ℝ ∧ ( 𝐴 ·e 𝑥 ) = 1 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) )
7	6	rexbidv2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ∃ 𝑥 ∈ ℝ ( 𝐴 ·e 𝑥 ) = 1 ↔ ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 ) )
8	1 7	mpbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 ·e 𝑥 ) = 1 )