Home | Metamath
Proof Explorer Theorem List (p. 135 of 454) | < 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-28701) |
Hilbert Space Explorer
(28702-30224) |
Users' Mathboxes
(30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | seqcaopr3 13401* | Lemma for seqcaopr2 13402. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀..^𝑁)) → (((seq𝑀( + , 𝐹)‘𝑛)𝑄(seq𝑀( + , 𝐺)‘𝑛)) + ((𝐹‘(𝑛 + 1))𝑄(𝐺‘(𝑛 + 1)))) = (((seq𝑀( + , 𝐹)‘𝑛) + (𝐹‘(𝑛 + 1)))𝑄((seq𝑀( + , 𝐺)‘𝑛) + (𝐺‘(𝑛 + 1))))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqcaopr2 13402* | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Mario Carneiro, 30-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝑄𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) ∧ (𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆))) → ((𝑥𝑄𝑧) + (𝑦𝑄𝑤)) = ((𝑥 + 𝑦)𝑄(𝑧 + 𝑤))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘)𝑄(𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁)𝑄(seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqcaopr 13403* | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 30-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqf1olem2a 13404* | Lemma for seqf1o 13407. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐶) & ⊢ (𝜑 → 𝐾 ∈ 𝐴) & ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐴) ⇒ ⊢ (𝜑 → ((𝐺‘𝐾) + (seq𝑀( + , 𝐺)‘𝑁)) = ((seq𝑀( + , 𝐺)‘𝑁) + (𝐺‘𝐾))) | ||
Theorem | seqf1olem1 13405* | Lemma for seqf1o 13407. (Contributed by Mario Carneiro, 26-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) & ⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) & ⊢ (𝜑 → 𝐺:(𝑀...(𝑁 + 1))⟶𝐶) & ⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) & ⊢ 𝐾 = (◡𝐹‘(𝑁 + 1)) ⇒ ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁)) | ||
Theorem | seqf1olem2 13406* | Lemma for seqf1o 13407. (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐶 ⊆ 𝑆) & ⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1))) & ⊢ (𝜑 → 𝐺:(𝑀...(𝑁 + 1))⟶𝐶) & ⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) & ⊢ 𝐾 = (◡𝐹‘(𝑁 + 1)) & ⊢ (𝜑 → ∀𝑔∀𝑓((𝑓:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ 𝑔:(𝑀...𝑁)⟶𝐶) → (seq𝑀( + , (𝑔 ∘ 𝑓))‘𝑁) = (seq𝑀( + , 𝑔)‘𝑁))) ⇒ ⊢ (𝜑 → (seq𝑀( + , (𝐺 ∘ 𝐹))‘(𝑁 + 1)) = (seq𝑀( + , 𝐺)‘(𝑁 + 1))) | ||
Theorem | seqf1o 13407* | 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 13408* | The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 26-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) + (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) + (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | sersub 13409* | The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐺‘𝑘) ∈ ℂ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = ((𝐹‘𝑘) − (𝐺‘𝑘))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = ((seq𝑀( + , 𝐹)‘𝑁) − (seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | seqid3 13410* | 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 13411* | 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 13412* | 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 13413* | Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) ∈ 𝑆) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐻‘(𝑥 + 𝑦)) = ((𝐻‘𝑥)𝑄(𝐻‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐻‘(𝐹‘𝑥)) = (𝐺‘𝑥)) ⇒ ⊢ (𝜑 → (𝐻‘(seq𝑀( + , 𝐹)‘𝑁)) = (seq𝑀(𝑄, 𝐺)‘𝑁)) | ||
Theorem | seqz 13414* | 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 13415* | 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 13416* | 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 13417* | The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐶𝑇(𝑥 + 𝑦)) = ((𝐶𝑇𝑥) + (𝐶𝑇𝑦))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘𝑥) ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐹‘𝑥) = (𝐶𝑇(𝐺‘𝑥))) ⇒ ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = (𝐶𝑇(seq𝑀( + , 𝐺)‘𝑁))) | ||
Theorem | ser0 13418 | 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 13419 | A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ (𝑀 ∈ ℤ → seq𝑀( + , (𝑍 × {0})) = (𝑍 × {0})) | ||
Theorem | serge0 13420* | 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 13421* | 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 13422 | 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 13423* | 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 13424* | Distribute function operation through a sequence. Maps-to notation version of seqof 13423. (Contributed by Mario Carneiro, 7-Jul-2017.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝑀...𝑁) ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴)) → 𝑋 ∈ 𝑊) ⇒ ⊢ (𝜑 → (seq𝑀( ∘f + , (𝑥 ∈ 𝐵 ↦ (𝑧 ∈ 𝐴 ↦ 𝑋)))‘𝑁) = (𝑧 ∈ 𝐴 ↦ (seq𝑀( + , (𝑥 ∈ 𝐵 ↦ 𝑋))‘𝑁))) | ||
Syntax | cexp 13425 | Extend class notation to include exponentiation of a complex number to an integer power. |
class ↑ | ||
Definition | df-exp 13426* |
Define exponentiation to nonnegative integer powers. For example,
(5↑2) = 25 (ex-exp 28235). 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 13429 and expp1 13432 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 13430). 4-Jun-2014: The definition was extended to include negative integer exponents. For example, (-3↑-2) = (1 / 9) (ex-exp 28235). 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 25149 (complex exponentiation). Both definitions are equivalent for integer exponents, see cxpexpz 25258. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.) |
⊢ ↑ = (𝑥 ∈ ℂ, 𝑦 ∈ ℤ ↦ if(𝑦 = 0, 1, if(0 < 𝑦, (seq1( · , (ℕ × {𝑥}))‘𝑦), (1 / (seq1( · , (ℕ × {𝑥}))‘-𝑦))))) | ||
Theorem | expval 13427 | 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 13428 | Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ × {𝐴}))‘𝑁)) | ||
Theorem | exp0 13429 | 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 13430 | 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 13431 | 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 13432 | 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 13433 | Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | ||
Theorem | expneg2 13434 | Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0) → (𝐴↑𝑁) = (1 / (𝐴↑-𝑁))) | ||
Theorem | expn1 13435 | A number to the negative one power is the reciprocal. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑-1) = (1 / 𝐴)) | ||
Theorem | expcllem 13436* | Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.) |
⊢ 𝐹 ⊆ ℂ & ⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹) & ⊢ 1 ∈ 𝐹 ⇒ ⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ 𝐹) | ||
Theorem | expcl2lem 13437* | 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 13438 | Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ) | ||
Theorem | nn0expcl 13439 | Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ0) | ||
Theorem | zexpcl 13440 | Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℤ) | ||
Theorem | qexpcl 13441 | Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℚ) | ||
Theorem | reexpcl 13442 | Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | expcl 13443 | Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ) | ||
Theorem | rpexpcl 13444 | Closure law for exponentiation of positive reals. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ+) | ||
Theorem | reexpclz 13445 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 4-Jun-2014.) (Revised by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | qexpclz 13446 | Closure of exponentiation of rational numbers. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℚ) | ||
Theorem | m1expcl2 13447 | Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ {-1, 1}) | ||
Theorem | m1expcl 13448 | Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (𝑁 ∈ ℤ → (-1↑𝑁) ∈ ℤ) | ||
Theorem | expclzlem 13449 | Closure law for integer exponentiation. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ (ℂ ∖ {0})) | ||
Theorem | expclz 13450 | Closure law for integer exponentiation. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑𝑁) ∈ ℂ) | ||
Theorem | nn0expcli 13451 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝐴↑𝑁) ∈ ℕ0 | ||
Theorem | nn0sqcl 13452 | The square of a nonnegative integer is a nonnegative integer. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (𝐴 ∈ ℕ0 → (𝐴↑2) ∈ ℕ0) | ||
Theorem | expm1t 13453 | Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = ((𝐴↑(𝑁 − 1)) · 𝐴)) | ||
Theorem | 1exp 13454 | 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 13455 | Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by NM, 23-Feb-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) = 0 ↔ 𝐴 = 0)) | ||
Theorem | expne0 13456 | Positive integer exponentiation is nonzero iff its mantissa is nonzero. (Contributed by NM, 6-May-2005.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) ≠ 0 ↔ 𝐴 ≠ 0)) | ||
Theorem | expne0i 13457 | 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 13458 | 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 13459 | Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | ||
Theorem | 0exp 13460 | Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.) |
⊢ (𝑁 ∈ ℕ → (0↑𝑁) = 0) | ||
Theorem | expge0 13461 | 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 13462 | 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 13463 | 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 13464 | 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 13465 | 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 13466 | Nonnegative integer exponentiation of a reciprocal. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → ((1 / 𝐴)↑𝑁) = (1 / (𝐴↑𝑁))) | ||
Theorem | expadd 13467 | 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 13468 | Lemma for expaddz 13469. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℝ ∧ -𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ0) → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁))) | ||
Theorem | expaddz 13469 | 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 13470 | 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 13471 | 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 13472 | Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018.) |
⊢ (𝑁 ∈ ℤ → (-1↑(2 · 𝑁)) = 1) | ||
Theorem | expsub 13473 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝐴↑(𝑀 − 𝑁)) = ((𝐴↑𝑀) / (𝐴↑𝑁))) | ||
Theorem | expp1z 13474 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴)) | ||
Theorem | expm1 13475 | 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 13476 | Nonnegative integer exponentiation of a quotient. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) ∧ 𝑁 ∈ ℕ0) → ((𝐴 / 𝐵)↑𝑁) = ((𝐴↑𝑁) / (𝐵↑𝑁))) | ||
Theorem | sqval 13477 | Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑2) = (𝐴 · 𝐴)) | ||
Theorem | sqneg 13478 | The square of the negative of a number. (Contributed by NM, 15-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → (-𝐴↑2) = (𝐴↑2)) | ||
Theorem | sqsubswap 13479 | Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = ((𝐵 − 𝐴)↑2)) | ||
Theorem | sqcl 13480 | Closure of square. (Contributed by NM, 10-Aug-1999.) |
⊢ (𝐴 ∈ ℂ → (𝐴↑2) ∈ ℂ) | ||
Theorem | sqmul 13481 | Distribution of square over multiplication. (Contributed by NM, 21-Mar-2008.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2))) | ||
Theorem | sqeq0 13482 | A number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006.) |
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) = 0 ↔ 𝐴 = 0)) | ||
Theorem | sqdiv 13483 | 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 13484 | The square of a nonzero number divided by itself yields the number itself. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((𝐴↑2) / 𝐴) = 𝐴) | ||
Theorem | sqne0 13485 | A number is nonzero iff its square is nonzero. (Contributed by NM, 11-Mar-2006.) |
⊢ (𝐴 ∈ ℂ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0)) | ||
Theorem | resqcl 13486 | Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.) |
⊢ (𝐴 ∈ ℝ → (𝐴↑2) ∈ ℝ) | ||
Theorem | sqgt0 13487 | The square of a nonzero real is positive. (Contributed by NM, 8-Sep-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 0 < (𝐴↑2)) | ||
Theorem | sqn0rp 13488 | The square of a nonzero real is a positive real. (Contributed by AV, 5-Mar-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ∈ ℝ+) | ||
Theorem | nnsqcl 13489 | The naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝐴 ∈ ℕ → (𝐴↑2) ∈ ℕ) | ||
Theorem | zsqcl 13490 | Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈ ℤ) | ||
Theorem | qsqcl 13491 | The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (𝐴↑2) ∈ ℚ) | ||
Theorem | sq11 13492 | 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 13493 | The square function is one-to-one for nonnegative integers. (Contributed by AV, 25-Jun-2023.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴↑2) = (𝐵↑2) ↔ 𝐴 = 𝐵)) | ||
Theorem | lt2sq 13494 | The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) | ||
Theorem | le2sq 13495 | The square function on nonnegative reals is monotonic. (Contributed by NM, 18-Oct-1999.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
Theorem | le2sq2 13496 | The square of a 'less than or equal to' ordering. (Contributed by NM, 21-Mar-2008.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵)) → (𝐴↑2) ≤ (𝐵↑2)) | ||
Theorem | sqge0 13497 | A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.) |
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴↑2)) | ||
Theorem | zsqcl2 13498 | 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 13499 | Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (0↑𝑁) = 0) | ||
Theorem | exp0d 13500 | Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴↑0) = 1) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |