Metamath Proof Explorer

Theorem expsp1

Description: Value of a surreal number raised to a non-negative integer power plus one. (Contributed by Scott Fenton, 6-Aug-2025)

Ref Expression
Assertion expsp1 
|- ( ( A e. No /\ N e. NN0_s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) )

Proof

Step Hyp Ref Expression
1 eln0s 
 |-  ( N e. NN0_s <-> ( N e. NN_s \/ N = 0s ) )
2 1sno 
 |-  1s e. No
3 2 a1i 
 |-  ( ( A e. No /\ N e. NN_s ) -> 1s e. No )
4 dfnns2 
 |-  NN_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om )
5 4 a1i 
 |-  ( ( A e. No /\ N e. NN_s ) -> NN_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om ) )
6 simpr 
 |-  ( ( A e. No /\ N e. NN_s ) -> N e. NN_s )
7 3 5 6 seqsp1 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( N +s 1s ) ) = ( ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) x.s ( ( NN_s X. { A } ) ` ( N +s 1s ) ) ) )
8 peano2nns 
 |-  ( N e. NN_s -> ( N +s 1s ) e. NN_s )
9 fvconst2g 
 |-  ( ( A e. No /\ ( N +s 1s ) e. NN_s ) -> ( ( NN_s X. { A } ) ` ( N +s 1s ) ) = A )
10 8 9 sylan2 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( ( NN_s X. { A } ) ` ( N +s 1s ) ) = A )
11 10 oveq2d 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) x.s ( ( NN_s X. { A } ) ` ( N +s 1s ) ) ) = ( ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) x.s A ) )
12 7 11 eqtrd 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( N +s 1s ) ) = ( ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) x.s A ) )
13 expsnnval 
 |-  ( ( A e. No /\ ( N +s 1s ) e. NN_s ) -> ( A ^su ( N +s 1s ) ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( N +s 1s ) ) )
14 8 13 sylan2 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( A ^su ( N +s 1s ) ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( N +s 1s ) ) )
15 expsnnval 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( A ^su N ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) )
16 15 oveq1d 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( ( A ^su N ) x.s A ) = ( ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` N ) x.s A ) )
17 12 14 16 3eqtr4d 
 |-  ( ( A e. No /\ N e. NN_s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) )
18 mulslid 
 |-  ( A e. No -> ( 1s x.s A ) = A )
19 18 adantr 
 |-  ( ( A e. No /\ N = 0s ) -> ( 1s x.s A ) = A )
20 oveq2 
 |-  ( N = 0s -> ( A ^su N ) = ( A ^su 0s ) )
21 exps0 
 |-  ( A e. No -> ( A ^su 0s ) = 1s )
22 20 21 sylan9eqr 
 |-  ( ( A e. No /\ N = 0s ) -> ( A ^su N ) = 1s )
23 22 oveq1d 
 |-  ( ( A e. No /\ N = 0s ) -> ( ( A ^su N ) x.s A ) = ( 1s x.s A ) )
24 oveq1 
 |-  ( N = 0s -> ( N +s 1s ) = ( 0s +s 1s ) )
25 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
26 2 25 ax-mp 
 |-  ( 0s +s 1s ) = 1s
27 24 26 eqtrdi 
 |-  ( N = 0s -> ( N +s 1s ) = 1s )
28 27 oveq2d 
 |-  ( N = 0s -> ( A ^su ( N +s 1s ) ) = ( A ^su 1s ) )
29 exps1 
 |-  ( A e. No -> ( A ^su 1s ) = A )
30 28 29 sylan9eqr 
 |-  ( ( A e. No /\ N = 0s ) -> ( A ^su ( N +s 1s ) ) = A )
31 19 23 30 3eqtr4rd 
 |-  ( ( A e. No /\ N = 0s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) )
32 17 31 jaodan 
 |-  ( ( A e. No /\ ( N e. NN_s \/ N = 0s ) ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) )
33 1 32 sylan2b 
 |-  ( ( A e. No /\ N e. NN0_s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) )