Definition df-exp 6764

Description: Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 6766 and expp1 6769 provide a 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. See expnnval 6767 for a description of how the recursive sequence builder is used. 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. (Based on definition contributed by Raph Levien, 15-Oct-2004.)

Assertion

Ref	Expression
df-exp	|- ^ = {<.<.x, y>., z>. | ((x e. CC /\ y e. NN0) /\ z = if(y = 0, 1, (( x. seq1 (NN X. {x}))` y)))}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-exp

Step	Hyp	Ref	Expression
1		cexp 6763	. 2 class ^
2		vx	. . . . . . 7 set x
3	2	cv 991	. . . . . 6 class x
4		cc 5386	. . . . . 6 class CC
5	3, 4	wcel 994	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 991	. . . . . 6 class y
8		cn0 5451	. . . . . 6 class NN0
9	7, 8	wcel 994	. . . . 5 wff y e. NN0
10	5, 9	wa 221	. . . 4 wff (x e. CC /\ y e. NN0)
11		vz	. . . . . 6 set z
12	11	cv 991	. . . . 5 class z
13		cc0 5388	. . . . . . 7 class 0
14	7, 13	wceq 992	. . . . . 6 wff y = 0
15		c1 5389	. . . . . 6 class 1
16		cmul 5393	. . . . . . . 8 class x.
17		cn 5450	. . . . . . . . 9 class NN
18	3	csn 2467	. . . . . . . . 9 class {x}
19	17, 18	cxp 3249	. . . . . . . 8 class (NN X. {x})
20		cseq1 6672	. . . . . . . 8 class seq1
21	16, 19, 20	co 4021	. . . . . . 7 class ( x. seq1 (NN X. {x}))
22	7, 21	cfv 3263	. . . . . 6 class (( x. seq1 (NN X. {x}))` y)
23	14, 15, 22	cif 2415	. . . . 5 class if(y = 0, 1, (( x. seq1 (NN X. {x}))` y))
24	12, 23	wceq 992	. . . 4 wff z = if(y = 0, 1, (( x. seq1 (NN X. {x}))` y))
25	10, 24	wa 221	. . 3 wff ((x e. CC /\ y e. NN0) /\ z = if(y = 0, 1, (( x. seq1 (NN X. {x}))` y)))
26	25, 2, 6, 11	copab2 4022	. 2 class {<.<.x, y>., z>. | ((x e. CC /\ y e. NN0) /\ z = if(y = 0, 1, (( x. seq1 (NN X. {x}))` y)))}
27	1, 26	wceq 992	1 wff ^ = {<.<.x, y>., z>. | ((x e. CC /\ y e. NN0) /\ z = if(y = 0, 1, (( x. seq1 (NN X. {x}))` y)))}

This definition is referenced by:  expval 6765

Copyright terms: Public domain