Theorem expscllem

Description: Lemma for proving non-negative surreal integer exponentiation closure. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Hypotheses	expscllem.1	|- F C_ No
	expscllem.2	|- ( ( x e. F /\ y e. F ) -> ( x x.s y ) e. F )
	expscllem.3	|- 1s e. F
Assertion	expscllem	|- ( ( A e. F /\ N e. NN0_s ) -> ( A ^su N ) e. F )

Proof

Step	Hyp	Ref	Expression
1		expscllem.1	|- F C_ No
2		expscllem.2	|- ( ( x e. F /\ y e. F ) -> ( x x.s y ) e. F )
3		expscllem.3	|- 1s e. F
4		oveq2	|- ( m = 0s -> ( A ^su m ) = ( A ^su 0s ) )
5	4	eleq1d	|- ( m = 0s -> ( ( A ^su m ) e. F <-> ( A ^su 0s ) e. F ) )
6	5	imbi2d	|- ( m = 0s -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su 0s ) e. F ) ) )
7		oveq2	|- ( m = n -> ( A ^su m ) = ( A ^su n ) )
8	7	eleq1d	|- ( m = n -> ( ( A ^su m ) e. F <-> ( A ^su n ) e. F ) )
9	8	imbi2d	|- ( m = n -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su n ) e. F ) ) )
10		oveq2	|- ( m = ( n +s 1s ) -> ( A ^su m ) = ( A ^su ( n +s 1s ) ) )
11	10	eleq1d	|- ( m = ( n +s 1s ) -> ( ( A ^su m ) e. F <-> ( A ^su ( n +s 1s ) ) e. F ) )
12	11	imbi2d	|- ( m = ( n +s 1s ) -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su ( n +s 1s ) ) e. F ) ) )
13		oveq2	|- ( m = N -> ( A ^su m ) = ( A ^su N ) )
14	13	eleq1d	|- ( m = N -> ( ( A ^su m ) e. F <-> ( A ^su N ) e. F ) )
15	14	imbi2d	|- ( m = N -> ( ( A e. F -> ( A ^su m ) e. F ) <-> ( A e. F -> ( A ^su N ) e. F ) ) )
16	1	sseli	|- ( A e. F -> A e. No )
17		exps0	|- ( A e. No -> ( A ^su 0s ) = 1s )
18	16 17	syl	|- ( A e. F -> ( A ^su 0s ) = 1s )
19	18 3	eqeltrdi	|- ( A e. F -> ( A ^su 0s ) e. F )
20	16	3ad2ant2	|- ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> A e. No )
21		simp1	|- ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> n e. NN0_s )
22		expsp1	|- ( ( A e. No /\ n e. NN0_s ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) )
23	20 21 22	syl2anc	|- ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> ( A ^su ( n +s 1s ) ) = ( ( A ^su n ) x.s A ) )
24	2	caovcl	|- ( ( ( A ^su n ) e. F /\ A e. F ) -> ( ( A ^su n ) x.s A ) e. F )
25	24	ancoms	|- ( ( A e. F /\ ( A ^su n ) e. F ) -> ( ( A ^su n ) x.s A ) e. F )
26	25	3adant1	|- ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> ( ( A ^su n ) x.s A ) e. F )
27	23 26	eqeltrd	|- ( ( n e. NN0_s /\ A e. F /\ ( A ^su n ) e. F ) -> ( A ^su ( n +s 1s ) ) e. F )
28	27	3exp	|- ( n e. NN0_s -> ( A e. F -> ( ( A ^su n ) e. F -> ( A ^su ( n +s 1s ) ) e. F ) ) )
29	28	a2d	|- ( n e. NN0_s -> ( ( A e. F -> ( A ^su n ) e. F ) -> ( A e. F -> ( A ^su ( n +s 1s ) ) e. F ) ) )
30	6 9 12 15 19 29	n0sind	|- ( N e. NN0_s -> ( A e. F -> ( A ^su N ) e. F ) )
31	30	impcom	|- ( ( A e. F /\ N e. NN0_s ) -> ( A ^su N ) e. F )