Theorem recsne0

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

	Ref	Expression
Hypotheses	recsne0.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	recsne0.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s )
Assertion	recsne0	⊢ ( 𝜑 → 𝐴 ≠ 0s )

Proof

Step	Hyp	Ref	Expression
1		recsne0.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		recsne0.2	⊢ ( 𝜑 → ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s )
3		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ·s 𝑥 ) = ( 𝐴 ·s 𝑦 ) )
4	3	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ·s 𝑥 ) = 1s ↔ ( 𝐴 ·s 𝑦 ) = 1s ) )
5	4	cbvrexvw	⊢ ( ∃ 𝑥 ∈ No ( 𝐴 ·s 𝑥 ) = 1s ↔ ∃ 𝑦 ∈ No ( 𝐴 ·s 𝑦 ) = 1s )
6	2 5	sylib	⊢ ( 𝜑 → ∃ 𝑦 ∈ No ( 𝐴 ·s 𝑦 ) = 1s )
7		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ No ∧ ( 𝐴 ·s 𝑦 ) = 1s ) ) → ( 𝐴 ·s 𝑦 ) = 1s )
8		1sne0s	⊢ 1s ≠ 0s
9	8	a1i	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ No ∧ ( 𝐴 ·s 𝑦 ) = 1s ) ) → 1s ≠ 0s )
10	7 9	eqnetrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ No ∧ ( 𝐴 ·s 𝑦 ) = 1s ) ) → ( 𝐴 ·s 𝑦 ) ≠ 0s )
11	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ No ∧ ( 𝐴 ·s 𝑦 ) = 1s ) ) → 𝐴 ∈ No )
12		simprl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ No ∧ ( 𝐴 ·s 𝑦 ) = 1s ) ) → 𝑦 ∈ No )
13	11 12	mulsne0bd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ No ∧ ( 𝐴 ·s 𝑦 ) = 1s ) ) → ( ( 𝐴 ·s 𝑦 ) ≠ 0s ↔ ( 𝐴 ≠ 0s ∧ 𝑦 ≠ 0s ) ) )
14	10 13	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ No ∧ ( 𝐴 ·s 𝑦 ) = 1s ) ) → ( 𝐴 ≠ 0s ∧ 𝑦 ≠ 0s ) )
15	14	simpld	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ No ∧ ( 𝐴 ·s 𝑦 ) = 1s ) ) → 𝐴 ≠ 0s )
16	6 15	rexlimddv	⊢ ( 𝜑 → 𝐴 ≠ 0s )