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 28397
Description: Define surreal exponentiation. Compare df-exp 14103. (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 28396 . 2 class s
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 csur 27684 . . 3 class No
5 czs 28364 . . 3 class s
63cv 1539 . . . . 5 class 𝑦
7 c0s 27867 . . . . 5 class 0s
86, 7wceq 1540 . . . 4 wff 𝑦 = 0s
9 c1s 27868 . . . 4 class 1s
10 cslt 27685 . . . . . 6 class <s
117, 6, 10wbr 5143 . . . . 5 wff 0s <s 𝑦
12 cmuls 28132 . . . . . . 7 class ·s
13 cnns 28319 . . . . . . . 8 class s
142cv 1539 . . . . . . . . 9 class 𝑥
1514csn 4626 . . . . . . . 8 class {𝑥}
1613, 15cxp 5683 . . . . . . 7 class (ℕs × {𝑥})
1712, 16, 9cseqs 28289 . . . . . 6 class seqs 1s ( ·s , (ℕs × {𝑥}))
186, 17cfv 6561 . . . . 5 class (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦)
19 cnegs 28051 . . . . . . . 8 class -us
206, 19cfv 6561 . . . . . . 7 class ( -us𝑦)
2120, 17cfv 6561 . . . . . 6 class (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦))
22 cdivs 28213 . . . . . 6 class /su
239, 21, 22co 7431 . . . . 5 class ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦)))
2411, 18, 23cif 4525 . . . 4 class if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦))))
258, 9, 24cif 4525 . . 3 class if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦)))))
262, 3, 4, 5, 25cmpo 7433 . 2 class (𝑥 No , 𝑦 ∈ ℤs ↦ if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us𝑦))))))
271, 26wceq 1540 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  28408
  Copyright terms: Public domain W3C validator