![]() |
Metamath
Proof Explorer Theorem List (p. 467 of 482) | < 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: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2leaddle2 46601 | If two real numbers are less than a third real number, the sum of the real numbers is less than twice the third real number. (Contributed by Alexander van der Vekens, 21-May-2018.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ถ โง ๐ต < ๐ถ) โ (๐ด + ๐ต) < (2 ยท ๐ถ))) | ||
Theorem | ltnltne 46602 | Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด < ๐ต โ (ยฌ ๐ต < ๐ด โง ยฌ ๐ต = ๐ด))) | ||
Theorem | p1lep2 46603 | A real number increasd by 1 is less than or equal to the number increased by 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
โข (๐ โ โ โ (๐ + 1) โค (๐ + 2)) | ||
Theorem | ltsubsubaddltsub 46604 | If the result of subtracting two numbers is greater than a number, the result of adding one of these subtracted numbers to the number is less than the result of subtracting the other subtracted number only. (Contributed by Alexander van der Vekens, 9-Jun-2018.) |
โข ((๐ฝ โ โ โง (๐ฟ โ โ โง ๐ โ โ โง ๐ โ โ)) โ (๐ฝ < ((๐ฟ โ ๐) โ ๐) โ (๐ฝ + ๐) < (๐ฟ โ ๐))) | ||
Theorem | zm1nn 46605 | An integer minus 1 is positive under certain circumstances. (Contributed by Alexander van der Vekens, 9-Jun-2018.) |
โข ((๐ โ โ0 โง ๐ฟ โ โค) โ ((๐ฝ โ โ โง 0 โค ๐ฝ โง ๐ฝ < ((๐ฟ โ ๐) โ 1)) โ (๐ฟ โ 1) โ โ)) | ||
Theorem | readdcnnred 46606 | The sum of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ (โ โ โ)) โ โข (๐ โ (๐ด + ๐ต) โ โ) | ||
Theorem | resubcnnred 46607 | The difference of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ (โ โ โ)) โ โข (๐ โ (๐ด โ ๐ต) โ โ) | ||
Theorem | recnmulnred 46608 | The product of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ (โ โ โ)) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (๐ด ยท ๐ต) โ โ) | ||
Theorem | cndivrenred 46609 | The quotient of an imaginary number and a real number is not a real number. (Contributed by AV, 23-Jan-2023.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ (โ โ โ)) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ (๐ต / ๐ด) โ โ) | ||
Theorem | sqrtnegnre 46610 | The square root of a negative number is not a real number. (Contributed by AV, 28-Feb-2023.) |
โข ((๐ โ โ โง ๐ < 0) โ (โโ๐) โ โ) | ||
Theorem | nn0resubcl 46611 | Closure law for subtraction of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
โข ((๐ด โ โ0 โง ๐ต โ โ0) โ (๐ด โ ๐ต) โ โ) | ||
Theorem | zgeltp1eq 46612 | If an integer is between another integer and its successor, the integer is equal to the other integer. (Contributed by AV, 30-May-2020.) |
โข ((๐ผ โ โค โง ๐ด โ โค) โ ((๐ด โค ๐ผ โง ๐ผ < (๐ด + 1)) โ ๐ผ = ๐ด)) | ||
Theorem | 1t10e1p1e11 46613 | 11 is 1 times 10 to the power of 1, plus 1. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
โข ;11 = ((1 ยท (;10โ1)) + 1) | ||
Theorem | deccarry 46614 | Add 1 to a 2 digit number with carry. This is a special case of decsucc 12740, but in closed form. As observed by ML, this theorem allows for carrying the 1 down multiple decimal constructors, so we can carry the 1 multiple times down a multi-digit number, e.g., by applying this theorem three times we get (;;999 + 1) = ;;;1000. (Contributed by AV, 4-Aug-2020.) (Revised by ML, 8-Aug-2020.) (Proof shortened by AV, 10-Sep-2021.) |
โข (๐ด โ โ โ (;๐ด9 + 1) = ;(๐ด + 1)0) | ||
Theorem | eluzge0nn0 46615 | If an integer is greater than or equal to a nonnegative integer, then it is a nonnegative integer. (Contributed by Alexander van der Vekens, 27-Aug-2018.) |
โข (๐ โ (โคโฅโ๐) โ (0 โค ๐ โ ๐ โ โ0)) | ||
Theorem | nltle2tri 46616 | Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020.) |
โข ((๐ด โ โ* โง ๐ต โ โ* โง ๐ถ โ โ*) โ ยฌ (๐ด < ๐ต โง ๐ต โค ๐ถ โง ๐ถ โค ๐ด)) | ||
Theorem | ssfz12 46617 | Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
โข ((๐พ โ โค โง ๐ฟ โ โค โง ๐พ โค ๐ฟ) โ ((๐พ...๐ฟ) โ (๐...๐) โ (๐ โค ๐พ โง ๐ฟ โค ๐))) | ||
Theorem | elfz2z 46618 | Membership of an integer in a finite set of sequential integers starting at 0. (Contributed by Alexander van der Vekens, 25-May-2018.) |
โข ((๐พ โ โค โง ๐ โ โค) โ (๐พ โ (0...๐) โ (0 โค ๐พ โง ๐พ โค ๐))) | ||
Theorem | 2elfz3nn0 46619 | If there are two elements in a finite set of sequential integers starting at 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018.) |
โข ((๐ด โ (0...๐) โง ๐ต โ (0...๐)) โ (๐ด โ โ0 โง ๐ต โ โ0 โง ๐ โ โ0)) | ||
Theorem | fz0addcom 46620 | The addition of two members of a finite set of sequential integers starting at 0 is commutative. (Contributed by Alexander van der Vekens, 22-May-2018.) (Revised by Alexander van der Vekens, 9-Jun-2018.) |
โข ((๐ด โ (0...๐) โง ๐ต โ (0...๐)) โ (๐ด + ๐ต) = (๐ต + ๐ด)) | ||
Theorem | 2elfz2melfz 46621 | If the sum of two integers of a 0-based finite set of sequential integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the 0-based finite set of sequential integers with the first integer as upper bound. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.) |
โข ((๐ด โ (0...๐) โง ๐ต โ (0...๐)) โ (๐ < (๐ด + ๐ต) โ (๐ต โ (๐ โ ๐ด)) โ (0...๐ด))) | ||
Theorem | fz0addge0 46622 | The sum of two integers in 0-based finite sets of sequential integers is greater than or equal to zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
โข ((๐ด โ (0...๐) โง ๐ต โ (0...๐)) โ 0 โค (๐ด + ๐ต)) | ||
Theorem | elfzlble 46623 | Membership of an integer in a finite set of sequential integers with the integer as upper bound and a lower bound less than or equal to the integer. (Contributed by AV, 21-Oct-2018.) |
โข ((๐ โ โค โง ๐ โ โ0) โ ๐ โ ((๐ โ ๐)...๐)) | ||
Theorem | elfzelfzlble 46624 | Membership of an element of a finite set of sequential integers in a finite set of sequential integers with the same upper bound and a lower bound less than the upper bound. (Contributed by AV, 21-Oct-2018.) |
โข ((๐ โ โค โง ๐พ โ (0...๐) โง ๐ < (๐ + ๐พ)) โ ๐พ โ ((๐ โ ๐)...๐)) | ||
Theorem | fzopred 46625 | Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 13745. (Contributed by AV, 14-Jul-2020.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐ < ๐) โ (๐..^๐) = ({๐} โช ((๐ + 1)..^๐))) | ||
Theorem | fzopredsuc 46626 | Join a predecessor and a successor to the beginning and the end of an open integer interval. This theorem holds even if ๐ = ๐ (then (๐...๐) = {๐} = ({๐} โช โ ) โช {๐}). (Contributed by AV, 14-Jul-2020.) |
โข (๐ โ (โคโฅโ๐) โ (๐...๐) = (({๐} โช ((๐ + 1)..^๐)) โช {๐})) | ||
Theorem | 1fzopredsuc 46627 | Join 0 and a successor to the beginning and the end of an open integer interval starting at 1. (Contributed by AV, 14-Jul-2020.) |
โข (๐ โ โ0 โ (0...๐) = (({0} โช (1..^๐)) โช {๐})) | ||
Theorem | el1fzopredsuc 46628 | An element of an open integer interval starting at 1 joined by 0 and a successor at the beginning and the end is either 0 or an element of the open integer interval or the successor. (Contributed by AV, 14-Jul-2020.) |
โข (๐ โ โ0 โ (๐ผ โ (0...๐) โ (๐ผ = 0 โจ ๐ผ โ (1..^๐) โจ ๐ผ = ๐))) | ||
Theorem | subsubelfzo0 46629 | Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.) |
โข ((๐ด โ (0..^๐) โง ๐ผ โ (0..^๐) โง ยฌ ๐ผ < (๐ โ ๐ด)) โ (๐ผ โ (๐ โ ๐ด)) โ (0..^๐ด)) | ||
Theorem | fzoopth 46630 | A half-open integer range can represent an ordered pair, analogous to fzopth 13562. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐ < ๐) โ ((๐..^๐) = (๐ฝ..^๐พ) โ (๐ = ๐ฝ โง ๐ = ๐พ))) | ||
Theorem | 2ffzoeq 46631* | Two functions over a half-open range of nonnegative integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
โข (((๐ โ โ0 โง ๐ โ โ0) โง (๐น:(0..^๐)โถ๐ โง ๐:(0..^๐)โถ๐)) โ (๐น = ๐ โ (๐ = ๐ โง โ๐ โ (0..^๐)(๐นโ๐) = (๐โ๐)))) | ||
Theorem | m1mod0mod1 46632 | An integer decreased by 1 is 0 modulo a positive integer iff the integer is 1 modulo the same modulus. (Contributed by AV, 6-Jun-2020.) |
โข ((๐ด โ โ โง ๐ โ โ โง 1 < ๐) โ (((๐ด โ 1) mod ๐) = 0 โ (๐ด mod ๐) = 1)) | ||
Theorem | elmod2 46633 | An integer modulo 2 is either 0 or 1. (Contributed by AV, 24-May-2020.) (Proof shortened by OpenAI, 3-Jul-2020.) |
โข (๐ โ โค โ (๐ mod 2) โ {0, 1}) | ||
Theorem | smonoord 46634* | Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord 14021 (except that the case ๐ = ๐ must be excluded). Duplicate of monoords 44602? (Contributed by AV, 12-Jul-2020.) |
โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ (โคโฅโ(๐ + 1))) & โข ((๐ โง ๐ โ (๐...๐)) โ (๐นโ๐) โ โ) & โข ((๐ โง ๐ โ (๐...(๐ โ 1))) โ (๐นโ๐) < (๐นโ(๐ + 1))) โ โข (๐ โ (๐นโ๐) < (๐นโ๐)) | ||
Theorem | fsummsndifre 46635* | A finite sum with one of its integer summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
โข ((๐ด โ Fin โง โ๐ โ ๐ด ๐ต โ โค) โ ฮฃ๐ โ (๐ด โ {๐})๐ต โ โ) | ||
Theorem | fsumsplitsndif 46636* | Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
โข ((๐ด โ Fin โง ๐ โ ๐ด โง โ๐ โ ๐ด ๐ต โ โค) โ ฮฃ๐ โ ๐ด ๐ต = (ฮฃ๐ โ (๐ด โ {๐})๐ต + โฆ๐ / ๐โฆ๐ต)) | ||
Theorem | fsummmodsndifre 46637* | A finite sum of summands modulo a positive number with one of its summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
โข ((๐ด โ Fin โง ๐ โ โ โง โ๐ โ ๐ด ๐ต โ โค) โ ฮฃ๐ โ (๐ด โ {๐})(๐ต mod ๐) โ โ) | ||
Theorem | fsummmodsnunz 46638* | A finite sum of summands modulo a positive number with an additional summand is an integer. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
โข ((๐ด โ Fin โง ๐ โ โ โง โ๐ โ (๐ด โช {๐ง})๐ต โ โค) โ ฮฃ๐ โ (๐ด โช {๐ง})(๐ต mod ๐) โ โค) | ||
Theorem | setsidel 46639 | The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.) |
โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ต โ ๐) & โข ๐ = (๐ sSet โจ๐ด, ๐ตโฉ) โ โข (๐ โ โจ๐ด, ๐ตโฉ โ ๐ ) | ||
Theorem | setsnidel 46640 | The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.) |
โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ต โ ๐) & โข ๐ = (๐ sSet โจ๐ด, ๐ตโฉ) & โข (๐ โ ๐ถ โ ๐) & โข (๐ โ ๐ท โ ๐) & โข (๐ โ โจ๐ถ, ๐ทโฉ โ ๐) & โข (๐ โ ๐ด โ ๐ถ) โ โข (๐ โ โจ๐ถ, ๐ทโฉ โ ๐ ) | ||
Theorem | setsv 46641 | The value of the structure replacement function is a set. (Contributed by AV, 10-Nov-2021.) |
โข ((๐ โ ๐ โง ๐ต โ ๐) โ (๐ sSet โจ๐ด, ๐ตโฉ) โ V) | ||
According to Wikipedia ("Image (mathematics)", 17-Mar-2024, https://en.wikipedia.org/wiki/ImageSupport_(mathematics)): "... evaluating a given function ๐ at each element of a given subset ๐ด of its domain produces a set, called the "image of ๐ด under (or through) ๐". Similarly, the inverse image (or preimage) of a given subset ๐ต of the codomain of ๐ is the set of all elements of the domain that map to the members of ๐ต." The preimage of a set ๐ต under a function ๐ is often denoted as "f^-1 (B)", but in set.mm, the idiom (โก๐ โ ๐ต) is used. As a special case, the idiom for the preimage of a function value at ๐ under a function ๐น is (โก๐น โ {(๐นโ๐)}) (according to Wikipedia, the preimage of a singleton is also called a "fiber"). We use the label fragment "preima" (as in mptpreima 6236) for theorems about preimages (sometimes, also "imacnv" is used as in fvimacnvi 7055), and "preimafv" (as in preimafvn0 46643) for theorems about preimages of a function value. In this section, ๐ = {๐ง โฃ โ๐ฅ โ ๐ด๐ง = (โก๐น โ {(๐นโ๐ฅ)})} will be the set of all preimages of function values of a function ๐น, that means ๐ โ ๐ is a preimage of a function value (see, for example, elsetpreimafv 46648): ๐ = (โก๐น โ {(๐นโ๐ฅ)}). With the help of such a set, it is shown that every function ๐น:๐ดโถ๐ต can be decomposed into a surjective and an injective function (see fundcmpsurinj 46672) by constructing a surjective function ๐:๐ดโontoโ๐ and an injective function โ:๐โ1-1โ๐ต so that ๐น = (โ โ ๐) ( see fundcmpsurinjpreimafv 46671). See also Wikipedia ("Surjective function", 17-Mar-2024, https://en.wikipedia.org/wiki/Surjective_function 46671 (section "Composition and decomposition"). This is different from the decomposition of ๐น into the surjective function ๐:๐ดโontoโ(๐น โ ๐ด) (with (๐โ๐ฅ) = (๐นโ๐ฅ) for ๐ฅ โ ๐ด) and the injective function โ = ( I โพ (๐น โ ๐ด)), ( see fundcmpsurinjimaid 46674), see also Wikipedia ("Bijection, injection and surjection", 17-Mar-2024, https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection 46674 (section "Properties"). Finally, it is shown that every function ๐น:๐ดโถ๐ต can be decomposed into a surjective, a bijective and an injective function (see fundcmpsurbijinj 46673), by showing that there is a bijection between the set of all preimages of values of a function and the range of the function (see imasetpreimafvbij 46669). From this, both variants of decompositions of a function into a surjective and an injective function can be derived: Let ๐น = ((๐ผ โ ๐ต) โ ๐) be a decomposition of a function into a surjective, a bijective and an injective function, then ๐น = (๐ฝ โ ๐) with ๐ฝ = (๐ผ โ ๐ต) (an injective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinj 46672, and ๐น = (๐ผ โ ๐) with ๐ = (๐ต โ ๐) (a surjective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinjimaid 46674. | ||
Theorem | preimafvsnel 46642 | The preimage of a function value at ๐ contains ๐. (Contributed by AV, 7-Mar-2024.) |
โข ((๐น Fn ๐ด โง ๐ โ ๐ด) โ ๐ โ (โก๐น โ {(๐นโ๐)})) | ||
Theorem | preimafvn0 46643 | The preimage of a function value is not empty. (Contributed by AV, 7-Mar-2024.) |
โข ((๐น Fn ๐ด โง ๐ โ ๐ด) โ (โก๐น โ {(๐นโ๐)}) โ โ ) | ||
Theorem | uniimafveqt 46644* | The union of the image of a subset ๐ of the domain of a function with elements having the same function value is the function value at one of the elements of ๐. (Contributed by AV, 5-Mar-2024.) |
โข ((๐น:๐ดโถ๐ต โง ๐ โ ๐ด โง ๐ โ ๐) โ (โ๐ฅ โ ๐ (๐นโ๐ฅ) = (๐นโ๐) โ โช (๐น โ ๐) = (๐นโ๐))) | ||
Theorem | uniimaprimaeqfv 46645 | The union of the image of the preimage of a function value is the function value. (Contributed by AV, 12-Mar-2024.) |
โข ((๐น Fn ๐ด โง ๐ โ ๐ด) โ โช (๐น โ (โก๐น โ {(๐นโ๐)})) = (๐นโ๐)) | ||
Theorem | setpreimafvex 46646* | The class ๐ of all preimages of function values is a set. (Contributed by AV, 10-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข (๐ด โ ๐ โ ๐ โ V) | ||
Theorem | elsetpreimafvb 46647* | The characterization of an element of the class ๐ of all preimages of function values. (Contributed by AV, 10-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข (๐ โ ๐ โ (๐ โ ๐ โ โ๐ฅ โ ๐ด ๐ = (โก๐น โ {(๐นโ๐ฅ)}))) | ||
Theorem | elsetpreimafv 46648* | An element of the class ๐ of all preimages of function values. (Contributed by AV, 8-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข (๐ โ ๐ โ โ๐ฅ โ ๐ด ๐ = (โก๐น โ {(๐นโ๐ฅ)})) | ||
Theorem | elsetpreimafvssdm 46649* | An element of the class ๐ of all preimages of function values is a subset of the domain of the function. (Contributed by AV, 8-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น Fn ๐ด โง ๐ โ ๐) โ ๐ โ ๐ด) | ||
Theorem | fvelsetpreimafv 46650* | There is an element in a preimage ๐ of function values so that ๐ is the preimage of the function value at this element. (Contributed by AV, 8-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น Fn ๐ด โง ๐ โ ๐) โ โ๐ฅ โ ๐ ๐ = (โก๐น โ {(๐นโ๐ฅ)})) | ||
Theorem | preimafvelsetpreimafv 46651* | The preimage of a function value is an element of the class ๐ of all preimages of function values. (Contributed by AV, 10-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น Fn ๐ด โง ๐ด โ ๐ โง ๐ โ ๐ด) โ (โก๐น โ {(๐นโ๐)}) โ ๐) | ||
Theorem | preimafvsspwdm 46652* | The class ๐ of all preimages of function values is a subset of the power set of the domain of the function. (Contributed by AV, 5-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข (๐น Fn ๐ด โ ๐ โ ๐ซ ๐ด) | ||
Theorem | 0nelsetpreimafv 46653* | The empty set is not an element of the class ๐ of all preimages of function values. (Contributed by AV, 6-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข (๐น Fn ๐ด โ โ โ ๐) | ||
Theorem | elsetpreimafvbi 46654* | An element of the preimage of a function value is an element of the domain of the function with the same value as another element of the preimage. (Contributed by AV, 9-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น Fn ๐ด โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ โ ๐ โ (๐ โ ๐ด โง (๐นโ๐) = (๐นโ๐)))) | ||
Theorem | elsetpreimafveqfv 46655* | The elements of the preimage of a function value have the same function values. (Contributed by AV, 5-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น Fn ๐ด โง (๐ โ ๐ โง ๐ โ ๐ โง ๐ โ ๐)) โ (๐นโ๐) = (๐นโ๐)) | ||
Theorem | eqfvelsetpreimafv 46656* | If an element of the domain of the function has the same function value as an element of the preimage of a function value, then it is an element of the same preimage. (Contributed by AV, 9-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น Fn ๐ด โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐ โ ๐ด โง (๐นโ๐) = (๐นโ๐)) โ ๐ โ ๐)) | ||
Theorem | elsetpreimafvrab 46657* | An element of the preimage of a function value expressed as a restricted class abstraction. (Contributed by AV, 9-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น Fn ๐ด โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ = {๐ฅ โ ๐ด โฃ (๐นโ๐ฅ) = (๐นโ๐)}) | ||
Theorem | imaelsetpreimafv 46658* | The image of an element of the preimage of a function value is the singleton consisting of the function value at one of its elements. (Contributed by AV, 5-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น Fn ๐ด โง ๐ โ ๐ โง ๐ โ ๐) โ (๐น โ ๐) = {(๐นโ๐)}) | ||
Theorem | uniimaelsetpreimafv 46659* | The union of the image of an element of the preimage of a function value is an element of the range of the function. (Contributed by AV, 5-Mar-2024.) (Revised by AV, 22-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น Fn ๐ด โง ๐ โ ๐) โ โช (๐น โ ๐) โ ran ๐น) | ||
Theorem | elsetpreimafveq 46660* | If two preimages of function values contain elements with identical function values, then both preimages are equal. (Contributed by AV, 8-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น Fn ๐ด โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐ )) โ ((๐นโ๐) = (๐นโ๐) โ ๐ = ๐ )) | ||
Theorem | fundcmpsurinjlem1 46661* | Lemma 1 for fundcmpsurinj 46672. (Contributed by AV, 4-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} & โข ๐บ = (๐ฅ โ ๐ด โฆ (โก๐น โ {(๐นโ๐ฅ)})) โ โข ran ๐บ = ๐ | ||
Theorem | fundcmpsurinjlem2 46662* | Lemma 2 for fundcmpsurinj 46672. (Contributed by AV, 4-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} & โข ๐บ = (๐ฅ โ ๐ด โฆ (โก๐น โ {(๐นโ๐ฅ)})) โ โข ((๐น Fn ๐ด โง ๐ด โ ๐) โ ๐บ:๐ดโontoโ๐) | ||
Theorem | fundcmpsurinjlem3 46663* | Lemma 3 for fundcmpsurinj 46672. (Contributed by AV, 3-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} & โข ๐ป = (๐ โ ๐ โฆ โช (๐น โ ๐)) โ โข ((Fun ๐น โง ๐ โ ๐) โ (๐ปโ๐) = โช (๐น โ ๐)) | ||
Theorem | imasetpreimafvbijlemf 46664* | Lemma for imasetpreimafvbij 46669: the mapping ๐ป is a function into the range of function ๐น. (Contributed by AV, 22-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} & โข ๐ป = (๐ โ ๐ โฆ โช (๐น โ ๐)) โ โข (๐น Fn ๐ด โ ๐ป:๐โถ(๐น โ ๐ด)) | ||
Theorem | imasetpreimafvbijlemfv 46665* | Lemma for imasetpreimafvbij 46669: the value of the mapping ๐ป at a preimage of a value of function ๐น. (Contributed by AV, 5-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} & โข ๐ป = (๐ โ ๐ โฆ โช (๐น โ ๐)) โ โข ((๐น Fn ๐ด โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ปโ๐) = (๐นโ๐)) | ||
Theorem | imasetpreimafvbijlemfv1 46666* | Lemma for imasetpreimafvbij 46669: for a preimage of a value of function ๐น there is an element of the preimage so that the value of the mapping ๐ป at this preimage is the function value at this element. (Contributed by AV, 5-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} & โข ๐ป = (๐ โ ๐ โฆ โช (๐น โ ๐)) โ โข ((๐น Fn ๐ด โง ๐ โ ๐) โ โ๐ฆ โ ๐ (๐ปโ๐) = (๐นโ๐ฆ)) | ||
Theorem | imasetpreimafvbijlemf1 46667* | Lemma for imasetpreimafvbij 46669: the mapping ๐ป is an injective function into the range of function ๐น. (Contributed by AV, 9-Mar-2024.) (Revised by AV, 22-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} & โข ๐ป = (๐ โ ๐ โฆ โช (๐น โ ๐)) โ โข (๐น Fn ๐ด โ ๐ป:๐โ1-1โ(๐น โ ๐ด)) | ||
Theorem | imasetpreimafvbijlemfo 46668* | Lemma for imasetpreimafvbij 46669: the mapping ๐ป is a function onto the range of function ๐น. (Contributed by AV, 22-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} & โข ๐ป = (๐ โ ๐ โฆ โช (๐น โ ๐)) โ โข ((๐น Fn ๐ด โง ๐ด โ ๐) โ ๐ป:๐โontoโ(๐น โ ๐ด)) | ||
Theorem | imasetpreimafvbij 46669* | The mapping ๐ป is a bijective function betwen the set ๐ of all preimages of values of function ๐น and the range of ๐น. (Contributed by AV, 22-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} & โข ๐ป = (๐ โ ๐ โฆ โช (๐น โ ๐)) โ โข ((๐น Fn ๐ด โง ๐ด โ ๐) โ ๐ป:๐โ1-1-ontoโ(๐น โ ๐ด)) | ||
Theorem | fundcmpsurbijinjpreimafv 46670* | Every function ๐น:๐ดโถ๐ต can be decomposed into a surjective function onto ๐, a bijective function from ๐ and an injective function into the codomain of ๐น. (Contributed by AV, 22-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น:๐ดโถ๐ต โง ๐ด โ ๐) โ โ๐โโโ๐((๐:๐ดโontoโ๐ โง โ:๐โ1-1-ontoโ(๐น โ ๐ด) โง ๐:(๐น โ ๐ด)โ1-1โ๐ต) โง ๐น = ((๐ โ โ) โ ๐))) | ||
Theorem | fundcmpsurinjpreimafv 46671* | Every function ๐น:๐ดโถ๐ต can be decomposed into a surjective function onto ๐ and an injective function from ๐. (Contributed by AV, 12-Mar-2024.) (Proof shortened by AV, 22-Mar-2024.) |
โข ๐ = {๐ง โฃ โ๐ฅ โ ๐ด ๐ง = (โก๐น โ {(๐นโ๐ฅ)})} โ โข ((๐น:๐ดโถ๐ต โง ๐ด โ ๐) โ โ๐โโ(๐:๐ดโontoโ๐ โง โ:๐โ1-1โ๐ต โง ๐น = (โ โ ๐))) | ||
Theorem | fundcmpsurinj 46672* | Every function ๐น:๐ดโถ๐ต can be decomposed into a surjective and an injective function. (Contributed by AV, 13-Mar-2024.) |
โข ((๐น:๐ดโถ๐ต โง ๐ด โ ๐) โ โ๐โโโ๐(๐:๐ดโontoโ๐ โง โ:๐โ1-1โ๐ต โง ๐น = (โ โ ๐))) | ||
Theorem | fundcmpsurbijinj 46673* | Every function ๐น:๐ดโถ๐ต can be decomposed into a surjective, a bijective and an injective function. (Contributed by AV, 23-Mar-2024.) |
โข ((๐น:๐ดโถ๐ต โง ๐ด โ ๐) โ โ๐โโโ๐โ๐โ๐((๐:๐ดโontoโ๐ โง โ:๐โ1-1-ontoโ๐ โง ๐:๐โ1-1โ๐ต) โง ๐น = ((๐ โ โ) โ ๐))) | ||
Theorem | fundcmpsurinjimaid 46674* | Every function ๐น:๐ดโถ๐ต can be decomposed into a surjective function onto the image (๐น โ ๐ด) of the domain of ๐น and an injective function from the image (๐น โ ๐ด). (Contributed by AV, 17-Mar-2024.) |
โข ๐ผ = (๐น โ ๐ด) & โข ๐บ = (๐ฅ โ ๐ด โฆ (๐นโ๐ฅ)) & โข ๐ป = ( I โพ ๐ผ) โ โข (๐น:๐ดโถ๐ต โ (๐บ:๐ดโontoโ๐ผ โง ๐ป:๐ผโ1-1โ๐ต โง ๐น = (๐ป โ ๐บ))) | ||
Theorem | fundcmpsurinjALT 46675* | Alternate proof of fundcmpsurinj 46672, based on fundcmpsurinjimaid 46674: Every function ๐น:๐ดโถ๐ต can be decomposed into a surjective and an injective function. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by AV, 13-Mar-2024.) |
โข ((๐น:๐ดโถ๐ต โง ๐ด โ ๐) โ โ๐โโโ๐(๐:๐ดโontoโ๐ โง โ:๐โ1-1โ๐ต โง ๐น = (โ โ ๐))) | ||
Based on the theorems of the fourierdlem* series of GS's mathbox. | ||
Syntax | ciccp 46676 | Extend class notation with the partitions of a closed interval of extended reals. |
class RePart | ||
Definition | df-iccp 46677* | Define partitions of a closed interval of extended reals. Such partitions are finite increasing sequences of extended reals. (Contributed by AV, 8-Jul-2020.) |
โข RePart = (๐ โ โ โฆ {๐ โ (โ* โm (0...๐)) โฃ โ๐ โ (0..^๐)(๐โ๐) < (๐โ(๐ + 1))}) | ||
Theorem | iccpval 46678* | Partition consisting of a fixed number ๐ of parts. (Contributed by AV, 9-Jul-2020.) |
โข (๐ โ โ โ (RePartโ๐) = {๐ โ (โ* โm (0...๐)) โฃ โ๐ โ (0..^๐)(๐โ๐) < (๐โ(๐ + 1))}) | ||
Theorem | iccpart 46679* | A special partition. Corresponds to fourierdlem2 45420 in GS's mathbox. (Contributed by AV, 9-Jul-2020.) |
โข (๐ โ โ โ (๐ โ (RePartโ๐) โ (๐ โ (โ* โm (0...๐)) โง โ๐ โ (0..^๐)(๐โ๐) < (๐โ(๐ + 1))))) | ||
Theorem | iccpartimp 46680 | Implications for a class being a partition. (Contributed by AV, 11-Jul-2020.) |
โข ((๐ โ โ โง ๐ โ (RePartโ๐) โง ๐ผ โ (0..^๐)) โ (๐ โ (โ* โm (0...๐)) โง (๐โ๐ผ) < (๐โ(๐ผ + 1)))) | ||
Theorem | iccpartres 46681 | The restriction of a partition is a partition. (Contributed by AV, 16-Jul-2020.) |
โข ((๐ โ โ โง ๐ โ (RePartโ(๐ + 1))) โ (๐ โพ (0...๐)) โ (RePartโ๐)) | ||
Theorem | iccpartxr 46682 | If there is a partition, then all intermediate points and bounds are extended real numbers. (Contributed by AV, 11-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) & โข (๐ โ ๐ผ โ (0...๐)) โ โข (๐ โ (๐โ๐ผ) โ โ*) | ||
Theorem | iccpartgtprec 46683 | If there is a partition, then all intermediate points and the upper bound are strictly greater than the preceeding intermediate points or lower bound. (Contributed by AV, 11-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) & โข (๐ โ ๐ผ โ (1...๐)) โ โข (๐ โ (๐โ(๐ผ โ 1)) < (๐โ๐ผ)) | ||
Theorem | iccpartipre 46684 | If there is a partition, then all intermediate points are real numbers. (Contributed by AV, 11-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) & โข (๐ โ ๐ผ โ (1..^๐)) โ โข (๐ โ (๐โ๐ผ) โ โ) | ||
Theorem | iccpartiltu 46685* | If there is a partition, then all intermediate points are strictly less than the upper bound. (Contributed by AV, 12-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ โ๐ โ (1..^๐)(๐โ๐) < (๐โ๐)) | ||
Theorem | iccpartigtl 46686* | If there is a partition, then all intermediate points are strictly greater than the lower bound. (Contributed by AV, 12-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ โ๐ โ (1..^๐)(๐โ0) < (๐โ๐)) | ||
Theorem | iccpartlt 46687 | If there is a partition, then the lower bound is strictly less than the upper bound. Corresponds to fourierdlem11 45429 in GS's mathbox. (Contributed by AV, 12-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ (๐โ0) < (๐โ๐)) | ||
Theorem | iccpartltu 46688* | If there is a partition, then all intermediate points and the lower bound are strictly less than the upper bound. (Contributed by AV, 14-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ โ๐ โ (0..^๐)(๐โ๐) < (๐โ๐)) | ||
Theorem | iccpartgtl 46689* | If there is a partition, then all intermediate points and the upper bound are strictly greater than the lower bound. (Contributed by AV, 14-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ โ๐ โ (1...๐)(๐โ0) < (๐โ๐)) | ||
Theorem | iccpartgt 46690* | If there is a partition, then all intermediate points and the bounds are strictly ordered. (Contributed by AV, 18-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ โ๐ โ (0...๐)โ๐ โ (0...๐)(๐ < ๐ โ (๐โ๐) < (๐โ๐))) | ||
Theorem | iccpartleu 46691* | If there is a partition, then all intermediate points and the lower and the upper bound are less than or equal to the upper bound. (Contributed by AV, 14-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ โ๐ โ (0...๐)(๐โ๐) โค (๐โ๐)) | ||
Theorem | iccpartgel 46692* | If there is a partition, then all intermediate points and the upper and the lower bound are greater than or equal to the lower bound. (Contributed by AV, 14-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ โ๐ โ (0...๐)(๐โ0) โค (๐โ๐)) | ||
Theorem | iccpartrn 46693 | If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ ran ๐ โ ((๐โ0)[,](๐โ๐))) | ||
Theorem | iccpartf 46694 | The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 45433 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 14-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ ๐:(0...๐)โถ((๐โ0)[,](๐โ๐))) | ||
Theorem | iccpartel 46695 | If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข ((๐ โง ๐ผ โ (0...๐)) โ (๐โ๐ผ) โ ((๐โ0)[,](๐โ๐))) | ||
Theorem | iccelpart 46696* | An element of any partitioned half-open interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020.) |
โข (๐ โ โ โ โ๐ โ (RePartโ๐)(๐ โ ((๐โ0)[,)(๐โ๐)) โ โ๐ โ (0..^๐)๐ โ ((๐โ๐)[,)(๐โ(๐ + 1))))) | ||
Theorem | iccpartiun 46697* | A half-open interval of extended reals is the union of the parts of its partition. (Contributed by AV, 18-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ ((๐โ0)[,)(๐โ๐)) = โช ๐ โ (0..^๐)((๐โ๐)[,)(๐โ(๐ + 1)))) | ||
Theorem | icceuelpartlem 46698 | Lemma for icceuelpart 46699. (Contributed by AV, 19-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐)) โ (๐ผ < ๐ฝ โ (๐โ(๐ผ + 1)) โค (๐โ๐ฝ)))) | ||
Theorem | icceuelpart 46699* | An element of a partitioned half-open interval of extended reals is an element of exactly one part of the partition. (Contributed by AV, 19-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข ((๐ โง ๐ โ ((๐โ0)[,)(๐โ๐))) โ โ!๐ โ (0..^๐)๐ โ ((๐โ๐)[,)(๐โ(๐ + 1)))) | ||
Theorem | iccpartdisj 46700* | The segments of a partitioned half-open interval of extended reals are a disjoint collection. (Contributed by AV, 19-Jul-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ (RePartโ๐)) โ โข (๐ โ Disj ๐ โ (0..^๐)((๐โ๐)[,)(๐โ(๐ + 1)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |