Home | Metamath
Proof Explorer Theorem List (p. 436 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sqrlearg 43501 | The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) β β’ (π β ((π΄β2) β€ π΄ β π΄ β (0[,]1))) | ||
Theorem | ressiocsup 43502 | If the supremum belongs to a set of reals, the set is a subset of the unbounded below, right-closed interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ π = sup(π΄, β*, < ) & β’ (π β π β π΄) & β’ πΌ = (-β(,]π) β β’ (π β π΄ β πΌ) | ||
Theorem | ressioosup 43503 | If the supremum does not belong to a set of reals, the set is a subset of the unbounded below, right-open interval, with upper bound equal to the supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ π = sup(π΄, β*, < ) & β’ (π β Β¬ π β π΄) & β’ πΌ = (-β(,)π) β β’ (π β π΄ β πΌ) | ||
Theorem | iooiinioc 43504* | A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) β β’ (π β β© π β β (π΄(,)(π΅ + (1 / π))) = (π΄(,]π΅)) | ||
Theorem | ressiooinf 43505 | If the infimum does not belong to a set of reals, the set is a subset of the unbounded above, left-open interval, with lower bound equal to the infimum. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) & β’ π = inf(π΄, β*, < ) & β’ (π β Β¬ π β π΄) & β’ πΌ = (π(,)+β) β β’ (π β π΄ β πΌ) | ||
Theorem | icogelbd 43506 | An element of a left-closed right-open interval is greater than or equal to its lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,)π΅)) β β’ (π β π΄ β€ πΆ) | ||
Theorem | iocleubd 43507 | An element of a left-open right-closed interval is smaller than or equal to its upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,]π΅)) β β’ (π β πΆ β€ π΅) | ||
Theorem | uzinico 43508 | An upper interval of integers is the intersection of the integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β π = (β€ β© (π[,)+β))) | ||
Theorem | preimaiocmnf 43509* | Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β(,]π΅)) = {π₯ β π΄ β£ (πΉβπ₯) β€ π΅}) | ||
Theorem | uzinico2 43510 | An upper interval of integers is the intersection of a larger upper interval of integers with an upper part of the reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β π β (β€β₯βπ)) β β’ (π β (β€β₯βπ) = ((β€β₯βπ) β© (π[,)+β))) | ||
Theorem | uzinico3 43511 | An upper interval of integers doesn't change when it's intersected with a left-closed, unbounded above interval, with the same lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β π = (π β© (π[,)+β))) | ||
Theorem | icossico2 43512 | Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π΅ β β*) & β’ (π β πΆ β β*) & β’ (π β π΅ β€ π΄) β β’ (π β (π΄[,)πΆ) β (π΅[,)πΆ)) | ||
Theorem | dmico 43513 | The domain of the closed-below, open-above interval function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ dom [,) = (β* Γ β*) | ||
Theorem | ndmico 43514 | The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (Β¬ (π΄ β β* β§ π΅ β β*) β (π΄[,)π΅) = β ) | ||
Theorem | uzubioo 43515* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β β) β β’ (π β βπ β (π(,)+β)π β π) | ||
Theorem | uzubico 43516* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β β) β β’ (π β βπ β (π[,)+β)π β π) | ||
Theorem | uzubioo2 43517* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β βπ₯ β β βπ β (π₯(,)+β)π β π) | ||
Theorem | uzubico2 43518* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β βπ₯ β β βπ β (π₯[,)+β)π β π) | ||
Theorem | iocgtlbd 43519 | An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,]π΅)) β β’ (π β π΄ < πΆ) | ||
Theorem | xrtgioo2 43520 | The topology on the extended reals coincides with the standard topology on the reals, when restricted to β. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (topGenβran (,)) = ((ordTopβ β€ ) βΎt β) | ||
Theorem | tgioo4 43521 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (topGenβran (,)) = ((TopOpenββfld) βΎt β) | ||
Theorem | fsummulc1f 43522* | Closure of a finite sum of complex numbers π΄(π). A version of fsummulc1 15605 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ (π β πΆ β β) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (Ξ£π β π΄ π΅ Β· πΆ) = Ξ£π β π΄ (π΅ Β· πΆ)) | ||
Theorem | fsumnncl 43523* | Closure of a nonempty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumge0cl 43524* | The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) β β’ (π β Ξ£π β π΄ π΅ β (0[,)+β)) | ||
Theorem | fsumf1of 43525* | Re-index a finite sum using a bijection. Same as fsumf1o 15543, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ β²ππ & β’ β²ππ & β’ (π = πΊ β π΅ = π·) & β’ (π β πΆ β Fin) & β’ (π β πΉ:πΆβ1-1-ontoβπ΄) & β’ ((π β§ π β πΆ) β (πΉβπ) = πΊ) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ = Ξ£π β πΆ π·) | ||
Theorem | fsumiunss 43526* | Sum over a disjoint indexed union, intersected with a finite set π·. Similar to fsumiun 15641, but here π΄ and π΅ need not be finite. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ ((π β§ π₯ β π΄) β π΅ β π) & β’ (π β Disj π₯ β π΄ π΅) & β’ ((π β§ π₯ β π΄ β§ π β π΅) β πΆ β β) & β’ (π β π· β Fin) β β’ (π β Ξ£π β βͺ π₯ β π΄ (π΅ β© π·)πΆ = Ξ£π₯ β {π₯ β π΄ β£ (π΅ β© π·) β β }Ξ£π β (π΅ β© π·)πΆ) | ||
Theorem | fsumreclf 43527* | Closure of a finite sum of reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumlessf 43528* | A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 0 β€ π΅) & β’ (π β πΆ β π΄) β β’ (π β Ξ£π β πΆ π΅ β€ Ξ£π β π΄ π΅) | ||
Theorem | fsumsupp0 43529* | Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β Fin) & β’ (π β πΉ:π΄βΆβ) β β’ (π β Ξ£π β (πΉ supp 0)(πΉβπ) = Ξ£π β π΄ (πΉβπ)) | ||
Theorem | fsumsermpt 43530* | A finite sum expressed in terms of a partial sum of an infinite series. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΄ β β) & β’ πΉ = (π β π β¦ Ξ£π β (π...π)π΄) & β’ πΊ = seqπ( + , (π β π β¦ π΄)) β β’ (π β πΉ = πΊ) | ||
Theorem | fmul01 43531* | Multiplying a finite number of values in [ 0 , 1 ] , gives the final product itself a number in [ 0 , 1 ]. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ΅ & β’ β²ππ & β’ π΄ = seqπΏ( Β· , π΅) & β’ (π β πΏ β β€) & β’ (π β π β (β€β₯βπΏ)) & β’ (π β πΎ β (πΏ...π)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β β) & β’ ((π β§ π β (πΏ...π)) β 0 β€ (π΅βπ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β€ 1) β β’ (π β (0 β€ (π΄βπΎ) β§ (π΄βπΎ) β€ 1)) | ||
Theorem | fmulcl 43532* | If ' Y ' is closed under the multiplication of two functions, then Y is closed under the multiplication ( ' X ' ) of a finite number of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ (π β π β (1...π)) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) & β’ (π β π β V) β β’ (π β π β π) | ||
Theorem | fmuldfeqlem1 43533* | induction step for the proof of fmuldfeq 43534. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²ππ & β’ β²π‘π & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ (π β π β V) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) & β’ (π β π β (1...π)) & β’ (π β (π + 1) β (1...π)) & β’ (π β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) & β’ ((π β§ π β π) β π:πβΆβ) β β’ ((π β§ π‘ β π) β ((seq1(π, π)β(π + 1))βπ‘) = (seq1( Β· , (πΉβπ‘))β(π + 1))) | ||
Theorem | fmuldfeq 43534* | X and Z are two equivalent definitions of the finite product of real functions. Y is a set of real functions from a common domain T, Y is closed under function multiplication and U is a finite sequence of functions in Y. M is the number of functions multiplied together. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²π‘π & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ π = (seq1(π, π)βπ) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ π = (π‘ β π β¦ (seq1( Β· , (πΉβπ‘))βπ)) & β’ (π β π β V) & β’ (π β π β β) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β π) β π:πβΆβ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) β β’ ((π β§ π‘ β π) β (πβπ‘) = (πβπ‘)) | ||
Theorem | fmul01lt1lem1 43535* | Given a finite multiplication of values betweeen 0 and 1, a value larger than its first element is larger the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ΅ & β’ β²ππ & β’ π΄ = seqπΏ( Β· , π΅) & β’ (π β πΏ β β€) & β’ (π β π β (β€β₯βπΏ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β β) & β’ ((π β§ π β (πΏ...π)) β 0 β€ (π΅βπ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β€ 1) & β’ (π β πΈ β β+) & β’ (π β (π΅βπΏ) < πΈ) β β’ (π β (π΄βπ) < πΈ) | ||
Theorem | fmul01lt1lem2 43536* | Given a finite multiplication of values betweeen 0 and 1, a value πΈ larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ΅ & β’ β²ππ & β’ π΄ = seqπΏ( Β· , π΅) & β’ (π β πΏ β β€) & β’ (π β π β (β€β₯βπΏ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β β) & β’ ((π β§ π β (πΏ...π)) β 0 β€ (π΅βπ)) & β’ ((π β§ π β (πΏ...π)) β (π΅βπ) β€ 1) & β’ (π β πΈ β β+) & β’ (π β π½ β (πΏ...π)) & β’ (π β (π΅βπ½) < πΈ) β β’ (π β (π΄βπ) < πΈ) | ||
Theorem | fmul01lt1 43537* | Given a finite multiplication of values betweeen 0 and 1, a value E larger than any multiplicand, is larger than the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ΅ & β’ β²ππ & β’ β²ππ΄ & β’ π΄ = seq1( Β· , π΅) & β’ (π β π β β) & β’ (π β π΅:(1...π)βΆβ) & β’ ((π β§ π β (1...π)) β 0 β€ (π΅βπ)) & β’ ((π β§ π β (1...π)) β (π΅βπ) β€ 1) & β’ (π β πΈ β β+) & β’ (π β βπ β (1...π)(π΅βπ) < πΈ) β β’ (π β (π΄βπ) < πΈ) | ||
Theorem | cncfmptss 43538* | A continuous complex function restricted to a subset is continuous, using maps-to notation. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²π₯πΉ & β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΆ β π΄) β β’ (π β (π₯ β πΆ β¦ (πΉβπ₯)) β (πΆβcnβπ΅)) | ||
Theorem | rrpsscn 43539 | The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β+ β β | ||
Theorem | mulc1cncfg 43540* | A version of mulc1cncf 24190 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
β’ β²π₯πΉ & β’ β²π₯π & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β π΅ β β) β β’ (π β (π₯ β π΄ β¦ (π΅ Β· (πΉβπ₯))) β (π΄βcnββ)) | ||
Theorem | infrglb 43541* | The infimum of a nonempty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.) |
β’ (((π΄ β β β§ π΄ β β β§ βπ₯ β β βπ¦ β π΄ π₯ β€ π¦) β§ π΅ β β) β (inf(π΄, β, < ) < π΅ β βπ§ β π΄ π§ < π΅)) | ||
Theorem | expcnfg 43542* | If πΉ is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 24211. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²π₯πΉ & β’ (π β πΉ β (π΄βcnββ)) & β’ (π β π β β0) β β’ (π β (π₯ β π΄ β¦ ((πΉβπ₯)βπ)) β (π΄βcnββ)) | ||
Theorem | prodeq2ad 43543* | Equality deduction for product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β βπ β π΄ π΅ = βπ β π΄ πΆ) | ||
Theorem | fprodsplit1 43544* | Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄) & β’ ((π β§ π = πΆ) β π΅ = π·) β β’ (π β βπ β π΄ π΅ = (π· Β· βπ β (π΄ β {πΆ})π΅)) | ||
Theorem | fprodexp 43545* | Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β π β β0) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β βπ β π΄ (π΅βπ) = (βπ β π΄ π΅βπ)) | ||
Theorem | fprodabs2 43546* | The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (absββπ β π΄ π΅) = βπ β π΄ (absβπ΅)) | ||
Theorem | fprod0 43547* | A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππΆ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π = πΎ β π΅ = πΆ) & β’ (π β πΎ β π΄) & β’ (π β πΆ = 0) β β’ (π β βπ β π΄ π΅ = 0) | ||
Theorem | mccllem 43548* | * Induction step for mccl 43549. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β Fin) & β’ (π β πΆ β π΄) & β’ (π β π· β (π΄ β πΆ)) & β’ (π β π΅ β (β0 βm (πΆ βͺ {π·}))) & β’ (π β βπ β (β0 βm πΆ)((!βΞ£π β πΆ (πβπ)) / βπ β πΆ (!β(πβπ))) β β) β β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / βπ β (πΆ βͺ {π·})(!β(π΅βπ))) β β) | ||
Theorem | mccl 43549* | A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ΅ & β’ (π β π΄ β Fin) & β’ (π β π΅ β (β0 βm π΄)) β β’ (π β ((!βΞ£π β π΄ (π΅βπ)) / βπ β π΄ (!β(π΅βπ))) β β) | ||
Theorem | fprodcnlem 43550* | A finite product of functions to complex numbers from a common topological space is continuous. Induction step. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ πΎ = (TopOpenββfld) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) & β’ (π β π β π΄) & β’ (π β π β (π΄ β π)) & β’ (π β (π₯ β π β¦ βπ β π π΅) β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ βπ β (π βͺ {π})π΅) β (π½ Cn πΎ)) | ||
Theorem | fprodcn 43551* | A finite product of functions to complex numbers from a common topological space is continuous. The class expression for π΅ normally contains free variables π and π₯ to index it. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ β²ππ & β’ πΎ = (TopOpenββfld) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ βπ β π΄ π΅) β (π½ Cn πΎ)) | ||
Theorem | clim1fr1 43552* | A class of sequences of fractions that converge to 1. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΉ = (π β β β¦ (((π΄ Β· π) + π΅) / (π΄ Β· π))) & β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) β β’ (π β πΉ β 1) | ||
Theorem | isumneg 43553* | Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β Ξ£π β π π΄ β β) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π -π΄ = -Ξ£π β π π΄) | ||
Theorem | climrec 43554* | Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ β π΄) & β’ (π β π΄ β 0) & β’ ((π β§ π β π) β (πΊβπ) β (β β {0})) & β’ ((π β§ π β π) β (π»βπ) = (1 / (πΊβπ))) & β’ (π β π» β π) β β’ (π β π» β (1 / π΄)) | ||
Theorem | climmulf 43555* | A version of climmul 15450 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β π» β π) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ) Β· (πΊβπ))) β β’ (π β π» β (π΄ Β· π΅)) | ||
Theorem | climexp 43556* | The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β π΄) & β’ (π β π β β0) & β’ (π β π» β π) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) β β’ (π β π» β (π΄βπ)) | ||
Theorem | climinf 43557* | A bounded monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ (π β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) β β’ (π β πΉ β inf(ran πΉ, β, < )) | ||
Theorem | climsuselem1 43558* | The subsequence index πΌ has the expected properties: it belongs to the same upper integers as the original index, and it is always greater than or equal to the original index. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β (πΌβπ) β π) & β’ ((π β§ π β π) β (πΌβ(π + 1)) β (β€β₯β((πΌβπ) + 1))) β β’ ((π β§ πΎ β π) β (πΌβπΎ) β (β€β₯βπΎ)) | ||
Theorem | climsuse 43559* | A subsequence πΊ of a converging sequence πΉ, converges to the same limit. πΌ is the strictly increasing and it is used to index the subsequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ β²ππΌ & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ (π β πΉ β π΄) & β’ (π β (πΌβπ) β π) & β’ ((π β§ π β π) β (πΌβ(π + 1)) β (β€β₯β((πΌβπ) + 1))) & β’ (π β πΊ β π) & β’ ((π β§ π β π) β (πΊβπ) = (πΉβ(πΌβπ))) β β’ (π β πΊ β π΄) | ||
Theorem | climrecf 43560* | A version of climrec 43554 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΊ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ β π΄) & β’ (π β π΄ β 0) & β’ ((π β§ π β π) β (πΊβπ) β (β β {0})) & β’ ((π β§ π β π) β (π»βπ) = (1 / (πΊβπ))) & β’ (π β π» β π) β β’ (π β π» β (1 / π΄)) | ||
Theorem | climneg 43561* | Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β (π β π β¦ -(πΉβπ)) β -π΄) | ||
Theorem | climinff 43562* | A version of climinf 43557 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 15-Sep-2020.) |
β’ β²ππ & β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π β π) β (πΉβ(π + 1)) β€ (πΉβπ)) & β’ (π β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) β β’ (π β πΉ β inf(ran πΉ, β, < )) | ||
Theorem | climdivf 43563* | Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β π» β π) & β’ (π β πΊ β π΅) & β’ (π β π΅ β 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β (β β {0})) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ) / (πΊβπ))) β β’ (π β π» β (π΄ / π΅)) | ||
Theorem | climreeq 43564 | If πΉ is a real function, then πΉ converges to π΄ with respect to the standard topology on the reals if and only if it converges to π΄ with respect to the standard topology on complex numbers. In the theorem, π is defined to be convergence w.r.t. the standard topology on the reals and then πΉπ π΄ represents the statement "πΉ converges to π΄, with respect to the standard topology on the reals". Notice that there is no need for the hypothesis that π΄ is a real number. (Contributed by Glauco Siliprandi, 2-Jul-2017.) |
β’ π = (βπ‘β(topGenβran (,))) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) β β’ (π β (πΉπ π΄ β πΉ β π΄)) | ||
Theorem | ellimciota 43565* | An explicit value for the limit, when the limit exists at a limit point. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β ((limPtβπΎ)βπ΄)) & β’ (π β (πΉ limβ π΅) β β ) & β’ πΎ = (TopOpenββfld) β β’ (π β (β©π₯π₯ β (πΉ limβ π΅)) β (πΉ limβ π΅)) | ||
Theorem | climaddf 43566* | A version of climadd 15449 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β π» β π) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ) + (πΊβπ))) β β’ (π β π» β (π΄ + π΅)) | ||
Theorem | mullimc 43567* | Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ πΊ = (π₯ β π΄ β¦ πΆ) & β’ π» = (π₯ β π΄ β¦ (π΅ Β· πΆ)) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β π β (πΉ limβ π·)) & β’ (π β π β (πΊ limβ π·)) β β’ (π β (π Β· π) β (π» limβ π·)) | ||
Theorem | ellimcabssub0 43568* | An equivalent condition for being a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ πΊ = (π₯ β π΄ β¦ (π΅ β πΆ)) & β’ (π β π΄ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β π· β β) & β’ (π β πΆ β β) β β’ (π β (πΆ β (πΉ limβ π·) β 0 β (πΊ limβ π·))) | ||
Theorem | limcdm0 43569 | If a function has empty domain, every complex number is a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:β βΆβ) & β’ (π β π΅ β β) β β’ (π β (πΉ limβ π΅) = β) | ||
Theorem | islptre 43570* | An equivalence condition for a limit point w.r.t. the standard topology on the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π½ = (topGenβran (,)) & β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β (π΅ β ((limPtβπ½)βπ΄) β βπ β β* βπ β β* (π΅ β (π(,)π) β ((π(,)π) β© (π΄ β {π΅})) β β ))) | ||
Theorem | limccog 43571 | Limit of the composition of two functions. If the limit of πΉ at π΄ is π΅ and the limit of πΊ at π΅ is πΆ, then the limit of πΊ β πΉ at π΄ is πΆ. With respect to limcco 25179 and limccnp 25177, here we drop continuity assumptions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β ran πΉ β (dom πΊ β {π΅})) & β’ (π β π΅ β (πΉ limβ π΄)) & β’ (π β πΆ β (πΊ limβ π΅)) β β’ (π β πΆ β ((πΊ β πΉ) limβ π΄)) | ||
Theorem | limciccioolb 43572 | The limit of a function at the lower bound of a closed interval only depends on the values in the inner open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄[,]π΅)βΆβ) β β’ (π β ((πΉ βΎ (π΄(,)π΅)) limβ π΄) = (πΉ limβ π΄)) | ||
Theorem | climf 43573* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄. Similar to clim 15311, but without the disjoint var constraint πΉπ. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²ππΉ & β’ (π β πΉ β π) & β’ ((π β§ π β β€) β (πΉβπ) = π΅) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β β€ βπ β (β€β₯βπ)(π΅ β β β§ (absβ(π΅ β π΄)) < π₯)))) | ||
Theorem | mullimcf 43574* | Limit of the multiplication of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) & β’ π» = (π₯ β π΄ β¦ ((πΉβπ₯) Β· (πΊβπ₯))) & β’ (π β π΅ β (πΉ limβ π·)) & β’ (π β πΆ β (πΊ limβ π·)) β β’ (π β (π΅ Β· πΆ) β (π» limβ π·)) | ||
Theorem | constlimc 43575* | Limit of constant function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β π΅ β (πΉ limβ πΆ)) | ||
Theorem | rexlim2d 43576* | Inference removing two restricted quantifiers. Same as rexlimdvv 3203, but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²π₯π & β’ β²π¦π & β’ (π β ((π₯ β π΄ β§ π¦ β π΅) β (π β π))) β β’ (π β (βπ₯ β π΄ βπ¦ β π΅ π β π)) | ||
Theorem | idlimc 43577* | Limit of the identity function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β π΄ β¦ π₯) & β’ (π β π β β) β β’ (π β π β (πΉ limβ π)) | ||
Theorem | divcnvg 43578* | The sequence of reciprocals of positive integers, multiplied by the factor π΄, converges to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π β β) β (π β (β€β₯βπ) β¦ (π΄ / π)) β 0) | ||
Theorem | limcperiod 43579* | If πΉ is a periodic function with period π, the limit doesn't change if we shift the limiting point by π. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:dom πΉβΆβ) & β’ (π β π΄ β β) & β’ (π β π΄ β dom πΉ) & β’ (π β π β β) & β’ π΅ = {π₯ β β β£ βπ¦ β π΄ π₯ = (π¦ + π)} & β’ (π β π΅ β dom πΉ) & β’ ((π β§ π¦ β π΄) β (πΉβ(π¦ + π)) = (πΉβπ¦)) & β’ (π β πΆ β ((πΉ βΎ π΄) limβ π·)) β β’ (π β πΆ β ((πΉ βΎ π΅) limβ (π· + π))) | ||
Theorem | limcrecl 43580 | If πΉ is a real-valued function, π΅ is a limit point of its domain, and the limit of πΉ at π΅ exists, then this limit is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β ((limPtβ(TopOpenββfld))βπ΄)) & β’ (π β πΏ β (πΉ limβ π΅)) β β’ (π β πΏ β β) | ||
Theorem | sumnnodd 43581* | A series indexed by β with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:ββΆβ) & β’ ((π β§ π β β β§ (π / 2) β β) β (πΉβπ) = 0) & β’ (π β seq1( + , πΉ) β π΅) β β’ (π β (seq1( + , (π β β β¦ (πΉβ((2 Β· π) β 1)))) β π΅ β§ Ξ£π β β (πΉβπ) = Ξ£π β β (πΉβ((2 Β· π) β 1)))) | ||
Theorem | lptioo2 43582 | The upper bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π½ = (topGenβran (,)) & β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) β β’ (π β π΅ β ((limPtβπ½)β(π΄(,)π΅))) | ||
Theorem | lptioo1 43583 | The lower bound of an open interval is a limit point of the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π½ = (topGenβran (,)) & β’ (π β π΄ β β) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) β β’ (π β π΄ β ((limPtβπ½)β(π΄(,)π΅))) | ||
Theorem | elprn1 43584 | A member of an unordered pair that is not the "first", must be the "second". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β {π΅, πΆ} β§ π΄ β π΅) β π΄ = πΆ) | ||
Theorem | elprn2 43585 | A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β {π΅, πΆ} β§ π΄ β πΆ) β π΄ = π΅) | ||
Theorem | limcmptdm 43586* | The domain of a maps-to function with a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β (πΉ limβ π·)) β β’ (π β π΄ β β) | ||
Theorem | clim2f 43587* | Express the predicate: The limit of complex number sequence πΉ is π΄, or πΉ converges to π΄, with more general quantifier restrictions than clim 15311. Similar to clim2 15321, but without the disjoint var constraint πΉπ. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π) & β’ ((π β§ π β π) β (πΉβπ) = π΅) β β’ (π β (πΉ β π΄ β (π΄ β β β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΅ β β β§ (absβ(π΅ β π΄)) < π₯)))) | ||
Theorem | limcicciooub 43588 | The limit of a function at the upper bound of a closed interval only depends on the values in the inner open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) & β’ (π β πΉ:(π΄[,]π΅)βΆβ) β β’ (π β ((πΉ βΎ (π΄(,)π΅)) limβ π΅) = (πΉ limβ π΅)) | ||
Theorem | ltmod 43589 | A sufficient condition for a "less than" relationship for the mod operator. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β+) & β’ (π β πΆ β ((π΄ β (π΄ mod π΅))[,)π΄)) β β’ (π β (πΆ mod π΅) < (π΄ mod π΅)) | ||
Theorem | islpcn 43590* | A characterization for a limit point for the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π β β) & β’ (π β π β β) β β’ (π β (π β ((limPtβ(TopOpenββfld))βπ) β βπ β β+ βπ₯ β (π β {π})(absβ(π₯ β π)) < π)) | ||
Theorem | lptre2pt 43591* | If a set in the real line has a limit point than it contains two distinct points that are closer than a given distance. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π½ = (topGenβran (,)) & β’ (π β π΄ β β) & β’ (π β ((limPtβπ½)βπ΄) β β ) & β’ (π β πΈ β β+) β β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β§ (absβ(π₯ β π¦)) < πΈ)) | ||
Theorem | limsupre 43592* | If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 13-Sep-2020.) |
β’ (π β π΅ β β) & β’ (π β sup(π΅, β*, < ) = +β) & β’ (π β πΉ:π΅βΆβ) & β’ (π β βπ β β βπ β β βπ β π΅ (π β€ π β (absβ(πΉβπ)) β€ π)) β β’ (π β (lim supβπΉ) β β) | ||
Theorem | limcresiooub 43593 | The left limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β*) & β’ (π β πΆ β β) & β’ (π β π΅ < πΆ) & β’ (π β (π΅(,)πΆ) β π΄) & β’ (π β π· β β*) & β’ (π β π· β€ π΅) β β’ (π β ((πΉ βΎ (π΅(,)πΆ)) limβ πΆ) = ((πΉ βΎ (π·(,)πΆ)) limβ πΆ)) | ||
Theorem | limcresioolb 43594 | The right limit doesn't change if the function is restricted to a smaller open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β) & β’ (π β πΆ β β*) & β’ (π β π΅ < πΆ) & β’ (π β (π΅(,)πΆ) β π΄) & β’ (π β π· β β*) & β’ (π β πΆ β€ π·) β β’ (π β ((πΉ βΎ (π΅(,)πΆ)) limβ π΅) = ((πΉ βΎ (π΅(,)π·)) limβ π΅)) | ||
Theorem | limcleqr 43595 | If the left and the right limits are equal, the limit of the function exits and the three limits coincide. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΎ = (TopOpenββfld) & β’ (π β π΄ β β) & β’ π½ = (topGenβran (,)) & β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β) & β’ (π β πΏ β ((πΉ βΎ (-β(,)π΅)) limβ π΅)) & β’ (π β π β ((πΉ βΎ (π΅(,)+β)) limβ π΅)) & β’ (π β πΏ = π ) β β’ (π β πΏ β (πΉ limβ π΅)) | ||
Theorem | lptioo2cn 43596 | The upper bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π½ = (TopOpenββfld) & β’ (π β π΄ β β*) & β’ (π β π΅ β β) & β’ (π β π΄ < π΅) β β’ (π β π΅ β ((limPtβπ½)β(π΄(,)π΅))) | ||
Theorem | lptioo1cn 43597 | The lower bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ π½ = (TopOpenββfld) & β’ (π β π΅ β β*) & β’ (π β π΄ β β) & β’ (π β π΄ < π΅) β β’ (π β π΄ β ((limPtβπ½)β(π΄(,)π΅))) | ||
Theorem | neglimc 43598* | Limit of the negative function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ πΊ = (π₯ β π΄ β¦ -π΅) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β (πΉ limβ π·)) β β’ (π β -πΆ β (πΊ limβ π·)) | ||
Theorem | addlimc 43599* | Sum of two limits. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ πΊ = (π₯ β π΄ β¦ πΆ) & β’ π» = (π₯ β π΄ β¦ (π΅ + πΆ)) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β πΈ β (πΉ limβ π·)) & β’ (π β πΌ β (πΊ limβ π·)) β β’ (π β (πΈ + πΌ) β (π» limβ π·)) | ||
Theorem | 0ellimcdiv 43600* | If the numerator converges to 0 and the denominator converges to a nonzero number, then the fraction converges to 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ πΊ = (π₯ β π΄ β¦ πΆ) & β’ π» = (π₯ β π΄ β¦ (π΅ / πΆ)) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β (β β {0})) & β’ (π β 0 β (πΉ limβ πΈ)) & β’ (π β π· β (πΊ limβ πΈ)) & β’ (π β π· β 0) β β’ (π β 0 β (π» limβ πΈ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |