P. 80 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7901-8000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	suplocsrlemb 7901*	Lemma for suplocsr 7904. 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 7902*	Lemma for suplocsr 7904. 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 7903*	Lemma for suplocsr 7904. 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 7904*	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 7905	Class of complex numbers.
class CC
Syntax	cr 7906	Class of real numbers.
class RR
Syntax	cc0 7907	Extend class notation to include the complex number 0.
class 0
Syntax	c1 7908	Extend class notation to include the complex number 1.
class 1
Syntax	ci 7909	Extend class notation to include the complex number i.
class _i
Syntax	caddc 7910	Addition on complex numbers.
class +
Syntax	cltrr 7911	'Less than' predicate (defined over real subset of complex numbers).
class <RR
Syntax	cmul 7912	Multiplication on complex numbers. The token x. is a center dot.
class x.
Definition	df-c 7913	Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- CC = ( R. X. R. )
Definition	df-0 7914	Define the complex number 0. (Contributed by NM, 22-Feb-1996.)
|- 0 = <. 0R , 0R >.
Definition	df-1 7915	Define the complex number 1. (Contributed by NM, 22-Feb-1996.)
|- 1 = <. 1R , 0R >.
Definition	df-i 7916	Define the complex number _i (the imaginary unit). (Contributed by NM, 22-Feb-1996.)
|- _i = <. 0R , 1R >.
Definition	df-r 7917	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.)
|- RR = ( R. X. { 0R } )
Definition	df-add 7918*	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 7919*	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 7920*	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 7921	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 7922	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 7923*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.)
|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A )
Theorem	elrealeu 7924*	The real number mapping in elreal 7923 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.)
|- ( A e. RR <-> E! x e. R. <. x , 0R >. = A )
Theorem	elreal2 7925	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 7926	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 7927 which is a related property. (Contributed by NM, 2-May-1996.)
|- -. (/) e. CC
Theorem	cnm 7927*	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 7928	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.)
|- <RR C_ ( RR X. RR )
Theorem	addcnsr 7929	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 7930	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 7931	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 7932	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 7933	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 7934	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 7935	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 7936	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in CC from those in R.. The trick involves qsid 6677, 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 7913), 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 7937	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7936 and mulcnsrec 7938. (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 7938	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6676, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7936. (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 7939	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 8032. (Contributed by Jim Kingdon, 14-Jul-2021.)
|- ( ( A e. V /\ B e. W ) -> ( A + B ) e. _V )
Theorem	pitonnlem1 7940*	Lemma for pitonn 7943. 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 7941	Lemma for pitonn 7943. 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 7942*	Lemma for pitonn 7943. 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 7943*	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 7944*	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 7945*	Embedding from N. to RR. Similar to pitonn 7943 but separate in the sense that we have not proved nnssre 9022 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 7946*	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 7947*	One is an element of NN. This is a counterpart to 1nn 9029 designed for real number axioms which involve natural numbers (notably, axcaucvg 7995). (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 7948*	A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 9030 designed for real number axioms which involve to natural numbers (notably, axcaucvg 7995). (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 7949*	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 7950*	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 7951*	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 7952	Lemma for recidpirq 7953. 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 7953*	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 7954	The complex numbers form a set. Use cnex 8031 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
|- CC e. _V
Theorem	axresscn 7955	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 7999. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
|- RR C_ CC
Theorem	ax1cn 7956	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 8000. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
|- 1 e. CC
Theorem	ax1re 7957	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 8001. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 8000 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 7958	_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 8002. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
|- _i e. CC
Theorem	axaddcl 7959	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 8003 be used later. Instead, in most cases use addcl 8032. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	axaddrcl 7960	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 8004 be used later. Instead, in most cases use readdcl 8033. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	axmulcl 7961	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 8005 be used later. Instead, in most cases use mulcl 8034. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	axmulrcl 7962	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 8006 be used later. Instead, in most cases use remulcl 8035. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	axaddf 7963	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 7959. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 8029. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
|- + : ( CC X. CC ) --> CC
Theorem	axmulf 7964	Multiplication is an operation on the complex numbers. This is the construction-dependent version of ax-mulf 8030 and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific mulcl 8034. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
|- x. : ( CC X. CC ) --> CC
Theorem	axaddcom 7965	Addition commutes. 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-addcom 8007 be used later. Instead, use addcom 8191. In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
Theorem	axmulcom 7966	Multiplication of complex numbers is commutative. 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-mulcom 8008 be used later. Instead, use mulcom 8036. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	axaddass 7967	Addition of complex numbers is associative. This theorem transfers the associative laws for the real and imaginary signed real components of complex number pairs, to complex number addition itself. 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-addass 8009 be used later. Instead, use addass 8037. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	axmulass 7968	Multiplication of complex numbers is associative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 8010. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
Theorem	axdistr 7969	Distributive law for complex numbers (left-distributivity). 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-distr 8011 be used later. Instead, use adddi 8039. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )
Theorem	axi2m1 7970	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 8012. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
|- ( ( _i x. _i ) + 1 ) = 0
Theorem	ax0lt1 7971	0 is less than 1. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0lt1 8013. The version of this axiom in the Metamath Proof Explorer reads 1 =/= 0; here we change it to 0 <RR 1. The proof of 0 <RR 1 from 1 =/= 0 in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- 0 <RR 1
Theorem	ax1rid 7972	1 is an identity element for real multiplication. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 8014. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
|- ( A e. RR -> ( A x. 1 ) = A )
Theorem	ax0id 7973	0 is an identity element for real addition. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-0id 8015. In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.)
|- ( A e. CC -> ( A + 0 ) = A )
Theorem	axrnegex 7974*	Existence of negative of real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex 8016. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Theorem	axprecex 7975*	Existence of positive reciprocal of positive real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-precex 8017. In treatments which assume excluded middle, the 0 <RR A condition is generally replaced by A =/= 0, and it may not be necessary to state that the reciproacal is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) (New usage is discouraged.)
|- ( ( A e. RR /\ 0 <RR A ) -> E. x e. RR ( 0 <RR x /\ ( A x. x ) = 1 ) )
Theorem	axcnre 7976*	A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre 8018. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
|- ( A e. CC -> E. x e. RR E. y e. RR A = ( x + ( _i x. y ) ) )
Theorem	axpre-ltirr 7977	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 8019. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- ( A e. RR -> -. A <RR A )
Theorem	axpre-ltwlin 7978	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 8020. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( A <RR C \/ C <RR B ) ) )
Theorem	axpre-lttrn 7979	Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 8021. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <RR B /\ B <RR C ) -> A <RR C ) )
Theorem	axpre-apti 7980	Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-apti 8022. (Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR /\ -. ( A <RR B \/ B <RR A ) ) -> A = B )
Theorem	axpre-ltadd 7981	Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 8023. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <RR B -> ( C + A ) <RR ( C + B ) ) )
Theorem	axpre-mulgt0 7982	The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 8024. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 <RR A /\ 0 <RR B ) -> 0 <RR ( A x. B ) ) )
Theorem	axpre-mulext 7983	Strong extensionality of multiplication (expressed in terms of <RR). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulext 8025. (Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <RR ( B x. C ) -> ( A <RR B \/ B <RR A ) ) )
Theorem	rereceu 7984*	The reciprocal from axprecex 7975 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.)
|- ( ( A e. RR /\ 0 <RR A ) -> E! x e. RR ( A x. x ) = 1 )
Theorem	recriota 7985*	Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.)
|- ( N e. N. -> ( iota_ r e. RR ( <. [ <. ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. x. r ) = 1 ) = <. [ <. ( <. { l | l <Q ( *Q ` [ <. N , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. N , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. )
Theorem	axarch 7986*	Archimedean axiom. The Archimedean property is more naturally stated once we have defined NN. Unless we find another way to state it, we'll just use the right hand side of dfnn2 9020 in stating what we mean by "natural number" in the context of this axiom. This construction-dependent theorem should not be referenced directly; instead, use ax-arch 8026. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)
|- ( A e. RR -> E. n e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } A <RR n )
Theorem	peano5nnnn 7987*	Peano's inductive postulate. This is a counterpart to peano5nni 9021 designed for real number axioms which involve natural numbers (notably, axcaucvg 7995). (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. A /\ A. z e. A ( z + 1 ) e. A ) -> N C_ A )
Theorem	nnindnn 7988*	Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 9034 designed for real number axioms which involve natural numbers (notably, axcaucvg 7995). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( z = 1 -> ( ph <-> ps ) )   &    |- ( z = k -> ( ph <-> ch ) )   &    |- ( z = ( k + 1 ) -> ( ph <-> th ) )   &    |- ( z = A -> ( ph <-> ta ) )   &    |- ps   &    |- ( k e. N -> ( ch -> th ) )   =>    |- ( A e. N -> ta )
Theorem	nntopi 7989*	Mapping from NN to N.. (Contributed by Jim Kingdon, 13-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   =>    |- ( A e. N -> E. z e. N. <. [ <. ( <. { l | l <Q [ <. z , 1o >. ] ~Q } , { u | [ <. z , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. = A )
Theorem	axcaucvglemcl 7990*	Lemma for axcaucvg 7995. Mapping to N. and R.. (Contributed by Jim Kingdon, 10-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   =>    |- ( ( ph /\ J e. N. ) -> ( iota_ z e. R. ( F ` <. [ <. ( <. { l | l <Q [ <. J , 1o >. ] ~Q } , { u | [ <. J , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. z , 0R >. ) e. R. )
Theorem	axcaucvglemf 7991*	Lemma for axcaucvg 7995. Mapping to N. and R. yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   &    |- G = ( j e. N. |-> ( iota_ z e. R. ( F ` <. [ <. ( <. { l | l <Q [ <. j , 1o >. ] ~Q } , { u | [ <. j , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. z , 0R >. ) )   =>    |- ( ph -> G : N. --> R. )
Theorem	axcaucvglemval 7992*	Lemma for axcaucvg 7995. Value of sequence when mapping to N. and R.. (Contributed by Jim Kingdon, 10-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   &    |- G = ( j e. N. |-> ( iota_ z e. R. ( F ` <. [ <. ( <. { l | l <Q [ <. j , 1o >. ] ~Q } , { u | [ <. j , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. z , 0R >. ) )   =>    |- ( ( ph /\ J e. N. ) -> ( F ` <. [ <. ( <. { l | l <Q [ <. J , 1o >. ] ~Q } , { u | [ <. J , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. ( G ` J ) , 0R >. )
Theorem	axcaucvglemcau 7993*	Lemma for axcaucvg 7995. The result of mapping to N. and R. satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   &    |- G = ( j e. N. |-> ( iota_ z e. R. ( F ` <. [ <. ( <. { l | l <Q [ <. j , 1o >. ] ~Q } , { u | [ <. j , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. z , 0R >. ) )   =>    |- ( 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	axcaucvglemres 7994*	Lemma for axcaucvg 7995. Mapping the limit from N. and R.. (Contributed by Jim Kingdon, 10-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   &    |- G = ( j e. N. |-> ( iota_ z e. R. ( F ` <. [ <. ( <. { l | l <Q [ <. j , 1o >. ] ~Q } , { u | [ <. j , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. z , 0R >. ) )   =>    |- ( ph -> E. y e. RR A. x e. RR ( 0 <RR x -> E. j e. N A. k e. N ( j <RR k -> ( ( F ` k ) <RR ( y + x ) /\ y <RR ( ( F ` k ) + x ) ) ) ) )
Theorem	axcaucvg 7995*	Real number completeness axiom. A Cauchy sequence with a modulus of convergence converges. 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). Because we are stating this axiom before we have introduced notations for NN or division, we use N for the natural numbers and express a reciprocal in terms of iota_. This construction-dependent theorem should not be referenced directly; instead, use ax-caucvg 8027. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   =>    |- ( ph -> E. y e. RR A. x e. RR ( 0 <RR x -> E. j e. N A. k e. N ( j <RR k -> ( ( F ` k ) <RR ( y + x ) /\ y <RR ( ( F ` k ) + x ) ) ) ) )
Theorem	axpre-suploclemres 7996*	Lemma for axpre-suploc 7997. The result. The proof just needs to define B as basically the same set as A (but expressed as a subset of R. rather than a subset of RR), and apply suplocsr 7904. (Contributed by Jim Kingdon, 24-Jan-2024.)
|- ( ph -> A C_ RR )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. RR A. y e. A y <RR x )   &    |- ( ph -> A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) )   &    |- B = { w e. R. | <. w , 0R >. e. A }   =>    |- ( ph -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
Theorem	axpre-suploc 7997*	An inhabited, bounded-above, located set of reals has a supremum. Locatedness here means that given x < y, either there is an element of the set greater than x, or y is an upper bound. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 8028. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.)
|- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
4.1.3  Real and complex number postulates restated as axioms
Axiom	ax-cnex 7998	The complex numbers form a set. Proofs should normally use cnex 8031 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
|- CC e. _V
Axiom	ax-resscn 7999	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 7955. (Contributed by NM, 1-Mar-1995.)
|- RR C_ CC
Axiom	ax-1cn 8000	1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 7956. (Contributed by NM, 1-Mar-1995.)
|- 1 e. CC