Home | Intuitionistic Logic Explorer Theorem List (p. 124 of 139) | < 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 | gzaddcl 12301 | The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | gzmulcl 12302 | The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | gzreim 12303 | Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.) |
Theorem | gzsubcl 12304 | The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | gzabssqcl 12305 | The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.) |
Theorem | 4sqlem5 12306 | Lemma for 4sq (not yet proved here). (Contributed by Mario Carneiro, 15-Jul-2014.) |
Theorem | 4sqlem6 12307 | Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.) |
Theorem | 4sqlem7 12308 | Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.) |
Theorem | 4sqlem8 12309 | Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.) |
Theorem | 4sqlem9 12310 | Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 15-Jul-2014.) |
Theorem | 4sqlem10 12311 | Lemma for 4sq (not yet proved here) . (Contributed by Mario Carneiro, 16-Jul-2014.) |
Theorem | 4sqlem1 12312* | Lemma for 4sq (not yet proved here) . The set is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that ; here we show one subset direction. (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | 4sqlem2 12313* | Lemma for 4sq (not yet proved here) . Change bound variables in . (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | 4sqlem3 12314* | Lemma for 4sq (not yet proved here) . Sufficient condition to be in . (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | 4sqlem4a 12315* | Lemma for 4sqlem4 12316. (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | 4sqlem4 12316* | Lemma for 4sq (not yet proved here) . We can express the four-square property more compactly in terms of gaussian integers, because the norms of gaussian integers are exactly sums of two squares. (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | mul4sqlem 12317* | Lemma for mul4sq 12318: algebraic manipulations. The extra assumptions involving would let us know not just that the product is a sum of squares, but also that it preserves divisibility by . (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | mul4sq 12318* | Euler's four-square identity: The product of two sums of four squares is also a sum of four squares. This is usually quoted as an explicit formula involving eight real variables; we save some time by working with complex numbers (gaussian integers) instead, so that we only have to work with four variables, and also hiding the actual formula for the product in the proof of mul4sqlem 12317. (For the curious, the explicit formula that is used is .) (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | oddennn 12319 | There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.) |
Theorem | evenennn 12320 | There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.) |
Theorem | xpnnen 12321 | 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 12322 | 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 12323 | The cartesian product of two sets dominated by is dominated by . (Contributed by Thierry Arnoux, 24-Sep-2017.) |
Theorem | unennn 12324 | The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.) |
Theorem | znnen 12325 | 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 12326* | Lemma for ennnfone 12352. A direct consequence of fidcenumlemrk 6913. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID DECID | ||
Theorem | ennnfonelemk 12327* | Lemma for ennnfone 12352. (Contributed by Jim Kingdon, 15-Jul-2023.) |
Theorem | ennnfonelemj0 12328* | Lemma for ennnfone 12352. Initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemjn 12329* | Lemma for ennnfone 12352. Non-initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemg 12330* | Lemma for ennnfone 12352. Closure for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemh 12331* | Lemma for ennnfone 12352. (Contributed by Jim Kingdon, 8-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelem0 12332* | Lemma for ennnfone 12352. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemp1 12333* | Lemma for ennnfone 12352. Value of at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelem1 12334* | Lemma for ennnfone 12352. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemom 12335* | Lemma for ennnfone 12352. yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhdmp1 12336* | Lemma for ennnfone 12352. 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 12337* | Lemma for ennnfone 12352. We only add elements to as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
Theorem | ennnfoneleminc 12338* | Lemma for ennnfone 12352. We only add elements to as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemkh 12339* | Lemma for ennnfone 12352. 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 12340* | Lemma for ennnfone 12352. 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 12341* | Lemma for ennnfone 12352. Extending the sequence to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemhom 12342* | Lemma for ennnfone 12352. 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 12343* | Lemma for ennnfone 12352. A consequence of ennnfonelemss 12337. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemfun 12344* | Lemma for ennnfone 12352. is a function. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemf1 12345* | Lemma for ennnfone 12352. is one-to-one. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemrn 12346* | Lemma for ennnfone 12352. is onto . (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemdm 12347* | Lemma for ennnfone 12352. The function is defined everywhere. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemen 12348* | Lemma for ennnfone 12352. The result. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
Theorem | ennnfonelemnn0 12349* | Lemma for ennnfone 12352. A version of ennnfonelemen 12348 expressed in terms of instead of . (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID frec | ||
Theorem | ennnfonelemr 12350* | Lemma for ennnfone 12352. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | ennnfonelemim 12351* | Lemma for ennnfone 12352. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
Theorem | ennnfone 12352* | 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 7068), 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 12353* | 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 12354* | Lemma for ctinfom 12355. Converting between and . (Contributed by Jim Kingdon, 10-Aug-2023.) |
frec | ||
Theorem | ctinfom 12355* | A condition for a set being countably infinite. Restates ennnfone 12352 in terms of and function image. Like ennnfone 12352 the condition can be summarized as being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | inffinp1 12356* | An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
Theorem | ctinf 12357* | 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 12358 | 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 12359* | Lemma for enct 12360. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
Theorem | enct 12360* | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
Theorem | ctiunctlemu1st 12361* | Lemma for ctiunct 12367. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemu2nd 12362* | Lemma for ctiunct 12367. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemuom 12363 | Lemma for ctiunct 12367. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemudc 12364* | Lemma for ctiunct 12367. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID DECID | ||
Theorem | ctiunctlemf 12365* | Lemma for ctiunct 12367. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunctlemfo 12366* | Lemma for ctiunct 12367. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
Theorem | ctiunct 12367* |
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. Theorem 8.1.19 of [AczelRathjen], p. 74.
For "countably many countable sets" the key hypothesis would be ⊔ . This is almost omiunct 12371 (which uses countable choice) although that is for a countably infinite collection not any countable collection. Compare with the case of two sets instead of countably many, as seen at unct 12369, which says that the union of two countable sets is countable . The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 12322) 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 7070 and ctssdc 7072. (Contributed by Jim Kingdon, 31-Oct-2023.) |
⊔ ⊔ ⊔ | ||
Theorem | ctiunctal 12368* | Variation of ctiunct 12367 which allows to be present in . (Contributed by Jim Kingdon, 5-May-2024.) |
⊔ ⊔ ⊔ | ||
Theorem | unct 12369* | The union of two countable sets is countable. Corollary 8.1.20 of [AczelRathjen], p. 75. (Contributed by Jim Kingdon, 1-Nov-2023.) |
⊔ ⊔ ⊔ | ||
Theorem | omctfn 12370* | Using countable choice to find a sequence of enumerations for a collection of countable sets. Lemma 8.1.27 of [AczelRathjen], p. 77. (Contributed by Jim Kingdon, 19-Apr-2024.) |
CCHOICE ⊔ ⊔ | ||
Theorem | omiunct 12371* | The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 12367 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.) |
CCHOICE ⊔ ⊔ | ||
Theorem | ssomct 12372* | A decidable subset of is countable. (Contributed by Jim Kingdon, 19-Sep-2024.) |
DECID ⊔ | ||
Theorem | ssnnctlemct 12373* | Lemma for ssnnct 12374. The result. (Contributed by Jim Kingdon, 29-Sep-2024.) |
frec DECID ⊔ | ||
Theorem | ssnnct 12374* | A decidable subset of is countable. (Contributed by Jim Kingdon, 29-Sep-2024.) |
DECID ⊔ | ||
Theorem | nninfdclemcl 12375* | Lemma for nninfdc 12380. (Contributed by Jim Kingdon, 25-Sep-2024.) |
DECID inf | ||
Theorem | nninfdclemf 12376* | Lemma for nninfdc 12380. A function from the natural numbers into . (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID inf | ||
Theorem | nninfdclemp1 12377* | Lemma for nninfdc 12380. Each element of the sequence is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.) |
DECID inf | ||
Theorem | nninfdclemlt 12378* | Lemma for nninfdc 12380. The function from nninfdclemf 12376 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.) |
DECID inf | ||
Theorem | nninfdclemf1 12379* | Lemma for nninfdc 12380. The function from nninfdclemf 12376 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID inf | ||
Theorem | nninfdc 12380* | An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID | ||
Theorem | unbendc 12381* | An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.) |
DECID | ||
Theorem | prminf 12382 | There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.) |
Theorem | infpn2 12383* | There exist infinitely many prime numbers: the set of all primes is unbounded by infpn 12285, so by unbendc 12381 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.) |
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 12412 and strslfv 12432. Using extractors makes it easier to change numeric indices and also makes the components' purpose clearer. See the comment of basendx 12442 for more details on numeric indices versus the structure component extractors. 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 12396. 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 12384 | Extend class notation with the class of structures with components numbered below . |
Struct | ||
Syntax | cnx 12385 | Extend class notation with the structure component index extractor. |
Syntax | csts 12386 | Set components of a structure. |
sSet | ||
Syntax | cslot 12387 | Extend class notation with the slot function. |
Slot | ||
Syntax | cbs 12388 | Extend class notation with the class of all base set extractors. |
Syntax | cress 12389 | Extend class notation with the extensible structure builder restriction operator. |
↾_{s} | ||
Definition | df-struct 12390* |
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 5203, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 12401: 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 3776). (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Definition | df-ndx 12391 | Define the structure component index extractor. See Theorem ndxarg 12411 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 12394) another set such as the set of finite ordinals (df-iom 4565). (Contributed by NM, 4-Sep-2011.) |
Definition | df-slot 12392* |
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 12411). 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 5503). 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 12393 | 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 12394 | 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 12395* | 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 12396 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 12396* |
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 12397 | The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.) |
Struct | ||
Theorem | isstruct2im 12398 | 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 12399 | 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 12400 | A structure is a set. (Contributed by AV, 10-Nov-2021.) |
Struct |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |