P. 82 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8101-8200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mulsrmo 8101*	There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
|- ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. t ) ) , ( ( w .P. t ) +P. ( v .P. u ) ) >. ] ~R ) )
Theorem	addsrpr 8102	Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R +R [ <. C , D >. ] ~R ) = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R )
Theorem	mulsrpr 8103	Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R .R [ <. C , D >. ] ~R ) = [ <. ( ( A .P. C ) +P. ( B .P. D ) ) , ( ( A .P. D ) +P. ( B .P. C ) ) >. ] ~R )
Theorem	ltsrprg 8104	Ordering of signed reals in terms of positive reals. (Contributed by Jim Kingdon, 2-Jan-2019.)
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R <R [ <. C , D >. ] ~R <-> ( A +P. D ) <P ( B +P. C ) ) )
Theorem	gt0srpr 8105	Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.)
|- ( 0R <R [ <. A , B >. ] ~R <-> B <P A )
Theorem	0nsr 8106	The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.)
|- -. (/) e. R.
Theorem	0r 8107	The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.)
|- 0R e. R.
Theorem	1sr 8108	The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.)
|- 1R e. R.
Theorem	m1r 8109	The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.)
|- -1R e. R.
Theorem	addclsr 8110	Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.)
|- ( ( A e. R. /\ B e. R. ) -> ( A +R B ) e. R. )
Theorem	mulclsr 8111	Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.)
|- ( ( A e. R. /\ B e. R. ) -> ( A .R B ) e. R. )
Theorem	addcomsrg 8112	Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ( ( A e. R. /\ B e. R. ) -> ( A +R B ) = ( B +R A ) )
Theorem	addasssrg 8113	Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( ( A +R B ) +R C ) = ( A +R ( B +R C ) ) )
Theorem	mulcomsrg 8114	Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ( ( A e. R. /\ B e. R. ) -> ( A .R B ) = ( B .R A ) )
Theorem	mulasssrg 8115	Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.)
|- ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( ( A .R B ) .R C ) = ( A .R ( B .R C ) ) )
Theorem	distrsrg 8116	Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.)
|- ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( A .R ( B +R C ) ) = ( ( A .R B ) +R ( A .R C ) ) )
Theorem	m1p1sr 8117	Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996.)
|- ( -1R +R 1R ) = 0R
Theorem	m1m1sr 8118	Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.)
|- ( -1R .R -1R ) = 1R
Theorem	lttrsr 8119*	Signed real 'less than' is a transitive relation. (Contributed by Jim Kingdon, 4-Jan-2019.)
|- ( ( f e. R. /\ g e. R. /\ h e. R. ) -> ( ( f <R g /\ g <R h ) -> f <R h ) )
Theorem	ltposr 8120	Signed real 'less than' is a partial order. (Contributed by Jim Kingdon, 4-Jan-2019.)
|- <R Po R.
Theorem	ltsosr 8121	Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.)
|- <R Or R.
Theorem	0lt1sr 8122	0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.)
|- 0R <R 1R
Theorem	1ne0sr 8123	1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.)
|- -. 1R = 0R
Theorem	0idsr 8124	The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996.)
|- ( A e. R. -> ( A +R 0R ) = A )
Theorem	1idsr 8125	1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
|- ( A e. R. -> ( A .R 1R ) = A )
Theorem	00sr 8126	A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.)
|- ( A e. R. -> ( A .R 0R ) = 0R )
Theorem	ltasrg 8127	Ordering property of addition. (Contributed by NM, 10-May-1996.)
|- ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) )
Theorem	pn0sr 8128	A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.)
|- ( A e. R. -> ( A +R ( A .R -1R ) ) = 0R )
Theorem	negexsr 8129*	Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.)
|- ( A e. R. -> E. x e. R. ( A +R x ) = 0R )
Theorem	recexgt0sr 8130*	The reciprocal of a positive signed real exists and is positive. (Contributed by Jim Kingdon, 6-Feb-2020.)
|- ( 0R <R A -> E. x e. R. ( 0R <R x /\ ( A .R x ) = 1R ) )
Theorem	recexsrlem 8131*	The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.)
|- ( 0R <R A -> E. x e. R. ( A .R x ) = 1R )
Theorem	addgt0sr 8132	The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.)
|- ( ( 0R <R A /\ 0R <R B ) -> 0R <R ( A +R B ) )
Theorem	ltadd1sr 8133	Adding one to a signed real yields a larger signed real. (Contributed by Jim Kingdon, 7-Jul-2021.)
|- ( A e. R. -> A <R ( A +R 1R ) )
Theorem	ltm1sr 8134	Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.)
|- ( A e. R. -> ( A +R -1R ) <R A )
Theorem	mulgt0sr 8135	The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.)
|- ( ( 0R <R A /\ 0R <R B ) -> 0R <R ( A .R B ) )
Theorem	aptisr 8136	Apartness of signed reals is tight. (Contributed by Jim Kingdon, 29-Jan-2020.)
|- ( ( A e. R. /\ B e. R. /\ -. ( A <R B \/ B <R A ) ) -> A = B )
Theorem	mulextsr1lem 8137	Lemma for mulextsr1 8138. (Contributed by Jim Kingdon, 17-Feb-2020.)
|- ( ( ( X e. P. /\ Y e. P. ) /\ ( Z e. P. /\ W e. P. ) /\ ( U e. P. /\ V e. P. ) ) -> ( ( ( ( X .P. U ) +P. ( Y .P. V ) ) +P. ( ( Z .P. V ) +P. ( W .P. U ) ) ) <P ( ( ( X .P. V ) +P. ( Y .P. U ) ) +P. ( ( Z .P. U ) +P. ( W .P. V ) ) ) -> ( ( X +P. W ) <P ( Y +P. Z ) \/ ( Z +P. Y ) <P ( W +P. X ) ) ) )
Theorem	mulextsr1 8138	Strong extensionality of multiplication of signed reals. (Contributed by Jim Kingdon, 18-Feb-2020.)
|- ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( ( A .R C ) <R ( B .R C ) -> ( A <R B \/ B <R A ) ) )
Theorem	archsr 8139*	For any signed real, there is an integer that is greater than it. This is also known as the "archimedean property". The expression [ <. ( <. { l | l <Q [ <. x , 1o >. ] ~Q }, { u | [ <. x , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R is the embedding of the positive integer x into the signed reals. (Contributed by Jim Kingdon, 23-Apr-2020.)
|- ( A e. R. -> E. x e. N. A <R [ <. ( <. { l | l <Q [ <. x , 1o >. ] ~Q } , { u | [ <. x , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R )
Theorem	srpospr 8140*	Mapping from a signed real greater than zero to a positive real. (Contributed by Jim Kingdon, 25-Jun-2021.)
|- ( ( A e. R. /\ 0R <R A ) -> E! x e. P. [ <. ( x +P. 1P ) , 1P >. ] ~R = A )
Theorem	prsrcl 8141	Mapping from a positive real to a signed real. (Contributed by Jim Kingdon, 25-Jun-2021.)
|- ( A e. P. -> [ <. ( A +P. 1P ) , 1P >. ] ~R e. R. )
Theorem	prsrpos 8142	Mapping from a positive real to a signed real yields a result greater than zero. (Contributed by Jim Kingdon, 25-Jun-2021.)
|- ( A e. P. -> 0R <R [ <. ( A +P. 1P ) , 1P >. ] ~R )
Theorem	prsradd 8143	Mapping from positive real addition to signed real addition. (Contributed by Jim Kingdon, 29-Jun-2021.)
|- ( ( A e. P. /\ B e. P. ) -> [ <. ( ( A +P. B ) +P. 1P ) , 1P >. ] ~R = ( [ <. ( A +P. 1P ) , 1P >. ] ~R +R [ <. ( B +P. 1P ) , 1P >. ] ~R ) )
Theorem	prsrlt 8144	Mapping from positive real ordering to signed real ordering. (Contributed by Jim Kingdon, 29-Jun-2021.)
|- ( ( A e. P. /\ B e. P. ) -> ( A <P B <-> [ <. ( A +P. 1P ) , 1P >. ] ~R <R [ <. ( B +P. 1P ) , 1P >. ] ~R ) )
Theorem	prsrriota 8145*	Mapping a restricted iota from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.)
|- ( ( A e. R. /\ 0R <R A ) -> [ <. ( ( iota_ x e. P. [ <. ( x +P. 1P ) , 1P >. ] ~R = A ) +P. 1P ) , 1P >. ] ~R = A )
Theorem	caucvgsrlemcl 8146*	Lemma for caucvgsr 8159. Terms of the sequence from caucvgsrlemgt1 8152 can be mapped to positive reals. (Contributed by Jim Kingdon, 2-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   =>    |- ( ( ph /\ A e. N. ) -> ( iota_ y e. P. ( F ` A ) = [ <. ( y +P. 1P ) , 1P >. ] ~R ) e. P. )
Theorem	caucvgsrlemasr 8147*	Lemma for caucvgsr 8159. The lower bound is a signed real. (Contributed by Jim Kingdon, 4-Jul-2021.)
|- ( ph -> A. m e. N. A <R ( F ` m ) )   =>    |- ( ph -> A e. R. )
Theorem	caucvgsrlemfv 8148*	Lemma for caucvgsr 8159. Coercing sequence value from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   &    |- G = ( x e. N. |-> ( iota_ y e. P. ( F ` x ) = [ <. ( y +P. 1P ) , 1P >. ] ~R ) )   =>    |- ( ( ph /\ A e. N. ) -> [ <. ( ( G ` A ) +P. 1P ) , 1P >. ] ~R = ( F ` A ) )
Theorem	caucvgsrlemf 8149*	Lemma for caucvgsr 8159. Defining the sequence in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   &    |- G = ( x e. N. |-> ( iota_ y e. P. ( F ` x ) = [ <. ( y +P. 1P ) , 1P >. ] ~R ) )   =>    |- ( ph -> G : N. --> P. )
Theorem	caucvgsrlemcau 8150*	Lemma for caucvgsr 8159. Defining the Cauchy condition in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   &    |- G = ( x e. N. |-> ( iota_ y e. P. ( F ` x ) = [ <. ( y +P. 1P ) , 1P >. ] ~R ) )   =>    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( G ` n ) <P ( ( G ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( G ` k ) <P ( ( G ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )
Theorem	caucvgsrlembound 8151*	Lemma for caucvgsr 8159. Defining the boundedness condition in terms of positive reals. (Contributed by Jim Kingdon, 25-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   &    |- G = ( x e. N. |-> ( iota_ y e. P. ( F ` x ) = [ <. ( y +P. 1P ) , 1P >. ] ~R ) )   =>    |- ( ph -> A. m e. N. 1P <P ( G ` m ) )
Theorem	caucvgsrlemgt1 8152*	Lemma for caucvgsr 8159. A Cauchy sequence whose terms are greater than one converges. (Contributed by Jim Kingdon, 22-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   =>    |- ( ph -> E. y e. R. A. x e. R. ( 0R <R x -> E. j e. N. A. i e. N. ( j <N i -> ( ( F ` i ) <R ( y +R x ) /\ y <R ( ( F ` i ) +R x ) ) ) ) )
Theorem	caucvgsrlemoffval 8153*	Lemma for caucvgsr 8159. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   &    |- G = ( a e. N. |-> ( ( ( F ` a ) +R 1R ) +R ( A .R -1R ) ) )   =>    |- ( ( ph /\ J e. N. ) -> ( ( G ` J ) +R A ) = ( ( F ` J ) +R 1R ) )
Theorem	caucvgsrlemofff 8154*	Lemma for caucvgsr 8159. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   &    |- G = ( a e. N. |-> ( ( ( F ` a ) +R 1R ) +R ( A .R -1R ) ) )   =>    |- ( ph -> G : N. --> R. )
Theorem	caucvgsrlemoffcau 8155*	Lemma for caucvgsr 8159. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   &    |- G = ( a e. N. |-> ( ( ( F ` a ) +R 1R ) +R ( A .R -1R ) ) )   =>    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( G ` n ) <R ( ( G ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( G ` k ) <R ( ( G ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )
Theorem	caucvgsrlemoffgt1 8156*	Lemma for caucvgsr 8159. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   &    |- G = ( a e. N. |-> ( ( ( F ` a ) +R 1R ) +R ( A .R -1R ) ) )   =>    |- ( ph -> A. m e. N. 1R <R ( G ` m ) )
Theorem	caucvgsrlemoffres 8157*	Lemma for caucvgsr 8159. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   &    |- G = ( a e. N. |-> ( ( ( F ` a ) +R 1R ) +R ( A .R -1R ) ) )   =>    |- ( ph -> E. y e. R. A. x e. R. ( 0R <R x -> E. j e. N. A. k e. N. ( j <N k -> ( ( F ` k ) <R ( y +R x ) /\ y <R ( ( F ` k ) +R x ) ) ) ) )
Theorem	caucvgsrlembnd 8158*	Lemma for caucvgsr 8159. A Cauchy sequence with a lower bound converges. (Contributed by Jim Kingdon, 19-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   =>    |- ( ph -> E. y e. R. A. x e. R. ( 0R <R x -> E. j e. N. A. k e. N. ( j <N k -> ( ( F ` k ) <R ( y +R x ) /\ y <R ( ( F ` k ) +R x ) ) ) ) )
Theorem	caucvgsr 8159*	A Cauchy sequence of signed reals with a modulus of convergence converges to a signed real. This is basically Corollary 11.2.13 of [HoTT], p. (varies). The HoTT book theorem has a modulus of convergence (that is, a rate of convergence) specified by (11.2.9) in HoTT whereas this theorem fixes the rate of convergence to say that all terms after the nth term must be within 1 / n of the nth term (it should later be able to prove versions of this theorem with a different fixed rate or a modulus of convergence supplied as a hypothesis). This is similar to caucvgprpr 8069 but is for signed reals rather than positive reals. Here is an outline of how we prove it: 1. Choose a lower bound for the sequence (see caucvgsrlembnd 8158). 2. Offset each element of the sequence so that each element of the resulting sequence is greater than one (greater than zero would not suffice, because the limit as well as the elements of the sequence need to be positive) (see caucvgsrlemofff 8154). 3. Since a signed real (element of R.) which is greater than zero can be mapped to a positive real (element of P.), perform that mapping on each element of the sequence and invoke caucvgprpr 8069 to get a limit (see caucvgsrlemgt1 8152). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 8152). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 8157). (Contributed by Jim Kingdon, 20-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   =>    |- ( ph -> E. y e. R. A. x e. R. ( 0R <R x -> E. j e. N. A. k e. N. ( j <N k -> ( ( F ` k ) <R ( y +R x ) /\ y <R ( ( F ` k ) +R x ) ) ) ) )
Theorem	ltpsrprg 8160	Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
|- ( ( A e. P. /\ B e. P. /\ C e. R. ) -> ( ( C +R [ <. A , 1P >. ] ~R ) <R ( C +R [ <. B , 1P >. ] ~R ) <-> A <P B ) )
Theorem	mappsrprg 8161	Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
|- ( ( A e. P. /\ C e. R. ) -> ( C +R -1R ) <R ( C +R [ <. A , 1P >. ] ~R ) )
Theorem	map2psrprg 8162*	Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
|- ( C e. R. -> ( ( C +R -1R ) <R A <-> E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A ) )
Theorem	suplocsrlemb 8163*	Lemma for suplocsr 8166. The set B is located. (Contributed by Jim Kingdon, 18-Jan-2024.)
|- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }   &    |- ( ph -> A C_ R. )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> A. u e. P. A. v e. P. ( u <P v -> ( E. q e. B u <P q \/ A. q e. B q <P v ) ) )
Theorem	suplocsrlempr 8164*	Lemma for suplocsr 8166. The set B has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.)
|- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }   &    |- ( ph -> A C_ R. )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> E. v e. P. ( A. w e. B -. v <P w /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) )
Theorem	suplocsrlem 8165*	Lemma for suplocsr 8166. The set A has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.)
|- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }   &    |- ( ph -> A C_ R. )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) )
Theorem	suplocsr 8166*	An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) )
Syntax	cc 8167	Class of complex numbers.
class CC
Syntax	cr 8168	Class of real numbers.
class RR
Syntax	cc0 8169	Extend class notation to include the complex number 0.
class 0
Syntax	c1 8170	Extend class notation to include the complex number 1.
class 1
Syntax	ci 8171	Extend class notation to include the complex number i.
class _i
Syntax	caddc 8172	Addition on complex numbers.
class +
Syntax	cltrr 8173	'Less than' predicate (defined over real subset of complex numbers).
class <RR
Syntax	cmul 8174	Multiplication on complex numbers. The token x. is a center dot.
class x.
Definition	df-c 8175	Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- CC = ( R. X. R. )
Definition	df-0 8176	Define the complex number 0. (Contributed by NM, 22-Feb-1996.)
|- 0 = <. 0R , 0R >.
Definition	df-1 8177	Define the complex number 1. (Contributed by NM, 22-Feb-1996.)
|- 1 = <. 1R , 0R >.
Definition	df-i 8178	Define the complex number _i (the imaginary unit). (Contributed by NM, 22-Feb-1996.)
|- _i = <. 0R , 1R >.
Definition	df-r 8179	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.)
|- RR = ( R. X. { 0R } )
Definition	df-add 8180*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.)
|- + = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) }
Definition	df-mul 8181*	Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.)
|- x. = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) }
Definition	df-lt 8182*	Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
Theorem	opelcn 8183	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.)
|- ( <. A , B >. e. CC <-> ( A e. R. /\ B e. R. ) )
Theorem	opelreal 8184	Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- ( <. A , 0R >. e. RR <-> A e. R. )
Theorem	elreal 8185*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.)
|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A )
Theorem	elrealeu 8186*	The real number mapping in elreal 8185 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.)
|- ( A e. RR <-> E! x e. R. <. x , 0R >. = A )
Theorem	elreal2 8187	Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.)
|- ( A e. RR <-> ( ( 1st ` A ) e. R. /\ A = <. ( 1st ` A ) , 0R >. ) )
Theorem	0ncn 8188	The empty set is not a complex number. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. See also cnm 8189 which is a related property. (Contributed by NM, 2-May-1996.)
|- -. (/) e. CC
Theorem	cnm 8189*	A complex number is an inhabited set. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by Jim Kingdon, 23-Oct-2023.) (New usage is discouraged.)
|- ( A e. CC -> E. x x e. A )
Theorem	ltrelre 8190	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.)
|- <RR C_ ( RR X. RR )
Theorem	addcnsr 8191	Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.)
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( <. A , B >. + <. C , D >. ) = <. ( A +R C ) , ( B +R D ) >. )
Theorem	mulcnsr 8192	Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.)
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( <. A , B >. x. <. C , D >. ) = <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. )
Theorem	eqresr 8193	Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
|- A e. _V   =>    |- ( <. A , 0R >. = <. B , 0R >. <-> A = B )
Theorem	addresr 8194	Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , 0R >. )
Theorem	mulresr 8195	Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. x. <. B , 0R >. ) = <. ( A .R B ) , 0R >. )
Theorem	ltresr 8196	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
|- ( <. A , 0R >. <RR <. B , 0R >. <-> A <R B )
Theorem	ltresr2 8197	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <RR B <-> ( 1st ` A ) <R ( 1st ` B ) ) )
Theorem	dfcnqs 8198	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in CC from those in R.. The trick involves qsid 6864, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that CC is a quotient set, even though it is not (compare df-c 8175), and allows us to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995.)
|- CC = ( ( R. X. R. ) /. `' _E )
Theorem	addcnsrec 8199	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 8198 and mulcnsrec 8200. (Contributed by NM, 13-Aug-1995.)
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( [ <. A , B >. ] `' _E + [ <. C , D >. ] `' _E ) = [ <. ( A +R C ) , ( B +R D ) >. ] `' _E )
Theorem	mulcnsrec 8200	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6863, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 8198. (Contributed by NM, 13-Aug-1995.)
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( [ <. A , B >. ] `' _E x. [ <. C , D >. ] `' _E ) = [ <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. ] `' _E )