Theorem exps0

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

	Ref	Expression
Assertion	exps0	Could not format assertion : No typesetting found for |- ( A e. No -> ( A ^su 0s ) = 1s ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0zs	$$⊢0_s\in {\mathbb{Z}}_s$$
2		expsval	Could not format ( ( A e. No /\ 0s e. ZZ_s ) -> ( A ^su 0s ) = if ( 0s = 0s , 1s , if ( 0s ( A ^su 0s ) = if ( 0s = 0s , 1s , if ( 0s
3	1 2	mpan2	Could not format ( A e. No -> ( A ^su 0s ) = if ( 0s = 0s , 1s , if ( 0s ( A ^su 0s ) = if ( 0s = 0s , 1s , if ( 0s
4		eqid	$$⊢0_s=0_s$$
5	4	iftruei	$$⊢if\left(0_s=0_s,1_s,if\left(0_s{<}_s{0}_s,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(0_s\right),1_s{/}_{\mathrm{su}}{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left({+}_s\left(0_s\right)\right)\right)\right)=1_s$$
6	3 5	eqtrdi	Could not format ( A e. No -> ( A ^su 0s ) = 1s ) : No typesetting found for |- ( A e. No -> ( A ^su 0s ) = 1s ) with typecode |-