Home | Intuitionistic Logic Explorer Theorem List (p. 119 of 132) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | phicl2 11801 | Bounds and closure for the value of the Euler function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Theorem | phicl 11802 | Closure for the value of the Euler function. (Contributed by Mario Carneiro, 28-Feb-2014.) |
Theorem | phibndlem 11803* | Lemma for phibnd 11804. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Theorem | phibnd 11804 | A slightly tighter bound on the value of the Euler function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Theorem | phicld 11805 | Closure for the value of the Euler function. (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | phi1 11806 | Value of the Euler function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Theorem | dfphi2 11807* | Alternate definition of the Euler function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 2-May-2016.) |
♯ ..^ | ||
Theorem | hashdvds 11808* | The number of numbers in a given residue class in a finite set of integers. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 7-Jun-2016.) |
♯ | ||
Theorem | phiprmpw 11809 | Value of the Euler function at a prime power. Theorem 2.5(a) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.) |
Theorem | phiprm 11810 | Value of the Euler function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.) |
Theorem | crth 11811* | The Chinese Remainder Theorem: the function that maps to its remainder classes and is 1-1 and onto when and are coprime. (Contributed by Mario Carneiro, 24-Feb-2014.) (Proof shortened by Mario Carneiro, 2-May-2016.) |
..^ ..^ ..^ | ||
Theorem | phimullem 11812* | Lemma for phimul 11813. (Contributed by Mario Carneiro, 24-Feb-2014.) |
..^ ..^ ..^ ..^ ..^ | ||
Theorem | phimul 11813 | The Euler function is a multiplicative function, meaning that it distributes over multiplication at relatively prime arguments. Theorem 2.5(c) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.) |
Theorem | hashgcdlem 11814* | A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
..^ ..^ | ||
Theorem | hashgcdeq 11815* | Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
♯ ..^ | ||
Theorem | oddennn 11816 | There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.) |
Theorem | evenennn 11817 | There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.) |
Theorem | xpnnen 11818 | The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.) |
Theorem | xpomen 11819 | The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.) |
Theorem | xpct 11820 | The cartesian product of two sets dominated by is dominated by . (Contributed by Thierry Arnoux, 24-Sep-2017.) |
Theorem | unennn 11821 | The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.) |
Theorem | znnen 11822 | The set of integers and the set of positive integers are equinumerous. Corollary 8.1.23 of [AczelRathjen], p. 75. (Contributed by NM, 31-Jul-2004.) |
Theorem | ennnfonelemdc 11823* | Lemma for ennnfone 11849. A direct consequence of fidcenumlemrk 6810. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID DECID | ||
Theorem | ennnfonelemk 11824* | Lemma for ennnfone 11849. (Contributed by Jim Kingdon, 15-Jul-2023.) |
Theorem | ennnfonelemj0 11825* | Lemma for ennnfone 11849. Initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemjn 11826* | Lemma for ennnfone 11849. Non-initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemg 11827* | Lemma for ennnfone 11849. Closure for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemh 11828* | Lemma for ennnfone 11849. (Contributed by Jim Kingdon, 8-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelem0 11829* | Lemma for ennnfone 11849. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemp1 11830* | Lemma for ennnfone 11849. Value of at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelem1 11831* | Lemma for ennnfone 11849. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemom 11832* | Lemma for ennnfone 11849. yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhdmp1 11833* | Lemma for ennnfone 11849. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemss 11834* | Lemma for ennnfone 11849. We only add elements to as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
Theorem | ennnfoneleminc 11835* | Lemma for ennnfone 11849. We only add elements to as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemkh 11836* | Lemma for ennnfone 11849. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhf1o 11837* | Lemma for ennnfone 11849. Each of the functions in is one to one and onto an image of . (Contributed by Jim Kingdon, 17-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemex 11838* | Lemma for ennnfone 11849. Extending the sequence to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhom 11839* | Lemma for ennnfone 11849. The sequences in increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemrnh 11840* | Lemma for ennnfone 11849. A consequence of ennnfonelemss 11834. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemfun 11841* | Lemma for ennnfone 11849. is a function. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemf1 11842* | Lemma for ennnfone 11849. is one-to-one. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemrn 11843* | Lemma for ennnfone 11849. is onto . (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemdm 11844* | Lemma for ennnfone 11849. The function is defined everywhere. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemen 11845* | Lemma for ennnfone 11849. The result. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemnn0 11846* | Lemma for ennnfone 11849. A version of ennnfonelemen 11845 expressed in terms of instead of . (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID frec | ||
Theorem | ennnfonelemr 11847* | Lemma for ennnfone 11849. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | ennnfonelemim 11848* | Lemma for ennnfone 11849. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | ennnfone 11849* | A condition for a set being countably infinite. Corollary 8.1.13 of [AczelRathjen], p. 73. Roughly speaking, the condition says that is countable (that's the part, as seen in theorems like ctm 6962), infinite (that's the part about being able to find an element of distinct from any mapping of a natural number via ), and has decidable equality. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | exmidunben 11850* | If any unbounded set of positive integers is equinumerous to , then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.) |
Omni EXMID | ||
Theorem | ctinfomlemom 11851* | Lemma for ctinfom 11852. Converting between and . (Contributed by Jim Kingdon, 10-Aug-2023.) |
frec | ||
Theorem | ctinfom 11852* | A condition for a set being countably infinite. Restates ennnfone 11849 in terms of and function image. Like ennnfone 11849 the condition can be summarized as being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | inffinp1 11853* | An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | ctinf 11854* | A set is countably infinite if and only if it has decidable equality, is countable, and is infinite. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | qnnen 11855 | The rational numbers are countably infinite. Corollary 8.1.23 of [AczelRathjen], p. 75. This is Metamath 100 proof #3. (Contributed by Jim Kingdon, 11-Aug-2023.) |
Theorem | enctlem 11856* | Lemma for enct 11857. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
Theorem | enct 11857* | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
Theorem | ctiunctlemu1st 11858* | Lemma for ctiunct 11864. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemu2nd 11859* | Lemma for ctiunct 11864. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemuom 11860 | Lemma for ctiunct 11864. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemudc 11861* | Lemma for ctiunct 11864. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID DECID | ||
Theorem | ctiunctlemf 11862* | Lemma for ctiunct 11864. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemfo 11863* | Lemma for ctiunct 11864. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunct 11864* |
A sequence of enumerations gives an enumeration of the union. We refer
to "sequence of enumerations" rather than "countably many
countable
sets" because the hypothesis provides more than countability for
each
: it refers to together with the
which enumerates it.
The "countably many countable sets" version could be expressed as ⊔ and countable choice would be needed to derive the current hypothesis from that. Compare with the case of two sets instead of countably many, as seen at unct 11865, in which case we express countability using . The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 11819) and using the first number to map to an element of and the second number to map to an element of B(x) . In this way we are able to map to every element of . Although it would be possible to work directly with countability expressed as ⊔ , we instead use functions from subsets of the natural numbers via ctssdccl 6964 and ctssdc 6966. (Contributed by Jim Kingdon, 31-Oct-2023.) |
⊔ ⊔ ⊔ | ||
Theorem | unct 11865* | The union of two countable sets is countable. (Contributed by Jim Kingdon, 1-Nov-2023.) |
⊔ ⊔ ⊔ | ||
An "extensible structure" (or "structure" in short, at least in this section) is used to define a specific group, ring, poset, and so on. An extensible structure can contain many components. For example, a group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This extensible structure approach allows theorems from more general structures (such as groups) to be reused for more specialized structures (such as rings) without having to reprove anything. Structures are common in mathematics, but in informal (natural language) proofs the details are assumed in ways that we must make explicit. An extensible structure is implemented as a function (a set of ordered pairs) on a finite (and not necessarily sequential) subset of . The function's argument is the index of a structure component (such as for the base set of a group), and its value is the component (such as the base set). By convention, we normally avoid direct reference to the hard-coded numeric index and instead use structure component extractors such as ndxid 11894 and strslfv 11914. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. There are many other possible ways to handle structures. We chose this extensible structure approach because this approach (1) results in simpler notation than other approaches we are aware of, and (2) is easier to do proofs with. We cannot use an approach that uses "hidden" arguments; Metamath does not support hidden arguments, and in any case we want nothing hidden. It would be possible to use a categorical approach (e.g., something vaguely similar to Lean's mathlib). However, instances (the chain of proofs that an is a via a bunch of forgetful functors) can cause serious performance problems for automated tooling, and the resulting proofs would be painful to look at directly (in the case of Lean, they are long past the level where people would find it acceptable to look at them directly). Metamath is working under much stricter conditions than this, and it has still managed to achieve about the same level of flexibility through this "extensible structure" approach. To create a substructure of a given extensible structure, you can simply use the multifunction restriction operator for extensible structures ↾s as defined in df-ress 11878. This can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the set while leaving operators alone. Individual kinds of structures will need to handle this behavior by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use. Extensible structures only work well when they represent concrete categories, where there is a "base set", morphisms are functions, and subobjects are subsets with induced operations. In short, they primarily work well for "sets with (some) extra structure". Extensible structures may not suffice for more complicated situations. For example, in manifolds, ↾s would not work. That said, extensible structures are sufficient for many of the structures that set.mm currently considers, and offer a good compromise for a goal-oriented formalization. | ||
Syntax | cstr 11866 | Extend class notation with the class of structures with components numbered below . |
Struct | ||
Syntax | cnx 11867 | Extend class notation with the structure component index extractor. |
Syntax | csts 11868 | Set components of a structure. |
sSet | ||
Syntax | cslot 11869 | Extend class notation with the slot function. |
Slot | ||
Syntax | cbs 11870 | Extend class notation with the class of all base set extractors. |
Syntax | cress 11871 | Extend class notation with the extensible structure builder restriction operator. |
↾s | ||
Definition | df-struct 11872* |
Define a structure with components in . This is
not a
requirement for groups, posets, etc., but it is a useful assumption for
component extraction theorems.
As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set to be extensible structures. Because of 0nelfun 5111, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 11883: Struct . Allowing an extensible structure to contain the empty set ensures that expressions like are structures without asserting or implying that , , and are sets (if or is a proper class, then , see opprc 3696). (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Definition | df-ndx 11873 | Define the structure component index extractor. See theorem ndxarg 11893 to understand its purpose. The restriction to ensures that is a set. The restriction to some set is necessary since is a proper class. In principle, we could have chosen or (if we revise all structure component definitions such as df-base 11876) another set such as the set of finite ordinals (df-iom 4475). (Contributed by NM, 4-Sep-2011.) |
Definition | df-slot 11874* |
Define the slot extractor for extensible structures. The class
Slot is a
function whose argument can be any set, although it is
meaningful only if that set is a member of an extensible structure (such
as a partially ordered set or a group).
Note that Slot is implemented as "evaluation at ". That is, Slot is defined to be , where will typically be a small nonzero natural number. Each extensible structure is a function defined on specific natural number "slots", and this function extracts the value at a particular slot. The special "structure" , defined as the identity function restricted to , can be used to extract the number from a slot, since Slot (see ndxarg 11893). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression in theorems and proofs instead of its value 1). The class Slot cannot be defined as because each Slot is a function on the proper class so is itself a proper class, and the values of functions are sets (fvex 5409). It is necessary to allow proper classes as values of Slot since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.) |
Slot | ||
Theorem | sloteq 11875 | Equality theorem for the Slot construction. The converse holds if (or ) is a set. (Contributed by BJ, 27-Dec-2021.) |
Slot Slot | ||
Definition | df-base 11876 | Define the base set (also called underlying set, ground set, carrier set, or carrier) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
Slot | ||
Definition | df-sets 11877* | Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-ress 11878 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. (Contributed by Mario Carneiro, 1-Dec-2014.) |
sSet | ||
Definition | df-ress 11878* |
Define a multifunction restriction operator for extensible structures,
which can be used to turn statements about rings into statements about
subrings, modules into submodules, etc. This definition knows nothing
about individual structures and merely truncates the set while
leaving operators alone; individual kinds of structures will need to
handle this behavior, by ignoring operators' values outside the range,
defining a function using the base set and applying that, or explicitly
truncating the slot before use.
(Credit for this operator goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.) |
↾s sSet | ||
Theorem | brstruct 11879 | The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Theorem | isstruct2im 11880 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | isstruct2r 11881 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | structex 11882 | A structure is a set. (Contributed by AV, 10-Nov-2021.) |
Struct | ||
Theorem | structn0fun 11883 | A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.) |
Struct | ||
Theorem | isstructim 11884 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | isstructr 11885 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
Theorem | structcnvcnv 11886 | Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Theorem | structfung 11887 | The converse of the converse of a structure is a function. Closed form of structfun 11888. (Contributed by AV, 12-Nov-2021.) |
Struct | ||
Theorem | structfun 11888 | Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.) |
Struct | ||
Theorem | structfn 11889 | Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Theorem | strnfvnd 11890 | Deduction version of strnfvn 11891. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.) |
Slot | ||
Theorem | strnfvn 11891 |
Value of a structure component extractor . Normally, is a
defined constant symbol such as (df-base 11876) and is a
fixed integer such as . is a
structure, i.e. a specific
member of a class of structures.
Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 11914. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.) |
Slot | ||
Theorem | strfvssn 11892 | A structure component extractor produces a value which is contained in a set dependent on , but not . This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.) |
Slot | ||
Theorem | ndxarg 11893 | Get the numeric argument from a defined structure component extractor such as df-base 11876. (Contributed by Mario Carneiro, 6-Oct-2013.) |
Slot | ||
Theorem | ndxid 11894 |
A structure component extractor is defined by its own index. This
theorem, together with strslfv 11914 below, is useful for avoiding direct
reference to the hard-coded numeric index in component extractor
definitions, such as the in df-base 11876, making it easier to change
should the need arise.
(Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.) |
Slot Slot | ||
Theorem | ndxslid 11895 | A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 11914. (Contributed by Jim Kingdon, 29-Jan-2023.) |
Slot Slot | ||
Theorem | slotslfn 11896 | A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.) |
Slot | ||
Theorem | slotex 11897 | Existence of slot value. A corollary of slotslfn 11896. (Contributed by Jim Kingdon, 12-Feb-2023.) |
Slot | ||
Theorem | strndxid 11898 | The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.) |
Slot | ||
Theorem | reldmsets 11899 | The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
sSet | ||
Theorem | setsvalg 11900 | Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
sSet |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |