P. 90 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8901-9000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	expap0i 8901	Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑𝑁) # 0)
Theorem	expgt0 8902	Nonnegative integer exponentiation with a positive mantissa is positive. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < A) → 0 < (A↑𝑁))
Theorem	expnegzap 8903	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑-𝑁) = (1 / (A↑𝑁)))
Theorem	0exp 8904	Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.)
⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0)
Theorem	expge0 8905	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ A) → 0 ≤ (A↑𝑁))
Theorem	expge1 8906	Nonnegative integer exponentiation with a mantissa greater than or equal to 1 is greater than or equal to 1. (Contributed by NM, 21-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 1 ≤ A) → 1 ≤ (A↑𝑁))
Theorem	expgt1 8907	Positive integer exponentiation with a mantissa greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ ∧ 1 < A) → 1 < (A↑𝑁))
Theorem	mulexp 8908	Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 13-Feb-2005.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((A · B)↑𝑁) = ((A↑𝑁) · (B↑𝑁)))
Theorem	mulexpzap 8909	Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ (((A ∈ ℂ ∧ A # 0) ∧ (B ∈ ℂ ∧ B # 0) ∧ 𝑁 ∈ ℤ) → ((A · B)↑𝑁) = ((A↑𝑁) · (B↑𝑁)))
Theorem	exprecap 8910	Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → ((1 / A)↑𝑁) = (1 / (A↑𝑁)))
Theorem	expadd 8911	Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by NM, 30-Nov-2004.)
⊢ ((A ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁)))
Theorem	expaddzaplem 8912	Lemma for expaddzap 8913. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁)))
Theorem	expaddzap 8913	Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁)))
Theorem	expmul 8914	Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 4-Jan-2006.)
⊢ ((A ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁))
Theorem	expmulzap 8915	Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁))
Theorem	expsubap 8916	Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ (((A ∈ ℂ ∧ A # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (A↑(𝑀 − 𝑁)) = ((A↑𝑀) / (A↑𝑁)))
Theorem	expp1zap 8917	Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑(𝑁 + 1)) = ((A↑𝑁) · A))
Theorem	expm1ap 8918	Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ ((A ∈ ℂ ∧ A # 0 ∧ 𝑁 ∈ ℤ) → (A↑(𝑁 − 1)) = ((A↑𝑁) / A))
Theorem	expdivap 8919	Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ ((A ∈ ℂ ∧ (B ∈ ℂ ∧ B # 0) ∧ 𝑁 ∈ ℕ0) → ((A / B)↑𝑁) = ((A↑𝑁) / (B↑𝑁)))
Theorem	ltexp2a 8920	Ordering relationship for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (((A ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 < A ∧ 𝑀 < 𝑁)) → (A↑𝑀) < (A↑𝑁))
Theorem	leexp2a 8921	Weak ordering relationship for exponentiation. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ ((A ∈ ℝ ∧ 1 ≤ A ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (A↑𝑀) ≤ (A↑𝑁))
Theorem	leexp2r 8922	Weak ordering relationship for exponentiation. (Contributed by Paul Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
⊢ (((A ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) ∧ (0 ≤ A ∧ A ≤ 1)) → (A↑𝑁) ≤ (A↑𝑀))
Theorem	leexp1a 8923	Weak mantissa ordering relationship for exponentiation. (Contributed by NM, 18-Dec-2005.)
⊢ (((A ∈ ℝ ∧ B ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤ A ∧ A ≤ B)) → (A↑𝑁) ≤ (B↑𝑁))
Theorem	exple1 8924	Nonnegative integer exponentiation with a mantissa between 0 and 1 inclusive is less than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A ∧ A ≤ 1) ∧ 𝑁 ∈ ℕ0) → (A↑𝑁) ≤ 1)
Theorem	expubnd 8925	An upper bound on A↑𝑁 when 2 ≤ A. (Contributed by NM, 19-Dec-2005.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ A) → (A↑𝑁) ≤ ((2↑𝑁) · ((A − 1)↑𝑁)))
Theorem	sqval 8926	Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.)
⊢ (A ∈ ℂ → (A↑2) = (A · A))
Theorem	sqneg 8927	The square of the negative of a number.) (Contributed by NM, 15-Jan-2006.)
⊢ (A ∈ ℂ → (-A↑2) = (A↑2))
Theorem	sqsubswap 8928	Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A − B)↑2) = ((B − A)↑2))
Theorem	sqcl 8929	Closure of square. (Contributed by NM, 10-Aug-1999.)
⊢ (A ∈ ℂ → (A↑2) ∈ ℂ)
Theorem	sqmul 8930	Distribution of square over multiplication. (Contributed by NM, 21-Mar-2008.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A · B)↑2) = ((A↑2) · (B↑2)))
Theorem	sqeq0 8931	A number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006.)
⊢ (A ∈ ℂ → ((A↑2) = 0 ↔ A = 0))
Theorem	sqdivap 8932	Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ ∧ B # 0) → ((A / B)↑2) = ((A↑2) / (B↑2)))
Theorem	sqne0 8933	A number is nonzero iff its square is nonzero. (Contributed by NM, 11-Mar-2006.)
⊢ (A ∈ ℂ → ((A↑2) ≠ 0 ↔ A ≠ 0))
Theorem	resqcl 8934	Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.)
⊢ (A ∈ ℝ → (A↑2) ∈ ℝ)
Theorem	sqgt0ap 8935	The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ ((A ∈ ℝ ∧ A # 0) → 0 < (A↑2))
Theorem	nnsqcl 8936	The naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (A ∈ ℕ → (A↑2) ∈ ℕ)
Theorem	zsqcl 8937	Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (A ∈ ℤ → (A↑2) ∈ ℤ)
Theorem	qsqcl 8938	The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (A ∈ ℚ → (A↑2) ∈ ℚ)
Theorem	sq11 8939	The square function is one-to-one for nonnegative reals. (Contributed by NM, 8-Apr-2001.) (Proof shortened by Mario Carneiro, 28-May-2016.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A) ∧ (B ∈ ℝ ∧ 0 ≤ B)) → ((A↑2) = (B↑2) ↔ A = B))
Theorem	lt2sq 8940	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A) ∧ (B ∈ ℝ ∧ 0 ≤ B)) → (A < B ↔ (A↑2) < (B↑2)))
Theorem	le2sq 8941	The square function on nonnegative reals is monotonic. (Contributed by NM, 18-Oct-1999.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A) ∧ (B ∈ ℝ ∧ 0 ≤ B)) → (A ≤ B ↔ (A↑2) ≤ (B↑2)))
Theorem	le2sq2 8942	The square of a 'less than or equal to' ordering. (Contributed by NM, 21-Mar-2008.)
⊢ (((A ∈ ℝ ∧ 0 ≤ A) ∧ (B ∈ ℝ ∧ A ≤ B)) → (A↑2) ≤ (B↑2))
Theorem	sqge0 8943	A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
⊢ (A ∈ ℝ → 0 ≤ (A↑2))
Theorem	zsqcl2 8944	The square of an integer is a nonnegative integer. (Contributed by Mario Carneiro, 18-Apr-2014.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (A ∈ ℤ → (A↑2) ∈ ℕ0)
Theorem	sumsqeq0 8945	Two real numbers are equal to 0 iff their Euclidean norm is. (Contributed by NM, 29-Apr-2005.) (Revised by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 28-May-2016.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ) → ((A = 0 ∧ B = 0) ↔ ((A↑2) + (B↑2)) = 0))
Theorem	sqvali 8946	Value of square. Inference version. (Contributed by NM, 1-Aug-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A↑2) = (A · A)
Theorem	sqcli 8947	Closure of square. (Contributed by NM, 2-Aug-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ (A↑2) ∈ ℂ
Theorem	sqeq0i 8948	A number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.)
⊢ A ∈ ℂ    ⇒   ⊢ ((A↑2) = 0 ↔ A = 0)
Theorem	sqmuli 8949	Distribution of square over multiplication. (Contributed by NM, 3-Sep-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A · B)↑2) = ((A↑2) · (B↑2))
Theorem	sqdivapi 8950	Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    &   ⊢ B # 0    ⇒   ⊢ ((A / B)↑2) = ((A↑2) / (B↑2))
Theorem	resqcli 8951	Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
⊢ A ∈ ℝ    ⇒   ⊢ (A↑2) ∈ ℝ
Theorem	sqgt0api 8952	The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ A ∈ ℝ    ⇒   ⊢ (A # 0 → 0 < (A↑2))
Theorem	sqge0i 8953	A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
⊢ A ∈ ℝ    ⇒   ⊢ 0 ≤ (A↑2)
Theorem	lt2sqi 8954	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 12-Sep-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → (A < B ↔ (A↑2) < (B↑2)))
Theorem	le2sqi 8955	The square function on nonnegative reals is monotonic. (Contributed by NM, 12-Sep-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → (A ≤ B ↔ (A↑2) ≤ (B↑2)))
Theorem	sq11i 8956	The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999.)
⊢ A ∈ ℝ    &   ⊢ B ∈ ℝ    ⇒   ⊢ ((0 ≤ A ∧ 0 ≤ B) → ((A↑2) = (B↑2) ↔ A = B))
Theorem	sq0 8957	The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
⊢ (0↑2) = 0
Theorem	sq0i 8958	If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
⊢ (A = 0 → (A↑2) = 0)
Theorem	sq0id 8959	If a number is zero, its square is zero. Deduction form of sq0i 8958. Converse of sqeq0d 8993. (Contributed by David Moews, 28-Feb-2017.)
⊢ (φ → A = 0)    ⇒   ⊢ (φ → (A↑2) = 0)
Theorem	sq1 8960	The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
⊢ (1↑2) = 1
Theorem	neg1sqe1 8961	-1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (-1↑2) = 1
Theorem	sq2 8962	The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
⊢ (2↑2) = 4
Theorem	sq3 8963	The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
⊢ (3↑2) = 9
Theorem	cu2 8964	The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
⊢ (2↑3) = 8
Theorem	irec 8965	The reciprocal of i. (Contributed by NM, 11-Oct-1999.)
⊢ (1 / i) = -i
Theorem	i2 8966	i squared. (Contributed by NM, 6-May-1999.)
⊢ (i↑2) = -1
Theorem	i3 8967	i cubed. (Contributed by NM, 31-Jan-2007.)
⊢ (i↑3) = -i
Theorem	i4 8968	i to the fourth power. (Contributed by NM, 31-Jan-2007.)
⊢ (i↑4) = 1
Theorem	nnlesq 8969	A positive integer is less than or equal to its square. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁↑2))
Theorem	expnass 8970	A counterexample showing that exponentiation is not associative. (Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
⊢ ((3↑3)↑3) < (3↑(3↑3))
Theorem	subsq 8971	Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A↑2) − (B↑2)) = ((A + B) · (A − B)))
Theorem	subsq2 8972	Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A↑2) − (B↑2)) = (((A − B)↑2) + ((2 · B) · (A − B))))
Theorem	binom2i 8973	The square of a binomial. (Contributed by NM, 11-Aug-1999.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A + B)↑2) = (((A↑2) + (2 · (A · B))) + (B↑2))
Theorem	subsqi 8974	Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A↑2) − (B↑2)) = ((A + B) · (A − B))
Theorem	binom2 8975	The square of a binomial. (Contributed by FL, 10-Dec-2006.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A + B)↑2) = (((A↑2) + (2 · (A · B))) + (B↑2)))
Theorem	binom21 8976	Special case of binom2 8975 where B = 1. (Contributed by Scott Fenton, 11-May-2014.)
⊢ (A ∈ ℂ → ((A + 1)↑2) = (((A↑2) + (2 · A)) + 1))
Theorem	binom2sub 8977	Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A − B)↑2) = (((A↑2) − (2 · (A · B))) + (B↑2)))
Theorem	binom2subi 8978	Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.)
⊢ A ∈ ℂ    &   ⊢ B ∈ ℂ    ⇒   ⊢ ((A − B)↑2) = (((A↑2) − (2 · (A · B))) + (B↑2))
Theorem	binom3 8979	The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
⊢ ((A ∈ ℂ ∧ B ∈ ℂ) → ((A + B)↑3) = (((A↑3) + (3 · ((A↑2) · B))) + ((3 · (A · (B↑2))) + (B↑3))))
Theorem	zesq 8980	An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ((𝑁↑2) / 2) ∈ ℤ))
Theorem	nnesq 8981	A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ↔ ((𝑁↑2) / 2) ∈ ℕ))
Theorem	bernneq 8982	Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤ A) → (1 + (A · 𝑁)) ≤ ((1 + A)↑𝑁))
Theorem	bernneq2 8983	Variation of Bernoulli's inequality bernneq 8982. (Contributed by NM, 18-Oct-2007.)
⊢ ((A ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ A) → (((A − 1) · 𝑁) + 1) ≤ (A↑𝑁))
Theorem	bernneq3 8984	A corollary of bernneq 8982. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 < (𝑃↑𝑁))
Theorem	expnbnd 8985*	Exponentiation with a mantissa greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
⊢ ((A ∈ ℝ ∧ B ∈ ℝ ∧ 1 < B) → ∃𝑘 ∈ ℕ A < (B↑𝑘))
Theorem	expnlbnd 8986*	The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.)
⊢ ((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 < B) → ∃𝑘 ∈ ℕ (1 / (B↑𝑘)) < A)
Theorem	expnlbnd2 8987*	The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
⊢ ((A ∈ ℝ+ ∧ B ∈ ℝ ∧ 1 < B) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(1 / (B↑𝑘)) < A)
Theorem	exp0d 8988	Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑0) = 1)
Theorem	exp1d 8989	Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑1) = A)
Theorem	expeq0d 8990	Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ)    &   ⊢ (φ → (A↑𝑁) = 0)    ⇒   ⊢ (φ → A = 0)
Theorem	sqvald 8991	Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑2) = (A · A))
Theorem	sqcld 8992	Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    ⇒   ⊢ (φ → (A↑2) ∈ ℂ)
Theorem	sqeq0d 8993	A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → (A↑2) = 0)    ⇒   ⊢ (φ → A = 0)
Theorem	expcld 8994	Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℂ)
Theorem	expp1d 8995	Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑(𝑁 + 1)) = ((A↑𝑁) · A))
Theorem	expaddd 8996	Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    &   ⊢ (φ → 𝑀 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑(𝑀 + 𝑁)) = ((A↑𝑀) · (A↑𝑁)))
Theorem	expmuld 8997	Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → 𝑁 ∈ ℕ0)    &   ⊢ (φ → 𝑀 ∈ ℕ0)    ⇒   ⊢ (φ → (A↑(𝑀 · 𝑁)) = ((A↑𝑀)↑𝑁))
Theorem	sqrecapd 8998	Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    ⇒   ⊢ (φ → ((1 / A)↑2) = (1 / (A↑2)))
Theorem	expclzapd 8999	Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) ∈ ℂ)
Theorem	expap0d 9000	Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (φ → A ∈ ℂ)    &   ⊢ (φ → A # 0)    &   ⊢ (φ → 𝑁 ∈ ℤ)    ⇒   ⊢ (φ → (A↑𝑁) # 0)