P. 106 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10501-10600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	expclzap 10501	Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ)
Theorem	nn0expcli 10502	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ (𝐴↑𝑁) ∈ ℕ0
Theorem	nn0sqcl 10503	The square of a nonnegative integer is a nonnegative integer. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ (𝐴 ∈ ℕ0 → (𝐴↑2) ∈ ℕ0)
Theorem	expm1t 10504	Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = ((𝐴↑(𝑁 − 1)) · 𝐴))
Theorem	1exp 10505	Value of one raised to a nonnegative integer power. (Contributed by NM, 15-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (𝑁 ∈ ℤ → (1↑𝑁) = 1)
Theorem	expap0 10506	Positive integer exponentiation is apart from zero iff its base is apart from zero. That it is easier to prove this first, and then prove expeq0 10507 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." (Remark of [Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) # 0 ↔ 𝐴 # 0))
Theorem	expeq0 10507	Positive integer exponentiation is 0 iff its base is 0. (Contributed by NM, 23-Feb-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0))
Theorem	expap0i 10508	Integer exponentiation is apart from zero if its base is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) # 0)
Theorem	expgt0 10509	A positive real raised to an integer power is positive. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < 𝐴) → 0 < (𝐴↑𝑁))
Theorem	expnegzap 10510	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁)))
Theorem	0exp 10511	Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.)
⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0)
Theorem	expge0 10512	A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴) → 0 ≤ (𝐴↑𝑁))
Theorem	expge1 10513	A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by NM, 21-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 1 ≤ 𝐴) → 1 ≤ (𝐴↑𝑁))
Theorem	expgt1 10514	A real greater than 1 raised to a positive integer is greater than 1. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ∧ 1 < 𝐴) → 1 < (𝐴↑𝑁))
Theorem	mulexp 10515	Nonnegative 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.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁)))
Theorem	mulexpzap 10516	Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝑁 ∈ ℤ) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁)))
Theorem	exprecap 10517	Integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → ((1 / 𝐴)↑𝑁) = (1 / (𝐴↑𝑁)))
Theorem	expadd 10518	Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by NM, 30-Nov-2004.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
Theorem	expaddzaplem 10519	Lemma for expaddzap 10520. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
Theorem	expaddzap 10520	Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
Theorem	expmul 10521	Product of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 4-Jan-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁))
Theorem	expmulzap 10522	Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁))
Theorem	m1expeven 10523	Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018.)
⊢ (𝑁 ∈ ℤ → (-1↑(2 · 𝑁)) = 1)
Theorem	expsubap 10524	Exponent subtraction law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 − 𝑁)) = ((𝐴↑𝑀) / (𝐴↑𝑁)))
Theorem	expp1zap 10525	Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴))
Theorem	expm1ap 10526	Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑(𝑁 − 1)) = ((𝐴↑𝑁) / 𝐴))
Theorem	expdivap 10527	Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝑁 ∈ ℕ0) → ((𝐴 / 𝐵)↑𝑁) = ((𝐴↑𝑁) / (𝐵↑𝑁)))
Theorem	ltexp2a 10528	Ordering relationship for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 < 𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑀) < (𝐴↑𝑁))
Theorem	leexp2a 10529	Weak ordering relationship for exponentiation. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ≤ (𝐴↑𝑁))
Theorem	leexp2r 10530	Weak ordering relationship for exponentiation. (Contributed by Paul Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀))
Theorem	leexp1a 10531	Weak base ordering relationship for exponentiation. (Contributed by NM, 18-Dec-2005.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁))
Theorem	exple1 10532	A real between 0 and 1 inclusive raised to a nonnegative integer is less than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1) ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ≤ 1)
Theorem	expubnd 10533	An upper bound on 𝐴↑𝑁 when 2 ≤ 𝐴. (Contributed by NM, 19-Dec-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴) → (𝐴↑𝑁) ≤ ((2↑𝑁) · ((𝐴 − 1)↑𝑁)))
Theorem	sqval 10534	Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.)
⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴))
Theorem	sqneg 10535	The square of the negative of a number.) (Contributed by NM, 15-Jan-2006.)
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2))
Theorem	sqsubswap 10536	Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = ((𝐵 − 𝐴)↑2))
Theorem	sqcl 10537	Closure of square. (Contributed by NM, 10-Aug-1999.)
⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈ ℂ)
Theorem	sqmul 10538	Distribution of square over multiplication. (Contributed by NM, 21-Mar-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2)))
Theorem	sqeq0 10539	A number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006.)
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0))
Theorem	sqdivap 10540	Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
Theorem	sqne0 10541	A number is nonzero iff its square is nonzero. See also sqap0 10542 which is the same but with not equal changed to apart. (Contributed by NM, 11-Mar-2006.)
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0))
Theorem	sqap0 10542	A number is apart from zero iff its square is apart from zero. (Contributed by Jim Kingdon, 13-Aug-2021.)
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) # 0 ↔ 𝐴 # 0))
Theorem	resqcl 10543	Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.)
⊢ (𝐴 ∈ ℝ → (𝐴↑2) ∈ ℝ)
Theorem	sqgt0ap 10544	The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0) → 0 < (𝐴↑2))
Theorem	nnsqcl 10545	The naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℕ)
Theorem	zsqcl 10546	Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ)
Theorem	qsqcl 10547	The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (𝐴↑2) ∈ ℚ)
Theorem	sq11 10548	The square function is one-to-one for nonnegative reals. Also see sq11ap 10643 which would easily follow from this given excluded middle, but which for us is proved another way. (Contributed by NM, 8-Apr-2001.) (Proof shortened by Mario Carneiro, 28-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵))
Theorem	lt2sq 10549	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2)))
Theorem	le2sq 10550	The square function on nonnegative reals is monotonic. (Contributed by NM, 18-Oct-1999.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2)))
Theorem	le2sq2 10551	The square of a 'less than or equal to' ordering. (Contributed by NM, 21-Mar-2008.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)) → (𝐴↑2) ≤ (𝐵↑2))
Theorem	sqge0 10552	A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴↑2))
Theorem	zsqcl2 10553	The square of an integer is a nonnegative integer. (Contributed by Mario Carneiro, 18-Apr-2014.) (Revised by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℕ0)
Theorem	sumsqeq0 10554	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.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 = 0 ∧ 𝐵 = 0) ↔ ((𝐴↑2) + (𝐵↑2)) = 0))
Theorem	sqvali 10555	Value of square. Inference version. (Contributed by NM, 1-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴↑2) = (𝐴 · 𝐴)
Theorem	sqcli 10556	Closure of square. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴↑2) ∈ ℂ
Theorem	sqeq0i 10557	A number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ ((𝐴↑2) = 0 ↔ 𝐴 = 0)
Theorem	sqmuli 10558	Distribution of square over multiplication. (Contributed by NM, 3-Sep-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))
Theorem	sqdivapi 10559	Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))
Theorem	resqcli 10560	Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴↑2) ∈ ℝ
Theorem	sqgt0api 10561	The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴 # 0 → 0 < (𝐴↑2))
Theorem	sqge0i 10562	A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 0 ≤ (𝐴↑2)
Theorem	lt2sqi 10563	The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 12-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2)))
Theorem	le2sqi 10564	The square function on nonnegative reals is monotonic. (Contributed by NM, 12-Sep-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2)))
Theorem	sq11i 10565	The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵))
Theorem	sq0 10566	The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
⊢ (0↑2) = 0
Theorem	sq0i 10567	If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
⊢ (𝐴 = 0 → (𝐴↑2) = 0)
Theorem	sq0id 10568	If a number is zero, its square is zero. Deduction form of sq0i 10567. Converse of sqeq0d 10608. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 = 0)    ⇒   ⊢ (𝜑 → (𝐴↑2) = 0)
Theorem	sq1 10569	The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
⊢ (1↑2) = 1
Theorem	neg1sqe1 10570	-1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ (-1↑2) = 1
Theorem	sq2 10571	The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
⊢ (2↑2) = 4
Theorem	sq3 10572	The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
⊢ (3↑2) = 9
Theorem	sq4e2t8 10573	The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
⊢ (4↑2) = (2 · 8)
Theorem	cu2 10574	The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
⊢ (2↑3) = 8
Theorem	irec 10575	The reciprocal of i. (Contributed by NM, 11-Oct-1999.)
⊢ (1 / i) = -i
Theorem	i2 10576	i squared. (Contributed by NM, 6-May-1999.)
⊢ (i↑2) = -1
Theorem	i3 10577	i cubed. (Contributed by NM, 31-Jan-2007.)
⊢ (i↑3) = -i
Theorem	i4 10578	i to the fourth power. (Contributed by NM, 31-Jan-2007.)
⊢ (i↑4) = 1
Theorem	nnlesq 10579	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	iexpcyc 10580	Taking i to the 𝐾-th power is the same as using the 𝐾 mod 4 -th power instead, by i4 10578. (Contributed by Mario Carneiro, 7-Jul-2014.)
⊢ (𝐾 ∈ ℤ → (i↑(𝐾 mod 4)) = (i↑𝐾))
Theorem	expnass 10581	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 10582	Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵)))
Theorem	subsq2 10583	Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) − (𝐵↑2)) = (((𝐴 − 𝐵)↑2) + ((2 · 𝐵) · (𝐴 − 𝐵))))
Theorem	binom2i 10584	The square of a binomial. (Contributed by NM, 11-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))
Theorem	subsqi 10585	Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵))
Theorem	qsqeqor 10586	The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)))
Theorem	binom2 10587	The square of a binomial. (Contributed by FL, 10-Dec-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
Theorem	binom21 10588	Special case of binom2 10587 where 𝐵 = 1. (Contributed by Scott Fenton, 11-May-2014.)
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1)↑2) = (((𝐴↑2) + (2 · 𝐴)) + 1))
Theorem	binom2sub 10589	Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
Theorem	binom2sub1 10590	Special case of binom2sub 10589 where 𝐵 = 1. (Contributed by AV, 2-Aug-2021.)
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1)↑2) = (((𝐴↑2) − (2 · 𝐴)) + 1))
Theorem	binom2subi 10591	Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))
Theorem	mulbinom2 10592	The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐶 · 𝐴) + 𝐵)↑2) = ((((𝐶 · 𝐴)↑2) + ((2 · 𝐶) · (𝐴 · 𝐵))) + (𝐵↑2)))
Theorem	binom3 10593	The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
Theorem	zesq 10594	An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ((𝑁↑2) / 2) ∈ ℤ))
Theorem	nnesq 10595	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 10596	Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁))
Theorem	bernneq2 10597	Variation of Bernoulli's inequality bernneq 10596. (Contributed by NM, 18-Oct-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴) → (((𝐴 − 1) · 𝑁) + 1) ≤ (𝐴↑𝑁))
Theorem	bernneq3 10598	A corollary of bernneq 10596. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 < (𝑃↑𝑁))
Theorem	expnbnd 10599*	Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
Theorem	expnlbnd 10600*	The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ (1 / (𝐵↑𝑘)) < 𝐴)