MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-exps Structured version   Visualization version   GIF version

Definition df-exps 28411
Description: Define surreal exponentiation. Compare df-exp 14099. (Contributed by Scott Fenton, 27-May-2025.)
Assertion
Ref Expression
df-exps s = (𝑥 No , 𝑦 ∈ ℤs ↦ if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦))))))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-exps
StepHypRef Expression
1 cexps 28410 . 2 class s
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 csur 27698 . . 3 class No
5 czs 28378 . . 3 class s
63cv 1535 . . . . 5 class 𝑦
7 c0s 27881 . . . . 5 class 0s
86, 7wceq 1536 . . . 4 wff 𝑦 = 0s
9 c1s 27882 . . . 4 class 1s
10 cslt 27699 . . . . . 6 class <s
117, 6, 10wbr 5147 . . . . 5 wff 0s <s 𝑦
12 cmuls 28146 . . . . . . 7 class ·s
13 cnns 28333 . . . . . . . 8 class s
142cv 1535 . . . . . . . . 9 class 𝑥
1514csn 4630 . . . . . . . 8 class {𝑥}
1613, 15cxp 5686 . . . . . . 7 class (ℕs × {𝑥})
1712, 16, 9cseqs 28303 . . . . . 6 class seqs 1s ( ·s , (ℕs × {𝑥}))
186, 17cfv 6562 . . . . 5 class (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦)
19 cnegs 28065 . . . . . . . 8 class -us
206, 19cfv 6562 . . . . . . 7 class ( -us𝑦)
2120, 17cfv 6562 . . . . . 6 class (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦))
22 cdivs 28227 . . . . . 6 class /su
239, 21, 22co 7430 . . . . 5 class ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦)))
2411, 18, 23cif 4530 . . . 4 class if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦))))
258, 9, 24cif 4530 . . 3 class if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦)))))
262, 3, 4, 5, 25cmpo 7432 . 2 class (𝑥 No , 𝑦 ∈ ℤs ↦ if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦))))))
271, 26wceq 1536 1 wff s = (𝑥 No , 𝑦 ∈ ℤs ↦ if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦))))))
Colors of variables: wff setvar class
This definition is referenced by:  expsval  28422
  Copyright terms: Public domain W3C validator