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