Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
26-Aug-2020 | sqrt0rlem 9192 | Lemma for sqrt0 9193. (Contributed by Jim Kingdon, 26-Aug-2020.) |
23-Aug-2020 | sqrtrval 9189 | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
23-Aug-2020 | df-rsqrt 9187 |
Define a function whose value is the square root of a nonnegative real
number.
Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.) |
19-Aug-2020 | addnqpr 6541 | Addition of fractions embedded into positive reals. One can either add the fractions as fractions, or embed them into positive reals and add them as positive reals, and get the same result. (Contributed by Jim Kingdon, 19-Aug-2020.) |
19-Aug-2020 | addnqprlemfu 6540 | Lemma for addnqpr 6541. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
19-Aug-2020 | addnqprlemfl 6539 | Lemma for addnqpr 6541. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
19-Aug-2020 | addnqprlemru 6538 | Lemma for addnqpr 6541. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
19-Aug-2020 | addnqprlemrl 6537 | Lemma for addnqpr 6541. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
15-Aug-2020 | cauappcvgprlemcan 6615 | Lemma for cauappcvgprlemladdrl 6628. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.) |
4-Aug-2020 | cauappcvgprlemupu 6620 | Lemma for cauappcvgpr 6633. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) |
4-Aug-2020 | cauappcvgprlemopu 6619 | Lemma for cauappcvgpr 6633. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
4-Aug-2020 | cauappcvgprlemlol 6618 | Lemma for cauappcvgpr 6633. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) |
4-Aug-2020 | cauappcvgprlemopl 6617 | Lemma for cauappcvgpr 6633. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
18-Jul-2020 | cauappcvgprlemloc 6623 | Lemma for cauappcvgpr 6633. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) |
18-Jul-2020 | cauappcvgprlemdisj 6622 | Lemma for cauappcvgpr 6633. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) |
18-Jul-2020 | cauappcvgprlemrnd 6621 | Lemma for cauappcvgpr 6633. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) |
18-Jul-2020 | cauappcvgprlemm 6616 | Lemma for cauappcvgpr 6633. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) |
11-Jul-2020 | cauappcvgprlemladdrl 6628 | Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
11-Jul-2020 | cauappcvgprlemladdru 6627 | Lemma for cauappcvgprlemladd 6629. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
11-Jul-2020 | cauappcvgprlemladdfl 6626 | Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
11-Jul-2020 | cauappcvgprlemladdfu 6625 | Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
8-Jul-2020 | nqprl 6532 | Comparing a fraction to a real can be done by whether it is an element of the lower cut, or by . (Contributed by Jim Kingdon, 8-Jul-2020.) |
24-Jun-2020 | nqprlu 6529 | The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.) |
23-Jun-2020 | cauappcvgprlem2 6631 | Lemma for cauappcvgpr 6633. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
23-Jun-2020 | cauappcvgprlem1 6630 | Lemma for cauappcvgpr 6633. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
23-Jun-2020 | cauappcvgprlemladd 6629 | Lemma for cauappcvgpr 6633. This takes and offsets it by the positive fraction . (Contributed by Jim Kingdon, 23-Jun-2020.) |
20-Jun-2020 | cauappcvgprlemlim 6632 | Lemma for cauappcvgpr 6633. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) |
20-Jun-2020 | cauappcvgprlemcl 6624 | Lemma for cauappcvgpr 6633. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) |
19-Jun-2020 | cauappcvgpr 6633 | A Cauchy approximation has a limit. A Cauchy approximation, here , is similar to a Cauchy sequence but is indexed by the desired tolerance (that is, how close together terms needs to be) rather than by natural numbers. This is basically Theorem 11.2.12 of [HoTT], p. (varies) with a few differences such as that we are proving the existence of a limit without anything about how fast it converges (that is, mere existence instead of existence, in HoTT terms), and that the codomain of is rather than . We also specify that every term needs to be larger than a fraction , to avoid the case where we have positive fractions which converge to zero (which is not a positive real). (Contributed by Jim Kingdon, 19-Jun-2020.) |
15-Jun-2020 | imdivapd 9182 | Imaginary part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
15-Jun-2020 | redivapd 9181 | Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
15-Jun-2020 | cjdivapd 9175 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) |
# | ||
15-Jun-2020 | riotaexg 5415 | Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.) |
14-Jun-2020 | cjdivapi 9143 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# | ||
14-Jun-2020 | cjdivap 9117 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# | ||
14-Jun-2020 | cjap0 9115 | A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# # | ||
14-Jun-2020 | cjap 9114 | Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# # | ||
14-Jun-2020 | imdivap 9089 | Imaginary part of a division. Related to immul2 9088. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# | ||
14-Jun-2020 | redivap 9082 | Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# | ||
14-Jun-2020 | mulreap 9072 | A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# | ||
13-Jun-2020 | sqgt0apd 9041 | The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
13-Jun-2020 | reexpclzapd 9038 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
13-Jun-2020 | expdivapd 9028 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
13-Jun-2020 | sqdivapd 9027 | Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
12-Jun-2020 | expsubapd 9025 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
12-Jun-2020 | expm1apd 9024 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
12-Jun-2020 | expp1zapd 9023 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
12-Jun-2020 | exprecapd 9022 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
12-Jun-2020 | expnegapd 9021 | Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
12-Jun-2020 | expap0d 9020 | Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# # | ||
12-Jun-2020 | expclzapd 9019 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
12-Jun-2020 | sqrecapd 9018 | Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
12-Jun-2020 | sqgt0api 8972 | The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
12-Jun-2020 | sqdivapi 8970 | Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
11-Jun-2020 | sqgt0ap 8955 | The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.) |
# | ||
11-Jun-2020 | sqdivap 8952 | Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.) |
# | ||
11-Jun-2020 | expdivap 8939 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.) |
# | ||
11-Jun-2020 | expm1ap 8938 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.) |
# | ||
11-Jun-2020 | expp1zap 8937 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.) |
# | ||
11-Jun-2020 | expsubap 8936 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) |
# | ||
11-Jun-2020 | expmulzap 8935 | Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) |
# | ||
10-Jun-2020 | expaddzap 8933 | Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.) |
# | ||
10-Jun-2020 | expaddzaplem 8932 | Lemma for expaddzap 8933. (Contributed by Jim Kingdon, 10-Jun-2020.) |
# | ||
10-Jun-2020 | exprecap 8930 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.) |
# | ||
10-Jun-2020 | mulexpzap 8929 | Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.) |
# # | ||
10-Jun-2020 | expap0i 8921 | Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.) |
# # | ||
10-Jun-2020 | expap0 8919 | Positive integer exponentiation is apart from zero iff its mantissa is apart from zero. That it is easier to prove this first, and then prove expeq0 8920 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." ([Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.) |
# # | ||
10-Jun-2020 | mvllmulapd 7570 | Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.) |
# | ||
9-Jun-2020 | expclzap 8914 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.) |
# | ||
9-Jun-2020 | expclzaplem 8913 | Closure law for integer exponentiation. Lemma for expclzap 8914 and expap0i 8921. (Contributed by Jim Kingdon, 9-Jun-2020.) |
# # | ||
9-Jun-2020 | reexpclzap 8909 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.) |
# | ||
9-Jun-2020 | neg1ap0 7784 | -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.) |
# | ||
8-Jun-2020 | expcl2lemap 8901 | Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.) |
# # | ||
8-Jun-2020 | expn1ap0 8899 | A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.) |
# | ||
8-Jun-2020 | expineg2 8898 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) |
# | ||
8-Jun-2020 | expnegap0 8897 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) |
# | ||
8-Jun-2020 | expinnval 8892 | Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.) |
7-Jun-2020 | expival 8891 | Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.) |
# | ||
7-Jun-2020 | expivallem 8890 | Lemma for expival 8891. If we take a complex number apart from zero and raise it to a positive integer power, the result is apart from zero. (Contributed by Jim Kingodon, 7-Jun-2020.) |
# # | ||
7-Jun-2020 | df-iexp 8889 | Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 8893 and expp1 8896 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. 10-Jun-2005: The definition was extended to include zero exponents, so that per the convention of Definition 10-4.1 of [Gleason] p. 134. 4-Jun-2014: The definition was extended to include negative integer exponents. The case gives the value , so we will avoid this case in our theorems. (Contributed by Jim Kingodon, 7-Jun-2020.) |
4-Jun-2020 | iseqfveq 8887 | Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.) |
3-Jun-2020 | iseqfeq2 8886 | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
3-Jun-2020 | iseqfveq2 8885 | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
1-Jun-2020 | iseqcl 8883 | Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.) |
1-Jun-2020 | fzdcel 8654 | Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
DECID | ||
1-Jun-2020 | fztri3or 8653 | Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
1-Jun-2020 | zdclt 8074 | Integer is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.) |
DECID | ||
31-May-2020 | iseqp1 8884 | Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 31-May-2020.) |
31-May-2020 | iseq1 8882 | Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.) |
31-May-2020 | iseqovex 8879 | Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.) |
31-May-2020 | frecuzrdgcl 8860 | Closure law for the recursive definition generator on upper integers. See comment in frec2uz0d 8846 for the description of as the mapping from to . (Contributed by Jim Kingdon, 31-May-2020.) |
frec frec | ||
30-May-2020 | iseqfn 8881 | The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.) |
30-May-2020 | iseqval 8880 | Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.) |
frec | ||
30-May-2020 | nfiseq 8878 | Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
30-May-2020 | iseqeq4 8877 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
30-May-2020 | iseqeq3 8876 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
30-May-2020 | iseqeq2 8875 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
30-May-2020 | iseqeq1 8874 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
30-May-2020 | nffrec 5921 | Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
frec | ||
30-May-2020 | freceq2 5920 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
frec frec | ||
30-May-2020 | freceq1 5919 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
frec frec | ||
29-May-2020 | df-iseq 8873 |
Define a general-purpose operation that builds a recursive sequence
(i.e. a function on the positive integers or some other upper
integer set) whose value at an index is a function of its previous value
and the value of an input sequence at that index. This definition is
complicated, but fortunately it is not intended to be used directly.
Instead, the only purpose of this definition is to provide us with an
object that has the properties expressed by iseq1 8882 and at successors.
Typically, those are the main theorems that would be used in practice.
The first operand in the parentheses is the operation that is applied to the previous value and the value of the input sequence (second operand). The operand to the left of the parenthesis is the integer to start from. For example, for the operation , an input sequence with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence with values 1, 3/2, 7/4, 15/8,.., so that , 3/2, etc. In other words, transforms a sequence into an infinite series. Internally, the frec function generates as its values a set of ordered pairs starting at , with the first member of each pair incremented by one in each successive value. So, the range of frec is exactly the sequence we want, and we just extract the range and throw away the domain. (Contributed by Jim Kingdon, 29-May-2020.) |
frec | ||
28-May-2020 | frecuzrdgsuc 8862 | Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 8846 for the description of as the mapping from to . (Contributed by Jim Kingdon, 28-May-2020.) |
frec frec | ||
27-May-2020 | frecuzrdg0 8861 | Initial value of a recursive definition generator on upper integers. See comment in frec2uz0d 8846 for the description of as the mapping from to . (Contributed by Jim Kingdon, 27-May-2020.) |
frec frec | ||
27-May-2020 | frecuzrdgrrn 8855 | The function (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of . (Contributed by Jim Kingdon, 27-May-2020.) |
frec frec | ||
27-May-2020 | dffun5r 4857 | A way of proving a relation is a function, analogous to mo2r 1949. (Contributed by Jim Kingdon, 27-May-2020.) |
26-May-2020 | frecuzrdgfn 8859 | The recursive definition generator on upper integers is a function. See comment in frec2uz0d 8846 for the description of as the mapping from to . (Contributed by Jim Kingdon, 26-May-2020.) |
frec frec | ||
26-May-2020 | frecuzrdglem 8858 | A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 26-May-2020.) |
frec frec | ||
26-May-2020 | frecuzrdgrom 8857 | The function (used in the definition of the recursive definition generator on upper integers) is a function defined for all natural numbers. (Contributed by Jim Kingdon, 26-May-2020.) |
frec frec | ||
25-May-2020 | freccl 5932 | Closure for finite recursion. (Contributed by Jim Kingdon, 25-May-2020.) |
frec | ||
24-May-2020 | frec2uzrdg 8856 | A helper lemma for the value of a recursive definition generator on upper integers (typically either or ) with characteristic function and initial value . This lemma shows that evaluating at an element of gives an ordered pair whose first element is the index (translated from to ). See comment in frec2uz0d 8846 which describes and the index translation. (Contributed by Jim Kingdon, 24-May-2020.) |
frec frec | ||
21-May-2020 | fzofig 8869 | Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.) |
..^ | ||
21-May-2020 | fzfigd 8868 | Deduction form of fzfig 8867. (Contributed by Jim Kingdon, 21-May-2020.) |
19-May-2020 | fzfig 8867 | A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.) |
19-May-2020 | frechashgf1o 8866 | maps one-to-one onto . (Contributed by Jim Kingdon, 19-May-2020.) |
frec | ||
19-May-2020 | ssfiexmid 6254 | If any subset of a finite set is finite, excluded middle follows. One direction of Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 19-May-2020.) |
19-May-2020 | enm 6230 | A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.) |
18-May-2020 | frecfzen2 8865 | The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Jim Kingdon, 18-May-2020.) |
frec | ||
18-May-2020 | frecfzennn 8864 | The cardinality of a finite set of sequential integers. (See frec2uz0d 8846 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.) |
frec | ||
17-May-2020 | frec2uzisod 8854 | (see frec2uz0d 8846) is an isomorphism from natural ordinals to upper integers. (Contributed by Jim Kingdon, 17-May-2020.) |
frec | ||
17-May-2020 | frec2uzf1od 8853 | (see frec2uz0d 8846) is a one-to-one onto mapping. (Contributed by Jim Kingdon, 17-May-2020.) |
frec | ||
17-May-2020 | frec2uzrand 8852 | Range of (see frec2uz0d 8846). (Contributed by Jim Kingdon, 17-May-2020.) |
frec | ||
16-May-2020 | frec2uzlt2d 8851 | The mapping (see frec2uz0d 8846) preserves order. (Contributed by Jim Kingdon, 16-May-2020.) |
frec | ||
16-May-2020 | frec2uzltd 8850 | Less-than relation for (see frec2uz0d 8846). (Contributed by Jim Kingdon, 16-May-2020.) |
frec | ||
16-May-2020 | frec2uzuzd 8849 | The value (see frec2uz0d 8846) at an ordinal natural number is in the upper integers. (Contributed by Jim Kingdon, 16-May-2020.) |
frec | ||
16-May-2020 | frec2uzsucd 8848 | The value of (see frec2uz0d 8846) at a successor. (Contributed by Jim Kingdon, 16-May-2020.) |
frec | ||
16-May-2020 | frec2uzzd 8847 | The value of (see frec2uz0d 8846) is an integer. (Contributed by Jim Kingdon, 16-May-2020.) |
frec | ||
16-May-2020 | frec2uz0d 8846 | The mapping is a one-to-one mapping from onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number (normally 0 for the upper integers or 1 for the upper integers ), 1 maps to + 1, etc. This theorem shows the value of at ordinal natural number zero. (Contributed by Jim Kingdon, 16-May-2020.) |
frec | ||
15-May-2020 | nntri3 6014 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.) |
14-May-2020 | rdgifnon2 5907 | The recursive definition generator is a function on ordinal numbers. (Contributed by Jim Kingdon, 14-May-2020.) |
14-May-2020 | rdgtfr 5901 | The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.) |
13-May-2020 | frecfnom 5925 | The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.) |
frec | ||
13-May-2020 | frecabex 5923 | The class abstraction from df-frec 5918 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.) |
8-May-2020 | tfr0 5878 | Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.) |
recs | ||
7-May-2020 | frec0g 5922 | The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.) |
frec | ||
3-May-2020 | dcned 2209 | Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.) |
DECID DECID | ||
2-May-2020 | ax-arch 6782 |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 6753.
This axiom should not be used directly; instead use arch 7934 (which is the same, but stated in terms of and ). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.) |
30-Apr-2020 | ltexnqi 6392 | Ordering on positive fractions in terms of existence of sum. (Contributed by Jim Kingdon, 30-Apr-2020.) |
26-Apr-2020 | pitonnlem1p1 6722 | Lemma for pitonn 6724. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.) |
26-Apr-2020 | addnqpr1 6542 | Addition of one to a fraction embedded into a positive real. One can either add the fraction one to the fraction, or the positive real one to the positive real, and get the same result. Special case of addnqpr 6541. (Contributed by Jim Kingdon, 26-Apr-2020.) |
26-Apr-2020 | addpinq1 6446 | Addition of one to the numerator of a fraction whose denominator is one. (Contributed by Jim Kingdon, 26-Apr-2020.) |
26-Apr-2020 | nnnq 6405 | The canonical embedding of positive integers into positive fractions. (Contributed by Jim Kingdon, 26-Apr-2020.) |
24-Apr-2020 | pitonnlem2 6723 | Lemma for pitonn 6724. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.) |
24-Apr-2020 | pitonnlem1 6721 | Lemma for pitonn 6724. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.) |
23-Apr-2020 | archsr 6688 | For any signed real, there is an integer that is greater than it. This is also known as the "archimedean property". The expression , is the embedding of the positive integer into the signed reals. (Contributed by Jim Kingdon, 23-Apr-2020.) |
23-Apr-2020 | nnprlu 6533 | The canonical embedding of positive integers into the positive reals. (Contributed by Jim Kingdon, 23-Apr-2020.) |
22-Apr-2020 | axarch 6753 |
Archimedean axiom. The Archimedean property is more naturally stated
once we have defined . Unless we find another way to state it,
we'll just use the right hand side of dfnn2 7677 in stating what we mean by
"natural number" in the context of this axiom.
This construction-dependent theorem should not be referenced directly; instead, use ax-arch 6782. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
22-Apr-2020 | pitonn 6724 | Mapping from to . (Contributed by Jim Kingdon, 22-Apr-2020.) |
22-Apr-2020 | archpr 6614 | For any positive real, there is an integer that is greater than it. This is also known as the "archimedean property". The integer is embedded into the reals as described at nnprlu 6533. (Contributed by Jim Kingdon, 22-Apr-2020.) |
20-Apr-2020 | fzo0m 8797 | A half-open integer range based at 0 is inhabited precisely if the upper bound is a positive integer. (Contributed by Jim Kingdon, 20-Apr-2020.) |
..^ | ||
20-Apr-2020 | fzom 8770 | A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.) |
..^ ..^ | ||
18-Apr-2020 | eluzdc 8303 | Membership of an integer in an upper set of integers is decidable. (Contributed by Jim Kingdon, 18-Apr-2020.) |
DECID | ||
17-Apr-2020 | zlelttric 8046 | Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.) |
16-Apr-2020 | fznlem 8655 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.) |
15-Apr-2020 | fzm 8652 | Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.) |
15-Apr-2020 | xpdom3m 6244 | A set is dominated by its Cartesian product with an inhabited set. Exercise 6 of [Suppes] p. 98. (Contributed by Jim Kingdon, 15-Apr-2020.) |
13-Apr-2020 | snfig 6227 | A singleton is finite. (Contributed by Jim Kingdon, 13-Apr-2020.) |
13-Apr-2020 | en1bg 6216 | A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.) |
10-Apr-2020 | negm 8306 | The image under negation of an inhabited set of reals is inhabited. (Contributed by Jim Kingdon, 10-Apr-2020.) |
8-Apr-2020 | zleloe 8048 | Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.) |
7-Apr-2020 | zdcle 8073 | Integer is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.) |
DECID | ||
4-Apr-2020 | ioorebasg 8594 | Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.) |
30-Mar-2020 | icc0r 8545 | An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.) |
30-Mar-2020 | ubioog 8533 | An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.) |
30-Mar-2020 | lbioog 8532 | An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.) |
29-Mar-2020 | iooidg 8528 | An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.) |
27-Mar-2020 | zletric 8045 | Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.) |
26-Mar-2020 | 4z 8031 | 4 is an integer. (Contributed by BJ, 26-Mar-2020.) |
25-Mar-2020 | elfzmlbm 8738 | Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
25-Mar-2020 | elfz0add 8729 | An element of a finite set of sequential nonnegative integers is an element of an extended finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
25-Mar-2020 | 2eluzge0 8273 | 2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
23-Mar-2020 | rpnegap 8370 | Either a real apart from zero or its negation is a positive real, but not both. (Contributed by Jim Kingdon, 23-Mar-2020.) |
# | ||
23-Mar-2020 | reapltxor 7353 | Real apartness in terms of less than (exclusive-or version). (Contributed by Jim Kingdon, 23-Mar-2020.) |
# | ||
22-Mar-2020 | rpcnap0 8358 | A positive real is a complex number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.) |
# | ||
22-Mar-2020 | rpreap0 8356 | A positive real is a real number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.) |
# | ||
22-Mar-2020 | rpap0 8354 | A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.) |
# | ||
20-Mar-2020 | qapne 8330 | Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 20-Mar-2020.) |
# | ||
20-Mar-2020 | divap1d 7538 | If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.) |
# # # | ||
20-Mar-2020 | apmul1 7526 | Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.) |
# # # | ||
19-Mar-2020 | divfnzn 8312 | Division restricted to is a function. Given excluded middle, it would be easy to prove this for . The key difference is that an element of is apart from zero, whereas being an element of implies being not equal to zero. (Contributed by Jim Kingdon, 19-Mar-2020.) |
19-Mar-2020 | div2negapd 7542 | Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.) |
# | ||
19-Mar-2020 | divneg2apd 7541 | Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.) |
# | ||
19-Mar-2020 | divnegapd 7540 | Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.) |
# | ||
19-Mar-2020 | divap0bd 7539 | A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.) |
# # # | ||
19-Mar-2020 | diveqap0ad 7537 | A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 7423. (Contributed by Jim Kingdon, 19-Mar-2020.) |
# | ||
19-Mar-2020 | diveqap1ad 7536 | The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 7444. Generalization of diveqap1d 7535. (Contributed by Jim Kingdon, 19-Mar-2020.) |
# | ||
19-Mar-2020 | diveqap1d 7535 | Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.) |
# | ||
19-Mar-2020 | diveqap0d 7534 | If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.) |
# | ||
15-Mar-2020 | nneoor 8096 | A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.) |
14-Mar-2020 | zltlen 8075 | Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7393 which is a similar result for complex numbers. (Contributed by Jim Kingdon, 14-Mar-2020.) |
14-Mar-2020 | zdceq 8072 | Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.) |
DECID | ||
14-Mar-2020 | zapne 8071 | Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.) |
# | ||
14-Mar-2020 | zltnle 8047 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.) |
14-Mar-2020 | ztri3or 8044 | Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.) |
14-Mar-2020 | ztri3or0 8043 | Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.) |
14-Mar-2020 | zaddcllemneg 8040 | Lemma for zaddcl 8041. Special case in which is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.) |
14-Mar-2020 | zaddcllempos 8038 | Lemma for zaddcl 8041. Special case in which is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.) |
14-Mar-2020 | dcne 2211 | Decidable equality expressed in terms of . Basically the same as df-dc 742. (Contributed by Jim Kingdon, 14-Mar-2020.) |
DECID | ||
9-Mar-2020 | 2muliap0 7906 | is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
9-Mar-2020 | iap0 7905 | The imaginary unit is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
9-Mar-2020 | 2ap0 7769 | The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
9-Mar-2020 | 1ne0 7743 | . See aso 1ap0 7354. (Contributed by Jim Kingdon, 9-Mar-2020.) |
9-Mar-2020 | redivclapi 7517 | Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
9-Mar-2020 | redivclapzi 7516 | Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
9-Mar-2020 | rerecclapi 7515 | Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
9-Mar-2020 | rerecclapzi 7514 | Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
9-Mar-2020 | divdivdivapi 7513 | Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# # # | ||
9-Mar-2020 | divadddivapi 7512 | Addition of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# # | ||
9-Mar-2020 | divmul13api 7511 | Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# # | ||
9-Mar-2020 | divmuldivapi 7510 | Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# # | ||
9-Mar-2020 | div11api 7509 | One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
9-Mar-2020 | div23api 7508 | A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
9-Mar-2020 | divdirapi 7507 | Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
9-Mar-2020 | divassapi 7506 | An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.) |
# | ||
8-Mar-2020 | nnap0 7704 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# | ||
8-Mar-2020 | divdivap2d 7559 | Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# # | ||
8-Mar-2020 | divdivap1d 7558 | Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# # | ||
8-Mar-2020 | dmdcanap2d 7557 | Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# # | ||
8-Mar-2020 | dmdcanapd 7556 | Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# # | ||
8-Mar-2020 | divcanap7d 7555 | Cancel equal divisors in a division. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# # | ||
8-Mar-2020 | divcanap5rd 7554 | Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# # | ||
8-Mar-2020 | divcanap5d 7553 | Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# # | ||
8-Mar-2020 | divdiv32apd 7552 | Swap denominators in a division. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# # | ||
8-Mar-2020 | div13apd 7551 | A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# | ||
8-Mar-2020 | div32apd 7550 | A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# | ||
8-Mar-2020 | divmulapd 7549 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.) |
# | ||
7-Mar-2020 | nn1gt1 7708 | A positive integer is either one or greater than one. This is for ; 0elnn 4283 is a similar theorem for (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.) |
5-Mar-2020 | crap0 7671 | The real representation of complex numbers is apart from zero iff one of its terms is apart from zero. (Contributed by Jim Kingdon, 5-Mar-2020.) |
# # # | ||
3-Mar-2020 | rec11apd 7548 | Reciprocal is one-to-one. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# # | ||
3-Mar-2020 | ddcanapd 7547 | Cancellation in a double division. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# # | ||
3-Mar-2020 | divcanap6d 7546 | Cancellation of inverted fractions. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# # | ||
3-Mar-2020 | recdivap2d 7545 | Division into a reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# # | ||
3-Mar-2020 | recdivapd 7544 | The reciprocal of a ratio. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# # | ||
3-Mar-2020 | divap0d 7543 | The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# # # | ||
3-Mar-2020 | div0apd 7525 | Division into zero is zero. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# | ||
3-Mar-2020 | dividapd 7524 | A number divided by itself is one. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# | ||
3-Mar-2020 | recrecapd 7523 | A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# | ||
3-Mar-2020 | recidap2d 7522 | Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# | ||
3-Mar-2020 | recidapd 7521 | Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# | ||
3-Mar-2020 | recap0d 7520 | The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# # | ||
3-Mar-2020 | recclapd 7519 | Closure law for reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.) |
# | ||
2-Mar-2020 | div11apd 7567 | One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.) |
# | ||
2-Mar-2020 | divsubdirapd 7566 | Distribution of division over subtraction. (Contributed by Jim Kingdon, 2-Mar-2020.) |
# | ||
2-Mar-2020 | divdirapd 7565 | Distribution of division over addition. (Contributed by Jim Kingdon, 2-Mar-2020.) |
# | ||
2-Mar-2020 | div23apd 7564 | A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.) |
# | ||
2-Mar-2020 | div12apd 7563 | A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.) |
# | ||
2-Mar-2020 | divassapd 7562 | An associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.) |
# | ||
2-Mar-2020 | divmulap3d 7561 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.) |
# | ||
2-Mar-2020 | divmulap2d 7560 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.) |
# | ||
29-Feb-2020 | prodgt0gt0 7578 | Infer that a multiplicand is positive from a positive multiplier and positive product. See prodgt0 7579 for the same theorem with replaced by the weaker condition . (Contributed by Jim Kingdon, 29-Feb-2020.) |
29-Feb-2020 | redivclapd 7569 | Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.) |
# | ||
29-Feb-2020 | rerecclapd 7568 | Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.) |
# | ||
29-Feb-2020 | divcanap4d 7533 | A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.) |
# | ||
29-Feb-2020 | divcanap3d 7532 | A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.) |
# | ||
29-Feb-2020 | divrecap2d 7531 | Relationship between division and reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.) |
# | ||
29-Feb-2020 | divrecapd 7530 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Jim Kingdon, 29-Feb-2020.) |
# | ||
29-Feb-2020 | divcanap2d 7529 | A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.) |
# | ||
29-Feb-2020 | divcanap1d 7528 | A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.) |
# | ||
29-Feb-2020 | divclapd 7527 | Closure law for division. (Contributed by Jim Kingdon, 29-Feb-2020.) |
# | ||
29-Feb-2020 | divdiv32api 7505 | Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.) |