Home | Metamath
Proof Explorer Theorem List (p. 104 of 450) | < 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-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | piord 10301 | A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → Ord 𝐴) | ||
Theorem | niex 10302 | The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ N ∈ V | ||
Theorem | 0npi 10303 | The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ N | ||
Theorem | 1pi 10304 | Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.) |
⊢ 1o ∈ N | ||
Theorem | addpiord 10305 | Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) = (𝐴 +o 𝐵)) | ||
Theorem | mulpiord 10306 | Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵)) | ||
Theorem | mulidpi 10307 | 1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → (𝐴 ·N 1o) = 𝐴) | ||
Theorem | ltpiord 10308 | Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <N 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | ltsopi 10309 | Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
⊢ <N Or N | ||
Theorem | ltrelpi 10310 | Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.) |
⊢ <N ⊆ (N × N) | ||
Theorem | dmaddpi 10311 | Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ dom +N = (N × N) | ||
Theorem | dmmulpi 10312 | Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ dom ·N = (N × N) | ||
Theorem | addclpi 10313 | Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) ∈ N) | ||
Theorem | mulclpi 10314 | Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) ∈ N) | ||
Theorem | addcompi 10315 | Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 +N 𝐵) = (𝐵 +N 𝐴) | ||
Theorem | addasspi 10316 | Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 +N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N 𝐶)) | ||
Theorem | mulcompi 10317 | Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ (𝐴 ·N 𝐵) = (𝐵 ·N 𝐴) | ||
Theorem | mulasspi 10318 | Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵 ·N 𝐶)) | ||
Theorem | distrpi 10319 | Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶)) | ||
Theorem | addcanpi 10320 | Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | mulcanpi 10321 | 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 10322 | There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → ¬ (𝐴 +N 𝐵) = 𝐴) | ||
Theorem | ltexpi 10323* | 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 10324 | Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.) |
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵))) | ||
Theorem | ltmpi 10325 | Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.) |
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 ·N 𝐴) <N (𝐶 ·N 𝐵))) | ||
Theorem | 1lt2pi 10326 | 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 10327 | No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
⊢ ¬ 𝐴 <N 1o | ||
Theorem | indpi 10328* | 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 10329* | Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10542, 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 10335) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 10332). (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 10330* | Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10542, 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 10331* | Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10542, 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 10332* | Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10542, 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 10333* | Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10542, 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 10334 | 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 10351. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ [Q] = ( ~Q ∩ ((N × N) × Q)) | ||
Definition | df-plq 10335 | Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10542, 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 10336 | Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10542, 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 10337 | Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 10542, 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 10338 | 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 10542, 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 10339 | Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10542, 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 10340 | 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 10341 | 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 10342 | 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 10343 | The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
⊢ ~Q ∈ V | ||
Theorem | nqex 10344 | 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 10345 | 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 10346 | 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 10347 | 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 10348 | 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 10349 | 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 10350* | 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 10351 | Corollary of nqereu 10350: the function [Q] is actually a function. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ [Q]:(N × N)⟶Q | ||
Theorem | nqercl 10352 | Corollary of nqereu 10350: closure of [Q]. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ (N × N) → ([Q]‘𝐴) ∈ Q) | ||
Theorem | nqerrel 10353 | 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 10354 | Corollary of nqereu 10350: 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 10355 | Corollary of nqereu 10350: 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 10356 | 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 10357 | 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 10358 | 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 10359 | 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 10360 | 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 10361 | 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 10362 | 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 10363 | 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 10364 | 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 10365 | 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 10366 | 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 10367 | 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 10368 | 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 10369 | 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 10370 | 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 10371 | 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 10372 | 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 10373 | 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 10374 | 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 10375 | Lemma for adderpq 10377. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 +pQ 𝐶) ~Q (𝐵 +pQ 𝐶))) | ||
Theorem | mulerpqlem 10376 | Lemma for mulerpq 10378. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 ·pQ 𝐶) ~Q (𝐵 ·pQ 𝐶))) | ||
Theorem | adderpq 10377 | 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 10378 | 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 10379 | 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 10380 | 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 10381 | 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 10382 | 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 10383 | 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 10384 | 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 10385 | 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 10386 | 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 10387 | 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 10388 | 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 10389 | 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 10390 | '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 10391 | Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 <pQ 𝐵 ↔ ([Q]‘𝐴) <Q ([Q]‘𝐵)) | ||
Theorem | ltanq 10392 | 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 10393 | 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 10394 | 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 10395 | 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 10396* | 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 10397* | 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 10398* | 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 10399* | 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 10400 | 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‘𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |