Definition df-exp 4676

Description: Define exponentiation to natural number powers. This definition is not intended to be used directly. Instead, exp1t 4679 and expp1t 4678 provide the 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 expvalt 4677 for a description of how the sequence builder is used.

Assertion

Ref	Expression
df-exp	⊢ ↑ = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℕ) ∧ z = (( · seq(ℕ × {x})) ‘y))}

Distinct variable group(s):   x,y,z

TD>16

Detailed syntax breakdown of Definition df-exp

Step	Hyp	Ref	Expression
1		cexp 4675	. 2 class ↑
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cc 4026	. . . . . 6 class ℂ
5	3, 4	wcel 1092	. . . . 5 wff x ∈ ℂ
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8		cn 4093	. . . . . 6 class ℕ
9	7, 8	wcel 1092	. . . . 5 wff y ∈ ℕ
10	5, 9	wa 196	. . . 4 wff (x ∈ ℂ ∧ y ∈ ℕ)
11		vz	. . . . . 6 set z
12	11	cv 1089	. . . . 5 class z
13		cmulc 4032	. . . . . . 7 class ·
14	3	csn 1808	. . . . . . . 8 class {x}
15	8, 14	cxp 2408	. . . . . . 7 class (ℕ × {x})
	cseq 4660	. . . . . . 7 class seq
17	13, 15, 16	co 3001	. . . . . 6 class ( · seq(ℕ × {x}))
18	7, 17	cfv 2422	. . . . 5 class (( · seq(ℕ × {x})) ‘y)
19	12, 18	wceq 1091	. . . 4 wff z = (( · seq(ℕ × {x})) ‘y)
20	10, 19	wa 196	. . 3 wff ((x ∈ ℂ ∧ y ∈ ℕ) ∧ z = (( · seq(ℕ × {x})) ‘y))
21	20, 2, 6, 11	copab2 3002	. 2 class {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℕ) ∧ z = (( · seq(ℕ × {x})) ‘y))}
22	1, 21	wceq 1091	1 wff ↑ = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℕ) ∧ z = (( · seq(ℕ × {x})) ‘y))}

This definition is referenced by:  expvalt 4677

metamath.org