Definition df-exp

Description: Define exponentiation to nonnegative integer powers. For example, ( 5 ^ 2 ) = 2 5 ( ex-exp ). Terminology: In general, "exponentiation" is the operation of raising a "base" x to the power of the "exponent" y , resulting in the "power" ( x ^ y ) , also called "x to the power of y". In this case, "integer exponentiation" is the operation of raising a complex "base" x to the power of an integer y , resulting in the "integer power" ( x ^ y ) .

This definition is not meant to be used directly; instead, exp0 and expp1 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 ).

4-Jun-2014: The definition was extended to include negative integer exponents. For example, ( -u 3 ^ -u 2 ) = ( 1 / 9 ) ( ex-exp ). The case x = 0 , y < 0 gives the value ( 1 / 0 ) , so we will avoid this case in our theorems.

For a definition of exponentiation including complex exponents see df-cxp (complex exponentiation). Both definitions are equivalent for integer exponents, see cxpexpz . (Contributed by Raph Levien, 20-May-2004) (Revised by NM, 15-Oct-2004)

	Ref	Expression
Assertion	df-exp	$$⊢^=\left(x\in ℂ,y\in \mathbb{Z}⟼if\left(y=0,1,if\left(0<y,seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(y\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-y\right)}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cexp	$$class^$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		vy	$$setvary$$
4		cz	$$class\mathbb{Z}$$
5	3	cv	$$setvary$$
6		cc0	$$class0$$
7	5 6	wceq	$$wffy=0$$
8		c1	$$class1$$
9		clt	$$class<$$
10	6 5 9	wbr	$$wff0<y$$
11		cmul	$$class\times$$
12		cn	$$class\mathbb{N}$$
13	1	cv	$$setvarx$$
14	13	csn	$$class\left\{x\right\}$$
15	12 14	cxp	$$class\left(\mathbb{N}\times \left\{x\right\}\right)$$
16	11 15 8	cseq	$$classseq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)$$
17	5 16	cfv	$$classseq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(y\right)$$
18		cdiv	$$class÷$$
19	5	cneg	$$class\left(-y\right)$$
20	19 16	cfv	$$classseq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-y\right)$$
21	8 20 18	co	$$class\left(\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-y\right)}\right)$$
22	10 17 21	cif	$$classif\left(0<y,seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(y\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-y\right)}\right)$$
23	7 8 22	cif	$$classif\left(y=0,1,if\left(0<y,seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(y\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-y\right)}\right)\right)$$
24	1 3 2 4 23	cmpo	$$class\left(x\in ℂ,y\in \mathbb{Z}⟼if\left(y=0,1,if\left(0<y,seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(y\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-y\right)}\right)\right)\right)$$
25	0 24	wceq	$$wff^=\left(x\in ℂ,y\in \mathbb{Z}⟼if\left(y=0,1,if\left(0<y,seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(y\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{x\right\}\right)\right)\left(-y\right)}\right)\right)\right)$$