mmtheorems74 - 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-10682

Statement List for Metamath Proof Explorer - 7301-7400 - Page 74 of 107

Type	Label	Description
Statement
Theorem	efaddlem4 7301	Lemma for efadd 7326. Real closure of the absolute value of the right-hand summation of efaddlem6 7303.
Theorem	efaddlem5 7302	Lemma for efadd 7326. Convert the truncated series for exp` (A + B) to a double summation using the binomial theorem binom 7028 and rearranging with fsum0diag2 7212.
Theorem	efaddlem6 7303	Lemma for efadd 7326. 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 7319. Warning: The HTML proof page is 0.6 megabyte in size.
Theorem	efaddlem7 7304	Lemma for efadd 7326. T is used to compute an upper bound for the numerator of the truncated series for exp` (A + B).
Theorem	efaddlem8 7305	Lemma for efadd 7326. T^S is used to compute an upper bound for the numerator of the truncated series for exp` (A + B).
Theorem	efaddlem9 7306	Lemma for efadd 7326. Properties of the index range for the summation on the right-hand side of efaddlem6 7303.
Theorem	efaddlem10 7307	Lemma for efadd 7326. Properties of A (or B) in the summation terms on the right-hand side of efaddlem6 7303.
Theorem	efaddlem11 7308	Lemma for efadd 7326. An upper bound for the numerator of the summation terms on the right-hand side of efaddlem6 7303.
Theorem	efaddlem12 7309	Lemma for efadd 7326. Further upper bound for the numerator of the summation terms on the right-hand side of efaddlem6 7303.
Theorem	efaddlem13 7310	Lemma for efadd 7326. Combine the bounds of efaddlem11 7308 and efaddlem12 7309.
Theorem	efaddlem14 7311	Lemma for efadd 7326. Importantly, the sum of the indices j and k of the double summation on the right-hand side of efaddlem6 7303 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 7312	Lemma for efadd 7326. A lower bound on the factorial product in the denominator of the summation terms on the right-hand side of efaddlem6 7303. The key theorem used is facavgt 6910, which says that the factorial of the average of two numbers is less than the product of their factorials.
Theorem	efaddlem16 7313	Lemma for efadd 7326. 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 7314	Lemma for efadd 7326. An upper bound for the summation terms on the right-hand side of efaddlem6 7303 that is independent of j and k.
Theorem	efaddlem18 7315	Lemma for efadd 7326. Closure of the double summation of the constant upper bound of efaddlem17 7314.
Theorem	efaddlem19 7316	Lemma for efadd 7326. Upper bound for the summation terms on the right-hand side of efaddlem6 7303.
Theorem	efaddlem20 7317	Lemma for efadd 7326. Further upper bound for the summation terms on the right-hand side of efaddlem6 7303.
Theorem	efaddlem21 7318	Lemma for efadd 7326. R will be part of our final upper bound for the summation on the right-hand side of efaddlem6 7303; importantly, R is independent of N.
Theorem	efaddlem22 7319	Lemma for efadd 7326. The final upper bound for the summation on the right-hand side of efaddlem6 7303. The key theorem used is faclbnd5 6908, 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 7320	Lemma for efadd 7326. 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 7321	Lemma for efadd 7326. Apply the Weak Deduction Theorem to efaddlem23 7320 to make N an antecedent.
Theorem	efaddlem25 7322	Lemma for efadd 7326. Convert from the explicit bound for N in efaddlem24 7321 to the existence of a bound m.
Theorem	efaddlem26 7323	Lemma for efadd 7326. Show that the sequence of partial sum products H converges to the product of exponentiations. The key theorem used is climmul 7082.
Theorem	efaddlem27 7324	Lemma for efadd 7326. Show that the convergence of the sequence of partial sum products H to exp` (A + B). The key theorem used is 2climnn 7057.
Theorem	efaddlem28 7325	Lemma for efadd 7326. The two expressions that H converges to are equal, since the limit of a converging series is unique by climunii 7053. The result is independent of H, which can therefore be eliminated with equid 1124 in the final theorem.
Theorem	efadd 7326	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	efaddt 7327	Sum of exponents law for exponential function.
|- ((A e. CC /\ B e. CC) -> (exp` (A + B)) = ((exp` A) x. (exp` B)))
Theorem	efcant 7328	Cancellation of law for exponential function. Equation 27 of [Rudin] p. 164.
|- (A e. CC -> ((exp` A) x. (exp` -uA)) = 1)
Theorem	efne0t 7329	The exponential function never vanishes. Corollary 15-4.3 of [Gleason] p. 309.
|- (A e. CC -> (exp` A) =/= 0)
Theorem	eff2 7330	The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008.)
|- exp:CC-->(CC \ {0})
Theorem	efsubt 7331	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	efexpt 7332	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	efnn0valt 7333	Value of the exponential function for nonnegative integers. Special case of efvalt 7268. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 16-Sep-2006.)
|- (N e. NN0 -> (exp` N) = (e^N))
Theorem	reeftclt 7334	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	eftabs 7335	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	eftlubclt 7336	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	eftlexOLD 7337	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	eftlext 7338	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	eftlclt 7339	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	reeftlclt 7340	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 7341	Lemma for ef1tlub 7342.
Theorem	ef1tlub 7342	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 7343	Lemma for ef01tlub 7345.
Theorem	ef01tllem2 7344	Lemma for ef01tlub 7345.
Theorem	ef01tlub 7345	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 7346	Lemma for absef01tlub 7347.
Theorem	absef01tlub 7347	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 7348	Lemma for eirr 7353.
Theorem	eirrlem2 7349	Lemma for eirr 7353.
Theorem	eirrlem3 7350	Lemma for eirr 7353.
Theorem	eirrlem4 7351	Lemma for eirr 7353.
Theorem	eirrlem5 7352	Lemma for eirr 7353.
Theorem	eirr 7353	e is irrational. (Contributed by Paul Chapman, 9-Feb-2008.)
|- e e/ QQ
The exponential, sine, and cosine functions (cont.)
Theorem	abspef01tlub 7354	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	efsep 7355	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	effsumle 7356	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	eft0val 7357	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	ef4p 7358	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	ef4pt 7359	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	efge1 7360	The exponenti