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-10700 108 10701-10766

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

Type	Label	Description
Statement
Theorem	ivthlem8 7301	Lemma for isupivth 7303.
Theorem	ivthlem9 7302	Lemma for isupivth 7303.
Theorem	isupivth 7303	The intermediate value theorem, increasing case with supremum solution. (Contributed by Paul Chapman, 22-Jan-2008.)
|- A e. RR   &   |- B e. RR   &   |- U e. RR   &   |- A < B   &   |- (A[,]B) (_ D   &   |- D (_ CC   &   |- F e. (D-cn->CC)   &   |- (x e. (A[,]B) -> (F` x) e. RR)   &   |- S = {x e. (A[,]B) | (F` x) = U}   &   |- ((F` A) < U /\ U < (F` B))   &   |- C = sup(S, RR, < )   =>   |- (C e. (A(,)B) /\ (F` C) = U)
Theorem	dsupivthlem 7304	Lemma for dsupivth 7305.
Theorem	dsupivth 7305	The intermediate value theorem, decreasing case with supremum solution. (Contributed by Paul Chapman, 22-Jan-2008.)
|- A e. RR   &   |- B e. RR   &   |- U e. RR   &   |- A < B   &   |- (A[,]B) (_ D   &   |- D (_ CC   &   |- F e. (D-cn->CC)   &   |- (x e. (A[,]B) -> (F` x) e. RR)   &   |- S = {x e. (A[,]B) | (F` x) = U}   &   |- ((F` B) < U /\ U < (F` A))   &   |- C = sup(S, RR, < )   =>   |- (C e. (A(,)B) /\ (F` C) = U)
The exponential, sine, and cosine functions
Syntax	ce 7306	Extend class notation to include the exponential function.
class exp
Syntax	ceu 7307	Extend class notation to include Euler's constant = 2.7182818....
class e
Syntax	csin 7308	Extend class notation to include the sine function.
class sin
Syntax	ccos 7309	Extend class notation to include the cosine function.
class cos
Syntax	cpi 7310	Extend class notation to include pi = 3.14159....
class pi
Definition	df-ef 7311	Define the exponential function.
|- exp = {<.x, y>. | (x e. CC /\ y = sum_k e. NN0 ((x^k) / (!` k)))}
Definition	df-e 7312	Define Euler's constant 2.71828....
|- e = (exp` 1)
Definition	df-sin 7313	Define the sine function.
|- sin = {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) - (exp` (-ui x. x))) / (2 x. i)))}
Definition	df-cos 7314	Define the cosine function.
|- cos = {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) + (exp` (-ui x. x))) / 2))}
Definition	df-pi 7315	Define pi = 3.14159..., which is the smallest positive number whose sine is zero. Definition of pi in [Gleason] p. 311. (We use the inverse of of less-than, "`' <", to turn supremum into infimum; currently we don't have infimum defined separately.)
|- pi = sup({x e. RR | (0 < x /\ (sin` x) = 0)}, RR, `' < )
Theorem	eftclt 7316	Closure of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 11-Sep-2007.)
|- ((A e. CC /\ K e. NN0) -> ((A^K) / (!` K)) e. CC)
Theorem	efcltlem1 7317	Lemma for efclt 7325. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrat 7268 is used to show convergence.
Theorem	efcltlem2 7318	Lemma for efclt 7325. The series defining the exponential function converges in the (trivial) case of a zero argument.
Theorem	efseq1ex 7319	The series defining the exponential function converges.
|- F = {<.y, z>. | (y e. NN /\ z = ((A^y) / (!` y)))}   =>   |- (A e. CC -> E.x( + seq1 F) ~~> x)
Theorem	dfef2 7320	Switch between definitions for df-ef 7311 that sum over NN0 or over NN. (Contributed by Steve Rodriguez, 30-Jun-2006.)
|- A e. CC   =>   |- sum_k e. NN0 ((A^k) / (!` k)) = (1 + sum_k e. NN ({<.j, y>. | (j e. NN /\ y = ((A^j) / (!` j)))}` k))
Theorem	efvalt 7321	Value of the exponential function.
|- (A e. CC -> (exp` A) = sum_k e. NN0 ((A^k) / (!` k)))
Theorem	eval 7322	Value of Euler's constant e = 2.71828... (Contributed by Steve Rodriguez, 5-Mar-2006.)
|- e = sum_k e. NN0 (1 / (!` k))
Theorem	ef0lem 7323	The series defining the exponential function converges in the (trivial) case of a zero argument.
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- (A = 0 -> ( + seq0 F) ~~> 1)
Theorem	efseq0ex 7324	The series defining the exponential function converges.
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- (A e. CC -> E.x( + seq0 F) ~~> x)
Theorem	efclt 7325	Closure law for the exponential function.
|- (A e. CC -> (exp` A) e. CC)
Theorem	eff 7326	Domain and codomain of the exponential function. (Contributed by Paul Chapman, 22-Oct-2007.)
|- exp:CC-->CC
Theorem	efcvg 7327	The series that defines the exponential function converges to it.
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- (A e. CC -> ( + seq0 F) ~~> (exp` A))
Theorem	efcvgfsum 7328	Exponential function convergence in terms of a sequence of partial finite sums.
|- F = {<.n, y>. | (n e. NN0 /\ y = sum_k e. (0...n)((A^k) / (!` k)))}   =>   |- (A e. CC -> F ~~> (exp` A))
Theorem	eftval 7329	The value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 21-Aug-2007.)
|- F = {<.j, y>. | (j e. NN0 /\ y = ((A^j) / (!` j)))}   =>   |- (N e. NN0 -> (F` N) = ((A^N) / (!` N)))
Theorem	reefcl 7330	Closure law for the exponential function with a real argument.
|- A e. RR   =>   |- (exp` A) e. RR
Theorem	reefclt 7331	The exponential function is real if its argument is real.
|- (A e. RR -> (exp` A) e. RR)
Theorem	erelem1 7332	Lemma for ereALT 7344.
Theorem	erelem2 7333	Lemma for ereALT 7344.
Theorem	erelem3 7334	Lemma for ereALT 7344.
Theorem	erelem4 7335	Lemma for ereALT 7344.
Theorem	erelem5 7336	Lemma for ereALT 7344.
Theorem	erelem6 7337	Lemma for ereALT 7344.
Theorem	erelem7 7338	Lemma for ereALT 7344.
Theorem	ele3lem 7339	Lemma for ele3 7346.
Theorem	ege2le3lem1 7340	Lemma for ege2le3 7347.
Theorem	ege2lem2 7341	Lemma for ege2 7345.
Theorem	ege2le3lem2 7342	Lemma for ege2le3 7347.
Theorem	ere 7343	Euler's constant e = 2.71828... is a real number. (Proof revised by Steve Rodriguez, 6-Mar-2006.)
|- e e. RR
Theorem	ereALT 7344	Euler's constant e = 2.71828... is a real number.
|- e e. RR
Theorem	ege2 7345	Euler's constant e = 2.71828... has a lower bound of 2.
|- 2 <_ e
Theorem	ele3 7346	Euler's constant e = 2.71828... has an upper bound of 3.
|- e <_ 3
Theorem	ege2le3 7347	Euler's constant e = 2.71828... is bounded by 2 and 3.
|- (2 <_ e /\ e <_ 3)
Theorem	ef0 7348	Value of the exponential function at 0. Equation 2 of [Gleason] p. 308. (Contributed by Steve Rodriguez, 27-Jun-2006.)
|- (exp` 0) = 1
Theorem	efcj 7349	Exponential function of a complex conjugate. Equation 3 of [Gleason] p. 308.
|- A e. CC   =>   |- (exp` (*` A)) = (*` (exp` A))
Theorem	efcjt 7350	Exponential function of a complex conjugate. Equation 3 of [Gleason] p. 308.
|- (A e. CC -> (exp` (*` A)) = (*` (exp` A)))
Theorem	efaddlem1 7351	Lemma for efadd 7379 (exponential function addition law). Technical result for later use. Note: if you want to see these lemmas in the Statement List summary, change the first word "Lemma" to "- Lemma" and re-run the "write th" command.
Theorem	efaddlem2 7352	Lemma for efadd 7379. For later use, show that the lower bound of a summation index range that we will use is greater than zero.
Theorem	efaddlem3 7353	Lemma for efadd 7379. Closure of the right-hand summation of efaddlem6 7356.
Theorem	efaddlem4 7354	Lemma for efadd 7379. Real closure of the absolute value of the right-hand summation of efaddlem6 7356.
Theorem	efaddlem5 7355	Lemma for efadd 7379. Convert the truncated series for exp` (A + B) to a double summation using the binomial theorem binom 7085 and rearranging with fsum0diag2 7272.
Theorem	efaddlem6 7356	Lemma for efadd 7379. 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 7372. Warning: The HTML proof page is 0.6 megabyte in size.
Theorem	efaddlem7 7357	Lemma for efadd 7379. T is used to compute an upper bound for the numerator of the truncated series for exp` (A + B).
Theorem	efaddlem8 7358	Lemma for efadd 7379. T^S is used to compute an upper bound for the numerator of the truncated series for exp` (A + B).
Theorem	efaddlem9 7359	Lemma for efadd 7379. Properties of the index range for the summation on the right-hand side of efaddlem6 7356.
Theorem	efaddlem10 7360	Lemma for efadd 7379. Properties of A (or B) in the summation terms on the right-hand side of efaddlem6 7356.
Theorem	efaddlem11 7361	Lemma for efadd 7379. An upper bound for the numerator of the summation terms on the right-hand side of efaddlem6 7356.
Theorem	efaddlem12 7362	Lemma for efadd 7379. Further upper bound for the numerator of the summation terms on the right-hand side of efaddlem6 7356.
Theorem	efaddlem13 7363	Lemma for efadd 7379. Combine the bounds of efaddlem11 7361 and efaddlem12 7362.
Theorem	efaddlem14 7364	Lemma for efadd 7379. Importantly, the sum of the indices j and k of the double summation on the right-hand side of efaddlem6 7356 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 7365	Lemma for efadd 7379. A lower bound on the factorial product in the denominator of the summation terms on the right-hand side of efaddlem6 7356. The key theorem used is facavgt 6968, which says that the factorial of the average of two numbers is less than the product of their factorials.
Theorem	efaddlem16 7366	Lemma for efadd 7379. 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 7367	Lemma for efadd 7379. An upper bound for the summation terms on the right-hand side of efaddlem6 7356 that is independent of j and k.
Theorem	efaddlem18 7368	Lemma for efadd 7379. Closure of the double summation of the constant upper bound of efaddlem17 7367.
Theorem	efaddlem19 7369	Lemma for efadd 7379. Upper bound for the summation terms on the right-hand side of efaddlem6 7356.
Theorem	efaddlem20 7370	Lemma for efadd 7379. Further upper bound for the summation terms on the right-hand side of efaddlem6 7356.
Theorem	efaddlem21 7371	Lemma for efadd 7379. R will be part of our final upper bound for the summation on the right-hand side of efaddlem6 7356; importantly, R is independent of N.
Theorem	efaddlem22 7372	Lemma for efadd 7379. The final upper bound for the summation on the right-hand side of efaddlem6 7356. The key theorem used is faclbnd5 6966, 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 7373	Lemma for efadd 7379. 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 7374	Lemma for efadd 7379. Apply the Weak Deduction Theorem to efaddlem23 7373 to make N an antecedent.
Theorem	efaddlem25 7375	Lemma for efadd 7379. Convert from the explicit bound for N in efaddlem24 7374 to the existence of a bound m.
Theorem	efaddlem26 7376	Lemma for efadd 7379. Show that the sequence of partial sum products H converges to the product of exponentiations. The key theorem used is climmul 7141.
Theorem	efaddlem27 7377	Lemma for efadd 7379. Show that the convergence of the sequence of partial sum products H to exp` (A + B). The key theorem used is 2climnn 7115.
Theorem	efaddlem28 7378	Lemma for efadd 7379. The two expressions that H converges to are equal, since the limit of a converging series is unique by climunii 7111. The result is independent of H, which can therefore be eliminated with equid 1129 in the final theorem.
Theorem	efadd 7379	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 7380	Sum of exponents law for exponential function.
|- ((A e. CC /\ B e. CC) -> (exp` (A + B)) = ((exp` A) x. (exp` B)))
Theorem	efcant 7381	Cancellation of law for exponential function. Equation 27 of [Rudin] p. 164.
|- (A e. CC -> ((exp` A) x. (exp` -uA)) = 1)
Theorem	efne0t 7382	The exponential function never vanishes. Corollary 15-4.3 of [Gleason] p. 309.
|- (A e. CC -> (exp` A) =/= 0)
Theorem	eff2 7383	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 7384	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 7385