recsex

Description: A nonzero surreal has a reciprocal. (Contributed by Scott Fenton, 15-Mar-2025)

		Ref	Expression
	Assertion	recsex	$⊢ (A \in No \land A \neq 0_{s}) \to \exists x \in No A \cdot_{s} x = 1_{s}$

Proof

Step	Hyp	Ref	Expression
1		0no	$⊢ 0_{s} \in No$
2		ltstrine	$⊢ (A \in No \land 0_{s} \in No) \to (A \neq 0_{s} \leftrightarrow (A <_{s} 0_{s} \lor 0_{s} <_{s} A))$
3	1 2	mpan2	$⊢ A \in No \to (A \neq 0_{s} \leftrightarrow (A <_{s} 0_{s} \lor 0_{s} <_{s} A))$
4		ltnegs	$⊢ (A \in No \land 0_{s} \in No) \to (A <_{s} 0_{s} \leftrightarrow +_{s} (0_{s}) <_{s} +_{s} (A))$
5	1 4	mpan2	$⊢ A \in No \to (A <_{s} 0_{s} \leftrightarrow +_{s} (0_{s}) <_{s} +_{s} (A))$
6		neg0s	$⊢ +_{s} (0_{s}) = 0_{s}$
7	6	breq1i	$⊢ +_{s} (0_{s}) <_{s} +_{s} (A) \leftrightarrow 0_{s} <_{s} +_{s} (A)$
8	5 7	bitrdi	$⊢ A \in No \to (A <_{s} 0_{s} \leftrightarrow 0_{s} <_{s} +_{s} (A))$
9		negscl	$⊢ A \in No \to +_{s} (A) \in No$
10		precsex	$⊢ (+_{s} (A) \in No \land 0_{s} <_{s} +_{s} (A)) \to \exists y \in No +_{s} (A) \cdot_{s} y = 1_{s}$
11	9 10	sylan	$⊢ (A \in No \land 0_{s} <_{s} +_{s} (A)) \to \exists y \in No +_{s} (A) \cdot_{s} y = 1_{s}$
12		simprl	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land (y \in No \land +_{s} (A) \cdot_{s} y = 1_{s})) \to y \in No$
13	12	negscld	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land (y \in No \land +_{s} (A) \cdot_{s} y = 1_{s})) \to +_{s} (y) \in No$
14		simpll	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land y \in No) \to A \in No$
15		simpr	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land y \in No) \to y \in No$
16	14 15	mulnegs1d	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land y \in No) \to +_{s} (A) \cdot_{s} y = +_{s} (A \cdot_{s} y)$
17	14 15	mulnegs2d	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land y \in No) \to A \cdot_{s} +_{s} (y) = +_{s} (A \cdot_{s} y)$
18	16 17	eqtr4d	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land y \in No) \to +_{s} (A) \cdot_{s} y = A \cdot_{s} +_{s} (y)$
19	18	eqeq1d	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land y \in No) \to (+_{s} (A) \cdot_{s} y = 1_{s} \leftrightarrow A \cdot_{s} +_{s} (y) = 1_{s})$
20	19	biimpd	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land y \in No) \to (+_{s} (A) \cdot_{s} y = 1_{s} \to A \cdot_{s} +_{s} (y) = 1_{s})$
21	20	impr	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land (y \in No \land +_{s} (A) \cdot_{s} y = 1_{s})) \to A \cdot_{s} +_{s} (y) = 1_{s}$
22		oveq2	$⊢ x = +_{s} (y) \to A \cdot_{s} x = A \cdot_{s} +_{s} (y)$
23	22	eqeq1d	$⊢ x = +_{s} (y) \to (A \cdot_{s} x = 1_{s} \leftrightarrow A \cdot_{s} +_{s} (y) = 1_{s})$
24	23	rspcev	$⊢ (+_{s} (y) \in No \land A \cdot_{s} +_{s} (y) = 1_{s}) \to \exists x \in No A \cdot_{s} x = 1_{s}$
25	13 21 24	syl2anc	$⊢ ((A \in No \land 0_{s} <_{s} +_{s} (A)) \land (y \in No \land +_{s} (A) \cdot_{s} y = 1_{s})) \to \exists x \in No A \cdot_{s} x = 1_{s}$
26	11 25	rexlimddv	$⊢ (A \in No \land 0_{s} <_{s} +_{s} (A)) \to \exists x \in No A \cdot_{s} x = 1_{s}$
27	26	ex	$⊢ A \in No \to (0_{s} <_{s} +_{s} (A) \to \exists x \in No A \cdot_{s} x = 1_{s})$
28	8 27	sylbid	$⊢ A \in No \to (A <_{s} 0_{s} \to \exists x \in No A \cdot_{s} x = 1_{s})$
29		precsex	$⊢ (A \in No \land 0_{s} <_{s} A) \to \exists x \in No A \cdot_{s} x = 1_{s}$
30	29	ex	$⊢ A \in No \to (0_{s} <_{s} A \to \exists x \in No A \cdot_{s} x = 1_{s})$
31	28 30	jaod	$⊢ A \in No \to ((A <_{s} 0_{s} \lor 0_{s} <_{s} A) \to \exists x \in No A \cdot_{s} x = 1_{s})$
32	3 31	sylbid	$⊢ A \in No \to (A \neq 0_{s} \to \exists x \in No A \cdot_{s} x = 1_{s})$
33	32	imp	$⊢ (A \in No \land A \neq 0_{s}) \to \exists x \in No A \cdot_{s} x = 1_{s}$

Metamath Proof Explorer

Theorem recsex

Proof