Home | Intuitionistic Logic Explorer Theorem List (p. 71 of 130) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dju1p1e2 7001 | Disjoint union version of one plus one equals two. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (1_{o} ⊔ 1_{o}) ≈ 2_{o} | ||
Theorem | infpwfidom 7002 | The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption (𝒫 𝐴 ∩ Fin) ∈ V because this theorem also implies that 𝐴 is a set if 𝒫 𝐴 ∩ Fin is.) (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ ((𝒫 𝐴 ∩ Fin) ∈ V → 𝐴 ≼ (𝒫 𝐴 ∩ Fin)) | ||
Theorem | exmidfodomrlemeldju 7003 | Lemma for exmidfodomr 7008. A variant of djur 6906. (Contributed by Jim Kingdon, 2-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1_{o}) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1_{o})) ⇒ ⊢ (𝜑 → (𝐵 = (inl‘∅) ∨ 𝐵 = (inr‘∅))) | ||
Theorem | exmidfodomrlemreseldju 7004 | Lemma for exmidfodomrlemrALT 7007. A variant of eldju 6905. (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (𝜑 → 𝐴 ⊆ 1_{o}) & ⊢ (𝜑 → 𝐵 ∈ (𝐴 ⊔ 1_{o})) ⇒ ⊢ (𝜑 → ((∅ ∈ 𝐴 ∧ 𝐵 = ((inl ↾ 𝐴)‘∅)) ∨ 𝐵 = ((inr ↾ 1_{o})‘∅))) | ||
Theorem | exmidfodomrlemim 7005* | Excluded middle implies the existence of a mapping from any set onto any inhabited set that it dominates. Proposition 1.1 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (EXMID → ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)) | ||
Theorem | exmidfodomrlemr 7006* | The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID) | ||
Theorem | exmidfodomrlemrALT 7007* | The existence of a mapping from any set onto any inhabited set that it dominates implies excluded middle. Proposition 1.2 of [PradicBrown2022], p. 2. An alternative proof of exmidfodomrlemr 7006. In particular, this proof uses eldju 6905 instead of djur 6906 and avoids djulclb 6892. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Jim Kingdon, 9-Jul-2022.) |
⊢ (∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦) → EXMID) | ||
Theorem | exmidfodomr 7008* | Excluded middle is equivalent to the existence of a mapping from any set onto any inhabited set that it dominates. (Contributed by Jim Kingdon, 1-Jul-2022.) |
⊢ (EXMID ↔ ∀𝑥∀𝑦((∃𝑧 𝑧 ∈ 𝑦 ∧ 𝑦 ≼ 𝑥) → ∃𝑓 𝑓:𝑥–onto→𝑦)) | ||
Syntax | wac 7009 | Formula for an abbreviation of the axiom of choice. |
wff CHOICE | ||
Definition | df-ac 7010* |
The expression CHOICE will be used as a
readable shorthand for any
form of the axiom of choice; all concrete forms are long, cryptic, have
dummy variables, or all three, making it useful to have a short name.
Similar to the Axiom of Choice (first form) of [Enderton] p. 49.
There are some decisions about how to write this definition especially around whether ax-setind 4412 is needed to show equivalence to other ways of stating choice, and about whether choice functions are available for nonempty sets or inhabited sets. (Contributed by Mario Carneiro, 22-Feb-2015.) |
⊢ (CHOICE ↔ ∀𝑥∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥)) | ||
Theorem | acfun 7011* | A convenient form of choice. The goal here is to state choice as the existence of a choice function on a set of inhabited sets, while making full use of our notation around functions and function values. (Contributed by Jim Kingdon, 20-Nov-2023.) |
⊢ (𝜑 → CHOICE) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑤 𝑤 ∈ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)) | ||
Theorem | exmidaclem 7012* | Lemma for exmidac 7013. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) |
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = ∅ ∨ 𝑦 = {∅})} & ⊢ 𝐵 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ 𝑦 = {∅})} & ⊢ 𝐶 = {𝐴, 𝐵} ⇒ ⊢ (CHOICE → EXMID) | ||
Theorem | exmidac 7013 | The axiom of choice implies excluded middle. See acexmid 5727 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.) |
⊢ (CHOICE → EXMID) | ||
Theorem | endjudisj 7014 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ⊔ 𝐵) ≈ (𝐴 ∪ 𝐵)) | ||
Theorem | djuen 7015 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ⊔ 𝐷)) | ||
Theorem | djuenun 7016 | Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷 ∧ (𝐵 ∩ 𝐷) = ∅) → (𝐴 ⊔ 𝐶) ≈ (𝐵 ∪ 𝐷)) | ||
Theorem | dju1en 7017 | Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 28-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ 𝐴) → (𝐴 ⊔ 1_{o}) ≈ suc 𝐴) | ||
Theorem | dju0en 7018 | Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of [Enderton] p. 143. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ⊔ ∅) ≈ 𝐴) | ||
Theorem | xp2dju 7019 | Two times a cardinal number. Exercise 4.56(g) of [Mendelson] p. 258. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (2_{o} × 𝐴) = (𝐴 ⊔ 𝐴) | ||
Theorem | djucomen 7020 | Commutative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 24-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ≈ (𝐵 ⊔ 𝐴)) | ||
Theorem | djuassen 7021 | Associative law for cardinal addition. Exercise 4.56(c) of [Mendelson] p. 258. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴 ⊔ 𝐵) ⊔ 𝐶) ≈ (𝐴 ⊔ (𝐵 ⊔ 𝐶))) | ||
Theorem | xpdjuen 7022 | Cardinal multiplication distributes over cardinal addition. Theorem 6I(3) of [Enderton] p. 142. (Contributed by NM, 26-Sep-2004.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴 × (𝐵 ⊔ 𝐶)) ≈ ((𝐴 × 𝐵) ⊔ (𝐴 × 𝐶))) | ||
Theorem | djudoml 7023 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ≼ (𝐴 ⊔ 𝐵)) | ||
Theorem | djudomr 7024 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ≼ (𝐴 ⊔ 𝐵)) | ||
We have already introduced the full Axiom of Choice df-ac 7010 but since it implies excluded middle as shown at exmidac 7013, 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 7025 | Formula for an abbreviation of countable choice. |
wff CCHOICE | ||
Definition | df-cc 7026* | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7010 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) |
⊢ (CCHOICE ↔ ∀𝑥(dom 𝑥 ≈ ω → ∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥))) | ||
Theorem | ccfunen 7027* | Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.) |
⊢ (𝜑 → CCHOICE) & ⊢ (𝜑 → 𝐴 ≈ ω) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑤 𝑤 ∈ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)) | ||
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 6324 and similar theorems ), going from there to positive integers (df-ni 7060) and then positive rational numbers (df-nqqs 7104) 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. With excluded middle, it is natural to define the cut as the lower set only (as Metamath Proof Explorer does), but 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". | ||
Syntax | cnpi 7028 |
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. |
class N | ||
Syntax | cpli 7029 | Positive integer addition. |
class +_{N} | ||
Syntax | cmi 7030 | Positive integer multiplication. |
class ·_{N} | ||
Syntax | clti 7031 | Positive integer ordering relation. |
class <_{N} | ||
Syntax | cplpq 7032 | Positive pre-fraction addition. |
class +_{pQ} | ||
Syntax | cmpq 7033 | Positive pre-fraction multiplication. |
class ·_{pQ} | ||
Syntax | cltpq 7034 | Positive pre-fraction ordering relation. |
class <_{pQ} | ||
Syntax | ceq 7035 | Equivalence class used to construct positive fractions. |
class ~_{Q} | ||
Syntax | cnq 7036 | Set of positive fractions. |
class Q | ||
Syntax | c1q 7037 | The positive fraction constant 1. |
class 1_{Q} | ||
Syntax | cplq 7038 | Positive fraction addition. |
class +_{Q} | ||
Syntax | cmq 7039 | Positive fraction multiplication. |
class ·_{Q} | ||
Syntax | crq 7040 | Positive fraction reciprocal operation. |
class *_{Q} | ||
Syntax | cltq 7041 | Positive fraction ordering relation. |
class <_{Q} | ||
Syntax | ceq0 7042 | Equivalence class used to construct nonnegative fractions. |
class ~_{Q0} | ||
Syntax | cnq0 7043 | Set of nonnegative fractions. |
class Q_{0} | ||
Syntax | c0q0 7044 | The nonnegative fraction constant 0. |
class 0_{Q0} | ||
Syntax | cplq0 7045 | Nonnegative fraction addition. |
class +_{Q0} | ||
Syntax | cmq0 7046 | Nonnegative fraction multiplication. |
class ·_{Q0} | ||
Syntax | cnp 7047 | Set of positive reals. |
class P | ||
Syntax | c1p 7048 | Positive real constant 1. |
class 1_{P} | ||
Syntax | cpp 7049 | Positive real addition. |
class +_{P} | ||
Syntax | cmp 7050 | Positive real multiplication. |
class ·_{P} | ||
Syntax | cltp 7051 | Positive real ordering relation. |
class <_{P} | ||
Syntax | cer 7052 | Equivalence class used to construct signed reals. |
class ~_{R} | ||
Syntax | cnr 7053 | Set of signed reals. |
class R | ||
Syntax | c0r 7054 | The signed real constant 0. |
class 0_{R} | ||
Syntax | c1r 7055 | The signed real constant 1. |
class 1_{R} | ||
Syntax | cm1r 7056 | The signed real constant -1. |
class -1_{R} | ||
Syntax | cplr 7057 | Signed real addition. |
class +_{R} | ||
Syntax | cmr 7058 | Signed real multiplication. |
class ·_{R} | ||
Syntax | cltr 7059 | Signed real ordering relation. |
class <_{R} | ||
Definition | df-ni 7060 | 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.) |
⊢ N = (ω ∖ {∅}) | ||
Definition | df-pli 7061 | 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.) |
⊢ +_{N} = ( +_{o} ↾ (N × N)) | ||
Definition | df-mi 7062 | 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.) |
⊢ ·_{N} = ( ·_{o} ↾ (N × N)) | ||
Definition | df-lti 7063 | 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.) |
⊢ <_{N} = ( E ∩ (N × N)) | ||
Theorem | elni 7064 | Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) |
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅)) | ||
Theorem | pinn 7065 | A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) |
⊢ (𝐴 ∈ N → 𝐴 ∈ ω) | ||
Theorem | pion 7066 | A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) |
⊢ (𝐴 ∈ N → 𝐴 ∈ On) | ||
Theorem | piord 7067 | A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) |
⊢ (𝐴 ∈ N → Ord 𝐴) | ||
Theorem | niex 7068 | The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) |
⊢ N ∈ V | ||
Theorem | 0npi 7069 | The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) |
⊢ ¬ ∅ ∈ N | ||
Theorem | elni2 7070 | Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) |
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴)) | ||
Theorem | 1pi 7071 | Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) |
⊢ 1_{o} ∈ N | ||
Theorem | addpiord 7072 | Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +_{N} 𝐵) = (𝐴 +_{o} 𝐵)) | ||
Theorem | mulpiord 7073 | Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·_{N} 𝐵) = (𝐴 ·_{o} 𝐵)) | ||
Theorem | mulidpi 7074 | 1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) |
⊢ (𝐴 ∈ N → (𝐴 ·_{N} 1_{o}) = 𝐴) | ||
Theorem | ltpiord 7075 | Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <_{N} 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | ltsopi 7076 | Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.) |
⊢ <_{N} Or N | ||
Theorem | pitric 7077 | Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <_{N} 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <_{N} 𝐴))) | ||
Theorem | pitri3or 7078 | Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <_{N} 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 <_{N} 𝐴)) | ||
Theorem | ltdcpi 7079 | Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → DECID 𝐴 <_{N} 𝐵) | ||
Theorem | ltrelpi 7080 | Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.) |
⊢ <_{N} ⊆ (N × N) | ||
Theorem | dmaddpi 7081 | Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) |
⊢ dom +_{N} = (N × N) | ||
Theorem | dmmulpi 7082 | Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) |
⊢ dom ·_{N} = (N × N) | ||
Theorem | addclpi 7083 | Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +_{N} 𝐵) ∈ N) | ||
Theorem | mulclpi 7084 | Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·_{N} 𝐵) ∈ N) | ||
Theorem | addcompig 7085 | Addition of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +_{N} 𝐵) = (𝐵 +_{N} 𝐴)) | ||
Theorem | addasspig 7086 | Addition of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → ((𝐴 +_{N} 𝐵) +_{N} 𝐶) = (𝐴 +_{N} (𝐵 +_{N} 𝐶))) | ||
Theorem | mulcompig 7087 | Multiplication of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·_{N} 𝐵) = (𝐵 ·_{N} 𝐴)) | ||
Theorem | mulasspig 7088 | Multiplication of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → ((𝐴 ·_{N} 𝐵) ·_{N} 𝐶) = (𝐴 ·_{N} (𝐵 ·_{N} 𝐶))) | ||
Theorem | distrpig 7089 | Multiplication of positive integers is distributive. (Contributed by Jim Kingdon, 26-Aug-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → (𝐴 ·_{N} (𝐵 +_{N} 𝐶)) = ((𝐴 ·_{N} 𝐵) +_{N} (𝐴 ·_{N} 𝐶))) | ||
Theorem | addcanpig 7090 | Addition cancellation law for positive integers. (Contributed by Jim Kingdon, 27-Aug-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → ((𝐴 +_{N} 𝐵) = (𝐴 +_{N} 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | mulcanpig 7091 | Multiplication cancellation law for positive integers. (Contributed by Jim Kingdon, 29-Aug-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → ((𝐴 ·_{N} 𝐵) = (𝐴 ·_{N} 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | addnidpig 7092 | There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ¬ (𝐴 +_{N} 𝐵) = 𝐴) | ||
Theorem | ltexpi 7093* | Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <_{N} 𝐵 ↔ ∃𝑥 ∈ N (𝐴 +_{N} 𝑥) = 𝐵)) | ||
Theorem | ltapig 7094 | Ordering property of addition for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → (𝐴 <_{N} 𝐵 ↔ (𝐶 +_{N} 𝐴) <_{N} (𝐶 +_{N} 𝐵))) | ||
Theorem | ltmpig 7095 | Ordering property of multiplication for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → (𝐴 <_{N} 𝐵 ↔ (𝐶 ·_{N} 𝐴) <_{N} (𝐶 ·_{N} 𝐵))) | ||
Theorem | 1lt2pi 7096 | One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) |
⊢ 1_{o} <_{N} (1_{o} +_{N} 1_{o}) | ||
Theorem | nlt1pig 7097 | No positive integer is less than one. (Contributed by Jim Kingdon, 31-Aug-2019.) |
⊢ (𝐴 ∈ N → ¬ 𝐴 <_{N} 1_{o}) | ||
Theorem | indpi 7098* | Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.) |
⊢ (𝑥 = 1_{o} → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 +_{N} 1_{o}) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ N → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ N → 𝜏) | ||
Theorem | nnppipi 7099 | A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) → (𝐴 +_{o} 𝐵) ∈ N) | ||
Definition | df-plpq 7100* | 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 +_{Q} (df-plqqs 7105) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~_{Q} (df-enq 7103). (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.) |
⊢ +_{pQ} = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨(((1^{st} ‘𝑥) ·_{N} (2^{nd} ‘𝑦)) +_{N} ((1^{st} ‘𝑦) ·_{N} (2^{nd} ‘𝑥))), ((2^{nd} ‘𝑥) ·_{N} (2^{nd} ‘𝑦))⟩) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |