Metamath Proof Explorer

Theorem expscl

Description: Closure law for surreal exponentiation. (Contributed by Scott Fenton, 7-Aug-2025)

Ref Expression
Assertion expscl 
|- ( ( A e. No /\ N e. NN0_s ) -> ( A ^su N ) e. No )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = 0s -> ( A ^su m ) = ( A ^su 0s ) )
2 1 eleq1d 
 |-  ( m = 0s -> ( ( A ^su m ) e. No <-> ( A ^su 0s ) e. No ) )
3 2 imbi2d 
 |-  ( m = 0s -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su 0s ) e. No ) ) )
4 oveq2 
 |-  ( m = n -> ( A ^su m ) = ( A ^su n ) )
5 4 eleq1d 
 |-  ( m = n -> ( ( A ^su m ) e. No <-> ( A ^su n ) e. No ) )
6 5 imbi2d 
 |-  ( m = n -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su n ) e. No ) ) )
7 oveq2 
 |-  ( m = ( n +s 1s ) -> ( A ^su m ) = ( A ^su ( n +s 1s ) ) )
8 7 eleq1d 
 |-  ( m = ( n +s 1s ) -> ( ( A ^su m ) e. No <-> ( A ^su ( n +s 1s ) ) e. No ) )
9 8 imbi2d 
 |-  ( m = ( n +s 1s ) -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su ( n +s 1s ) ) e. No ) ) )
10 oveq2 
 |-  ( m = N -> ( A ^su m ) = ( A ^su N ) )
11 10 eleq1d 
 |-  ( m = N -> ( ( A ^su m ) e. No <-> ( A ^su N ) e. No ) )
12 11 imbi2d 
 |-  ( m = N -> ( ( A e. No -> ( A ^su m ) e. No ) <-> ( A e. No -> ( A ^su N ) e. No ) ) )
13 exps0 
 |-  ( A e. No -> ( A ^su 0s ) = 1s )
14 1sno 
 |-  1s e. No
15 13 14 eqeltrdi 
 |-  ( A e. No -> ( A ^su 0s ) e. No )
16 simp2 
 |-  ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> A e. No )
17 simp1 
 |-  ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> n e. NN0_s )
18 expsp1 
 |-  ( ( A e. No /\ n e. NN0_s ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) )
19 16 17 18 syl2anc 
 |-  ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) )
20 simp3 
 |-  ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( A ^su n ) e. No )
21 20 16 mulscld 
 |-  ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( ( A ^su n ) x.s A ) e. No )
22 19 21 eqeltrd 
 |-  ( ( n e. NN0_s /\ A e. No /\ ( A ^su n ) e. No ) -> ( A ^su ( n +s 1s ) ) e. No )
23 22 3exp 
 |-  ( n e. NN0_s -> ( A e. No -> ( ( A ^su n ) e. No -> ( A ^su ( n +s 1s ) ) e. No ) ) )
24 23 a2d 
 |-  ( n e. NN0_s -> ( ( A e. No -> ( A ^su n ) e. No ) -> ( A e. No -> ( A ^su ( n +s 1s ) ) e. No ) ) )
25 3 6 9 12 15 24 n0sind 
 |-  ( N e. NN0_s -> ( A e. No -> ( A ^su N ) e. No ) )
26 25 impcom 
 |-  ( ( A e. No /\ N e. NN0_s ) -> ( A ^su N ) e. No )