![]() |
Metamath
Proof Explorer Theorem List (p. 141 of 480) | < 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | serf 14001* | An infinite series of complex terms is a function from β to β. (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β seqπ( + , πΉ):πβΆβ) | ||
Theorem | serfre 14002* | An infinite series of real numbers is a function from β to β. (Contributed by NM, 18-Apr-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β seqπ( + , πΉ):πβΆβ) | ||
Theorem | monoord 14003* | Ordering relation for a monotonic sequence, increasing case. (Contributed by NM, 13-Mar-2005.) (Revised by Mario Carneiro, 9-Feb-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...(π β 1))) β (πΉβπ) β€ (πΉβ(π + 1))) β β’ (π β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | monoord2 14004* | Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) β β’ (π β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | sermono 14005* | The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 30-Jun-2013.) |
β’ (π β πΎ β (β€β₯βπ)) & β’ (π β π β (β€β₯βπΎ)) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β β) & β’ ((π β§ π₯ β ((πΎ + 1)...π)) β 0 β€ (πΉβπ₯)) β β’ (π β (seqπ( + , πΉ)βπΎ) β€ (seqπ( + , πΉ)βπ)) | ||
Theorem | seqsplit 14006* | Split a sequence into two sequences. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯β(π + 1))) & β’ (π β π β (β€β₯βπΎ)) & β’ ((π β§ π₯ β (πΎ...π)) β (πΉβπ₯) β π) β β’ (π β (seqπΎ( + , πΉ)βπ) = ((seqπΎ( + , πΉ)βπ) + (seq(π + 1)( + , πΉ)βπ))) | ||
Theorem | seq1p 14007* | Removing the first term from a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯β(π + 1))) & β’ (π β π β β€) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β π) β β’ (π β (seqπ( + , πΉ)βπ) = ((πΉβπ) + (seq(π + 1)( + , πΉ)βπ))) | ||
Theorem | seqcaopr3 14008* | Lemma for seqcaopr2 14009. (Contributed by Mario Carneiro, 25-Apr-2016.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ππ¦) β π) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β π) & β’ ((π β§ π β (π...π)) β (πΊβπ) β π) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ)π(πΊβπ))) & β’ ((π β§ π β (π..^π)) β (((seqπ( + , πΉ)βπ)π(seqπ( + , πΊ)βπ)) + ((πΉβ(π + 1))π(πΊβ(π + 1)))) = (((seqπ( + , πΉ)βπ) + (πΉβ(π + 1)))π((seqπ( + , πΊ)βπ) + (πΊβ(π + 1))))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ)π(seqπ( + , πΊ)βπ))) | ||
Theorem | seqcaopr2 14009* | 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 14010* | 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 14011* | Lemma for seqf1o 14014. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯ + π¦) = (π¦ + π₯)) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΆ β π) & β’ (π β πΊ:π΄βΆπΆ) & β’ (π β πΎ β π΄) & β’ (π β (π...π) β π΄) β β’ (π β ((πΊβπΎ) + (seqπ( + , πΊ)βπ)) = ((seqπ( + , πΊ)βπ) + (πΊβπΎ))) | ||
Theorem | seqf1olem1 14012* | Lemma for seqf1o 14014. (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 14013* | Lemma for seqf1o 14014. (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 14014* | 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 14015* | The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 26-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...π)) β (πΊβπ) β β) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ) + (πΊβπ))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ) + (seqπ( + , πΊ)βπ))) | ||
Theorem | sersub 14016* | The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π β (π...π)) β (πΉβπ) β β) & β’ ((π β§ π β (π...π)) β (πΊβπ) β β) & β’ ((π β§ π β (π...π)) β (π»βπ) = ((πΉβπ) β (πΊβπ))) β β’ (π β (seqπ( + , π»)βπ) = ((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ))) | ||
Theorem | seqid3 14017* | 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 14018* | 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 14019* | 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 14020* | Apply a homomorphism to a sequence. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) β π) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π»β(π₯ + π¦)) = ((π»βπ₯)π(π»βπ¦))) & β’ ((π β§ π₯ β (π...π)) β (π»β(πΉβπ₯)) = (πΊβπ₯)) β β’ (π β (π»β(seqπ( + , πΉ)βπ)) = (seqπ(π, πΊ)βπ)) | ||
Theorem | seqz 14021* | 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 14022* | 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 14023* | 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 14024* | The distributive property for series. (Contributed by Mario Carneiro, 28-Jul-2013.) (Revised by Mario Carneiro, 27-May-2014.) |
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΆπ(π₯ + π¦)) = ((πΆππ₯) + (πΆππ¦))) & β’ (π β π β (β€β₯βπ)) & β’ ((π β§ π₯ β (π...π)) β (πΊβπ₯) β π) & β’ ((π β§ π₯ β (π...π)) β (πΉβπ₯) = (πΆπ(πΊβπ₯))) β β’ (π β (seqπ( + , πΉ)βπ) = (πΆπ(seqπ( + , πΊ)βπ))) | ||
Theorem | ser0 14025 | 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 14026 | A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014.) |
β’ π = (β€β₯βπ) β β’ (π β β€ β seqπ( + , (π Γ {0})) = (π Γ {0})) | ||
Theorem | serge0 14027* | 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 14028* | 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 14029 | 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 14030* | 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 14031* | Distribute function operation through a sequence. Maps-to notation version of seqof 14030. (Contributed by Mario Carneiro, 7-Jul-2017.) |
β’ (π β π΄ β π) & β’ (π β π β (β€β₯βπ)) & β’ (π β (π...π) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π§ β π΄)) β π β π) β β’ (π β (seqπ( βf + , (π₯ β π΅ β¦ (π§ β π΄ β¦ π)))βπ) = (π§ β π΄ β¦ (seqπ( + , (π₯ β π΅ β¦ π))βπ))) | ||
Syntax | cexp 14032 | Extend class notation to include exponentiation of a complex number to an integer power. |
class β | ||
Definition | df-exp 14033* |
Define exponentiation of complex numbers with integer exponents. For
example, (5β2) = 25 (ex-exp 29971). 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 14036 and expp1 14039 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 do not have superscripts. 10-Jun-2005: The definition was extended from positive exponents to nonegative exponent, so that 0β0 = 1, following standard convention, for instance Definition 10-4.1 of [Gleason] p. 134 (0exp0e1 14037). 4-Jun-2014: The definition was extended to integer exponents. For example, (-3β-2) = (1 / 9) (ex-exp 29971). The case π₯ = 0, π¦ < 0 gives the "value" (1 / 0); relying on this should be avoided in applications. For a definition of exponentiation including complex exponents see df-cxp 26303 (complex exponentiation). Both definitions are equivalent for integer exponents, see cxpexpz 26412. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.) |
β’ β = (π₯ β β, π¦ β β€ β¦ if(π¦ = 0, 1, if(0 < π¦, (seq1( Β· , (β Γ {π₯}))βπ¦), (1 / (seq1( Β· , (β Γ {π₯}))β-π¦))))) | ||
Theorem | expval 14034 | 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 14035 | Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ π β β) β (π΄βπ) = (seq1( Β· , (β Γ {π΄}))βπ)) | ||
Theorem | exp0 14036 | Value of a complex number raised to the zeroth power. Under our definition, 0β0 = 1 (0exp0e1 14037), following standard convention, for instance 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 14037 | The zeroth power of zero equals one. See comment of exp0 14036. (Contributed by David A. Wheeler, 8-Dec-2018.) |
β’ (0β0) = 1 | ||
Theorem | exp1 14038 | 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 14039 | Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. When π΄ is nonzero, this holds for all integers π, see expneg 14040. (Contributed by NM, 20-May-2005.) (Revised by Mario Carneiro, 2-Jul-2013.) |
β’ ((π΄ β β β§ π β β0) β (π΄β(π + 1)) = ((π΄βπ) Β· π΄)) | ||
Theorem | expneg 14040 | Value of a complex number raised to a nonpositive integer power. When π΄ = 0 and π is nonzero, both sides have the "value" (1 / 0); relying on that should be avoid in applications. (Contributed by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ π β β0) β (π΄β-π) = (1 / (π΄βπ))) | ||
Theorem | expneg2 14041 | Value of a complex number raised to a nonpositive integer power. When π΄ = 0 and π is nonzero, both sides have the "value" (1 / 0); relying on that should be avoid in applications. (Contributed by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ π β β β§ -π β β0) β (π΄βπ) = (1 / (π΄β-π))) | ||
Theorem | expn1 14042 | A complex number raised to the negative one power is its reciprocal. When π΄ = 0, both sides have the "value" (1 / 0); relying on that should be avoid in applications. (Contributed by Mario Carneiro, 4-Jun-2014.) |
β’ (π΄ β β β (π΄β-1) = (1 / π΄)) | ||
Theorem | expcllem 14043* | Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005.) |
β’ πΉ β β & β’ ((π₯ β πΉ β§ π¦ β πΉ) β (π₯ Β· π¦) β πΉ) & β’ 1 β πΉ β β’ ((π΄ β πΉ β§ π΅ β β0) β (π΄βπ΅) β πΉ) | ||
Theorem | expcl2lem 14044* | 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 14045 | Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.) |
β’ ((π΄ β β β§ π β β0) β (π΄βπ) β β) | ||
Theorem | nn0expcl 14046 | Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005.) |
β’ ((π΄ β β0 β§ π β β0) β (π΄βπ) β β0) | ||
Theorem | zexpcl 14047 | Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.) |
β’ ((π΄ β β€ β§ π β β0) β (π΄βπ) β β€) | ||
Theorem | qexpcl 14048 | Closure of exponentiation of rationals. For integer exponents, see qexpclz 14052. (Contributed by NM, 16-Dec-2005.) |
β’ ((π΄ β β β§ π β β0) β (π΄βπ) β β) | ||
Theorem | reexpcl 14049 | Closure of exponentiation of reals. For integer exponents, see reexpclz 14053. (Contributed by NM, 14-Dec-2005.) |
β’ ((π΄ β β β§ π β β0) β (π΄βπ) β β) | ||
Theorem | expcl 14050 | Closure law for nonnegative integer exponentiation. For integer exponents, see expclz 14055. (Contributed by NM, 26-May-2005.) |
β’ ((π΄ β β β§ π β β0) β (π΄βπ) β β) | ||
Theorem | rpexpcl 14051 | Closure law for integer exponentiation of positive reals. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 9-Sep-2014.) |
β’ ((π΄ β β+ β§ π β β€) β (π΄βπ) β β+) | ||
Theorem | qexpclz 14052 | Closure of integer exponentiation of rational numbers. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π β β€) β (π΄βπ) β β) | ||
Theorem | reexpclz 14053 | Closure of integer exponentiation of reals. (Contributed by Mario Carneiro, 4-Jun-2014.) (Revised by Mario Carneiro, 9-Sep-2014.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π β β€) β (π΄βπ) β β) | ||
Theorem | expclzlem 14054 | Lemma for expclz 14055. (Contributed by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π β β€) β (π΄βπ) β (β β {0})) | ||
Theorem | expclz 14055 | Closure law for integer exponentiation of complex numnbers. (Contributed by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π β β€) β (π΄βπ) β β) | ||
Theorem | m1expcl2 14056 | Closure of integer exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ (π β β€ β (-1βπ) β {-1, 1}) | ||
Theorem | m1expcl 14057 | Closure of exponentiation of negative one. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ (π β β€ β (-1βπ) β β€) | ||
Theorem | zexpcld 14058 | Closure of exponentiation of integers, deduction form. (Contributed by SN, 15-Sep-2024.) |
β’ (π β π΄ β β€) & β’ (π β π β β0) β β’ (π β (π΄βπ) β β€) | ||
Theorem | nn0expcli 14059 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 17-Apr-2015.) |
β’ π΄ β β0 & β’ π β β0 β β’ (π΄βπ) β β0 | ||
Theorem | nn0sqcl 14060 | The square of a nonnegative integer is a nonnegative integer. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ (π΄ β β0 β (π΄β2) β β0) | ||
Theorem | expm1t 14061 | Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005.) |
β’ ((π΄ β β β§ π β β) β (π΄βπ) = ((π΄β(π β 1)) Β· π΄)) | ||
Theorem | 1exp 14062 | 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 14063 | A positive integer power is zero if and only if its base is zero. (Contributed by NM, 23-Feb-2005.) |
β’ ((π΄ β β β§ π β β) β ((π΄βπ) = 0 β π΄ = 0)) | ||
Theorem | expne0 14064 | A positive integer power is nonzero if and only if its base is nonzero. (Contributed by NM, 6-May-2005.) |
β’ ((π΄ β β β§ π β β) β ((π΄βπ) β 0 β π΄ β 0)) | ||
Theorem | expne0i 14065 | 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 14066 | 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 14067 | 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 14068 | Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.) |
β’ (π β β β (0βπ) = 0) | ||
Theorem | expge0 14069 | 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 14070 | 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 14071 | 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 14072 | 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 14073 | 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 14074 | Integer exponentiation of a reciprocal. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π β β€) β ((1 / π΄)βπ) = (1 / (π΄βπ))) | ||
Theorem | expadd 14075 | 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 14076 | Lemma for expaddz 14077. (Contributed by Mario Carneiro, 4-Jun-2014.) |
β’ (((π΄ β β β§ π΄ β 0) β§ (π β β β§ -π β β) β§ π β β0) β (π΄β(π + π)) = ((π΄βπ) Β· (π΄βπ))) | ||
Theorem | expaddz 14077 | 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 14078 | 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 14079 | 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 14080 | Exponentiation of negative one to an even power. (Contributed by Scott Fenton, 17-Jan-2018.) |
β’ (π β β€ β (-1β(2 Β· π)) = 1) | ||
Theorem | expsub 14081 | Exponent subtraction law for integer exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
β’ (((π΄ β β β§ π΄ β 0) β§ (π β β€ β§ π β β€)) β (π΄β(π β π)) = ((π΄βπ) / (π΄βπ))) | ||
Theorem | expp1z 14082 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ π΄ β 0 β§ π β β€) β (π΄β(π + 1)) = ((π΄βπ) Β· π΄)) | ||
Theorem | expm1 14083 | 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 14084 | Nonnegative integer exponentiation of a quotient. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
β’ ((π΄ β β β§ (π΅ β β β§ π΅ β 0) β§ π β β0) β ((π΄ / π΅)βπ) = ((π΄βπ) / (π΅βπ))) | ||
Theorem | sqval 14085 | Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.) |
β’ (π΄ β β β (π΄β2) = (π΄ Β· π΄)) | ||
Theorem | sqneg 14086 | The square of the negative of a number. (Contributed by NM, 15-Jan-2006.) |
β’ (π΄ β β β (-π΄β2) = (π΄β2)) | ||
Theorem | sqsubswap 14087 | Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ β π΅)β2) = ((π΅ β π΄)β2)) | ||
Theorem | sqcl 14088 | Closure of square. (Contributed by NM, 10-Aug-1999.) |
β’ (π΄ β β β (π΄β2) β β) | ||
Theorem | sqmul 14089 | Distribution of squaring over multiplication. (Contributed by NM, 21-Mar-2008.) |
β’ ((π΄ β β β§ π΅ β β) β ((π΄ Β· π΅)β2) = ((π΄β2) Β· (π΅β2))) | ||
Theorem | sqeq0 14090 | A complex number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006.) |
β’ (π΄ β β β ((π΄β2) = 0 β π΄ = 0)) | ||
Theorem | sqdiv 14091 | 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 14092 | The square of a nonzero complex number divided by itself equals that number. (Contributed by AV, 19-Jul-2021.) |
β’ ((π΄ β β β§ π΄ β 0) β ((π΄β2) / π΄) = π΄) | ||
Theorem | sqne0 14093 | A complex number is nonzero if and only if its square is nonzero. (Contributed by NM, 11-Mar-2006.) |
β’ (π΄ β β β ((π΄β2) β 0 β π΄ β 0)) | ||
Theorem | resqcl 14094 | Closure of squaring in reals. (Contributed by NM, 18-Oct-1999.) |
β’ (π΄ β β β (π΄β2) β β) | ||
Theorem | resqcld 14095 | Closure of squaring in reals, deduction form. (Contributed by Mario Carneiro, 28-May-2016.) |
β’ (π β π΄ β β) β β’ (π β (π΄β2) β β) | ||
Theorem | sqgt0 14096 | The square of a nonzero real is positive. (Contributed by NM, 8-Sep-2007.) |
β’ ((π΄ β β β§ π΄ β 0) β 0 < (π΄β2)) | ||
Theorem | sqn0rp 14097 | The square of a nonzero real is a positive real. (Contributed by AV, 5-Mar-2023.) |
β’ ((π΄ β β β§ π΄ β 0) β (π΄β2) β β+) | ||
Theorem | nnsqcl 14098 | The positive naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π΄ β β β (π΄β2) β β) | ||
Theorem | zsqcl 14099 | Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ (π΄ β β€ β (π΄β2) β β€) | ||
Theorem | qsqcl 14100 | The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
β’ (π΄ β β β (π΄β2) β β) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |