![]() |
Metamath
Proof Explorer Theorem List (p. 101 of 437) | < 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-28361) |
![]() (28362-29886) |
![]() (29887-43649) |
Type | Label | Description |
---|---|---|
Statement | ||
This section derives the basics of real and complex numbers. We first construct and axiomatize real and complex numbers (e.g., ax-resscn 10329). After that, we derive their basic properties, various operations like addition (df-add 10283) and sine (df-sin 15202), and subsets such as the integers (df-z 11729) and natural numbers (df-nn 11375). | ||
Syntax | cnpi 10001 |
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. The last lemma of the construction is mulcnsrec 10301. The actual set of Dedekind cuts is defined by df-np 10138. |
class N | ||
Syntax | cpli 10002 | Positive integer addition. |
class +N | ||
Syntax | cmi 10003 | Positive integer multiplication. |
class ·N | ||
Syntax | clti 10004 | Positive integer ordering relation. |
class <N | ||
Syntax | cplpq 10005 | Positive pre-fraction addition. |
class +pQ | ||
Syntax | cmpq 10006 | Positive pre-fraction multiplication. |
class ·pQ | ||
Syntax | cltpq 10007 | Positive pre-fraction ordering relation. |
class <pQ | ||
Syntax | ceq 10008 | Equivalence class used to construct positive fractions. |
class ~Q | ||
Syntax | cnq 10009 | Set of positive fractions. |
class Q | ||
Syntax | c1q 10010 | The positive fraction constant 1. |
class 1Q | ||
Syntax | cerq 10011 | Positive fraction equivalence class. |
class [Q] | ||
Syntax | cplq 10012 | Positive fraction addition. |
class +Q | ||
Syntax | cmq 10013 | Positive fraction multiplication. |
class ·Q | ||
Syntax | crq 10014 | Positive fraction reciprocal operation. |
class *Q | ||
Syntax | cltq 10015 | Positive fraction ordering relation. |
class <Q | ||
Syntax | cnp 10016 | Set of positive reals. |
class P | ||
Syntax | c1p 10017 | Positive real constant 1. |
class 1P | ||
Syntax | cpp 10018 | Positive real addition. |
class +P | ||
Syntax | cmp 10019 | Positive real multiplication. |
class ·P | ||
Syntax | cltp 10020 | Positive real ordering relation. |
class <P | ||
Syntax | cer 10021 | Equivalence class used to construct signed reals. |
class ~R | ||
Syntax | cnr 10022 | Set of signed reals. |
class R | ||
Syntax | c0r 10023 | The signed real constant 0. |
class 0R | ||
Syntax | c1r 10024 | The signed real constant 1. |
class 1R | ||
Syntax | cm1r 10025 | The signed real constant -1. |
class -1R | ||
Syntax | cplr 10026 | Signed real addition. |
class +R | ||
Syntax | cmr 10027 | Signed real multiplication. |
class ·R | ||
Syntax | cltr 10028 | Signed real ordering relation. |
class <R | ||
Definition | df-ni 10029 | Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10278, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ N = (ω ∖ {∅}) | ||
Definition | df-pli 10030 | Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10031 | Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10032 | Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10033 | Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅)) | ||
Theorem | elni2 10034 | Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴)) | ||
Theorem | pinn 10035 | A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → 𝐴 ∈ ω) | ||
Theorem | pion 10036 | A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → 𝐴 ∈ On) | ||
Theorem | piord 10037 | A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → Ord 𝐴) | ||
Theorem | niex 10038 | The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.) |
⊢ N ∈ V | ||
Theorem | 0npi 10039 | The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ N | ||
Theorem | 1pi 10040 | Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.) |
⊢ 1o ∈ N | ||
Theorem | addpiord 10041 | Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) = (𝐴 +o 𝐵)) | ||
Theorem | mulpiord 10042 | Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵)) | ||
Theorem | mulidpi 10043 | 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 10044 | 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 10045 | 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 10046 | 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 10047 | Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ dom +N = (N × N) | ||
Theorem | dmmulpi 10048 | Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.) |
⊢ dom ·N = (N × N) | ||
Theorem | addclpi 10049 | Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) ∈ N) | ||
Theorem | mulclpi 10050 | Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) ∈ N) | ||
Theorem | addcompi 10051 | Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ (𝐴 +N 𝐵) = (𝐵 +N 𝐴) | ||
Theorem | addasspi 10052 | Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ ((𝐴 +N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N 𝐶)) | ||
Theorem | mulcompi 10053 | Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ (𝐴 ·N 𝐵) = (𝐵 ·N 𝐴) | ||
Theorem | mulasspi 10054 | Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ ((𝐴 ·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵 ·N 𝐶)) | ||
Theorem | distrpi 10055 | Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.) |
⊢ (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶)) | ||
Theorem | addcanpi 10056 | Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶)) | ||
Theorem | mulcanpi 10057 | 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 10058 | There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.) |
⊢ (𝐴 ∈ N → ¬ (𝐴 +N 𝐵) = 𝐴) | ||
Theorem | ltexpi 10059* | 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 10060 | Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.) |
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵))) | ||
Theorem | ltmpi 10061 | Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.) |
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 ·N 𝐴) <N (𝐶 ·N 𝐵))) | ||
Theorem | 1lt2pi 10062 | 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 10063 | No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.) |
⊢ ¬ 𝐴 <N 1o | ||
Theorem | indpi 10064* | 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 10065* | Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10071) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 10068). (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 10066* | Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10067* | Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10068* | Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10069* | Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10070 | 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 10087. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.) |
⊢ [Q] = ( ~Q ∩ ((N × N) × Q)) | ||
Definition | df-plq 10071 | Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10072 | Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10073 | Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10074 | 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 10278, 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 10075 | Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 10278, 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 10076 | 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 10077 | 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 10078 | 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 10079 | The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
⊢ ~Q ∈ V | ||
Theorem | nqex 10080 | 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 10081 | 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 10082 | 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 10083 | 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 10084 | 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 10085 | 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 10086* | 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 10087 | Corollary of nqereu 10086: the function [Q] is actually a function. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ [Q]:(N × N)⟶Q | ||
Theorem | nqercl 10088 | Corollary of nqereu 10086: closure of [Q]. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.) |
⊢ (𝐴 ∈ (N × N) → ([Q]‘𝐴) ∈ Q) | ||
Theorem | nqerrel 10089 | 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 10090 | Corollary of nqereu 10086: 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 10091 | Corollary of nqereu 10086: 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 10092 | 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 10093 | 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 10094 | 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 10095 | 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 10096 | 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 10097 | 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 10098 | 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 10099 | 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 10100 | 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 ‘𝐴)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |