P. 74 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7301-7400   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cmr 7301	Signed real multiplication.
class .R
Syntax	cltr 7302	Signed real ordering relation.
class <R
Definition	df-ni 7303	Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.)
|- N. = ( om \ { (/) } )
Definition	df-pli 7304	Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.)
|- +N = ( +o |` ( N. X. N. ) )
Definition	df-mi 7305	Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.)
|- .N = ( .o |` ( N. X. N. ) )
Definition	df-lti 7306	Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.)
|- <N = ( _E i^i ( N. X. N. ) )
Theorem	elni 7307	Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.)
|- ( A e. N. <-> ( A e. om /\ A =/= (/) ) )
Theorem	pinn 7308	A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.)
|- ( A e. N. -> A e. om )
Theorem	pion 7309	A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.)
|- ( A e. N. -> A e. On )
Theorem	piord 7310	A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.)
|- ( A e. N. -> Ord A )
Theorem	niex 7311	The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.)
|- N. e. _V
Theorem	0npi 7312	The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.)
|- -. (/) e. N.
Theorem	elni2 7313	Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.)
|- ( A e. N. <-> ( A e. om /\ (/) e. A ) )
Theorem	1pi 7314	Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)
|- 1o e. N.
Theorem	addpiord 7315	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 7316	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 7317	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 7318	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 7319	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 7320	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 7321	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 7322	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 7323	Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.)
|- <N C_ ( N. X. N. )
Theorem	dmaddpi 7324	Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.)
|- dom +N = ( N. X. N. )
Theorem	dmmulpi 7325	Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.)
|- dom .N = ( N. X. N. )
Theorem	addclpi 7326	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 7327	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 7328	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 7329	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 7330	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 7331	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 7332	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 7333	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 7334	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 7335	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 7336*	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 7337	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 7338	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 7339	One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
|- 1o <N ( 1o +N 1o )
Theorem	nlt1pig 7340	No positive integer is less than one. (Contributed by Jim Kingdon, 31-Aug-2019.)
|- ( A e. N. -> -. A <N 1o )
Theorem	indpi 7341*	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 7342	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 7343*	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 7348) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 7346). (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 7344*	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 7345*	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 7346*	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 7347	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 7348*	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 7349*	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 7350	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 7351*	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 7352*	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 7353*	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 7354*	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 7355	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 7356	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 7357	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 7358	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 7359	The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.)
|- ~Q e. _V
Theorem	enqdc 7360	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 7361	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 7362	The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|- Q. e. _V
Theorem	0nnq 7363	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 7364	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 7365	The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
|- 1Q e. Q.
Theorem	addcmpblnq 7366	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 7367	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 7368	Lemma for addpipqqs 7369. (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 7369	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 7370	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 7371	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 7372	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 7373	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 7374	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 7375	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 7376*	Decomposition of a positive fraction into numerator and denominator. Lemma for dmaddpq 7378. (Contributed by Jim Kingdon, 15-Sep-2019.)
|- ( x e. Q. -> E. w E. v x = [ <. w , v >. ] ~Q )
Theorem	nqpi 7377*	Decomposition of a positive fraction into numerator and denominator. Similar to dmaddpqlem 7376 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 7378	Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.)
|- dom +Q = ( Q. X. Q. )
Theorem	dmmulpq 7379	Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.)
|- dom .Q = ( Q. X. Q. )
Theorem	addcomnqg 7380	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 7381	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 7382	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 7383	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 7384	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 7385	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 7386	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 7387	The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
|- ( A e. N. -> 1Q = [ <. A , A >. ] ~Q )
Theorem	mulidnq 7388	Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.)
|- ( A e. Q. -> ( A .Q 1Q ) = A )
Theorem	recexnq 7389*	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 7390	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 7391	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 7392	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 7393	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 7394	Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
|- ( *Q ` 1Q ) = 1Q
Theorem	nqtri3or 7395	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 7396	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 7397	'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 7398	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 7399	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 7400	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 ) ) )