P. 77 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7601-7700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	00sr 7601	A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.)
|- ( A e. R. -> ( A .R 0R ) = 0R )
Theorem	ltasrg 7602	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 7603	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 7604*	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 7605*	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 7606*	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 7607	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 7608	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 7609	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 7610	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 7611	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 7612	Lemma for mulextsr1 7613. (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 7613	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 7614*	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 7615*	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 7616	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 7617	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 7618	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 7619	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 7620*	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 7621*	Lemma for caucvgsr 7634. Terms of the sequence from caucvgsrlemgt1 7627 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 7622*	Lemma for caucvgsr 7634. 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 7623*	Lemma for caucvgsr 7634. 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 7624*	Lemma for caucvgsr 7634. 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 7625*	Lemma for caucvgsr 7634. 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 7626*	Lemma for caucvgsr 7634. 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 7627*	Lemma for caucvgsr 7634. 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 7628*	Lemma for caucvgsr 7634. 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 7629*	Lemma for caucvgsr 7634. 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 7630*	Lemma for caucvgsr 7634. 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 7631*	Lemma for caucvgsr 7634. 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 7632*	Lemma for caucvgsr 7634. 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 7633*	Lemma for caucvgsr 7634. 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 7634*	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 7544 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 7633). 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 7629). 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 7544 to get a limit (see caucvgsrlemgt1 7627). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 7627). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7632). (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 7635	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 7636	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 7637*	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 7638*	Lemma for suplocsr 7641. 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 7639*	Lemma for suplocsr 7641. 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 7640*	Lemma for suplocsr 7641. 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 7641*	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 7642	Class of complex numbers.
class CC
Syntax	cr 7643	Class of real numbers.
class RR
Syntax	cc0 7644	Extend class notation to include the complex number 0.
class 0
Syntax	c1 7645	Extend class notation to include the complex number 1.
class 1
Syntax	ci 7646	Extend class notation to include the complex number i.
class _i
Syntax	caddc 7647	Addition on complex numbers.
class +
Syntax	cltrr 7648	'Less than' predicate (defined over real subset of complex numbers).
class <RR
Syntax	cmul 7649	Multiplication on complex numbers. The token x. is a center dot.
class x.
Definition	df-c 7650	Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- CC = ( R. X. R. )
Definition	df-0 7651	Define the complex number 0. (Contributed by NM, 22-Feb-1996.)
|- 0 = <. 0R , 0R >.
Definition	df-1 7652	Define the complex number 1. (Contributed by NM, 22-Feb-1996.)
|- 1 = <. 1R , 0R >.
Definition	df-i 7653	Define the complex number _i (the imaginary unit). (Contributed by NM, 22-Feb-1996.)
|- _i = <. 0R , 1R >.
Definition	df-r 7654	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.)
|- RR = ( R. X. { 0R } )
Definition	df-add 7655*	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 7656*	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 7657*	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 7658	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 7659	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 7660*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.)
|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A )
Theorem	elrealeu 7661*	The real number mapping in elreal 7660 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.)
|- ( A e. RR <-> E! x e. R. <. x , 0R >. = A )
Theorem	elreal2 7662	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 7663	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 7664 which is a related property. (Contributed by NM, 2-May-1996.)
|- -. (/) e. CC
Theorem	cnm 7664*	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 7665	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.)
|- <RR C_ ( RR X. RR )
Theorem	addcnsr 7666	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 7667	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 7668	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 7669	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 7670	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 7671	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 7672	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 7673	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in CC from those in R.. The trick involves qsid 6502, 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 7650), 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 7674	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7673 and mulcnsrec 7675. (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 7675	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6501, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7673. (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 )
Theorem	addvalex 7676	Existence of a sum. This is dependent on how we define + so once we proceed to real number axioms we will replace it with theorems such as addcl 7769. (Contributed by Jim Kingdon, 14-Jul-2021.)
|- ( ( A e. V /\ B e. W ) -> ( A + B ) e. _V )
Theorem	pitonnlem1 7677*	Lemma for pitonn 7680. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.)
|- <. [ <. ( <. { l | l <Q [ <. 1o , 1o >. ] ~Q } , { u | [ <. 1o , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. = 1
Theorem	pitonnlem1p1 7678	Lemma for pitonn 7680. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.)
|- ( A e. P. -> [ <. ( A +P. ( 1P +P. 1P ) ) , ( 1P +P. 1P ) >. ] ~R = [ <. ( A +P. 1P ) , 1P >. ] ~R )
Theorem	pitonnlem2 7679*	Lemma for pitonn 7680. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.)
|- ( K e. N. -> ( <. [ <. ( <. { l | l <Q [ <. K , 1o >. ] ~Q } , { u | [ <. K , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. + 1 ) = <. [ <. ( <. { l | l <Q [ <. ( K +N 1o ) , 1o >. ] ~Q } , { u | [ <. ( K +N 1o ) , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. )
Theorem	pitonn 7680*	Mapping from N. to NN. (Contributed by Jim Kingdon, 22-Apr-2020.)
|- ( N e. N. -> <. [ <. ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
Theorem	pitoregt0 7681*	Embedding from N. to RR yields a number greater than zero. (Contributed by Jim Kingdon, 15-Jul-2021.)
|- ( N e. N. -> 0 <RR <. [ <. ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. )
Theorem	pitore 7682*	Embedding from N. to RR. Similar to pitonn 7680 but separate in the sense that we have not proved nnssre 8748 yet. (Contributed by Jim Kingdon, 15-Jul-2021.)
|- ( N e. N. -> <. [ <. ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. e. RR )
Theorem	recnnre 7683*	Embedding the reciprocal of a natural number into RR. (Contributed by Jim Kingdon, 15-Jul-2021.)
|- ( N e. N. -> <. [ <. ( <. { l | l <Q ( *Q ` [ <. N , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. N , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. e. RR )
Theorem	peano1nnnn 7684*	One is an element of NN. This is a counterpart to 1nn 8755 designed for real number axioms which involve natural numbers (notably, axcaucvg 7732). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   =>    |- 1 e. N
Theorem	peano2nnnn 7685*	A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 8756 designed for real number axioms which involve to natural numbers (notably, axcaucvg 7732). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   =>    |- ( A e. N -> ( A + 1 ) e. N )
Theorem	ltrennb 7686*	Ordering of natural numbers with <N or <RR. (Contributed by Jim Kingdon, 13-Jul-2021.)
|- ( ( J e. N. /\ K e. N. ) -> ( J <N K <-> <. [ <. ( <. { l | l <Q [ <. J , 1o >. ] ~Q } , { u | [ <. J , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. <RR <. [ <. ( <. { l | l <Q [ <. K , 1o >. ] ~Q } , { u | [ <. K , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) )
Theorem	ltrenn 7687*	Ordering of natural numbers with <N or <RR. (Contributed by Jim Kingdon, 12-Jul-2021.)
|- ( J <N K -> <. [ <. ( <. { l | l <Q [ <. J , 1o >. ] ~Q } , { u | [ <. J , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. <RR <. [ <. ( <. { l | l <Q [ <. K , 1o >. ] ~Q } , { u | [ <. K , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. )
Theorem	recidpipr 7688*	Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.)
|- ( N e. N. -> ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. .P. <. { l | l <Q ( *Q ` [ <. N , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. N , 1o >. ] ~Q ) <Q u } >. ) = 1P )
Theorem	recidpirqlemcalc 7689	Lemma for recidpirq 7690. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.)
|- ( ph -> A e. P. )   &    |- ( ph -> B e. P. )   &    |- ( ph -> ( A .P. B ) = 1P )   =>    |- ( ph -> ( ( ( ( A +P. 1P ) .P. ( B +P. 1P ) ) +P. ( 1P .P. 1P ) ) +P. 1P ) = ( ( ( ( A +P. 1P ) .P. 1P ) +P. ( 1P .P. ( B +P. 1P ) ) ) +P. ( 1P +P. 1P ) ) )
Theorem	recidpirq 7690*	A real number times its reciprocal is one, where reciprocal is expressed with *Q. (Contributed by Jim Kingdon, 15-Jul-2021.)
|- ( N e. N. -> ( <. [ <. ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. x. <. [ <. ( <. { l | l <Q ( *Q ` [ <. N , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. N , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = 1 )
4.1.2  Final derivation of real and complex number postulates
Theorem	axcnex 7691	The complex numbers form a set. Use cnex 7768 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
|- CC e. _V
Theorem	axresscn 7692	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 7736. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
|- RR C_ CC
Theorem	ax1cn 7693	1 is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 7737. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
|- 1 e. CC
Theorem	ax1re 7694	1 is a real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1re 7738. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 7737 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
Theorem	axicn 7695	_i is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 7739. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
|- _i e. CC
Theorem	axaddcl 7696	Closure law for addition of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcl 7740 be used later. Instead, in most cases use addcl 7769. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	axaddrcl 7697	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl 7741 be used later. Instead, in most cases use readdcl 7770. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	axmulcl 7698	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcl 7742 be used later. Instead, in most cases use mulcl 7771. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	axmulrcl 7699	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 7743 be used later. Instead, in most cases use remulcl 7772. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	axaddf 7700	Addition is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axaddcl 7696. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 7766. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
|- + : ( CC X. CC ) --> CC