Metamath Proof Explorer

Theorem expsnnval

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

Ref Expression
Assertion expsnnval 
|- ( ( A e. No /\ N e. NN_s ) -> ( A ^su N ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) )

Proof

Step Hyp Ref Expression
1 nnzs 
 |-  ( N e. NN_s -> N e. ZZ_s )
2 expsval 
 |-  ( ( A e. No /\ N e. ZZ_s ) -> ( A ^su N ) = if ( N = 0s , 1s , if ( 0s
3 1 2 sylan2 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( A ^su N ) = if ( N = 0s , 1s , if ( 0s
4 nnne0s 
 |-  ( N e. NN_s -> N =/= 0s )
5 4 neneqd 
 |-  ( N e. NN_s -> -. N = 0s )
6 5 iffalsed 
 |-  ( N e. NN_s -> if ( N = 0s , 1s , if ( 0s
7 nnsgt0 
 |-  ( N e. NN_s -> 0s
8 7 iftrued 
 |-  ( N e. NN_s -> if ( 0s
9 6 8 eqtrd 
 |-  ( N e. NN_s -> if ( N = 0s , 1s , if ( 0s
10 9 adantl 
 |-  ( ( A e. No /\ N e. NN_s ) -> if ( N = 0s , 1s , if ( 0s
11 3 10 eqtrd 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( A ^su N ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) )