P. 76 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7501-7600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	caucvgprprlemupu 7501*	Lemma for caucvgprpr 7513. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 21-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   =>    |- ( ( ph /\ s <Q t /\ s e. ( 2nd ` L ) ) -> t e. ( 2nd ` L ) )
Theorem	caucvgprprlemrnd 7502*	Lemma for caucvgprpr 7513. The putative limit is rounded. (Contributed by Jim Kingdon, 21-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   =>    |- ( ph -> ( A. s e. Q. ( s e. ( 1st ` L ) <-> E. t e. Q. ( s <Q t /\ t e. ( 1st ` L ) ) ) /\ A. t e. Q. ( t e. ( 2nd ` L ) <-> E. s e. Q. ( s <Q t /\ s e. ( 2nd ` L ) ) ) ) )
Theorem	caucvgprprlemdisj 7503*	Lemma for caucvgprpr 7513. The putative limit is disjoint. (Contributed by Jim Kingdon, 21-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   =>    |- ( ph -> A. s e. Q. -. ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) )
Theorem	caucvgprprlemloc 7504*	Lemma for caucvgprpr 7513. The putative limit is located. (Contributed by Jim Kingdon, 21-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   =>    |- ( ph -> A. s e. Q. A. t e. Q. ( s <Q t -> ( s e. ( 1st ` L ) \/ t e. ( 2nd ` L ) ) ) )
Theorem	caucvgprprlemcl 7505*	Lemma for caucvgprpr 7513. The putative limit is a positive real. (Contributed by Jim Kingdon, 21-Nov-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   =>    |- ( ph -> L e. P. )
Theorem	caucvgprprlemclphr 7506*	Lemma for caucvgprpr 7513. The putative limit is a positive real. Like caucvgprprlemcl 7505 but without a distinct variable constraint between ph and r. (Contributed by Jim Kingdon, 19-Jun-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   =>    |- ( ph -> L e. P. )
Theorem	caucvgprprlemexbt 7507*	Lemma for caucvgprpr 7513. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 16-Jun-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   &    |- ( ph -> Q e. Q. )   &    |- ( ph -> T e. P. )   &    |- ( ph -> ( L +P. <. { p | p <Q Q } , { q | Q <Q q } >. ) <P T )   =>    |- ( ph -> E. b e. N. ( ( ( F ` b ) +P. <. { p | p <Q ( *Q ` [ <. b , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. b , 1o >. ] ~Q ) <Q q } >. ) +P. <. { p | p <Q Q } , { q | Q <Q q } >. ) <P T )
Theorem	caucvgprprlemexb 7508*	Lemma for caucvgprpr 7513. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 15-Jun-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   &    |- ( ph -> Q e. P. )   &    |- ( ph -> R e. N. )   =>    |- ( ph -> ( ( ( L +P. Q ) +P. <. { p | p <Q ( *Q ` [ <. R , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. R , 1o >. ] ~Q ) <Q q } >. ) <P ( ( F ` R ) +P. Q ) -> E. b e. N. ( ( ( F ` b ) +P. <. { p | p <Q ( *Q ` [ <. b , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. b , 1o >. ] ~Q ) <Q q } >. ) +P. ( Q +P. <. { p | p <Q ( *Q ` [ <. R , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. R , 1o >. ] ~Q ) <Q q } >. ) ) <P ( ( F ` R ) +P. Q ) ) )
Theorem	caucvgprprlemaddq 7509*	Lemma for caucvgprpr 7513. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 5-Jun-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   &    |- ( ph -> X e. P. )   &    |- ( ph -> Q e. P. )   &    |- ( ph -> E. r e. N. ( X +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P ( ( F ` r ) +P. Q ) )   =>    |- ( ph -> X <P ( L +P. Q ) )
Theorem	caucvgprprlem1 7510*	Lemma for caucvgprpr 7513. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   &    |- ( ph -> Q e. P. )   &    |- ( ph -> J <N K )   &    |- ( ph -> <. { l | l <Q ( *Q ` [ <. J , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. J , 1o >. ] ~Q ) <Q u } >. <P Q )   =>    |- ( ph -> ( F ` K ) <P ( L +P. Q ) )
Theorem	caucvgprprlem2 7511*	Lemma for caucvgprpr 7513. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   &    |- ( ph -> Q e. P. )   &    |- ( ph -> J <N K )   &    |- ( ph -> <. { l | l <Q ( *Q ` [ <. J , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. J , 1o >. ] ~Q ) <Q u } >. <P Q )   =>    |- ( ph -> L <P ( ( F ` K ) +P. Q ) )
Theorem	caucvgprprlemlim 7512*	Lemma for caucvgprpr 7513. The putative limit is a limit. (Contributed by Jim Kingdon, 21-Nov-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   =>    |- ( ph -> A. x e. P. E. j e. N. A. k e. N. ( j <N k -> ( ( F ` k ) <P ( L +P. x ) /\ L <P ( ( F ` k ) +P. x ) ) ) )
Theorem	caucvgprpr 7513*	A Cauchy sequence of positive reals with a modulus of convergence converges to a positive real. This is basically Corollary 11.2.13 of [HoTT], p. (varies) (one key difference being that this is for positive reals rather than signed reals). Also, 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). We also specify that every term needs to be larger than a given value A, to avoid the case where we have positive terms which "converge" to zero (which is not a positive real). This is similar to caucvgpr 7483 except that values of the sequence are positive reals rather than positive fractions. Reading that proof first (or cauappcvgpr 7463) might help in understanding this one, as they are slightly simpler but similarly structured. (Contributed by Jim Kingdon, 14-Nov-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   =>    |- ( ph -> E. y e. P. A. x e. P. E. j e. N. A. k e. N. ( j <N k -> ( ( F ` k ) <P ( y +P. x ) /\ y <P ( ( F ` k ) +P. x ) ) ) )
Theorem	suplocexprlemell 7514*	Lemma for suplocexpr 7526. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- ( B e. U. ( 1st " A ) <-> E. x e. A B e. ( 1st ` x ) )
Theorem	suplocexprlem2b 7515	Lemma for suplocexpr 7526. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( A C_ P. -> ( 2nd ` B ) = { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } )
Theorem	suplocexprlemss 7516*	Lemma for suplocexpr 7526. A is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   =>    |- ( ph -> A C_ P. )
Theorem	suplocexprlemml 7517*	Lemma for suplocexpr 7526. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   =>    |- ( ph -> E. s e. Q. s e. U. ( 1st " A ) )
Theorem	suplocexprlemrl 7518*	Lemma for suplocexpr 7526. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   =>    |- ( ph -> A. q e. Q. ( q e. U. ( 1st " A ) <-> E. r e. Q. ( q <Q r /\ r e. U. ( 1st " A ) ) ) )
Theorem	suplocexprlemmu 7519*	Lemma for suplocexpr 7526. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> E. s e. Q. s e. ( 2nd ` B ) )
Theorem	suplocexprlemru 7520*	Lemma for suplocexpr 7526. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> A. r e. Q. ( r e. ( 2nd ` B ) <-> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` B ) ) ) )
Theorem	suplocexprlemdisj 7521*	Lemma for suplocexpr 7526. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> A. q e. Q. -. ( q e. U. ( 1st " A ) /\ q e. ( 2nd ` B ) ) )
Theorem	suplocexprlemloc 7522*	Lemma for suplocexpr 7526. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. U. ( 1st " A ) \/ r e. ( 2nd ` B ) ) ) )
Theorem	suplocexprlemex 7523*	Lemma for suplocexpr 7526. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> B e. P. )
Theorem	suplocexprlemub 7524*	Lemma for suplocexpr 7526. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> A. y e. A -. B <P y )
Theorem	suplocexprlemlub 7525*	Lemma for suplocexpr 7526. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> ( y <P B -> E. z e. A y <P z ) )
Theorem	suplocexpr 7526*	An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   =>    |- ( ph -> E. x e. P. ( A. y e. A -. x <P y /\ A. y e. P. ( y <P x -> E. z e. A y <P z ) ) )
Definition	df-enr 7527*	Define equivalence relation for signed reals. 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-4.1 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.)
|- ~R = { <. x , y >. | ( ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) ) ) }
Definition	df-nr 7528	Define class of signed reals. 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-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.)
|- R. = ( ( P. X. P. ) /. ~R )
Definition	df-plr 7529*	Define addition on signed reals. 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-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.)
|- +R = { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R ) ) }
Definition	df-mr 7530*	Define multiplication on signed reals. 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-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.)
|- .R = { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R ) ) }
Definition	df-ltr 7531*	Define ordering relation on signed reals. 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-4.4 of [Gleason] p. 127. (Contributed by NM, 14-Feb-1996.)
|- <R = { <. x , y >. | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) ) ) }
Definition	df-0r 7532	Define signed real constant 0. 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-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.)
|- 0R = [ <. 1P , 1P >. ] ~R
Definition	df-1r 7533	Define signed 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. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.)
|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
Definition	df-m1r 7534	Define signed 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 NM, 9-Aug-1995.)
|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
Theorem	enrbreq 7535	Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.)
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( <. A , B >. ~R <. C , D >. <-> ( A +P. D ) = ( B +P. C ) ) )
Theorem	enrer 7536	The equivalence relation for signed reals is an equivalence relation. Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
|- ~R Er ( P. X. P. )
Theorem	enreceq 7537	Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.)
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R = [ <. C , D >. ] ~R <-> ( A +P. D ) = ( B +P. C ) ) )
Theorem	enrex 7538	The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.)
|- ~R e. _V
Theorem	ltrelsr 7539	Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.)
|- <R C_ ( R. X. R. )
Theorem	addcmpblnr 7540	Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995.)
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> <. ( A +P. F ) , ( B +P. G ) >. ~R <. ( C +P. R ) , ( D +P. S ) >. ) )
Theorem	mulcmpblnrlemg 7541	Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.)
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( D .P. F ) +P. ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) ) )
Theorem	mulcmpblnr 7542	Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.)
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> <. ( ( A .P. F ) +P. ( B .P. G ) ) , ( ( A .P. G ) +P. ( B .P. F ) ) >. ~R <. ( ( C .P. R ) +P. ( D .P. S ) ) , ( ( C .P. S ) +P. ( D .P. R ) ) >. ) )
Theorem	prsrlem1 7543*	Decomposing signed reals into positive reals. Lemma for addsrpr 7546 and mulsrpr 7547. (Contributed by Jim Kingdon, 30-Dec-2019.)
|- ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) ) ) -> ( ( ( ( w e. P. /\ v e. P. ) /\ ( s e. P. /\ f e. P. ) ) /\ ( ( u e. P. /\ t e. P. ) /\ ( g e. P. /\ h e. P. ) ) ) /\ ( ( w +P. f ) = ( v +P. s ) /\ ( u +P. h ) = ( t +P. g ) ) ) )
Theorem	addsrmo 7544*	There is at most one result from adding 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 ) , ( v +P. t ) >. ] ~R ) )
Theorem	mulsrmo 7545*	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 7546	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 7547	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 7548	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 7549	Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.)
|- ( 0R <R [ <. A , B >. ] ~R <-> B <P A )
Theorem	0nsr 7550	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 7551	The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.)
|- 0R e. R.
Theorem	1sr 7552	The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.)
|- 1R e. R.
Theorem	m1r 7553	The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.)
|- -1R e. R.
Theorem	addclsr 7554	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 7555	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 7556	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 7557	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 7558	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 7559	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 7560	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 7561	Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996.)
|- ( -1R +R 1R ) = 0R
Theorem	m1m1sr 7562	Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.)
|- ( -1R .R -1R ) = 1R
Theorem	lttrsr 7563*	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 7564	Signed real 'less than' is a partial order. (Contributed by Jim Kingdon, 4-Jan-2019.)
|- <R Po R.
Theorem	ltsosr 7565	Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.)
|- <R Or R.
Theorem	0lt1sr 7566	0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.)
|- 0R <R 1R
Theorem	1ne0sr 7567	1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.)
|- -. 1R = 0R
Theorem	0idsr 7568	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 7569	1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.)
|- ( A e. R. -> ( A .R 1R ) = A )
Theorem	00sr 7570	A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.)
|- ( A e. R. -> ( A .R 0R ) = 0R )
Theorem	ltasrg 7571	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 7572	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 7573*	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 7574*	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 7575*	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 7576	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 7577	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 7578	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 7579	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 7580	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 7581	Lemma for mulextsr1 7582. (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 7582	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 7583*	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 7584*	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 7585	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 7586	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 7587	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 7588	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 7589*	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 7590*	Lemma for caucvgsr 7603. Terms of the sequence from caucvgsrlemgt1 7596 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 7591*	Lemma for caucvgsr 7603. 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 7592*	Lemma for caucvgsr 7603. 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 7593*	Lemma for caucvgsr 7603. 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 7594*	Lemma for caucvgsr 7603. 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 7595*	Lemma for caucvgsr 7603. 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 7596*	Lemma for caucvgsr 7603. 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 7597*	Lemma for caucvgsr 7603. 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 7598*	Lemma for caucvgsr 7603. 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 7599*	Lemma for caucvgsr 7603. 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 7600*	Lemma for caucvgsr 7603. 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 ) )