Metamath Proof Explorer

Theorem expsval

Description: The value of surreal exponentiation. (Contributed by Scott Fenton, 24-Jul-2025)

Ref Expression
Assertion expsval ( ( 𝐴 ∈ No ∧ 𝐵 ∈ ℤs ) → ( 𝐴 ↑s 𝐵 ) = if ( 𝐵 = 0s , 1s , if ( 0s <s 𝐵 , ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝐵 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝐵 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eqidd ⊢ ( 𝑥 = 𝐴 → 1s = 1s )
2 eqidd ⊢ ( 𝑥 = 𝐴 → ·s = ·s )
3 sneq ⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
4 3 xpeq2d ⊢ ( 𝑥 = 𝐴 → ( ℕs × { 𝑥 } ) = ( ℕs × { 𝐴 } ) )
5 1 2 4 seqseq123d ⊢ ( 𝑥 = 𝐴 → seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) = seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) )
6 5 fveq1d ⊢ ( 𝑥 = 𝐴 → ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ 𝑦 ) = ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑦 ) )
7 5 fveq1d ⊢ ( 𝑥 = 𝐴 → ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) ) = ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝑦 ) ) )
8 7 oveq2d ⊢ ( 𝑥 = 𝐴 → ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) = ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) )
9 6 8 ifeq12d ⊢ ( 𝑥 = 𝐴 → if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) ) = if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) ) )
10 9 ifeq2d ⊢ ( 𝑥 = 𝐴 → if ( 𝑦 = 0s , 1s , if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) ) ) = if ( 𝑦 = 0s , 1s , if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) ) ) )
11 eqeq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 = 0s ↔ 𝐵 = 0s ) )
12 breq2 ⊢ ( 𝑦 = 𝐵 → ( 0s <s 𝑦 ↔ 0s <s 𝐵 ) )
13 fveq2 ⊢ ( 𝑦 = 𝐵 → ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑦 ) = ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝐵 ) )
14 2fveq3 ⊢ ( 𝑦 = 𝐵 → ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝑦 ) ) = ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝐵 ) ) )
15 14 oveq2d ⊢ ( 𝑦 = 𝐵 → ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) = ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝐵 ) ) ) )
16 12 13 15 ifbieq12d ⊢ ( 𝑦 = 𝐵 → if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) ) = if ( 0s <s 𝐵 , ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝐵 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝐵 ) ) ) ) )
17 11 16 ifbieq2d ⊢ ( 𝑦 = 𝐵 → if ( 𝑦 = 0s , 1s , if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) ) ) = if ( 𝐵 = 0s , 1s , if ( 0s <s 𝐵 , ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝐵 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝐵 ) ) ) ) ) )
18 df-exps ⊢ ↑s = ( 𝑥 ∈ No , 𝑦 ∈ ℤs ↦ if ( 𝑦 = 0s , 1s , if ( 0s <s 𝑦 , ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝑥 } ) ) ‘ ( -us ‘ 𝑦 ) ) ) ) ) )
19 1sno ⊢ 1s ∈ No
20 19 elexi ⊢ 1s ∈ V
21 fvex ⊢ ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝐵 ) ∈ V
22 ovex ⊢ ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝐵 ) ) ) ∈ V
23 21 22 ifex ⊢ if ( 0s <s 𝐵 , ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝐵 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝐵 ) ) ) ) ∈ V
24 20 23 ifex ⊢ if ( 𝐵 = 0s , 1s , if ( 0s <s 𝐵 , ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝐵 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝐵 ) ) ) ) ) ∈ V
25 10 17 18 24 ovmpo ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ ℤs ) → ( 𝐴 ↑s 𝐵 ) = if ( 𝐵 = 0s , 1s , if ( 0s <s 𝐵 , ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 𝐵 ) , ( 1s /su ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ ( -us ‘ 𝐵 ) ) ) ) ) )