mmtheorems76 - 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 - 7501-7600 - Page 76 of 123

Type	Label	Description
Statement
Syntax	ccos 7501	Extend class notation to include the cosine function.
class cos
Syntax	cpi 7502	Extend class notation to include pi = 3.14159....
class pi
Definition	df-ef 7503	Define the exponential function.
|- exp = {<.x, y>. | (x e. CC /\ y = sum_k e. NN0 ((x^k) / (!` k)))}
Definition	df-e 7504	Define Euler's constant 2.71828....
|- e = (exp` 1)
Definition	df-sin 7505	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 7506	Define the cosine function.
|- cos = {<.x, y>. | (x e. CC /\ y = (((exp` (i x. x)) + (exp` (-ui x. x))) / 2))}
Definition	df-pi 7507	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	eftcl 7508	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 7509	Lemma for efcl 7517. The series that defines the exponential function converges, in the case where its argument is nonzero. The ratio test cvgrati 7460 is used to show convergence.
Theorem	efcltlem2 7510	Lemma for efcl 7517. The series defining the exponential function converges in the (trivial) case of a zero argument.
Theorem	efseq1ex 7511	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	dfef2i 7512	Switch between definitions for df-ef 7503 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	efval 7513	Value of the exponential function.
|- (A e. CC -> (exp` A) = sum_k e. NN0 ((A^k) / (!` k)))
Theorem	eval 7514	Value of Euler's constant e = 2.71828... (Contributed by Steve Rodriguez, 5-Mar-2006.)
|- e = sum_k e. NN0 (1 / (!` k))
Theorem	ef0lem 7515	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 7516	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	efcl 7517	Closure law for the exponential function.
|- (A e. CC -> (exp` A) e. CC)
Theorem	eff 7518	Domain and codomain of the exponential function. (Contributed by Paul Chapman, 22-Oct-2007.)
|- exp:CC-->CC
Theorem	efcvg 7519	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 7520	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 7521	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	reefcli 7522	Closure law for the exponential function with a real argument.
|- A e. RR   =>   |- (exp` A) e. RR
Theorem	reefcl 7523	The exponential function is real if its argument is real.
|- (A e. RR -> (exp` A) e. RR)
Theorem	erelem1 7524	Lemma for ereALT 7536.
Theorem	erelem2 7525	Lemma for ereALT 7536.
Theorem	erelem3 7526	Lemma for ereALT 7536.
Theorem	erelem4 7527	Lemma for ereALT 7536.
Theorem	erelem5 7528	Lemma for ereALT 7536.
Theorem	erelem6 7529	Lemma for ereALT 7536.
Theorem	erelem7 7530	Lemma for ereALT 7536.
Theorem	ele3lem 7531	Lemma for ele3 7538.
Theorem	ege2le3lem1 7532	Lemma for ege2le3 7539.
Theorem	ege2lem2 7533	Lemma for ege2 7537.
Theorem	ege2le3lem2 7534	Lemma for ege2le3 7539.
Theorem	ere 7535	Euler's constant e = 2.71828... is a real number. (Proof revised by Steve Rodriguez, 6-Mar-2006.)
|- e e. RR
Theorem	ereALT 7536	Euler's constant e = 2.71828... is a real number.
|- e e. RR
Theorem	ege2 7537	Euler's constant e = 2.71828... has a lower bound of 2.
|- 2 <_ e
Theorem	ele3 7538	Euler's constant e = 2.71828... has an upper bound of 3.
|- e <_ 3
Theorem	ege2le3 7539	Euler's constant e = 2.71828... is bounded by 2 and 3.
|- (2 <_ e /\ e <_ 3)
Theorem	ef0 7540	Value of the exponential function at 0. Equation 2 of [Gleason] p. 308. (Contributed by Steve Rodriguez, 27-Jun-2006.)
|- (exp` 0) = 1
Theorem	efcji 7541	Exponential function of a complex conjugate. Equation 3 of [Gleason] p. 308.
|- A e. CC   =>   |- (exp` (*` A)) = (*` (exp` A))
Theorem	efcj 7542	Exponential function of a complex conjugate. Equation 3 of [Gleason] p. 308.
|- (A e. CC -> (exp` (*` A)) = (*` (exp` A)))
Theorem	efaddlem1 7543	Lemma for efaddi 7571 (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 7544	Lemma for efaddi 7571. For later use, show that the lower bound of a summation index range that we will use is greater than zero.
Theorem	efaddlem3 7545	Lemma for efaddi 7571. Closure of the right-hand summation of efaddlem6 7548.
Theorem	efaddlem4 7546	Lemma for efaddi 7571. Real closure of the absolute value of the right-hand summation of efaddlem6 7548.
Theorem	efaddlem5 7547	Lemma for efaddi 7571. Convert the truncated series for exp` (A + B) to a double summation using the binomial theorem binomi 7275 and rearranging with fsum0diag2 7464.
Theorem	efaddlem6 7548	Lemma for efaddi 7571. 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 7564. Warning: The HTML proof page is 0.6 megabyte in size.
Theorem	efaddlem7 7549	Lemma for efaddi 7571. T is used to compute an upper bound for the numerator of the truncated series for exp` (A + B).
Theorem	efaddlem8 7550	Lemma for efaddi 7571. T^S is used to compute an upper bound for the numerator of the truncated series for exp` (A + B).
Theorem	efaddlem9 7551	Lemma for efaddi 7571. Properties of the index range for the summation on the right-hand side of efaddlem6 7548.
Theorem	efaddlem10 7552	Lemma for efaddi 7571. Properties of A (or B) in the summation terms on the right-hand side of efaddlem6 7548.
Theorem	efaddlem11 7553	Lemma for efaddi 7571. An upper bound for the numerator of the summation terms on the right-hand side of efaddlem6 7548.
Theorem	efaddlem12 7554	Lemma for efaddi 7571. Further upper bound for the numerator of the summation terms on the right-hand side of efaddlem6 7548.
Theorem	efaddlem13 7555	Lemma for efaddi 7571. Combine the bounds of efaddlem11 7553 and efaddlem12 7554.
Theorem	efaddlem14 7556	Lemma for efaddi 7571. Importantly, the sum of the indices j and k of the double summation on the right-hand side of efaddlem6 7548 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 7557	Lemma for efaddi 7571. A lower bound on the factorial product in the denominator of the summation terms on the right-hand side of efaddlem6 7548. The key theorem used is facavg 7158, which says that the factorial of the average of two numbers is less than the product of their factorials.
Theorem	efaddlem16 7558	Lemma for efaddi 7571. 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 7559	Lemma for efaddi 7571. An upper bound for the summation terms on the right-hand side of efaddlem6 7548 that is independent of j and k.
Theorem	efaddlem18 7560	Lemma for efaddi 7571. Closure of the double summation of the constant upper bound of efaddlem17 7559.
Theorem	efaddlem19 7561	Lemma for efaddi 7571. Upper bound for the summation terms on the right-hand side of efaddlem6 7548.
Theorem	efaddlem20 7562	Lemma for efaddi 7571. Further upper bound for the summation terms on the right-hand side of efaddlem6 7548.
Theorem	efaddlem21 7563	Lemma for efaddi 7571. R will be part of our final upper bound for the summation on the right-hand side of efaddlem6 7548; importantly, R is independent of N.
Theorem	efaddlem22 7564	Lemma for efaddi 7571. The final upper bound for the summation on the right-hand side of efaddlem6 7548. The key theorem used is faclbnd5 7156, 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 7565	Lemma for efaddi 7571. 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 7566	Lemma for efaddi 7571. Apply the Weak Deduction Theorem to efaddlem23 7565 to make N an antecedent.
Theorem	efaddlem25 7567	Lemma for efaddi 7571. Convert from the explicit bound for N in efaddlem24 7566 to the existence of a bound m.
Theorem	efaddlem26 7568	Lemma for efaddi 7571. Show that the sequence of partial sum products H converges to the product of exponentiations. The key theorem used is climmul 7331.
Theorem	efaddlem27 7569	Lemma for efaddi 7571. Show that the convergence of the sequence of partial sum products H to exp` (A + B). The key theorem used is 2climnn 7305.
Theorem	efaddlem28 7570	Lemma for efaddi 7571. The two expressions that H converges to are equal, since the limit of a converging series is unique by climunii 7301. The result is independent of H, which can therefore be eliminated with equid 1162 in the final theorem.
Theorem	efaddi 7571	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 7572	Sum of exponents law for exponential function.
|- ((A e. CC /\ B e. CC) -> (exp` (A + B)) = ((exp` A) x. (exp` B)))
Theorem	efcan 7573	Cancellation of law for exponential function. Equation 27 of [Rudin] p. 164.
|- (A e. CC -> ((exp` A) x. (exp` -uA)) = 1)
Theorem	efne0 7574	The exponential function never vanishes. Corollary 15-4.3 of [Gleason] p. 309.
|- (A e. CC -> (exp` A) =/= 0)
Theorem	eff2 7575	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 7576	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 7577	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 7578	Value of the exponential function for nonnegative integers. Special case of efval 7513. Equation 30 of [Rudin] p. 164. (Contributed by Steve Rodriguez, 16-Sep-2006.)
|- (N e. NN0 -> (exp` N) = (e^N))
Theorem	reeftcl 7579	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 7580	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 7581	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 7582	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 7583	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 7584	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 7585	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 7586	Lemma for ef1tlubi 7587.
Theorem	ef1tlubi 7587	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 7588	Lemma for ef01tlubi 7591.
Theorem	ef01tllem2 7589	Lemma for ef01tlubi 7591.
Theorem	ef01tllem2OLD 7590	Lemma for ef01tlubi 7591.
Theorem	ef01tlubi 7591	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 7592	Lemma for absef01tlubi 7593.
Theorem	absef01tlubi 7593	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 7594	Lemma for eirr 7599.
Theorem	eirrlem2 7595	Lemma for eirr 7599.
Theorem	eirrlem3 7596	Lemma for eirr 7599.
Theorem	eirrlem4 7597	Lemma for eirr 7599.
Theorem	eirrlem5 7598	Lemma for eirr 7599.
Theorem	eirr 7599	e is irrational. (Contributed by Paul Chapman, 9-Feb-2008.)
|- e e/ QQ
Theorem	egt2OLD 7600	Euler's constant e = 2.71828... is greater than 2.
|- 2 < e