HomeTheorem List (p. 142 of 505)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 142 of 505) | < 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-31175) |
Hilbert Space Explorer
(31176-32698) |
Users' Mathboxes
(32699-50435) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | qexpcl 14101 | Closure of exponentiation of rationals. For integer exponents, see qexpclz 14105. (Contributed by NM, 16-Dec-2005.) |
| ⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℚ) | ||
| Theorem | reexpcl 14102 | Closure of exponentiation of reals. For integer exponents, see reexpclz 14106. (Contributed by NM, 14-Dec-2005.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ) | ||
| Theorem | expcl 14103 | Closure law for nonnegative integer exponentiation. For integer exponents, see expclz 14108. (Contributed by NM, 26-May-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ) | ||
| Theorem | rpexpcl 14104 | Closure law for integer exponentiation of positive reals. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ+) | ||
| Theorem | qexpclz 14105 | Closure of integer exponentiation of rational numbers. (Contributed by Mario Carneiro, 9-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℚ) | ||
| Theorem | reexpclz 14106 | Closure of integer exponentiation of reals. (Contributed by Mario Carneiro, 4-Jun-2014.) (Revised by Mario Carneiro, 9-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ) | ||
| Theorem | expclzlem 14107 | Lemma for expclz 14108. (Contributed by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ (ℂ ∖ {0})) | ||
| Theorem | expclz 14108 | Closure law for integer exponentiation of complex numnbers. (Contributed by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ) | ||
| Theorem | m1expcl2 14109 | Closure of integer exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ {-1, 1}) | ||
| Theorem | m1expcl 14110 | Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ ℤ) | ||
| Theorem | zexpcld 14111 | Closure of exponentiation of integers, deduction form. (Contributed by SN, 15-Sep-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℤ) | ||
| Theorem | nn0expcli 14112 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝐴↑𝑁) ∈ ℕ0 | ||
| Theorem | nn0sqcl 14113 | The square of a nonnegative integer is a nonnegative integer. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
| ⊢ (𝐴 ∈ ℕ0 → (𝐴↑2) ∈ ℕ0) | ||
| Theorem | expm1t 14114 | Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = ((𝐴↑(𝑁 − 1)) · 𝐴)) | ||
| Theorem | 1exp 14115 | Value of 1 raised to an integer power. (Contributed by NM, 15-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ (𝑁 ∈ ℤ → (1↑𝑁) = 1) | ||
| Theorem | expeq0 14116 | A positive integer power is zero if and only if its base is zero. (Contributed by NM, 23-Feb-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0)) | ||
| Theorem | expne0 14117 | A positive integer power is nonzero if and only if its base is nonzero. (Contributed by NM, 6-May-2005.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) ≠ 0 ↔ 𝐴 ≠ 0)) | ||
| Theorem | expne0i 14118 | An integer power is nonzero if its base is nonzero. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ≠ 0) | ||
| Theorem | expgt0 14119 | A positive real raised to an integer power is positive. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < 𝐴) → 0 < (𝐴↑𝑁)) | ||
| Theorem | expnegz 14120 | Value of a nonzero complex number raised to the negative of an integer power. (Contributed by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | ||
| Theorem | 0exp 14121 | Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.) |
| ⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0) | ||
| Theorem | expge0 14122 | A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴) → 0 ≤ (𝐴↑𝑁)) | ||
| Theorem | expge1 14123 | A real greater than or equal to 1 raised to a nonnegative integer 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 14124 | A real greater than 1 raised to a positive integer is greater than 1. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ ∧ 1 < 𝐴) → 1 < (𝐴↑𝑁)) | ||
| Theorem | mulexp 14125 | Nonnegative 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 | mulexpz 14126 | Integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 4-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑁 ∈ ℤ) → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁))) | ||
| Theorem | exprec 14127 | Integer exponentiation of a reciprocal. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → ((1 / 𝐴)↑𝑁) = (1 / (𝐴↑𝑁))) | ||
| Theorem | expadd 14128 | 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 | expaddzlem 14129 | Lemma for expaddz 14130. (Contributed by Mario Carneiro, 4-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) | ||
| Theorem | expaddz 14130 | Sum of exponents law for integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 4-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) | ||
| Theorem | expmul 14131 | Product of exponents law for nonnegative 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 | expmulz 14132 | Product of exponents law for integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 7-Jul-2014.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁)) | ||
| Theorem | m1expeven 14133 | Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018.) |
| ⊢ (𝑁 ∈ ℤ → (-1↑(2 · 𝑁)) = 1) | ||
| Theorem | expsub 14134 | Exponent subtraction law for integer exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 − 𝑁)) = ((𝐴↑𝑀) / (𝐴↑𝑁))) | ||
| Theorem | expp1z 14135 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) | ||
| Theorem | expm1 14136 | Value of a nonzero complex number raised to an integer power minus one. (Contributed by NM, 25-Dec-2008.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑(𝑁 − 1)) = ((𝐴↑𝑁) / 𝐴)) | ||
| Theorem | expdiv 14137 | Nonnegative integer exponentiation of a quotient. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑁 ∈ ℕ0) → ((𝐴 / 𝐵)↑𝑁) = ((𝐴↑𝑁) / (𝐵↑𝑁))) | ||
| Theorem | sqval 14138 | Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴)) | ||
| Theorem | sqneg 14139 | The square of the negative of a number. (Contributed by NM, 15-Jan-2006.) |
| ⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) | ||
| Theorem | sqnegd 14140 | The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (-𝐴↑2) = (𝐴↑2)) | ||
| Theorem | sqsubswap 14141 | Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = ((𝐵 − 𝐴)↑2)) | ||
| Theorem | sqcl 14142 | Closure of square. (Contributed by NM, 10-Aug-1999.) |
| ⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈ ℂ) | ||
| Theorem | sqmul 14143 | Distribution of squaring over multiplication. (Contributed by NM, 21-Mar-2008.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) | ||
| Theorem | sqeq0 14144 | A complex number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006.) |
| ⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0)) | ||
| Theorem | sqdiv 14145 | Distribution of squaring over division. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof shortened by Mario Carneiro, 9-Jul-2013.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) | ||
| Theorem | sqdivid 14146 | The square of a nonzero complex number divided by itself equals that number. (Contributed by AV, 19-Jul-2021.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴↑2) / 𝐴) = 𝐴) | ||
| Theorem | sqne0 14147 | A complex number is nonzero if and only if its square is nonzero. (Contributed by NM, 11-Mar-2006.) |
| ⊢ (𝐴 ∈ ℂ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0)) | ||
| Theorem | resqcl 14148 | Closure of squaring in reals. (Contributed by NM, 18-Oct-1999.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴↑2) ∈ ℝ) | ||
| Theorem | resqcld 14149 | Closure of squaring in reals, deduction form. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴↑2) ∈ ℝ) | ||
| Theorem | sqgt0 14150 | The square of a nonzero real is positive. (Contributed by NM, 8-Sep-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 0 < (𝐴↑2)) | ||
| Theorem | sqn0rp 14151 | The square of a nonzero real is a positive real. (Contributed by AV, 5-Mar-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ∈ ℝ+) | ||
| Theorem | nnsqcl 14152 | The positive naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℕ) | ||
| Theorem | zsqcl 14153 | Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
| ⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ) | ||
| Theorem | qsqcl 14154 | The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
| ⊢ (𝐴 ∈ ℚ → (𝐴↑2) ∈ ℚ) | ||
| Theorem | sq11 14155 | The square function is one-to-one for nonnegative reals. (Contributed by NM, 8-Apr-2001.) (Proof shortened by Mario Carneiro, 28-May-2016.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) | ||
| Theorem | nn0sq11 14156 | The square function is one-to-one for nonnegative integers. (Contributed by AV, 25-Jun-2023.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) | ||
| Theorem | lt2sq 14157 | The square function is increasing on nonnegative reals. (Contributed by NM, 24-Feb-2006.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) | ||
| Theorem | le2sq 14158 | The square function is nondecreasing on nonnegative reals. (Contributed by NM, 18-Oct-1999.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
| Theorem | le2sq2 14159 | The square function is nondecreasing on the nonnegative reals. (Contributed by NM, 21-Mar-2008.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)) → (𝐴↑2) ≤ (𝐵↑2)) | ||
| Theorem | sqge0 14160 | The square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.) |
| ⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴↑2)) | ||
| Theorem | sqge0d 14161 | The square of a real is nonnegative, deduction form. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴↑2)) | ||
| Theorem | zsqcl2 14162 | 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 | 0expd 14163 | Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (0↑𝑁) = 0) | ||
| Theorem | exp0d 14164 | Value of a complex number raised to the zeroth power. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑0) = 1) | ||
| Theorem | exp1d 14165 | Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑1) = 𝐴) | ||
| Theorem | expeq0d 14166 | If a positive integer power is zero, then its base is zero. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐴↑𝑁) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
| Theorem | sqvald 14167 | Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) | ||
| Theorem | sqcld 14168 | Closure of square. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑2) ∈ ℂ) | ||
| Theorem | sqeq0d 14169 | A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝐴↑2) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
| Theorem | expcld 14170 | Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ) | ||
| Theorem | expp1d 14171 | Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) | ||
| Theorem | expaddd 14172 | Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) | ||
| Theorem | expmuld 14173 | 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 14174 | Square of reciprocal is reciprocal of square. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → ((1 / 𝐴)↑2) = (1 / (𝐴↑2))) | ||
| Theorem | expclzd 14175 | Closure law for integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ) | ||
| Theorem | expne0d 14176 | A nonnegative integer power is nonzero if its base is nonzero. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≠ 0) | ||
| Theorem | expnegd 14177 | Value of a nonzero complex number raised to the negative of an integer power. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | ||
| Theorem | exprecd 14178 | An integer power of a reciprocal is the reciprocal of the integer power with same exponent. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → ((1 / 𝐴)↑𝑁) = (1 / (𝐴↑𝑁))) | ||
| Theorem | expp1zd 14179 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) | ||
| Theorem | expm1d 14180 | Value of a nonzero complex number raised to an integer power minus one. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑(𝑁 − 1)) = ((𝐴↑𝑁) / 𝐴)) | ||
| Theorem | expsubd 14181 | Exponent subtraction law for integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑(𝑀 − 𝑁)) = ((𝐴↑𝑀) / (𝐴↑𝑁))) | ||
| Theorem | sqmuld 14182 | Distribution of squaring over multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) | ||
| Theorem | sqdivd 14183 | Distribution of squaring over division. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) | ||
| Theorem | expdivd 14184 | Nonnegative integer exponentiation of a quotient. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐴 / 𝐵)↑𝑁) = ((𝐴↑𝑁) / (𝐵↑𝑁))) | ||
| Theorem | mulexpd 14185 | 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 14186 | The square of a nonzero integer is a positive integer. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ≠ 0) ⇒ ⊢ (𝜑 → (𝑁↑2) ∈ ℕ) | ||
| Theorem | reexpcld 14187 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ) | ||
| Theorem | expge0d 14188 | A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → 0 ≤ (𝐴↑𝑁)) | ||
| Theorem | expge1d 14189 | 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 14190 | 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 14191 | 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 14192 | Base ordering relationship for exponentiation of positive reals to a fixed positive integer exponent. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑁) < (𝐵↑𝑁))) | ||
| Theorem | expcan 14193 | Cancellation law for integer exponentiation of reals. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 1 < 𝐴) → ((𝐴↑𝑀) = (𝐴↑𝑁) ↔ 𝑀 = 𝑁)) | ||
| Theorem | ltexp2 14194 | 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 14195 | 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 14196 | 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 14197 | The integer powers of a fixed positive real less than 1 decrease as the exponent increases. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) |
| ⊢ (((𝐴 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐴 < 1) → (𝑀 < 𝑁 ↔ (𝐴↑𝑁) < (𝐴↑𝑀))) | ||
| Theorem | leexp2r 14198 | 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 14199 | Weak base ordering relationship for exponentiation of real bases to a fixed nonnegative integer exponent. (Contributed by NM, 18-Dec-2005.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0) ∧ (0 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵)) → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) | ||
| Theorem | leexp1ad 14200 | Weak base ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐵↑𝑁)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |