| Metamath
Proof Explorer Theorem List (p. 143 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mulexpd 14201 | Nonnegative integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) | ||
| Theorem | znsqcld 14202 | The square of a nonzero integer is a positive integer. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ≠ 0) ⇒ ⊢ (𝜑 → (𝑁↑2) ∈ ℕ) | ||
| Theorem | reexpcld 14203 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ) | ||
| Theorem | expge0d 14204 | A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴↑𝑁)) | ||
| Theorem | expge1d 14205 | A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → 1 ≤ (𝐴↑𝑁)) | ||
| Theorem | ltexp2a 14206 | Exponent ordering relationship for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 < 𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑀) < (𝐴↑𝑁)) | ||
| Theorem | expmordi 14207 | Base ordering relationship for exponentiation of nonnegative reals to a fixed positive integer power. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵) ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) < (𝐵↑𝑁)) | ||
| Theorem | rpexpmord 14208 | Base ordering relationship for exponentiation of positive reals to a fixed positive integer exponent. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑁) < (𝐵↑𝑁))) | ||
| Theorem | expcan 14209 | Cancellation law for integer exponentiation of reals. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 1 < 𝐴) → ((𝐴↑𝑀) = (𝐴↑𝑁) ↔ 𝑀 = 𝑁)) | ||
| Theorem | ltexp2 14210 | Strict ordering law for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 1 < 𝐴) → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁))) | ||
| Theorem | leexp2 14211 | Ordering law for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 1 < 𝐴) → (𝑀 ≤ 𝑁 ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑁))) | ||
| Theorem | leexp2a 14212 | Weak ordering relationship for exponentiation of a fixed real base greater than or equal to 1 to integer exponents. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ≤ (𝐴↑𝑁)) | ||
| Theorem | ltexp2r 14213 | The integer powers of a fixed positive real smaller than 1 decrease as the exponent increases. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐴 < 1) → (𝑀 < 𝑁 ↔ (𝐴↑𝑁) < (𝐴↑𝑀))) | ||
| Theorem | leexp2r 14214 | Weak ordering relationship for exponentiation of a fixed real base in [0, 1] to integer exponents. (Contributed by Paul Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)) | ||
| Theorem | leexp1a 14215 | Weak base ordering relationship for exponentiation of real bases to a fixed nonnegative integer exponent. (Contributed by NM, 18-Dec-2005.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) | ||
| Theorem | exple1 14216 | A real between 0 and 1 inclusive raised to a nonnegative integer power 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 14217 | An upper bound on 𝐴↑𝑁 when 2 ≤ 𝐴. (Contributed by NM, 19-Dec-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴) → (𝐴↑𝑁) ≤ ((2↑𝑁) · ((𝐴 − 1)↑𝑁))) | ||
| Theorem | sumsqeq0 14218 | The sum of two squres of reals is zero if and only if both reals are zero. (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 14219 | Value of square. Inference version. (Contributed by NM, 1-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴↑2) = (𝐴 · 𝐴) | ||
| Theorem | sqcli 14220 | Closure of square. (Contributed by NM, 2-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴↑2) ∈ ℂ | ||
| Theorem | sqeq0i 14221 | A complex number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.) |
| ⊢ 𝐴 ∈ ℂ ⇒ ⊢ ((𝐴↑2) = 0 ↔ 𝐴 = 0) | ||
| Theorem | sqrecii 14222 | The square of a reciprocal is the reciprocal of the square. (Contributed by NM, 17-Sep-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ ((1 / 𝐴)↑2) = (1 / (𝐴↑2)) | ||
| Theorem | sqmuli 14223 | Distribution of squaring over multiplication. (Contributed by NM, 3-Sep-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2)) | ||
| Theorem | sqdivi 14224 | Distribution of squaring over division. (Contributed by NM, 20-Aug-2001.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐵 ≠ 0 ⇒ ⊢ ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)) | ||
| Theorem | resqcli 14225 | Closure of square in reals. (Contributed by NM, 2-Aug-1999.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴↑2) ∈ ℝ | ||
| Theorem | sqgt0i 14226 | The square of a nonzero real is positive. (Contributed by NM, 17-Sep-1999.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 ≠ 0 → 0 < (𝐴↑2)) | ||
| Theorem | sqge0i 14227 | The square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.) |
| ⊢ 𝐴 ∈ ℝ ⇒ ⊢ 0 ≤ (𝐴↑2) | ||
| Theorem | lt2sqi 14228 | The square function on nonnegative reals is increasing. (Contributed by NM, 12-Sep-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) | ||
| Theorem | le2sqi 14229 | The square function on nonnegative reals is nondecreasing. (Contributed by NM, 12-Sep-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
| Theorem | sq11i 14230 | The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) | ||
| Theorem | sq0 14231 | The square of 0 is 0. (Contributed by NM, 6-Jun-2006.) |
| ⊢ (0↑2) = 0 | ||
| Theorem | sq0i 14232 | If a number is zero, then its square is zero. (Contributed by FL, 10-Dec-2006.) |
| ⊢ (𝐴 = 0 → (𝐴↑2) = 0) | ||
| Theorem | sq0id 14233 | If a number is zero, then its square is zero. Deduction form of sq0i 14232. Converse of sqeq0d 14185. (Contributed by David Moews, 28-Feb-2017.) |
| ⊢ (𝜑 → 𝐴 = 0) ⇒ ⊢ (𝜑 → (𝐴↑2) = 0) | ||
| Theorem | sq1 14234 | The square of 1 is 1. (Contributed by NM, 22-Aug-1999.) |
| ⊢ (1↑2) = 1 | ||
| Theorem | neg1sqe1 14235 | The square of -1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
| ⊢ (-1↑2) = 1 | ||
| Theorem | sq2 14236 | The square of 2 is 4. (Contributed by NM, 22-Aug-1999.) |
| ⊢ (2↑2) = 4 | ||
| Theorem | sq3 14237 | The square of 3 is 9. (Contributed by NM, 26-Apr-2006.) |
| ⊢ (3↑2) = 9 | ||
| Theorem | sq4e2t8 14238 | The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.) |
| ⊢ (4↑2) = (2 · 8) | ||
| Theorem | cu2 14239 | The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.) |
| ⊢ (2↑3) = 8 | ||
| Theorem | irec 14240 | The reciprocal of i. (Contributed by NM, 11-Oct-1999.) |
| ⊢ (1 / i) = -i | ||
| Theorem | i2 14241 | i squared. (Contributed by NM, 6-May-1999.) |
| ⊢ (i↑2) = -1 | ||
| Theorem | i3 14242 | i cubed. (Contributed by NM, 31-Jan-2007.) |
| ⊢ (i↑3) = -i | ||
| Theorem | i4 14243 | i to the fourth power. (Contributed by NM, 31-Jan-2007.) |
| ⊢ (i↑4) = 1 | ||
| Theorem | nnlesq 14244 | A positive integer is less than or equal to its square. For general integers, see zzlesq 14245. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.) |
| ⊢ (𝑁 ∈ ℕ → 𝑁 ≤ (𝑁↑2)) | ||
| Theorem | zzlesq 14245 | An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.) |
| ⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (𝑁↑2)) | ||
| Theorem | iexpcyc 14246 | Taking i to the 𝐾-th power is the same as using the 𝐾 mod 4 -th power instead, by i4 14243. (Contributed by Mario Carneiro, 7-Jul-2014.) |
| ⊢ (𝐾 ∈ ℤ → (i↑(𝐾 mod 4)) = (i↑𝐾)) | ||
| Theorem | expnass 14247 | 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 | sqlecan 14248 | Cancel one factor of a square in a ≤ comparison. Unlike lemul1 12119, the common factor 𝐴 may be zero. (Contributed by NM, 17-Jan-2008.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)) | ||
| Theorem | subsq 14249 | Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵))) | ||
| Theorem | subsq2 14250 | 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 14251 | The square of a binomial. (Contributed by NM, 11-Aug-1999.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) | ||
| Theorem | subsqi 14252 | Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵)) | ||
| Theorem | sqeqori 14253 | The squares of two complex numbers are equal iff one number equals the other or its negative. Lemma 15-4.7 of [Gleason] p. 311 and its converse. (Contributed by NM, 15-Jan-2006.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)) | ||
| Theorem | subsq0i 14254 | The two solutions to the difference of squares set equal to zero. (Contributed by NM, 25-Apr-2006.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (((𝐴↑2) − (𝐵↑2)) = 0 ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)) | ||
| Theorem | sqeqor 14255 | The squares of two complex numbers are equal iff one number equals the other or its negative. Lemma 15-4.7 of [Gleason] p. 311 and its converse. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵))) | ||
| Theorem | binom2 14256 | The square of a binomial. (Contributed by FL, 10-Dec-2006.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
| Theorem | binom2d 14257 | Deduction form of binom2 14256. (Contributed by Igor Ieskov, 14-Dec-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
| Theorem | binom21 14258 | Special case of binom2 14256 where 𝐵 = 1. (Contributed by Scott Fenton, 11-May-2014.) |
| ⊢ (𝐴 ∈ ℂ → ((𝐴 + 1)↑2) = (((𝐴↑2) + (2 · 𝐴)) + 1)) | ||
| Theorem | binom2sub 14259 | Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
| Theorem | binom2sub1 14260 | Special case of binom2sub 14259 where 𝐵 = 1. (Contributed by AV, 2-Aug-2021.) |
| ⊢ (𝐴 ∈ ℂ → ((𝐴 − 1)↑2) = (((𝐴↑2) − (2 · 𝐴)) + 1)) | ||
| Theorem | binom2subi 14261 | Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2)) | ||
| Theorem | mulbinom2 14262 | The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐶 · 𝐴) + 𝐵)↑2) = ((((𝐶 · 𝐴)↑2) + ((2 · 𝐶) · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
| Theorem | binom3 14263 | The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) | ||
| Theorem | sq01 14264 | If a complex number equals its square, it must be 0 or 1. (Contributed by NM, 6-Jun-2006.) |
| ⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 𝐴 ↔ (𝐴 = 0 ∨ 𝐴 = 1))) | ||
| Theorem | zesq 14265 | An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.) |
| ⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ((𝑁↑2) / 2) ∈ ℤ)) | ||
| Theorem | nnesq 14266 | 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 | crreczi 14267 | Reciprocal of a complex number in terms of real and imaginary components. Remark in [Apostol] p. 361. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Jeff Hankins, 16-Dec-2013.) |
| ⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((𝐴 ≠ 0 ∨ 𝐵 ≠ 0) → (1 / (𝐴 + (i · 𝐵))) = ((𝐴 − (i · 𝐵)) / ((𝐴↑2) + (𝐵↑2)))) | ||
| Theorem | bernneq 14268 | Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁)) | ||
| Theorem | bernneq2 14269 | Variation of Bernoulli's inequality bernneq 14268. (Contributed by NM, 18-Oct-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴) → (((𝐴 − 1) · 𝑁) + 1) ≤ (𝐴↑𝑁)) | ||
| Theorem | bernneq3 14270 | A corollary of bernneq 14268. (Contributed by Mario Carneiro, 11-Mar-2014.) |
| ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 < (𝑃↑𝑁)) | ||
| Theorem | expnbnd 14271* | Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) | ||
| Theorem | expnlbnd 14272* | The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ (1 / (𝐵↑𝑘)) < 𝐴) | ||
| Theorem | expnlbnd2 14273* | The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(1 / (𝐵↑𝑘)) < 𝐴) | ||
| Theorem | expmulnbnd 14274* | Exponentiation with a base greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘)) | ||
| Theorem | digit2 14275 | Two ways to express the 𝐾 th digit in the decimal (when base 𝐵 = 10) expansion of a number 𝐴. 𝐾 = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 25-Dec-2008.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = ((⌊‘((𝐵↑𝐾) · 𝐴)) − (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))))) | ||
| Theorem | digit1 14276 | Two ways to express the 𝐾 th digit in the decimal expansion of a number 𝐴 (when base 𝐵 = 10). 𝐾 = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 3-Jan-2009.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = (((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) − ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)))) | ||
| Theorem | modexp 14277 | Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) |
| ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ+) ∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴↑𝐶) mod 𝐷) = ((𝐵↑𝐶) mod 𝐷)) | ||
| Theorem | discr1 14278* | A nonnegative quadratic form has nonnegative leading coefficient. (Contributed by Mario Carneiro, 4-Jun-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) & ⊢ 𝑋 = if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) | ||
| Theorem | discr 14279* | If a quadratic polynomial with real coefficients is nonnegative for all values, then its discriminant is nonpositive. (Contributed by NM, 10-Aug-1999.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) ⇒ ⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ≤ 0) | ||
| Theorem | expnngt1 14280 | If an integer power with a positive integer base is greater than 1, then the exponent is positive. (Contributed by AV, 28-Dec-2022.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 1 < (𝐴↑𝐵)) → 𝐵 ∈ ℕ) | ||
| Theorem | expnngt1b 14281 | An integer power with an integer base greater than 1 is greater than 1 iff the exponent is positive. (Contributed by AV, 28-Dec-2022.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (1 < (𝐴↑𝐵) ↔ 𝐵 ∈ ℕ)) | ||
| Theorem | sqoddm1div8 14282 | A squared odd number minus 1 divided by 8 is the odd number multiplied with its successor divided by 2. (Contributed by AV, 19-Jul-2021.) |
| ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = ((2 · 𝑁) + 1)) → (((𝑀↑2) − 1) / 8) = ((𝑁 · (𝑁 + 1)) / 2)) | ||
| Theorem | nnsqcld 14283 | The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴↑2) ∈ ℕ) | ||
| Theorem | nnexpcld 14284 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ) | ||
| Theorem | nn0expcld 14285 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ0) | ||
| Theorem | rpexpcld 14286 | Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ+) | ||
| Theorem | ltexp2rd 14287 | The power of a positive number smaller than 1 decreases as its exponent increases. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 < 1) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝐴↑𝑁) < (𝐴↑𝑀))) | ||
| Theorem | reexpclzd 14288 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ) | ||
| Theorem | sqgt0d 14289 | The square of a nonzero real is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → 0 < (𝐴↑2)) | ||
| Theorem | ltexp2d 14290 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁))) | ||
| Theorem | leexp2d 14291 | Ordering law for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (𝑀 ≤ 𝑁 ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑁))) | ||
| Theorem | expcand 14292 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → (𝐴↑𝑀) = (𝐴↑𝑁)) ⇒ ⊢ (𝜑 → 𝑀 = 𝑁) | ||
| Theorem | leexp2ad 14293 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → (𝐴↑𝑀) ≤ (𝐴↑𝑁)) | ||
| Theorem | leexp2rd 14294 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 1) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐴↑𝑀)) | ||
| Theorem | lt2sqd 14295 | The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) | ||
| Theorem | le2sqd 14296 | The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
| Theorem | sq11d 14297 | The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → (𝐴↑2) = (𝐵↑2)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | ltexp1d 14298 | Elevating to a positive power does not affect inequalities. Similar to ltmul1d 13118 for exponentiation of positive reals. (Contributed by Steven Nguyen, 22-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑𝑁) < (𝐵↑𝑁))) | ||
| Theorem | ltexp1dd 14299 | Raising both sides of 'less than' to the same positive integer preserves ordering. (Contributed by Steven Nguyen, 24-Aug-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) < (𝐵↑𝑁)) | ||
| Theorem | exp11nnd 14300 | The function elevating nonnegative reals to a positive integer is one-to-one. Similar to sq11d 14297 for positive real bases and positive integer exponents. The base cannot be generalized much further, since if 𝑁 is even then we have 𝐴↑𝑁 = -𝐴↑𝑁. (Contributed by SN, 14-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |