mmtheorems68 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 6701-6800 - Page 68 of 123

Type	Label	Description
Statement
Theorem	ser1p1i 6701	The value of the next term in an infinite series.
|- F = {<.x, y>. | (x e. NN /\ y = A)}   &   |- C e. V   &   |- (x = (B + 1) -> A = C)   =>   |- (B e. NN -> (( + seq1 F)` (B + 1)) = ((( + seq1 F)` B) + C))
Theorem	ser1monoi 6702	The partial sums in an infinite series of positive terms form a monotonic sequence.
|- F:NN-->RR   &   |- (x e. NN -> 0 <_ (F` x))   =>   |- (A e. NN -> (( + seq1 F)` A) <_ (( + seq1 F)` (A + 1)))
Theorem	ser1add2i 6703	The sum of two infinite series.
|- F:NN-->CC   &   |- G:NN-->CC   &   |- H e. V   &   |- ((k e. NN /\ N e. NN /\ k <_ N) -> (H` k) = ((F` k) + (G` k)))   =>   |- (N e. NN -> (( + seq1 H)` N) = ((( + seq1 F)` N) + (( + seq1 G)` N)))
Theorem	ser1addi 6704	The sum of two infinite series.
|- F:NN-->CC   &   |- G:NN-->CC   &   |- H e. V   &   |- ((k e. NN /\ k <_ N) -> (H` k) = ((F` k) + (G` k)))   =>   |- (N e. NN -> (( + seq1 H)` N) = ((( + seq1 F)` N) + (( + seq1 G)` N)))
The "shift" operation
Syntax	cshi 6705	Extend class notation with function shifter.
class shift
Definition	df-shft 6706	Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of CC) and produces a new function on CC. See shftval 6711 for its value.
|- shift = {<.<.f, x>., g>. | g = {<.y, z>. | (y e. CC /\ z = (f` (y - x)))}}
Theorem	shftfval 6707	The value of the sequence shifter operation is a function on CC. A is ordinarily an integer.
|- F e. V   =>   |- (A e. B -> (F shift A) = {<.x, y>. | (x e. CC /\ y = (F` (x - A)))})
Theorem	shftfn 6708	Functionality and domain of a sequence shifted by A.
|- F e. V   =>   |- (A e. B -> (F shift A) Fn CC)
Theorem	shftres 6709	Restriction of a shifted sequence.
|- F e. V   =>   |- ((A e. C /\ B (_ CC) -> ((F shift A) |` B) Fn B)
Theorem	shftresval 6710	Value of a restricted shifted sequence.
|- F e. V   =>   |- (B e. C -> (((F shift A) |` C)` B) = ((F shift A)` B))
Theorem	shftval 6711	Value of a sequence shifted by A.
|- F e. V   =>   |- ((A e. C /\ B e. CC) -> ((F shift A)` B) = (F` (B - A)))
Theorem	shftval2 6712	Value of a sequence shifted by A - B.
|- F e. V   =>   |- ((A e. CC /\ B e. CC /\ C e. CC) -> ((F shift (A - B))` (A + C)) = (F` (B + C)))
Theorem	shftval3 6713	Value of a sequence shifted by A - B.
|- F e. V   =>   |- ((A e. CC /\ B e. CC) -> ((F shift (A - B))` A) = (F` B))
Theorem	shftval4 6714	Value of a sequence shifted by -uA.
|- F e. V   =>   |- ((A e. CC /\ B e. CC) -> ((F shift -uA)` B) = (F` (A + B)))
Theorem	shftval5 6715	Value of a shifted sequence.
|- F e. V   =>   |- ((A e. CC /\ B e. CC) -> ((F shift A)` (B + A)) = (F` B))
Theorem	shftf 6716	Functionality of a restricted shifted sequence.
|- F e. V   =>   |- ((A e. D /\ B (_ CC /\ A.x e. B (F` (x - A)) e. C) -> ((F shift A) |` B):B-->C)
Theorem	2shfti 6717	Composite shift operations.
|- F e. V   =>   |- ((A e. CC /\ B e. CC) -> ((F shift A) shift B) = (F shift (A + B)))
Theorem	shftcan2 6718	Cancellation law for the shift operation.
|- F e. V   =>   |- ((A e. CC /\ B e. CC) -> (((F shift -uA) shift A)` B) = (F` B))
Theorem	shftcan1 6719	Cancellation law for the shift operation.
|- F e. V   =>   |- ((A e. CC /\ B e. CC) -> (((F shift A) shift -uA)` B) = (F` B))
Theorem	shftidt 6720	Identity law for the shift operation.
|- F e. V   =>   |- (A e. CC -> ((F shift 0)` A) = (F` A))
Theorem	seq1shftid 6721	Identity law for the shift operation in a 1-based sequence builder.
|- S e. V   &   |- F e. V   =>   |- (S seq1 (F shift 0)) = (S seq1 F)
Superior limit (lim sup)
Syntax	clsp 6722	Extend class notation to include the limsup function.
class limsup
Definition	df-limsup 6723	Define the superior limit of an infinite sequence of extended real numbers. Definition 12-4.1 of [Gleason] p. 175. See limsupval 6724 for its value.
|- limsup = {<.x, y>. | y = sup({z | E.k e. ZZ z = sup(((x"(ZZ>=` k)) i^i RR*), RR*, < )}, RR*, `' < )}
Theorem	limsupval 6724	The superior limit of an infinite sequence F of extended real numbers, which is the infimum (indicated by `' <) of the set of suprema of all upper infinite subsequences of F. Definition 12-4.1 of [Gleason] p. 175.
|- (F e. A -> (limsup` F) = sup({x | E.k e. ZZ x = sup(((F"(ZZ>=` k)) i^i RR*), RR*, < )}, RR*, `' < ))
Theorem	limsupcl 6725	Closure of the superior limit.
|- (F e. A -> (limsup` F) e. RR*)
Infinite sequence builders "seq" and "seq0"
Syntax	cseqz 6726	Extend class notation with arbitrarily-based recursive sequence builder.
class seq
Syntax	cseq0 6727	Extend class notation with 0-based recursive sequence builder.
class seq0
Definition	df-seqz 6728	Define a recursive sequence builder operation that starts at an arbitrary integer index. See seqz1 6742 and seqzp1 6743 for its initial and successor values. Theorems seq0seqz 6737 and seq1seqz 6736 derive the 0-based seq0 and the 1-based seq1 as special cases.
|- seq = {<.<.x, g>., h>. | h = ((((2nd` x) seq1 (g shift (1 - (1st` x)))) shift ((1st` x) - 1)) |` {k e. ZZ | (1st` x) <_ k})}
Definition	df-seq0 6729	Define a recursive sequence builder operation that starts at index 0. This is a frequently-used variation of the seq1 operation (see df-seq1 6673), which starts at index 1. See seq00 6745 and seq0p1 6746 for its initial and successor values. See dfseq0 6758 for an alternate definition.
|- seq0 = {<.<.f, g>., h>. | h = (((f seq1 (g shift 1)) shift -u1) |` NN0)}
Theorem	seq0fval 6730	Value of the 0-based recursive sequence builder operation.
|- S e. V   &   |- F e. V   =>   |- (S seq0 F) = (((S seq1 (F shift 1)) shift -u1) |` NN0)
Theorem	seq0valt 6731	Value of the 0-based recursive sequence builder operation.
|- S e. V   &   |- F e. V   =>   |- (N e. NN0 -> ((S seq0 F)` N) = (((S seq1 (F shift 1)) shift -u1)` N))
Theorem	seqzfval 6732	Value of the arbitrary-based recursive sequence builder operation.
|- S e. V   &   |- F e. V   =>   |- (M e. A -> (<.M, S>. seq F) = (((S seq1 (F shift (1 - M))) shift (M - 1)) |` {k e. ZZ | M <_ k}))
Theorem	seqzfval2 6733	Value of the arbitrary-based recursive sequence builder operation.
|- S e. V   &   |- F e. V   =>   |- (M e. ZZ -> (<.M, S>. seq F) = (((S seq1 (F shift (1 - M))) shift (M - 1)) |` (ZZ>=` M)))
Theorem	seqzfn 6734	Functionality and domain of a sequence generated by the arbitrary-based recursive sequence builder.
|- S e. V   &   |- F e. V   =>   |- (M e. ZZ -> (<.M, S>. seq F) Fn (ZZ>=` M))
Theorem	seqzval 6735	Value of the arbitrary-based recursive sequence builder operation.
|- S e. V   &   |- F e. V   =>   |- ((M e. A /\ N e. ZZ /\ M <_ N) -> ((<.M, S>. seq F)` N) = (((S seq1 (F shift (1 - M))) shift (M - 1))` N))
Theorem	seq1seqz 6736	The 1-based recursive sequence in terms of the arbitrary-based one.
|- S e. V   &   |- F e. V   =>   |- (S seq1 F) = (<.1, S>. seq F)
Theorem	seq0seqz 6737	The 0-based recursive sequence in terms of the arbitrary-based one.
|- S e. V   &   |- F e. V   =>   |- (S seq0 F) = (<.0, S>. seq F)
Theorem	seq1seq02 6738	A relationship between the 1-based and 0-based recursive sequence builders.
|- S e. V   &   |- F e. V   =>   |- (N e. NN -> ((S seq1 (F shift 1))` N) = (((S seq0 F) shift 1)` N))
Theorem	seq1seq01 6739	The 1-based recursive sequence builder operation in terms of the 0-based one.
|- S e. V   &   |- F e. V   =>   |- (N e. NN -> ((S seq1 F)` N) = (((S seq0 (F shift -u1)) shift 1)` N))
Theorem	seq1seq0 6740	The 1-based recursive sequence builder operation in terms of the 0-based one.
|- S e. V   &   |- F e. V   =>   |- (S seq1 F) = (((S seq0 (F shift -u1)) shift 1) |` NN)
Theorem	seq0fn 6741	Functionality and domain of the 0-based recursive sequence builder.
|- S e. V   &   |- F e. V   =>   |- (S seq0 F) Fn NN0
Theorem	seqz1 6742	Value of the arbitrary-based recursive sequence builder at its initial value.
|- S e. V   &   |- F e. V   =>   |- (M e. ZZ -> ((<.M, S>. seq F)` M) = (F` M))
Theorem	seqzp1 6743	Value of the arbitrary-based recursive sequence builder at a successor value.
|- S e. V   &   |- F e. V   =>   |- (N e. (ZZ>=` M) -> ((<.M, S>. seq F)` (N + 1)) = (((<.M, S>. seq F)` N)S(F` (N + 1))))
Theorem	seqzm1 6744	Value of the recursive sequence builder in terms of its previous value.
|- S e. V   &   |- F e. V   =>   |- ((M e. ZZ /\ N e. ZZ /\ M < N) -> ((<.M, S>. seq F)` N) = (((<.M, S>. seq F)` (N - 1))S(F` N)))
Theorem	seq00 6745	Value of the 0-based recursive sequence builder at 0.
|- S e. V   &   |- F e. V   =>   |- ((S seq0 F)` 0) = (F` 0)
Theorem	seq0p1 6746	Value of the 0-based recursive sequence builder at a successor.
|- S e. V   &   |- F e. V   =>   |- (N e. NN0 -> ((S seq0 F)` (N + 1)) = (((S seq0 F)` N)S(F` (N + 1))))
Theorem	seq01 6747	Value of the 0-based recursive sequence builder at 1.
|- S e. V   &   |- F e. V   =>   |- ((S seq0 F)` 1) = ((F` 0)S(F` 1))
Theorem	seqzval2 6748	Value of the arbitrary-based recursive sequence builder operation.
|- S e. V   &   |- F e. V   =>   |- ((M e. ZZ /\ N e. ZZ /\ M <_ N) -> ((<.M, S>. seq F)` N) = (((S seq0 (F shift -uM)) shift M)` N))
Theorem	seqzfveq 6749	Equality theorem for the recursive sequence builder.
|- S e. V   &   |- F e. V   &   |- G e. V   =>   |- ((N e. (ZZ>=` M) /\ A.k e. (M...N)(F` k) = (G` k)) -> ((<.M, S>. seq F)` N) = ((<.M, S>. seq G)` N))
Theorem	seqzeq 6750	Equality theorem for the recursive sequence builder.
|- S e. V   &   |- F e. V   &   |- G e. V   =>   |- ((M e. ZZ /\ A.k e. (ZZ>=` M)(F` k) = (G` k)) -> (<.M, S>. seq F) = (<.M, S>. seq G))
Theorem	seqzrn2 6751	Range of a sequence generated by the arbitrary-based recursive sequence builder.
|- S e. V   &   |- F e. V   =>   |- (((M e. ZZ /\ (F` M) e. C) /\ ((F |` (ZZ>=` (M + 1))):(ZZ>=` (M + 1))-->B /\ S:(C X. B)-->C)) -> ran (<.M, S>. seq F) (_ C)
Theorem	seqzrn 6752	Range of the arbitrary-based recursive sequence builder (special case of seqzrn2 6751).
|- S e. V   &   |- F e. V   =>   |- ((M e. ZZ /\ F:(ZZ>=` M)-->C /\ S:(C X. C)-->C) -> ran (<.M, S>. seq F) (_ C)
Theorem	seqzcl 6753	Closure of the value of the arbitrary-based recursive sequence builder.
|- S e. V   &   |- F e. V   =>   |- ((N e. (ZZ>=` M) /\ F:(ZZ>=` M)-->C /\ S:(C X. C)-->C) -> ((<.M, S>. seq F)` N) e. C)
Theorem	seqzresval 6754	A restriction of its characteristic function that doesn't change the value of the seq function.
|- S e. V   &   |- F e. V   =>   |- (N e. (ZZ>=` M) -> ((<.M, S>. seq (F |` (M...N)))` N) = ((<.M, S>. seq F)` N))
Theorem	seqzres 6755	The seq function is unchanged by restricting its characteristic function to the seq function's domain.
|- S e. V   &   |- F e. V   =>   |- (M e. ZZ -> (<.M, S>. seq (F |` (ZZ>=` M))) = (<.M, S>. seq F))
Theorem	seqzres2 6756	The seq function is unchanged by substituting its characteristic function with a restricted class builder based on that function.
|- S e. V   &   |- F e. V   =>   |- (M e. ZZ -> (<.M, S>. seq ({<.k, y>. | y = (F` k)} |` ZZ)) = (<.M, S>. seq F))
Theorem	serzcl1i 6757	The partial sums in an infinite series of complex terms are complex.
|- F:(ZZ>=` M)-->CC   =>   |- (N e. (ZZ>=` M) -> ((<.M, + >. seq F)` N) e. CC)
Theorem	dfseq0 6758	Alternate version of df-seq0 6729.
|- seq0 = {<.<.f, g>., h>. | h = (<.0, f>. seq g)}
Theorem	ser0cl1i 6759	The partial sums in an infinite 0-based series of complex terms are complex.
|- F:NN0-->CC   =>   |- (N e. NN0 -> (( + seq0 F)` N) e. CC)
Theorem	ser0fi 6760	A 0-based infinite series is a function from NN0 to CC.
|- F:NN0-->CC   =>   |- ( + seq0 F):NN0-->CC
Theorem	ser00i 6761	The value of the first term in a 0-based infinite series.
|- F = {<.k, y>. | (k e. NN0 /\ y = A)}   &   |- B e. V   &   |- (k = 0 -> A = B)   =>   |- (( + seq0 F)` 0) = B
Theorem	ser0p1i 6762	The value of the next term in a 0-based infinite series.
|- F = {<.k, y>. | (k e. NN0 /\ y = A)}   &   |- B e. V   &   |- (k = (N + 1) -> A = B)   =>   |- (N e. NN0 -> (( + seq0 F)` (N + 1)) = ((( + seq0 F)` N) + B))
Integer powers
Syntax	cexp 6763	Extend class notation to include exponentiation of a complex number to an integer power.
class ^
Definition	df-exp 6764	Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 6766 and expp1 6769 provide a 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. See expnnval 6767 for a description of how the recursive sequence builder is used. 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. (Based on definition contributed by Raph Levien, 15-Oct-2004.)
|- ^ = {<.<.x, y>., z>. | ((x e. CC /\ y e. NN0) /\ z = if(y = 0, 1, (( x. seq1 (NN X. {x}))` y)))}
Theorem	expval 6765	Value of exponentiation to nonnegative integer powers.
|- ((A e. CC /\ N e. NN0) -> (A^N) = if(N = 0, 1, (( x. seq1 (NN X. {A}))` N)))
Theorem	exp0 6766	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.
|- (A e. CC -> (A^0) = 1)
Theorem	expnnval 6767	Value of exponentiation to natural number powers. NN X. {A} is the constant function with value A. The seq1 operation produces the sequence A, A x. A, (A x. A) x. A,... that we evaluate at index B.
|- ((A e. CC /\ B e. NN) -> (A^B) = (( x. seq1 (NN X. {A}))` B))
Theorem	exp1 6768	Value of a complex number raised to the first power.
|- (A e. CC -> (A^1) = A)
Theorem	expp1 6769	Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134.
|- ((A e. CC /\ N e. NN0) -> (A^(N + 1)) = ((A^N) x. A))
Theorem	expcllem 6770	Lemma for proving nonnegative integer exponentiation closure laws.
Theorem	nnexpcl 6771	Closure of exponentiation of nonnegative integers.
|- ((A e. NN /\ N e. NN0) -> (A^N) e. NN)
Theorem	nn0expcl 6772	Closure of exponentiation of nonnegative integers.
|- ((A e. NN0 /\ N e. NN0) -> (A^N) e. NN0)
Theorem	zexpcl 6773	Closure of exponentiation of integers.
|- ((A e. ZZ /\ N e. NN0) -> (A^N) e. ZZ)
Theorem	qexpcl 6774	Closure of exponentiation of rationals.
|- ((A e. QQ /\ N e. NN0) -> (A^N) e. QQ)
Theorem	reexpcl 6775	Closure of exponentiation of reals.
|- ((A e. RR /\ N e. NN0) -> (A^N) e. RR)
Theorem	expcl 6776	Closure law for nonnegative integer exponentiation.
|- ((A e. CC /\ N e. NN0) -> (A^N) e. CC)
Theorem	rpexpcl 6777	Closure law for exponentiation of positive reals.
|- ((A e. RR+ /\ N e. NN0) -> (A^N) e. RR+)
Theorem	expm1t 6778	Exponentiation in terms of predecessor exponent.
|- ((A e. CC /\ N e. NN) -> (A^N) = ((A^(N - 1)) x. A))
Theorem	1exp 6779	Value of one raised to a nonnegative integer power.
|- (N e. NN0 -> (1^N) = 1)
Theorem	expeq0 6780	Natural number exponentiation is 0 iff its mantissa is 0.
|- ((A e. CC /\ N e. NN) -> ((A^N) = 0 <-> A = 0))
Theorem	expne0 6781	Natural number exponentiation is nonzero iff its mantissa is nonzero.
|- ((A e. CC /\ N e. NN) -> ((A^N) =/= 0 <-> A =/= 0))
Theorem	expne0i 6782	Nonnegative integer exponentiation is nonzero if its mantissa is nonzero.
|- ((A e. CC /\ A =/= 0 /\ N e. NN0) -> (A^N) =/= 0)
Theorem	expgt0 6783	Nonnegative integer exponentiation with a positive mantissa is positive.
|- ((A e. RR /\ N e. NN0 /\ 0 < A) -> 0 < (A^N))
Theorem	0exp 6784	Value of zero raised to a natural number power.
|- (N e. NN -> (0^N) = 0)
Theorem	expge0 6785	Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative.
|- ((A e. RR /\ N e. NN0 /\ 0 <_ A) -> 0 <_ (A^N))
Theorem	expgt1 6786	Natural number exponentiation with a mantissa greater than 1 is greater than 1.
|- ((A e. RR /\ N e. NN /\ 1 < A) -> 1 < (A^N))
Theorem	expge1 6787	Nonnegative integer exponentiation with a mantissa greater than or equal to 1 is greater than or equal to 1.
|- ((A e. RR /\ N e. NN0 /\ 1 <_ A) -> 1 <_ (A^N))
Theorem	mulexp 6788	Natural number exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents.
|- ((A e. CC /\ B e. CC /\ N e. NN0) -> ((A x. B)^N) = ((A^N) x. (B^N)))
Theorem	exprec 6789	Nonnegative integer exponentiation of a reciprocal.
|- ((A e. CC /\ A =/= 0 /\ N e. NN0) -> ((1 / A)^N) = (1 / (A^N)))
Theorem	exprecOLD 6790	Nonnegative integer exponentiation of a reciprocal.
|- ((A e. CC /\ N e. NN0 /\ A =/= 0) -> ((1 / A)^N) = (1 / (A^N)))
Theorem	expadd 6791	Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135.
|- ((A e. CC /\ M e. NN0 /\ N e. NN0) -> (A^(M + N)) = ((A^M) x. (A^N)))
Theorem	expmul 6792	Product of exponents law for natural number exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents.
|- ((A e. CC /\ M e. NN0 /\ N e. NN0) -> (A^(M x. N)) = ((A^M)^N))
Theorem	expsub 6793	Exponent subtraction law for nonnegative integer exponentiation.
|- ((((A e. CC /\ A =/= 0) /\ M e. NN0 /\ N e. NN0) /\ N <_ M) -> (A^(M - N)) = ((A^M) / (A^N)))
Theorem	expsubOLD 6794	Exponent subtraction law for nonnegative integer exponentiation.
|- (((A e. CC /\ M e. NN0 /\ N e. NN0) /\ (A =/= 0 /\ N <_ M)) -> (A^(M - N)) = ((A^M) / (A^N)))
Theorem	expm1 6795	Value of a complex number raised to a nonnegative integer power minus one.
|- ((A e. CC /\ A =/= 0 /\ N e. NN) -> (A^(N - 1)) = ((A^N) / A))
Theorem	expdiv 6796	Nonnegative integer exponentiation of a quotient.
|- ((A e. CC /\ (B e. CC /\ B =/= 0) /\ N e. NN0) -> ((A / B)^N) = ((A^N) / (B^N)))
Theorem	expordi 6797	Ordering relationship for exponentiation.
|- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 < A /\ M < N)) -> (A^M) < (A^N))
Theorem	expcan 6798	Cancellation law for exponentiation.
|- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ 1 < A) -> ((A^M) = (A^N) <-> M = N))
Theorem	expord 6799	Ordering law for exponentiation.
|- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ 1 < A) -> (M < N <-> (A^M) < (A^N)))
Theorem	expwordi 6800	Weak ordering relationship for exponentiation.
|- (((A e. RR /\ M e. NN0 /\ N e. NN0) /\ (1 <_ A /\ M <_ N)) -> (A^M) <_ (A^N))