Theorem List for Intuitionistic Logic Explorer - 10301-10400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | zexpcl 10301 |
Closure of exponentiation of integers. (Contributed by NM,
16-Dec-2005.)
|
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℤ) |
|
Theorem | qexpcl 10302 |
Closure of exponentiation of rationals. (Contributed by NM,
16-Dec-2005.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℚ) |
|
Theorem | reexpcl 10303 |
Closure of exponentiation of reals. (Contributed by NM,
14-Dec-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ) |
|
Theorem | expcl 10304 |
Closure law for nonnegative integer exponentiation. (Contributed by NM,
26-May-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ) |
|
Theorem | rpexpcl 10305 |
Closure law for exponentiation of positive reals. (Contributed by NM,
24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈
ℝ+) |
|
Theorem | reexpclzap 10306 |
Closure of exponentiation of reals. (Contributed by Jim Kingdon,
9-Jun-2020.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ) |
|
Theorem | qexpclz 10307 |
Closure of exponentiation of rational numbers. (Contributed by Mario
Carneiro, 9-Sep-2014.)
|
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℚ) |
|
Theorem | m1expcl2 10308 |
Closure of exponentiation of negative one. (Contributed by Mario
Carneiro, 18-Jun-2015.)
|
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ {-1,
1}) |
|
Theorem | m1expcl 10309 |
Closure of exponentiation of negative one. (Contributed by Mario
Carneiro, 18-Jun-2015.)
|
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈
ℤ) |
|
Theorem | expclzaplem 10310* |
Closure law for integer exponentiation. Lemma for expclzap 10311 and
expap0i 10318. (Contributed by Jim Kingdon, 9-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ {𝑧 ∈ ℂ ∣ 𝑧 # 0}) |
|
Theorem | expclzap 10311 |
Closure law for integer exponentiation. (Contributed by Jim Kingdon,
9-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ) |
|
Theorem | nn0expcli 10312 |
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 17-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ (𝐴↑𝑁) ∈
ℕ0 |
|
Theorem | nn0sqcl 10313 |
The square of a nonnegative integer is a nonnegative integer.
(Contributed by Stefan O'Rear, 16-Oct-2014.)
|
⊢ (𝐴 ∈ ℕ0 → (𝐴↑2) ∈
ℕ0) |
|
Theorem | expm1t 10314 |
Exponentiation in terms of predecessor exponent. (Contributed by NM,
19-Dec-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = ((𝐴↑(𝑁 − 1)) · 𝐴)) |
|
Theorem | 1exp 10315 |
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 10316 |
Positive integer exponentiation is apart from zero iff its mantissa is
apart from zero. That it is easier to prove this first, and then prove
expeq0 10317 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 10317 |
Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed
by NM, 23-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0)) |
|
Theorem | expap0i 10318 |
Integer exponentiation is apart from zero if its mantissa is apart from
zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) # 0) |
|
Theorem | expgt0 10319 |
Nonnegative integer exponentiation with a positive mantissa is positive.
(Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro,
4-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < 𝐴) → 0 < (𝐴↑𝑁)) |
|
Theorem | expnegzap 10320 |
Value of a complex number raised to a negative power. (Contributed by
Mario Carneiro, 4-Jun-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
|
Theorem | 0exp 10321 |
Value of zero raised to a positive integer power. (Contributed by NM,
19-Aug-2004.)
|
⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0) |
|
Theorem | expge0 10322 |
Nonnegative integer exponentiation with a nonnegative mantissa is
nonnegative. (Contributed by NM, 16-Dec-2005.) (Revised by Mario
Carneiro, 4-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤
𝐴) → 0 ≤ (𝐴↑𝑁)) |
|
Theorem | expge1 10323 |
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.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 1 ≤
𝐴) → 1 ≤ (𝐴↑𝑁)) |
|
Theorem | expgt1 10324 |
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.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ∧ 1 < 𝐴) → 1 < (𝐴↑𝑁)) |
|
Theorem | mulexp 10325 |
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.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
|
Theorem | mulexpzap 10326 |
Integer exponentiation of a product. (Contributed by Jim Kingdon,
10-Jun-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝑁 ∈ ℤ) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
|
Theorem | exprecap 10327 |
Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim
Kingdon, 10-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → ((1 / 𝐴)↑𝑁) = (1 / (𝐴↑𝑁))) |
|
Theorem | expadd 10328 |
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 10329 |
Lemma for expaddzap 10330. (Contributed by Jim Kingdon, 10-Jun-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) |
|
Theorem | expaddzap 10330 |
Sum of exponents law for integer exponentiation. (Contributed by Jim
Kingdon, 10-Jun-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) |
|
Theorem | expmul 10331 |
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.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁)) |
|
Theorem | expmulzap 10332 |
Product of exponents law for integer exponentiation. (Contributed by
Jim Kingdon, 11-Jun-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁)) |
|
Theorem | m1expeven 10333 |
Exponentiation of negative one to an even power. (Contributed by Scott
Fenton, 17-Jan-2018.)
|
⊢ (𝑁 ∈ ℤ → (-1↑(2 ·
𝑁)) = 1) |
|
Theorem | expsubap 10334 |
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 − 𝑁)) = ((𝐴↑𝑀) / (𝐴↑𝑁))) |
|
Theorem | expp1zap 10335 |
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) |
|
Theorem | expm1ap 10336 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑(𝑁 − 1)) = ((𝐴↑𝑁) / 𝐴)) |
|
Theorem | expdivap 10337 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 11-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝑁 ∈ ℕ0) → ((𝐴 / 𝐵)↑𝑁) = ((𝐴↑𝑁) / (𝐵↑𝑁))) |
|
Theorem | ltexp2a 10338 |
Ordering relationship for exponentiation. (Contributed by NM,
2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 < 𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑀) < (𝐴↑𝑁)) |
|
Theorem | leexp2a 10339 |
Weak ordering relationship for exponentiation. (Contributed by NM,
14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ≤ (𝐴↑𝑁)) |
|
Theorem | leexp2r 10340 |
Weak ordering relationship for exponentiation. (Contributed by Paul
Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)) |
|
Theorem | leexp1a 10341 |
Weak mantissa ordering relationship for exponentiation. (Contributed by
NM, 18-Dec-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) |
|
Theorem | exple1 10342 |
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.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ 1) ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ≤ 1) |
|
Theorem | expubnd 10343 |
An upper bound on 𝐴↑𝑁 when 2 ≤ 𝐴. (Contributed by NM,
19-Dec-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤
𝐴) → (𝐴↑𝑁) ≤ ((2↑𝑁) · ((𝐴 − 1)↑𝑁))) |
|
Theorem | sqval 10344 |
Value of the square of a complex number. (Contributed by Raph Levien,
10-Apr-2004.)
|
⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴)) |
|
Theorem | sqneg 10345 |
The square of the negative of a number.) (Contributed by NM,
15-Jan-2006.)
|
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) |
|
Theorem | sqsubswap 10346 |
Swap the order of subtraction in a square. (Contributed by Scott Fenton,
10-Jun-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = ((𝐵 − 𝐴)↑2)) |
|
Theorem | sqcl 10347 |
Closure of square. (Contributed by NM, 10-Aug-1999.)
|
⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈ ℂ) |
|
Theorem | sqmul 10348 |
Distribution of square over multiplication. (Contributed by NM,
21-Mar-2008.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) |
|
Theorem | sqeq0 10349 |
A number is zero iff its square is zero. (Contributed by NM,
11-Mar-2006.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0)) |
|
Theorem | sqdivap 10350 |
Distribution of square over division. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) |
|
Theorem | sqne0 10351 |
A number is nonzero iff its square is nonzero. See also sqap0 10352 which is
the same but with not equal changed to apart. (Contributed by NM,
11-Mar-2006.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0)) |
|
Theorem | sqap0 10352 |
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 10353 |
Closure of the square of a real number. (Contributed by NM,
18-Oct-1999.)
|
⊢ (𝐴 ∈ ℝ → (𝐴↑2) ∈ ℝ) |
|
Theorem | sqgt0ap 10354 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0) → 0 < (𝐴↑2)) |
|
Theorem | nnsqcl 10355 |
The naturals are closed under squaring. (Contributed by Scott Fenton,
29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℕ) |
|
Theorem | zsqcl 10356 |
Integers are closed under squaring. (Contributed by Scott Fenton,
18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ) |
|
Theorem | qsqcl 10357 |
The square of a rational is rational. (Contributed by Stefan O'Rear,
15-Sep-2014.)
|
⊢ (𝐴 ∈ ℚ → (𝐴↑2) ∈ ℚ) |
|
Theorem | sq11 10358 |
The square function is one-to-one for nonnegative reals. Also see
sq11ap 10451 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 10359 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 24-Feb-2006.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) |
|
Theorem | le2sq 10360 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 18-Oct-1999.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) |
|
Theorem | le2sq2 10361 |
The square of a 'less than or equal to' ordering. (Contributed by NM,
21-Mar-2008.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)) → (𝐴↑2) ≤ (𝐵↑2)) |
|
Theorem | sqge0 10362 |
A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴↑2)) |
|
Theorem | zsqcl2 10363 |
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 10364 |
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 10365 |
Value of square. Inference version. (Contributed by NM,
1-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴↑2) = (𝐴 · 𝐴) |
|
Theorem | sqcli 10366 |
Closure of square. (Contributed by NM, 2-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴↑2) ∈ ℂ |
|
Theorem | sqeq0i 10367 |
A number is zero iff its square is zero. (Contributed by NM,
2-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ ((𝐴↑2) = 0 ↔ 𝐴 = 0) |
|
Theorem | sqmuli 10368 |
Distribution of square over multiplication. (Contributed by NM,
3-Sep-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2)) |
|
Theorem | sqdivapi 10369 |
Distribution of square over division. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐵 # 0
⇒ ⊢ ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)) |
|
Theorem | resqcli 10370 |
Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐴↑2) ∈ ℝ |
|
Theorem | sqgt0api 10371 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐴 # 0 → 0 < (𝐴↑2)) |
|
Theorem | sqge0i 10372 |
A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ 0 ≤ (𝐴↑2) |
|
Theorem | lt2sqi 10373 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 12-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) |
|
Theorem | le2sqi 10374 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 12-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) |
|
Theorem | sq11i 10375 |
The square function is one-to-one for nonnegative reals. (Contributed
by NM, 27-Oct-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) |
|
Theorem | sq0 10376 |
The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|
⊢ (0↑2) = 0 |
|
Theorem | sq0i 10377 |
If a number is zero, its square is zero. (Contributed by FL,
10-Dec-2006.)
|
⊢ (𝐴 = 0 → (𝐴↑2) = 0) |
|
Theorem | sq0id 10378 |
If a number is zero, its square is zero. Deduction form of sq0i 10377.
Converse of sqeq0d 10416. (Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 = 0) ⇒ ⊢ (𝜑 → (𝐴↑2) = 0) |
|
Theorem | sq1 10379 |
The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|
⊢ (1↑2) = 1 |
|
Theorem | neg1sqe1 10380 |
-1 squared is 1 (common case). (Contributed by David
A. Wheeler,
8-Dec-2018.)
|
⊢ (-1↑2) = 1 |
|
Theorem | sq2 10381 |
The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|
⊢ (2↑2) = 4 |
|
Theorem | sq3 10382 |
The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|
⊢ (3↑2) = 9 |
|
Theorem | sq4e2t8 10383 |
The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.)
|
⊢ (4↑2) = (2 · 8) |
|
Theorem | cu2 10384 |
The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|
⊢ (2↑3) = 8 |
|
Theorem | irec 10385 |
The reciprocal of i. (Contributed by NM, 11-Oct-1999.)
|
⊢ (1 / i) = -i |
|
Theorem | i2 10386 |
i squared. (Contributed by NM, 6-May-1999.)
|
⊢ (i↑2) = -1 |
|
Theorem | i3 10387 |
i cubed. (Contributed by NM, 31-Jan-2007.)
|
⊢ (i↑3) = -i |
|
Theorem | i4 10388 |
i to the fourth power. (Contributed by NM,
31-Jan-2007.)
|
⊢ (i↑4) = 1 |
|
Theorem | nnlesq 10389 |
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 10390 |
Taking i to the 𝐾-th power is the same as using the
𝐾 mod
4
-th power instead, by i4 10388. (Contributed by Mario Carneiro,
7-Jul-2014.)
|
⊢ (𝐾 ∈ ℤ → (i↑(𝐾 mod 4)) = (i↑𝐾)) |
|
Theorem | expnass 10391 |
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 10392 |
Factor the difference of two squares. (Contributed by NM,
21-Feb-2008.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵))) |
|
Theorem | subsq2 10393 |
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 10394 |
The square of a binomial. (Contributed by NM, 11-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) |
|
Theorem | subsqi 10395 |
Factor the difference of two squares. (Contributed by NM,
7-Feb-2005.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵)) |
|
Theorem | binom2 10396 |
The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
|
Theorem | binom21 10397 |
Special case of binom2 10396 where 𝐵 = 1. (Contributed by Scott Fenton,
11-May-2014.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1)↑2) = (((𝐴↑2) + (2 · 𝐴)) + 1)) |
|
Theorem | binom2sub 10398 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
10-Jun-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
|
Theorem | binom2sub1 10399 |
Special case of binom2sub 10398 where 𝐵 = 1. (Contributed by AV,
2-Aug-2021.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1)↑2) = (((𝐴↑2) − (2 · 𝐴)) + 1)) |
|
Theorem | binom2subi 10400 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
13-Jun-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2)) |