P. 75 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7401-7500   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cplq0 7401	Nonnegative fraction addition.
class +Q0
Syntax	cmq0 7402	Nonnegative fraction multiplication.
class ·Q0
Syntax	cnp 7403	Set of positive reals.
class P.
Syntax	c1p 7404	Positive real constant 1.
class 1P
Syntax	cpp 7405	Positive real addition.
class +P.
Syntax	cmp 7406	Positive real multiplication.
class .P.
Syntax	cltp 7407	Positive real ordering relation.
class <P
Syntax	cer 7408	Equivalence class used to construct signed reals.
class ~R
Syntax	cnr 7409	Set of signed reals.
class R.
Syntax	c0r 7410	The signed real constant 0.
class 0R
Syntax	c1r 7411	The signed real constant 1.
class 1R
Syntax	cm1r 7412	The signed real constant -1.
class -1R
Syntax	cplr 7413	Signed real addition.
class +R
Syntax	cmr 7414	Signed real multiplication.
class .R
Syntax	cltr 7415	Signed real ordering relation.
class <R
Definition	df-ni 7416	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 7417	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 7418	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 7419	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 7420	Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.)
|- ( A e. N. <-> ( A e. om /\ A =/= (/) ) )
Theorem	pinn 7421	A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.)
|- ( A e. N. -> A e. om )
Theorem	pion 7422	A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.)
|- ( A e. N. -> A e. On )
Theorem	piord 7423	A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.)
|- ( A e. N. -> Ord A )
Theorem	niex 7424	The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.)
|- N. e. _V
Theorem	0npi 7425	The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.)
|- -. (/) e. N.
Theorem	elni2 7426	Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.)
|- ( A e. N. <-> ( A e. om /\ (/) e. A ) )
Theorem	1pi 7427	Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)
|- 1o e. N.
Theorem	addpiord 7428	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 7429	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 7430	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 7431	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 7432	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 7433	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 7434	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 7435	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 7436	Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.)
|- <N C_ ( N. X. N. )
Theorem	dmaddpi 7437	Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.)
|- dom +N = ( N. X. N. )
Theorem	dmmulpi 7438	Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.)
|- dom .N = ( N. X. N. )
Theorem	addclpi 7439	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 7440	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 7441	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 7442	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 7443	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 7444	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 7445	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 7446	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 7447	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 7448	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 7449*	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 7450	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 7451	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 7452	One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
|- 1o <N ( 1o +N 1o )
Theorem	nlt1pig 7453	No positive integer is less than one. (Contributed by Jim Kingdon, 31-Aug-2019.)
|- ( A e. N. -> -. A <N 1o )
Theorem	indpi 7454*	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 7455	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 7456*	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 7461) works with the equivalence classes of these ordered pairs determined by the equivalence relation ~Q (df-enq 7459). (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 7457*	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 7458*	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 7459*	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 7460	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 7461*	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 7462*	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 7463	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 7464*	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 7465*	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 7466*	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 7467*	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 7468	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 7469	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 7470	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 7471	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 7472	The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.)
|- ~Q e. _V
Theorem	enqdc 7473	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 7474	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 7475	The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
|- Q. e. _V
Theorem	0nnq 7476	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 7477	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 7478	The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
|- 1Q e. Q.
Theorem	addcmpblnq 7479	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 7480	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 7481	Lemma for addpipqqs 7482. (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 7482	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 7483	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 7484	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 7485	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 7486	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 7487	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 7488	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 7489*	Decomposition of a positive fraction into numerator and denominator. Lemma for dmaddpq 7491. (Contributed by Jim Kingdon, 15-Sep-2019.)
|- ( x e. Q. -> E. w E. v x = [ <. w , v >. ] ~Q )
Theorem	nqpi 7490*	Decomposition of a positive fraction into numerator and denominator. Similar to dmaddpqlem 7489 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 7491	Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.)
|- dom +Q = ( Q. X. Q. )
Theorem	dmmulpq 7492	Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.)
|- dom .Q = ( Q. X. Q. )
Theorem	addcomnqg 7493	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 7494	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 7495	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 7496	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 7497	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 7498	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 7499	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 7500	The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
|- ( A e. N. -> 1Q = [ <. A , A >. ] ~Q )