Home | Metamath
Proof Explorer Theorem List (p. 104 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmmulpi 10301 | Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ dom ·N = (N × N) | ||
Theorem | addclpi 10302 | Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) ∈ N) | ||
Theorem | mulclpi 10303 | Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) ∈ N) | ||
Theorem | addcompi 10304 | Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 +N 𝐵) = (𝐵 +N 𝐴) | ||
Theorem | addasspi 10305 | Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 +N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N 𝐶)) | ||
Theorem | mulcompi 10306 | Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ (𝐴 ·N 𝐵) = (𝐵 ·N 𝐴) | ||
Theorem | mulasspi 10307 | Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵 ·N 𝐶)) | ||
Theorem | distrpi 10308 | Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶)) | ||
Theorem | addcanpi 10309 | Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | mulcanpi 10310 | Multiplication cancellation law for positive integers. (Contributed by NM, 4-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 ·N 𝐵) = (𝐴 ·N 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | addnidpi 10311 | There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → ¬ (𝐴 +N 𝐵) = 𝐴) | ||
Theorem | ltexpi 10312* | Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <N 𝐵 ↔ ∃𝑥 ∈ N (𝐴 +N 𝑥) = 𝐵)) | ||
Theorem | ltapi 10313 | Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.) |
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵))) | ||
Theorem | ltmpi 10314 | Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.) |
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 ·N 𝐴) <N (𝐶 ·N 𝐵))) | ||
Theorem | 1lt2pi 10315 | One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |
⊢ 1o <N (1o +N 1o) | ||
Theorem | nlt1pi 10316 | No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
⊢ ¬ 𝐴 <N 1o | ||
Theorem | indpi 10317* | Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
⊢ (𝑥 = 1o → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 +N 1o) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ N → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ N → 𝜏) | ||
Definition | df-plpq 10318* | Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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-plq 10324) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 10321). (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.) (New usage is discouraged.) |
⊢ +pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ 〈(((1st ‘𝑥) ·N (2nd ‘𝑦)) +N ((1st ‘𝑦) ·N (2nd ‘𝑥))), ((2nd ‘𝑥) ·N (2nd ‘𝑦))〉) | ||
Definition | df-mpq 10319* | Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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.) (New usage is discouraged.) |
⊢ ·pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ 〈((1st ‘𝑥) ·N (1st ‘𝑦)), ((2nd ‘𝑥) ·N (2nd ‘𝑦))〉) | ||
Definition | df-ltpq 10320* | Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 28-Aug-1995.) (New usage is discouraged.) |
⊢ <pQ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ((1st ‘𝑥) ·N (2nd ‘𝑦)) <N ((1st ‘𝑦) ·N (2nd ‘𝑥)))} | ||
Definition | df-enq 10321* | Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. From Proposition 9-2.1 of [Gleason] p. 117. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ~Q = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (N × N) ∧ 𝑦 ∈ (N × N)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) ∧ (𝑧 ·N 𝑢) = (𝑤 ·N 𝑣)))} | ||
Definition | df-nq 10322* | Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117. (Contributed by NM, 16-Aug-1995.) (New usage is discouraged.) |
⊢ Q = {𝑥 ∈ (N × N) ∣ ∀𝑦 ∈ (N × N)(𝑥 ~Q 𝑦 → ¬ (2nd ‘𝑦) <N (2nd ‘𝑥))} | ||
Definition | df-erq 10323 | Define a convenience function that "reduces" a fraction to lowest terms. Note that in this form, it is not obviously a function; we prove this in nqerf 10340. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ [Q] = ( ~Q ∩ ((N × N) × Q)) | ||
Definition | df-plq 10324 | Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. From Proposition 9-2.3 of [Gleason] p. 117. (Contributed by NM, 24-Aug-1995.) (New usage is discouraged.) |
⊢ +Q = (([Q] ∘ +pQ ) ↾ (Q × Q)) | ||
Definition | df-mq 10325 | Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. From Proposition 9-2.4 of [Gleason] p. 119. (Contributed by NM, 24-Aug-1995.) (New usage is discouraged.) |
⊢ ·Q = (([Q] ∘ ·pQ ) ↾ (Q × Q)) | ||
Definition | df-1nq 10326 | Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.) |
⊢ 1Q = 〈1o, 1o〉 | ||
Definition | df-rq 10327 | Define reciprocal on positive fractions. It means the same thing as one divided by the argument (although we don't define full division since we will never need it). This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. From Proposition 9-2.5 of [Gleason] p. 119, who uses an asterisk to denote this unary operation. (Contributed by NM, 6-Mar-1996.) (New usage is discouraged.) |
⊢ *Q = (◡ ·Q “ {1Q}) | ||
Definition | df-ltnq 10328 | Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 13-Feb-1996.) (New usage is discouraged.) |
⊢ <Q = ( <pQ ∩ (Q × Q)) | ||
Theorem | enqbreq 10329 | Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → (〈𝐴, 𝐵〉 ~Q 〈𝐶, 𝐷〉 ↔ (𝐴 ·N 𝐷) = (𝐵 ·N 𝐶))) | ||
Theorem | enqbreq2 10330 | Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ ((1st ‘𝐴) ·N (2nd ‘𝐵)) = ((1st ‘𝐵) ·N (2nd ‘𝐴)))) | ||
Theorem | enqer 10331 | The equivalence relation for positive fractions is an equivalence relation. Proposition 9-2.1 of [Gleason] p. 117. (Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) (New usage is discouraged.) |
⊢ ~Q Er (N × N) | ||
Theorem | enqex 10332 | The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
⊢ ~Q ∈ V | ||
Theorem | nqex 10333 | The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.) |
⊢ Q ∈ V | ||
Theorem | 0nnq 10334 | The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ Q | ||
Theorem | elpqn 10335 | Each positive fraction is an ordered pair of positive integers (the numerator and denominator, in "lowest terms". (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Q → 𝐴 ∈ (N × N)) | ||
Theorem | ltrelnq 10336 | Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.) |
⊢ <Q ⊆ (Q × Q) | ||
Theorem | pinq 10337 | The representatives of positive integers as positive fractions. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → 〈𝐴, 1o〉 ∈ Q) | ||
Theorem | 1nq 10338 | The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ 1Q ∈ Q | ||
Theorem | nqereu 10339* | There is a unique element of Q equivalent to each element of N × N. (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ (N × N) → ∃!𝑥 ∈ Q 𝑥 ~Q 𝐴) | ||
Theorem | nqerf 10340 | Corollary of nqereu 10339: the function [Q] is actually a function. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ [Q]:(N × N)⟶Q | ||
Theorem | nqercl 10341 | Corollary of nqereu 10339: closure of [Q]. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ (N × N) → ([Q]‘𝐴) ∈ Q) | ||
Theorem | nqerrel 10342 | Any member of (N × N) relates to the representative of its equivalence class. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ (N × N) → 𝐴 ~Q ([Q]‘𝐴)) | ||
Theorem | nqerid 10343 | Corollary of nqereu 10339: the function [Q] acts as the identity on members of Q. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Q → ([Q]‘𝐴) = 𝐴) | ||
Theorem | enqeq 10344 | Corollary of nqereu 10339: if two fractions are both reduced and equivalent, then they are equal. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q ∧ 𝐴 ~Q 𝐵) → 𝐴 = 𝐵) | ||
Theorem | nqereq 10345 | The function [Q] acts as a substitute for equivalence classes, and it satisfies the fundamental requirement for equivalence representatives: the representatives are equal iff the members are equivalent. (Contributed by Mario Carneiro, 6-May-2013.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ ([Q]‘𝐴) = ([Q]‘𝐵))) | ||
Theorem | addpipq2 10346 | Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 +pQ 𝐵) = 〈(((1st ‘𝐴) ·N (2nd ‘𝐵)) +N ((1st ‘𝐵) ·N (2nd ‘𝐴))), ((2nd ‘𝐴) ·N (2nd ‘𝐵))〉) | ||
Theorem | addpipq 10347 | Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → (〈𝐴, 𝐵〉 +pQ 〈𝐶, 𝐷〉) = 〈((𝐴 ·N 𝐷) +N (𝐶 ·N 𝐵)), (𝐵 ·N 𝐷)〉) | ||
Theorem | addpqnq 10348 | Addition of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 26-Dec-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) = ([Q]‘(𝐴 +pQ 𝐵))) | ||
Theorem | mulpipq2 10349 | Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → (𝐴 ·pQ 𝐵) = 〈((1st ‘𝐴) ·N (1st ‘𝐵)), ((2nd ‘𝐴) ·N (2nd ‘𝐵))〉) | ||
Theorem | mulpipq 10350 | Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ N ∧ 𝐵 ∈ N) ∧ (𝐶 ∈ N ∧ 𝐷 ∈ N)) → (〈𝐴, 𝐵〉 ·pQ 〈𝐶, 𝐷〉) = 〈(𝐴 ·N 𝐶), (𝐵 ·N 𝐷)〉) | ||
Theorem | mulpqnq 10351 | Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 26-Dec-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) = ([Q]‘(𝐴 ·pQ 𝐵))) | ||
Theorem | ordpipq 10352 | Ordering of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ (〈𝐴, 𝐵〉 <pQ 〈𝐶, 𝐷〉 ↔ (𝐴 ·N 𝐷) <N (𝐶 ·N 𝐵)) | ||
Theorem | ordpinq 10353 | Ordering of positive fractions in terms of positive integers. (Contributed by NM, 13-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 <Q 𝐵 ↔ ((1st ‘𝐴) ·N (2nd ‘𝐵)) <N ((1st ‘𝐵) ·N (2nd ‘𝐴)))) | ||
Theorem | addpqf 10354 | Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ +pQ :((N × N) × (N × N))⟶(N × N) | ||
Theorem | addclnq 10355 | Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 +Q 𝐵) ∈ Q) | ||
Theorem | mulpqf 10356 | Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ·pQ :((N × N) × (N × N))⟶(N × N) | ||
Theorem | mulclnq 10357 | Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) ∈ Q) | ||
Theorem | addnqf 10358 | Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
⊢ +Q :(Q × Q)⟶Q | ||
Theorem | mulnqf 10359 | Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
⊢ ·Q :(Q × Q)⟶Q | ||
Theorem | addcompq 10360 | Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ (𝐴 +pQ 𝐵) = (𝐵 +pQ 𝐴) | ||
Theorem | addcomnq 10361 | Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ (𝐴 +Q 𝐵) = (𝐵 +Q 𝐴) | ||
Theorem | mulcompq 10362 | Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ (𝐴 ·pQ 𝐵) = (𝐵 ·pQ 𝐴) | ||
Theorem | mulcomnq 10363 | Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ (𝐴 ·Q 𝐵) = (𝐵 ·Q 𝐴) | ||
Theorem | adderpqlem 10364 | Lemma for adderpq 10366. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 +pQ 𝐶) ~Q (𝐵 +pQ 𝐶))) | ||
Theorem | mulerpqlem 10365 | Lemma for mulerpq 10367. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 ·pQ 𝐶) ~Q (𝐵 ·pQ 𝐶))) | ||
Theorem | adderpq 10366 | Addition is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ (([Q]‘𝐴) +Q ([Q]‘𝐵)) = ([Q]‘(𝐴 +pQ 𝐵)) | ||
Theorem | mulerpq 10367 | Multiplication is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ (([Q]‘𝐴) ·Q ([Q]‘𝐵)) = ([Q]‘(𝐴 ·pQ 𝐵)) | ||
Theorem | addassnq 10368 | Addition of positive fractions is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ ((𝐴 +Q 𝐵) +Q 𝐶) = (𝐴 +Q (𝐵 +Q 𝐶)) | ||
Theorem | mulassnq 10369 | Multiplication of positive fractions is associative. (Contributed by NM, 1-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ·Q 𝐵) ·Q 𝐶) = (𝐴 ·Q (𝐵 ·Q 𝐶)) | ||
Theorem | mulcanenq 10370 | Lemma for distributive law: cancellation of common factor. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N) → 〈(𝐴 ·N 𝐵), (𝐴 ·N 𝐶)〉 ~Q 〈𝐵, 𝐶〉) | ||
Theorem | distrnq 10371 | Multiplication of positive fractions is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ (𝐴 ·Q (𝐵 +Q 𝐶)) = ((𝐴 ·Q 𝐵) +Q (𝐴 ·Q 𝐶)) | ||
Theorem | 1nqenq 10372 | The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → 1Q ~Q 〈𝐴, 𝐴〉) | ||
Theorem | mulidnq 10373 | Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Q → (𝐴 ·Q 1Q) = 𝐴) | ||
Theorem | recmulnq 10374 | Relationship between reciprocal and multiplication on positive fractions. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Q → ((*Q‘𝐴) = 𝐵 ↔ (𝐴 ·Q 𝐵) = 1Q)) | ||
Theorem | recidnq 10375 | A positive fraction times its reciprocal is 1. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Q → (𝐴 ·Q (*Q‘𝐴)) = 1Q) | ||
Theorem | recclnq 10376 | Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Q → (*Q‘𝐴) ∈ Q) | ||
Theorem | recrecnq 10377 | Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Q → (*Q‘(*Q‘𝐴)) = 𝐴) | ||
Theorem | dmrecnq 10378 | Domain of reciprocal on positive fractions. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
⊢ dom *Q = Q | ||
Theorem | ltsonq 10379 | 'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.) (New usage is discouraged.) |
⊢ <Q Or Q | ||
Theorem | lterpq 10380 | Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 <pQ 𝐵 ↔ ([Q]‘𝐴) <Q ([Q]‘𝐵)) | ||
Theorem | ltanq 10381 | Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ (𝐶 ∈ Q → (𝐴 <Q 𝐵 ↔ (𝐶 +Q 𝐴) <Q (𝐶 +Q 𝐵))) | ||
Theorem | ltmnq 10382 | Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of [Gleason] p. 120. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ (𝐶 ∈ Q → (𝐴 <Q 𝐵 ↔ (𝐶 ·Q 𝐴) <Q (𝐶 ·Q 𝐵))) | ||
Theorem | 1lt2nq 10383 | One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ 1Q <Q (1Q +Q 1Q) | ||
Theorem | ltaddnq 10384 | The sum of two fractions is greater than one of them. (Contributed by NM, 14-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → 𝐴 <Q (𝐴 +Q 𝐵)) | ||
Theorem | ltexnq 10385* | Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of [Gleason] p. 119. (Contributed by NM, 24-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ (𝐵 ∈ Q → (𝐴 <Q 𝐵 ↔ ∃𝑥(𝐴 +Q 𝑥) = 𝐵)) | ||
Theorem | halfnq 10386* | One-half of any positive fraction exists. Lemma for Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 16-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Q → ∃𝑥(𝑥 +Q 𝑥) = 𝐴) | ||
Theorem | nsmallnq 10387* | The is no smallest positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Q → ∃𝑥 𝑥 <Q 𝐴) | ||
Theorem | ltbtwnnq 10388* | There exists a number between any two positive fractions. Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 17-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 <Q 𝐵 ↔ ∃𝑥(𝐴 <Q 𝑥 ∧ 𝑥 <Q 𝐵)) | ||
Theorem | ltrnq 10389 | Ordering property of reciprocal for positive fractions. Proposition 9-2.6(iv) of [Gleason] p. 120. (Contributed by NM, 9-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 <Q 𝐵 ↔ (*Q‘𝐵) <Q (*Q‘𝐴)) | ||
Theorem | archnq 10390* | For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Mario Carneiro, 10-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Q → ∃𝑥 ∈ N 𝐴 <Q 〈𝑥, 1o〉) | ||
Definition | df-np 10391* | Define the set of positive reals. A "Dedekind cut" is a partition of the positive rational numbers into two classes such that all the numbers of one class are less than all the numbers of the other. A positive real is defined as the lower class of a Dedekind cut. Definition 9-3.1 of [Gleason] p. 121. (Note: This is a "temporary" definition used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |
⊢ P = {𝑥 ∣ ((∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q) ∧ ∀𝑦 ∈ 𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧))} | ||
Definition | df-1p 10392 | Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. Definition of [Gleason] p. 122. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.) |
⊢ 1P = {𝑥 ∣ 𝑥 <Q 1Q} | ||
Definition | df-plp 10393* | Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. From Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |
⊢ +P = (𝑥 ∈ P, 𝑦 ∈ P ↦ {𝑤 ∣ ∃𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑦 𝑤 = (𝑣 +Q 𝑢)}) | ||
Definition | df-mp 10394* | Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. From Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.) |
⊢ ·P = (𝑥 ∈ P, 𝑦 ∈ P ↦ {𝑤 ∣ ∃𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑦 𝑤 = (𝑣 ·Q 𝑢)}) | ||
Definition | df-ltp 10395* | Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 10531, and is intended to be used only by the construction. From Proposition 9-3.2 of [Gleason] p. 122. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |
⊢ <P = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ 𝑥 ⊊ 𝑦)} | ||
Theorem | npex 10396 | The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.) |
⊢ P ∈ V | ||
Theorem | elnp 10397* | Membership in positive reals. (Contributed by NM, 16-Feb-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ P ↔ ((∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧ ∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦))) | ||
Theorem | elnpi 10398* | Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ P ↔ ((𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q) ∧ ∀𝑥 ∈ 𝐴 (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 𝑥 <Q 𝑦))) | ||
Theorem | prn0 10399 | A positive real is not empty. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ P → 𝐴 ≠ ∅) | ||
Theorem | prpssnq 10400 | A positive real is a subset of the positive fractions. (Contributed by NM, 29-Feb-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ P → 𝐴 ⊊ Q) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |