P. 66 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6501-6600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	piord 6501	A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.)
|- ( A e. N. -> Ord A )
Theorem	niex 6502	The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.)
|- N. e. _V
Theorem	0npi 6503	The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.)
|- -. (/) e. N.
Theorem	elni2 6504	Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.)
|- ( A e. N. <-> ( A e. om /\ (/) e. A ) )
Theorem	1pi 6505	Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)
|- 1o e. N.
Theorem	addpiord 6506	Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.)
|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) = ( A +o B ) )
Theorem	mulpiord 6507	Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.)
|- ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( A .o B ) )
Theorem	mulidpi 6508	1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. N. -> ( A .N 1o ) = A )
Theorem	ltpiord 6509	Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ( A e. N. /\ B e. N. ) -> ( A <N B <-> A e. B ) )
Theorem	ltsopi 6510	Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.)
|- <N Or N.
Theorem	pitric 6511	Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
|- ( ( A e. N. /\ B e. N. ) -> ( A <N B <-> -. ( A = B \/ B <N A ) ) )
Theorem	pitri3or 6512	Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
|- ( ( A e. N. /\ B e. N. ) -> ( A <N B \/ A = B \/ B <N A ) )
Theorem	ltdcpi 6513	Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ( ( A e. N. /\ B e. N. ) -> DECID A <N B )
Theorem	ltrelpi 6514	Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.)
|- <N C_ ( N. X. N. )
Theorem	dmaddpi 6515	Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.)
|- dom +N = ( N. X. N. )
Theorem	dmmulpi 6516	Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.)
|- dom .N = ( N. X. N. )
Theorem	addclpi 6517	Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.)
|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) e. N. )
Theorem	mulclpi 6518	Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.)
|- ( ( A e. N. /\ B e. N. ) -> ( A .N B ) e. N. )
Theorem	addcompig 6519	Addition of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.)
|- ( ( A e. N. /\ B e. N. ) -> ( A +N B ) = ( B +N A ) )
Theorem	addasspig 6520	Addition of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( ( A +N B ) +N C ) = ( A +N ( B +N C ) ) )
Theorem	mulcompig 6521	Multiplication of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.)
|- ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( B .N A ) )
Theorem	mulasspig 6522	Multiplication of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( ( A .N B ) .N C ) = ( A .N ( B .N C ) ) )
Theorem	distrpig 6523	Multiplication of positive integers is distributive. (Contributed by Jim Kingdon, 26-Aug-2019.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A .N ( B +N C ) ) = ( ( A .N B ) +N ( A .N C ) ) )
Theorem	addcanpig 6524	Addition cancellation law for positive integers. (Contributed by Jim Kingdon, 27-Aug-2019.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( ( A +N B ) = ( A +N C ) <-> B = C ) )
Theorem	mulcanpig 6525	Multiplication cancellation law for positive integers. (Contributed by Jim Kingdon, 29-Aug-2019.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( ( A .N B ) = ( A .N C ) <-> B = C ) )
Theorem	addnidpig 6526	There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.)
|- ( ( A e. N. /\ B e. N. ) -> -. ( A +N B ) = A )
Theorem	ltexpi 6527*	Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.)
|- ( ( A e. N. /\ B e. N. ) -> ( A <N B <-> E. x e. N. ( A +N x ) = B ) )
Theorem	ltapig 6528	Ordering property of addition for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A <N B <-> ( C +N A ) <N ( C +N B ) ) )
Theorem	ltmpig 6529	Ordering property of multiplication for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A <N B <-> ( C .N A ) <N ( C .N B ) ) )
Theorem	1lt2pi 6530	One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
|- 1o <N ( 1o +N 1o )
Theorem	nlt1pig 6531	No positive integer is less than one. (Contributed by Jim Kingdon, 31-Aug-2019.)
|- ( A e. N. -> -. A <N 1o )
Theorem	indpi 6532*	Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.)
|- ( 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 )
Theorem	nnppipi 6533	A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ( ( A e. om /\ B e. N. ) -> ( A +o B ) e. N. )
Definition	df-plpq 6534*	Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers, 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-plqqs 6539) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 6537). (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.)
|- +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 6535*	Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)
|- .pQ = ( x e. ( N. X. N. ) , y e. ( N. X. N. ) |-> <. ( ( 1st ` x ) .N ( 1st ` y ) ) , ( ( 2nd ` x ) .N ( 2nd ` y ) ) >. )
Definition	df-ltpq 6536*	Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 28-Aug-1995.)
|- <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 6537*	Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)
|- ~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-nqqs 6538	Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)
|- Q. = ( ( N. X. N. ) /. ~Q )
Definition	df-plqqs 6539*	Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)
|- +Q = { <. <. x , y >. , z >. | ( ( x e. Q. /\ y e. Q. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~Q /\ y = [ <. u , f >. ] ~Q ) /\ z = [ ( <. w , v >. +pQ <. u , f >. ) ] ~Q ) ) }
Definition	df-mqqs 6540*	Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers, 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.)
|- .Q = { <. <. x , y >. , z >. | ( ( x e. Q. /\ y e. Q. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~Q /\ y = [ <. u , f >. ] ~Q ) /\ z = [ ( <. w , v >. .pQ <. u , f >. ) ] ~Q ) ) }
Definition	df-1nqqs 6541	Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers, 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.)
|- 1Q = [ <. 1o , 1o >. ] ~Q
Definition	df-rq 6542*	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, 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 Jim Kingdon, 20-Sep-2019.)
|- *Q = { <. x , y >. | ( x e. Q. /\ y e. Q. /\ ( x .Q y ) = 1Q ) }
Definition	df-ltnqqs 6543*	Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 13-Feb-1996.)
|- <Q = { <. x , y >. | ( ( x e. Q. /\ y e. Q. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) ) ) }
Theorem	dfplpq2 6544*	Alternate definition of pre-addition on positive fractions. (Contributed by Jim Kingdon, 12-Sep-2019.)
|- +pQ = { <. <. x , y >. , z >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .N f ) +N ( v .N u ) ) , ( v .N f ) >. ) ) }
Theorem	dfmpq2 6545*	Alternate definition of pre-multiplication on positive fractions. (Contributed by Jim Kingdon, 13-Sep-2019.)
|- .pQ = { <. <. x , y >. , z >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w .N u ) , ( v .N f ) >. ) ) }
Theorem	enqbreq 6546	Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.)
|- ( ( ( 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 6547	Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.)
|- ( ( 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 6548	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.)
|- ~Q Er ( N. X. N. )
Theorem	enqeceq 6549	Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.)
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( [ <. A , B >. ] ~Q = [ <. C , D >. ] ~Q <-> ( A .N D ) = ( B .N C ) ) )
Theorem	enqex 6550	The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.)
|- ~Q e. _V
Theorem	enqdc 6551	The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> DECID <. A , B >. ~Q <. C , D >. )
Theorem	enqdc1 6552	The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
|- ( ( ( A e. N. /\ B e. N. ) /\ C e. ( N. X. N. ) ) -> DECID <. A , B >. ~Q C )
Theorem	nqex 6553	The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|- Q. e. _V
Theorem	0nnq 6554	The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|- -. (/) e. Q.
Theorem	ltrelnq 6555	Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.)
|- <Q C_ ( Q. X. Q. )
Theorem	1nq 6556	The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
|- 1Q e. Q.
Theorem	addcmpblnq 6557	Lemma showing compatibility of addition. (Contributed by NM, 27-Aug-1995.)
|- ( ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) /\ ( ( F e. N. /\ G e. N. ) /\ ( R e. N. /\ S e. N. ) ) ) -> ( ( ( A .N D ) = ( B .N C ) /\ ( F .N S ) = ( G .N R ) ) -> <. ( ( A .N G ) +N ( B .N F ) ) , ( B .N G ) >. ~Q <. ( ( C .N S ) +N ( D .N R ) ) , ( D .N S ) >. ) )
Theorem	mulcmpblnq 6558	Lemma showing compatibility of multiplication. (Contributed by NM, 27-Aug-1995.)
|- ( ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) /\ ( ( F e. N. /\ G e. N. ) /\ ( R e. N. /\ S e. N. ) ) ) -> ( ( ( A .N D ) = ( B .N C ) /\ ( F .N S ) = ( G .N R ) ) -> <. ( A .N F ) , ( B .N G ) >. ~Q <. ( C .N R ) , ( D .N S ) >. ) )
Theorem	addpipqqslem 6559	Lemma for addpipqqs 6560. (Contributed by Jim Kingdon, 11-Sep-2019.)
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> <. ( ( A .N D ) +N ( B .N C ) ) , ( B .N D ) >. e. ( N. X. N. ) )
Theorem	addpipqqs 6560	Addition of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.)
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( [ <. A , B >. ] ~Q +Q [ <. C , D >. ] ~Q ) = [ <. ( ( A .N D ) +N ( B .N C ) ) , ( B .N D ) >. ] ~Q )
Theorem	mulpipq2 6561	Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.)
|- ( ( 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 6562	Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.)
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( <. A , B >. .pQ <. C , D >. ) = <. ( A .N C ) , ( B .N D ) >. )
Theorem	mulpipqqs 6563	Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.)
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( [ <. A , B >. ] ~Q .Q [ <. C , D >. ] ~Q ) = [ <. ( A .N C ) , ( B .N D ) >. ] ~Q )
Theorem	ordpipqqs 6564	Ordering of positive fractions in terms of positive integers. (Contributed by Jim Kingdon, 14-Sep-2019.)
|- ( ( ( A e. N. /\ B e. N. ) /\ ( C e. N. /\ D e. N. ) ) -> ( [ <. A , B >. ] ~Q <Q [ <. C , D >. ] ~Q <-> ( A .N D ) <N ( B .N C ) ) )
Theorem	addclnq 6565	Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) e. Q. )
Theorem	mulclnq 6566	Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) e. Q. )
Theorem	dmaddpqlem 6567*	Decomposition of a positive fraction into numerator and denominator. Lemma for dmaddpq 6569. (Contributed by Jim Kingdon, 15-Sep-2019.)
|- ( x e. Q. -> E. w E. v x = [ <. w , v >. ] ~Q )
Theorem	nqpi 6568*	Decomposition of a positive fraction into numerator and denominator. Similar to dmaddpqlem 6567 but also shows that the numerator and denominator are positive integers. (Contributed by Jim Kingdon, 20-Sep-2019.)
|- ( A e. Q. -> E. w E. v ( ( w e. N. /\ v e. N. ) /\ A = [ <. w , v >. ] ~Q ) )
Theorem	dmaddpq 6569	Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.)
|- dom +Q = ( Q. X. Q. )
Theorem	dmmulpq 6570	Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.)
|- dom .Q = ( Q. X. Q. )
Theorem	addcomnqg 6571	Addition of positive fractions is commutative. (Contributed by Jim Kingdon, 15-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) = ( B +Q A ) )
Theorem	addassnqg 6572	Addition of positive fractions is associative. (Contributed by Jim Kingdon, 16-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A +Q B ) +Q C ) = ( A +Q ( B +Q C ) ) )
Theorem	mulcomnqg 6573	Multiplication of positive fractions is commutative. (Contributed by Jim Kingdon, 17-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( B .Q A ) )
Theorem	mulassnqg 6574	Multiplication of positive fractions is associative. (Contributed by Jim Kingdon, 17-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( ( A .Q B ) .Q C ) = ( A .Q ( B .Q C ) ) )
Theorem	mulcanenq 6575	Lemma for distributive law: cancellation of common factor. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> <. ( A .N B ) , ( A .N C ) >. ~Q <. B , C >. )
Theorem	mulcanenqec 6576	Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 17-Sep-2019.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> [ <. ( A .N B ) , ( A .N C ) >. ] ~Q = [ <. B , C >. ] ~Q )
Theorem	distrnqg 6577	Multiplication of positive fractions is distributive. (Contributed by Jim Kingdon, 17-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A .Q ( B +Q C ) ) = ( ( A .Q B ) +Q ( A .Q C ) ) )
Theorem	1qec 6578	The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
|- ( A e. N. -> 1Q = [ <. A , A >. ] ~Q )
Theorem	mulidnq 6579	Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.)
|- ( A e. Q. -> ( A .Q 1Q ) = A )
Theorem	recexnq 6580*	Existence of positive fraction reciprocal. (Contributed by Jim Kingdon, 20-Sep-2019.)
|- ( A e. Q. -> E. y ( y e. Q. /\ ( A .Q y ) = 1Q ) )
Theorem	recmulnqg 6581	Relationship between reciprocal and multiplication on positive fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( ( *Q ` A ) = B <-> ( A .Q B ) = 1Q ) )
Theorem	recclnq 6582	Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
|- ( A e. Q. -> ( *Q ` A ) e. Q. )
Theorem	recidnq 6583	A positive fraction times its reciprocal is 1. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
|- ( A e. Q. -> ( A .Q ( *Q ` A ) ) = 1Q )
Theorem	recrecnq 6584	Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)
|- ( A e. Q. -> ( *Q ` ( *Q ` A ) ) = A )
Theorem	rec1nq 6585	Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
|- ( *Q ` 1Q ) = 1Q
Theorem	nqtri3or 6586	Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A <Q B \/ A = B \/ B <Q A ) )
Theorem	ltdcnq 6587	Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ( ( A e. Q. /\ B e. Q. ) -> DECID A <Q B )
Theorem	ltsonq 6588	'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.)
|- <Q Or Q.
Theorem	nqtric 6589	Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A <Q B <-> -. ( A = B \/ B <Q A ) ) )
Theorem	ltanqg 6590	Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A <Q B <-> ( C +Q A ) <Q ( C +Q B ) ) )
Theorem	ltmnqg 6591	Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. /\ C e. Q. ) -> ( A <Q B <-> ( C .Q A ) <Q ( C .Q B ) ) )
Theorem	ltanqi 6592	Ordering property of addition for positive fractions. One direction of ltanqg 6590. (Contributed by Jim Kingdon, 9-Dec-2019.)
|- ( ( A <Q B /\ C e. Q. ) -> ( C +Q A ) <Q ( C +Q B ) )
Theorem	ltmnqi 6593	Ordering property of multiplication for positive fractions. One direction of ltmnqg 6591. (Contributed by Jim Kingdon, 9-Dec-2019.)
|- ( ( A <Q B /\ C e. Q. ) -> ( C .Q A ) <Q ( C .Q B ) )
Theorem	lt2addnq 6594	Ordering property of addition for positive fractions. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- ( ( ( A e. Q. /\ B e. Q. ) /\ ( C e. Q. /\ D e. Q. ) ) -> ( ( A <Q B /\ C <Q D ) -> ( A +Q C ) <Q ( B +Q D ) ) )
Theorem	lt2mulnq 6595	Ordering property of multiplication for positive fractions. (Contributed by Jim Kingdon, 18-Jul-2021.)
|- ( ( ( A e. Q. /\ B e. Q. ) /\ ( C e. Q. /\ D e. Q. ) ) -> ( ( A <Q B /\ C <Q D ) -> ( A .Q C ) <Q ( B .Q D ) ) )
Theorem	1lt2nq 6596	One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|- 1Q <Q ( 1Q +Q 1Q )
Theorem	ltaddnq 6597	The sum of two fractions is greater than one of them. (Contributed by NM, 14-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.)
|- ( ( A e. Q. /\ B e. Q. ) -> A <Q ( A +Q B ) )
Theorem	ltexnqq 6598*	Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of [Gleason] p. 119. (Contributed by Jim Kingdon, 23-Sep-2019.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A <Q B <-> E. x e. Q. ( A +Q x ) = B ) )
Theorem	ltexnqi 6599*	Ordering on positive fractions in terms of existence of sum. (Contributed by Jim Kingdon, 30-Apr-2020.)
|- ( A <Q B -> E. x e. Q. ( A +Q x ) = B )
Theorem	halfnqq 6600*	One-half of any positive fraction is a fraction. (Contributed by Jim Kingdon, 23-Sep-2019.)
|- ( A e. Q. -> E. x e. Q. ( x +Q x ) = A )