P. 98 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pion 9701	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 9702	A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.)
|- ( A e. N. -> Ord A )
Theorem	niex 9703	The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
|- N. e. _V
Theorem	0npi 9704	The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
|- -. (/) e. N.
Theorem	1pi 9705	Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.)
|- 1o e. N.
Theorem	addpiord 9706	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 9707	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 9708	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 9709	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 9710	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 9711	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 9712	Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
|- dom +N = ( N. X. N. )
Theorem	dmmulpi 9713	Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
|- dom .N = ( N. X. N. )
Theorem	addclpi 9714	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 9715	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 9716	Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
|- ( A +N B ) = ( B +N A )
Theorem	addasspi 9717	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 9718	Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
|- ( A .N B ) = ( B .N A )
Theorem	mulasspi 9719	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 9720	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 9721	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 9722	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 9723	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 9724*	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 9725	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 9726	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 9727	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 9728	No positive integer is less than one. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
|- -. A <N 1o
Theorem	indpi 9729*	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 9730*	Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9736) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 9733). (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 9731*	Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9732*	Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9733*	Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9734*	Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9735	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 9752. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
|- /Q = ( ~Q i^i ( ( N. X. N. ) X. Q. ) )
Definition	df-plq 9736	Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9737	Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9738	Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9739	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 9942, 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 9740	Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 9942, 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 9741	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 9742	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 9743	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 9744	The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
|- ~Q e. _V
Theorem	nqex 9745	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 9746	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 9747	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 9748	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 9749	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 9750	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 9751*	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 9752	Corollary of nqereu 9751: 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 9753	Corollary of nqereu 9751: 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 9754	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 9755	Corollary of nqereu 9751: 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 9756	Corollary of nqereu 9751: 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 9757	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 9758	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 9759	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 9760	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 9761	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 9762	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 9763	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 9764	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 9765	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 9766	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 9767	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 9768	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 9769	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 9770	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 9771	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 9772	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 9773	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 9774	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 9775	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 9776	Lemma for adderpq 9778. (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 9777	Lemma for mulerpq 9779. (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 9778	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 9779	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 9780	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 9781	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 9782	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 9783	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 9784	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 9785	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 9786	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 9787	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 9788	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 9789	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 )
Theorem	dmrecnq 9790	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 9791	'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 9792	Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.)
|- ( A <pQ B <-> ( /Q ` A ) <Q ( /Q ` B ) )
Theorem	ltanq 9793	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.)
|- ( C e. Q. -> ( A <Q B <-> ( C +Q A ) <Q ( C +Q B ) ) )
Theorem	ltmnq 9794	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.)
|- ( C e. Q. -> ( A <Q B <-> ( C .Q A ) <Q ( C .Q B ) ) )
Theorem	1lt2nq 9795	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 9796	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.)
|- ( ( A e. Q. /\ B e. Q. ) -> A <Q ( A +Q B ) )
Theorem	ltexnq 9797*	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.)
|- ( B e. Q. -> ( A <Q B <-> E. x ( A +Q x ) = B ) )
Theorem	halfnq 9798*	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.)
|- ( A e. Q. -> E. x ( x +Q x ) = A )
Theorem	nsmallnq 9799*	The is no smallest positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( A e. Q. -> E. x x <Q A )
Theorem	ltbtwnnq 9800*	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.)
|- ( A <Q B <-> E. x ( A <Q x /\ x <Q B ) )