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-10687

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

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