Theorem 1ne0s

Description: Surreal zero does not equal surreal one. (Contributed by Scott Fenton, 5-Sep-2025)

	Ref	Expression
Assertion	1ne0s	$$⊢1_s\ne 0_s$$

Proof

Step	Hyp	Ref	Expression
1		0lt1s	$$⊢0_s{<}_s{1}_s$$
2		gt0ne0s	$$⊢0_s{<}_s{1}_s\to 1_s\ne 0_s$$
3	1 2	ax-mp	$$⊢1_s\ne 0_s$$