Definition df-exp 6501

Description: Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0t 6503 and expp1t 6506 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 expnnvalt 6504 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 6500	. 2 class ^
2		vx	. . . . . . 7 set x
3	2	cv 952	. . . . . 6 class x
4		cc 5204	. . . . . 6 class CC
5	3, 4	wcel 955	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 952	. . . . . 6 class y
8		cn0 5269	. . . . . 6 class NN0
9	7, 8	wcel 955	. . . . 5 wff y e. NN0
10	5, 9	wa 223	. . . 4 wff (x e. CC /\ y e. NN0)
11		vz	. . . . . 6 set z
12	11	cv 952	. . . . 5 class z
13		cc0 5206	. . . . . . 7 class 0
14	7, 13	wceq 953	. . . . . 6 wff y = 0
15		c1 5207	. . . . . 6 class 1
16		cmul 5211	. . . . . . . 8 class x.
17		cn 5268	. . . . . . . . 9 class NN
18	3	csn 2399	. . . . . . . . 9 class {x}
19	17, 18	cxp 3158	. . . . . . . 8 class (NN X. {x})
20		cseq1 6244	. . . . . . . 8 class seq1
21	16, 19, 20	co 3948	. . . . . . 7 class ( x. seq1 (NN X. {x}))
22	7, 21	cfv 3172	. . . . . 6 class (( x. seq1 (NN X. {x}))` y)
23	14, 15, 22	cif 2351	. . . . 5 class if(y = 0, 1, (( x. seq1 (NN X. {x}))` y))
24	12, 23	wceq 953	. . . 4 wff z = if(y = 0, 1, (( x. seq1 (NN X. {x}))` y))
25	10, 24	wa 223	. . 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 3949	. 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 953	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:  expvalt 6502

Copyright terms: Public domain