Metamath Proof Explorer - mmtheorems47

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 4601-4700 - Page 47 of 58

Type	Label	Description
Statement
Theorem	zneo 4601	No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28.
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → ¬ (2 · A) = ((2 · B) + 1))
Theorem	peano2uz 4602	Second Peano postulate for upper integer partition.
⊢ ((A ∈ ℤ ∧ B ∈ {x ∈ ℤ∣A ≤ x}) → (B + 1) ∈ {x ∈ ℤ∣A ≤ x})
Theorem	uzind 4603	Induction on the upper partition of ℤ that starts at an integer B. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction hypothesis. Warning: The HTML proof page is 3/4 megabyte in size. An attempt to shorten it is on my to-do list.
⊢ (x = B → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    &   ⊢ ψ    &   ⊢ (((y ∈ ℤ ∧ B ∈ ℤ) ∧ B ≤ y) → (χ → θ))    ⇒   ⊢ (((A ∈ ℤ ∧ B ∈ ℤ) ∧ B ≤ A) → τ)
Theorem	uzind2 4604	Induction on an upper partition of ℤ that starts at an integer B. The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction hypothesis.
⊢ (x = B → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    &   ⊢ ψ    &   ⊢ ((B ∈ ℤ ∧ y ∈ {z ∈ ℤ∣B ≤ z}) → (χ → θ))    ⇒   ⊢ ((B ∈ ℤ ∧ A ∈ {z ∈ ℤ∣B ≤ z}) → τ)
Theorem	uzwo 4605	Well-ordering principle: any non-empty subset of an upper partition of ℤ has a least element.
⊢ ((B ∈ ℤ ∧ (A ⊆ {z ∈ ℤ∣B ≤ z} ∧ A ≠ ∅)) → ∃x ∈ A ∀y ∈ A x ≤ y)
Theorem	uzwo2 4606	Well-ordering principle: any non-empty subset of an upper partition of ℤ has a unique least element.
⊢ ((B ∈ ℤ ∧ (A ⊆ {z ∈ ℤ∣B ≤ z} ∧ A ≠ ∅)) → ∃!x ∈ A ∀y ∈ A x ≤ y)
Theorem	nnwo 4607	Well-ordering principle: any non-empty set of natural numbers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34.
⊢ ((A ⊆ ℕ ∧ A ≠ ∅) → ∃x ∈ A ∀y ∈ A x ≤ y)
Theorem	nnwoOLD 4608	Well-ordering principle: any non-empty set of natural numbers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34.
⊢ ((A ⊆ ℕ ∧ A ≠ ∅) → ∃x ∈ A ∀y ∈ A x ≤ y)
Theorem	nnwof 4609	Well-ordering principle: any non-empty set of natural numbers has a least element. This version allows x and y to be present in A as long as they are effectively not free.
⊢ (z ∈ A → ∀x z ∈ A)    &   ⊢ (z ∈ A → ∀y z ∈ A)    ⇒   ⊢ ((A ⊆ ℕ ∧ A ≠ ∅) → ∃x ∈ A ∀y ∈ A x ≤ y)
Theorem	nnwos 4610	Well-ordering principle: any non-empty set of natural numbers has a least element (schema form).
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃x ∈ ℕ φ → ∃x ∈ ℕ (φ ∧ ∀y ∈ ℕ (ψ → x ≤ y)))
Theorem	indstr 4611	Strong Mathematical Induction for positive integers (inference schema).
⊢ (x = y → (φ ↔ ψ))    &   ⊢ (x ∈ ℕ → (∀y ∈ ℕ (y < x → ψ) → φ))    ⇒   ⊢ (x ∈ ℕ → φ)
Theorem	nn0ind 4612	Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction hypothesis. (Contributed by Raph Levien, 10-Apr-04. Raph says: "This seems a bit painful. I wonder if an explicit substitution version would be easier.")
⊢ (x = 0 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    &   ⊢ ψ    &   ⊢ (y ∈ ℕ0 → (χ → θ))    ⇒   ⊢ (A ∈ ℕ0 → τ)
Theorem	btwnz 4613	Any real number can be sandwiched between two integers. Exercise 2 of [Apostol] p. 28.
⊢ (A ∈ ℝ → (∃x ∈ ℤ x < A ∧ ∃y ∈ ℤ A < y))
Theorem	uzwo3lem1 4614	Lemma for uzwo3 4616 and zmin 4617.
⊢ R = {z ∈ ℤ∣B ≤ z}    ⇒   ⊢ (B ∈ ℝ → ∃!x ∈ R ∀y ∈ R x ≤ y)
Theorem	uzwo3lem2 4615	Lemma for uzwo3 4616.
⊢ R = {z ∈ ℤ∣B ≤ z}    &   ⊢ S = ∪{w ∈ R∣∀v ∈ R w ≤ v}    ⇒   ⊢ ((B ∈ ℝ ∧ (A ⊆ R ∧ A ≠ ∅)) → ∃!x ∈ A ∀y ∈ A x ≤ y)
Theorem	uzwo3 4616	Well-ordering principle: any non-empty subset of an upper partition of ℤ has a unique least element. This generalization of uzwo2 4606 allows the partition boundary B to be any real number.
⊢ ((B ∈ ℝ ∧ (A ⊆ {z ∈ ℤ∣B ≤ z} ∧ A ≠ ∅)) → ∃!x ∈ A ∀y ∈ A x ≤ y)
Theorem	zmin 4617	There is a unique smallest integer greater than or equal to a given real number.
⊢ (A ∈ ℝ → ∃!x ∈ ℤ (A ≤ x ∧ ∀y ∈ ℤ (A ≤ y → x ≤ y)))
Theorem	zmax 4618	There is a unique largest integer less than or equal to a given real number.
⊢ (A ∈ ℝ → ∃!x ∈ ℤ (x ≤ A ∧ ∀y ∈ ℤ (y ≤ A → y ≤ x)))
Theorem	zbtwnre 4619	There is a unique integer between a real number and the number plus one. Exercise 5 of [Apostol] p. 28.
⊢ (A ∈ ℝ → ∃!x ∈ ℤ (A ≤ x ∧ x < (A + 1)))
Theorem	rebtwnz 4620	There is a unique greatest integer less than or equal to a real number. Exercise 4 of [Apostol] p. 28.
⊢ (A ∈ ℝ → ∃!x ∈ ℤ (x ≤ A ∧ A < (x + 1)))
Syntax	cfl 4621	Extend class notation with floor (greatest integer) function.
class floor
Definition	df-fl 4622	Define the floor (greatest integer) function. See flleltt 4625 for its basic property and flclt 4624 for its closure.
⊢ floor = {⟨x, y⟩∣(x ∈ ℝ ∧ y = ∪{z ∈ ℤ∣(z ≤ x ∧ x < (z + 1))})}
Theorem	flvalt 4623	Value of the floor (greatest integer) function. The floor of A is the (unique) integer less than or equal to A whose successor is strictly greater than A.
⊢ (A ∈ ℝ → (floor ‘A) = ∪{x ∈ ℤ∣(x ≤ A ∧ A < (x + 1))})
Theorem	flclt 4624	The floor (greatest integer) function is an integer (closure law).
⊢ (A ∈ ℝ → (floor ‘A) ∈ ℤ)
Theorem	flleltt 4625	A basic property of the floor (greatest integer) function.
⊢ (A ∈ ℝ → ((floor ‘A) ≤ A ∧ A < ((floor ‘A) + 1)))
Theorem	flgzt 4626	The floor function value is the greatest integer less than or equal to its argument.
⊢ ((A ∈ ℝ ∧ B ∈ ℤ) → (B ≤ A ↔ B ≤ (floor ‘A)))
Theorem	flidt 4627	An integer is its own floor.
⊢ (A ∈ ℤ → (floor ‘A) = A)
Definition	df-q 4628	Define the set of rationals. Definition of rational numbers in [Apostol] p. 22.
⊢ ℚ = {x∣∃y ∈ ℤ ∃z ∈ ℕ x = (y / z)}
Theorem	elq 4629	Membership in the set of rationals.
⊢ (A ∈ ℚ ↔ ∃x ∈ ℤ ∃y ∈ ℕ A = (x / y))
Theorem	znq 4630	The ratio of an integer and a natural number is a rational number.
⊢ ((A ∈ ℤ ∧ B ∈ ℕ) → (A / B) ∈ ℚ)
Theorem	qret 4631	A rational number is a real number.
⊢ (A ∈ ℚ → A ∈ ℝ)
Theorem	zqt 4632	An integer is a rational number.
⊢ (A ∈ ℤ → A ∈ ℚ)
Theorem	zssq 4633	The integers are a subset of the rationals.
⊢ ℤ ⊆ ℚ
Theorem	nn0ssq 4634	The nonnegative integers are a subset of the rationals.
⊢ ℕ0 ⊆ ℚ
Theorem	nnssq 4635	The natural numbers are a subset of the rationals.
⊢ ℕ ⊆ ℚ
Theorem	qssre 4636	The rationals are a subset of the reals.
⊢ ℚ ⊆ ℝ
Theorem	qsscn 4637	The rationals are a subset of the complex numbers.
⊢ ℚ ⊆ ℂ
Theorem	nnqt 4638	A natural number is rational.
⊢ (A ∈ ℕ → A ∈ ℚ)
Theorem	qcnt 4639	A rational number is a complex number.
⊢ (A ∈ ℚ → A ∈ ℂ)
Theorem	reex 4640	The set of real numbers exists.
⊢ ℝ ∈ V
Theorem	qex 4641	The set of rational numbers exists.
⊢ ℚ ∈ V
Theorem	qaddclt 4642	Closure of addition of rationals.
⊢ ((A ∈ ℚ ∧ B ∈ ℚ) → (A + B) ∈ ℚ)
Theorem	qnegclt 4643	Closure law for the negative of a rational.
⊢ (A ∈ ℚ → -A ∈ ℚ)
Theorem	qmulclt 4644	Closure of multiplication of rationals.
⊢ ((A ∈ ℚ ∧ B ∈ ℚ) → (A · B) ∈ ℚ)
Theorem	qsubclt 4645	Closure of subtraction of rationals.
⊢ ((A ∈ ℚ ∧ B ∈ ℚ) → (A − B) ∈ ℚ)
Theorem	qrecclt 4646	Closure of reciprocal of rationals.
⊢ ((A ∈ ℚ ∧ A ≠ 0) → (1 / A) ∈ ℚ)
Theorem	qdivclt 4647	Closure of division of rationals.
⊢ (((A ∈ ℚ ∧ B ∈ ℚ) ∧ B ≠ 0) → (A / B) ∈ ℚ)
Theorem	qrevaddclt 4648	Reverse closure law for addition of rationals.
⊢ (B ∈ ℚ → ((A ∈ ℂ ∧ (A + B) ∈ ℚ) ↔ A ∈ ℚ))
Theorem	nnrecqt 4649	The reciprocal of a natural number is rational.
⊢ (A ∈ ℕ → (1 / A) ∈ ℚ)
Theorem	qbtwnre 4650	The rational numbers are dense in ℝ: any two real numbers have a rational between them. Exercise 6 of [Apostol] p. 28.
⊢ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ A < B) → ∃x ∈ ℚ (A < x ∧ x < B))
Theorem	om2uz0 4651	The mapping G is a one-to-one mapping from ω onto an upper partition of ℤ that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number C (normally 0 for the upper partition ℕ0 or 1 for the upper partition ℕ), 1 maps to C + 1, etc. This theorem shows the value of G at ordinal natural number zero. (Another version of this series of theorems was contributed by Raph Levien, 10-Apr-04.)
⊢ C ∈ ℤ    &   ⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, C) ↾ ω)    ⇒   ⊢ (G ‘∅) = C
Theorem	om2uzsuc 4652	The value of G (see om2uz0 4651) at a successor.
⊢ C ∈ ℤ    &   ⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, C) ↾ ω)    ⇒   ⊢ (A ∈ ω → (G ‘suc A) = ((G ‘A) + 1))
Theorem	om2uzuz 4653	The value G (see om2uz0 4651) at an ordinal natural number is in the upper partition of ℤ.
⊢ C ∈ ℤ    &   ⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, C) ↾ ω)    ⇒   ⊢ (A ∈ ω → (G ‘A) ∈ {z ∈ ℤ∣C ≤ z})
Theorem	om2uzlt 4654	Less-than relation for G (see om2uz0 4651).
⊢ C ∈ ℤ    &   ⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, C) ↾ ω)    ⇒   ⊢ ((A ∈ ω ∧ B ∈ ω) → (A ∈ B → (G ‘A) < (G ‘B)))
Theorem	om2uzran 4655	Range of G (see om2uz0 4651).
⊢ C ∈ ℤ    &   ⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, C) ↾ ω)    ⇒   ⊢ ran G = {z ∈ ℤ∣C ≤ z}
Theorem	om2uzf1o 4656	G (see om2uz0 4651) is a one-to-one onto mapping.
⊢ C ∈ ℤ    &   ⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, C) ↾ ω)    ⇒   ⊢ G:ω–1-1-onto→{z ∈ ℤ∣C ≤ z}
Theorem	uzrdgval 4657	A helper lemma for the value of a recursive definition generator on an upper partition of ℤ (typically either ℕ or ℕ0) with characteristic function F and initial value A. Normally F is a function on the partition, and A is a member of the partition.
⊢ C ∈ ℤ    &   ⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, C) ↾ ω)    ⇒   ⊢ (B ∈ {z ∈ ℤ∣C ≤ z} → ((rec(F, A) ∘ ◡G) ‘B) = (rec(F, A) ‘(◡G ‘B)))
Theorem	uzrdgini 4658	Initial value of a recursive definition generator on an upper partition of ℤ. See comment in uzrdgval 4657.
⊢ C ∈ ℤ    &   ⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, C) ↾ ω)    ⇒   ⊢ (A ∈ B → ((rec(F, A) ∘ ◡G) ‘C) = A)
Theorem	uzrdgsuc 4659	Successor value of a recursive definition generator on an upper partition of ℤ. See comment in uzrdgval 4657.
⊢ C ∈ ℤ    &   ⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, C) ↾ ω)    ⇒   ⊢ (B ∈ {z ∈ ℤ∣C ≤ z} → ((rec(F, A) ∘ ◡G) ‘(B + 1)) = (F ‘((rec(F, A) ∘ ◡G) ‘B)))
Syntax	cseq 4660	Extend class notation with infinite sequence builder.
class seq
Definition	df-seq 4661	Define a general-purpose operation that builds an infinite sequence (i.e. a function on the natural numbers ℕ) whose value at an index is a function of its previous value and the value of an input sequence at that index. This definition is complicated, but fortunately it is not intended to be used directly. Instead, the only purpose of this definition is to provide us with an object that has the properties expressed by seq1 4670 and seqsuc 4671. Typically, those are the main theorems that would be used in practice. The first operand is the operation that is applied to the previous value and the value of the input sequence (second operand). For example, for the operation +, an input sequence F with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence ( + seqF) with values 1, 3/2, 7/4, 15/8,.., so that (( + seqF) ‘1) = 1, (( + seqF) ‘2) = 3/2, etc. In other words, ( + seqF) transforms a sequence F into an infinite series. ( + seqF) ⇝ 2 means "the sum of F(n) from n = 1 to infinity is 2". Since limits are unique (climuni 4884), then by eusn 1913 and unisn 1932 the "sum of F(n) from n = 1 to infinity" can be expressed as ∪{x∣( + seqF) ⇝ x} (provided the sequence converges) and evaluates to 2 in this example. Internally, a recursive function is defined whose values are ordered pairs starting at ⟨1, (g ‘1)⟩. The first member of the ordered pair is a counter used to select the appropriate value of the input sequence g. The first rec constructs this function on ω, and the converse of the second rec maps ℕ to ω.
⊢ seq = {⟨⟨f, g⟩, h⟩∣h = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2nd ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)f(g ‘((1st ‘z) + 1)))⟩}, ⟨1, (g ‘1)⟩) ∘ ◡(rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)) ‘x)))}}
Theorem	seqlem1 4662	We prove by induction that the first member of the ordered pair value of the internal sequence of seq equals its index.
⊢ G = (rec({⟨x, y⟩∣y = (x + 1)}, 1) ↾ ω)    ⇒   ⊢ (A ∈ ℕ → (1st ‘((rec({⟨z, w⟩∣w = ⟨((1st ‘z) + 1), B⟩}, ⟨1, C⟩) ∘ ◡G) ‘A)) = A)
Theorem	seqlem2 4663	Lemma for sequence builder theorems.
⊢ (A ∈ ℕ → (A + 1) ∈ (ℕ ∖ {1}))
Theorem	seqrval 4664	Value of the characteristic function of the inner recursion in df-seq 4661.
⊢ H = {⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)S(F ‘((1st ‘z) + 1)))⟩}    &   ⊢ A ∈ V    ⇒   ⊢ (H ‘A) = ⟨((1st ‘A) + 1), ((2nd ‘A)S(F ‘((1st ‘A) + 1)))⟩
Theorem	seqval 4665	Value of the infinite sequence builder operation.
⊢ S ∈ V    &   ⊢ F ∈ V    &   ⊢ G = (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)    &   ⊢ H = {⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)S(F ‘((1st ‘z) + 1)))⟩}    ⇒   ⊢ (SseqF) = {⟨x, y⟩∣(x ∈ ℕ ∧ y = (2nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ◡G) ‘x)))}
Theorem	seqfnlem 4666	Lemma for seqfn 4672.
⊢ S ∈ V    &   ⊢ F ∈ V    &   ⊢ G = (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)    &   ⊢ H = {⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)S(F ‘((1st ‘z) + 1)))⟩}    ⇒   ⊢ (SseqF) Fn ℕ
Theorem	seqval2 4667	Value of the value of the infinite sequence builder operation.
⊢ S ∈ V    &   ⊢ F ∈ V    &   ⊢ G = (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)    &   ⊢ H = {⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)S(F ‘((1st ‘z) + 1)))⟩}    ⇒   ⊢ (A ∈ ℕ → ((SseqF) ‘A) = (2nd ‘((rec(H, ⟨1, (F ‘1)⟩) ∘ ◡G) ‘A)))
Theorem	seq1lem 4668	Lemma for seq1 4670.
⊢ S ∈ V    &   ⊢ F ∈ V    &   ⊢ G = (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)    &   ⊢ H = {⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)S(F ‘((1st ‘z) + 1)))⟩}    ⇒   ⊢ ((SseqF) ‘1) = (F ‘1)
Theorem	seqsuclem 4669	Lemma for seqsuc 4671.
⊢ S ∈ V    &   ⊢ F ∈ V    &   ⊢ G = (rec({⟨z, w⟩∣w = (z + 1)}, 1) ↾ ω)    &   ⊢ H = {⟨z, w⟩∣w = ⟨((1st ‘z) + 1), ((2nd ‘z)S(F ‘((1st ‘z) + 1)))⟩}    ⇒   ⊢ (A ∈ ℕ → ((SseqF) ‘(A + 1)) = (((SseqF) ‘A)S(F ‘(A + 1))))
Theorem	seq1 4670	Value of the infinite sequence builder at 1. See description in df-seq 4661.
⊢ S ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ ((SseqF) ‘1) = (F ‘1)
Theorem	seqsuc 4671	Value of the infinite sequence builder at a successor. See description in df-seq 4661.
⊢ S ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ (A ∈ ℕ → ((SseqF) ‘(A + 1)) = (((SseqF) ‘A)S(F ‘(A + 1))))
Theorem	seqfn 4672	Functionality and domain of the infinite sequence builder.
⊢ S ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ (SseqF) Fn ℕ
Theorem	seqrn 4673	Range of the infinite sequence builder.
⊢ S ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ (((F ‘1) ∈ C ∧ (F ↾ (ℕ ∖ {1})):(ℕ ∖ {1})–→D ∧ S:(C × D)–→C) → ran (SseqF) ⊆ C)
Theorem	seqrn2 4674	Range of the infinite sequence builder (special case of seqrn 4673).
⊢ S ∈ V    &   ⊢ F ∈ V    ⇒   ⊢ ((F:ℕ–→C ∧ S:(C × C)–→C) → ran (SseqF) ⊆ C)
Syntax	cexp 4675	Extend class notation to include exponentiation of a complex number to an integer power.
class ↑
Definition	df-exp 4676	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.
⊢ ↑ = {⟨⟨x, y⟩, z⟩∣((x ∈ ℂ ∧ y ∈ ℕ) ∧ z = (( · seq(ℕ × {x})) ‘y))}
Theorem	expvalt 4677	Value of exponentiation to natural number powers. ℕ × {A} is the constant function with value A. The seq operation produces the sequence A, A · A, (A · A) · A,... that we evaluate at index B.
⊢ ((A ∈ ℂ ∧ B ∈ ℕ) → (A↑B) = (( · seq(ℕ × {A})) ‘B))
Theorem	expp1t 4678	Value of a complex number raised to a natural number power plus one.
⊢ ((A ∈ ℂ ∧ B ∈ ℕ) → (A↑(B + 1)) = ((A↑B) · A))
Theorem	exp1t 4679	Value of a complex number raised to the first power.
⊢ (A ∈ ℂ → (A↑1) = A)
Theorem	0expt 4680	Value of zero raised to a natural number power.
⊢ (A ∈ ℕ → (0↑A) = 0)
Theorem	1expt 4681	Value of one raised to a natural number power.
⊢ (A ∈ ℕ → (1↑A) = 1)
Theorem	expcllem 4682	Lemma for proving natural number exponentiation closure laws.
⊢ F ⊆ ℂ    &   ⊢ ((x ∈ F ∧ y ∈ F) → (x · y) ∈ F)    ⇒   ⊢ ((A ∈ F ∧ B ∈ ℕ) → (A↑B) ∈ F)
Theorem	exp2t 4683	Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-04.)
⊢ (A ∈ ℂ → (A↑2) = (A · A))
Theorem	sqclt 4684	Closure of square.
⊢ (A ∈ ℂ → (A↑2) ∈ ℂ)
Theorem	sqval 4685	Value of square. Inference version.
⊢ A ∈ ℂ    ⇒   ⊢ (A↑2) = (A · A)
Theorem	sqcl 4686	Closure of square.
⊢ A ∈ ℂ    ⇒   ⊢ (A↑2) ∈ ℂ
Theorem	sqe0 4687	A number is zero iff its square is zero.
⊢ A ∈ ℂ    ⇒   ⊢ ((A↑2) = 0 ↔ A = 0)
Theorem	sqmul 4688	Distribution of square over multiplication.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A · B)↑2) = ((A↑2) · (B↑2))
Theorem	sqdiv 4689	Distribution of square over division.
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ B ≠ 0    ⇒   ⊢ ((A / B)↑2) = ((A↑2) / (B↑2))
Theorem	sqreci 4690	Square of reciprocal.
⊢ A ∈ ℂ    &   ⊢ A ≠ 0    ⇒   ⊢ ((1 / A)↑2) = (1 / (A↑2))
Theorem	nnexpclt 4691	Closure of nonnegative integer exponentiation of natural numbers.
⊢ ((A ∈ ℕ ∧ B ∈ ℕ) → (A↑B) ∈ ℕ)
Theorem	nn0expclt 4692	Closure of natural number exponentiation of nonnegative integers.
⊢ ((A ∈ ℕ0 ∧ B ∈ ℕ) → (A↑B) ∈ ℕ0)
Theorem	zexpclt 4693	Closure of natural number exponentiation of integers.
⊢ ((A ∈ ℤ ∧ B ∈ ℕ) → (A↑B) ∈ ℤ)
Theorem	qexpclt 4694	Closure of natural number exponentiation of rationals.
⊢ ((A ∈ ℚ ∧ B ∈ ℕ) → (A↑B) ∈ ℚ)
Theorem	reexpclt 4695	Closure of natural number exponentiation of reals.
⊢ ((A ∈ ℝ ∧ B ∈ ℕ) → (A↑B) ∈ ℝ)
Theorem	expclt 4696	Closure law for natural number exponentiation.
⊢ ((A ∈ ℂ ∧ B ∈ ℕ) → (A↑B) ∈ ℂ)
Theorem	sqreclt 4697	Closure of the square of a real number.
⊢ (A ∈ ℝ → (A↑2) ∈ ℝ)
Theorem	expaddt 4698	Sum of exponents law for natural number exponentiation.
⊢ ((A ∈ ℂ ∧ B ∈ ℕ ∧ C ∈ ℕ) → (A↑(B + C)) = ((A↑B) · (A↑C)))
Theorem	sqrecl 4699	Closure of square in reals.
⊢ A ∈ ℝ    ⇒   ⊢ (A↑2) ∈ ℝ
Theorem	lt2sqe 4700	Two nonnegative reals compare the same as their squares.
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → (A < B ↔ (A↑2) < (B↑2)))