Home | Metamath
Proof Explorer Theorem List (p. 136 of 449) | < 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: | Metamath Proof Explorer
(1-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | expmuld 13501 | Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁)) | ||
Theorem | sqrecd 13502 | Square of reciprocal. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → ((1 / 𝐴)↑2) = (1 / (𝐴↑2))) | ||
Theorem | expclzd 13503 | Closure law for integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ) | ||
Theorem | expne0d 13504 | Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≠ 0) | ||
Theorem | expnegd 13505 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | ||
Theorem | exprecd 13506 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → ((1 / 𝐴)↑𝑁) = (1 / (𝐴↑𝑁))) | ||
Theorem | expp1zd 13507 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) | ||
Theorem | expm1d 13508 | Value of a complex number raised to an integer power minus one. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑(𝑁 − 1)) = ((𝐴↑𝑁) / 𝐴)) | ||
Theorem | expsubd 13509 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑(𝑀 − 𝑁)) = ((𝐴↑𝑀) / (𝐴↑𝑁))) | ||
Theorem | sqmuld 13510 | Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) | ||
Theorem | sqdivd 13511 | Distribution of square over division. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) | ||
Theorem | expdivd 13512 | Nonnegative integer exponentiation of a quotient. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵)↑𝑁) = ((𝐴↑𝑁) / (𝐵↑𝑁))) | ||
Theorem | mulexpd 13513 | Positive 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 13514 | The square of a nonzero integer is a positive integer. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ≠ 0) ⇒ ⊢ (𝜑 → (𝑁↑2) ∈ ℕ) | ||
Theorem | reexpcld 13515 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | expge0d 13516 | Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴↑𝑁)) | ||
Theorem | expge1d 13517 | Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ (𝜑 → 1 ≤ (𝐴↑𝑁)) | ||
Theorem | ltexp2a 13518 | Ordering relationship for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (1 < 𝐴 ∧ 𝑀 < 𝑁)) → (𝐴↑𝑀) < (𝐴↑𝑁)) | ||
Theorem | expmordi 13519 | Mantissa ordering relationship for exponentiation. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵) ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) < (𝐵↑𝑁)) | ||
Theorem | rpexpmord 13520 | Mantissa ordering relationship for exponentiation of positive reals. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑁) < (𝐵↑𝑁))) | ||
Theorem | expcan 13521 | Cancellation law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 1 < 𝐴) → ((𝐴↑𝑀) = (𝐴↑𝑁) ↔ 𝑀 = 𝑁)) | ||
Theorem | ltexp2 13522 | Ordering law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 1 < 𝐴) → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁))) | ||
Theorem | leexp2 13523 | Ordering law for exponentiation. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 1 < 𝐴) → (𝑀 ≤ 𝑁 ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑁))) | ||
Theorem | leexp2a 13524 | Weak ordering relationship for exponentiation. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ≤ (𝐴↑𝑁)) | ||
Theorem | ltexp2r 13525 | The power of a positive number smaller than 1 decreases as its exponent increases. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐴 < 1) → (𝑀 < 𝑁 ↔ (𝐴↑𝑁) < (𝐴↑𝑀))) | ||
Theorem | leexp2r 13526 | Weak ordering relationship for exponentiation. (Contributed by Paul Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 1)) → (𝐴↑𝑁) ≤ (𝐴↑𝑀)) | ||
Theorem | leexp1a 13527 | Weak mantissa ordering relationship for exponentiation. (Contributed by NM, 18-Dec-2005.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) | ||
Theorem | exple1 13528 | 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 13529 | An upper bound on 𝐴↑𝑁 when 2 ≤ 𝐴. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝐴) → (𝐴↑𝑁) ≤ ((2↑𝑁) · ((𝐴 − 1)↑𝑁))) | ||
Theorem | sumsqeq0 13530 | 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 13531 | Value of square. Inference version. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴↑2) = (𝐴 · 𝐴) | ||
Theorem | sqcli 13532 | Closure of square. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴↑2) ∈ ℂ | ||
Theorem | sqeq0i 13533 | A number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ ((𝐴↑2) = 0 ↔ 𝐴 = 0) | ||
Theorem | sqrecii 13534 | Square of reciprocal. (Contributed by NM, 17-Sep-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐴 ≠ 0 ⇒ ⊢ ((1 / 𝐴)↑2) = (1 / (𝐴↑2)) | ||
Theorem | sqmuli 13535 | Distribution of square over multiplication. (Contributed by NM, 3-Sep-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2)) | ||
Theorem | sqdivi 13536 | Distribution of square over division. (Contributed by NM, 20-Aug-2001.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐵 ≠ 0 ⇒ ⊢ ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)) | ||
Theorem | resqcli 13537 | Closure of square in reals. (Contributed by NM, 2-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴↑2) ∈ ℝ | ||
Theorem | sqgt0i 13538 | The square of a nonzero real is positive. (Contributed by NM, 17-Sep-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 ≠ 0 → 0 < (𝐴↑2)) | ||
Theorem | sqge0i 13539 | A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ 0 ≤ (𝐴↑2) | ||
Theorem | lt2sqi 13540 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 12-Sep-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) | ||
Theorem | le2sqi 13541 | The square function on nonnegative reals is monotonic. (Contributed by NM, 12-Sep-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
Theorem | sq11i 13542 | The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ ⇒ ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) | ||
Theorem | sq0 13543 | The square of 0 is 0. (Contributed by NM, 6-Jun-2006.) |
⊢ (0↑2) = 0 | ||
Theorem | sq0i 13544 | If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.) |
⊢ (𝐴 = 0 → (𝐴↑2) = 0) | ||
Theorem | sq0id 13545 | If a number is zero, its square is zero. Deduction form of sq0i 13544. Converse of sqeq0d 13497. (Contributed by David Moews, 28-Feb-2017.) |
⊢ (𝜑 → 𝐴 = 0) ⇒ ⊢ (𝜑 → (𝐴↑2) = 0) | ||
Theorem | sq1 13546 | The square of 1 is 1. (Contributed by NM, 22-Aug-1999.) |
⊢ (1↑2) = 1 | ||
Theorem | neg1sqe1 13547 | -1 squared is 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (-1↑2) = 1 | ||
Theorem | sq2 13548 | The square of 2 is 4. (Contributed by NM, 22-Aug-1999.) |
⊢ (2↑2) = 4 | ||
Theorem | sq3 13549 | The square of 3 is 9. (Contributed by NM, 26-Apr-2006.) |
⊢ (3↑2) = 9 | ||
Theorem | sq4e2t8 13550 | The square of 4 is 2 times 8. (Contributed by AV, 20-Jul-2021.) |
⊢ (4↑2) = (2 · 8) | ||
Theorem | cu2 13551 | The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.) |
⊢ (2↑3) = 8 | ||
Theorem | irec 13552 | The reciprocal of i. (Contributed by NM, 11-Oct-1999.) |
⊢ (1 / i) = -i | ||
Theorem | i2 13553 | i squared. (Contributed by NM, 6-May-1999.) |
⊢ (i↑2) = -1 | ||
Theorem | i3 13554 | i cubed. (Contributed by NM, 31-Jan-2007.) |
⊢ (i↑3) = -i | ||
Theorem | i4 13555 | i to the fourth power. (Contributed by NM, 31-Jan-2007.) |
⊢ (i↑4) = 1 | ||
Theorem | nnlesq 13556 | 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 13557 | Taking i to the 𝐾-th power is the same as using the 𝐾 mod 4 -th power instead, by i4 13555. (Contributed by Mario Carneiro, 7-Jul-2014.) |
⊢ (𝐾 ∈ ℤ → (i↑(𝐾 mod 4)) = (i↑𝐾)) | ||
Theorem | expnass 13558 | 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 13559 | Cancel one factor of a square in a ≤ comparison. Unlike lemul1 11480, the common factor 𝐴 may be zero. (Contributed by NM, 17-Jan-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) ≤ (𝐵 · 𝐴) ↔ 𝐴 ≤ 𝐵)) | ||
Theorem | subsq 13560 | Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵))) | ||
Theorem | subsq2 13561 | 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 13562 | The square of a binomial. (Contributed by NM, 11-Aug-1999.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)) | ||
Theorem | subsqi 13563 | Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵)) | ||
Theorem | sqeqori 13564 | 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 13565 | The two solutions to the difference of squares set equal to zero. (Contributed by NM, 25-Apr-2006.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ (((𝐴↑2) − (𝐵↑2)) = 0 ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)) | ||
Theorem | sqeqor 13566 | 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 13567 | The square of a binomial. (Contributed by FL, 10-Dec-2006.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
Theorem | binom21 13568 | Special case of binom2 13567 where 𝐵 = 1. (Contributed by Scott Fenton, 11-May-2014.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1)↑2) = (((𝐴↑2) + (2 · 𝐴)) + 1)) | ||
Theorem | binom2sub 13569 | Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
Theorem | binom2sub1 13570 | Special case of binom2sub 13569 where 𝐵 = 1. (Contributed by AV, 2-Aug-2021.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1)↑2) = (((𝐴↑2) − (2 · 𝐴)) + 1)) | ||
Theorem | binom2subi 13571 | Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.) |
⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2)) | ||
Theorem | mulbinom2 13572 | The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐶 · 𝐴) + 𝐵)↑2) = ((((𝐶 · 𝐴)↑2) + ((2 · 𝐶) · (𝐴 · 𝐵))) + (𝐵↑2))) | ||
Theorem | binom3 13573 | The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3)))) | ||
Theorem | sq01 13574 | If a complex number equals its square, it must be 0 or 1. (Contributed by NM, 6-Jun-2006.) |
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 𝐴 ↔ (𝐴 = 0 ∨ 𝐴 = 1))) | ||
Theorem | zesq 13575 | An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.) |
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ((𝑁↑2) / 2) ∈ ℤ)) | ||
Theorem | nnesq 13576 | 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 13577 | 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 13578 | Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁)) | ||
Theorem | bernneq2 13579 | Variation of Bernoulli's inequality bernneq 13578. (Contributed by NM, 18-Oct-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴) → (((𝐴 − 1) · 𝑁) + 1) ≤ (𝐴↑𝑁)) | ||
Theorem | bernneq3 13580 | A corollary of bernneq 13578. (Contributed by Mario Carneiro, 11-Mar-2014.) |
⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 < (𝑃↑𝑁)) | ||
Theorem | expnbnd 13581* | Exponentiation with a mantissa greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) | ||
Theorem | expnlbnd 13582* | The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ (1 / (𝐵↑𝑘)) < 𝐴) | ||
Theorem | expnlbnd2 13583* | 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 | expmulnbnd 13584* | Exponentiation with a mantissa greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘)) | ||
Theorem | digit2 13585 | 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 13586 | 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 13587 | 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 13588* | 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 13589* | 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 13590 | 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 13591 | 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 13592 | 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 13593 | The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴↑2) ∈ ℕ) | ||
Theorem | nnexpcld 13594 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ) | ||
Theorem | nn0expcld 13595 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ0) | ||
Theorem | rpexpcld 13596 | Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ+) | ||
Theorem | ltexp2rd 13597 | The power of a positive number smaller than 1 decreases as its exponent increases. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 < 1) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝐴↑𝑁) < (𝐴↑𝑀))) | ||
Theorem | reexpclzd 13598 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | resqcld 13599 | Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴↑2) ∈ ℝ) | ||
Theorem | sqge0d 13600 | A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴↑2)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |