P. 79 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7801-7900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	enq0ref 7801	The equivalence relation for nonnegative fractions is reflexive. Lemma for enq0er 7803. (Contributed by Jim Kingdon, 14-Nov-2019.)
|- ( f e. ( om X. N. ) <-> f ~Q0 f )
Theorem	enq0tr 7802	The equivalence relation for nonnegative fractions is transitive. Lemma for enq0er 7803. (Contributed by Jim Kingdon, 14-Nov-2019.)
|- ( ( f ~Q0 g /\ g ~Q0 h ) -> f ~Q0 h )
Theorem	enq0er 7803	The equivalence relation for nonnegative fractions is an equivalence relation. (Contributed by Jim Kingdon, 12-Nov-2019.)
|- ~Q0 Er ( om X. N. )
Theorem	enq0breq 7804	Equivalence relation for nonnegative fractions in terms of natural numbers. (Contributed by NM, 27-Aug-1995.)
|- ( ( ( A e. om /\ B e. N. ) /\ ( C e. om /\ D e. N. ) ) -> ( <. A , B >. ~Q0 <. C , D >. <-> ( A .o D ) = ( B .o C ) ) )
Theorem	enq0eceq 7805	Equivalence class equality of nonnegative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 24-Nov-2019.)
|- ( ( ( A e. om /\ B e. N. ) /\ ( C e. om /\ D e. N. ) ) -> ( [ <. A , B >. ] ~Q0 = [ <. C , D >. ] ~Q0 <-> ( A .o D ) = ( B .o C ) ) )
Theorem	nqnq0pi 7806	A nonnegative fraction is a positive fraction if its numerator and denominator are positive integers. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ( ( A e. N. /\ B e. N. ) -> [ <. A , B >. ] ~Q0 = [ <. A , B >. ] ~Q )
Theorem	enq0ex 7807	The equivalence relation for positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
|- ~Q0 e. _V
Theorem	nq0ex 7808	The class of positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.)
|- Q0 e. _V
Theorem	nqnq0 7809	A positive fraction is a nonnegative fraction. (Contributed by Jim Kingdon, 18-Nov-2019.)
|- Q. C_ Q0
Theorem	nq0nn 7810*	Decomposition of a nonnegative fraction into numerator and denominator. (Contributed by Jim Kingdon, 24-Nov-2019.)
|- ( A e. Q0 -> E. w E. v ( ( w e. om /\ v e. N. ) /\ A = [ <. w , v >. ] ~Q0 ) )
Theorem	addcmpblnq0 7811	Lemma showing compatibility of addition on nonnegative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
|- ( ( ( ( A e. om /\ B e. N. ) /\ ( C e. om /\ D e. N. ) ) /\ ( ( F e. om /\ G e. N. ) /\ ( R e. om /\ S e. N. ) ) ) -> ( ( ( A .o D ) = ( B .o C ) /\ ( F .o S ) = ( G .o R ) ) -> <. ( ( A .o G ) +o ( B .o F ) ) , ( B .o G ) >. ~Q0 <. ( ( C .o S ) +o ( D .o R ) ) , ( D .o S ) >. ) )
Theorem	mulcmpblnq0 7812	Lemma showing compatibility of multiplication on nonnegative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)
|- ( ( ( ( A e. om /\ B e. N. ) /\ ( C e. om /\ D e. N. ) ) /\ ( ( F e. om /\ G e. N. ) /\ ( R e. om /\ S e. N. ) ) ) -> ( ( ( A .o D ) = ( B .o C ) /\ ( F .o S ) = ( G .o R ) ) -> <. ( A .o F ) , ( B .o G ) >. ~Q0 <. ( C .o R ) , ( D .o S ) >. ) )
Theorem	mulcanenq0ec 7813	Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 29-Nov-2019.)
|- ( ( A e. N. /\ B e. om /\ C e. N. ) -> [ <. ( A .o B ) , ( A .o C ) >. ] ~Q0 = [ <. B , C >. ] ~Q0 )
Theorem	nnnq0lem1 7814*	Decomposing nonnegative fractions into natural numbers. Lemma for addnnnq0 7817 and mulnnnq0 7818. (Contributed by Jim Kingdon, 23-Nov-2019.)
|- ( ( ( A e. ( ( om X. N. ) /. ~Q0 ) /\ B e. ( ( om X. N. ) /. ~Q0 ) ) /\ ( ( ( A = [ <. w , v >. ] ~Q0 /\ B = [ <. u , t >. ] ~Q0 ) /\ z = [ C ] ~Q0 ) /\ ( ( A = [ <. s , f >. ] ~Q0 /\ B = [ <. g , h >. ] ~Q0 ) /\ q = [ D ] ~Q0 ) ) ) -> ( ( ( ( w e. om /\ v e. N. ) /\ ( s e. om /\ f e. N. ) ) /\ ( ( u e. om /\ t e. N. ) /\ ( g e. om /\ h e. N. ) ) ) /\ ( ( w .o f ) = ( v .o s ) /\ ( u .o h ) = ( t .o g ) ) ) )
Theorem	addnq0mo 7815*	There is at most one result from adding nonnegative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.)
|- ( ( A e. ( ( om X. N. ) /. ~Q0 ) /\ B e. ( ( om X. N. ) /. ~Q0 ) ) -> E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~Q0 /\ B = [ <. u , t >. ] ~Q0 ) /\ z = [ <. ( ( w .o t ) +o ( v .o u ) ) , ( v .o t ) >. ] ~Q0 ) )
Theorem	mulnq0mo 7816*	There is at most one result from multiplying nonnegative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.)
|- ( ( A e. ( ( om X. N. ) /. ~Q0 ) /\ B e. ( ( om X. N. ) /. ~Q0 ) ) -> E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~Q0 /\ B = [ <. u , t >. ] ~Q0 ) /\ z = [ <. ( w .o u ) , ( v .o t ) >. ] ~Q0 ) )
Theorem	addnnnq0 7817	Addition of nonnegative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 22-Nov-2019.)
|- ( ( ( A e. om /\ B e. N. ) /\ ( C e. om /\ D e. N. ) ) -> ( [ <. A , B >. ] ~Q0 +Q0 [ <. C , D >. ] ~Q0 ) = [ <. ( ( A .o D ) +o ( B .o C ) ) , ( B .o D ) >. ] ~Q0 )
Theorem	mulnnnq0 7818	Multiplication of nonnegative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 19-Nov-2019.)
|- ( ( ( A e. om /\ B e. N. ) /\ ( C e. om /\ D e. N. ) ) -> ( [ <. A , B >. ] ~Q0 ·Q0 [ <. C , D >. ] ~Q0 ) = [ <. ( A .o C ) , ( B .o D ) >. ] ~Q0 )
Theorem	addclnq0 7819	Closure of addition on nonnegative fractions. (Contributed by Jim Kingdon, 29-Nov-2019.)
|- ( ( A e. Q0 /\ B e. Q0 ) -> ( A +Q0 B ) e. Q0 )
Theorem	mulclnq0 7820	Closure of multiplication on nonnegative fractions. (Contributed by Jim Kingdon, 30-Nov-2019.)
|- ( ( A e. Q0 /\ B e. Q0 ) -> ( A ·Q0 B ) e. Q0 )
Theorem	nqpnq0nq 7821	A positive fraction plus a nonnegative fraction is a positive fraction. (Contributed by Jim Kingdon, 30-Nov-2019.)
|- ( ( A e. Q. /\ B e. Q0 ) -> ( A +Q0 B ) e. Q. )
Theorem	nqnq0a 7822	Addition of positive fractions is equal with +Q or +Q0. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A +Q B ) = ( A +Q0 B ) )
Theorem	nqnq0m 7823	Multiplication of positive fractions is equal with .Q or ·Q0. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A .Q B ) = ( A ·Q0 B ) )
Theorem	nq0m0r 7824	Multiplication with zero for nonnegative fractions. (Contributed by Jim Kingdon, 5-Nov-2019.)
|- ( A e. Q0 -> (0Q0 ·Q0 A ) = 0Q0 )
Theorem	nq0a0 7825	Addition with zero for nonnegative fractions. (Contributed by Jim Kingdon, 5-Nov-2019.)
|- ( A e. Q0 -> ( A +Q0 0Q0 ) = A )
Theorem	nnanq0 7826	Addition of nonnegative fractions with a common denominator. You can add two fractions with the same denominator by adding their numerators and keeping the same denominator. (Contributed by Jim Kingdon, 1-Dec-2019.)
|- ( ( N e. om /\ M e. om /\ A e. N. ) -> [ <. ( N +o M ) , A >. ] ~Q0 = ( [ <. N , A >. ] ~Q0 +Q0 [ <. M , A >. ] ~Q0 ) )
Theorem	distrnq0 7827	Multiplication of nonnegative fractions is distributive. (Contributed by Jim Kingdon, 27-Nov-2019.)
|- ( ( A e. Q0 /\ B e. Q0 /\ C e. Q0 ) -> ( A ·Q0 ( B +Q0 C ) ) = ( ( A ·Q0 B ) +Q0 ( A ·Q0 C ) ) )
Theorem	mulcomnq0 7828	Multiplication of nonnegative fractions is commutative. (Contributed by Jim Kingdon, 27-Nov-2019.)
|- ( ( A e. Q0 /\ B e. Q0 ) -> ( A ·Q0 B ) = ( B ·Q0 A ) )
Theorem	addassnq0lemcl 7829	A natural number closure law. Lemma for addassnq0 7830. (Contributed by Jim Kingdon, 3-Dec-2019.)
|- ( ( ( I e. om /\ J e. N. ) /\ ( K e. om /\ L e. N. ) ) -> ( ( ( I .o L ) +o ( J .o K ) ) e. om /\ ( J .o L ) e. N. ) )
Theorem	addassnq0 7830	Addition of nonnegative fractions is associative. (Contributed by Jim Kingdon, 29-Nov-2019.)
|- ( ( A e. Q0 /\ B e. Q0 /\ C e. Q0 ) -> ( ( A +Q0 B ) +Q0 C ) = ( A +Q0 ( B +Q0 C ) ) )
Theorem	distnq0r 7831	Multiplication of nonnegative fractions is distributive. Version of distrnq0 7827 with the multiplications commuted. (Contributed by Jim Kingdon, 29-Nov-2019.)
|- ( ( A e. Q0 /\ B e. Q0 /\ C e. Q0 ) -> ( ( B +Q0 C ) ·Q0 A ) = ( ( B ·Q0 A ) +Q0 ( C ·Q0 A ) ) )
Theorem	addpinq1 7832	Addition of one to the numerator of a fraction whose denominator is one. (Contributed by Jim Kingdon, 26-Apr-2020.)
|- ( A e. N. -> [ <. ( A +N 1o ) , 1o >. ] ~Q = ( [ <. A , 1o >. ] ~Q +Q 1Q ) )
Theorem	nq02m 7833	Multiply a nonnegative fraction by two. (Contributed by Jim Kingdon, 29-Nov-2019.)
|- ( A e. Q0 -> ( [ <. 2o , 1o >. ] ~Q0 ·Q0 A ) = ( A +Q0 A ) )
Definition	df-inp 7834*	Define the set of positive reals. A "Dedekind cut" is a partition of the positive rational numbers into two classes such that all the numbers of one class are less than all the numbers of the other. Here we follow the definition of a Dedekind cut from Definition 11.2.1 of [HoTT], p. (varies) with the one exception that we define it over positive rational numbers rather than all rational numbers. A Dedekind cut is an ordered pair of a lower set l and an upper set u which is inhabited ( E. q e. Q. q e. l /\ E. r e. Q. r e. u), rounded ( A. q e. Q. ( q e. l <-> E. r e. Q. ( q <Q r /\ r e. l ) ) and likewise for u), disjoint ( A. q e. Q. -. ( q e. l /\ q e. u )) and located ( A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. l \/ r e. u ) )). See HoTT for more discussion of those terms and different ways of defining Dedekind cuts. (Note: This is a "temporary" definition used in the construction of complex numbers, and is intended to be used only by the construction.) (Contributed by Jim Kingdon, 25-Sep-2019.)
|- P. = { <. l , u >. | ( ( ( l C_ Q. /\ u C_ Q. ) /\ ( E. q e. Q. q e. l /\ E. r e. Q. r e. u ) ) /\ ( ( A. q e. Q. ( q e. l <-> E. r e. Q. ( q <Q r /\ r e. l ) ) /\ A. r e. Q. ( r e. u <-> E. q e. Q. ( q <Q r /\ q e. u ) ) ) /\ A. q e. Q. -. ( q e. l /\ q e. u ) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. l \/ r e. u ) ) ) ) }
Definition	df-i1p 7835*	Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers and is intended to be used only by the construction. (Contributed by Jim Kingdon, 25-Sep-2019.)
|- 1P = <. { l | l <Q 1Q } , { u | 1Q <Q u } >.
Definition	df-iplp 7836*	Define addition on positive reals. From Section 11.2.1 of [HoTT], p. (varies). We write this definition to closely resemble the definition in HoTT although some of the conditions are redundant (for example, r e. ( 1st ` x ) implies r e. Q.) and can be simplified as shown at genpdf 7876. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 26-Sep-2019.)
|- +P. = ( x e. P. , y e. P. |-> <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r +Q s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r +Q s ) ) } >. )
Definition	df-imp 7837*	Define multiplication on positive reals. Here we use a simple definition which is similar to df-iplp 7836 or the definition of multiplication on positive reals in Metamath Proof Explorer. This is as opposed to the more complicated definition of multiplication given in Section 11.2.1 of [HoTT], p. (varies), which appears to be motivated by handling negative numbers or handling modified Dedekind cuts in which locatedness is omitted. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 29-Sep-2019.)
|- .P. = ( x e. P. , y e. P. |-> <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` x ) /\ s e. ( 1st ` y ) /\ q = ( r .Q s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` x ) /\ s e. ( 2nd ` y ) /\ q = ( r .Q s ) ) } >. )
Definition	df-iltp 7838*	Define ordering on positive reals. We define x <P y if there is a positive fraction q which is an element of the upper cut of x and the lower cut of y. From the definition of < in Section 11.2.1 of [HoTT], p. (varies). This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 29-Sep-2019.)
|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ E. q e. Q. ( q e. ( 2nd ` x ) /\ q e. ( 1st ` y ) ) ) }
Theorem	npsspw 7839	Lemma for proving existence of reals. (Contributed by Jim Kingdon, 27-Sep-2019.)
|- P. C_ ( ~P Q. X. ~P Q. )
Theorem	preqlu 7840	Two reals are equal if and only if their lower and upper cuts are. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- ( ( A e. P. /\ B e. P. ) -> ( A = B <-> ( ( 1st ` A ) = ( 1st ` B ) /\ ( 2nd ` A ) = ( 2nd ` B ) ) ) )
Theorem	npex 7841	The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.)
|- P. e. _V
Theorem	elinp 7842*	Membership in positive reals. (Contributed by Jim Kingdon, 27-Sep-2019.)
|- ( <. L , U >. e. P. <-> ( ( ( L C_ Q. /\ U C_ Q. ) /\ ( E. q e. Q. q e. L /\ E. r e. Q. r e. U ) ) /\ ( ( A. q e. Q. ( q e. L <-> E. r e. Q. ( q <Q r /\ r e. L ) ) /\ A. r e. Q. ( r e. U <-> E. q e. Q. ( q <Q r /\ q e. U ) ) ) /\ A. q e. Q. -. ( q e. L /\ q e. U ) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. L \/ r e. U ) ) ) ) )
Theorem	prop 7843	A positive real is an ordered pair of a lower cut and an upper cut. (Contributed by Jim Kingdon, 27-Sep-2019.)
|- ( A e. P. -> <. ( 1st ` A ) , ( 2nd ` A ) >. e. P. )
Theorem	elnp1st2nd 7844*	Membership in positive reals, using 1st and 2nd to refer to the lower and upper cut. (Contributed by Jim Kingdon, 3-Oct-2019.)
|- ( A e. P. <-> ( ( A e. ( ~P Q. X. ~P Q. ) /\ ( E. q e. Q. q e. ( 1st ` A ) /\ E. r e. Q. r e. ( 2nd ` A ) ) ) /\ ( ( A. q e. Q. ( q e. ( 1st ` A ) <-> E. r e. Q. ( q <Q r /\ r e. ( 1st ` A ) ) ) /\ A. r e. Q. ( r e. ( 2nd ` A ) <-> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` A ) ) ) ) /\ A. q e. Q. -. ( q e. ( 1st ` A ) /\ q e. ( 2nd ` A ) ) /\ A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. ( 1st ` A ) \/ r e. ( 2nd ` A ) ) ) ) ) )
Theorem	prml 7845*	A positive real's lower cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.)
|- ( <. L , U >. e. P. -> E. x e. Q. x e. L )
Theorem	prmu 7846*	A positive real's upper cut is inhabited. (Contributed by Jim Kingdon, 27-Sep-2019.)
|- ( <. L , U >. e. P. -> E. x e. Q. x e. U )
Theorem	prssnql 7847	The lower cut of a positive real is a subset of the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- ( <. L , U >. e. P. -> L C_ Q. )
Theorem	prssnqu 7848	The upper cut of a positive real is a subset of the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- ( <. L , U >. e. P. -> U C_ Q. )
Theorem	elprnql 7849	An element of a positive real's lower cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- ( ( <. L , U >. e. P. /\ B e. L ) -> B e. Q. )
Theorem	elprnqu 7850	An element of a positive real's upper cut is a positive fraction. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- ( ( <. L , U >. e. P. /\ B e. U ) -> B e. Q. )
Theorem	0npr 7851	The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.)
|- -. (/) e. P.
Theorem	prcdnql 7852	A lower cut is closed downwards under the positive fractions. (Contributed by Jim Kingdon, 28-Sep-2019.)
|- ( ( <. L , U >. e. P. /\ B e. L ) -> ( C <Q B -> C e. L ) )
Theorem	prcunqu 7853	An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.)
|- ( ( <. L , U >. e. P. /\ C e. U ) -> ( C <Q B -> B e. U ) )
Theorem	prubl 7854	A positive fraction not in a lower cut is an upper bound. (Contributed by Jim Kingdon, 29-Sep-2019.)
|- ( ( ( <. L , U >. e. P. /\ B e. L ) /\ C e. Q. ) -> ( -. C e. L -> B <Q C ) )
Theorem	prltlu 7855	An element of a lower cut is less than an element of the corresponding upper cut. (Contributed by Jim Kingdon, 15-Oct-2019.)
|- ( ( <. L , U >. e. P. /\ B e. L /\ C e. U ) -> B <Q C )
Theorem	prnmaxl 7856*	A lower cut has no largest member. (Contributed by Jim Kingdon, 29-Sep-2019.)
|- ( ( <. L , U >. e. P. /\ B e. L ) -> E. x e. L B <Q x )
Theorem	prnminu 7857*	An upper cut has no smallest member. (Contributed by Jim Kingdon, 7-Nov-2019.)
|- ( ( <. L , U >. e. P. /\ B e. U ) -> E. x e. U x <Q B )
Theorem	prnmaddl 7858*	A lower cut has no largest member. Addition version. (Contributed by Jim Kingdon, 29-Sep-2019.)
|- ( ( <. L , U >. e. P. /\ B e. L ) -> E. x e. Q. ( B +Q x ) e. L )
Theorem	prloc 7859	A Dedekind cut is located. (Contributed by Jim Kingdon, 23-Oct-2019.)
|- ( ( <. L , U >. e. P. /\ A <Q B ) -> ( A e. L \/ B e. U ) )
Theorem	prdisj 7860	A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.)
|- ( ( <. L , U >. e. P. /\ A e. Q. ) -> -. ( A e. L /\ A e. U ) )
Theorem	prarloclemlt 7861	Two possible ways of contracting an interval which straddles a Dedekind cut. Lemma for prarloc 7871. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ( ( ( X e. om /\ ( <. L , U >. e. P. /\ A e. L /\ P e. Q. ) ) /\ y e. om ) -> ( A +Q ( [ <. ( y +o 1o ) , 1o >. ] ~Q .Q P ) ) <Q ( A +Q ( [ <. ( ( y +o 2o ) +o X ) , 1o >. ] ~Q .Q P ) ) )
Theorem	prarloclemlo 7862*	Contracting the lower side of an interval which straddles a Dedekind cut. Lemma for prarloc 7871. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ( ( ( X e. om /\ ( <. L , U >. e. P. /\ A e. L /\ P e. Q. ) ) /\ y e. om ) -> ( ( A +Q ( [ <. ( y +o 1o ) , 1o >. ] ~Q .Q P ) ) e. L -> ( ( ( A +Q0 ( [ <. y , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( ( y +o 2o ) +o suc X ) , 1o >. ] ~Q .Q P ) ) e. U ) -> E. y e. om ( ( A +Q0 ( [ <. y , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( ( y +o 2o ) +o X ) , 1o >. ] ~Q .Q P ) ) e. U ) ) ) )
Theorem	prarloclemup 7863	Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 7871. (Contributed by Jim Kingdon, 10-Nov-2019.)
|- ( ( ( X e. om /\ ( <. L , U >. e. P. /\ A e. L /\ P e. Q. ) ) /\ y e. om ) -> ( ( A +Q ( [ <. ( ( y +o 2o ) +o X ) , 1o >. ] ~Q .Q P ) ) e. U -> ( ( ( A +Q0 ( [ <. y , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( ( y +o 2o ) +o suc X ) , 1o >. ] ~Q .Q P ) ) e. U ) -> E. y e. om ( ( A +Q0 ( [ <. y , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( ( y +o 2o ) +o X ) , 1o >. ] ~Q .Q P ) ) e. U ) ) ) )
Theorem	prarloclem3step 7864*	Induction step for prarloclem3 7865. (Contributed by Jim Kingdon, 9-Nov-2019.)
|- ( ( ( X e. om /\ ( <. L , U >. e. P. /\ A e. L /\ P e. Q. ) ) /\ E. y e. om ( ( A +Q0 ( [ <. y , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( ( y +o 2o ) +o suc X ) , 1o >. ] ~Q .Q P ) ) e. U ) ) -> E. y e. om ( ( A +Q0 ( [ <. y , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( ( y +o 2o ) +o X ) , 1o >. ] ~Q .Q P ) ) e. U ) )
Theorem	prarloclem3 7865*	Contracting an interval which straddles a Dedekind cut. Lemma for prarloc 7871. (Contributed by Jim Kingdon, 27-Oct-2019.)
|- ( ( ( <. L , U >. e. P. /\ A e. L ) /\ ( X e. om /\ P e. Q. ) /\ E. y e. om ( ( A +Q0 ( [ <. y , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( ( y +o 2o ) +o X ) , 1o >. ] ~Q .Q P ) ) e. U ) ) -> E. j e. om ( ( A +Q0 ( [ <. j , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( j +o 2o ) , 1o >. ] ~Q .Q P ) ) e. U ) )
Theorem	prarloclem4 7866*	A slight rearrangement of prarloclem3 7865. Lemma for prarloc 7871. (Contributed by Jim Kingdon, 4-Nov-2019.)
|- ( ( ( <. L , U >. e. P. /\ A e. L ) /\ P e. Q. ) -> ( E. x e. om E. y e. om ( ( A +Q0 ( [ <. y , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( ( y +o 2o ) +o x ) , 1o >. ] ~Q .Q P ) ) e. U ) -> E. j e. om ( ( A +Q0 ( [ <. j , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( j +o 2o ) , 1o >. ] ~Q .Q P ) ) e. U ) ) )
Theorem	prarloclemn 7867*	Subtracting two from a positive integer. Lemma for prarloc 7871. (Contributed by Jim Kingdon, 5-Nov-2019.)
|- ( ( N e. N. /\ 1o <N N ) -> E. x e. om ( 2o +o x ) = N )
Theorem	prarloclem5 7868*	A substitution of zero for y and N minus two for x. Lemma for prarloc 7871. (Contributed by Jim Kingdon, 4-Nov-2019.)
|- ( ( ( <. L , U >. e. P. /\ A e. L ) /\ ( N e. N. /\ P e. Q. /\ 1o <N N ) /\ ( A +Q ( [ <. N , 1o >. ] ~Q .Q P ) ) e. U ) -> E. x e. om E. y e. om ( ( A +Q0 ( [ <. y , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( ( y +o 2o ) +o x ) , 1o >. ] ~Q .Q P ) ) e. U ) )
Theorem	prarloclem 7869*	A special case of Lemma 6.16 from [BauerTaylor], p. 32. Given evenly spaced rational numbers from A to A +Q ( N .Q P ) (which are in the lower and upper cuts, respectively, of a real number), there are a pair of numbers, two positions apart in the even spacing, which straddle the cut. (Contributed by Jim Kingdon, 22-Oct-2019.)
|- ( ( ( <. L , U >. e. P. /\ A e. L ) /\ ( N e. N. /\ P e. Q. /\ 1o <N N ) /\ ( A +Q ( [ <. N , 1o >. ] ~Q .Q P ) ) e. U ) -> E. j e. om ( ( A +Q0 ( [ <. j , 1o >. ] ~Q0 ·Q0 P ) ) e. L /\ ( A +Q ( [ <. ( j +o 2o ) , 1o >. ] ~Q .Q P ) ) e. U ) )
Theorem	prarloclemcalc 7870	Some calculations for prarloc 7871. (Contributed by Jim Kingdon, 26-Oct-2019.)
|- ( ( ( A = ( X +Q0 ( [ <. M , 1o >. ] ~Q0 ·Q0 Q ) ) /\ B = ( X +Q ( [ <. ( M +o 2o ) , 1o >. ] ~Q .Q Q ) ) ) /\ ( ( Q e. Q. /\ ( Q +Q Q ) <Q P ) /\ ( X e. Q. /\ M e. om ) ) ) -> B <Q ( A +Q P ) )
Theorem	prarloc 7871*	A Dedekind cut is arithmetically located. Part of Proposition 11.15 of [BauerTaylor], p. 52, slightly modified. It states that given a tolerance P, there are elements of the lower and upper cut which are within that tolerance of each other. Usually, proofs will be shorter if they use prarloc2 7872 instead. (Contributed by Jim Kingdon, 22-Oct-2019.)
|- ( ( <. L , U >. e. P. /\ P e. Q. ) -> E. a e. L E. b e. U b <Q ( a +Q P ) )
Theorem	prarloc2 7872*	A Dedekind cut is arithmetically located. This is a variation of prarloc 7871 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance P, there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.)
|- ( ( <. L , U >. e. P. /\ P e. Q. ) -> E. a e. L ( a +Q P ) e. U )
Theorem	ltrelpr 7873	Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.)
|- <P C_ ( P. X. P. )
Theorem	ltdfpr 7874*	More convenient form of df-iltp 7838. (Contributed by Jim Kingdon, 15-Dec-2019.)
|- ( ( A e. P. /\ B e. P. ) -> ( A <P B <-> E. q e. Q. ( q e. ( 2nd ` A ) /\ q e. ( 1st ` B ) ) ) )
Theorem	genpdflem 7875*	Simplification of upper or lower cut expression. Lemma for genpdf 7876. (Contributed by Jim Kingdon, 30-Sep-2019.)
|- ( ( ph /\ r e. A ) -> r e. Q. )   &    |- ( ( ph /\ s e. B ) -> s e. Q. )   =>    |- ( ph -> { q e. Q. | E. r e. Q. E. s e. Q. ( r e. A /\ s e. B /\ q = ( r G s ) ) } = { q e. Q. | E. r e. A E. s e. B q = ( r G s ) } )
Theorem	genpdf 7876*	Simplified definition of addition or multiplication on positive reals. (Contributed by Jim Kingdon, 30-Sep-2019.)
|- F = ( w e. P. , v e. P. |-> <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` w ) /\ s e. ( 1st ` v ) /\ q = ( r G s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` w ) /\ s e. ( 2nd ` v ) /\ q = ( r G s ) ) } >. )   =>    |- F = ( w e. P. , v e. P. |-> <. { q e. Q. | E. r e. ( 1st ` w ) E. s e. ( 1st ` v ) q = ( r G s ) } , { q e. Q. | E. r e. ( 2nd ` w ) E. s e. ( 2nd ` v ) q = ( r G s ) } >. )
Theorem	genipv 7877*	Value of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingon, 3-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( A F B ) = <. { q e. Q. | E. r e. ( 1st ` A ) E. s e. ( 1st ` B ) q = ( r G s ) } , { q e. Q. | E. r e. ( 2nd ` A ) E. s e. ( 2nd ` B ) q = ( r G s ) } >. )
Theorem	genplt2i 7878*	Operating on both sides of two inequalities, when the operation is consistent with <Q. (Contributed by Jim Kingdon, 6-Oct-2019.)
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x <Q y <-> ( z G x ) <Q ( z G y ) ) )   &    |- ( ( x e. Q. /\ y e. Q. ) -> ( x G y ) = ( y G x ) )   =>    |- ( ( A <Q B /\ C <Q D ) -> ( A G C ) <Q ( B G D ) )
Theorem	genpelxp 7879*	Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( A F B ) e. ( ~P Q. X. ~P Q. ) )
Theorem	genpelvl 7880*	Membership in lower cut of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingdon, 2-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( C e. ( 1st ` ( A F B ) ) <-> E. g e. ( 1st ` A ) E. h e. ( 1st ` B ) C = ( g G h ) ) )
Theorem	genpelvu 7881*	Membership in upper cut of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingdon, 15-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( C e. ( 2nd ` ( A F B ) ) <-> E. g e. ( 2nd ` A ) E. h e. ( 2nd ` B ) C = ( g G h ) ) )
Theorem	genpprecll 7882*	Pre-closure law for general operation on lower cuts. (Contributed by Jim Kingdon, 2-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( ( C e. ( 1st ` A ) /\ D e. ( 1st ` B ) ) -> ( C G D ) e. ( 1st ` ( A F B ) ) ) )
Theorem	genppreclu 7883*	Pre-closure law for general operation on upper cuts. (Contributed by Jim Kingdon, 7-Nov-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( ( C e. ( 2nd ` A ) /\ D e. ( 2nd ` B ) ) -> ( C G D ) e. ( 2nd ` ( A F B ) ) ) )
Theorem	genipdm 7884*	Domain of general operation on positive reals. (Contributed by Jim Kingdon, 2-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- dom F = ( P. X. P. )
Theorem	genpml 7885*	The lower cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> E. q e. Q. q e. ( 1st ` ( A F B ) ) )
Theorem	genpmu 7886*	The upper cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> E. q e. Q. q e. ( 2nd ` ( A F B ) ) )
Theorem	genpcdl 7887*	Downward closure of an operation on positive reals. (Contributed by Jim Kingdon, 14-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( ( ( A e. P. /\ g e. ( 1st ` A ) ) /\ ( B e. P. /\ h e. ( 1st ` B ) ) ) /\ x e. Q. ) -> ( x <Q ( g G h ) -> x e. ( 1st ` ( A F B ) ) ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( f e. ( 1st ` ( A F B ) ) -> ( x <Q f -> x e. ( 1st ` ( A F B ) ) ) ) )
Theorem	genpcuu 7888*	Upward closure of an operation on positive reals. (Contributed by Jim Kingdon, 8-Nov-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( ( ( A e. P. /\ g e. ( 2nd ` A ) ) /\ ( B e. P. /\ h e. ( 2nd ` B ) ) ) /\ x e. Q. ) -> ( ( g G h ) <Q x -> x e. ( 2nd ` ( A F B ) ) ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( f e. ( 2nd ` ( A F B ) ) -> ( f <Q x -> x e. ( 2nd ` ( A F B ) ) ) ) )
Theorem	genprndl 7889*	The lower cut produced by addition or multiplication on positive reals is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x <Q y <-> ( z G x ) <Q ( z G y ) ) )   &    |- ( ( x e. Q. /\ y e. Q. ) -> ( x G y ) = ( y G x ) )   &    |- ( ( ( ( A e. P. /\ g e. ( 1st ` A ) ) /\ ( B e. P. /\ h e. ( 1st ` B ) ) ) /\ x e. Q. ) -> ( x <Q ( g G h ) -> x e. ( 1st ` ( A F B ) ) ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> A. q e. Q. ( q e. ( 1st ` ( A F B ) ) <-> E. r e. Q. ( q <Q r /\ r e. ( 1st ` ( A F B ) ) ) ) )
Theorem	genprndu 7890*	The upper cut produced by addition or multiplication on positive reals is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x <Q y <-> ( z G x ) <Q ( z G y ) ) )   &    |- ( ( x e. Q. /\ y e. Q. ) -> ( x G y ) = ( y G x ) )   &    |- ( ( ( ( A e. P. /\ g e. ( 2nd ` A ) ) /\ ( B e. P. /\ h e. ( 2nd ` B ) ) ) /\ x e. Q. ) -> ( ( g G h ) <Q x -> x e. ( 2nd ` ( A F B ) ) ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> A. r e. Q. ( r e. ( 2nd ` ( A F B ) ) <-> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` ( A F B ) ) ) ) )
Theorem	genpdisj 7891*	The lower and upper cuts produced by addition or multiplication on positive reals are disjoint. (Contributed by Jim Kingdon, 15-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x <Q y <-> ( z G x ) <Q ( z G y ) ) )   &    |- ( ( x e. Q. /\ y e. Q. ) -> ( x G y ) = ( y G x ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> A. q e. Q. -. ( q e. ( 1st ` ( A F B ) ) /\ q e. ( 2nd ` ( A F B ) ) ) )
Theorem	genpassl 7892*	Associativity of lower cuts. Lemma for genpassg 7894. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- dom F = ( P. X. P. )   &    |- ( ( f e. P. /\ g e. P. ) -> ( f F g ) e. P. )   &    |- ( ( f e. Q. /\ g e. Q. /\ h e. Q. ) -> ( ( f G g ) G h ) = ( f G ( g G h ) ) )   =>    |- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( 1st ` ( ( A F B ) F C ) ) = ( 1st ` ( A F ( B F C ) ) ) )
Theorem	genpassu 7893*	Associativity of upper cuts. Lemma for genpassg 7894. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- dom F = ( P. X. P. )   &    |- ( ( f e. P. /\ g e. P. ) -> ( f F g ) e. P. )   &    |- ( ( f e. Q. /\ g e. Q. /\ h e. Q. ) -> ( ( f G g ) G h ) = ( f G ( g G h ) ) )   =>    |- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( 2nd ` ( ( A F B ) F C ) ) = ( 2nd ` ( A F ( B F C ) ) ) )
Theorem	genpassg 7894*	Associativity of an operation on reals. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- dom F = ( P. X. P. )   &    |- ( ( f e. P. /\ g e. P. ) -> ( f F g ) e. P. )   &    |- ( ( f e. Q. /\ g e. Q. /\ h e. Q. ) -> ( ( f G g ) G h ) = ( f G ( g G h ) ) )   =>    |- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
Theorem	addnqprllem 7895	Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- ( ( ( <. L , U >. e. P. /\ G e. L ) /\ X e. Q. ) -> ( X <Q S -> ( ( X .Q ( *Q ` S ) ) .Q G ) e. L ) )
Theorem	addnqprulem 7896	Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- ( ( ( <. L , U >. e. P. /\ G e. U ) /\ X e. Q. ) -> ( S <Q X -> ( ( X .Q ( *Q ` S ) ) .Q G ) e. U ) )
Theorem	addnqprl 7897	Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- ( ( ( ( A e. P. /\ G e. ( 1st ` A ) ) /\ ( B e. P. /\ H e. ( 1st ` B ) ) ) /\ X e. Q. ) -> ( X <Q ( G +Q H ) -> X e. ( 1st ` ( A +P. B ) ) ) )
Theorem	addnqpru 7898	Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- ( ( ( ( A e. P. /\ G e. ( 2nd ` A ) ) /\ ( B e. P. /\ H e. ( 2nd ` B ) ) ) /\ X e. Q. ) -> ( ( G +Q H ) <Q X -> X e. ( 2nd ` ( A +P. B ) ) ) )
Theorem	addlocprlemlt 7899	Lemma for addlocpr 7904. The Q <Q ( D +Q E ) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
|- ( ph -> A e. P. )   &    |- ( ph -> B e. P. )   &    |- ( ph -> Q <Q R )   &    |- ( ph -> P e. Q. )   &    |- ( ph -> ( Q +Q ( P +Q P ) ) = R )   &    |- ( ph -> D e. ( 1st ` A ) )   &    |- ( ph -> U e. ( 2nd ` A ) )   &    |- ( ph -> U <Q ( D +Q P ) )   &    |- ( ph -> E e. ( 1st ` B ) )   &    |- ( ph -> T e. ( 2nd ` B ) )   &    |- ( ph -> T <Q ( E +Q P ) )   =>    |- ( ph -> ( Q <Q ( D +Q E ) -> Q e. ( 1st ` ( A +P. B ) ) ) )
Theorem	addlocprlemeqgt 7900	Lemma for addlocpr 7904. This is a step used in both the Q = ( D +Q E ) and ( D +Q E ) <Q Q cases. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- ( ph -> A e. P. )   &    |- ( ph -> B e. P. )   &    |- ( ph -> Q <Q R )   &    |- ( ph -> P e. Q. )   &    |- ( ph -> ( Q +Q ( P +Q P ) ) = R )   &    |- ( ph -> D e. ( 1st ` A ) )   &    |- ( ph -> U e. ( 2nd ` A ) )   &    |- ( ph -> U <Q ( D +Q P ) )   &    |- ( ph -> E e. ( 1st ` B ) )   &    |- ( ph -> T e. ( 2nd ` B ) )   &    |- ( ph -> T <Q ( E +Q P ) )   =>    |- ( ph -> ( U +Q T ) <Q ( ( D +Q E ) +Q ( P +Q P ) ) )