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	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑁 +s 1s ) ) = ( ( 𝐴 ↑s 𝑁 ) ·s 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eln0s	⊢ ( 𝑁 ∈ ℕ0s ↔ ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ) )
2		1no	⊢ 1s ∈ No
3	2	a1i	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → 1s ∈ No )
4		dfnns2	⊢ ℕs = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω )
5	4	a1i	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → ℕs = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 1s ) “ ω ) )
6		simpr	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → 𝑁 ∈ ℕs )
7	3 5 6	seqsp1	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( 𝑁 +s 1s ) ) = ( ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑁 ) ·s ( ( ℕs × { 𝐴 } ) ‘ ( 𝑁 +s 1s ) ) ) )
8		peano2nns	⊢ ( 𝑁 ∈ ℕs → ( 𝑁 +s 1s ) ∈ ℕs )
9		fvconst2g	⊢ ( ( 𝐴 ∈ No ∧ ( 𝑁 +s 1s ) ∈ ℕs ) → ( ( ℕs × { 𝐴 } ) ‘ ( 𝑁 +s 1s ) ) = 𝐴 )
10	8 9	sylan2	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → ( ( ℕs × { 𝐴 } ) ‘ ( 𝑁 +s 1s ) ) = 𝐴 )
11	10	oveq2d	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → ( ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑁 ) ·s ( ( ℕs × { 𝐴 } ) ‘ ( 𝑁 +s 1s ) ) ) = ( ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑁 ) ·s 𝐴 ) )
12	7 11	eqtrd	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( 𝑁 +s 1s ) ) = ( ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑁 ) ·s 𝐴 ) )
13		expnnsval	⊢ ( ( 𝐴 ∈ No ∧ ( 𝑁 +s 1s ) ∈ ℕs ) → ( 𝐴 ↑s ( 𝑁 +s 1s ) ) = ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( 𝑁 +s 1s ) ) )
14	8 13	sylan2	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → ( 𝐴 ↑s ( 𝑁 +s 1s ) ) = ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( 𝑁 +s 1s ) ) )
15		expnnsval	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → ( 𝐴 ↑s 𝑁 ) = ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑁 ) )
16	15	oveq1d	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → ( ( 𝐴 ↑s 𝑁 ) ·s 𝐴 ) = ( ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑁 ) ·s 𝐴 ) )
17	12 14 16	3eqtr4d	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕs ) → ( 𝐴 ↑s ( 𝑁 +s 1s ) ) = ( ( 𝐴 ↑s 𝑁 ) ·s 𝐴 ) )
18		mulslid	⊢ ( 𝐴 ∈ No → ( 1s ·s 𝐴 ) = 𝐴 )
19	18	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 = 0s ) → ( 1s ·s 𝐴 ) = 𝐴 )
20		oveq2	⊢ ( 𝑁 = 0s → ( 𝐴 ↑s 𝑁 ) = ( 𝐴 ↑s 0s ) )
21		exps0	⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 0s ) = 1s )
22	20 21	sylan9eqr	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 = 0s ) → ( 𝐴 ↑s 𝑁 ) = 1s )
23	22	oveq1d	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 = 0s ) → ( ( 𝐴 ↑s 𝑁 ) ·s 𝐴 ) = ( 1s ·s 𝐴 ) )
24		oveq1	⊢ ( 𝑁 = 0s → ( 𝑁 +s 1s ) = ( 0s +s 1s ) )
25		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
26	2 25	ax-mp	⊢ ( 0s +s 1s ) = 1s
27	24 26	eqtrdi	⊢ ( 𝑁 = 0s → ( 𝑁 +s 1s ) = 1s )
28	27	oveq2d	⊢ ( 𝑁 = 0s → ( 𝐴 ↑s ( 𝑁 +s 1s ) ) = ( 𝐴 ↑s 1s ) )
29		exps1	⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 1s ) = 𝐴 )
30	28 29	sylan9eqr	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 = 0s ) → ( 𝐴 ↑s ( 𝑁 +s 1s ) ) = 𝐴 )
31	19 23 30	3eqtr4rd	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 = 0s ) → ( 𝐴 ↑s ( 𝑁 +s 1s ) ) = ( ( 𝐴 ↑s 𝑁 ) ·s 𝐴 ) )
32	17 31	jaodan	⊢ ( ( 𝐴 ∈ No ∧ ( 𝑁 ∈ ℕs ∨ 𝑁 = 0s ) ) → ( 𝐴 ↑s ( 𝑁 +s 1s ) ) = ( ( 𝐴 ↑s 𝑁 ) ·s 𝐴 ) )
33	1 32	sylan2b	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s ( 𝑁 +s 1s ) ) = ( ( 𝐴 ↑s 𝑁 ) ·s 𝐴 ) )