Most Recent Proofs - Intuitionistic Logic Explorer

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Last updated on 24-Sep-2020 at 4:02 PM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
26-Aug-2020	sqrt0rlem 9192	Lemma for sqrt0 9193. (Contributed by Jim Kingdon, 26-Aug-2020.)
|- ((A e. RR /\ ((A ^ 2) = 0 /\ 0 <_ A)) <-> A = 0)
23-Aug-2020	sqrtrval 9189	Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
|- (A e. RR -> ( sqr ` A) = ( iota_x e. RR ((x ^ 2) = A /\ 0 <_ x)))
23-Aug-2020	df-rsqrt 9187	Define a function whose value is the square root of a nonnegative real number. Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.)
|- sqr = (x e. RR |-> ( iota_y e. RR ((y ^ 2) = x /\ 0 <_ y)))
19-Aug-2020	addnqpr 6541	Addition of fractions embedded into positive reals. One can either add the fractions as fractions, or embed them into positive reals and add them as positive reals, and get the same result. (Contributed by Jim Kingdon, 19-Aug-2020.)
|- ((A e. Q. /\ B e. Q.) -> <. { l | l <Q (A +Q B) } , {u | (A +Q B) <Q u } >. = ( <. { l | l <Q A } , {u | A <Q u } >. +P. <. { l | l <Q B } , {u | B <Q u } >.))
19-Aug-2020	addnqprlemfu 6540	Lemma for addnqpr 6541. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|- ((A e. Q. /\ B e. Q.) -> ( 2nd ` <. { l | l <Q (A +Q B) } , {u | (A +Q B) <Q u } >.) C_ ( 2nd ` ( <. { l | l <Q A } , {u | A <Q u } >. +P. <. { l | l <Q B } , {u | B <Q u } >.)))
19-Aug-2020	addnqprlemfl 6539	Lemma for addnqpr 6541. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|- ((A e. Q. /\ B e. Q.) -> ( 1st ` <. { l | l <Q (A +Q B) } , {u | (A +Q B) <Q u } >.) C_ ( 1st ` ( <. { l | l <Q A } , {u | A <Q u } >. +P. <. { l | l <Q B } , {u | B <Q u } >.)))
19-Aug-2020	addnqprlemru 6538	Lemma for addnqpr 6541. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|- ((A e. Q. /\ B e. Q.) -> ( 2nd ` ( <. { l | l <Q A } , {u | A <Q u } >. +P. <. { l | l <Q B } , {u | B <Q u } >.)) C_ ( 2nd ` <. { l | l <Q (A +Q B) } , {u | (A +Q B) <Q u } >.))
19-Aug-2020	addnqprlemrl 6537	Lemma for addnqpr 6541. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|- ((A e. Q. /\ B e. Q.) -> ( 1st ` ( <. { l | l <Q A } , {u | A <Q u } >. +P. <. { l | l <Q B } , {u | B <Q u } >.)) C_ ( 1st ` <. { l | l <Q (A +Q B) } , {u | (A +Q B) <Q u } >.))
15-Aug-2020	cauappcvgprlemcan 6615	Lemma for cauappcvgprlemladdrl 6628. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.)
|- (ph -> L e. P.)   &   |- (ph -> S e. Q.)   &   |- (ph -> R e. Q.)   &   |- (ph -> Q e. Q.)   =>   |- (ph -> (( R +Q Q) e. ( 1st ` ( L +P. <. { l | l <Q ( S +Q Q) } , {u | ( S +Q Q) <Q u } >.)) <-> R e. ( 1st ` ( L +P. <. { l | l <Q S } , {u | S <Q u } >.))))
4-Aug-2020	cauappcvgprlemupu 6620	Lemma for cauappcvgpr 6633. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   =>   |- ((ph /\ s <Q r /\ s e. ( 2nd ` L)) -> r e. ( 2nd ` L))
4-Aug-2020	cauappcvgprlemopu 6619	Lemma for cauappcvgpr 6633. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   =>   |- ((ph /\ r e. ( 2nd ` L)) -> E. s e. Q. ( s <Q r /\ s e. ( 2nd ` L)))
4-Aug-2020	cauappcvgprlemlol 6618	Lemma for cauappcvgpr 6633. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   =>   |- ((ph /\ s <Q r /\ r e. ( 1st ` L)) -> s e. ( 1st ` L))
4-Aug-2020	cauappcvgprlemopl 6617	Lemma for cauappcvgpr 6633. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   =>   |- ((ph /\ s e. ( 1st ` L)) -> E. r e. Q. ( s <Q r /\ r e. ( 1st ` L)))
18-Jul-2020	cauappcvgprlemloc 6623	Lemma for cauappcvgpr 6633. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   =>   |- (ph -> A. s e. Q. A. r e. Q. ( s <Q r -> ( s e. ( 1st ` L) \/ r e. ( 2nd ` L))))
18-Jul-2020	cauappcvgprlemdisj 6622	Lemma for cauappcvgpr 6633. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   =>   |- (ph -> A. s e. Q. -. ( s e. ( 1st ` L) /\ s e. ( 2nd ` L)))
18-Jul-2020	cauappcvgprlemrnd 6621	Lemma for cauappcvgpr 6633. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   =>   |- (ph -> (A. s e. Q. ( s e. ( 1st ` L) <-> E. r e. Q. ( s <Q r /\ r e. ( 1st ` L))) /\ A. r e. Q. ( r e. ( 2nd ` L) <-> E. s e. Q. ( s <Q r /\ s e. ( 2nd ` L)))))
18-Jul-2020	cauappcvgprlemm 6616	Lemma for cauappcvgpr 6633. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   =>   |- (ph -> (E. s e. Q. s e. ( 1st ` L) /\ E. r e. Q. r e. ( 2nd ` L)))
11-Jul-2020	cauappcvgprlemladdrl 6628	Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   &   |- (ph -> S e. Q.)   =>   |- (ph -> ( 1st ` <. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q S) } , {u e. Q. | E. q e. Q. ((( F ` q) +Q q) +Q S) <Q u } >.) C_ ( 1st ` ( L +P. <. { l | l <Q S } , {u | S <Q u } >.)))
11-Jul-2020	cauappcvgprlemladdru 6627	Lemma for cauappcvgprlemladd 6629. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   &   |- (ph -> S e. Q.)   =>   |- (ph -> ( 2nd ` <. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q S) } , {u e. Q. | E. q e. Q. ((( F ` q) +Q q) +Q S) <Q u } >.) C_ ( 2nd ` ( L +P. <. { l | l <Q S } , {u | S <Q u } >.)))
11-Jul-2020	cauappcvgprlemladdfl 6626	Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   &   |- (ph -> S e. Q.)   =>   |- (ph -> ( 1st ` ( L +P. <. { l | l <Q S } , {u | S <Q u } >.)) C_ ( 1st ` <. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q S) } , {u e. Q. | E. q e. Q. ((( F ` q) +Q q) +Q S) <Q u } >.))
11-Jul-2020	cauappcvgprlemladdfu 6625	Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   &   |- (ph -> S e. Q.)   =>   |- (ph -> ( 2nd ` ( L +P. <. { l | l <Q S } , {u | S <Q u } >.)) C_ ( 2nd ` <. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q S) } , {u e. Q. | E. q e. Q. ((( F ` q) +Q q) +Q S) <Q u } >.))
8-Jul-2020	nqprl 6532	Comparing a fraction to a real can be done by whether it is an element of the lower cut, or by <P. (Contributed by Jim Kingdon, 8-Jul-2020.)
|- ((A e. Q. /\ B e. P.) -> (A e. ( 1st ` B) <-> <. { l | l <Q A } , {u | A <Q u } >. <P B))
24-Jun-2020	nqprlu 6529	The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.)
|- (A e. Q. -> <. { l | l <Q A } , {u | A <Q u } >. e. P.)
23-Jun-2020	cauappcvgprlem2 6631	Lemma for cauappcvgpr 6633. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   &   |- (ph -> Q e. Q.)   &   |- (ph -> R e. Q.)   =>   |- (ph -> L <P <. { l | l <Q (( F ` Q) +Q ( Q +Q R)) } , {u | (( F ` Q) +Q ( Q +Q R)) <Q u } >.)
23-Jun-2020	cauappcvgprlem1 6630	Lemma for cauappcvgpr 6633. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   &   |- (ph -> Q e. Q.)   &   |- (ph -> R e. Q.)   =>   |- (ph -> <. { l | l <Q ( F ` Q) } , {u | ( F ` Q) <Q u } >. <P ( L +P. <. { l | l <Q ( Q +Q R) } , {u | ( Q +Q R) <Q u } >.))
23-Jun-2020	cauappcvgprlemladd 6629	Lemma for cauappcvgpr 6633. This takes L and offsets it by the positive fraction S. (Contributed by Jim Kingdon, 23-Jun-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   &   |- (ph -> S e. Q.)   =>   |- (ph -> ( L +P. <. { l | l <Q S } , {u | S <Q u } >.) = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q (( F ` q) +Q S) } , {u e. Q. | E. q e. Q. ((( F ` q) +Q q) +Q S) <Q u } >.)
20-Jun-2020	cauappcvgprlemlim 6632	Lemma for cauappcvgpr 6633. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   =>   |- (ph -> A. q e. Q. A. r e. Q. ( <. { l | l <Q ( F ` q) } , {u | ( F ` q) <Q u } >. <P ( L +P. <. { l | l <Q ( q +Q r) } , {u | ( q +Q r) <Q u } >.) /\ L <P <. { l | l <Q (( F ` q) +Q ( q +Q r)) } , {u | (( F ` q) +Q ( q +Q r)) <Q u } >.))
20-Jun-2020	cauappcvgprlemcl 6624	Lemma for cauappcvgpr 6633. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   &   |- L = <. { l e. Q. | E. q e. Q. ( l +Q q) <Q ( F ` q) } , {u e. Q. | E. q e. Q. (( F ` q) +Q q) <Q u } >.   =>   |- (ph -> L e. P.)
19-Jun-2020	cauappcvgpr 6633	A Cauchy approximation has a limit. A Cauchy approximation, here F, is similar to a Cauchy sequence but is indexed by the desired tolerance (that is, how close together terms needs to be) rather than by natural numbers. This is basically Theorem 11.2.12 of [HoTT], p. (varies) with a few differences such as that we are proving the existence of a limit without anything about how fast it converges (that is, mere existence instead of existence, in HoTT terms), and that the codomain of F is Q. rather than P.. We also specify that every term needs to be larger than a fraction A, to avoid the case where we have positive fractions which converge to zero (which is not a positive real). (Contributed by Jim Kingdon, 19-Jun-2020.)
|- (ph -> F : Q. --> Q.)   &   |- (ph -> A. p e. Q. A. q e. Q. (( F ` p) <Q (( F ` q) +Q ( p +Q q)) /\ ( F ` q) <Q (( F ` p) +Q ( p +Q q))))   &   |- (ph -> A. p e. Q. A <Q ( F ` p))   =>   |- (ph -> E.y e. P. A. q e. Q. A. r e. Q. ( <. { l | l <Q ( F ` q) } , {u | ( F ` q) <Q u } >. <P (y +P. <. { l | l <Q ( q +Q r) } , {u | ( q +Q r) <Q u } >.) /\ y <P <. { l | l <Q (( F ` q) +Q ( q +Q r)) } , {u | (( F ` q) +Q ( q +Q r)) <Q u } >.))
15-Jun-2020	imdivapd 9182	Imaginary part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- (ph -> A e. RR)   &   |- (ph -> B e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> ( Im ` (B / A)) = (( Im ` B) / A))
15-Jun-2020	redivapd 9181	Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- (ph -> A e. RR)   &   |- (ph -> B e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> ( Re ` (B / A)) = (( Re ` B) / A))
15-Jun-2020	cjdivapd 9175	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ( * ` (A / B)) = (( * ` A) / ( * ` B)))
15-Jun-2020	riotaexg 5415	Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.)
|- (A e. V -> ( iota_x e. A ps) e. _V)
14-Jun-2020	cjdivapi 9143	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- A e. CC   &   |- B e. CC   =>   |- (B # 0 -> ( * ` (A / B)) = (( * ` A) / ( * ` B)))
14-Jun-2020	cjdivap 9117	Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ((A e. CC /\ B e. CC /\ B # 0) -> ( * ` (A / B)) = (( * ` A) / ( * ` B)))
14-Jun-2020	cjap0 9115	A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- (A e. CC -> (A # 0 <-> ( * ` A) # 0))
14-Jun-2020	cjap 9114	Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ((A e. CC /\ B e. CC) -> (( * ` A) # ( * ` B) <-> A # B))
14-Jun-2020	imdivap 9089	Imaginary part of a division. Related to immul2 9088. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ((A e. CC /\ B e. RR /\ B # 0) -> ( Im ` (A / B)) = (( Im ` A) / B))
14-Jun-2020	redivap 9082	Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ((A e. CC /\ B e. RR /\ B # 0) -> ( Re ` (A / B)) = (( Re ` A) / B))
14-Jun-2020	mulreap 9072	A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
|- ((A e. CC /\ B e. RR /\ B # 0) -> (A e. RR <-> (B x. A) e. RR))
13-Jun-2020	sqgt0apd 9041	The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
|- (ph -> A e. RR)   &   |- (ph -> A # 0)   =>   |- (ph -> 0 < (A ^ 2))
13-Jun-2020	reexpclzapd 9038	Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
|- (ph -> A e. RR)   &   |- (ph -> A # 0)   &   |- (ph -> N e. ZZ)   =>   |- (ph -> (A ^ N) e. RR)
13-Jun-2020	expdivapd 9028	Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> N e. NN0)   =>   |- (ph -> ((A / B) ^ N) = ((A ^ N) / (B ^ N)))
13-Jun-2020	sqdivapd 9027	Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ((A / B) ^ 2) = ((A ^ 2) / (B ^ 2)))
12-Jun-2020	expsubapd 9025	Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> N e. ZZ)   &   |- (ph -> M e. ZZ)   =>   |- (ph -> (A ^( M - N)) = ((A ^ M) / (A ^ N)))
12-Jun-2020	expm1apd 9024	Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> N e. ZZ)   =>   |- (ph -> (A ^( N - 1)) = ((A ^ N) / A))
12-Jun-2020	expp1zapd 9023	Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> N e. ZZ)   =>   |- (ph -> (A ^( N + 1)) = ((A ^ N) x. A))
12-Jun-2020	exprecapd 9022	Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> N e. ZZ)   =>   |- (ph -> (( 1 / A) ^ N) = ( 1 / (A ^ N)))
12-Jun-2020	expnegapd 9021	Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> N e. ZZ)   =>   |- (ph -> (A ^ -u N) = ( 1 / (A ^ N)))
12-Jun-2020	expap0d 9020	Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> N e. ZZ)   =>   |- (ph -> (A ^ N) # 0)
12-Jun-2020	expclzapd 9019	Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> N e. ZZ)   =>   |- (ph -> (A ^ N) e. CC)
12-Jun-2020	sqrecapd 9018	Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> (( 1 / A) ^ 2) = ( 1 / (A ^ 2)))
12-Jun-2020	sqgt0api 8972	The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- A e. RR   =>   |- (A # 0 -> 0 < (A ^ 2))
12-Jun-2020	sqdivapi 8970	Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
|- A e. CC   &   |- B e. CC   &   |- B # 0   =>   |- ((A / B) ^ 2) = ((A ^ 2) / (B ^ 2))
11-Jun-2020	sqgt0ap 8955	The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ((A e. RR /\ A # 0) -> 0 < (A ^ 2))
11-Jun-2020	sqdivap 8952	Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ((A e. CC /\ B e. CC /\ B # 0) -> ((A / B) ^ 2) = ((A ^ 2) / (B ^ 2)))
11-Jun-2020	expdivap 8939	Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ((A e. CC /\ (B e. CC /\ B # 0) /\ N e. NN0) -> ((A / B) ^ N) = ((A ^ N) / (B ^ N)))
11-Jun-2020	expm1ap 8938	Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ((A e. CC /\ A # 0 /\ N e. ZZ) -> (A ^( N - 1)) = ((A ^ N) / A))
11-Jun-2020	expp1zap 8937	Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- ((A e. CC /\ A # 0 /\ N e. ZZ) -> (A ^( N + 1)) = ((A ^ N) x. A))
11-Jun-2020	expsubap 8936	Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- (((A e. CC /\ A # 0) /\ ( M e. ZZ /\ N e. ZZ)) -> (A ^( M - N)) = ((A ^ M) / (A ^ N)))
11-Jun-2020	expmulzap 8935	Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
|- (((A e. CC /\ A # 0) /\ ( M e. ZZ /\ N e. ZZ)) -> (A ^( M x. N)) = ((A ^ M) ^ N))
10-Jun-2020	expaddzap 8933	Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- (((A e. CC /\ A # 0) /\ ( M e. ZZ /\ N e. ZZ)) -> (A ^( M + N)) = ((A ^ M) x. (A ^ N)))
10-Jun-2020	expaddzaplem 8932	Lemma for expaddzap 8933. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- (((A e. CC /\ A # 0) /\ ( M e. RR /\ -u M e. NN) /\ N e. NN0) -> (A ^( M + N)) = ((A ^ M) x. (A ^ N)))
10-Jun-2020	exprecap 8930	Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ((A e. CC /\ A # 0 /\ N e. ZZ) -> (( 1 / A) ^ N) = ( 1 / (A ^ N)))
10-Jun-2020	mulexpzap 8929	Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- (((A e. CC /\ A # 0) /\ (B e. CC /\ B # 0) /\ N e. ZZ) -> ((A x. B) ^ N) = ((A ^ N) x. (B ^ N)))
10-Jun-2020	expap0i 8921	Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ((A e. CC /\ A # 0 /\ N e. ZZ) -> (A ^ N) # 0)
10-Jun-2020	expap0 8919	Positive integer exponentiation is apart from zero iff its mantissa is apart from zero. That it is easier to prove this first, and then prove expeq0 8920 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." ([Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ((A e. CC /\ N e. NN) -> ((A ^ N) # 0 <-> A # 0))
10-Jun-2020	mvllmulapd 7570	Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> (A x. B) = C)   =>   |- (ph -> B = ( C / A))
9-Jun-2020	expclzap 8914	Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- ((A e. CC /\ A # 0 /\ N e. ZZ) -> (A ^ N) e. CC)
9-Jun-2020	expclzaplem 8913	Closure law for integer exponentiation. Lemma for expclzap 8914 and expap0i 8921. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- ((A e. CC /\ A # 0 /\ N e. ZZ) -> (A ^ N) e. {z e. CC | z # 0 })
9-Jun-2020	reexpclzap 8909	Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- ((A e. RR /\ A # 0 /\ N e. ZZ) -> (A ^ N) e. RR)
9-Jun-2020	neg1ap0 7784	-1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
|- -u 1 # 0
8-Jun-2020	expcl2lemap 8901	Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.)
|- F C_ CC   &   |- ((x e. F /\ y e. F) -> (x x. y) e. F)   &   |- 1 e. F   &   |- ((x e. F /\ x # 0) -> ( 1 / x) e. F)   =>   |- ((A e. F /\ A # 0 /\ B e. ZZ) -> (A ^B) e. F)
8-Jun-2020	expn1ap0 8899	A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.)
|- ((A e. CC /\ A # 0) -> (A ^ -u 1) = ( 1 / A))
8-Jun-2020	expineg2 8898	Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.)
|- (((A e. CC /\ A # 0) /\ ( N e. CC /\ -u N e. NN0)) -> (A ^ N) = ( 1 / (A ^ -u N)))
8-Jun-2020	expnegap0 8897	Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.)
|- ((A e. CC /\ A # 0 /\ N e. NN0) -> (A ^ -u N) = ( 1 / (A ^ N)))
8-Jun-2020	expinnval 8892	Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.)
|- ((A e. CC /\ N e. NN) -> (A ^ N) = ( seq 1( x. , ( NN X. {A }) , CC) ` N))
7-Jun-2020	expival 8891	Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.)
|- ((A e. CC /\ N e. ZZ /\ (A # 0 \/ 0 <_ N)) -> (A ^ N) = if( N = 0 , 1 , if( 0 < N , ( seq 1( x. , ( NN X. {A }) , CC) ` N) , ( 1 / ( seq 1( x. , ( NN X. {A }) , CC) ` -u N)))))
7-Jun-2020	expivallem 8890	Lemma for expival 8891. If we take a complex number apart from zero and raise it to a positive integer power, the result is apart from zero. (Contributed by Jim Kingodon, 7-Jun-2020.)
|- ((A e. CC /\ A # 0 /\ N e. NN) -> ( seq 1( x. , ( NN X. {A }) , CC) ` N) # 0)
7-Jun-2020	df-iexp 8889	Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 8893 and expp1 8896 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. 10-Jun-2005: The definition was extended to include zero exponents, so that 0 ^ 0 = 1 per the convention of Definition 10-4.1 of [Gleason] p. 134. 4-Jun-2014: The definition was extended to include negative integer exponents. The case x = 0 , y < 0 gives the value ( 1 / 0), so we will avoid this case in our theorems. (Contributed by Jim Kingodon, 7-Jun-2020.)
|- ^ = (x e. CC , y e. ZZ |-> if(y = 0 , 1 , if( 0 < y , ( seq 1( x. , ( NN X. {x }) , CC) ` y) , ( 1 / ( seq 1( x. , ( NN X. {x }) , CC) ` -uy)))))
4-Jun-2020	iseqfveq 8887	Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.)
|- (ph -> N e. ( ZZ>= ` M))   &   |- ((ph /\ k e. ( M ... N)) -> ( F ` k) = ( G ` k))   &   |- (ph -> S e. V)   &   |- ((ph /\ x e. ( ZZ>= ` M)) -> ( F ` x) e. S)   &   |- ((ph /\ x e. ( ZZ>= ` M)) -> ( G ` x) e. S)   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x .+ y) e. S)   =>   |- (ph -> ( seq M( .+ , F , S) ` N) = ( seq M( .+ , G , S) ` N))
3-Jun-2020	iseqfeq2 8886	Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
|- (ph -> K e. ( ZZ>= ` M))   &   |- (ph -> ( seq M( .+ , F , S) ` K) = ( G ` K))   &   |- (ph -> S e. V)   &   |- ((ph /\ x e. ( ZZ>= ` M)) -> ( F ` x) e. S)   &   |- ((ph /\ x e. ( ZZ>= ` K)) -> ( G ` x) e. S)   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x .+ y) e. S)   &   |- ((ph /\ k e. ( ZZ>= ` ( K + 1))) -> ( F ` k) = ( G ` k))   =>   |- (ph -> ( seq M( .+ , F , S) |` ( ZZ>= ` K)) = seq K( .+ , G , S))
3-Jun-2020	iseqfveq2 8885	Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
|- (ph -> K e. ( ZZ>= ` M))   &   |- (ph -> ( seq M( .+ , F , S) ` K) = ( G ` K))   &   |- (ph -> S e. V)   &   |- ((ph /\ x e. ( ZZ>= ` M)) -> ( F ` x) e. S)   &   |- ((ph /\ x e. ( ZZ>= ` K)) -> ( G ` x) e. S)   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x .+ y) e. S)   &   |- (ph -> N e. ( ZZ>= ` K))   &   |- ((ph /\ k e. (( K + 1) ... N)) -> ( F ` k) = ( G ` k))   =>   |- (ph -> ( seq M( .+ , F , S) ` N) = ( seq K( .+ , G , S) ` N))
1-Jun-2020	iseqcl 8883	Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.)
|- (ph -> N e. ( ZZ>= ` M))   &   |- (ph -> S e. V)   &   |- ((ph /\ x e. ( ZZ>= ` M)) -> ( F ` x) e. S)   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x .+ y) e. S)   =>   |- (ph -> ( seq M( .+ , F , S) ` N) e. S)
1-Jun-2020	fzdcel 8654	Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
|- (( K e. ZZ /\ M e. ZZ /\ N e. ZZ) -> DECID K e. ( M ... N))
1-Jun-2020	fztri3or 8653	Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
|- (( K e. ZZ /\ M e. ZZ /\ N e. ZZ) -> ( K < M \/ K e. ( M ... N) \/ N < K))
1-Jun-2020	zdclt 8074	Integer < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
|- ((A e. ZZ /\ B e. ZZ) -> DECID A < B)
31-May-2020	iseqp1 8884	Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 31-May-2020.)
|- (ph -> N e. ( ZZ>= ` M))   &   |- (ph -> S e. V)   &   |- ((ph /\ x e. ( ZZ>= ` M)) -> ( F ` x) e. S)   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x .+ y) e. S)   =>   |- (ph -> ( seq M( .+ , F , S) ` ( N + 1)) = (( seq M( .+ , F , S) ` N) .+ ( F ` ( N + 1))))
31-May-2020	iseq1 8882	Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.)
|- (ph -> M e. ZZ)   &   |- (ph -> S e. V)   &   |- ((ph /\ x e. ( ZZ>= ` M)) -> ( F ` x) e. S)   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x .+ y) e. S)   =>   |- (ph -> ( seq M( .+ , F , S) ` M) = ( F ` M))
31-May-2020	iseqovex 8879	Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.)
|- ((ph /\ x e. ( ZZ>= ` M)) -> ( F ` x) e. S)   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x .+ y) e. S)   =>   |- ((ph /\ (x e. ( ZZ>= ` M) /\ y e. S)) -> (x(z e. ( ZZ>= ` M) , w e. S |-> (w .+ ( F ` (z + 1))))y) e. S)
31-May-2020	frecuzrdgcl 8860	Closure law for the recursive definition generator on upper integers. See comment in frec2uz0d 8846 for the description of G as the mapping from om to ( ZZ>= ` C). (Contributed by Jim Kingdon, 31-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> S e. V)   &   |- (ph -> A e. S)   &   |- ((ph /\ (x e. ( ZZ>= ` C) /\ y e. S)) -> (x Fy) e. S)   &   |- R = frec((x e. ( ZZ>= ` C) , y e. S |-> <.(x + 1) , (x Fy) >.) , <. C , A >.)   &   |- (ph -> T = ran R)   =>   |- ((ph /\ B e. ( ZZ>= ` C)) -> ( T ` B) e. S)
30-May-2020	iseqfn 8881	The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.)
|- (ph -> M e. ZZ)   &   |- (ph -> S e. V)   &   |- ((ph /\ x e. ( ZZ>= ` M)) -> ( F ` x) e. S)   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x .+ y) e. S)   =>   |- (ph -> seq M( .+ , F , S) Fn ( ZZ>= ` M))
30-May-2020	iseqval 8880	Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.)
|- R = frec((x e. ( ZZ>= ` M) , y e. S |-> <.(x + 1) , (x(z e. ( ZZ>= ` M) , w e. S |-> (w .+ ( F ` (z + 1))))y) >.) , <. M , ( F ` M) >.)   &   |- ((ph /\ x e. ( ZZ>= ` M)) -> ( F ` x) e. S)   &   |- ((ph /\ (x e. S /\ y e. S)) -> (x .+ y) e. S)   =>   |- (ph -> seq M( .+ , F , S) = ran R)
30-May-2020	nfiseq 8878	Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
|- F/_x M   &   |- F/_x .+   &   |- F/_x F   &   |- F/_x S   =>   |- F/_x seq M( .+ , F , S)
30-May-2020	iseqeq4 8877	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( S = T -> seq M( .+ , F , S) = seq M( .+ , F , T))
30-May-2020	iseqeq3 8876	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( F = G -> seq M( .+ , F , S) = seq M( .+ , G , S))
30-May-2020	iseqeq2 8875	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( .+ = Q -> seq M( .+ , F , S) = seq M( Q , F , S))
30-May-2020	iseqeq1 8874	Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( M = N -> seq M( .+ , F , S) = seq N( .+ , F , S))
30-May-2020	nffrec 5921	Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- F/_x F   &   |- F/_xA   =>   |- F/_xfrec( F , A)
30-May-2020	freceq2 5920	Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- (A = B -> frec( F , A) = frec( F , B))
30-May-2020	freceq1 5919	Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( F = G -> frec( F , A) = frec( G , A))
29-May-2020	df-iseq 8873	Define a general-purpose operation that builds a recursive sequence (i.e. a function on the positive integers NN or some other upper integer set) whose value at an index is a function of its previous value and the value of an input sequence at that index. This definition is complicated, but fortunately it is not intended to be used directly. Instead, the only purpose of this definition is to provide us with an object that has the properties expressed by iseq1 8882 and at successors. Typically, those are the main theorems that would be used in practice. The first operand in the parentheses is the operation that is applied to the previous value and the value of the input sequence (second operand). The operand to the left of the parenthesis is the integer to start from. For example, for the operation +, an input sequence F with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence seq 1( + , F) with values 1, 3/2, 7/4, 15/8,.., so that ( seq 1( + , F) ` 1) = 1, ( seq 1( + , F) ` 2) = 3/2, etc. In other words, seq M( + , F) transforms a sequence F into an infinite series. Internally, the frec function generates as its values a set of ordered pairs starting at <. M , ( F ` M) >., with the first member of each pair incremented by one in each successive value. So, the range of frec is exactly the sequence we want, and we just extract the range and throw away the domain. (Contributed by Jim Kingdon, 29-May-2020.)
|- seq M( .+ , F , S) = ran frec((x e. ( ZZ>= ` M) , y e. S |-> <.(x + 1) , (y .+ ( F ` (x + 1))) >.) , <. M , ( F ` M) >.)
28-May-2020	frecuzrdgsuc 8862	Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 8846 for the description of G as the mapping from om to ( ZZ>= ` C). (Contributed by Jim Kingdon, 28-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> S e. V)   &   |- (ph -> A e. S)   &   |- ((ph /\ (x e. ( ZZ>= ` C) /\ y e. S)) -> (x Fy) e. S)   &   |- R = frec((x e. ( ZZ>= ` C) , y e. S |-> <.(x + 1) , (x Fy) >.) , <. C , A >.)   &   |- (ph -> T = ran R)   =>   |- ((ph /\ B e. ( ZZ>= ` C)) -> ( T ` (B + 1)) = (B F( T ` B)))
27-May-2020	frecuzrdg0 8861	Initial value of a recursive definition generator on upper integers. See comment in frec2uz0d 8846 for the description of G as the mapping from om to ( ZZ>= ` C). (Contributed by Jim Kingdon, 27-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> S e. V)   &   |- (ph -> A e. S)   &   |- ((ph /\ (x e. ( ZZ>= ` C) /\ y e. S)) -> (x Fy) e. S)   &   |- R = frec((x e. ( ZZ>= ` C) , y e. S |-> <.(x + 1) , (x Fy) >.) , <. C , A >.)   &   |- (ph -> T = ran R)   =>   |- (ph -> ( T ` C) = A)
27-May-2020	frecuzrdgrrn 8855	The function R (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of S. (Contributed by Jim Kingdon, 27-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> S e. V)   &   |- (ph -> A e. S)   &   |- ((ph /\ (x e. ( ZZ>= ` C) /\ y e. S)) -> (x Fy) e. S)   &   |- R = frec((x e. ( ZZ>= ` C) , y e. S |-> <.(x + 1) , (x Fy) >.) , <. C , A >.)   =>   |- ((ph /\ D e. om) -> ( R ` D) e. (( ZZ>= ` C) X. S))
27-May-2020	dffun5r 4857	A way of proving a relation is a function, analogous to mo2r 1949. (Contributed by Jim Kingdon, 27-May-2020.)
|- (( Rel A /\ A.xE.zA.y( <.x , y >. e. A -> y = z)) -> Fun A)
26-May-2020	frecuzrdgfn 8859	The recursive definition generator on upper integers is a function. See comment in frec2uz0d 8846 for the description of G as the mapping from om to ( ZZ>= ` C). (Contributed by Jim Kingdon, 26-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> S e. V)   &   |- (ph -> A e. S)   &   |- ((ph /\ (x e. ( ZZ>= ` C) /\ y e. S)) -> (x Fy) e. S)   &   |- R = frec((x e. ( ZZ>= ` C) , y e. S |-> <.(x + 1) , (x Fy) >.) , <. C , A >.)   &   |- (ph -> T = ran R)   =>   |- (ph -> T Fn ( ZZ>= ` C))
26-May-2020	frecuzrdglem 8858	A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 26-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> S e. V)   &   |- (ph -> A e. S)   &   |- ((ph /\ (x e. ( ZZ>= ` C) /\ y e. S)) -> (x Fy) e. S)   &   |- R = frec((x e. ( ZZ>= ` C) , y e. S |-> <.(x + 1) , (x Fy) >.) , <. C , A >.)   &   |- (ph -> B e. ( ZZ>= ` C))   =>   |- (ph -> <.B , ( 2nd ` ( R ` ( `' G ` B))) >. e. ran R)
26-May-2020	frecuzrdgrom 8857	The function R (used in the definition of the recursive definition generator on upper integers) is a function defined for all natural numbers. (Contributed by Jim Kingdon, 26-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> S e. V)   &   |- (ph -> A e. S)   &   |- ((ph /\ (x e. ( ZZ>= ` C) /\ y e. S)) -> (x Fy) e. S)   &   |- R = frec((x e. ( ZZ>= ` C) , y e. S |-> <.(x + 1) , (x Fy) >.) , <. C , A >.)   =>   |- (ph -> R Fn om)
25-May-2020	freccl 5932	Closure for finite recursion. (Contributed by Jim Kingdon, 25-May-2020.)
|- (ph -> A.z( F ` z) e. _V)   &   |- (ph -> A e. S)   &   |- ((ph /\ z e. S) -> ( F ` z) e. S)   &   |- (ph -> B e. om)   =>   |- (ph -> (frec( F , A) ` B) e. S)
24-May-2020	frec2uzrdg 8856	A helper lemma for the value of a recursive definition generator on upper integers (typically either NN or NN0) with characteristic function F(x , y) and initial value A. This lemma shows that evaluating R at an element of om gives an ordered pair whose first element is the index (translated from om to ( ZZ>= ` C)). See comment in frec2uz0d 8846 which describes G and the index translation. (Contributed by Jim Kingdon, 24-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> S e. V)   &   |- (ph -> A e. S)   &   |- ((ph /\ (x e. ( ZZ>= ` C) /\ y e. S)) -> (x Fy) e. S)   &   |- R = frec((x e. ( ZZ>= ` C) , y e. S |-> <.(x + 1) , (x Fy) >.) , <. C , A >.)   &   |- (ph -> B e. om)   =>   |- (ph -> ( R ` B) = <.( G ` B) , ( 2nd ` ( R ` B)) >.)
21-May-2020	fzofig 8869	Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.)
|- (( M e. ZZ /\ N e. ZZ) -> ( M..^ N) e. Fin)
21-May-2020	fzfigd 8868	Deduction form of fzfig 8867. (Contributed by Jim Kingdon, 21-May-2020.)
|- (ph -> M e. ZZ)   &   |- (ph -> N e. ZZ)   =>   |- (ph -> ( M ... N) e. Fin)
19-May-2020	fzfig 8867	A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.)
|- (( M e. ZZ /\ N e. ZZ) -> ( M ... N) e. Fin)
19-May-2020	frechashgf1o 8866	G maps om one-to-one onto NN0. (Contributed by Jim Kingdon, 19-May-2020.)
|- G = frec((x e. ZZ |-> (x + 1)) , 0)   =>   |- G : om -1-1-onto-> NN0
19-May-2020	ssfiexmid 6254	If any subset of a finite set is finite, excluded middle follows. One direction of Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 19-May-2020.)
|- A.xA.y((x e. Fin /\ y C_ x) -> y e. Fin)   =>   |- (ph \/ -. ph)
19-May-2020	enm 6230	A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.)
|- ((A ~~ B /\ E.x x e. A) -> E.y y e. B)
18-May-2020	frecfzen2 8865	The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Jim Kingdon, 18-May-2020.)
|- G = frec((x e. ZZ |-> (x + 1)) , 0)   =>   |- ( N e. ( ZZ>= ` M) -> ( M ... N) ~~ ( `' G ` (( N + 1) - M)))
18-May-2020	frecfzennn 8864	The cardinality of a finite set of sequential integers. (See frec2uz0d 8846 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.)
|- G = frec((x e. ZZ |-> (x + 1)) , 0)   =>   |- ( N e. NN0 -> ( 1 ... N) ~~ ( `' G ` N))
17-May-2020	frec2uzisod 8854	G (see frec2uz0d 8846) is an isomorphism from natural ordinals to upper integers. (Contributed by Jim Kingdon, 17-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   =>   |- (ph -> G Isom _E , < ( om , ( ZZ>= ` C)))
17-May-2020	frec2uzf1od 8853	G (see frec2uz0d 8846) is a one-to-one onto mapping. (Contributed by Jim Kingdon, 17-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   =>   |- (ph -> G : om -1-1-onto->( ZZ>= ` C))
17-May-2020	frec2uzrand 8852	Range of G (see frec2uz0d 8846). (Contributed by Jim Kingdon, 17-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   =>   |- (ph -> ran G = ( ZZ>= ` C))
16-May-2020	frec2uzlt2d 8851	The mapping G (see frec2uz0d 8846) preserves order. (Contributed by Jim Kingdon, 16-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> A e. om)   &   |- (ph -> B e. om)   =>   |- (ph -> (A e. B <-> ( G ` A) < ( G ` B)))
16-May-2020	frec2uzltd 8850	Less-than relation for G (see frec2uz0d 8846). (Contributed by Jim Kingdon, 16-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> A e. om)   &   |- (ph -> B e. om)   =>   |- (ph -> (A e. B -> ( G ` A) < ( G ` B)))
16-May-2020	frec2uzuzd 8849	The value G (see frec2uz0d 8846) at an ordinal natural number is in the upper integers. (Contributed by Jim Kingdon, 16-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> A e. om)   =>   |- (ph -> ( G ` A) e. ( ZZ>= ` C))
16-May-2020	frec2uzsucd 8848	The value of G (see frec2uz0d 8846) at a successor. (Contributed by Jim Kingdon, 16-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> A e. om)   =>   |- (ph -> ( G ` suc A) = (( G ` A) + 1))
16-May-2020	frec2uzzd 8847	The value of G (see frec2uz0d 8846) is an integer. (Contributed by Jim Kingdon, 16-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   &   |- (ph -> A e. om)   =>   |- (ph -> ( G ` A) e. ZZ)
16-May-2020	frec2uz0d 8846	The mapping G is a one-to-one mapping from om onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number C (normally 0 for the upper integers NN0 or 1 for the upper integers NN), 1 maps to C + 1, etc. This theorem shows the value of G at ordinal natural number zero. (Contributed by Jim Kingdon, 16-May-2020.)
|- (ph -> C e. ZZ)   &   |- G = frec((x e. ZZ |-> (x + 1)) , C)   =>   |- (ph -> ( G ` (/)) = C)
15-May-2020	nntri3 6014	A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.)
|- ((A e. om /\ B e. om) -> (A = B <-> (-. A e. B /\ -. B e. A)))
14-May-2020	rdgifnon2 5907	The recursive definition generator is a function on ordinal numbers. (Contributed by Jim Kingdon, 14-May-2020.)
|- ((A.z( F ` z) e. _V /\ A e. V) -> rec( F , A) Fn On)
14-May-2020	rdgtfr 5901	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.)
|- ((A.z( F ` z) e. _V /\ A e. V) -> ( Fun (g e. _V |-> (A u. U_x e. dom g( F ` (g ` x)))) /\ ((g e. _V |-> (A u. U_x e. dom g( F ` (g ` x)))) ` f) e. _V))
13-May-2020	frecfnom 5925	The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.)
|- ((A.z( F ` z) e. _V /\ A e. V) -> frec( F , A) Fn om)
13-May-2020	frecabex 5923	The class abstraction from df-frec 5918 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.)
|- (ph -> S e. V)   &   |- (ph -> A.y( F ` y) e. _V)   &   |- (ph -> A e. W)   =>   |- (ph -> {x | (E. m e. om ( dom S = suc m /\ x e. ( F ` ( S ` m))) \/ ( dom S = (/) /\ x e. A)) } e. _V)
8-May-2020	tfr0 5878	Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.)
|- F = recs( G)   =>   |- (( G ` (/)) e. V -> ( F ` (/)) = ( G ` (/)))
7-May-2020	frec0g 5922	The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.)
|- (A e. V -> (frec( F , A) ` (/)) = A)
3-May-2020	dcned 2209	Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
|- (ph -> DECID A = B)   =>   |- (ph -> DECID A =/= B)
2-May-2020	ax-arch 6782	Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by theorem axarch 6753. This axiom should not be used directly; instead use arch 7934 (which is the same, but stated in terms of NN and <). (Contributed by Jim Kingdon, 2-May-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)
30-Apr-2020	ltexnqi 6392	Ordering on positive fractions in terms of existence of sum. (Contributed by Jim Kingdon, 30-Apr-2020.)
|- (A <Q B -> E.x e. Q. (A +Q x) = B)
26-Apr-2020	pitonnlem1p1 6722	Lemma for pitonn 6724. 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 )
26-Apr-2020	addnqpr1 6542	Addition of one to a fraction embedded into a positive real. One can either add the fraction one to the fraction, or the positive real one to the positive real, and get the same result. Special case of addnqpr 6541. (Contributed by Jim Kingdon, 26-Apr-2020.)
|- (A e. Q. -> <. { l | l <Q (A +Q 1Q) } , {u | (A +Q 1Q) <Q u } >. = ( <. { l | l <Q A } , {u | A <Q u } >. +P. 1P))
26-Apr-2020	addpinq1 6446	Addition of one to the numerator of a fraction whose denominator is one. (Contributed by Jim Kingdon, 26-Apr-2020.)
|- (A e. N. -> [ <.(A +N 1o) , 1o >.] ~Q = ([ <.A , 1o >.] ~Q +Q 1Q))
26-Apr-2020	nnnq 6405	The canonical embedding of positive integers into positive fractions. (Contributed by Jim Kingdon, 26-Apr-2020.)
|- (A e. N. -> [ <.A , 1o >.] ~Q e. Q.)
24-Apr-2020	pitonnlem2 6723	Lemma for pitonn 6724. 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 >.)
24-Apr-2020	pitonnlem1 6721	Lemma for pitonn 6724. 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
23-Apr-2020	archsr 6688	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 )
23-Apr-2020	nnprlu 6533	The canonical embedding of positive integers into the positive reals. (Contributed by Jim Kingdon, 23-Apr-2020.)
|- (A e. N. -> <. { l | l <Q [ <.A , 1o >.] ~Q } , {u | [ <.A , 1o >.] ~Q <Q u } >. e. P.)
22-Apr-2020	axarch 6753	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 7677 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 6782. (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)
22-Apr-2020	pitonn 6724	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) })
22-Apr-2020	archpr 6614	For any positive real, there is an integer that is greater than it. This is also known as the "archimedean property". The integer x is embedded into the reals as described at nnprlu 6533. (Contributed by Jim Kingdon, 22-Apr-2020.)
|- (A e. P. -> E.x e. N. A <P <. { l | l <Q [ <.x , 1o >.] ~Q } , {u | [ <.x , 1o >.] ~Q <Q u } >.)
20-Apr-2020	fzo0m 8797	A half-open integer range based at 0 is inhabited precisely if the upper bound is a positive integer. (Contributed by Jim Kingdon, 20-Apr-2020.)
|- (E.x x e. ( 0..^A) <-> A e. NN)
20-Apr-2020	fzom 8770	A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.)
|- (E.x x e. ( M..^ N) <-> M e. ( M..^ N))
18-Apr-2020	eluzdc 8303	Membership of an integer in an upper set of integers is decidable. (Contributed by Jim Kingdon, 18-Apr-2020.)
|- (( M e. ZZ /\ N e. ZZ) -> DECID N e. ( ZZ>= ` M))
17-Apr-2020	zlelttric 8046	Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
|- ((A e. ZZ /\ B e. ZZ) -> (A <_ B \/ B < A))
16-Apr-2020	fznlem 8655	A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.)
|- (( M e. ZZ /\ N e. ZZ) -> ( N < M -> ( M ... N) = (/)))
15-Apr-2020	fzm 8652	Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.)
|- (E.x x e. ( M ... N) <-> N e. ( ZZ>= ` M))
15-Apr-2020	xpdom3m 6244	A set is dominated by its Cartesian product with an inhabited set. Exercise 6 of [Suppes] p. 98. (Contributed by Jim Kingdon, 15-Apr-2020.)
|- ((A e. V /\ B e. W /\ E.x x e. B) -> A ~<_ (A X. B))
13-Apr-2020	snfig 6227	A singleton is finite. (Contributed by Jim Kingdon, 13-Apr-2020.)
|- (A e. V -> {A } e. Fin)
13-Apr-2020	en1bg 6216	A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.)
|- (A e. V -> (A ~~ 1o <-> A = { U.A }))
10-Apr-2020	negm 8306	The image under negation of an inhabited set of reals is inhabited. (Contributed by Jim Kingdon, 10-Apr-2020.)
|- ((A C_ RR /\ E.x x e. A) -> E.y y e. {z e. RR | -uz e. A })
8-Apr-2020	zleloe 8048	Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
|- ((A e. ZZ /\ B e. ZZ) -> (A <_ B <-> (A < B \/ A = B)))
7-Apr-2020	zdcle 8073	Integer <_ is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
|- ((A e. ZZ /\ B e. ZZ) -> DECID A <_ B)
4-Apr-2020	ioorebasg 8594	Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.)
|- ((A e. RR* /\ B e. RR*) -> (A (,)B) e. ran (,))
30-Mar-2020	icc0r 8545	An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.)
|- ((A e. RR* /\ B e. RR*) -> (B < A -> (A [,]B) = (/)))
30-Mar-2020	ubioog 8533	An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
|- ((A e. RR* /\ B e. RR*) -> -. B e. (A (,)B))
30-Mar-2020	lbioog 8532	An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
|- ((A e. RR* /\ B e. RR*) -> -. A e. (A (,)B))
29-Mar-2020	iooidg 8528	An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
|- (A e. RR* -> (A (,)A) = (/))
27-Mar-2020	zletric 8045	Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
|- ((A e. ZZ /\ B e. ZZ) -> (A <_ B \/ B <_ A))
26-Mar-2020	4z 8031	4 is an integer. (Contributed by BJ, 26-Mar-2020.)
|- 4 e. ZZ
25-Mar-2020	elfzmlbm 8738	Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- ( K e. ( M ... N) -> ( K - M) e. ( 0 ...( N - M)))
25-Mar-2020	elfz0add 8729	An element of a finite set of sequential nonnegative integers is an element of an extended finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- ((A e. NN0 /\ B e. NN0) -> ( N e. ( 0 ...A) -> N e. ( 0 ...(A + B))))
25-Mar-2020	2eluzge0 8273	2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- 2 e. ( ZZ>= ` 0)
23-Mar-2020	rpnegap 8370	Either a real apart from zero or its negation is a positive real, but not both. (Contributed by Jim Kingdon, 23-Mar-2020.)
|- ((A e. RR /\ A # 0) -> (A e. RR+ \/_ -uA e. RR+))
23-Mar-2020	reapltxor 7353	Real apartness in terms of less than (exclusive-or version). (Contributed by Jim Kingdon, 23-Mar-2020.)
|- ((A e. RR /\ B e. RR) -> (A # B <-> (A < B \/_ B < A)))
22-Mar-2020	rpcnap0 8358	A positive real is a complex number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- (A e. RR+ -> (A e. CC /\ A # 0))
22-Mar-2020	rpreap0 8356	A positive real is a real number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- (A e. RR+ -> (A e. RR /\ A # 0))
22-Mar-2020	rpap0 8354	A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- (A e. RR+ -> A # 0)
20-Mar-2020	qapne 8330	Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 20-Mar-2020.)
|- ((A e. QQ /\ B e. QQ) -> (A # B <-> A =/= B))
20-Mar-2020	divap1d 7538	If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> A # B)   =>   |- (ph -> (A / B) # 1)
20-Mar-2020	apmul1 7526	Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.)
|- ((A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0)) -> (A # B <-> (A x. C) # (B x. C)))
19-Mar-2020	divfnzn 8312	Division restricted to ZZ X. NN is a function. Given excluded middle, it would be easy to prove this for CC X. ( CC \ { 0 }). The key difference is that an element of NN is apart from zero, whereas being an element of CC \ { 0 } implies being not equal to zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( / |` ( ZZ X. NN)) Fn ( ZZ X. NN)
19-Mar-2020	div2negapd 7542	Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ( -uA / -uB) = (A / B))
19-Mar-2020	divneg2apd 7541	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> -u(A / B) = (A / -uB))
19-Mar-2020	divnegapd 7540	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> -u(A / B) = ( -uA / B))
19-Mar-2020	divap0bd 7539	A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> (A # 0 <-> (A / B) # 0))
19-Mar-2020	diveqap0ad 7537	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 7423. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ((A / B) = 0 <-> A = 0))
19-Mar-2020	diveqap1ad 7536	The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 7444. Generalization of diveqap1d 7535. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ((A / B) = 1 <-> A = B))
19-Mar-2020	diveqap1d 7535	Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> (A / B) = 1)   =>   |- (ph -> A = B)
19-Mar-2020	diveqap0d 7534	If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> (A / B) = 0)   =>   |- (ph -> A = 0)
15-Mar-2020	nneoor 8096	A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.)
|- ( N e. NN -> (( N / 2) e. NN \/ (( N + 1) / 2) e. NN))
14-Mar-2020	zltlen 8075	Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7393 which is a similar result for complex numbers. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ((A e. ZZ /\ B e. ZZ) -> (A < B <-> (A <_ B /\ B =/= A)))
14-Mar-2020	zdceq 8072	Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ((A e. ZZ /\ B e. ZZ) -> DECID A = B)
14-Mar-2020	zapne 8071	Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- (( M e. ZZ /\ N e. ZZ) -> ( M # N <-> M =/= N))
14-Mar-2020	zltnle 8047	'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ((A e. ZZ /\ B e. ZZ) -> (A < B <-> -. B <_ A))
14-Mar-2020	ztri3or 8044	Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- (( M e. ZZ /\ N e. ZZ) -> ( M < N \/ M = N \/ N < M))
14-Mar-2020	ztri3or0 8043	Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ( N e. ZZ -> ( N < 0 \/ N = 0 \/ 0 < N))
14-Mar-2020	zaddcllemneg 8040	Lemma for zaddcl 8041. Special case in which -u N is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- (( M e. ZZ /\ N e. RR /\ -u N e. NN) -> ( M + N) e. ZZ)
14-Mar-2020	zaddcllempos 8038	Lemma for zaddcl 8041. Special case in which N is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- (( M e. ZZ /\ N e. NN) -> ( M + N) e. ZZ)
14-Mar-2020	dcne 2211	Decidable equality expressed in terms of =/=. Basically the same as df-dc 742. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- (DECID A = B <-> (A = B \/ A =/= B))
9-Mar-2020	2muliap0 7906	2 x. _i is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- ( 2 x. _i) # 0
9-Mar-2020	iap0 7905	The imaginary unit _i is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- _i # 0
9-Mar-2020	2ap0 7769	The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 2 # 0
9-Mar-2020	1ne0 7743	1 =/= 0. See aso 1ap0 7354. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- 1 =/= 0
9-Mar-2020	redivclapi 7517	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   &   |- B e. RR   &   |- B # 0   =>   |- (A / B) e. RR
9-Mar-2020	redivclapzi 7516	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   &   |- B e. RR   =>   |- (B # 0 -> (A / B) e. RR)
9-Mar-2020	rerecclapi 7515	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   &   |- A # 0   =>   |- ( 1 / A) e. RR
9-Mar-2020	rerecclapzi 7514	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   =>   |- (A # 0 -> ( 1 / A) e. RR)
9-Mar-2020	divdivdivapi 7513	Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B # 0   &   |- D # 0   &   |- C # 0   =>   |- ((A / B) / ( C / D)) = ((A x. D) / (B x. C))
9-Mar-2020	divadddivapi 7512	Addition of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B # 0   &   |- D # 0   =>   |- ((A / B) + ( C / D)) = (((A x. D) + ( C x. B)) / (B x. D))
9-Mar-2020	divmul13api 7511	Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B # 0   &   |- D # 0   =>   |- ((A / B) x. ( C / D)) = (( C / B) x. (A / D))
9-Mar-2020	divmuldivapi 7510	Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B # 0   &   |- D # 0   =>   |- ((A / B) x. ( C / D)) = ((A x. C) / (B x. D))
9-Mar-2020	div11api 7509	One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C # 0   =>   |- ((A / C) = (B / C) <-> A = B)
9-Mar-2020	div23api 7508	A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C # 0   =>   |- ((A x. B) / C) = ((A / C) x. B)
9-Mar-2020	divdirapi 7507	Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C # 0   =>   |- ((A + B) / C) = ((A / C) + (B / C))
9-Mar-2020	divassapi 7506	An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C # 0   =>   |- ((A x. B) / C) = (A x. (B / C))
8-Mar-2020	nnap0 7704	A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (A e. NN -> A # 0)
8-Mar-2020	divdivap2d 7559	Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> C # 0)   =>   |- (ph -> (A / (B / C)) = ((A x. C) / B))
8-Mar-2020	divdivap1d 7558	Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A / B) / C) = (A / (B x. C)))
8-Mar-2020	dmdcanap2d 7557	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A / B) x. (B / C)) = (A / C))
8-Mar-2020	dmdcanapd 7556	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> C # 0)   =>   |- (ph -> ((B / C) x. (A / B)) = (A / C))
8-Mar-2020	divcanap7d 7555	Cancel equal divisors in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A / C) / (B / C)) = (A / B))
8-Mar-2020	divcanap5rd 7554	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A x. C) / (B x. C)) = (A / B))
8-Mar-2020	divcanap5d 7553	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> C # 0)   =>   |- (ph -> (( C x. A) / ( C x. B)) = (A / B))
8-Mar-2020	divdiv32apd 7552	Swap denominators in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A / B) / C) = ((A / C) / B))
8-Mar-2020	div13apd 7551	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ((A / B) x. C) = (( C / B) x. A))
8-Mar-2020	div32apd 7550	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ((A / B) x. C) = (A x. ( C / B)))
8-Mar-2020	divmulapd 7549	Relationship between division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ((A / B) = C <-> (B x. C) = A))
7-Mar-2020	nn1gt1 7708	A positive integer is either one or greater than one. This is for NN; 0elnn 4283 is a similar theorem for om (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.)
|- (A e. NN -> (A = 1 \/ 1 < A))
5-Mar-2020	crap0 7671	The real representation of complex numbers is apart from zero iff one of its terms is apart from zero. (Contributed by Jim Kingdon, 5-Mar-2020.)
|- ((A e. RR /\ B e. RR) -> ((A # 0 \/ B # 0) <-> (A + ( _i x. B)) # 0))
3-Mar-2020	rec11apd 7548	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> B # 0)   &   |- (ph -> ( 1 / A) = ( 1 / B))   =>   |- (ph -> A = B)
3-Mar-2020	ddcanapd 7547	Cancellation in a double division. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> B # 0)   =>   |- (ph -> (A / (A / B)) = B)
3-Mar-2020	divcanap6d 7546	Cancellation of inverted fractions. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> B # 0)   =>   |- (ph -> ((A / B) x. (B / A)) = 1)
3-Mar-2020	recdivap2d 7545	Division into a reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> B # 0)   =>   |- (ph -> (( 1 / A) / B) = ( 1 / (A x. B)))
3-Mar-2020	recdivapd 7544	The reciprocal of a ratio. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> B # 0)   =>   |- (ph -> ( 1 / (A / B)) = (B / A))
3-Mar-2020	divap0d 7543	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> A # 0)   &   |- (ph -> B # 0)   =>   |- (ph -> (A / B) # 0)
3-Mar-2020	div0apd 7525	Division into zero is zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> ( 0 / A) = 0)
3-Mar-2020	dividapd 7524	A number divided by itself is one. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> (A / A) = 1)
3-Mar-2020	recrecapd 7523	A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> ( 1 / ( 1 / A)) = A)
3-Mar-2020	recidap2d 7522	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> (( 1 / A) x. A) = 1)
3-Mar-2020	recidapd 7521	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> (A x. ( 1 / A)) = 1)
3-Mar-2020	recap0d 7520	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> ( 1 / A) # 0)
3-Mar-2020	recclapd 7519	Closure law for reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> ( 1 / A) e. CC)
2-Mar-2020	div11apd 7567	One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> C # 0)   &   |- (ph -> (A / C) = (B / C))   =>   |- (ph -> A = B)
2-Mar-2020	divsubdirapd 7566	Distribution of division over subtraction. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A - B) / C) = ((A / C) - (B / C)))
2-Mar-2020	divdirapd 7565	Distribution of division over addition. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A + B) / C) = ((A / C) + (B / C)))
2-Mar-2020	div23apd 7564	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A x. B) / C) = ((A / C) x. B))
2-Mar-2020	div12apd 7563	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> C # 0)   =>   |- (ph -> (A x. (B / C)) = (B x. (A / C)))
2-Mar-2020	divassapd 7562	An associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A x. B) / C) = (A x. (B / C)))
2-Mar-2020	divmulap3d 7561	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A / C) = B <-> A = (B x. C)))
2-Mar-2020	divmulap2d 7560	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> C e. CC)   &   |- (ph -> C # 0)   =>   |- (ph -> ((A / C) = B <-> A = ( C x. B)))
29-Feb-2020	prodgt0gt0 7578	Infer that a multiplicand is positive from a positive multiplier and positive product. See prodgt0 7579 for the same theorem with 0 < A replaced by the weaker condition 0 <_ A. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (((A e. RR /\ B e. RR) /\ ( 0 < A /\ 0 < (A x. B))) -> 0 < B)
29-Feb-2020	redivclapd 7569	Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. RR)   &   |- (ph -> B e. RR)   &   |- (ph -> B # 0)   =>   |- (ph -> (A / B) e. RR)
29-Feb-2020	rerecclapd 7568	Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. RR)   &   |- (ph -> A # 0)   =>   |- (ph -> ( 1 / A) e. RR)
29-Feb-2020	divcanap4d 7533	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ((A x. B) / B) = A)
29-Feb-2020	divcanap3d 7532	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ((B x. A) / B) = A)
29-Feb-2020	divrecap2d 7531	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> (A / B) = (( 1 / B) x. A))
29-Feb-2020	divrecapd 7530	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> (A / B) = (A x. ( 1 / B)))
29-Feb-2020	divcanap2d 7529	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> (B x. (A / B)) = A)
29-Feb-2020	divcanap1d 7528	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ((A / B) x. B) = A)
29-Feb-2020	divclapd 7527	Closure law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> (A / B) e. CC)
29-Feb-2020	divdiv32api 7505	Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- A e. CC   &   |- B e.