Metamath Proof Explorer

Definition df-exps

Description: Define surreal exponentiation. Compare df-exp . (Contributed by Scott Fenton, 27-May-2025)

Ref Expression
Assertion df-exps 
|- ^su = ( x e. No , y e. ZZ_s |-> if ( y = 0s , 1s , if ( 0s

Detailed syntax breakdown

Step Hyp Ref Expression
0 cexps 
 |-  ^su
1 vx 
 |-  x
2 csur 
 |-  No
3 vy 
 |-  y
4 czs 
 |-  ZZ_s
5 3 cv 
 |-  y
6 c0s 
 |-  0s
7 5 6 wceq 
 |-  y = 0s
8 c1s 
 |-  1s
9 cslt 
 |-
10 6 5 9 wbr 
 |-  0s
11 cmuls 
 |-  x.s
12 cnns 
 |-  NN_s
13 1 cv 
 |-  x
14 13 csn 
 |-  { x }
15 12 14 cxp 
 |-  ( NN_s X. { x } )
16 11 15 8 cseqs 
 |-  seq_s 1s ( x.s , ( NN_s X. { x } ) )
17 5 16 cfv 
 |-  ( seq_s 1s ( x.s , ( NN_s X. { x } ) ) ` y )
18 cdivs 
 |-  /su
19 cnegs 
 |-  -us
20 5 19 cfv 
 |-  ( -us ` y )
21 20 16 cfv 
 |-  ( seq_s 1s ( x.s , ( NN_s X. { x } ) ) ` ( -us ` y ) )
22 8 21 18 co 
 |-  ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { x } ) ) ` ( -us ` y ) ) )
23 10 17 22 cif 
 |-  if ( 0s
24 7 8 23 cif 
 |-  if ( y = 0s , 1s , if ( 0s
25 1 3 2 4 24 cmpo 
 |-  ( x e. No , y e. ZZ_s |-> if ( y = 0s , 1s , if ( 0s
26 0 25 wceq 
 |-  ^su = ( x e. No , y e. ZZ_s |-> if ( y = 0s , 1s , if ( 0s