Home | Intuitionistic Logic Explorer Theorem List (p. 73 of 141) | < 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 | pw1nel3 7201 | Negated excluded middle implies that the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
EXMID | ||
Theorem | sucpw1ne3 7202 | Negated excluded middle implies that the successor of the power set of is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
EXMID | ||
Theorem | sucpw1nel3 7203 | The successor of the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
Theorem | 3nelsucpw1 7204 | Three is not an element of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
Theorem | sucpw1nss3 7205 | Negated excluded middle implies that the successor of the power set of is not a subset of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.) |
EXMID | ||
Theorem | 3nsssucpw1 7206 | Negated excluded middle implies that is not a subset of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.) |
EXMID | ||
Theorem | onntri35 7207* |
Double negated ordinal trichotomy.
There are five equivalent statements: (1) , (2) , (3) , (4) , and (5) EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7208), (3) implies (5) (onntri35 7207), (5) implies (1) (onntri51 7210), (2) implies (4) (onntri24 7212), (4) implies (5) (onntri45 7211), and (5) implies (2) (onntri52 7214). Another way of stating this is that EXMID is equivalent to trichotomy, either the or the form, as shown in exmidontri 7209 and exmidontri2or 7213, respectively. Thus EXMID is equivalent to (1) or (2). In addition, EXMID is equivalent to (3) by onntri3or 7215 and (4) by onntri2or 7216. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
Theorem | onntri13 7208 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
Theorem | exmidontri 7209* | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
EXMID | ||
Theorem | onntri51 7210* | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
Theorem | onntri45 7211* | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
Theorem | onntri24 7212 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
Theorem | exmidontri2or 7213* | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
EXMID | ||
Theorem | onntri52 7214* | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
Theorem | onntri3or 7215* | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
EXMID | ||
Theorem | onntri2or 7216* | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
EXMID | ||
We have already introduced the full Axiom of Choice df-ac 7176 but since it implies excluded middle as shown at exmidac 7179, it is not especially relevant to us. In this section we define countable choice and dependent choice, which are not as strong as thus often considered in mathematics which seeks to avoid full excluded middle. | ||
Syntax | wacc 7217 | Formula for an abbreviation of countable choice. |
CCHOICE | ||
Definition | df-cc 7218* | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7176 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) |
CCHOICE | ||
Theorem | ccfunen 7219* | Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.) |
CCHOICE | ||
Theorem | cc1 7220* | Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
Theorem | cc2lem 7221* | Lemma for cc2 7222. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
Theorem | cc2 7222* | Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
Theorem | cc3 7223* | Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.) |
CCHOICE | ||
Theorem | cc4f 7224* | Countable choice by showing the existence of a function which can choose a value at each index such that holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.) |
CCHOICE | ||
Theorem | cc4 7225* | Countable choice by showing the existence of a function which can choose a value at each index such that holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 1-May-2024.) |
CCHOICE | ||
Theorem | cc4n 7226* | Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7225, the hypotheses only require an A(n) for each value of , not a single set which suffices for every . (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.) |
CCHOICE | ||
This section derives the basics of real and complex numbers. To construct the real numbers constructively, we follow two main sources. The first is Metamath Proof Explorer, which has the advantage of being already formalized in metamath. Its disadvantage, for our purposes, is that it assumes the law of the excluded middle throughout. Since we have already developed natural numbers ( for example, nna0 6451 and similar theorems ), going from there to positive integers (df-ni 7259) and then positive rational numbers (df-nqqs 7303) does not involve a major change in approach compared with the Metamath Proof Explorer. It is when we proceed to Dedekind cuts that we bring in more material from Section 11.2 of [HoTT], which focuses on the aspects of Dedekind cuts which are different without excluded middle or choice principles. With excluded middle, it is natural to define a cut as the lower set only (as Metamath Proof Explorer does), but here we define the cut as a pair of both the lower and upper sets, as [HoTT] does. There are also differences in how we handle order and replacing "not equal to zero" with "apart from zero". When working constructively, there are several possible definitions of real numbers. Here we adopt the most common definition, as two-sided Dedekind cuts with the properties described at df-inp 7421. The Cauchy reals (without countable choice) fail to satisfy ax-caucvg 7887 and the MacNeille reals fail to satisfy axltwlin 7980, and we do not develop them here. For more on differing definitions of the reals, see the introduction to Chapter 11 in [HoTT] or Section 1.2 of [BauerHanson]. | ||
Syntax | cnpi 7227 |
The set of positive integers, which is the set of natural numbers
with 0 removed.
Note: This is the start of the Dedekind-cut construction of real and complex numbers. |
Syntax | cpli 7228 | Positive integer addition. |
Syntax | cmi 7229 | Positive integer multiplication. |
Syntax | clti 7230 | Positive integer ordering relation. |
Syntax | cplpq 7231 | Positive pre-fraction addition. |
Syntax | cmpq 7232 | Positive pre-fraction multiplication. |
Syntax | cltpq 7233 | Positive pre-fraction ordering relation. |
Syntax | ceq 7234 | Equivalence class used to construct positive fractions. |
Syntax | cnq 7235 | Set of positive fractions. |
Syntax | c1q 7236 | The positive fraction constant 1. |
Syntax | cplq 7237 | Positive fraction addition. |
Syntax | cmq 7238 | Positive fraction multiplication. |
Syntax | crq 7239 | Positive fraction reciprocal operation. |
Syntax | cltq 7240 | Positive fraction ordering relation. |
Syntax | ceq0 7241 | Equivalence class used to construct nonnegative fractions. |
~Q0 | ||
Syntax | cnq0 7242 | Set of nonnegative fractions. |
Q0 | ||
Syntax | c0q0 7243 | The nonnegative fraction constant 0. |
0Q0 | ||
Syntax | cplq0 7244 | Nonnegative fraction addition. |
+Q0 | ||
Syntax | cmq0 7245 | Nonnegative fraction multiplication. |
·Q0 | ||
Syntax | cnp 7246 | Set of positive reals. |
Syntax | c1p 7247 | Positive real constant 1. |
Syntax | cpp 7248 | Positive real addition. |
Syntax | cmp 7249 | Positive real multiplication. |
Syntax | cltp 7250 | Positive real ordering relation. |
Syntax | cer 7251 | Equivalence class used to construct signed reals. |
Syntax | cnr 7252 | Set of signed reals. |
Syntax | c0r 7253 | The signed real constant 0. |
Syntax | c1r 7254 | The signed real constant 1. |
Syntax | cm1r 7255 | The signed real constant -1. |
Syntax | cplr 7256 | Signed real addition. |
Syntax | cmr 7257 | Signed real multiplication. |
Syntax | cltr 7258 | Signed real ordering relation. |
Definition | df-ni 7259 | Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) |
Definition | df-pli 7260 | Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) |
Definition | df-mi 7261 | Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) |
Definition | df-lti 7262 | Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.) |
Theorem | elni 7263 | Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) |
Theorem | pinn 7264 | A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) |
Theorem | pion 7265 | A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) |
Theorem | piord 7266 | A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) |
Theorem | niex 7267 | The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) |
Theorem | 0npi 7268 | The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) |
Theorem | elni2 7269 | Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) |
Theorem | 1pi 7270 | Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) |
Theorem | addpiord 7271 | Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) |
Theorem | mulpiord 7272 | Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) |
Theorem | mulidpi 7273 | 1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | ltpiord 7274 | Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | ltsopi 7275 | Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.) |
Theorem | pitric 7276 | Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.) |
Theorem | pitri3or 7277 | Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.) |
Theorem | ltdcpi 7278 | Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.) |
DECID | ||
Theorem | ltrelpi 7279 | Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.) |
Theorem | dmaddpi 7280 | Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) |
Theorem | dmmulpi 7281 | Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) |
Theorem | addclpi 7282 | Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) |
Theorem | mulclpi 7283 | Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) |
Theorem | addcompig 7284 | Addition of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.) |
Theorem | addasspig 7285 | Addition of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.) |
Theorem | mulcompig 7286 | Multiplication of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.) |
Theorem | mulasspig 7287 | Multiplication of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.) |
Theorem | distrpig 7288 | Multiplication of positive integers is distributive. (Contributed by Jim Kingdon, 26-Aug-2019.) |
Theorem | addcanpig 7289 | Addition cancellation law for positive integers. (Contributed by Jim Kingdon, 27-Aug-2019.) |
Theorem | mulcanpig 7290 | Multiplication cancellation law for positive integers. (Contributed by Jim Kingdon, 29-Aug-2019.) |
Theorem | addnidpig 7291 | There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) |
Theorem | ltexpi 7292* | Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) |
Theorem | ltapig 7293 | Ordering property of addition for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.) |
Theorem | ltmpig 7294 | Ordering property of multiplication for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.) |
Theorem | 1lt2pi 7295 | One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) |
Theorem | nlt1pig 7296 | No positive integer is less than one. (Contributed by Jim Kingdon, 31-Aug-2019.) |
Theorem | indpi 7297* | Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.) |
Theorem | nnppipi 7298 | A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.) |
Definition | df-plpq 7299* | Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. This "pre-addition" operation works directly with ordered pairs of integers. The actual positive fraction addition (df-plqqs 7304) works with the equivalence classes of these ordered pairs determined by the equivalence relation (df-enq 7302). (Analogous remarks apply to the other "pre-" operations in the complex number construction that follows.) From Proposition 9-2.3 of [Gleason] p. 117. (Contributed by NM, 28-Aug-1995.) |
Definition | df-mpq 7300* | Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.4 of [Gleason] p. 119. (Contributed by NM, 28-Aug-1995.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |