Theorem List for Intuitionistic Logic Explorer - 9501-9600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | expclzap 9501 |
Closure law for integer exponentiation. (Contributed by Jim Kingdon,
9-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ) |
|
Theorem | nn0expcli 9502 |
Closure of exponentiation of nonnegative integers. (Contributed by
Mario Carneiro, 17-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ (𝐴↑𝑁) ∈
ℕ0 |
|
Theorem | nn0sqcl 9503 |
The square of a nonnegative integer is a nonnegative integer.
(Contributed by Stefan O'Rear, 16-Oct-2014.)
|
⊢ (𝐴 ∈ ℕ0 → (𝐴↑2) ∈
ℕ0) |
|
Theorem | expm1t 9504 |
Exponentiation in terms of predecessor exponent. (Contributed by NM,
19-Dec-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = ((𝐴↑(𝑁 − 1)) · 𝐴)) |
|
Theorem | 1exp 9505 |
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 9506 |
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 9507 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." ([Geuvers], p. 1). (Contributed by Jim
Kingdon, 10-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) # 0 ↔ 𝐴 # 0)) |
|
Theorem | expeq0 9507 |
Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed
by NM, 23-Feb-2005.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0)) |
|
Theorem | expap0i 9508 |
Integer exponentiation is apart from zero if its mantissa is apart from
zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) # 0) |
|
Theorem | expgt0 9509 |
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 9510 |
Value of a complex number raised to a negative power. (Contributed by
Mario Carneiro, 4-Jun-2014.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |
|
Theorem | 0exp 9511 |
Value of zero raised to a positive integer power. (Contributed by NM,
19-Aug-2004.)
|
⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0) |
|
Theorem | expge0 9512 |
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 9513 |
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 9514 |
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 9515 |
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 9516 |
Integer exponentiation of a product. (Contributed by Jim Kingdon,
10-Jun-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝑁 ∈ ℤ) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) |
|
Theorem | exprecap 9517 |
Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim
Kingdon, 10-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → ((1 / 𝐴)↑𝑁) = (1 / (𝐴↑𝑁))) |
|
Theorem | expadd 9518 |
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 9519 |
Lemma for expaddzap 9520. (Contributed by Jim Kingdon, 10-Jun-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) |
|
Theorem | expaddzap 9520 |
Sum of exponents law for integer exponentiation. (Contributed by Jim
Kingdon, 10-Jun-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) |
|
Theorem | expmul 9521 |
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 9522 |
Product of exponents law for integer exponentiation. (Contributed by
Jim Kingdon, 11-Jun-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁)) |
|
Theorem | m1expeven 9523 |
Exponentiation of negative one to an even power. (Contributed by Scott
Fenton, 17-Jan-2018.)
|
⊢ (𝑁 ∈ ℤ → (-1↑(2 ·
𝑁)) = 1) |
|
Theorem | expsubap 9524 |
Exponent subtraction law for nonnegative integer exponentiation.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 − 𝑁)) = ((𝐴↑𝑀) / (𝐴↑𝑁))) |
|
Theorem | expp1zap 9525 |
Value of a nonzero complex number raised to an integer power plus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) |
|
Theorem | expm1ap 9526 |
Value of a complex number raised to an integer power minus one.
(Contributed by Jim Kingdon, 11-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑(𝑁 − 1)) = ((𝐴↑𝑁) / 𝐴)) |
|
Theorem | expdivap 9527 |
Nonnegative integer exponentiation of a quotient. (Contributed by Jim
Kingdon, 11-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝑁 ∈ ℕ0) → ((𝐴 / 𝐵)↑𝑁) = ((𝐴↑𝑁) / (𝐵↑𝑁))) |
|
Theorem | ltexp2a 9528 |
Ordering relationship for exponentiation. (Contributed by NM,
2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 < 𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑀) < (𝐴↑𝑁)) |
|
Theorem | leexp2a 9529 |
Weak ordering relationship for exponentiation. (Contributed by NM,
14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
|
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ≤ (𝐴↑𝑁)) |
|
Theorem | leexp2r 9530 |
Weak ordering relationship for exponentiation. (Contributed by Paul
Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘𝑀)) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)) |
|
Theorem | leexp1a 9531 |
Weak mantissa ordering relationship for exponentiation. (Contributed by
NM, 18-Dec-2005.)
|
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤
𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) |
|
Theorem | exple1 9532 |
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 9533 |
An upper bound on 𝐴↑𝑁 when 2 ≤ 𝐴. (Contributed by NM,
19-Dec-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤
𝐴) → (𝐴↑𝑁) ≤ ((2↑𝑁) · ((𝐴 − 1)↑𝑁))) |
|
Theorem | sqval 9534 |
Value of the square of a complex number. (Contributed by Raph Levien,
10-Apr-2004.)
|
⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴)) |
|
Theorem | sqneg 9535 |
The square of the negative of a number.) (Contributed by NM,
15-Jan-2006.)
|
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) |
|
Theorem | sqsubswap 9536 |
Swap the order of subtraction in a square. (Contributed by Scott Fenton,
10-Jun-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = ((𝐵 − 𝐴)↑2)) |
|
Theorem | sqcl 9537 |
Closure of square. (Contributed by NM, 10-Aug-1999.)
|
⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈ ℂ) |
|
Theorem | sqmul 9538 |
Distribution of square over multiplication. (Contributed by NM,
21-Mar-2008.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) |
|
Theorem | sqeq0 9539 |
A number is zero iff its square is zero. (Contributed by NM,
11-Mar-2006.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0)) |
|
Theorem | sqdivap 9540 |
Distribution of square over division. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) |
|
Theorem | sqne0 9541 |
A number is nonzero iff its square is nonzero. See also sqap0 9542 which is
the same but with not equal changed to apart. (Contributed by NM,
11-Mar-2006.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0)) |
|
Theorem | sqap0 9542 |
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 9543 |
Closure of the square of a real number. (Contributed by NM,
18-Oct-1999.)
|
⊢ (𝐴 ∈ ℝ → (𝐴↑2) ∈ ℝ) |
|
Theorem | sqgt0ap 9544 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
11-Jun-2020.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0) → 0 < (𝐴↑2)) |
|
Theorem | nnsqcl 9545 |
The naturals are closed under squaring. (Contributed by Scott Fenton,
29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℕ) |
|
Theorem | zsqcl 9546 |
Integers are closed under squaring. (Contributed by Scott Fenton,
18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ) |
|
Theorem | qsqcl 9547 |
The square of a rational is rational. (Contributed by Stefan O'Rear,
15-Sep-2014.)
|
⊢ (𝐴 ∈ ℚ → (𝐴↑2) ∈ ℚ) |
|
Theorem | sq11 9548 |
The square function is one-to-one for nonnegative reals. Also see
sq11ap 9639 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 9549 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 24-Feb-2006.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) |
|
Theorem | le2sq 9550 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 18-Oct-1999.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) |
|
Theorem | le2sq2 9551 |
The square of a 'less than or equal to' ordering. (Contributed by NM,
21-Mar-2008.)
|
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)) → (𝐴↑2) ≤ (𝐵↑2)) |
|
Theorem | sqge0 9552 |
A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
|
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴↑2)) |
|
Theorem | zsqcl2 9553 |
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 9554 |
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 9555 |
Value of square. Inference version. (Contributed by NM,
1-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴↑2) = (𝐴 · 𝐴) |
|
Theorem | sqcli 9556 |
Closure of square. (Contributed by NM, 2-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ (𝐴↑2) ∈ ℂ |
|
Theorem | sqeq0i 9557 |
A number is zero iff its square is zero. (Contributed by NM,
2-Oct-1999.)
|
⊢ 𝐴 ∈ ℂ
⇒ ⊢ ((𝐴↑2) = 0 ↔ 𝐴 = 0) |
|
Theorem | sqmuli 9558 |
Distribution of square over multiplication. (Contributed by NM,
3-Sep-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2)) |
|
Theorem | sqdivapi 9559 |
Distribution of square over division. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐵 # 0
⇒ ⊢ ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)) |
|
Theorem | resqcli 9560 |
Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐴↑2) ∈ ℝ |
|
Theorem | sqgt0api 9561 |
The square of a nonzero real is positive. (Contributed by Jim Kingdon,
12-Jun-2020.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ (𝐴 # 0 → 0 < (𝐴↑2)) |
|
Theorem | sqge0i 9562 |
A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
|
⊢ 𝐴 ∈ ℝ
⇒ ⊢ 0 ≤ (𝐴↑2) |
|
Theorem | lt2sqi 9563 |
The square function on nonnegative reals is strictly monotonic.
(Contributed by NM, 12-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) |
|
Theorem | le2sqi 9564 |
The square function on nonnegative reals is monotonic. (Contributed by
NM, 12-Sep-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) |
|
Theorem | sq11i 9565 |
The square function is one-to-one for nonnegative reals. (Contributed
by NM, 27-Oct-1999.)
|
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈
ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) |
|
Theorem | sq0 9566 |
The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
|
⊢ (0↑2) = 0 |
|
Theorem | sq0i 9567 |
If a number is zero, its square is zero. (Contributed by FL,
10-Dec-2006.)
|
⊢ (𝐴 = 0 → (𝐴↑2) = 0) |
|
Theorem | sq0id 9568 |
If a number is zero, its square is zero. Deduction form of sq0i 9567.
Converse of sqeq0d 9604. (Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 = 0) ⇒ ⊢ (𝜑 → (𝐴↑2) = 0) |
|
Theorem | sq1 9569 |
The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
|
⊢ (1↑2) = 1 |
|
Theorem | neg1sqe1 9570 |
-1 squared is 1 (common case). (Contributed by David
A. Wheeler,
8-Dec-2018.)
|
⊢ (-1↑2) = 1 |
|
Theorem | sq2 9571 |
The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
|
⊢ (2↑2) = 4 |
|
Theorem | sq3 9572 |
The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
|
⊢ (3↑2) = 9 |
|
Theorem | cu2 9573 |
The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
|
⊢ (2↑3) = 8 |
|
Theorem | irec 9574 |
The reciprocal of i. (Contributed by NM, 11-Oct-1999.)
|
⊢ (1 / i) = -i |
|
Theorem | i2 9575 |
i squared. (Contributed by NM, 6-May-1999.)
|
⊢ (i↑2) = -1 |
|
Theorem | i3 9576 |
i cubed. (Contributed by NM, 31-Jan-2007.)
|
⊢ (i↑3) = -i |
|
Theorem | i4 9577 |
i to the fourth power. (Contributed by NM,
31-Jan-2007.)
|
⊢ (i↑4) = 1 |
|
Theorem | nnlesq 9578 |
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 9579 |
Taking i to the 𝐾-th power is the same as using the
𝐾 mod
4
-th power instead, by i4 9577. (Contributed by Mario Carneiro,
7-Jul-2014.)
|
⊢ (𝐾 ∈ ℤ → (i↑(𝐾 mod 4)) = (i↑𝐾)) |
|
Theorem | expnass 9580 |
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 9581 |
Factor the difference of two squares. (Contributed by NM,
21-Feb-2008.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵))) |
|
Theorem | subsq2 9582 |
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 9583 |
The square of a binomial. (Contributed by NM, 11-Aug-1999.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) |
|
Theorem | subsqi 9584 |
Factor the difference of two squares. (Contributed by NM,
7-Feb-2005.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵)) |
|
Theorem | binom2 9585 |
The square of a binomial. (Contributed by FL, 10-Dec-2006.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
|
Theorem | binom21 9586 |
Special case of binom2 9585 where 𝐵 = 1. (Contributed by Scott Fenton,
11-May-2014.)
|
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1)↑2) = (((𝐴↑2) + (2 · 𝐴)) + 1)) |
|
Theorem | binom2sub 9587 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
10-Jun-2013.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) |
|
Theorem | binom2subi 9588 |
Expand the square of a subtraction. (Contributed by Scott Fenton,
13-Jun-2013.)
|
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈
ℂ ⇒ ⊢ ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2)) |
|
Theorem | mulbinom2 9589 |
The square of a binomial with factor. (Contributed by AV,
19-Jul-2021.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐶 · 𝐴) + 𝐵)↑2) = ((((𝐶 · 𝐴)↑2) + ((2 · 𝐶) · (𝐴 · 𝐵))) + (𝐵↑2))) |
|
Theorem | binom3 9590 |
The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
|
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) |
|
Theorem | zesq 9591 |
An integer is even iff its square is even. (Contributed by Mario
Carneiro, 12-Sep-2015.)
|
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ((𝑁↑2) / 2) ∈
ℤ)) |
|
Theorem | nnesq 9592 |
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 9593 |
Bernoulli's inequality, due to Johan Bernoulli (1667-1748).
(Contributed by NM, 21-Feb-2005.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤
𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁)) |
|
Theorem | bernneq2 9594 |
Variation of Bernoulli's inequality bernneq 9593. (Contributed by NM,
18-Oct-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤
𝐴) → (((𝐴 − 1) · 𝑁) + 1) ≤ (𝐴↑𝑁)) |
|
Theorem | bernneq3 9595 |
A corollary of bernneq 9593. (Contributed by Mario Carneiro,
11-Mar-2014.)
|
⊢ ((𝑃 ∈ (ℤ≥‘2)
∧ 𝑁 ∈
ℕ0) → 𝑁 < (𝑃↑𝑁)) |
|
Theorem | expnbnd 9596* |
Exponentiation with a mantissa greater than 1 has no upper bound.
(Contributed by NM, 20-Oct-2007.)
|
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) |
|
Theorem | expnlbnd 9597* |
The reciprocal of exponentiation with a mantissa greater than 1 has no
lower bound. (Contributed by NM, 18-Jul-2008.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ∃𝑘 ∈ ℕ (1 / (𝐵↑𝑘)) < 𝐴) |
|
Theorem | expnlbnd2 9598* |
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.)
|
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 <
𝐵) → ∃𝑗 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(1 / (𝐵↑𝑘)) < 𝐴) |
|
Theorem | exp0d 9599 |
Value of a complex number raised to the 0th power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴↑0) = 1) |
|
Theorem | exp1d 9600 |
Value of a complex number raised to the first power. (Contributed by
Mario Carneiro, 28-May-2016.)
|
⊢ (𝜑 → 𝐴 ∈ ℂ)
⇒ ⊢ (𝜑 → (𝐴↑1) = 𝐴) |