![]() |
Metamath
Proof Explorer Theorem List (p. 110 of 484) | < 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: | ![]() (1-30748) |
![]() (30749-32271) |
![]() (32272-48316) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cmr 10901 | Signed real multiplication. |
class ·R | ||
Syntax | cltr 10902 | Signed real ordering relation. |
class <R | ||
Definition | df-ni 10903 | Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11152, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ N = (ω ∖ {∅}) | ||
Definition | df-pli 10904 | Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11152, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ +N = ( +o ↾ (N × N)) | ||
Definition | df-mi 10905 | Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11152, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ ·N = ( ·o ↾ (N × N)) | ||
Definition | df-lti 10906 | Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11152, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.) (New usage is discouraged.) |
⊢ <N = ( E ∩ (N × N)) | ||
Theorem | elni 10907 | Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅)) | ||
Theorem | elni2 10908 | Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴)) | ||
Theorem | pinn 10909 | A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → 𝐴 ∈ ω) | ||
Theorem | pion 10910 | A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → 𝐴 ∈ On) | ||
Theorem | piord 10911 | A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → Ord 𝐴) | ||
Theorem | niex 10912 | The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ N ∈ V | ||
Theorem | 0npi 10913 | The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ N | ||
Theorem | 1pi 10914 | Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.) |
⊢ 1o ∈ N | ||
Theorem | addpiord 10915 | Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) = (𝐴 +o 𝐵)) | ||
Theorem | mulpiord 10916 | Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵)) | ||
Theorem | mulidpi 10917 | 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 10918 | 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 10919 | 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 10920 | 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 10921 | Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ dom +N = (N × N) | ||
Theorem | dmmulpi 10922 | Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ dom ·N = (N × N) | ||
Theorem | addclpi 10923 | Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) ∈ N) | ||
Theorem | mulclpi 10924 | Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) ∈ N) | ||
Theorem | addcompi 10925 | Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 +N 𝐵) = (𝐵 +N 𝐴) | ||
Theorem | addasspi 10926 | Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 +N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N 𝐶)) | ||
Theorem | mulcompi 10927 | Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ (𝐴 ·N 𝐵) = (𝐵 ·N 𝐴) | ||
Theorem | mulasspi 10928 | Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵 ·N 𝐶)) | ||
Theorem | distrpi 10929 | Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶)) | ||
Theorem | addcanpi 10930 | Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | mulcanpi 10931 | 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 10932 | There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → ¬ (𝐴 +N 𝐵) = 𝐴) | ||
Theorem | ltexpi 10933* | 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 10934 | Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.) |
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵))) | ||
Theorem | ltmpi 10935 | Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.) |
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 ·N 𝐴) <N (𝐶 ·N 𝐵))) | ||
Theorem | 1lt2pi 10936 | 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 10937 | No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
⊢ ¬ 𝐴 <N 1o | ||
Theorem | indpi 10938* | 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 10939* | Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11152, 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 10945) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 10942). (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 10940* | Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11152, 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 10941* | Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11152, 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 10942* | Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11152, 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 10943* | Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11152, 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 10944 | 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 10961. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ [Q] = ( ~Q ∩ ((N × N) × Q)) | ||
Definition | df-plq 10945 | Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11152, 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 10946 | Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11152, 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 10947 | Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 11152, 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 10948 | 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 11152, 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 10949 | Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 11152, 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 10950 | 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 10951 | 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 10952 | 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 10953 | The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
⊢ ~Q ∈ V | ||
Theorem | nqex 10954 | 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 10955 | 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 10956 | 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 10957 | 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 10958 | 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 10959 | 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 10960* | 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 10961 | Corollary of nqereu 10960: the function [Q] is actually a function. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ [Q]:(N × N)⟶Q | ||
Theorem | nqercl 10962 | Corollary of nqereu 10960: closure of [Q]. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ (N × N) → ([Q]‘𝐴) ∈ Q) | ||
Theorem | nqerrel 10963 | 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 10964 | Corollary of nqereu 10960: 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 10965 | Corollary of nqereu 10960: 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 10966 | 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 10967 | 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 10968 | 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 10969 | 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 10970 | 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 10971 | 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 10972 | 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 10973 | 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 10974 | 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 10975 | 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 10976 | 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 10977 | 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 10978 | 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 10979 | 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 10980 | 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 10981 | 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 10982 | 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 10983 | 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 10984 | 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 10985 | Lemma for adderpq 10987. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 +pQ 𝐶) ~Q (𝐵 +pQ 𝐶))) | ||
Theorem | mulerpqlem 10986 | Lemma for mulerpq 10988. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N) ∧ 𝐶 ∈ (N × N)) → (𝐴 ~Q 𝐵 ↔ (𝐴 ·pQ 𝐶) ~Q (𝐵 ·pQ 𝐶))) | ||
Theorem | adderpq 10987 | 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 10988 | 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 10989 | 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 10990 | 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 10991 | 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 10992 | 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 10993 | 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 10994 | 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 10995 | 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 10996 | 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 10997 | 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 10998 | 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 10999 | 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 11000 | '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 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |