Metamath Proof Explorer

Theorem expsnnval

Description: Value of surreal exponentiation at a natural number. (Contributed by Scott Fenton, 25-Jul-2025)

		Ref	Expression
	Assertion	expsnnval	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕ_s ) → ( 𝐴 ↑_s 𝑁 ) = ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		nnzs	⊢ ( 𝑁 ∈ ℕ_s → 𝑁 ∈ ℤ_s )
2		expsval	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℤ_s ) → ( 𝐴 ↑_s 𝑁 ) = if ( 𝑁 = 0_s , 1_s , if ( 0_s <s 𝑁 , ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1_s /_su ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ ( -u_s ‘ 𝑁 ) ) ) ) ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕ_s ) → ( 𝐴 ↑_s 𝑁 ) = if ( 𝑁 = 0_s , 1_s , if ( 0_s <s 𝑁 , ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1_s /_su ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ ( -u_s ‘ 𝑁 ) ) ) ) ) )
4		nnne0s	⊢ ( 𝑁 ∈ ℕ_s → 𝑁 ≠ 0_s )
5	4	neneqd	⊢ ( 𝑁 ∈ ℕ_s → ¬ 𝑁 = 0_s )
6	5	iffalsed	⊢ ( 𝑁 ∈ ℕ_s → if ( 𝑁 = 0_s , 1_s , if ( 0_s <s 𝑁 , ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1_s /_su ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ ( -u_s ‘ 𝑁 ) ) ) ) ) = if ( 0_s <s 𝑁 , ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1_s /_su ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ ( -u_s ‘ 𝑁 ) ) ) ) )
7		nnsgt0	⊢ ( 𝑁 ∈ ℕ_s → 0_s <s 𝑁 )
8	7	iftrued	⊢ ( 𝑁 ∈ ℕ_s → if ( 0_s <s 𝑁 , ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1_s /_su ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ ( -u_s ‘ 𝑁 ) ) ) ) = ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) )
9	6 8	eqtrd	⊢ ( 𝑁 ∈ ℕ_s → if ( 𝑁 = 0_s , 1_s , if ( 0_s <s 𝑁 , ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1_s /_su ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ ( -u_s ‘ 𝑁 ) ) ) ) ) = ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) )
10	9	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕ_s ) → if ( 𝑁 = 0_s , 1_s , if ( 0_s <s 𝑁 , ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) , ( 1_s /_su ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ ( -u_s ‘ 𝑁 ) ) ) ) ) = ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) )
11	3 10	eqtrd	⊢ ( ( 𝐴 ∈ No ∧ 𝑁 ∈ ℕ_s ) → ( 𝐴 ↑_s 𝑁 ) = ( seq_s 1_s ( ·_s , ( ℕ_s × { 𝐴 } ) ) ‘ 𝑁 ) )