Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100

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.

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 24-Sep-2020 at 4:02 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
26-Aug-2020sqrt0rlem 9192 Lemma for sqrt0 9193. (Contributed by Jim Kingdon, 26-Aug-2020.)
 RR 
 ^ 2  0  0  <_  0
 
23-Aug-2020sqrtrval 9189 Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
 RR  sqr `  iota_  RR  ^
 2  0  <_
 
23-Aug-2020df-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  RR  |->  iota_ 
 RR 
 ^ 2  0  <_
 
19-Aug-2020addnqpr 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.)
 Q.  Q.  <. { l  |  l  <Q  +Q  } ,  {  |  +Q  <Q  } >.  <. { l  |  l 
 <Q  } ,  {  |  <Q  } >.  +P.  <. { l  |  l  <Q  } ,  {  |  <Q  } >.
 
19-Aug-2020addnqprlemfu 6540 Lemma for addnqpr 6541. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
 Q.  Q.  2nd `  <. { l  |  l  <Q 
 +Q  } ,  {  |  +Q 
 <Q  } >.  C_  2nd `  <. { l  |  l  <Q  } ,  {  |  <Q  } >.  +P.  <. { l  |  l  <Q  } ,  {  |  <Q  } >.
 
19-Aug-2020addnqprlemfl 6539 Lemma for addnqpr 6541. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
 Q.  Q.  1st `  <. { l  |  l  <Q 
 +Q  } ,  {  |  +Q 
 <Q  } >.  C_  1st `  <. { l  |  l  <Q  } ,  {  |  <Q  } >.  +P.  <. { l  |  l  <Q  } ,  {  |  <Q  } >.
 
19-Aug-2020addnqprlemru 6538 Lemma for addnqpr 6541. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
 Q.  Q.  2nd `  <. { l  |  l 
 <Q  } ,  {  |  <Q  } >.  +P.  <. { l  |  l  <Q  } ,  {  |  <Q  } >.  C_  2nd `  <. { l  |  l  <Q 
 +Q  } ,  {  |  +Q 
 <Q  } >.
 
19-Aug-2020addnqprlemrl 6537 Lemma for addnqpr 6541. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
 Q.  Q.  1st `  <. { l  |  l 
 <Q  } ,  {  |  <Q  } >.  +P.  <. { l  |  l  <Q  } ,  {  |  <Q  } >.  C_  1st `  <. { l  |  l  <Q 
 +Q  } ,  {  |  +Q 
 <Q  } >.
 
15-Aug-2020cauappcvgprlemcan 6615 Lemma for cauappcvgprlemladdrl 6628. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.)
 L  P.   &     S  Q.   &     R  Q.   &     Q  Q.   =>     R  +Q  Q  1st `  L  +P.  <. { l  |  l  <Q  S  +Q  Q } ,  {  |  S  +Q  Q  <Q  } >.  R  1st `  L  +P.  <. { l  |  l  <Q  S } ,  {  |  S  <Q  } >.
 
4-Aug-2020cauappcvgprlemupu 6620 Lemma for cauappcvgpr 6633. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   =>     s  <Q  r  s  2nd `  L  r  2nd `  L
 
4-Aug-2020cauappcvgprlemopu 6619 Lemma for cauappcvgpr 6633. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   =>     r  2nd `  L  s  Q.  s  <Q  r  s  2nd `  L
 
4-Aug-2020cauappcvgprlemlol 6618 Lemma for cauappcvgpr 6633. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   =>     s  <Q  r  r  1st `  L  s  1st `  L
 
4-Aug-2020cauappcvgprlemopl 6617 Lemma for cauappcvgpr 6633. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   =>     s  1st `  L  r  Q.  s  <Q  r  r  1st `  L
 
18-Jul-2020cauappcvgprlemloc 6623 Lemma for cauappcvgpr 6633. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   =>     s  Q.  r  Q.  s  <Q  r  s  1st `  L  r  2nd `  L
 
18-Jul-2020cauappcvgprlemdisj 6622 Lemma for cauappcvgpr 6633. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   =>     s  Q.  s  1st `  L  s  2nd `  L
 
18-Jul-2020cauappcvgprlemrnd 6621 Lemma for cauappcvgpr 6633. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   =>     s  Q.  s  1st `  L  r  Q.  s  <Q  r  r  1st `  L  r  Q.  r  2nd `  L  s  Q.  s  <Q  r  s  2nd `  L
 
18-Jul-2020cauappcvgprlemm 6616 Lemma for cauappcvgpr 6633. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   =>     s  Q.  s  1st `  L  r  Q.  r  2nd `  L
 
11-Jul-2020cauappcvgprlemladdrl 6628 Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   &     S  Q.   =>     1st `  <. { l 
 Q.  |  q  Q.  l  +Q  q  <Q  F `  q 
 +Q  S } ,  {  Q.  |  q  Q.  F `  q  +Q  q  +Q  S  <Q  } >.  C_  1st `  L  +P.  <. { l  |  l  <Q  S } ,  {  |  S  <Q  } >.
 
11-Jul-2020cauappcvgprlemladdru 6627 Lemma for cauappcvgprlemladd 6629. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   &     S  Q.   =>     2nd `  <. { l 
 Q.  |  q  Q.  l  +Q  q  <Q  F `  q 
 +Q  S } ,  {  Q.  |  q  Q.  F `  q  +Q  q  +Q  S  <Q  } >.  C_  2nd `  L  +P.  <. { l  |  l  <Q  S } ,  {  |  S  <Q  } >.
 
11-Jul-2020cauappcvgprlemladdfl 6626 Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   &     S  Q.   =>     1st `  L  +P.  <. { l  |  l  <Q  S } ,  {  |  S  <Q  } >.  C_  1st `  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `  q 
 +Q  S } ,  {  Q.  |  q  Q.  F `  q  +Q  q  +Q  S  <Q  } >.
 
11-Jul-2020cauappcvgprlemladdfu 6625 Lemma for cauappcvgprlemladd 6629. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   &     S  Q.   =>     2nd `  L  +P.  <. { l  |  l  <Q  S } ,  {  |  S  <Q  } >.  C_  2nd `  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `  q 
 +Q  S } ,  {  Q.  |  q  Q.  F `  q  +Q  q  +Q  S  <Q  } >.
 
8-Jul-2020nqprl 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.)
 Q.  P.  1st `  <. { l  |  l  <Q  } ,  {  |  <Q  } >.  <P
 
24-Jun-2020nqprlu 6529 The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.)
 Q.  <. { l  |  l  <Q  } ,  {  |  <Q  } >.  P.
 
23-Jun-2020cauappcvgprlem2 6631 Lemma for cauappcvgpr 6633. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   &     Q  Q.   &     R  Q.   =>     L  <P 
 <. { l  |  l 
 <Q  F `  Q  +Q  Q  +Q  R } ,  {  |  F `  Q  +Q  Q  +Q  R 
 <Q  } >.
 
23-Jun-2020cauappcvgprlem1 6630 Lemma for cauappcvgpr 6633. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   &     Q  Q.   &     R  Q.   =>     <. { l  |  l  <Q  F `  Q } ,  {  |  F `  Q  <Q  } >.  <P  L  +P.  <. { l  |  l  <Q  Q  +Q  R } ,  {  |  Q  +Q  R 
 <Q  } >.
 
23-Jun-2020cauappcvgprlemladd 6629 Lemma for cauappcvgpr 6633. This takes  L and offsets it by the positive fraction  S. (Contributed by Jim Kingdon, 23-Jun-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   &     S  Q.   =>     L  +P.  <. { l  |  l  <Q  S } ,  {  |  S  <Q  } >. 
 <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q  +Q  S } ,  {  Q.  |  q  Q.  F `  q  +Q  q  +Q  S  <Q  } >.
 
20-Jun-2020cauappcvgprlemlim 6632 Lemma for cauappcvgpr 6633. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   =>     q  Q.  r  Q.  <. { l  |  l  <Q  F `
  q } ,  {  |  F `  q 
 <Q  } >.  <P  L 
 +P.  <. { l  |  l  <Q  q  +Q  r } ,  {  |  q  +Q  r  <Q  } >.  L  <P 
 <. { l  |  l 
 <Q  F `  q  +Q  q  +Q  r } ,  {  |  F `  q  +Q  q  +Q  r 
 <Q  } >.
 
20-Jun-2020cauappcvgprlemcl 6624 Lemma for cauappcvgpr 6633. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   &     L  <. { l  Q.  |  q  Q.  l  +Q  q  <Q  F `
  q } ,  {  Q.  |  q  Q.  F `  q  +Q  q  <Q  } >.   =>     L  P.
 
19-Jun-2020cauappcvgpr 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 , 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.)
 F : Q. --> Q.   &     p  Q.  q  Q.  F `
  p  <Q  F `  q  +Q  p  +Q  q  F `  q  <Q  F `  p  +Q  p  +Q  q   &     p  Q.  <Q  F `
  p   =>     P.  q 
 Q.  r  Q.  <. { l  |  l  <Q  F `  q } ,  {  |  F `  q  <Q  } >.  <P 
 +P.  <. { l  |  l  <Q  q  +Q  r } ,  {  |  q  +Q  r  <Q  } >.  <P 
 <. { l  |  l 
 <Q  F `  q  +Q  q  +Q  r } ,  {  |  F `  q  +Q  q  +Q  r 
 <Q  } >.
 
15-Jun-2020imdivapd 9182 Imaginary part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.)
 RR   &     CC   &    #  0   =>     Im `  Im `
 
15-Jun-2020redivapd 9181 Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 15-Jun-2020.)
 RR   &     CC   &    #  0   =>     Re `  Re `
 
15-Jun-2020cjdivapd 9175 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.)
 CC   &     CC   &    #  0   =>     * `  * `  * `
 
15-Jun-2020riotaexg 5415 Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.)
 V  iota_  _V
 
14-Jun-2020cjdivapi 9143 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC   &     CC   =>    #  0  * `  * `  * `
 
14-Jun-2020cjdivap 9117 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC  CC #  0  * `  * `  * `
 
14-Jun-2020cjap0 9115 A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC #  0  * `
 #  0
 
14-Jun-2020cjap 9114 Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC  CC  * `
 #  * ` #
 
14-Jun-2020imdivap 9089 Imaginary part of a division. Related to immul2 9088. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC  RR #  0  Im `  Im `
 
14-Jun-2020redivap 9082 Real part of a division. Related to remul2 9081. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC  RR #  0  Re `  Re `
 
14-Jun-2020mulreap 9072 A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC  RR #  0  RR  x. 
 RR
 
13-Jun-2020sqgt0apd 9041 The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
 RR   &    #  0   =>     0  <  ^ 2
 
13-Jun-2020reexpclzapd 9038 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
 RR   &    #  0   &     N  ZZ   =>     ^ N 
 RR
 
13-Jun-2020expdivapd 9028 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
 CC   &     CC   &    #  0   &     N  NN0   =>    
 ^ N  ^ N 
 ^ N
 
13-Jun-2020sqdivapd 9027 Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
 CC   &     CC   &    #  0   =>    
 ^ 2  ^
 2  ^ 2
 
12-Jun-2020expsubapd 9025 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   &     M  ZZ   =>     ^ M  -  N  ^ M  ^ N
 
12-Jun-2020expm1apd 9024 Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N  -  1  ^ N
 
12-Jun-2020expp1zapd 9023 Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N  +  1  ^ N  x.
 
12-Jun-2020exprecapd 9022 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     1 
 ^ N  1  ^ N
 
12-Jun-2020expnegapd 9021 Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ -u N  1  ^ N
 
12-Jun-2020expap0d 9020 Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N #  0
 
12-Jun-2020expclzapd 9019 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N 
 CC
 
12-Jun-2020sqrecapd 9018 Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   =>     1 
 ^ 2  1  ^ 2
 
12-Jun-2020sqgt0api 8972 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
 RR   =>    #  0  0  < 
 ^ 2
 
12-Jun-2020sqdivapi 8970 Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &     CC   &    #  0   =>     ^ 2 
 ^ 2  ^ 2
 
11-Jun-2020sqgt0ap 8955 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
 RR #  0  0  < 
 ^ 2
 
11-Jun-2020sqdivap 8952 Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC  CC #  0 
 ^ 2  ^
 2  ^ 2
 
11-Jun-2020expdivap 8939 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC  CC #  0  N  NN0  ^ N 
 ^ N  ^ N
 
11-Jun-2020expm1ap 8938 Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC #  0  N  ZZ  ^ N  -  1 
 ^ N
 
11-Jun-2020expp1zap 8937 Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC #  0  N  ZZ  ^ N  +  1  ^ N  x.
 
11-Jun-2020expsubap 8936 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC #  0  M  ZZ  N  ZZ  ^ M  -  N 
 ^ M  ^ N
 
11-Jun-2020expmulzap 8935 Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC #  0  M  ZZ  N  ZZ  ^ M  x.  N 
 ^ M ^ N
 
10-Jun-2020expaddzap 8933 Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  M  ZZ  N  ZZ  ^ M  +  N 
 ^ M  x.  ^ N
 
10-Jun-2020expaddzaplem 8932 Lemma for expaddzap 8933. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  M  RR  -u M  NN  N  NN0  ^ M  +  N  ^ M  x.  ^ N
 
10-Jun-2020exprecap 8930 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  N  ZZ  1  ^ N  1  ^ N
 
10-Jun-2020mulexpzap 8929 Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  CC #  0  N  ZZ  x. 
 ^ N  ^ N  x.  ^ N
 
10-Jun-2020expap0i 8921 Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  N  ZZ  ^ N #  0
 
10-Jun-2020expap0 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.)
 CC  N  NN 
 ^ N #  0 #  0
 
10-Jun-2020mvllmulapd 7570 Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC   &     CC   &    #  0   &     x.  C   =>     C
 
9-Jun-2020expclzap 8914 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.)
 CC #  0  N  ZZ  ^ N  CC
 
9-Jun-2020expclzaplem 8913 Closure law for integer exponentiation. Lemma for expclzap 8914 and expap0i 8921. (Contributed by Jim Kingdon, 9-Jun-2020.)
 CC #  0  N  ZZ  ^ N  { 
 CC  | #  0 }
 
9-Jun-2020reexpclzap 8909 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.)
 RR #  0  N  ZZ  ^ N  RR
 
9-Jun-2020neg1ap0 7784 -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.)
 -u 1 #  0
 
8-Jun-2020expcl2lemap 8901 Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.)
 F  C_  CC   &     F  F  x.  F   &     1  F   &     F #  0  1  F   =>     F #  0  ZZ  ^  F
 
8-Jun-2020expn1ap0 8899 A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.)
 CC #  0  ^ -u 1  1
 
8-Jun-2020expineg2 8898 Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.)
 CC #  0  N  CC  -u N  NN0  ^ N  1  ^ -u N
 
8-Jun-2020expnegap0 8897 Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.)
 CC #  0  N  NN0  ^ -u N  1  ^ N
 
8-Jun-2020expinnval 8892 Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.)
 CC  N  NN  ^ N  seq 1  x.  ,  NN  X.  { } ,  CC `  N
 
7-Jun-2020expival 8891 Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.)
 CC  N  ZZ #  0  0  <_  N  ^ N  if N  0 ,  1 ,  if 0  <  N ,  seq 1  x.  ,  NN  X.  { } ,  CC `  N ,  1  seq 1  x.  ,  NN  X.  { } ,  CC `  -u N
 
7-Jun-2020expivallem 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.)
 CC #  0  N  NN  seq 1  x.  ,  NN 
 X.  { } ,  CC `  N #  0
 
7-Jun-2020df-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  0 ,  <  0 gives the value  1  0, so we will avoid this case in our theorems. (Contributed by Jim Kingodon, 7-Jun-2020.)

 ^  CC ,  ZZ  |->  if  0 ,  1 ,  if 0  <  ,  seq 1  x.  ,  NN  X.  { } ,  CC `  , 
 1  seq 1  x.  ,  NN  X.  { } ,  CC `  -u
 
4-Jun-2020iseqfveq 8887 Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.)
 N  ZZ>= `  M   &     k  M ... N  F `
  k  G `  k   &     S  V   &     ZZ>= `  M  F `  S   &     ZZ>= `  M  G `  S   &     S  S  .+  S   =>     seq M  .+  ,  F ,  S `  N 
 seq M  .+  ,  G ,  S
 `  N
 
3-Jun-2020iseqfeq2 8886 Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
 K  ZZ>= `  M   &     seq M  .+  ,  F ,  S `  K  G `  K   &     S  V   &     ZZ>= `  M  F `  S   &     ZZ>= `  K  G `  S   &     S  S  .+  S   &     k  ZZ>= `  K  +  1  F `
  k  G `  k   =>     seq M  .+  ,  F ,  S  |`  ZZ>= `  K  seq K 
 .+  ,  G ,  S
 
3-Jun-2020iseqfveq2 8885 Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.)
 K  ZZ>= `  M   &     seq M  .+  ,  F ,  S `  K  G `  K   &     S  V   &     ZZ>= `  M  F `  S   &     ZZ>= `  K  G `  S   &     S  S  .+  S   &     N  ZZ>= `  K   &     k  K  +  1 ... N  F `
  k  G `  k   =>     seq M  .+  ,  F ,  S `  N 
 seq K  .+  ,  G ,  S
 `  N
 
1-Jun-2020iseqcl 8883 Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.)
 N  ZZ>= `  M   &     S  V   &     ZZ>= `  M  F `  S   &     S  S  .+  S   =>     seq M  .+  ,  F ,  S `  N  S
 
1-Jun-2020fzdcel 8654 Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
 K  ZZ  M  ZZ  N  ZZ DECID  K  M ... N
 
1-Jun-2020fztri3or 8653 Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.)
 K  ZZ  M  ZZ  N  ZZ  K  <  M  K  M
 ... N  N  <  K
 
1-Jun-2020zdclt 8074 Integer  < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
 ZZ  ZZ DECID  <
 
31-May-2020iseqp1 8884 Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 31-May-2020.)
 N  ZZ>= `  M   &     S  V   &     ZZ>= `  M  F `  S   &     S  S  .+  S   =>     seq M  .+  ,  F ,  S `  N  +  1  seq M 
 .+  ,  F ,  S `  N 
 .+  F `  N  +  1
 
31-May-2020iseq1 8882 Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.)
 M  ZZ   &     S  V   &     ZZ>= `  M  F `  S   &     S  S  .+  S   =>     seq M  .+  ,  F ,  S `  M  F `  M
 
31-May-2020iseqovex 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.)
 ZZ>= `  M  F `  S   &     S  S  .+  S   =>     ZZ>= `  M  S  ZZ>=
 `  M ,  S  |-> 
 .+  F `  +  1  S
 
31-May-2020frecuzrdgcl 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.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     S  V   &     S   &     ZZ>= `  C  S  F  S   &     R frec  ZZ>= `  C ,  S  |->  <.  +  1 ,  F >. ,  <. C ,  >.   &     T  ran  R   =>     ZZ>= `  C  T `  S
 
30-May-2020iseqfn 8881 The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.)
 M  ZZ   &     S  V   &     ZZ>= `  M  F `  S   &     S  S  .+  S   =>     seq M  .+  ,  F ,  S  Fn  ZZ>=
 `  M
 
30-May-2020iseqval 8880 Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.)
 R frec  ZZ>= `  M ,  S  |->  <.  +  1 ,  ZZ>=
 `  M ,  S  |-> 
 .+  F `  +  1 >. ,  <. M ,  F `  M >.   &     ZZ>= `  M  F `  S   &     S  S  .+  S   =>     seq M  .+  ,  F ,  S  ran  R
 
30-May-2020nfiseq 8878 Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.)
 F/_ M   &     F/_  .+   &     F/_ F   &     F/_ S   =>     F/_  seq M 
 .+  ,  F ,  S
 
30-May-2020iseqeq4 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-2020iseqeq3 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-2020iseqeq2 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-2020iseqeq1 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-2020nffrec 5921 Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
 F/_ F   &     F/_   =>     F/_frec F ,
 
30-May-2020freceq2 5920 Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
frec F , frec F ,
 
30-May-2020freceq1 5919 Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
 F  G frec F , frec G ,
 
29-May-2020df-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  ZZ>= `  M ,  S  |->  <.  +  1 , 
 .+  F `  +  1 >. ,  <. M ,  F `
  M >.
 
28-May-2020frecuzrdgsuc 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.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     S  V   &     S   &     ZZ>= `  C  S  F  S   &     R frec  ZZ>= `  C ,  S  |->  <.  +  1 ,  F >. ,  <. C ,  >.   &     T  ran  R   =>     ZZ>= `  C  T `  +  1  F T `
 
27-May-2020frecuzrdg0 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.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     S  V   &     S   &     ZZ>= `  C  S  F  S   &     R frec  ZZ>= `  C ,  S  |->  <.  +  1 ,  F >. ,  <. C ,  >.   &     T  ran  R   =>     T `  C
 
27-May-2020frecuzrdgrrn 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.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     S  V   &     S   &     ZZ>= `  C  S  F  S   &     R frec  ZZ>= `  C ,  S  |->  <.  +  1 ,  F >. ,  <. C ,  >.   =>     D  om  R `  D  ZZ>= `  C  X.  S
 
27-May-2020dffun5r 4857 A way of proving a relation is a function, analogous to mo2r 1949. (Contributed by Jim Kingdon, 27-May-2020.)
 Rel  <. ,  >.  Fun
 
26-May-2020frecuzrdgfn 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.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     S  V   &     S   &     ZZ>= `  C  S  F  S   &     R frec  ZZ>= `  C ,  S  |->  <.  +  1 ,  F >. ,  <. C ,  >.   &     T  ran  R   =>     T  Fn  ZZ>= `  C
 
26-May-2020frecuzrdglem 8858 A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 26-May-2020.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     S  V   &     S   &     ZZ>= `  C  S  F  S   &     R frec  ZZ>= `  C ,  S  |->  <.  +  1 ,  F >. ,  <. C ,  >.   &     ZZ>= `  C   =>     <. ,  2nd `  R `  `' G ` 
 >.  ran  R
 
26-May-2020frecuzrdgrom 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.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     S  V   &     S   &     ZZ>= `  C  S  F  S   &     R frec  ZZ>= `  C ,  S  |->  <.  +  1 ,  F >. ,  <. C ,  >.   =>     R  Fn  om
 
25-May-2020freccl 5932 Closure for finite recursion. (Contributed by Jim Kingdon, 25-May-2020.)
 F `  _V   &     S   &     S  F `  S   &     om   =>    frec F , 
 `  S
 
24-May-2020frec2uzrdg 8856 A helper lemma for the value of a recursive definition generator on upper integers (typically either  NN or  NN0) with characteristic function 
F , and initial value . 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.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     S  V   &     S   &     ZZ>= `  C  S  F  S   &     R frec  ZZ>= `  C ,  S  |->  <.  +  1 ,  F >. ,  <. C ,  >.   &     om   =>     R ` 
 <. G `  ,  2nd `  R `  >.
 
21-May-2020fzofig 8869 Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.)
 M  ZZ  N  ZZ  M..^ N  Fin
 
21-May-2020fzfigd 8868 Deduction form of fzfig 8867. (Contributed by Jim Kingdon, 21-May-2020.)
 M  ZZ   &     N  ZZ   =>     M ... N 
 Fin
 
19-May-2020fzfig 8867 A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.)
 M  ZZ  N  ZZ  M ... N  Fin
 
19-May-2020frechashgf1o 8866  G maps  om one-to-one onto  NN0. (Contributed by Jim Kingdon, 19-May-2020.)
 G frec  ZZ  |->  +  1 ,  0   =>     G : om -1-1-onto-> NN0
 
19-May-2020ssfiexmid 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.)
 Fin  C_  Fin   =>   
 
19-May-2020enm 6230 A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.)
 ~~
 
18-May-2020frecfzen2 8865 The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Jim Kingdon, 18-May-2020.)
 G frec  ZZ  |->  +  1 ,  0   =>     N  ZZ>=
 `  M  M ... N 
 ~~  `' G `  N  +  1  -  M
 
18-May-2020frecfzennn 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  ZZ  |->  +  1 ,  0   =>     N  NN0  1 ... N 
 ~~  `' G `  N
 
17-May-2020frec2uzisod 8854  G (see frec2uz0d 8846) is an isomorphism from natural ordinals to upper integers. (Contributed by Jim Kingdon, 17-May-2020.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   =>     G  Isom  _E 
 ,  <  om ,  ZZ>= `  C
 
17-May-2020frec2uzf1od 8853  G (see frec2uz0d 8846) is a one-to-one onto mapping. (Contributed by Jim Kingdon, 17-May-2020.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   =>     G : om
 -1-1-onto-> ZZ>= `  C
 
17-May-2020frec2uzrand 8852 Range of  G (see frec2uz0d 8846). (Contributed by Jim Kingdon, 17-May-2020.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   =>     ran  G  ZZ>= `  C
 
16-May-2020frec2uzlt2d 8851 The mapping  G (see frec2uz0d 8846) preserves order. (Contributed by Jim Kingdon, 16-May-2020.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     om   &     om   =>     G `
  <  G `
 
16-May-2020frec2uzltd 8850 Less-than relation for  G (see frec2uz0d 8846). (Contributed by Jim Kingdon, 16-May-2020.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     om   &     om   =>     G `  <  G `
 
16-May-2020frec2uzuzd 8849 The value  G (see frec2uz0d 8846) at an ordinal natural number is in the upper integers. (Contributed by Jim Kingdon, 16-May-2020.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     om   =>     G `  ZZ>= `  C
 
16-May-2020frec2uzsucd 8848 The value of  G (see frec2uz0d 8846) at a successor. (Contributed by Jim Kingdon, 16-May-2020.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     om   =>     G `  suc  G `
  +  1
 
16-May-2020frec2uzzd 8847 The value of  G (see frec2uz0d 8846) is an integer. (Contributed by Jim Kingdon, 16-May-2020.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   &     om   =>     G ` 
 ZZ
 
16-May-2020frec2uz0d 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.)
 C  ZZ   &     G frec  ZZ  |->  +  1 ,  C   =>     G `
  (/)  C
 
15-May-2020nntri3 6014 A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.)
 om  om
 
14-May-2020rdgifnon2 5907 The recursive definition generator is a function on ordinal numbers. (Contributed by Jim Kingdon, 14-May-2020.)
 F `  _V  V  rec F ,  Fn  On
 
14-May-2020rdgtfr 5901 The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.)
 F `  _V  V  Fun  _V  |->  u.  U_  dom  F `
  ` 
 _V  |->  u.  U_  dom  F ` 
 `  `  _V
 
13-May-2020frecfnom 5925 The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.)
 F `  _V  V frec F ,  Fn  om
 
13-May-2020frecabex 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.)
 S  V   &     F `  _V   &     W   =>     {  |  m 
 om  dom  S  suc  m  F `  S `  m  dom  S  (/)  }  _V
 
8-May-2020tfr0 5878 Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.)
 F recs G   =>     G `  (/)  V  F `  (/)  G `  (/)
 
7-May-2020frec0g 5922 The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.)
 V frec F ,  `  (/)
 
3-May-2020dcned 2209 Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
DECID    =>    DECID  =/=
 
2-May-2020ax-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.)

 RR  n  |^| {  |  1  +  1  }  <RR  n
 
30-Apr-2020ltexnqi 6392 Ordering on positive fractions in terms of existence of sum. (Contributed by Jim Kingdon, 30-Apr-2020.)
 <Q  Q.  +Q
 
26-Apr-2020pitonnlem1p1 6722 Lemma for pitonn 6724. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.)
 P.  <.  +P.  1P  +P.  1P ,  1P  +P. 
 1P >.  ~R  <.  +P.  1P ,  1P >. 
 ~R
 
26-Apr-2020addnqpr1 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.)
 Q.  <. { l  |  l  <Q  +Q  1Q } ,  {  |  +Q  1Q  <Q  } >.  <. { l  |  l 
 <Q  } ,  {  |  <Q  } >.  +P.  1P
 
26-Apr-2020addpinq1 6446 Addition of one to the numerator of a fraction whose denominator is one. (Contributed by Jim Kingdon, 26-Apr-2020.)
 N.  <.  +N  1o ,  1o >. 
 ~Q  <. ,  1o >. 
 ~Q  +Q  1Q
 
26-Apr-2020nnnq 6405 The canonical embedding of positive integers into positive fractions. (Contributed by Jim Kingdon, 26-Apr-2020.)
 N.  <. ,  1o >.  ~Q  Q.
 
24-Apr-2020pitonnlem2 6723 Lemma for pitonn 6724. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.)
 K  N.  <. <. <. { l  |  l  <Q 
 <. K ,  1o >. 
 ~Q  } ,  {  |  <. K ,  1o >.  ~Q  <Q  } >.  +P.  1P ,  1P >.  ~R  ,  0R >.  +  1 
 <. <. <. { l  |  l  <Q  <. K  +N  1o ,  1o >.  ~Q  } ,  {  |  <. K  +N  1o ,  1o >.  ~Q  <Q  } >.  +P.  1P ,  1P >.  ~R  ,  0R >.
 
24-Apr-2020pitonnlem1 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  } ,  {  |  <. 1o ,  1o >.  ~Q  <Q  } >.  +P.  1P ,  1P >.  ~R  ,  0R >.  1
 
23-Apr-2020archsr 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  <. ,  1o >.  ~Q  },  {  |  <. ,  1o >.  ~Q  <Q  } >.  +P.  1P ,  1P >.  ~R is the embedding of the positive integer into the signed reals. (Contributed by Jim Kingdon, 23-Apr-2020.)
 R.  N.  <R  <. <. { l  |  l  <Q  <. ,  1o >.  ~Q  } ,  {  |  <. ,  1o >.  ~Q  <Q  } >.  +P.  1P ,  1P >.  ~R
 
23-Apr-2020nnprlu 6533 The canonical embedding of positive integers into the positive reals. (Contributed by Jim Kingdon, 23-Apr-2020.)
 N.  <. { l  |  l  <Q  <. ,  1o >.  ~Q  } ,  {  |  <. ,  1o >.  ~Q  <Q  } >.  P.
 
22-Apr-2020axarch 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.)

 RR  n  |^| {  |  1  +  1  }  <RR  n
 
22-Apr-2020pitonn 6724 Mapping from  N. to  NN. (Contributed by Jim Kingdon, 22-Apr-2020.)
 n  N.  <. <. <. { l  |  l  <Q 
 <. n ,  1o >. 
 ~Q  } ,  {  |  <. n ,  1o >.  ~Q  <Q  } >.  +P.  1P ,  1P >.  ~R  ,  0R >.  |^| {  |  1  +  1  }
 
22-Apr-2020archpr 6614 For any positive real, there is an integer that is greater than it. This is also known as the "archimedean property". The integer is embedded into the reals as described at nnprlu 6533. (Contributed by Jim Kingdon, 22-Apr-2020.)
 P.  N.  <P  <. { l  |  l  <Q  <. ,  1o >.  ~Q  } ,  {  |  <. ,  1o >.  ~Q  <Q  } >.
 
20-Apr-2020fzo0m 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.)
 0..^  NN
 
20-Apr-2020fzom 8770 A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.)
 M..^ N  M  M..^ N
 
18-Apr-2020eluzdc 8303 Membership of an integer in an upper set of integers is decidable. (Contributed by Jim Kingdon, 18-Apr-2020.)
 M  ZZ  N  ZZ DECID  N  ZZ>= `  M
 
17-Apr-2020zlelttric 8046 Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
 ZZ  ZZ  <_  <
 
16-Apr-2020fznlem 8655 A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.)
 M  ZZ  N  ZZ  N  <  M  M ... N  (/)
 
15-Apr-2020fzm 8652 Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.)
 M ... N  N  ZZ>= `  M
 
15-Apr-2020xpdom3m 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.)
 V  W  ~<_ 
 X.
 
13-Apr-2020snfig 6227 A singleton is finite. (Contributed by Jim Kingdon, 13-Apr-2020.)
 V  { }  Fin
 
13-Apr-2020en1bg 6216 A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.)
 V  ~~  1o  { U. }
 
10-Apr-2020negm 8306 The image under negation of an inhabited set of reals is inhabited. (Contributed by Jim Kingdon, 10-Apr-2020.)
 C_  RR  {  RR  |  -u  }
 
8-Apr-2020zleloe 8048 Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
 ZZ  ZZ  <_  <
 
7-Apr-2020zdcle 8073 Integer  <_ is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
 ZZ  ZZ DECID  <_
 
4-Apr-2020ioorebasg 8594 Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.)
 RR*  RR*  (,)  ran  (,)
 
30-Mar-2020icc0r 8545 An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.)
 RR*  RR*  <  [,]  (/)
 
30-Mar-2020ubioog 8533 An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
 RR*  RR*  (,)
 
30-Mar-2020lbioog 8532 An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
 RR*  RR*  (,)
 
29-Mar-2020iooidg 8528 An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
 RR*  (,)  (/)
 
27-Mar-2020zletric 8045 Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
 ZZ  ZZ  <_  <_
 
26-Mar-20204z 8031 4 is an integer. (Contributed by BJ, 26-Mar-2020.)
 4  ZZ
 
25-Mar-2020elfzmlbm 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  M ... N  K  -  M  0 ... N  -  M
 
25-Mar-2020elfz0add 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.)
 NN0  NN0  N 
 0 ... 
 N  0
 ...  +
 
25-Mar-20202eluzge0 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  ZZ>= `  0
 
23-Mar-2020rpnegap 8370 Either a real apart from zero or its negation is a positive real, but not both. (Contributed by Jim Kingdon, 23-Mar-2020.)
 RR #  0  RR+  \/_  -u  RR+
 
23-Mar-2020reapltxor 7353 Real apartness in terms of less than (exclusive-or version). (Contributed by Jim Kingdon, 23-Mar-2020.)
 RR  RR #  <  \/_ 
 <
 
22-Mar-2020rpcnap0 8358 A positive real is a complex number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
 RR+  CC #  0
 
22-Mar-2020rpreap0 8356 A positive real is a real number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
 RR+  RR #  0
 
22-Mar-2020rpap0 8354 A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
 RR+ #  0
 
20-Mar-2020qapne 8330 Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 20-Mar-2020.)
 QQ  QQ #  =/=
 
20-Mar-2020divap1d 7538 If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.)
 CC   &     CC   &    #  0   &    #    =>    #  1
 
20-Mar-2020apmul1 7526 Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.)
 CC  CC  C  CC  C #  0 #  x.  C #  x.  C
 
19-Mar-2020divfnzn 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-2020div2negapd 7542 Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.)
 CC   &     CC   &    #  0   =>     -u  -u
 
19-Mar-2020divneg2apd 7541 Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
 CC   &     CC   &    #  0   =>     -u  -u
 
19-Mar-2020divnegapd 7540 Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
 CC   &     CC   &    #  0   =>     -u  -u
 
19-Mar-2020divap0bd 7539 A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
 CC   &     CC   &    #  0   =>    #  0 #  0
 
19-Mar-2020diveqap0ad 7537 A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 7423. (Contributed by Jim Kingdon, 19-Mar-2020.)
 CC   &     CC   &    #  0   =>     0  0
 
19-Mar-2020diveqap1ad 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.)
 CC   &     CC   &    #  0   =>     1
 
19-Mar-2020diveqap1d 7535 Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.)
 CC   &     CC   &    #  0   &     1   =>   
 
19-Mar-2020diveqap0d 7534 If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
 CC   &     CC   &    #  0   &     0   =>     0
 
15-Mar-2020nneoor 8096 A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.)
 N  NN  N  2  NN  N  +  1  2  NN
 
14-Mar-2020zltlen 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.)
 ZZ  ZZ  <  <_  =/=
 
14-Mar-2020zdceq 8072 Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.)
 ZZ  ZZ DECID
 
14-Mar-2020zapne 8071 Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.)
 M  ZZ  N  ZZ  M #  N  M  =/=  N
 
14-Mar-2020zltnle 8047 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)
 ZZ  ZZ  <  <_
 
14-Mar-2020ztri3or 8044 Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
 M  ZZ  N  ZZ  M  <  N  M  N  N  <  M
 
14-Mar-2020ztri3or0 8043 Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.)
 N  ZZ  N  <  0  N  0  0  <  N
 
14-Mar-2020zaddcllemneg 8040 Lemma for zaddcl 8041. Special case in which  -u N is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
 M  ZZ  N  RR  -u N  NN  M  +  N  ZZ
 
14-Mar-2020zaddcllempos 8038 Lemma for zaddcl 8041. Special case in which  N is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
 M  ZZ  N  NN  M  +  N  ZZ
 
14-Mar-2020dcne 2211 Decidable equality expressed in terms of  =/=. Basically the same as df-dc 742. (Contributed by Jim Kingdon, 14-Mar-2020.)
DECID  =/=
 
9-Mar-20202muliap0 7906  2  x.  _i is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
 2  x.  _i #  0
 
9-Mar-2020iap0 7905 The imaginary unit  _i is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
 _i #  0
 
9-Mar-20202ap0 7769 The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.)
 2 #  0
 
9-Mar-20201ne0 7743  1  =/=  0. See aso 1ap0 7354. (Contributed by Jim Kingdon, 9-Mar-2020.)
 1  =/=  0
 
9-Mar-2020redivclapi 7517 Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
 RR   &     RR   &    #  0   =>     RR
 
9-Mar-2020redivclapzi 7516 Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
 RR   &     RR   =>    #  0  RR
 
9-Mar-2020rerecclapi 7515 Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
 RR   &    #  0   =>     1  RR
 
9-Mar-2020rerecclapzi 7514 Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
 RR   =>    #  0  1  RR
 
9-Mar-2020divdivdivapi 7513 Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
 CC   &     CC   &     C  CC   &     D  CC   &    #  0   &     D #  0   &     C #  0   =>     C  D  x.  D  x.  C
 
9-Mar-2020divadddivapi 7512 Addition of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
 CC   &     CC   &     C  CC   &     D  CC   &    #  0   &     D #  0   =>     +  C  D  x.  D  +  C  x.  x.  D
 
9-Mar-2020divmul13api 7511 Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
 CC   &     CC   &     C  CC   &     D  CC   &    #  0   &     D #  0   =>     x.  C  D  C  x.  D
 
9-Mar-2020divmuldivapi 7510 Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
 CC   &     CC   &     C  CC   &     D  CC   &    #  0   &     D #  0   =>     x.  C  D  x.  C  x.  D
 
9-Mar-2020div11api 7509 One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     C  C
 
9-Mar-2020div23api 7508 A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     x.  C  C  x.
 
9-Mar-2020divdirapi 7507 Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     +  C  C  +  C
 
9-Mar-2020divassapi 7506 An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     x.  C  x.  C
 
8-Mar-2020nnap0 7704 A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.)
 NN #  0
 
8-Mar-2020divdivap2d 7559 Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   &     C #  0   =>     C  x.  C
 
8-Mar-2020divdivap1d 7558 Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   &     C #  0   =>     C  x.  C
 
8-Mar-2020dmdcanap2d 7557 Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   &     C #  0   =>     x.  C  C
 
8-Mar-2020dmdcanapd 7556 Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   &     C #  0   =>     C  x.  C
 
8-Mar-2020divcanap7d 7555 Cancel equal divisors in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   &     C #  0   =>     C  C
 
8-Mar-2020divcanap5rd 7554 Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   &     C #  0   =>     x.  C  x.  C
 
8-Mar-2020divcanap5d 7553 Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   &     C #  0   =>     C  x.  C  x.
 
8-Mar-2020divdiv32apd 7552 Swap denominators in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   &     C #  0   =>     C  C
 
8-Mar-2020div13apd 7551 A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   =>     x.  C  C  x.
 
8-Mar-2020div32apd 7550 A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   =>     x.  C  x.  C
 
8-Mar-2020divmulapd 7549 Relationship between division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
 CC   &     CC   &     C  CC   &    #  0   =>     C  x.  C
 
7-Mar-2020nn1gt1 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.)
 NN  1  1  <
 
5-Mar-2020crap0 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.)
 RR  RR #  0 #  0  +  _i  x. #  0
 
3-Mar-2020rec11apd 7548 Reciprocal is one-to-one. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &     CC   &    #  0   &    #  0   &    
 1  1    =>   
 
3-Mar-2020ddcanapd 7547 Cancellation in a double division. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &     CC   &    #  0   &    #  0   =>   
 
3-Mar-2020divcanap6d 7546 Cancellation of inverted fractions. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &     CC   &    #  0   &    #  0   =>     x.  1
 
3-Mar-2020recdivap2d 7545 Division into a reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &     CC   &    #  0   &    #  0   =>     1  1  x.
 
3-Mar-2020recdivapd 7544 The reciprocal of a ratio. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &     CC   &    #  0   &    #  0   =>    
 1
 
3-Mar-2020divap0d 7543 The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &     CC   &    #  0   &    #  0   =>    #  0
 
3-Mar-2020div0apd 7525 Division into zero is zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &    #  0   =>    
 0  0
 
3-Mar-2020dividapd 7524 A number divided by itself is one. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &    #  0   =>     1
 
3-Mar-2020recrecapd 7523 A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &    #  0   =>    
 1  1
 
3-Mar-2020recidap2d 7522 Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &    #  0   =>     1  x.  1
 
3-Mar-2020recidapd 7521 Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &    #  0   =>     x.  1  1
 
3-Mar-2020recap0d 7520 The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &    #  0   =>    
 1 #  0
 
3-Mar-2020recclapd 7519 Closure law for reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
 CC   &    #  0   =>    
 1  CC
 
2-Mar-2020div11apd 7567 One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   &     C  C   =>   
 
2-Mar-2020divsubdirapd 7566 Distribution of division over subtraction. (Contributed by Jim Kingdon, 2-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     -  C  C  -  C
 
2-Mar-2020divdirapd 7565 Distribution of division over addition. (Contributed by Jim Kingdon, 2-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     +  C  C  +  C
 
2-Mar-2020div23apd 7564 A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     x.  C  C  x.
 
2-Mar-2020div12apd 7563 A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     x.  C  x.  C
 
2-Mar-2020divassapd 7562 An associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     x.  C  x.  C
 
2-Mar-2020divmulap3d 7561 Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     C  x.  C
 
2-Mar-2020divmulap2d 7560 Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
 CC   &     CC   &     C  CC   &     C #  0   =>     C  C  x.
 
29-Feb-2020prodgt0gt0 7578 Infer that a multiplicand is positive from a positive multiplier and positive product. See prodgt0 7579 for the same theorem with  0  < replaced by the weaker condition 
0  <_ . (Contributed by Jim Kingdon, 29-Feb-2020.)
 RR  RR 
 0  <  0  <  x.  0  <
 
29-Feb-2020redivclapd 7569 Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.)
 RR   &     RR   &    #  0   =>    
 RR
 
29-Feb-2020rerecclapd 7568 Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
 RR   &    #  0   =>    
 1  RR
 
29-Feb-2020divcanap4d 7533 A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
 CC   &     CC   &    #  0   =>     x.
 
29-Feb-2020divcanap3d 7532 A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
 CC   &     CC   &    #  0   =>     x.
 
29-Feb-2020divrecap2d 7531 Relationship between division and reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
 CC   &     CC   &    #  0   =>     1  x.
 
29-Feb-2020divrecapd 7530 Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Jim Kingdon, 29-Feb-2020.)
 CC   &     CC   &    #  0   =>     x. 
 1
 
29-Feb-2020divcanap2d 7529 A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
 CC   &     CC   &    #  0   =>     x.
 
29-Feb-2020divcanap1d 7528 A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
 CC   &     CC   &    #  0   =>     x.
 
29-Feb-2020divclapd 7527 Closure law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
 CC   &     CC   &    #  0   =>    
 CC
 
29-Feb-2020divdiv32api 7505 Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.)
 CC   &