axrrecex

Description: Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rrecex . (Contributed by NM, 15-May-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	axrrecex	$⊢ (A \in ℝ \land A \neq 0) \to \exists x \in ℝ A x = 1$

Proof

Step	Hyp	Ref	Expression
1		elreal	$⊢ A \in ℝ \leftrightarrow \exists y \in 𝑹 ⟨y, 0_{𝑹}⟩ = A$
2		df-rex	$⊢ \exists y \in 𝑹 ⟨y, 0_{𝑹}⟩ = A \leftrightarrow \exists y (y \in 𝑹 \land ⟨y, 0_{𝑹}⟩ = A)$
3	1 2	bitri	$⊢ A \in ℝ \leftrightarrow \exists y (y \in 𝑹 \land ⟨y, 0_{𝑹}⟩ = A)$
4		neeq1	$⊢ ⟨y, 0_{𝑹}⟩ = A \to (⟨y, 0_{𝑹}⟩ \neq 0 \leftrightarrow A \neq 0)$
5		oveq1	$⊢ ⟨y, 0_{𝑹}⟩ = A \to ⟨y, 0_{𝑹}⟩ x = A x$
6	5	eqeq1d	$⊢ ⟨y, 0_{𝑹}⟩ = A \to (⟨y, 0_{𝑹}⟩ x = 1 \leftrightarrow A x = 1)$
7	6	rexbidv	$⊢ ⟨y, 0_{𝑹}⟩ = A \to (\exists x \in ℝ ⟨y, 0_{𝑹}⟩ x = 1 \leftrightarrow \exists x \in ℝ A x = 1)$
8	4 7	imbi12d	$⊢ ⟨y, 0_{𝑹}⟩ = A \to ((⟨y, 0_{𝑹}⟩ \neq 0 \to \exists x \in ℝ ⟨y, 0_{𝑹}⟩ x = 1) \leftrightarrow (A \neq 0 \to \exists x \in ℝ A x = 1))$
9		df-0	$⊢ 0 = ⟨0_{𝑹}, 0_{𝑹}⟩$
10	9	eqeq2i	$⊢ ⟨y, 0_{𝑹}⟩ = 0 \leftrightarrow ⟨y, 0_{𝑹}⟩ = ⟨0_{𝑹}, 0_{𝑹}⟩$
11		vex	$⊢ y \in V$
12	11	eqresr	$⊢ ⟨y, 0_{𝑹}⟩ = ⟨0_{𝑹}, 0_{𝑹}⟩ \leftrightarrow y = 0_{𝑹}$
13	10 12	bitri	$⊢ ⟨y, 0_{𝑹}⟩ = 0 \leftrightarrow y = 0_{𝑹}$
14	13	necon3bii	$⊢ ⟨y, 0_{𝑹}⟩ \neq 0 \leftrightarrow y \neq 0_{𝑹}$
15		recexsr	$⊢ (y \in 𝑹 \land y \neq 0_{𝑹}) \to \exists z \in 𝑹 y \cdot_{𝑹} z = 1_{𝑹}$
16	15	ex	$⊢ y \in 𝑹 \to (y \neq 0_{𝑹} \to \exists z \in 𝑹 y \cdot_{𝑹} z = 1_{𝑹})$
17		opelreal	$⊢ ⟨z, 0_{𝑹}⟩ \in ℝ \leftrightarrow z \in 𝑹$
18	17	anbi1i	$⊢ (⟨z, 0_{𝑹}⟩ \in ℝ \land ⟨y, 0_{𝑹}⟩ ⟨z, 0_{𝑹}⟩ = 1) \leftrightarrow (z \in 𝑹 \land ⟨y, 0_{𝑹}⟩ ⟨z, 0_{𝑹}⟩ = 1)$
19		mulresr	$⊢ (y \in 𝑹 \land z \in 𝑹) \to ⟨y, 0_{𝑹}⟩ ⟨z, 0_{𝑹}⟩ = ⟨y \cdot_{𝑹} z, 0_{𝑹}⟩$
20	19	eqeq1d	$⊢ (y \in 𝑹 \land z \in 𝑹) \to (⟨y, 0_{𝑹}⟩ ⟨z, 0_{𝑹}⟩ = 1 \leftrightarrow ⟨y \cdot_{𝑹} z, 0_{𝑹}⟩ = 1)$
21		df-1	$⊢ 1 = ⟨1_{𝑹}, 0_{𝑹}⟩$
22	21	eqeq2i	$⊢ ⟨y \cdot_{𝑹} z, 0_{𝑹}⟩ = 1 \leftrightarrow ⟨y \cdot_{𝑹} z, 0_{𝑹}⟩ = ⟨1_{𝑹}, 0_{𝑹}⟩$
23		ovex	$⊢ y \cdot_{𝑹} z \in V$
24	23	eqresr	$⊢ ⟨y \cdot_{𝑹} z, 0_{𝑹}⟩ = ⟨1_{𝑹}, 0_{𝑹}⟩ \leftrightarrow y \cdot_{𝑹} z = 1_{𝑹}$
25	22 24	bitri	$⊢ ⟨y \cdot_{𝑹} z, 0_{𝑹}⟩ = 1 \leftrightarrow y \cdot_{𝑹} z = 1_{𝑹}$
26	20 25	bitrdi	$⊢ (y \in 𝑹 \land z \in 𝑹) \to (⟨y, 0_{𝑹}⟩ ⟨z, 0_{𝑹}⟩ = 1 \leftrightarrow y \cdot_{𝑹} z = 1_{𝑹})$
27	26	pm5.32da	$⊢ y \in 𝑹 \to ((z \in 𝑹 \land ⟨y, 0_{𝑹}⟩ ⟨z, 0_{𝑹}⟩ = 1) \leftrightarrow (z \in 𝑹 \land y \cdot_{𝑹} z = 1_{𝑹}))$
28	18 27	bitrid	$⊢ y \in 𝑹 \to ((⟨z, 0_{𝑹}⟩ \in ℝ \land ⟨y, 0_{𝑹}⟩ ⟨z, 0_{𝑹}⟩ = 1) \leftrightarrow (z \in 𝑹 \land y \cdot_{𝑹} z = 1_{𝑹}))$
29		oveq2	$⊢ x = ⟨z, 0_{𝑹}⟩ \to ⟨y, 0_{𝑹}⟩ x = ⟨y, 0_{𝑹}⟩ ⟨z, 0_{𝑹}⟩$
30	29	eqeq1d	$⊢ x = ⟨z, 0_{𝑹}⟩ \to (⟨y, 0_{𝑹}⟩ x = 1 \leftrightarrow ⟨y, 0_{𝑹}⟩ ⟨z, 0_{𝑹}⟩ = 1)$
31	30	rspcev	$⊢ (⟨z, 0_{𝑹}⟩ \in ℝ \land ⟨y, 0_{𝑹}⟩ ⟨z, 0_{𝑹}⟩ = 1) \to \exists x \in ℝ ⟨y, 0_{𝑹}⟩ x = 1$
32	28 31	syl6bir	$⊢ y \in 𝑹 \to ((z \in 𝑹 \land y \cdot_{𝑹} z = 1_{𝑹}) \to \exists x \in ℝ ⟨y, 0_{𝑹}⟩ x = 1)$
33	32	expd	$⊢ y \in 𝑹 \to (z \in 𝑹 \to (y \cdot_{𝑹} z = 1_{𝑹} \to \exists x \in ℝ ⟨y, 0_{𝑹}⟩ x = 1))$
34	33	rexlimdv	$⊢ y \in 𝑹 \to (\exists z \in 𝑹 y \cdot_{𝑹} z = 1_{𝑹} \to \exists x \in ℝ ⟨y, 0_{𝑹}⟩ x = 1)$
35	16 34	syld	$⊢ y \in 𝑹 \to (y \neq 0_{𝑹} \to \exists x \in ℝ ⟨y, 0_{𝑹}⟩ x = 1)$
36	14 35	biimtrid	$⊢ y \in 𝑹 \to (⟨y, 0_{𝑹}⟩ \neq 0 \to \exists x \in ℝ ⟨y, 0_{𝑹}⟩ x = 1)$
37	3 8 36	gencl	$⊢ A \in ℝ \to (A \neq 0 \to \exists x \in ℝ A x = 1)$
38	37	imp	$⊢ (A \in ℝ \land A \neq 0) \to \exists x \in ℝ A x = 1$

Metamath Proof Explorer

Theorem axrrecex

Proof