P. 88 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 8701-8800   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cm1r 8701	The signed real constant -1.
class -1R
Syntax	cplr 8702	Signed real addition.
class +R
Syntax	cmr 8703	Signed real multiplication.
class .R
Syntax	cltr 8704	Signed real ordering relation.
class <R
Definition	df-ni 8705	Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
|- N. = ( om \ { (/) } )
Definition	df-pli 8706	Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
|- +N = ( +o |` ( N. X. N. ) )
Definition	df-mi 8707	Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
|- .N = ( .o |` ( N. X. N. ) )
Definition	df-lti 8708	Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.) (New usage is discouraged.)
|- <N = ( _E i^i ( N. X. N. ) )
Theorem	elni 8709	Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
|- ( A e. N. <-> ( A e. om /\ A =/= (/) ) )
Theorem	elni2 8710	Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.)
|- ( A e. N. <-> ( A e. om /\ (/) e. A ) )
Theorem	pinn 8711	A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
|- ( A e. N. -> A e. om )
Theorem	pion 8712	A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
|- ( A e. N. -> A e. On )
Theorem	piord 8713	A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.)
|- ( A e. N. -> Ord A )
Theorem	niex 8714	The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
|- N. e. _V
Theorem	0npi 8715	The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
|- -. (/) e. N.
Theorem	1pi 8716	Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.)
|- 1o e. N.
Theorem	addpiord 8717	Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) = ( A +o B ) )
Theorem	mulpiord 8718	Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( A .o B ) )
Theorem	mulidpi 8719	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.)
|- ( A e. N. -> ( A .N 1o ) = A )
Theorem	ltpiord 8720	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.)
|- ( ( A e. N. /\ B e. N. ) -> ( A <N B <-> A e. B ) )
Theorem	ltsopi 8721	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 8722	Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.)
|- <N C_ ( N. X. N. )
Theorem	dmaddpi 8723	Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
|- dom +N = ( N. X. N. )
Theorem	dmmulpi 8724	Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
|- dom .N = ( N. X. N. )
Theorem	addclpi 8725	Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) e. N. )
Theorem	mulclpi 8726	Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
|- ( ( A e. N. /\ B e. N. ) -> ( A .N B ) e. N. )
Theorem	addcompi 8727	Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
|- ( A +N B ) = ( B +N A )
Theorem	addasspi 8728	Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
|- ( ( A +N B ) +N C ) = ( A +N ( B +N C ) )
Theorem	mulcompi 8729	Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
|- ( A .N B ) = ( B .N A )
Theorem	mulasspi 8730	Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
|- ( ( A .N B ) .N C ) = ( A .N ( B .N C ) )
Theorem	distrpi 8731	Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
|- ( A .N ( B +N C ) ) = ( ( A .N B ) +N ( A .N C ) )
Theorem	addcanpi 8732	Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. N. /\ B e. N. ) -> ( ( A +N B ) = ( A +N C ) <-> B = C ) )
Theorem	mulcanpi 8733	Multiplication cancellation law for positive integers. (Contributed by NM, 4-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( ( A e. N. /\ B e. N. ) -> ( ( A .N B ) = ( A .N C ) <-> B = C ) )
Theorem	addnidpi 8734	There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.)
|- ( A e. N. -> -. ( A +N B ) = A )
Theorem	ltexpi 8735*	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.)
|- ( ( A e. N. /\ B e. N. ) -> ( A <N B <-> E. x e. N. ( A +N x ) = B ) )
Theorem	ltapi 8736	Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.)
|- ( C e. N. -> ( A <N B <-> ( C +N A ) <N ( C +N B ) ) )
Theorem	ltmpi 8737	Ordering property of multiplication for positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.)
|- ( C e. N. -> ( A <N B <-> ( C .N A ) <N ( C .N B ) ) )
Theorem	1lt2pi 8738	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 8739	No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
|- -. A <N 1o
Theorem	indpi 8740*	Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
|- ( x = 1o -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y +N 1o ) -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> ta ) )   &    |- ps   &    |- ( y e. N. -> ( ch -> th ) )   =>    |- ( A e. N. -> ta )
Definition	df-plpq 8741*	Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8747) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 8744). (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 = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( ( 1st ` x ) .N ( 2nd ` y ) ) +N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
Definition	df-mpq 8742*	Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
Definition	df-ltpq 8743*	Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 = { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) <N ( ( 1st ` y ) .N ( 2nd ` x ) ) ) }
Definition	df-enq 8744*	Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 = { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) ) ) }
Definition	df-nq 8745*	Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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. = { x e. ( N. X. N. ) | A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) <N ( 2nd ` x ) ) }
Definition	df-erq 8746	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 8763. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
|- /Q = ( ~Q i^i ( ( N. X. N. ) X. Q. ) )
Definition	df-plq 8747	Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 o. +pQ ) |` ( Q. X. Q. ) )
Definition	df-mq 8748	Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 o. .pQ ) |` ( Q. X. Q. ) )
Definition	df-1nq 8749	Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8750	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 8952, 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 8751	Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 i^i ( Q. X. Q. ) )
Theorem	enqbreq 8752	Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( <. A , B >. ~Q <. C , D >. <-> ( A .N D ) = ( B .N C ) ) )
Theorem	enqbreq2 8753	Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q B <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) = ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
Theorem	enqer 8754	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. X. N. )
Theorem	enqex 8755	The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
|- ~Q e. _V
Theorem	nqex 8756	The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.)
|- Q. e. _V
Theorem	0nnq 8757	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.)
|- -. (/) e. Q.
Theorem	elpqn 8758	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.)
|- ( A e. Q. -> A e. ( N. X. N. ) )
Theorem	ltrelnq 8759	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 C_ ( Q. X. Q. )
Theorem	pinq 8760	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.)
|- ( A e. N. -> <. A , 1o >. e. Q. )
Theorem	1nq 8761	The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- 1Q e. Q.
Theorem	nqereu 8762*	There is a unique element of Q. equivalent to each element of N. X. N.. (Contributed by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A e. ( N. X. N. ) -> E! x e. Q. x ~Q A )
Theorem	nqerf 8763	Corollary of nqereu 8762: the function /Q is actually a function. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
|- /Q : ( N. X. N. ) --> Q.
Theorem	nqercl 8764	Corollary of nqereu 8762: closure of /Q. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
|- ( A e. ( N. X. N. ) -> ( /Q ` A ) e. Q. )
Theorem	nqerrel 8765	Any member of ( N. X. N. ) relates to the representative of its equivalence class. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
|- ( A e. ( N. X. N. ) -> A ~Q ( /Q ` A ) )
Theorem	nqerid 8766	Corollary of nqereu 8762: the function /Q acts as the identity on members of Q.. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
|- ( A e. Q. -> ( /Q ` A ) = A )
Theorem	enqeq 8767	Corollary of nqereu 8762: if two fractions are both reduced and equivalent, then they are equal. (Contributed by Mario Carneiro, 6-May-2013.) (New usage is discouraged.)
|- ( ( A e. Q. /\ B e. Q. /\ A ~Q B ) -> A = B )
Theorem	nqereq 8768	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.)
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q B <-> ( /Q ` A ) = ( /Q ` B ) ) )
Theorem	addpipq2 8769	Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A +pQ B ) = <. ( ( ( 1st ` A ) .N ( 2nd ` B ) ) +N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. )
Theorem	addpipq 8770	Addition of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( <. A , B >. +pQ <. C , D >. ) = <. ( ( A .N D ) +N ( C .N B ) ) , ( B .N D ) >. )
Theorem	addpqnq 8771	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.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) = ( /Q ` ( A +pQ B ) ) )
Theorem	mulpipq2 8772	Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) = <. ( ( 1st ` A ) .N ( 1st ` B ) ) , ( ( 2nd ` A ) .N ( 2nd ` B ) ) >. )
Theorem	mulpipq 8773	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.)
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( <. A , B >. .pQ <. C , D >. ) = <. ( A .N C ) , ( B .N D ) >. )
Theorem	mulpqnq 8774	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.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( /Q ` ( A .pQ B ) ) )
Theorem	ordpipq 8775	Ordering of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( <. A , B >. <pQ <. C , D >. <-> ( A .N D ) <N ( C .N B ) )
Theorem	ordpinq 8776	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.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A <Q B <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) <N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) )
Theorem	addpqf 8777	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. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )
Theorem	addclnq 8778	Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) e. Q. )
Theorem	mulpqf 8779	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. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )
Theorem	mulclnq 8780	Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) e. Q. )
Theorem	addnqf 8781	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. X. Q. ) --> Q.
Theorem	mulnqf 8782	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. X. Q. ) --> Q.
Theorem	addcompq 8783	Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A +pQ B ) = ( B +pQ A )
Theorem	addcomnq 8784	Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A +Q B ) = ( B +Q A )
Theorem	mulcompq 8785	Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A .pQ B ) = ( B .pQ A )
Theorem	mulcomnq 8786	Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A .Q B ) = ( B .Q A )
Theorem	adderpqlem 8787	Lemma for adderpq 8789. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A ~Q B <-> ( A +pQ C ) ~Q ( B +pQ C ) ) )
Theorem	mulerpqlem 8788	Lemma for mulerpq 8790. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A ~Q B <-> ( A .pQ C ) ~Q ( B .pQ C ) ) )
Theorem	adderpq 8789	Addition is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( /Q ` A ) +Q ( /Q ` B ) ) = ( /Q ` ( A +pQ B ) )
Theorem	mulerpq 8790	Multiplication is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( /Q ` A ) .Q ( /Q ` B ) ) = ( /Q ` ( A .pQ B ) )
Theorem	addassnq 8791	Addition of positive fractions is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( ( A +Q B ) +Q C ) = ( A +Q ( B +Q C ) )
Theorem	mulassnq 8792	Multiplication of positive fractions is associative. (Contributed by NM, 1-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A .Q B ) .Q C ) = ( A .Q ( B .Q C ) )
Theorem	mulcanenq 8793	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.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> <. ( A .N B ) , ( A .N C ) >. ~Q <. B , C >. )
Theorem	distrnq 8794	Multiplication of positive fractions is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A .Q ( B +Q C ) ) = ( ( A .Q B ) +Q ( A .Q C ) )
Theorem	1nqenq 8795	The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A e. N. -> 1Q ~Q <. A , A >. )
Theorem	mulidnq 8796	Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A e. Q. -> ( A .Q 1Q ) = A )
Theorem	recmulnq 8797	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.)
|- ( A e. Q. -> ( ( *Q ` A ) = B <-> ( A .Q B ) = 1Q ) )
Theorem	recidnq 8798	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.)
|- ( A e. Q. -> ( A .Q ( *Q ` A ) ) = 1Q )
Theorem	recclnq 8799	Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( A e. Q. -> ( *Q ` A ) e. Q. )
Theorem	recrecnq 8800	Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.) (New usage is discouraged.)
|- ( A e. Q. -> ( *Q ` ( *Q ` A ) ) = A )