rereccl

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

		Ref	Expression
	Assertion	rereccl	$⊢ (A \in ℝ \land A \neq 0) \to \frac{1}{A} \in ℝ$

Step	Hyp	Ref	Expression
1		ax-rrecex	$⊢ (A \in ℝ \land A \neq 0) \to \exists x \in ℝ A x = 1$
2		eqcom	$⊢ x = \frac{1}{A} \leftrightarrow \frac{1}{A} = x$
3		1cnd	$⊢ ((A \in ℝ \land A \neq 0) \land x \in ℝ) \to 1 \in ℂ$
4		simpr	$⊢ ((A \in ℝ \land A \neq 0) \land x \in ℝ) \to x \in ℝ$
5	4	recnd	$⊢ ((A \in ℝ \land A \neq 0) \land x \in ℝ) \to x \in ℂ$
6		simpll	$⊢ ((A \in ℝ \land A \neq 0) \land x \in ℝ) \to A \in ℝ$
7	6	recnd	$⊢ ((A \in ℝ \land A \neq 0) \land x \in ℝ) \to A \in ℂ$
8		simplr	$⊢ ((A \in ℝ \land A \neq 0) \land x \in ℝ) \to A \neq 0$
9		divmul	$⊢ (1 \in ℂ \land x \in ℂ \land (A \in ℂ \land A \neq 0)) \to (\frac{1}{A} = x \leftrightarrow A x = 1)$
10	3 5 7 8 9	syl112anc	$⊢ ((A \in ℝ \land A \neq 0) \land x \in ℝ) \to (\frac{1}{A} = x \leftrightarrow A x = 1)$
11	2 10	syl5bb	$⊢ ((A \in ℝ \land A \neq 0) \land x \in ℝ) \to (x = \frac{1}{A} \leftrightarrow A x = 1)$
12	11	rexbidva	$⊢ (A \in ℝ \land A \neq 0) \to (\exists x \in ℝ x = \frac{1}{A} \leftrightarrow \exists x \in ℝ A x = 1)$
13	1 12	mpbird	$⊢ (A \in ℝ \land A \neq 0) \to \exists x \in ℝ x = \frac{1}{A}$
14		risset	$⊢ \frac{1}{A} \in ℝ \leftrightarrow \exists x \in ℝ x = \frac{1}{A}$
15	13 14	sylibr	$⊢ (A \in ℝ \land A \neq 0) \to \frac{1}{A} \in ℝ$

Metamath Proof Explorer