Theorem exps0

Description: Surreal exponentiation to zero. (Contributed by Scott Fenton, 24-Jul-2025)

	Ref	Expression
Assertion	exps0	|- ( A e. No -> ( A ^su 0s ) = 1s )

Proof

Step	Hyp	Ref	Expression
1		0zs	|- 0s e. ZZ_s
2		expsval	|- ( ( A e. No /\ 0s e. ZZ_s ) -> ( A ^su 0s ) = if ( 0s = 0s , 1s , if ( 0s
3	1 2	mpan2	|- ( A e. No -> ( A ^su 0s ) = if ( 0s = 0s , 1s , if ( 0s
4		eqid	|- 0s = 0s
5	4	iftruei	|- if ( 0s = 0s , 1s , if ( 0s
6	3 5	eqtrdi	|- ( A e. No -> ( A ^su 0s ) = 1s )