ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-exp Unicode version

Definition df-exp 10233
Description: Define exponentiation to nonnegative integer powers. For example,  ( 5 ^ 2 )  =  2 5 (ex-exp 12762).

This definition is not meant to be used directly; instead, exp0 10237 and expp1 10240 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts.

10-Jun-2005: The definition was extended to include zero exponents, so that  0 ^ 0  =  1 per the convention of Definition 10-4.1 of [Gleason] p. 134 (0exp0e1 10238).

4-Jun-2014: The definition was extended to include negative integer exponents. For example,  ( -u 3 ^
-u 2 )  =  ( 1  /  9
) (ex-exp 12762). The case  x  =  0 ,  y  <  0 gives the value  ( 1  /  0 ), so we will avoid this case in our theorems. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.)

Assertion
Ref Expression
df-exp  |-  ^  =  ( x  e.  CC ,  y  e.  ZZ  |->  if ( y  =  0 ,  1 ,  if ( 0  <  y ,  (  seq 1
(  x.  ,  ( NN  X.  { x } ) ) `  y ) ,  ( 1  /  (  seq 1 (  x.  , 
( NN  X.  {
x } ) ) `
 -u y ) ) ) ) )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-exp
StepHypRef Expression
1 cexp 10232 . 2  class  ^
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cc 7582 . . 3  class  CC
5 cz 9005 . . 3  class  ZZ
63cv 1313 . . . . 5  class  y
7 cc0 7584 . . . . 5  class  0
86, 7wceq 1314 . . . 4  wff  y  =  0
9 c1 7585 . . . 4  class  1
10 clt 7764 . . . . . 6  class  <
117, 6, 10wbr 3897 . . . . 5  wff  0  <  y
12 cmul 7589 . . . . . . 7  class  x.
13 cn 8677 . . . . . . . 8  class  NN
142cv 1313 . . . . . . . . 9  class  x
1514csn 3495 . . . . . . . 8  class  { x }
1613, 15cxp 4505 . . . . . . 7  class  ( NN 
X.  { x }
)
1712, 16, 9cseq 10158 . . . . . 6  class  seq 1
(  x.  ,  ( NN  X.  { x } ) )
186, 17cfv 5091 . . . . 5  class  (  seq 1 (  x.  , 
( NN  X.  {
x } ) ) `
 y )
196cneg 7898 . . . . . . 7  class  -u y
2019, 17cfv 5091 . . . . . 6  class  (  seq 1 (  x.  , 
( NN  X.  {
x } ) ) `
 -u y )
21 cdiv 8392 . . . . . 6  class  /
229, 20, 21co 5740 . . . . 5  class  ( 1  /  (  seq 1
(  x.  ,  ( NN  X.  { x } ) ) `  -u y ) )
2311, 18, 22cif 3442 . . . 4  class  if ( 0  <  y ,  (  seq 1 (  x.  ,  ( NN 
X.  { x }
) ) `  y
) ,  ( 1  /  (  seq 1
(  x.  ,  ( NN  X.  { x } ) ) `  -u y ) ) )
248, 9, 23cif 3442 . . 3  class  if ( y  =  0 ,  1 ,  if ( 0  <  y ,  (  seq 1 (  x.  ,  ( NN 
X.  { x }
) ) `  y
) ,  ( 1  /  (  seq 1
(  x.  ,  ( NN  X.  { x } ) ) `  -u y ) ) ) )
252, 3, 4, 5, 24cmpo 5742 . 2  class  ( x  e.  CC ,  y  e.  ZZ  |->  if ( y  =  0 ,  1 ,  if ( 0  <  y ,  (  seq 1 (  x.  ,  ( NN 
X.  { x }
) ) `  y
) ,  ( 1  /  (  seq 1
(  x.  ,  ( NN  X.  { x } ) ) `  -u y ) ) ) ) )
261, 25wceq 1314 1  wff  ^  =  ( x  e.  CC ,  y  e.  ZZ  |->  if ( y  =  0 ,  1 ,  if ( 0  <  y ,  (  seq 1
(  x.  ,  ( NN  X.  { x } ) ) `  y ) ,  ( 1  /  (  seq 1 (  x.  , 
( NN  X.  {
x } ) ) `
 -u y ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  exp3val  10235
  Copyright terms: Public domain W3C validator