Theorem rereccl

Description: Closure law for reciprocal. (Contributed by NM, 30-Apr-2005) (Revised by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	rereccl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		ax-rrecex	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 )
2		eqcom	⊢ ( 𝑥 = ( 1 / 𝐴 ) ↔ ( 1 / 𝐴 ) = 𝑥 )
3		1cnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 1 ∈ ℂ )
4		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
5	4	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
6		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
7	6	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℂ )
8		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ≠ 0 )
9		divmul	⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 1 / 𝐴 ) = 𝑥 ↔ ( 𝐴 · 𝑥 ) = 1 ) )
10	3 5 7 8 9	syl112anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → ( ( 1 / 𝐴 ) = 𝑥 ↔ ( 𝐴 · 𝑥 ) = 1 ) )
11	2 10	bitrid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 = ( 1 / 𝐴 ) ↔ ( 𝐴 · 𝑥 ) = 1 ) )
12	11	rexbidva	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ∃ 𝑥 ∈ ℝ 𝑥 = ( 1 / 𝐴 ) ↔ ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 ) )
13	1 12	mpbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ 𝑥 = ( 1 / 𝐴 ) )
14		risset	⊢ ( ( 1 / 𝐴 ) ∈ ℝ ↔ ∃ 𝑥 ∈ ℝ 𝑥 = ( 1 / 𝐴 ) )
15	13 14	sylibr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℝ )