Theorem expnnsval

Description: Value of surreal exponentiation at a natural number. (Contributed by Scott Fenton, 25-Jul-2025)

	Ref	Expression
Assertion	expnnsval	Could not format assertion : No typesetting found for |- ( ( A e. No /\ N e. NN_s ) -> ( A ^su N ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nnzs	$$⊢N\in {\mathbb{N}}_s\to N\in {\mathbb{Z}}_s$$
2		expsval	Could not format ( ( A e. No /\ N e. ZZ_s ) -> ( A ^su N ) = if ( N = 0s , 1s , if ( 0s ( A ^su N ) = if ( N = 0s , 1s , if ( 0s
3	1 2	sylan2	Could not format ( ( A e. No /\ N e. NN_s ) -> ( A ^su N ) = if ( N = 0s , 1s , if ( 0s ( A ^su N ) = if ( N = 0s , 1s , if ( 0s
4		nnne0s	$$⊢N\in {\mathbb{N}}_s\to N\ne 0_s$$
5	4	neneqd	$$⊢N\in {\mathbb{N}}_s\to \neg N=0_s$$
6	5	iffalsed	$$⊢N\in {\mathbb{N}}_s\to if\left(N=0_s,1_s,if\left(0_s{<}_{s}N,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\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(N\right)\right)\right)\right)=if\left(0_s{<}_{s}N,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\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(N\right)\right)\right)$$
7		nnsgt0	$$⊢N\in {\mathbb{N}}_s\to 0_s{<}_{s}N$$
8	7	iftrued	$$⊢N\in {\mathbb{N}}_s\to if\left(0_s{<}_{s}N,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\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(N\right)\right)\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\right)$$
9	6 8	eqtrd	$$⊢N\in {\mathbb{N}}_s\to if\left(N=0_s,1_s,if\left(0_s{<}_{s}N,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\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(N\right)\right)\right)\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\right)$$
10	9	adantl	$$⊢\left(A\in \mathrm{No}\wedge N\in {\mathbb{N}}_s\right)\to if\left(N=0_s,1_s,if\left(0_s{<}_{s}N,{seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\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(N\right)\right)\right)\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\right)$$
11	3 10	eqtrd	Could not format ( ( A e. No /\ N e. NN_s ) -> ( A ^su N ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) ) : No typesetting found for |- ( ( A e. No /\ N e. NN_s ) -> ( A ^su N ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) ) with typecode |-