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 1-Dec-2020 at 1:08 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
17-Nov-2020pm3.2 126 Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) (Proof shortened by Jia Ming, 17-Nov-2020.)
 
27-Oct-2020bj-omssonALT 9423 Alternate proof of bj-omsson 9422. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
 om  C_ 
 On
 
27-Oct-2020bj-omsson 9422 Constructive proof of omsson 4278. See also bj-omssonALT 9423. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.
 om  C_ 
 On
 
27-Oct-2020bj-nnelon 9419 A natural number is an ordinal. Constructive proof of nnon 4275. Can also be proved from bj-omssonALT 9423. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.)
 om  On
 
27-Oct-2020bj-nnord 9418 A natural number is an ordinal. Constructive proof of nnord 4277. Can also be proved from bj-nnelon 9419 if the latter is proved from bj-omssonALT 9423. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.)
 om  Ord
 
27-Oct-2020bj-axempty2 9349 Axiom of the empty set from bounded separation, alternate version to bj-axempty 9348. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3874 instead. (New usage is discouraged.)
 
25-Oct-2020bj-indind 9391 If is inductive and is "inductive in ", then  i^i is inductive. (Contributed by BJ, 25-Oct-2020.)
Ind  (/)  suc Ind  i^i
 
25-Oct-2020bj-axempty 9348 Axiom of the empty set from bounded separation. It is provable from bounded separation since the intuitionistic FOL used in iset.mm assumes a non-empty universe. See axnul 3873. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3874 instead. (New usage is discouraged.)
 
25-Oct-2020bj-axemptylem 9347 Lemma for bj-axempty 9348 and bj-axempty2 9349. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3874 instead. (New usage is discouraged.)
 
23-Oct-2020caucvgprlemnkj 6637 Lemma for caucvgpr 6653. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     K  N.   &     J  N.   &     S  Q.   =>     S  +Q  *Q `  <. K ,  1o >.  ~Q 
 <Q  F `  K  F `
  J  +Q  *Q `  <. J ,  1o >.  ~Q  <Q  S
 
20-Oct-2020caucvgprlemupu 6643 Lemma for caucvgpr 6653. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   =>     s  <Q  r  s  2nd `  L  r  2nd `  L
 
20-Oct-2020caucvgprlemopu 6642 Lemma for caucvgpr 6653. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   =>     r  2nd `  L  s  Q.  s  <Q  r  s  2nd `  L
 
20-Oct-2020caucvgprlemlol 6641 Lemma for caucvgpr 6653. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   =>     s  <Q  r  r  1st `  L  s  1st `  L
 
20-Oct-2020caucvgprlemopl 6640 Lemma for caucvgpr 6653. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   =>     s  1st `  L  r  Q.  s  <Q  r  r  1st `  L
 
18-Oct-2020caucvgprlemnbj 6638 Lemma for caucvgpr 6653. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     N.   &     J  N.   =>     F `  +Q  *Q `  <. ,  1o >.  ~Q 
 +Q  *Q `  <. J ,  1o >.  ~Q  <Q  F `
  J
 
9-Oct-2020caucvgprlemladdfu 6648 Lemma for caucvgpr 6653. Adding  S after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   &     S  Q.   =>     2nd `  L  +P.  <. { l  |  l  <Q  S } ,  {  |  S  <Q  } >.  C_  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q 
 +Q  S  <Q  }
 
9-Oct-2020caucvgprlemk 6636 Lemma for caucvgpr 6653. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.)
 J  <N  K   &     *Q `  <. J ,  1o >.  ~Q  <Q  Q   =>     *Q `  <. K ,  1o >.  ~Q  <Q  Q
 
8-Oct-2020caucvgprlemladdrl 6649 Lemma for caucvgpr 6653. Adding  S after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   &     S  Q.   =>     {
 l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q 
 <Q  F `  j  +Q  S }  C_  1st `  L  +P.  <. { l  |  l  <Q  S } ,  {  |  S  <Q  } >.
 
3-Oct-2020caucvgprlem2 6651 Lemma for caucvgpr 6653. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   &     Q  Q.   &     J  <N  K   &     *Q `  <. J ,  1o >.  ~Q  <Q  Q   =>     L  <P 
 <. { l  |  l 
 <Q  F `  K  +Q  Q } ,  {  |  F `  K  +Q  Q 
 <Q  } >.
 
3-Oct-2020caucvgprlem1 6650 Lemma for caucvgpr 6653. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   &     Q  Q.   &     J  <N  K   &     *Q `  <. J ,  1o >.  ~Q  <Q  Q   =>     <. { l  |  l  <Q  F `  K } ,  {  |  F `  K  <Q  } >.  <P  L  +P.  <. { l  |  l  <Q  Q } ,  {  |  Q  <Q  } >.
 
3-Oct-2020ltnnnq 6406 Ordering of positive integers via 
<N or  <Q is equivalent. (Contributed by Jim Kingdon, 3-Oct-2020.)
 N.  N.  <N  <. ,  1o >.  ~Q  <Q  <. ,  1o >.  ~Q
 
1-Oct-2020caucvgprlemlim 6652 Lemma for caucvgpr 6653. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   =>     Q.  j 
 N.  k  N.  j  <N  k  <. { l  |  l  <Q  F `  k } ,  {  |  F `  k  <Q  } >.  <P  L 
 +P.  <. { l  |  l  <Q  } ,  {  |  <Q  } >.  L  <P  <. { l  |  l  <Q  F `  k  +Q  } ,  {  |  F `  k  +Q  <Q  } >.
 
27-Sep-2020caucvgprlemloc 6646 Lemma for caucvgpr 6653. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   =>     s  Q.  r 
 Q.  s  <Q  r  s  1st `  L  r  2nd `  L
 
27-Sep-2020caucvgprlemdisj 6645 Lemma for caucvgpr 6653. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   =>     s  Q.  s  1st `  L  s  2nd `  L
 
27-Sep-2020caucvgprlemrnd 6644 Lemma for caucvgpr 6653. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~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
 
27-Sep-2020caucvgprlemm 6639 Lemma for caucvgpr 6653. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   =>     s  Q.  s  1st `  L  r 
 Q.  r  2nd `  L
 
27-Sep-2020archrecnq 6635 Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.)
 Q.  j  N.  *Q `  <. j ,  1o >.  ~Q  <Q
 
26-Sep-2020caucvgprlemcl 6647 Lemma for caucvgpr 6653. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   &     L  <. { l  Q.  |  j  N.  l  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  F `
  j } ,  {  Q.  |  j  N.  F `  j  +Q  *Q `  <. j ,  1o >.  ~Q  <Q  } >.   =>     L  P.
 
26-Aug-2020sqrt0rlem 9212 Lemma for sqrt0 9213. (Contributed by Jim Kingdon, 26-Aug-2020.)
 RR 
 ^ 2  0  0  <_  0
 
23-Aug-2020sqrtrval 9209 Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
 RR  sqr `  iota_  RR  ^
 2  0  <_
 
23-Aug-2020df-rsqrt 9207 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 6542 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 6541 Lemma for addnqpr 6542. 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 6540 Lemma for addnqpr 6542. 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 6539 Lemma for addnqpr 6542. 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 6538 Lemma for addnqpr 6542. 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 6616 Lemma for cauappcvgprlemladdrl 6629. 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 6621 Lemma for cauappcvgpr 6634. 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 6620 Lemma for cauappcvgpr 6634. 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 6619 Lemma for cauappcvgpr 6634. 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 6618 Lemma for cauappcvgpr 6634. 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 6624 Lemma for cauappcvgpr 6634. 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 6623 Lemma for cauappcvgpr 6634. 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 6622 Lemma for cauappcvgpr 6634. 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 6617 Lemma for cauappcvgpr 6634. 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 6629 Lemma for cauappcvgprlemladd 6630. 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 6628 Lemma for cauappcvgprlemladd 6630. 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 6627 Lemma for cauappcvgprlemladd 6630. 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 6626 Lemma for cauappcvgprlemladd 6630. 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 6533 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 6530 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 6632 Lemma for cauappcvgpr 6634. 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 6631 Lemma for cauappcvgpr 6634. 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 6630 Lemma for cauappcvgpr 6634. 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 6633 Lemma for cauappcvgpr 6634. 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 6625 Lemma for cauappcvgpr 6634. 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 6634 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  } >.
 
18-Jun-2020caucvgpr 6653 A Cauchy sequence of positive fractions with a modulus of convergence converges to a positive real. This is basically Corollary 11.2.13 of [HoTT], p. (varies) (one key difference being that this is for positive reals rather than signed reals). Also, the HoTT book theorem has a modulus of convergence (that is, a rate of convergence) specified by (11.2.9) in HoTT whereas this theorem fixes the rate of convergence to say that all terms after the nth term must be within  1  n of the nth term (it should later be able to prove versions of this theorem with a different fixed rate or a modulus of convergence supplied as a hypothesis). We also specify that every term needs to be larger than a fraction , to avoid the case where we have positive fractions which converge to zero (which is not a positive real). (Contributed by Jim Kingdon, 18-Jun-2020.)
 F : N. --> Q.   &     n  N.  k  N.  n  <N  k  F `  n  <Q  F `  k 
 +Q  *Q `  <. n ,  1o >.  ~Q  F `
  k  <Q  F `  n  +Q  *Q `  <. n ,  1o >.  ~Q    &     j  N.  <Q  F `
  j   =>     P.  Q.  j  N.  k  N.  j  <N  k  <. { l  |  l 
 <Q  F `  k } ,  {  |  F `  k  <Q  } >.  <P  +P.  <. { l  |  l  <Q  } ,  {  |  <Q  } >.  <P  <. { l  |  l  <Q  F `  k  +Q  } ,  {  |  F `  k  +Q  <Q  } >.
 
15-Jun-2020imdivapd 9202 Imaginary part of a division. Related to remul2 9101. (Contributed by Jim Kingdon, 15-Jun-2020.)
 RR   &     CC   &    #  0   =>     Im `  Im `
 
15-Jun-2020redivapd 9201 Real part of a division. Related to remul2 9101. (Contributed by Jim Kingdon, 15-Jun-2020.)
 RR   &     CC   &    #  0   =>     Re `  Re `
 
15-Jun-2020cjdivapd 9195 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 9163 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC   &     CC   =>    #  0  * `  * `  * `
 
14-Jun-2020cjdivap 9137 Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC  CC #  0  * `  * `  * `
 
14-Jun-2020cjap0 9135 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 9134 Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC  CC  * `
 #  * ` #
 
14-Jun-2020imdivap 9109 Imaginary part of a division. Related to immul2 9108. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC  RR #  0  Im `  Im `
 
14-Jun-2020redivap 9102 Real part of a division. Related to remul2 9101. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC  RR #  0  Re `  Re `
 
14-Jun-2020mulreap 9092 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 9061 The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
 RR   &    #  0   =>     0  <  ^ 2
 
13-Jun-2020reexpclzapd 9058 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
 RR   &    #  0   &     N  ZZ   =>     ^ N 
 RR
 
13-Jun-2020expdivapd 9048 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
 CC   &     CC   &    #  0   &     N  NN0   =>    
 ^ N  ^ N 
 ^ N
 
13-Jun-2020sqdivapd 9047 Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
 CC   &     CC   &    #  0   =>    
 ^ 2  ^
 2  ^ 2
 
12-Jun-2020expsubapd 9045 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 9044 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 9043 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 9042 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     1 
 ^ N  1  ^ N
 
12-Jun-2020expnegapd 9041 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 9040 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 9039 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N 
 CC
 
12-Jun-2020sqrecapd 9038 Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   =>     1 
 ^ 2  1  ^ 2
 
12-Jun-2020sqgt0api 8992 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
 RR   =>    #  0  0  < 
 ^ 2
 
12-Jun-2020sqdivapi 8990 Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &     CC   &    #  0   =>     ^ 2 
 ^ 2  ^ 2
 
11-Jun-2020sqgt0ap 8975 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
 RR #  0  0  < 
 ^ 2
 
11-Jun-2020sqdivap 8972 Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC  CC #  0 
 ^ 2  ^
 2  ^ 2
 
11-Jun-2020expdivap 8959 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC  CC #  0  N  NN0  ^ N 
 ^ N  ^ N
 
11-Jun-2020expm1ap 8958 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 8957 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 8956 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 8955 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 8953 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 8952 Lemma for expaddzap 8953. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  M  RR  -u M  NN  N  NN0  ^ M  +  N  ^ M  x.  ^ N
 
10-Jun-2020exprecap 8950 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  N  ZZ  1  ^ N  1  ^ N
 
10-Jun-2020mulexpzap 8949 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 8941 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 8939 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 8940 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 7590 Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC   &     CC   &    #  0   &     x.  C   =>     C
 
9-Jun-2020expclzap 8934 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.)
 CC #  0  N  ZZ  ^ N  CC
 
9-Jun-2020expclzaplem 8933 Closure law for integer exponentiation. Lemma for expclzap 8934 and expap0i 8941. (Contributed by Jim Kingdon, 9-Jun-2020.)
 CC #  0  N  ZZ  ^ N  { 
 CC  | #  0 }
 
9-Jun-2020reexpclzap 8929 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.)
 RR #  0  N  ZZ  ^ N  RR

  Copyright terms: Public domain W3C HTML validation [external]