Home | Metamath
Proof Explorer Theorem List (p. 135 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | seqf1o 13401* | Rearrange a sum via an arbitrary bijection on (𝑀...𝑁). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘𝑥) ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = (𝐺‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁)) | ||
Theorem | seradd 13402* | The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 26-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | sersub 13403* | The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) − (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqid3 13404* | A sequence that consists entirely of "zeroes" sums to "zero". More precisely, a constant sequence with value an element which is a + -idempotent sums (or "+'s") to that element. (Contributed by Mario Carneiro, 15-Dec-2014.) |
⊢ (𝜑 → (𝑍 + 𝑍) = 𝑍) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = 𝑍) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍) | ||
Theorem | seqid 13405* | Discarding the first few terms of a sequence that starts with all zeroes (or any element which is a left-identity for +) has no effect on its sum. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑍 + 𝑥) = 𝑥) & ⊢ (𝜑 → 𝑍 ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝐹‘𝑁) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑥) = 𝑍) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹) ↾ (ℤ≥‘𝑁)) = seq𝑁( + , 𝐹)) | ||
Theorem | seqid2 13406* | The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for +) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 + 𝑍) = 𝑥) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝐾)) & ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐾 + 1)...𝑁)) → (𝐹‘𝑥) = 𝑍) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (seq𝑀( + , 𝐹)‘𝑁)) | ||
Theorem | seqhomo 13407* | Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁)) | ||
Theorem | seqz 13408* | If the operation + has an absorbing element 𝑍 (a.k.a. zero element), then any sequence containing a 𝑍 evaluates to 𝑍. (Contributed by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑍 + 𝑥) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 + 𝑍) = 𝑍) & ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁)) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → (𝐹‘𝐾) = 𝑍) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝑍) | ||
Theorem | seqfeq4 13409* | Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑥𝑄𝑦)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (seq𝑀(𝑄, 𝐹)‘𝑁)) | ||
Theorem | seqfeq3 13410* | Equality of series under different addition operations which agree on an additively closed subset. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑥𝑄𝑦)) ⇒ ⊢ (𝜑 → seq𝑀( + , 𝐹) = seq𝑀(𝑄, 𝐹)) | ||
Theorem | seqdistr 13411* | The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐶𝑇(𝑥 + 𝑦)) = ((𝐶𝑇𝑥) + (𝐶𝑇𝑦))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝐶𝑇(𝐺‘𝑥))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (𝐶𝑇(seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | ser0 13412 | The value of the partial sums in a zero-valued infinite series. (Contributed by Mario Carneiro, 31-Aug-2013.) (Revised by Mario Carneiro, 15-Dec-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑁 ∈ 𝑍 → (seq𝑀( + , (𝑍 × {0}))‘𝑁) = 0) | ||
Theorem | ser0f 13413 | A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( + , (𝑍 × {0})) = (𝑍 × {0})) | ||
Theorem | serge0 13414* | A finite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 8-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 0 ≤ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → 0 ≤ (seq𝑀( + , 𝐹)‘𝑁)) | ||
Theorem | serle 13415* | Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ≤ (𝐺‘𝑘)) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) ≤ (seq𝑀( + , 𝐺)‘𝑁)) | ||
Theorem | ser1const 13416 | Value of the partial series sum of a constant function. (Contributed by NM, 8-Aug-2005.) (Revised by Mario Carneiro, 16-Feb-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (seq1( + , (ℕ × {𝐴}))‘𝑁) = (𝑁 · 𝐴)) | ||
Theorem | seqof 13417* | Distribute function operation through a sequence. Note that 𝐺(𝑧) is an implicit function on 𝑧. (Contributed by Mario Carneiro, 3-Mar-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝑧 ∈ 𝐴 ↦ (𝐺‘𝑥))) ⇒ ⊢ (𝜑 → (seq𝑀( ∘f + , 𝐹)‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqof2 13418* | Distribute function operation through a sequence. Maps-to notation version of seqof 13417. (Contributed by Mario Carneiro, 7-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴)) → 𝑋 ∈ 𝑊) ⇒ ⊢ (𝜑 → (seq𝑀( ∘f + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁))) | ||
Syntax | cexp 13419 | Extend class notation to include exponentiation of a complex number to an integer power. |
class ↑ | ||
Definition | df-exp 13420* |
Define exponentiation to nonnegative integer powers. For example,
(5↑2) = 25 (ex-exp 28157). Terminology: In general,
"exponentiation" is the operation of raising a
"base" 𝑥 to the power
of the "exponent" 𝑦, resulting in the "power"
(𝑥↑𝑦), also
called "x to the power of y". In this case, "integer
exponentiation" is
the operation of raising a complex "base" 𝑥 to the
power of an
integer 𝑦, resulting in the "integer
power" (𝑥↑𝑦).
This definition is not meant to be used directly; instead, exp0 13423 and expp1 13426 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. 10-Jun-2005: The definition was extended to include zero exponents, so that 0↑0 = 1 per the convention of Definition 10-4.1 of [Gleason] p. 134 (0exp0e1 13424). 4-Jun-2014: The definition was extended to include negative integer exponents. For example, (-3↑-2) = (1 / 9) (ex-exp 28157). The case 𝑥 = 0, 𝑦 < 0 gives the value (1 / 0), so we will avoid this case in our theorems. For a definition of exponentiation including complex exponents see df-cxp 25068 (complex exponentiation). Both definitions are equivalent for integer exponents, see cxpexpz 25177. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.) |
⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}))‘-𝑦))))) | ||
Theorem | expval 13421 | Value of exponentiation to integer powers. (Contributed by NM, 20-May-2004.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) = if(𝑁 = 0, 1, if(0 < 𝑁, (seq1( · , (ℕ × {𝐴}))‘𝑁), (1 / (seq1( · , (ℕ × {𝐴}))‘-𝑁))))) | ||
Theorem | expnnval 13422 | Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ × {𝐴}))‘𝑁)) | ||
Theorem | exp0 13423 | Value of a complex number raised to the 0th power. Note that under our definition, 0↑0 = 1, following the convention used by Gleason. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by NM, 20-May-2004.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) | ||
Theorem | 0exp0e1 13424 | 0↑0 = 1. This is our convention. It follows the convention used by Gleason; see Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (0↑0) = 1 | ||
Theorem | exp1 13425 | Value of a complex number raised to the first power. (Contributed by NM, 20-Oct-2004.) (Revised by Mario Carneiro, 2-Jul-2013.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴) | ||
Theorem | expp1 13426 | 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 NM, 20-May-2005.) (Revised by Mario Carneiro, 2-Jul-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) | ||
Theorem | expneg 13427 | Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | ||
Theorem | expneg2 13428 | Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) | ||
Theorem | expn1 13429 | A number to the negative one power is the reciprocal. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑-1) = (1 / 𝐴)) | ||
Theorem | expcllem 13430* | Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.) |
⊢ 𝐹 ⊆ ℂ & ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹) & ⊢ 1 ∈ 𝐹 ⇒ ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ 𝐹) | ||
Theorem | expcl2lem 13431* | Lemma for proving integer exponentiation closure laws. (Contributed by Mario Carneiro, 4-Jun-2014.) (Revised by Mario Carneiro, 9-Sep-2014.) |
⊢ 𝐹 ⊆ ℂ & ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹) & ⊢ 1 ∈ 𝐹 & ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐹) ⇒ ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ 𝐹) | ||
Theorem | nnexpcl 13432 | Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ) | ||
Theorem | nn0expcl 13433 | Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ0) | ||
Theorem | zexpcl 13434 | Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℤ) | ||
Theorem | qexpcl 13435 | Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℚ) | ||
Theorem | reexpcl 13436 | Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | expcl 13437 | Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ) | ||
Theorem | rpexpcl 13438 | Closure law for exponentiation of positive reals. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ+) | ||
Theorem | reexpclz 13439 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 4-Jun-2014.) (Revised by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | qexpclz 13440 | Closure of exponentiation of rational numbers. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℚ) | ||
Theorem | m1expcl2 13441 | Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ {-1, 1}) | ||
Theorem | m1expcl 13442 | Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ ℤ) | ||
Theorem | expclzlem 13443 | Closure law for integer exponentiation. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ (ℂ ∖ {0})) | ||
Theorem | expclz 13444 | Closure law for integer exponentiation. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ) | ||
Theorem | nn0expcli 13445 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝐴↑𝑁) ∈ ℕ0 | ||
Theorem | nn0sqcl 13446 | The square of a nonnegative integer is a nonnegative integer. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (𝐴 ∈ ℕ0 → (𝐴↑2) ∈ ℕ0) | ||
Theorem | expm1t 13447 | Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = ((𝐴↑(𝑁 − 1)) · 𝐴)) | ||
Theorem | 1exp 13448 | 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 | expeq0 13449 | Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by NM, 23-Feb-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0)) | ||
Theorem | expne0 13450 | Positive integer exponentiation is nonzero iff its mantissa is nonzero. (Contributed by NM, 6-May-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) ≠ 0 ↔ 𝐴 ≠ 0)) | ||
Theorem | expne0i 13451 | Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ≠ 0) | ||
Theorem | expgt0 13452 | 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 | expnegz 13453 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | ||
Theorem | 0exp 13454 | Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.) |
⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0) | ||
Theorem | expge0 13455 | 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 13456 | 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 13457 | 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 13458 | 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 | mulexpz 13459 | 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 13460 | Nonnegative integer exponentiation of a reciprocal. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → ((1 / 𝐴)↑𝑁) = (1 / (𝐴↑𝑁))) | ||
Theorem | expadd 13461 | 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 13462 | Lemma for expaddz 13463. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) | ||
Theorem | expaddz 13463 | 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 13464 | 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 | expmulz 13465 | 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 13466 | Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018.) |
⊢ (𝑁 ∈ ℤ → (-1↑(2 · 𝑁)) = 1) | ||
Theorem | expsub 13467 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 − 𝑁)) = ((𝐴↑𝑀) / (𝐴↑𝑁))) | ||
Theorem | expp1z 13468 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) | ||
Theorem | expm1 13469 | Value of a 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 13470 | Nonnegative integer exponentiation of a quotient. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑁 ∈ ℕ0) → ((𝐴 / 𝐵)↑𝑁) = ((𝐴↑𝑁) / (𝐵↑𝑁))) | ||
Theorem | sqval 13471 | Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴)) | ||
Theorem | sqneg 13472 | The square of the negative of a number. (Contributed by NM, 15-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) | ||
Theorem | sqsubswap 13473 | Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = ((𝐵 − 𝐴)↑2)) | ||
Theorem | sqcl 13474 | Closure of square. (Contributed by NM, 10-Aug-1999.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈ ℂ) | ||
Theorem | sqmul 13475 | Distribution of square over multiplication. (Contributed by NM, 21-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) | ||
Theorem | sqeq0 13476 | A number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006.) |
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0)) | ||
Theorem | sqdiv 13477 | Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.) (Proof shortened by Mario Carneiro, 9-Jul-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2))) | ||
Theorem | sqdivid 13478 | The square of a nonzero number divided by itself yields the number itself. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴↑2) / 𝐴) = 𝐴) | ||
Theorem | sqne0 13479 | A number is nonzero iff its square is nonzero. (Contributed by NM, 11-Mar-2006.) |
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0)) | ||
Theorem | resqcl 13480 | Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.) |
⊢ (𝐴 ∈ ℝ → (𝐴↑2) ∈ ℝ) | ||
Theorem | sqgt0 13481 | The square of a nonzero real is positive. (Contributed by NM, 8-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 0 < (𝐴↑2)) | ||
Theorem | sqn0rp 13482 | The square of a nonzero real is a positive real. (Contributed by AV, 5-Mar-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ∈ ℝ+) | ||
Theorem | nnsqcl 13483 | The naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℕ) | ||
Theorem | zsqcl 13484 | Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ) | ||
Theorem | qsqcl 13485 | The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (𝐴↑2) ∈ ℚ) | ||
Theorem | sq11 13486 | 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 13487 | The square function is one-to-one for nonnegative integers. (Contributed by AV, 25-Jun-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) | ||
Theorem | lt2sq 13488 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) | ||
Theorem | le2sq 13489 | The square function on nonnegative reals is monotonic. (Contributed by NM, 18-Oct-1999.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
Theorem | le2sq2 13490 | The square of a 'less than or equal to' ordering. (Contributed by NM, 21-Mar-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)) → (𝐴↑2) ≤ (𝐵↑2)) | ||
Theorem | sqge0 13491 | A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴↑2)) | ||
Theorem | zsqcl2 13492 | 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 13493 | Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (0↑𝑁) = 0) | ||
Theorem | exp0d 13494 | Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑0) = 1) | ||
Theorem | exp1d 13495 | Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑1) = 𝐴) | ||
Theorem | expeq0d 13496 | Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐴↑𝑁) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
Theorem | sqvald 13497 | Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) | ||
Theorem | sqcld 13498 | Closure of square. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑2) ∈ ℂ) | ||
Theorem | sqeq0d 13499 | A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (𝐴↑2) = 0) ⇒ ⊢ (𝜑 → 𝐴 = 0) | ||
Theorem | expcld 13500 | Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |