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	Could not format assertion : No typesetting found for |- ( ( A e. No /\ N e. NN0_s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eln0s	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(N\in {\mathbb{N}}_s\vee N=0_s\right)$$
2		1no	$$⊢1_s\in \mathrm{No}$$
3	2	a1i	$$⊢\left(A\in \mathrm{No}\wedge N\in {\mathbb{N}}_s\right)\to 1_s\in \mathrm{No}$$
4		dfnns2	$$⊢{\mathbb{N}}_s=\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right),1_s\right)\left[\mathrm{\omega }\right]$$
5	4	a1i	$$⊢\left(A\in \mathrm{No}\wedge N\in {\mathbb{N}}_s\right)\to {\mathbb{N}}_s=\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right),1_s\right)\left[\mathrm{\omega }\right]$$
6		simpr	$$⊢\left(A\in \mathrm{No}\wedge N\in {\mathbb{N}}_s\right)\to N\in {\mathbb{N}}_s$$
7	3 5 6	seqsp1	$$⊢\left(A\in \mathrm{No}\wedge N\in {\mathbb{N}}_s\right)\to {seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N{+}_s{1}_s\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\right){\cdot }_s\left({\mathbb{N}}_s\times \left\{A\right\}\right)\left(N{+}_s{1}_s\right)$$
8		peano2nns	$$⊢N\in {\mathbb{N}}_s\to N{+}_s{1}_s\in {\mathbb{N}}_s$$
9		fvconst2g	$$⊢\left(A\in \mathrm{No}\wedge N{+}_s{1}_s\in {\mathbb{N}}_s\right)\to \left({\mathbb{N}}_s\times \left\{A\right\}\right)\left(N{+}_s{1}_s\right)=A$$
10	8 9	sylan2	$$⊢\left(A\in \mathrm{No}\wedge N\in {\mathbb{N}}_s\right)\to \left({\mathbb{N}}_s\times \left\{A\right\}\right)\left(N{+}_s{1}_s\right)=A$$
11	10	oveq2d	$$⊢\left(A\in \mathrm{No}\wedge N\in {\mathbb{N}}_s\right)\to {seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\right){\cdot }_s\left({\mathbb{N}}_s\times \left\{A\right\}\right)\left(N{+}_s{1}_s\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\right){\cdot }_{s}A$$
12	7 11	eqtrd	$$⊢\left(A\in \mathrm{No}\wedge N\in {\mathbb{N}}_s\right)\to {seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N{+}_s{1}_s\right)={seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(N\right){\cdot }_{s}A$$
13		expnnsval	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
14	8 13	sylan2	Could not format ( ( A e. No /\ N e. NN_s ) -> ( A ^su ( N +s 1s ) ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( N +s 1s ) ) ) : No typesetting found for |- ( ( A e. No /\ N e. NN_s ) -> ( A ^su ( N +s 1s ) ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( N +s 1s ) ) ) with typecode |-
15		expnnsval	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 |-
16	15	oveq1d	Could not format ( ( 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 ) ) : No typesetting found for |- ( ( 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 ) ) with typecode |-
17	12 14 16	3eqtr4d	Could not format ( ( A e. No /\ N e. NN_s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) ) : No typesetting found for |- ( ( A e. No /\ N e. NN_s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) ) with typecode |-
18		mulslid	$$⊢A\in \mathrm{No}\to 1_s{\cdot }_{s}A=A$$
19	18	adantr	$$⊢\left(A\in \mathrm{No}\wedge N=0_s\right)\to 1_s{\cdot }_{s}A=A$$
20		oveq2	Could not format ( N = 0s -> ( A ^su N ) = ( A ^su 0s ) ) : No typesetting found for |- ( N = 0s -> ( A ^su N ) = ( A ^su 0s ) ) with typecode |-
21		exps0	Could not format ( A e. No -> ( A ^su 0s ) = 1s ) : No typesetting found for |- ( A e. No -> ( A ^su 0s ) = 1s ) with typecode |-
22	20 21	sylan9eqr	Could not format ( ( A e. No /\ N = 0s ) -> ( A ^su N ) = 1s ) : No typesetting found for |- ( ( A e. No /\ N = 0s ) -> ( A ^su N ) = 1s ) with typecode |-
23	22	oveq1d	Could not format ( ( A e. No /\ N = 0s ) -> ( ( A ^su N ) x.s A ) = ( 1s x.s A ) ) : No typesetting found for |- ( ( A e. No /\ N = 0s ) -> ( ( A ^su N ) x.s A ) = ( 1s x.s A ) ) with typecode |-
24		oveq1	$$⊢N=0_s\to N{+}_s{1}_s=0_s{+}_s{1}_s$$
25		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
26	2 25	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
27	24 26	eqtrdi	$$⊢N=0_s\to N{+}_s{1}_s=1_s$$
28	27	oveq2d	Could not format ( N = 0s -> ( A ^su ( N +s 1s ) ) = ( A ^su 1s ) ) : No typesetting found for |- ( N = 0s -> ( A ^su ( N +s 1s ) ) = ( A ^su 1s ) ) with typecode |-
29		exps1	Could not format ( A e. No -> ( A ^su 1s ) = A ) : No typesetting found for |- ( A e. No -> ( A ^su 1s ) = A ) with typecode |-
30	28 29	sylan9eqr	Could not format ( ( A e. No /\ N = 0s ) -> ( A ^su ( N +s 1s ) ) = A ) : No typesetting found for |- ( ( A e. No /\ N = 0s ) -> ( A ^su ( N +s 1s ) ) = A ) with typecode |-
31	19 23 30	3eqtr4rd	Could not format ( ( A e. No /\ N = 0s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) ) : No typesetting found for |- ( ( A e. No /\ N = 0s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) ) with typecode |-
32	17 31	jaodan	Could not format ( ( A e. No /\ ( N e. NN_s \/ N = 0s ) ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) ) : No typesetting found for |- ( ( A e. No /\ ( N e. NN_s \/ N = 0s ) ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) ) with typecode |-
33	1 32	sylan2b	Could not format ( ( A e. No /\ N e. NN0_s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) ) : No typesetting found for |- ( ( A e. No /\ N e. NN0_s ) -> ( A ^su ( N +s 1s ) ) = ( ( A ^su N ) x.s A ) ) with typecode |-