mmtheorems87 - 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-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Statement List for Metamath Proof Explorer - 8601-8700 - Page 87 of 175

Type	Label	Description
Statement
Theorem	efaddlem2 8601	Lemma for efaddi 8628. For later use, show that the lower bound of a summation index range that we will use is greater than zero.
Theorem	efaddlem3 8602	Lemma for efaddi 8628. Closure of the right-hand summation of efaddlem6 8605.
Theorem	efaddlem4 8603	Lemma for efaddi 8628. Real closure of the absolute value of the right-hand summation of efaddlem6 8605.
Theorem	efaddlem5 8604	Lemma for efaddi 8628. Convert the truncated series for exp` (A + B) to a double summation using the binomial theorem binomi 8332 and rearranging with fsum0diag2 8521.
Theorem	efaddlem6 8605	Lemma for efaddi 8628. Compute the difference between the truncated series for (exp` A) x. (exp` B) and exp` (A + B). A main goal of the proof is to show that this difference goes to zero as N approaches infinity; this is finally accomplished in efaddlem22 8621. Warning: The HTML proof page is 0.6 megabyte in size.
Theorem	efaddlem7 8606	Lemma for efaddi 8628. T is used to compute an upper bound for the numerator of the truncated series for exp` (A + B).
Theorem	efaddlem8 8607	Lemma for efaddi 8628. T^S is used to compute an upper bound for the numerator of the truncated series for exp` (A + B).
Theorem	efaddlem9 8608	Lemma for efaddi 8628. Properties of the index range for the summation on the right-hand side of efaddlem6 8605.
Theorem	efaddlem10 8609	Lemma for efaddi 8628. Properties of A (or B) in the summation terms on the right-hand side of efaddlem6 8605.
Theorem	efaddlem11 8610	Lemma for efaddi 8628. An upper bound for the numerator of the summation terms on the right-hand side of efaddlem6 8605.
Theorem	efaddlem12 8611	Lemma for efaddi 8628. Further upper bound for the numerator of the summation terms on the right-hand side of efaddlem6 8605.
Theorem	efaddlem13 8612	Lemma for efaddi 8628. Combine the bounds of efaddlem11 8610 and efaddlem12 8611.
Theorem	efaddlem14 8613	Lemma for efaddi 8628. Importantly, the sum of the indices j and k of the double summation on the right-hand side of efaddlem6 8605 is larger than N. This will be used to find a lower bound on the factorials in the denominator of the summation terms.
Theorem	efaddlem15 8614	Lemma for efaddi 8628. A lower bound on the factorial product in the denominator of the summation terms on the right-hand side of efaddlem6 8605. The key theorem used is facavg 8207, which says that the factorial of the average of two numbers is less than the product of their factorials.
Theorem	efaddlem16 8615	Lemma for efaddi 8628. The double summation of a constant C (that is independent of j and k) has an upper bound that grows as the square of N.
Theorem	efaddlem17 8616	Lemma for efaddi 8628. An upper bound for the summation terms on the right-hand side of efaddlem6 8605 that is independent of j and k.
Theorem	efaddlem18 8617	Lemma for efaddi 8628. Closure of the double summation of the constant upper bound of efaddlem17 8616.
Theorem	efaddlem19 8618	Lemma for efaddi 8628. Upper bound for the summation terms on the right-hand side of efaddlem6 8605.
Theorem	efaddlem20 8619	Lemma for efaddi 8628. Further upper bound for the summation terms on the right-hand side of efaddlem6 8605.
Theorem	efaddlem21 8620	Lemma for efaddi 8628. R will be part of our final upper bound for the summation on the right-hand side of efaddlem6 8605; importantly, R is independent of N.
Theorem	efaddlem22 8621	Lemma for efaddi 8628. The final upper bound for the summation on the right-hand side of efaddlem6 8605. The key theorem used is faclbnd5 8205, which shows that the factorial grows faster than powers. As the number of terms N grows to infinity, the sum shrinks to zero, since R is independent of N.
Theorem	efaddlem23 8622	Lemma for efaddi 8628. Given any positive x, no matter how small, there is an N such that the difference between the truncated series for (exp` A) x. (exp` B) and exp` (A + B) is less than x. Here we show an explicit lower bound for N.
Theorem	efaddlem24 8623	Lemma for efaddi 8628. Apply the Weak Deduction Theorem to efaddlem23 8622 to make N an antecedent.
Theorem	efaddlem25 8624	Lemma for efaddi 8628. Convert from the explicit bound for N in efaddlem24 8623 to the existence of a bound m.
Theorem	efaddlem26 8625	Lemma for efaddi 8628. Show that the sequence of partial sum products H converges to the product of exponentiations. The key theorem used is climmul 8388.
Theorem	efaddlem27 8626	Lemma for efaddi 8628. Show that the convergence of the sequence of partial sum products H to exp` (A + B). The key theorem used is 2climnn 8362.
Theorem	efaddlem28 8627	Lemma for efaddi 8628. The two expressions that H converges to are equal, since the limit of a converging series is unique by climunii 8358. The result is independent of H, which can therefore be eliminated with equid 1484 in the final theorem.
Theorem	efaddi 8628	Sum of exponents law for exponential function. Equation 26 of [Rudin] p. 164.
|- A e. CC   &   |- B e. CC   =>   |- (exp` (A + B)) = ((exp` A) x. (exp` B))
Theorem	efadd 8629	Sum of exponents law for exponential function.
|- ((A e. CC /\ B e. CC) -> (exp` (A + B)) = ((exp` A) x. (exp` B)))
Theorem	efcan 8630	Cancellation of law for exponential function. Equation 27 of [Rudin] p. 164.
|- (A e. CC -> ((exp` A) x. (exp` -uA)) = 1)
Theorem	efne0 8631	The exponential function never vanishes. Corollary 15-4.3 of [Gleason] p. 309.
|- (A e. CC -> (exp` A) =/= 0)
Theorem	eff2 8632	The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
|- exp:CC-->(CC \ {0})
Theorem	efsub 8633	Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ((A e. CC /\ B e. CC) -> (exp` (A - B)) = ((exp` A) / (exp` B)))
Theorem	efexp 8634	Exponential function to a nonnegative integer power. Corollary 15-4.4 of [Gleason] p. 309, restricted to nonnegative integers.
|- ((A e. CC /\ N e. NN0) -> (exp` (N x. A)) = ((exp` A)^N))
Theorem	efnn0val 8635	Value of the exponential function for nonnegative integers. Special case of efval 8570. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 16-Sep-2006.)
|- (N e. NN0 -> (exp` N) = (_e^N))
Theorem	reeftcl 8636	The terms of the series expansion of the exponential function of a real number are real. (Contributed by Paul Chapman, 15-Jan-2008.)
|- ((A e. RR /\ K e. NN0) -> ((A^K) / (!` K)) e. RR)
Theorem	eftabsi 8637	The absolute value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 23-Nov-2007.)
|- A e. CC   =>   |- (K e. NN0 -> (abs` ((A^K) / (!` K))) = (((abs` A)^K) / (!` K)))
Theorem	eftlubcl 8638	Closure of the upper bound of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008.)
|- (M e. NN -> ((M + 1) / ((!` M) x. M)) e. RR)
Theorem	eftlexiOLD 8639	An upper part of the series defining the exponential function converges. (Contributed by Paul Chapman, 23-Nov-2007.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   &   |- A e. CC   =>   |- (N e. NN -> E.x(<.N, + >. seq F) ~~> x)
Theorem	eftlex 8640	An infinite tail of the series defining the exponential function converges. (Contributed by Paul Chapman, 17-Jan-2008.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- ((A e. CC /\ M e. NN) -> E.x(<.M, + >. seq F) ~~> x)
Theorem	eftlcl 8641	Closure of the sum of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- ((A e. CC /\ M e. NN) -> sum_k e. (ZZ>=` M)(F` k) e. CC)
Theorem	reeftlcl 8642	Closure of the sum of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- ((A e. RR /\ M e. NN) -> sum_k e. (ZZ>=` M)(F` k) e. RR)
Theorem	ef1tllem 8643	Lemma for ef1tlubi 8644.
Theorem	ef1tlubi 8644	An upper bound on the infinite tail of the series expansion of the exponential function at 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- ((M e. NN /\ A = 1) -> sum_k e. (ZZ>=` M)(F` k) <_ ((M + 1) / ((!` M) x. M)))
Theorem	ef01tllem1 8645	Lemma for ef01tlubi 8648.
Theorem	ef01tllem2 8646	Lemma for ef01tlubi 8648.
Theorem	ef01tllem2OLD 8647	Lemma for ef01tlubi 8648.
Theorem	ef01tlubi 8648	An upper bound on the infinite tail of the series expansion of the exponential function on the positive reals less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- ((A e. (0(,]1) /\ M e. NN) -> sum_k e. (ZZ>=` M)(F` k) <_ ((A^M) x. ((M + 1) / ((!` M) x. M))))
Theorem	absef01tllem 8649	Lemma for absef01tlubi 8650.
Theorem	absef01tlubi 8650	An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the punctured closed unit disk. (Contributed by Paul Chapman, 19-Jan-2008.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- ((A e. CC /\ (abs` A) e. (0(,]1) /\ M e. NN) -> (abs` sum_k e. (ZZ>=` M)(F` k)) <_ (((abs` A)^M) x. ((M + 1) / ((!` M) x. M))))
_e is irrational
Theorem	eirrlem1 8651	Lemma for eirr 8656.
Theorem	eirrlem2 8652	Lemma for eirr 8656.
Theorem	eirrlem3 8653	Lemma for eirr 8656.
Theorem	eirrlem4 8654	Lemma for eirr 8656.
Theorem	eirrlem5 8655	Lemma for eirr 8656.
Theorem	eirr 8656	_e is irrational. (Contributed by Paul Chapman, 9-Feb-2008.)
|- _e e/ QQ
Theorem	egt2OLD 8657	Euler's constant _e = 2.71828... is greater than 2.
|- 2 < _e
Theorem	elt3OLD 8658	Euler's constant _e = 2.71828... is less than 3.
|- _e < 3
Theorem	egt2lt3 8659	Euler's constant _e = 2.71828... is bounded by 2 and 3.
|- (2 < _e /\ _e < 3)
The exponential, sine, and cosine functions (cont.)
Theorem	abspef01tlubi 8660	An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the punctured closed unit disc projected onto the real or imaginary axis. (Contributed by Paul Chapman, 19-Jan-2008.)
|- F = {<.j, y>. | (j e. NN0 /\ y = (((_i x. A)^j) / (!` j)))}   &   |- (P = Re \/ P = Im)   =>   |- ((A e. (0(,]1) /\ M e. NN) -> (abs` (P` sum_k e. (ZZ>=` M)(F` k))) <_ ((A^M) x. ((M + 1) / ((!` M) x. M))))
Theorem	efsepi 8661	Separate out the next term of the power series expansion of the exponential function. The last hypothesis allows the separated terms to be rearranged as desired. (Contributed by Paul Chapman, 23-Nov-2007.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   &   |- A e. CC   &   |- M e. NN0   &   |- B e. CC   &   |- (exp` A) = (B + sum_k e. (ZZ>=` M)(F` k))   &   |- (F` M) = C   &   |- N = (M + 1)   &   |- D = (B + C)   =>   |- (exp` A) = (D + sum_k e. (ZZ>=` N)(F` k))
Theorem	effsumlei 8662	The partial sums of the series expansion of the exponential function of a nonnegative real number are bounded by the value of the function. (Contributed by Paul Chapman, 21-Aug-2007.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   &   |- A e. RR   &   |- N e. NN0   =>   |- (0 <_ A -> (( + seq0 F)` N) <_ (exp` A))
Theorem	eft0vali 8663	The value of the first term of the series expansion of the exponential function is 1. (Contributed by Paul Chapman, 21-Aug-2007.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   &   |- A e. CC   =>   |- (F` 0) = 1
Theorem	ef4pi 8664	Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   &   |- A e. CC   =>   |- (exp` A) = ((((1 + A) + ((A^2) / 2)) + ((A^3) / 6)) + sum_k e. (ZZ>=` 4)(F` k))
Theorem	ef4p 8665	Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- (A e. CC -> (exp` A) = ((((1 + A) + ((A^2) / 2)) + ((A^3) / 6)) + sum_k e. (ZZ>=` 4)(F` k)))
Theorem	efge1i 8666	The exponential function of a nonnegative real number is greater than or equal to 1. (Contributed by Paul Chapman, 21-Aug-2007.)
|- A e. RR   =>   |- (0 <_ A -> 1 <_ (exp` A))
Theorem	efge1pi 8667	The exponential function of a nonnegative real number is greater than or equal to 1 plus that number. (Contributed by Paul Chapman, 18-Oct-2007.)
|- A e. RR   =>   |- (0 <_ A -> (1 + A) <_ (exp` A))
Theorem	efgt1i 8668	The exponential function of a positive real number is greater than 1. (Contributed by Paul Chapman, 21-Aug-2007.)
|- A e. RR   =>   |- (0 < A -> 1 < (exp` A))
Theorem	efgt0i 8669	The exponential function of a real number is greater than 0. (Contributed by Paul Chapman, 21-Aug-2007.)
|- A e. RR   =>   |- 0 < (exp` A)
Theorem	efgt0 8670	The exponential function of a real number is greater than 0. (Contributed by Paul Chapman, 13-Sep-2007.)
|- (A e. RR -> 0 < (exp` A))
Theorem	eflti 8671	The exponential function on the reals is strictly monotonic. (Contributed by Paul Chapman, 21-Aug-2007.)
|- A e. RR   &   |- B e. RR   =>   |- (A < B -> (exp` A) < (exp` B))
Theorem	efltbi 8672	The exponential function on the reals is strictly monotonic. (Contributed by Steve Rodriguez, 22-Aug-2007.)
|- A e. RR   &   |- B e. RR   =>   |- (A < B <-> (exp` A) < (exp` B))
Theorem	reef11i 8673	The exponential function on real numbers is one-to-one. (Contributed by Steve Rodriguez, 25-Aug-2007.)
|- A e. RR   &   |- B e. RR   =>   |- ((exp` A) = (exp` B) <-> A = B)
Theorem	reef11 8674	The exponential function on real numbers is one-to-one.
|- ((A e. RR /\ B e. RR) -> ((exp` A) = (exp` B) <-> A = B))
Theorem	reeff1 8675	The exponential function maps real arguments one-to-one to positive reals. (Contributed by Steve Rodriguez, 25-Aug-2007.)
|- (exp |` RR):RR-1-1->(0(,) +oo)
Theorem	efm1limi 8676	Series convergence to the exponential function minus 1. (Contributed by Paul Chapman, 11-Sep-2007.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   &   |- A e. CC   =>   |- (<.1, + >. seq F) ~~> ((exp` A) - 1)
Theorem	absefm1lei 8677	The absolute value of the exponential function minus 1 is less than or equal to the exponential function minus 1 of the absolute value. (Contributed by Paul Chapman, 11-Sep-2007.)
|- A e. CC   =>   |- (abs` ((exp` A) - 1)) <_ ((exp` (abs` A)) - 1)
Theorem	eflegeolem1 8678	Lemma for eflegeoi 8680.
Theorem	eflegeolem2 8679	Lemma for eflegeoi 8680.
Theorem	eflegeoi 8680	The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007.)
|- A e. RR   &   |- (0 <_ A /\ A < 1)   =>   |- (exp` A) <_ (1 / (1 - A))
Theorem	eflegeo 8681	The exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 11-Sep-2007.)
|- ((A e. RR /\ 0 <_ A /\ A < 1) -> (exp` A) <_ (1 / (1 - A)))
Theorem	efm1legeoi 8682	One less than the exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 15-Sep-2007.)
|- A e. RR   &   |- (0 <_ A /\ A < 1)   =>   |- ((exp` A) - 1) <_ (A / (1 - A))
Theorem	efm1legeo 8683	One less than the exponential function on the reals between 0 and 1 lies below the comparable geometric series sum. (Contributed by Paul Chapman, 15-Sep-2007.)
|- ((A e. RR /\ 0 <_ A /\ A < 1) -> ((exp` A) - 1) <_ (A / (1 - A)))
Theorem	efcnlem1 8684	Lemma for efcn 8688.
Theorem	efcnlem2 8685	Lemma for efcn 8688.
Theorem	efcnlem3 8686	Lemma for efcn 8688.
Theorem	efcnlem4 8687	Lemma for efcn 8688.
Theorem	efcn 8688	The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007.)
|- exp e. (CC-cn->CC)
Theorem	reeff1olem1 8689	Lemma for reeff1o 8691.
Theorem	reeff1olem2 8690	Lemma for reeff1o 8691.
Theorem	reeff1o 8691	The real exponential function is one-to-one onto. (Contributed by Paul Chapman, 18-Oct-2007.)
|- (exp |` RR):RR-1-1-onto->(0(,) +oo)
Theorem	reeff1o2 8692	The real exponential function is one-to-one onto. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- (exp |` RR):RR-1-1-onto->RR+
Theorem	reefiso 8693	The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- (exp |` RR) Isom < , < (RR, RR+)
Theorem	sinval 8694	Value of the sine function.
|- (A e. CC -> (sin` A) = (((exp` (_i x. A)) - (exp` (-u_i x. A))) / (2 x. _i)))
Theorem	cosval 8695	Value of the cosine function.
|- (A e. CC -> (cos` A) = (((exp` (_i x. A)) + (exp` (-u_i x. A))) / 2))
Theorem	sincl 8696	Closure of the sine function.
|- (A e. CC -> (sin` A) e. CC)
Theorem	coscl 8697	Closure of the cosine function with a complex argument.
|- (A e. CC -> (cos` A) e. CC)
Theorem	resinval 8698	The sine of a real number in terms of the exponential function.
|- (A e. RR -> (sin` A) = (Im` (exp` (_i x. A))))
Theorem	recosval 8699	The cosine of a real number in terms of the exponential function.
|- (A e. RR -> (cos` A) = (Re` (exp` (_i x. A))))
Theorem	efi4p 8700	Separate out the first four terms of the infinite series expansion of the exponential function of a pure imaginary number. (Contributed by Paul Chapman, 19-Jan-2008.)
|- F = {<.j, y>. | (j e. NN0 /\ y = (((_i x. A)^j) / (!` j)))}   =>   |- (A e. RR -> (exp` (_i x. A)) = (((1 - ((A^2) / 2)) + (_i x. (A - ((A^3) / 6)))) + sum_k e. (ZZ>=` 4)(F` k)))