recsne0

Description: If a surreal has a reciprocal, then it is non-zero. (Contributed by Scott Fenton, 5-Sep-2025)

Step	Hyp	Ref	Expression
1		recsne0.1	$⊢ φ \to A \in No$
2		recsne0.2	$⊢ φ \to \exists x \in No A \cdot_{s} x = 1_{s}$
3		oveq2	$⊢ x = y \to A \cdot_{s} x = A \cdot_{s} y$
4	3	eqeq1d	$⊢ x = y \to (A \cdot_{s} x = 1_{s} \leftrightarrow A \cdot_{s} y = 1_{s})$
5	4	cbvrexvw	$⊢ \exists x \in No A \cdot_{s} x = 1_{s} \leftrightarrow \exists y \in No A \cdot_{s} y = 1_{s}$
6	2 5	sylib	$⊢ φ \to \exists y \in No A \cdot_{s} y = 1_{s}$
7		simprr	$⊢ (φ \land (y \in No \land A \cdot_{s} y = 1_{s})) \to A \cdot_{s} y = 1_{s}$
8		1sne0s	$⊢ 1_{s} \neq 0_{s}$
9	8	a1i	$⊢ (φ \land (y \in No \land A \cdot_{s} y = 1_{s})) \to 1_{s} \neq 0_{s}$
10	7 9	eqnetrd	$⊢ (φ \land (y \in No \land A \cdot_{s} y = 1_{s})) \to A \cdot_{s} y \neq 0_{s}$
11	1	adantr	$⊢ (φ \land (y \in No \land A \cdot_{s} y = 1_{s})) \to A \in No$
12		simprl	$⊢ (φ \land (y \in No \land A \cdot_{s} y = 1_{s})) \to y \in No$
13	11 12	mulsne0bd	$⊢ (φ \land (y \in No \land A \cdot_{s} y = 1_{s})) \to (A \cdot_{s} y \neq 0_{s} \leftrightarrow (A \neq 0_{s} \land y \neq 0_{s}))$
14	10 13	mpbid	$⊢ (φ \land (y \in No \land A \cdot_{s} y = 1_{s})) \to (A \neq 0_{s} \land y \neq 0_{s})$
15	14	simpld	$⊢ (φ \land (y \in No \land A \cdot_{s} y = 1_{s})) \to A \neq 0_{s}$
16	6 15	rexlimddv	$⊢ φ \to A \neq 0_{s}$

Metamath Proof Explorer