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	⊢ ↑ = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℤ ↦ if ( 𝑦 = 0 , 1 , if ( 0 < 𝑦 , ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cexp	⊢ ↑
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		vy	⊢ 𝑦
4		cz	⊢ ℤ
5	3	cv	⊢ 𝑦
6		cc0	⊢ 0
7	5 6	wceq	⊢ 𝑦 = 0
8		c1	⊢ 1
9		clt	⊢ <
10	6 5 9	wbr	⊢ 0 < 𝑦
11		cmul	⊢ ·
12		cn	⊢ ℕ
13	1	cv	⊢ 𝑥
14	13	csn	⊢ { 𝑥 }
15	12 14	cxp	⊢ ( ℕ × { 𝑥 } )
16	11 15 8	cseq	⊢ seq 1 ( · , ( ℕ × { 𝑥 } ) )
17	5 16	cfv	⊢ ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ 𝑦 )
18		cdiv	⊢ /
19	5	cneg	⊢ - 𝑦
20	19 16	cfv	⊢ ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 )
21	8 20 18	co	⊢ ( 1 / ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) )
22	10 17 21	cif	⊢ if ( 0 < 𝑦 , ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) ) )
23	7 8 22	cif	⊢ if ( 𝑦 = 0 , 1 , if ( 0 < 𝑦 , ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) ) ) )
24	1 3 2 4 23	cmpo	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℤ ↦ if ( 𝑦 = 0 , 1 , if ( 0 < 𝑦 , ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) ) ) ) )
25	0 24	wceq	⊢ ↑ = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℤ ↦ if ( 𝑦 = 0 , 1 , if ( 0 < 𝑦 , ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ 𝑦 ) , ( 1 / ( seq 1 ( · , ( ℕ × { 𝑥 } ) ) ‘ - 𝑦 ) ) ) ) )