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-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iccnct 43501 | A closed interval, with more than one element is uncountable. (Contributed by Glauco Siliprandi, 3-Jan-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) & β’ πΆ = (π΄[,]π΅) β β’ (π β Β¬ πΆ βΌ Ο) | ||
Theorem | iooiinicc 43502* | A closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) β β’ (π β β© π β β ((π΄ β (1 / π))(,)(π΅ + (1 / π))) = (π΄[,]π΅)) | ||
Theorem | iccgelbd 43503 | An element of a closed interval is more than or equal to its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) β β’ (π β π΄ β€ πΆ) | ||
Theorem | iooltubd 43504 | An element of an open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β πΆ < π΅) | ||
Theorem | icoltubd 43505 | An element of a left-closed right-open interval is less than its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,)π΅)) β β’ (π β πΆ < π΅) | ||
Theorem | qelioo 43506* | The rational numbers are dense in β*: any two extended real numbers have a rational between them. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β π΄ < π΅) β β’ (π β βπ₯ β β π₯ β (π΄(,)π΅)) | ||
Theorem | tgqioo2 43507* | Every open set of reals is the (countable) union of open interval with rational bounds. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ π½ = (topGenβran (,)) & β’ (π β π΄ β π½) β β’ (π β βπ(π β ((,) β (β Γ β)) β§ π΄ = βͺ π)) | ||
Theorem | iccleubd 43508 | An element of a closed interval is less than or equal to its upper bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄[,]π΅)) β β’ (π β πΆ β€ π΅) | ||
Theorem | elioored 43509 | A member of an open interval of reals is a real. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β (π΅(,)πΆ)) β β’ (π β π΄ β β) | ||
Theorem | ioogtlbd 43510 | An element of a closed interval is greater than its lower bound. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,)π΅)) β β’ (π β π΄ < πΆ) | ||
Theorem | ioofun 43511 | (,) is a function. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ Fun (,) | ||
Theorem | icomnfinre 43512 | A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) β β’ (π β ((-β[,)π΄) β© β) = (-β(,)π΄)) | ||
Theorem | sqrlearg 43513 | The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β) β β’ (π β ((π΄β2) β€ π΄ β π΄ β (0[,]1))) | ||
Theorem | ressiocsup 43514 | 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 43515 | 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 43516* | A left-open, right-closed interval expressed as the indexed intersection of open intervals. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β) β β’ (π β β© π β β (π΄(,)(π΅ + (1 / π))) = (π΄(,]π΅)) | ||
Theorem | ressiooinf 43517 | 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 43518 | 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 43519 | 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 43520 | 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 43521* | Preimage of a right-closed interval, unbounded below. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β π΅ β β*) β β’ (π β (β‘πΉ β (-β(,]π΅)) = {π₯ β π΄ β£ (πΉβπ₯) β€ π΅}) | ||
Theorem | uzinico2 43522 | 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 43523 | 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 43524 | 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 43525 | The domain of the closed-below, open-above interval function. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ dom [,) = (β* Γ β*) | ||
Theorem | ndmico 43526 | The closed-below, open-above interval function's value is empty outside of its domain. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (Β¬ (π΄ β β* β§ π΅ β β*) β (π΄[,)π΅) = β ) | ||
Theorem | uzubioo 43527* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β β) β β’ (π β βπ β (π(,)+β)π β π) | ||
Theorem | uzubico 43528* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ (π β π β β) β β’ (π β βπ β (π[,)+β)π β π) | ||
Theorem | uzubioo2 43529* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β βπ₯ β β βπ β (π₯(,)+β)π β π) | ||
Theorem | uzubico2 43530* | The upper integers are unbounded above. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) β β’ (π β βπ₯ β β βπ β (π₯[,)+β)π β π) | ||
Theorem | iocgtlbd 43531 | An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
β’ (π β π΄ β β*) & β’ (π β π΅ β β*) & β’ (π β πΆ β (π΄(,]π΅)) β β’ (π β π΄ < πΆ) | ||
Theorem | xrtgioo2 43532 | 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 43533 | 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 43534* | 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 43535* | Closure of a nonempty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β β ) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumge0cl 43536* | The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β (0[,)+β)) β β’ (π β Ξ£π β π΄ π΅ β (0[,)+β)) | ||
Theorem | fsumf1of 43537* | 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 43538* | 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 43539* | Closure of a finite sum of reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β Ξ£π β π΄ π΅ β β) | ||
Theorem | fsumlessf 43540* | A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020.) |
β’ β²ππ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ ((π β§ π β π΄) β 0 β€ π΅) & β’ (π β πΆ β π΄) β β’ (π β Ξ£π β πΆ π΅ β€ Ξ£π β π΄ π΅) | ||
Theorem | fsumsupp0 43541* | Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
β’ (π β π΄ β Fin) & β’ (π β πΉ:π΄βΆβ) β β’ (π β Ξ£π β (πΉ supp 0)(πΉβπ) = Ξ£π β π΄ (πΉβπ)) | ||
Theorem | fsumsermpt 43542* | A finite sum expressed in terms of a partial sum of an infinite series. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
β’ (π β π β β€) & β’ π = (β€β₯βπ) & β’ ((π β§ π β π) β π΄ β β) & β’ πΉ = (π β π β¦ Ξ£π β (π...π)π΄) & β’ πΊ = seqπ( + , (π β π β¦ π΄)) β β’ (π β πΉ = πΊ) | ||
Theorem | fmul01 43543* | 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 43544* | 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 43545* | induction step for the proof of fmuldfeq 43546. (Contributed by Glauco Siliprandi, 20-Apr-2017.) |
β’ β²ππ & β’ β²ππ & β’ β²π‘π & β’ π = (π β π, π β π β¦ (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘)))) & β’ πΉ = (π‘ β π β¦ (π β (1...π) β¦ ((πβπ)βπ‘))) & β’ (π β π β V) & β’ (π β π:(1...π)βΆπ) & β’ ((π β§ π β π β§ π β π) β (π‘ β π β¦ ((πβπ‘) Β· (πβπ‘))) β π) & β’ (π β π β (1...π)) & β’ (π β (π + 1) β (1...π)) & β’ (π β ((seq1(π, π)βπ)βπ‘) = (seq1( Β· , (πΉβπ‘))βπ)) & β’ ((π β§ π β π) β π:πβΆβ) β β’ ((π β§ π‘ β π) β ((seq1(π, π)β(π + 1))βπ‘) = (seq1( Β· , (πΉβπ‘))β(π + 1))) | ||
Theorem | fmuldfeq 43546* | 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 43547* | 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 43548* | 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 43549* | 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 43550* | 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 43551 | The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β+ β β | ||
Theorem | mulc1cncfg 43552* | 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 43553* | 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 43554* | 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 43555* | Equality deduction for product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΅ = πΆ) β β’ (π β βπ β π΄ π΅ = βπ β π΄ πΆ) | ||
Theorem | fprodsplit1 43556* | Separate out a term in a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π β πΆ β π΄) & β’ ((π β§ π = πΆ) β π΅ = π·) β β’ (π β βπ β π΄ π΅ = (π· Β· βπ β (π΄ β {πΆ})π΅)) | ||
Theorem | fprodexp 43557* | Positive integer exponentiation of a finite product. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ (π β π β β0) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β βπ β π΄ (π΅βπ) = (βπ β π΄ π΅βπ)) | ||
Theorem | fprodabs2 43558* | The absolute value of a finite product . (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) β β’ (π β (absββπ β π΄ π΅) = βπ β π΄ (absβπ΅)) | ||
Theorem | fprod0 43559* | A finite product with a zero term is zero. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ & β’ β²ππΆ & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β π΅ β β) & β’ (π = πΎ β π΅ = πΆ) & β’ (π β πΎ β π΄) & β’ (π β πΆ = 0) β β’ (π β βπ β π΄ π΅ = 0) | ||
Theorem | mccllem 43560* | * Induction step for mccl 43561. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ (π β π΄ β Fin) & β’ (π β πΆ β π΄) & β’ (π β π· β (π΄ β πΆ)) & β’ (π β π΅ β (β0 βm (πΆ βͺ {π·}))) & β’ (π β βπ β (β0 βm πΆ)((!βΞ£π β πΆ (πβπ)) / βπ β πΆ (!β(πβπ))) β β) β β’ (π β ((!βΞ£π β (πΆ βͺ {π·})(π΅βπ)) / βπ β (πΆ βͺ {π·})(!β(π΅βπ))) β β) | ||
Theorem | mccl 43561* | A multinomial coefficient, in its standard domain, is a positive integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
β’ β²ππ΅ & β’ (π β π΄ β Fin) & β’ (π β π΅ β (β0 βm π΄)) β β’ (π β ((!βΞ£π β π΄ (π΅βπ)) / βπ β π΄ (!β(π΅βπ))) β β) | ||
Theorem | fprodcnlem 43562* | 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 43563* | 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 43564* | A class of sequences of fractions that converge to 1. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ πΉ = (π β β β¦ (((π΄ Β· π) + π΅) / (π΄ Β· π))) & β’ (π β π΄ β β) & β’ (π β π΄ β 0) & β’ (π β π΅ β β) β β’ (π β πΉ β 1) | ||
Theorem | isumneg 43565* | Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β Ξ£π β π π΄ β β) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β π΄ β β) & β’ (π β seqπ( + , πΉ) β dom β ) β β’ (π β Ξ£π β π -π΄ = -Ξ£π β π π΄) | ||
Theorem | climrec 43566* | Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ β π΄) & β’ (π β π΄ β 0) & β’ ((π β§ π β π) β (πΊβπ) β (β β {0})) & β’ ((π β§ π β π) β (π»βπ) = (1 / (πΊβπ))) & β’ (π β π» β π) β β’ (π β π» β (1 / π΄)) | ||
Theorem | climmulf 43567* | A version of climmul 15450 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β π» β π) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ) Β· (πΊβπ))) β β’ (π β π» β (π΄ Β· π΅)) | ||
Theorem | climexp 43568* | The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆβ) & β’ (π β πΉ β π΄) & β’ (π β π β β0) & β’ (π β π» β π) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) β β’ (π β π» β (π΄βπ)) | ||
Theorem | climinf 43569* | 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 43570* | 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 43571* | 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 43572* | A version of climrec 43566 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΊ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΊ β π΄) & β’ (π β π΄ β 0) & β’ ((π β§ π β π) β (πΊβπ) β (β β {0})) & β’ ((π β§ π β π) β (π»βπ) = (1 / (πΊβπ))) & β’ (π β π» β π) β β’ (π β π» β (1 / π΄)) | ||
Theorem | climneg 43573* | Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ ((π β§ π β π) β (πΉβπ) β β) β β’ (π β (π β π β¦ -(πΉβπ)) β -π΄) | ||
Theorem | climinff 43574* | A version of climinf 43569 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 43575* | Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β π» β π) & β’ (π β πΊ β π΅) & β’ (π β π΅ β 0) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β (β β {0})) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ) / (πΊβπ))) β β’ (π β π» β (π΄ / π΅)) | ||
Theorem | climreeq 43576 | 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 43577* | 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 43578* | A version of climadd 15449 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ β²ππ & β’ β²ππΉ & β’ β²ππΊ & β’ β²ππ» & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β π΄) & β’ (π β π» β π) & β’ (π β πΊ β π΅) & β’ ((π β§ π β π) β (πΉβπ) β β) & β’ ((π β§ π β π) β (πΊβπ) β β) & β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ) + (πΊβπ))) β β’ (π β π» β (π΄ + π΅)) | ||
Theorem | mullimc 43579* | Limit of the product of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ πΊ = (π₯ β π΄ β¦ πΆ) & β’ π» = (π₯ β π΄ β¦ (π΅ Β· πΆ)) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ ((π β§ π₯ β π΄) β πΆ β β) & β’ (π β π β (πΉ limβ π·)) & β’ (π β π β (πΊ limβ π·)) β β’ (π β (π Β· π) β (π» limβ π·)) | ||
Theorem | ellimcabssub0 43580* | An equivalent condition for being a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ πΊ = (π₯ β π΄ β¦ (π΅ β πΆ)) & β’ (π β π΄ β β) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β π· β β) & β’ (π β πΆ β β) β β’ (π β (πΆ β (πΉ limβ π·) β 0 β (πΊ limβ π·))) | ||
Theorem | limcdm0 43581 | If a function has empty domain, every complex number is a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:β βΆβ) & β’ (π β π΅ β β) β β’ (π β (πΉ limβ π΅) = β) | ||
Theorem | islptre 43582* | 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 43583 | 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 43584 | 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 43585* | 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 43586* | Limit of the multiplication of two functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β πΉ:π΄βΆβ) & β’ (π β πΊ:π΄βΆβ) & β’ π» = (π₯ β π΄ β¦ ((πΉβπ₯) Β· (πΊβπ₯))) & β’ (π β π΅ β (πΉ limβ π·)) & β’ (π β πΆ β (πΊ limβ π·)) β β’ (π β (π΅ Β· πΆ) β (π» limβ π·)) | ||
Theorem | constlimc 43587* | Limit of constant function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β π΅ β (πΉ limβ πΆ)) | ||
Theorem | rexlim2d 43588* | 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 43589* | Limit of the identity function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ (π β π΄ β β) & β’ πΉ = (π₯ β π΄ β¦ π₯) & β’ (π β π β β) β β’ (π β π β (πΉ limβ π)) | ||
Theorem | divcnvg 43590* | The sequence of reciprocals of positive integers, multiplied by the factor π΄, converges to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β β β§ π β β) β (π β (β€β₯βπ) β¦ (π΄ / π)) β 0) | ||
Theorem | limcperiod 43591* | 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 43592 | 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 43593* | 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 43594 | 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 43595 | 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 43596 | A member of an unordered pair that is not the "first", must be the "second". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β {π΅, πΆ} β§ π΄ β π΅) β π΄ = πΆ) | ||
Theorem | elprn2 43597 | A member of an unordered pair that is not the "second", must be the "first". (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ ((π΄ β {π΅, πΆ} β§ π΄ β πΆ) β π΄ = π΅) | ||
Theorem | limcmptdm 43598* | The domain of a maps-to function with a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ ((π β§ π₯ β π΄) β π΅ β β) & β’ (π β πΆ β (πΉ limβ π·)) β β’ (π β π΄ β β) | ||
Theorem | clim2f 43599* | 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 43600 | 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β π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |