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 12-Oct-2024 at 6:35 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
1-Oct-2024infex2g 6979 Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.)
 |-  ( A  e.  C  -> inf ( B ,  A ,  R )  e.  _V )
 
30-Sep-2024unbendc 12227 An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.)
 |-  ( ( A  C_  NN  /\  A. x  e. 
 NN DECID  x  e.  A  /\  A. m  e.  NN  E. n  e.  A  m  <  n )  ->  A  ~~ 
 NN )
 
30-Sep-2024prmdc 12011 Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.)
 |-  ( N  e.  NN  -> DECID  N  e.  Prime )
 
30-Sep-2024dcfi 6926 Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.)
 |-  ( ( A  e.  Fin  /\  A. x  e.  A DECID  ph )  -> DECID  A. x  e.  A  ph )
 
29-Sep-2024ssnnct 12218 A decidable subset of  NN is countable. (Contributed by Jim Kingdon, 29-Sep-2024.)
 |-  ( ( A  C_  NN  /\  A. x  e. 
 NN DECID  x  e.  A )  ->  E. f  f : om -onto-> ( A 1o )
 )
 
29-Sep-2024ssnnctlemct 12217 Lemma for ssnnct 12218. The result. (Contributed by Jim Kingdon, 29-Sep-2024.)
 |-  G  = frec ( ( x  e.  ZZ  |->  ( x  +  1 ) ) ,  1 )   =>    |-  ( ( A  C_  NN  /\  A. x  e. 
 NN DECID  x  e.  A )  ->  E. f  f : om -onto-> ( A 1o )
 )
 
28-Sep-2024nninfdcex 11843 A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.)
 |-  ( ph  ->  A  C_ 
 NN )   &    |-  ( ph  ->  A. x  e.  NN DECID  x  e.  A )   &    |-  ( ph  ->  E. y  y  e.  A )   =>    |-  ( ph  ->  E. x  e.  RR  ( A. y  e.  A  -.  y  < 
 x  /\  A. y  e. 
 RR  ( x  < 
 y  ->  E. z  e.  A  z  <  y
 ) ) )
 
27-Sep-2024infregelbex 9510 Any lower bound of a set of real numbers with an infimum is less than or equal to the infimum. (Contributed by Jim Kingdon, 27-Sep-2024.)
 |-  ( ph  ->  E. x  e.  RR  ( A. y  e.  A  -.  y  < 
 x  /\  A. y  e. 
 RR  ( x  < 
 y  ->  E. z  e.  A  z  <  y
 ) ) )   &    |-  ( ph  ->  A  C_  RR )   &    |-  ( ph  ->  B  e.  RR )   =>    |-  ( ph  ->  ( B  <_ inf ( A ,  RR ,  <  )  <->  A. z  e.  A  B  <_  z ) )
 
26-Sep-2024nninfdclemp1 12223 Lemma for nninfdc 12226. Each element of the sequence  F is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.)
 |-  ( ph  ->  A  C_ 
 NN )   &    |-  ( ph  ->  A. x  e.  NN DECID  x  e.  A )   &    |-  ( ph  ->  A. m  e.  NN  E. n  e.  A  m  <  n )   &    |-  ( ph  ->  ( J  e.  A  /\  1  <  J ) )   &    |-  F  =  seq 1
 ( ( y  e. 
 NN ,  z  e. 
 NN  |-> inf ( ( A  i^i  ( ZZ>= `  (
 y  +  1 ) ) ) ,  RR ,  <  ) ) ,  ( i  e.  NN  |->  J ) )   &    |-  ( ph  ->  U  e.  NN )   =>    |-  ( ph  ->  ( F `  U )  < 
 ( F `  ( U  +  1 )
 ) )
 
26-Sep-2024nnminle 12220 The infimum of a decidable subset of the natural numbers is less than an element of the set. The infimum is also a minimum as shown at nnmindc 12219. (Contributed by Jim Kingdon, 26-Sep-2024.)
 |-  ( ( A  C_  NN  /\  A. x  e. 
 NN DECID  x  e.  A  /\  B  e.  A )  -> inf ( A ,  RR ,  <  )  <_  B )
 
25-Sep-2024nninfdclemcl 12221 Lemma for nninfdc 12226. (Contributed by Jim Kingdon, 25-Sep-2024.)
 |-  ( ph  ->  A  C_ 
 NN )   &    |-  ( ph  ->  A. x  e.  NN DECID  x  e.  A )   &    |-  ( ph  ->  A. m  e.  NN  E. n  e.  A  m  <  n )   &    |-  ( ph  ->  P  e.  A )   &    |-  ( ph  ->  Q  e.  A )   =>    |-  ( ph  ->  ( P ( y  e. 
 NN ,  z  e. 
 NN  |-> inf ( ( A  i^i  ( ZZ>= `  (
 y  +  1 ) ) ) ,  RR ,  <  ) ) Q )  e.  A )
 
24-Sep-2024nninfdclemlt 12224 Lemma for nninfdc 12226. The function from nninfdclemf 12222 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.)
 |-  ( ph  ->  A  C_ 
 NN )   &    |-  ( ph  ->  A. x  e.  NN DECID  x  e.  A )   &    |-  ( ph  ->  A. m  e.  NN  E. n  e.  A  m  <  n )   &    |-  ( ph  ->  ( J  e.  A  /\  1  <  J ) )   &    |-  F  =  seq 1
 ( ( y  e. 
 NN ,  z  e. 
 NN  |-> inf ( ( A  i^i  ( ZZ>= `  (
 y  +  1 ) ) ) ,  RR ,  <  ) ) ,  ( i  e.  NN  |->  J ) )   &    |-  ( ph  ->  U  e.  NN )   &    |-  ( ph  ->  V  e.  NN )   &    |-  ( ph  ->  U  <  V )   =>    |-  ( ph  ->  ( F `  U )  <  ( F `  V ) )
 
23-Sep-2024nninfdc 12226 An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.)
 |-  ( ( A  C_  NN  /\  A. x  e. 
 NN DECID  x  e.  A  /\  A. m  e.  NN  E. n  e.  A  m  <  n )  ->  om  ~<_  A )
 
23-Sep-2024nninfdclemf1 12225 Lemma for nninfdc 12226. The function from nninfdclemf 12222 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.)
 |-  ( ph  ->  A  C_ 
 NN )   &    |-  ( ph  ->  A. x  e.  NN DECID  x  e.  A )   &    |-  ( ph  ->  A. m  e.  NN  E. n  e.  A  m  <  n )   &    |-  ( ph  ->  ( J  e.  A  /\  1  <  J ) )   &    |-  F  =  seq 1
 ( ( y  e. 
 NN ,  z  e. 
 NN  |-> inf ( ( A  i^i  ( ZZ>= `  (
 y  +  1 ) ) ) ,  RR ,  <  ) ) ,  ( i  e.  NN  |->  J ) )   =>    |-  ( ph  ->  F : NN -1-1-> A )
 
23-Sep-2024nninfdclemf 12222 Lemma for nninfdc 12226. A function from the natural numbers into  A. (Contributed by Jim Kingdon, 23-Sep-2024.)
 |-  ( ph  ->  A  C_ 
 NN )   &    |-  ( ph  ->  A. x  e.  NN DECID  x  e.  A )   &    |-  ( ph  ->  A. m  e.  NN  E. n  e.  A  m  <  n )   &    |-  ( ph  ->  ( J  e.  A  /\  1  <  J ) )   &    |-  F  =  seq 1
 ( ( y  e. 
 NN ,  z  e. 
 NN  |-> inf ( ( A  i^i  ( ZZ>= `  (
 y  +  1 ) ) ) ,  RR ,  <  ) ) ,  ( i  e.  NN  |->  J ) )   =>    |-  ( ph  ->  F : NN --> A )
 
23-Sep-2024nnmindc 12219 An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.)
 |-  ( ( A  C_  NN  /\  A. x  e. 
 NN DECID  x  e.  A  /\  E. y  y  e.  A )  -> inf ( A ,  RR ,  <  )  e.  A )
 
19-Sep-2024ssomct 12216 A decidable subset of  om is countable. (Contributed by Jim Kingdon, 19-Sep-2024.)
 |-  ( ( A  C_  om 
 /\  A. x  e.  om DECID  x  e.  A )  ->  E. f  f : om -onto-> ( A 1o ) )
 
14-Sep-2024nnpredlt 4584 The predecessor (see nnpredcl 4583) of a nonzero natural number is less than (see df-iord 4327) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)
 |-  ( ( A  e.  om 
 /\  A  =/=  (/) )  ->  U. A  e.  A )
 
13-Sep-2024nninfisollemeq 7076 Lemma for nninfisol 7077. The case where  N is a successor and  N and  X are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
 |-  ( ph  ->  X  e. )   &    |-  ( ph  ->  ( X `  N )  =  (/) )   &    |-  ( ph  ->  N  e.  om )   &    |-  ( ph  ->  N  =/=  (/) )   &    |-  ( ph  ->  ( X `  U. N )  =  1o )   =>    |-  ( ph  -> DECID 
 ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
 
13-Sep-2024nninfisollemne 7075 Lemma for nninfisol 7077. A case where  N is a successor and  N and  X are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
 |-  ( ph  ->  X  e. )   &    |-  ( ph  ->  ( X `  N )  =  (/) )   &    |-  ( ph  ->  N  e.  om )   &    |-  ( ph  ->  N  =/=  (/) )   &    |-  ( ph  ->  ( X `  U. N )  =  (/) )   =>    |-  ( ph  -> DECID  ( i  e.  om  |->  if (
 i  e.  N ,  1o ,  (/) ) )  =  X )
 
13-Sep-2024nninfisollem0 7074 Lemma for nninfisol 7077. The case where  N is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
 |-  ( ph  ->  X  e. )   &    |-  ( ph  ->  ( X `  N )  =  (/) )   &    |-  ( ph  ->  N  e.  om )   &    |-  ( ph  ->  N  =  (/) )   =>    |-  ( ph  -> DECID  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
 
12-Sep-2024nninfisol 7077 Finite elements of ℕ are isolated. That is, given a natural number and any element of ℕ, it is decidable whether the natural number (when converted to an element of ℕ) is equal to the given element of ℕ. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence  X to decide whether it is equal to  N (in fact, you only need to look at two elements and  N tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
 |-  ( ( N  e.  om 
 /\  X  e. )  -> DECID  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
 
7-Sep-2024eulerthlemfi 12107 Lemma for eulerth 12112. The set  S is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   =>    |-  ( ph  ->  S  e.  Fin )
 
7-Sep-2024modqexp 10548 Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
 |-  ( ph  ->  A  e.  ZZ )   &    |-  ( ph  ->  B  e.  ZZ )   &    |-  ( ph  ->  C  e.  NN0 )   &    |-  ( ph  ->  D  e.  QQ )   &    |-  ( ph  ->  0  <  D )   &    |-  ( ph  ->  ( A  mod  D )  =  ( B 
 mod  D ) )   =>    |-  ( ph  ->  ( ( A ^ C )  mod  D )  =  ( ( B ^ C )  mod  D ) )
 
5-Sep-2024eulerthlemh 12110 Lemma for eulerth 12112. A permutation of  ( 1 ... ( phi `  N ) ). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  ( ph  ->  F : ( 1 ... ( phi `  N ) ) -1-1-onto-> S )   &    |-  H  =  ( `' F  o.  ( y  e.  ( 1 ... ( phi `  N ) ) 
 |->  ( ( A  x.  ( F `  y ) )  mod  N ) ) )   =>    |-  ( ph  ->  H : ( 1 ... ( phi `  N ) ) -1-1-onto-> ( 1 ... ( phi `  N ) ) )
 
2-Sep-2024eulerthlemth 12111 Lemma for eulerth 12112. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  ( ph  ->  F : ( 1 ... ( phi `  N ) ) -1-1-onto-> S )   =>    |-  ( ph  ->  ( ( A ^ ( phi `  N ) )  mod  N )  =  ( 1  mod 
 N ) )
 
2-Sep-2024eulerthlema 12109 Lemma for eulerth 12112. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  ( ph  ->  F : ( 1 ... ( phi `  N ) ) -1-1-onto-> S )   =>    |-  ( ph  ->  ( (
 ( A ^ ( phi `  N ) )  x.  prod_ x  e.  (
 1 ... ( phi `  N ) ) ( F `
  x ) ) 
 mod  N )  =  (
 prod_ x  e.  (
 1 ... ( phi `  N ) ) ( ( A  x.  ( F `
  x ) ) 
 mod  N )  mod  N ) )
 
2-Sep-2024eulerthlemrprm 12108 Lemma for eulerth 12112. 
N and  prod_ x  e.  ( 1 ... ( phi `  N ) ) ( F `  x
) are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  ( ph  ->  F : ( 1 ... ( phi `  N ) ) -1-1-onto-> S )   =>    |-  ( ph  ->  ( N  gcd  prod_ x  e.  (
 1 ... ( phi `  N ) ) ( F `
  x ) )  =  1 )
 
30-Aug-2024fprodap0f 11537 A finite product of terms apart from zero is apart from zero. A version of fprodap0 11522 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.)
 |- 
 F/ k ph   &    |-  ( ph  ->  A  e.  Fin )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B #  0 )   =>    |-  ( ph  ->  prod_
 k  e.  A  B #  0 )
 
28-Aug-2024fprodrec 11530 The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.)
 |-  ( ph  ->  A  e.  Fin )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B #  0 )   =>    |-  ( ph  ->  prod_ k  e.  A  ( 1  /  B )  =  (
 1  /  prod_ k  e.  A  B ) )
 
26-Aug-2024exmidontri2or 7179 Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
 |-  (EXMID  <->  A. x  e.  On  A. y  e.  On  ( x  C_  y  \/  y  C_  x ) )
 
26-Aug-2024exmidontri 7175 Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
 |-  (EXMID  <->  A. x  e.  On  A. y  e.  On  ( x  e.  y  \/  x  =  y  \/  y  e.  x )
 )
 
26-Aug-2024ontri2orexmidim 4532 Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4531. (Contributed by Jim Kingdon, 26-Aug-2024.)
 |-  ( A. x  e. 
 On  A. y  e.  On  ( x  C_  y  \/  y  C_  x )  -> DECID  ph )
 
26-Aug-2024ontriexmidim 4482 Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4481. (Contributed by Jim Kingdon, 26-Aug-2024.)
 |-  ( A. x  e. 
 On  A. y  e.  On  ( x  e.  y  \/  x  =  y  \/  y  e.  x )  -> DECID  ph )
 
25-Aug-2024onntri2or 7182 Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
 |-  ( -.  -. EXMID  <->  A. x  e.  On  A. y  e.  On  -.  -.  ( x  C_  y  \/  y  C_  x ) )
 
25-Aug-2024onntri3or 7181 Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
 |-  ( -.  -. EXMID  <->  A. x  e.  On  A. y  e.  On  -.  -.  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) )
 
25-Aug-2024csbcow 3042 Composition law for chained substitutions into a class. Version of csbco 3041 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by Gino Giotto, 25-Aug-2024.)
 |-  [_ A  /  y ]_ [_ y  /  x ]_ B  =  [_ A  /  x ]_ B
 
25-Aug-2024cbvreuvw 2686 Version of cbvreuv 2682 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( E! x  e.  A  ph  <->  E! y  e.  A  ps )
 
25-Aug-2024cbvrexvw 2685 Version of cbvrexv 2681 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
 
25-Aug-2024cbvralvw 2684 Version of cbvralv 2680 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
 
25-Aug-2024cbvabw 2280 Version of cbvab 2281 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
 |- 
 F/ y ph   &    |-  F/ x ps   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  { x  |  ph
 }  =  { y  |  ps }
 
25-Aug-2024nfsbv 1927 If  z is not free in  ph, it is not free in  [ y  /  x ] ph when  z is distinct from  x and  y. Version of nfsb 1926 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on  x ,  y. (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
 |- 
 F/ z ph   =>    |- 
 F/ z [ y  /  x ] ph
 
25-Aug-2024cbvexvw 1900 Change bound variable. See cbvexv 1898 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1428. (Revised by Gino Giotto, 25-Aug-2024.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( E. x ph  <->  E. y ps )
 
25-Aug-2024cbvalvw 1899 Change bound variable. See cbvalv 1897 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1428. (Revised by Gino Giotto, 25-Aug-2024.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( A. x ph  <->  A. y ps )
 
25-Aug-2024nfal 1556 If  x is not free in  ph, it is not free in  A. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1490. (Revised by Gino Giotto, 25-Aug-2024.)
 |- 
 F/ x ph   =>    |- 
 F/ x A. y ph
 
24-Aug-2024gcdcomd 11862 The  gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  ZZ )   =>    |-  ( ph  ->  ( M  gcd  N )  =  ( N  gcd  M ) )
 
17-Aug-2024fprodcl2lem 11506 Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)
 |-  ( ph  ->  S  C_ 
 CC )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x  x.  y )  e.  S )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B  e.  S )   &    |-  ( ph  ->  A  =/=  (/) )   =>    |-  ( ph  ->  prod_ k  e.  A  B  e.  S )
 
16-Aug-2024if0ab 13422 Expression of a conditional class as a class abstraction when the False alternative is the empty class: in that case, the conditional class is the extension, in the True alternative, of the condition.

Remark: a consequence which could be formalized is the inclusion  |-  if (
ph ,  A ,  (/) )  C_  A and therefore, using elpwg 3551,  |-  ( A  e.  V  ->  if ( ph ,  A ,  (/) )  e.  ~P A
), from which fmelpw1o 13423 could be derived, yielding an alternative proof. (Contributed by BJ, 16-Aug-2024.)

 |-  if ( ph ,  A ,  (/) )  =  { x  e.  A  |  ph }
 
16-Aug-2024fprodunsn 11505 Multiply in an additional term in a finite product. See also fprodsplitsn 11534 which is the same but with a  F/ k
ph hypothesis in place of the distinct variable condition between  ph and  k. (Contributed by Jim Kingdon, 16-Aug-2024.)
 |-  F/_ k D   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  B  e.  V )   &    |-  ( ph  ->  -.  B  e.  A )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( k  =  B  ->  C  =  D )   =>    |-  ( ph  ->  prod_ k  e.  ( A  u.  { B } ) C  =  ( prod_ k  e.  A  C  x.  D ) )
 
15-Aug-2024bj-charfundcALT 13426 Alternate proof of bj-charfundc 13425. It was expected to be much shorter since it uses bj-charfun 13424 for the main part of the proof and the rest is basic computations, but these turn out to be lengthy, maybe because of the limited library of available lemmas. (Contributed by BJ, 15-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( ph  ->  F  =  ( x  e.  X  |->  if ( x  e.  A ,  1o ,  (/) ) ) )   &    |-  ( ph  ->  A. x  e.  X DECID  x  e.  A )   =>    |-  ( ph  ->  ( F : X --> 2o  /\  ( A. x  e.  ( X  i^i  A ) ( F `  x )  =  1o  /\  A. x  e.  ( X  \  A ) ( F `
  x )  =  (/) ) ) )
 
15-Aug-2024bj-charfun 13424 Properties of the characteristic function on the class  X of the class  A. (Contributed by BJ, 15-Aug-2024.)
 |-  ( ph  ->  F  =  ( x  e.  X  |->  if ( x  e.  A ,  1o ,  (/) ) ) )   =>    |-  ( ph  ->  (
 ( F : X --> ~P 1o  /\  ( F  |`  ( ( X  i^i  A )  u.  ( X 
 \  A ) ) ) : ( ( X  i^i  A )  u.  ( X  \  A ) ) --> 2o )  /\  ( A. x  e.  ( X  i^i  A ) ( F `  x )  =  1o  /\ 
 A. x  e.  ( X  \  A ) ( F `  x )  =  (/) ) ) )
 
15-Aug-2024fmelpw1o 13423 With a formula  ph one can associate an element of 
~P 1o, which can therefore be thought of as the set of "truth values" (but recall that there are no other genuine truth values than T. and F., by nndc 837, which translate to  1o and  (/) respectively by iftrue 3510 and iffalse 3513, giving pwtrufal 13611).

As proved in if0ab 13422, the associated element of  ~P 1o is the extension, in  ~P 1o, of the formula  ph. (Contributed by BJ, 15-Aug-2024.)

 |-  if ( ph ,  1o ,  (/) )  e.  ~P 1o
 
15-Aug-2024cnstab 8521 Equality of complex numbers is stable. Stability here means  -.  -.  A  =  B  ->  A  =  B as defined at df-stab 817. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.)
 |-  ( ( A  e.  CC  /\  B  e.  CC )  -> STAB 
 A  =  B )
 
15-Aug-2024subap0d 8520 Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ, 15-Aug-2024.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  A #  B )   =>    |-  ( ph  ->  ( A  -  B ) #  0 )
 
15-Aug-2024ifexd 4445 Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  B  e.  W )   =>    |-  ( ph  ->  if ( ph ,  A ,  B )  e.  _V )
 
15-Aug-2024ifelpwun 4444 Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.)
 |-  A  e.  _V   &    |-  B  e.  _V   =>    |- 
 if ( ph ,  A ,  B )  e.  ~P ( A  u.  B )
 
15-Aug-2024ifelpwund 4443 Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  B  e.  W )   =>    |-  ( ph  ->  if ( ph ,  A ,  B )  e.  ~P ( A  u.  B ) )
 
15-Aug-2024ifelpwung 4442 Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.)
 |-  ( ( A  e.  V  /\  B  e.  W )  ->  if ( ph ,  A ,  B )  e.  ~P ( A  u.  B ) )
 
15-Aug-2024ifidss 3520 A conditional class whose two alternatives are equal is included in that alternative. With excluded middle, we can prove it is equal to it. (Contributed by BJ, 15-Aug-2024.)
 |- 
 if ( ph ,  A ,  A )  C_  A
 
15-Aug-2024ifssun 3519 A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.)
 |- 
 if ( ph ,  A ,  B )  C_  ( A  u.  B )
 
12-Aug-2024exmidontriimlem2 7158 Lemma for exmidontriim 7161. (Contributed by Jim Kingdon, 12-Aug-2024.)
 |-  ( ph  ->  B  e.  On )   &    |-  ( ph  -> EXMID )   &    |-  ( ph  ->  A. y  e.  B  ( A  e.  y  \/  A  =  y  \/  y  e.  A ) )   =>    |-  ( ph  ->  ( A  e.  B  \/  A. y  e.  B  y  e.  A ) )
 
12-Aug-2024exmidontriimlem1 7157 Lemma for exmidontriim 7161. A variation of r19.30dc 2604. (Contributed by Jim Kingdon, 12-Aug-2024.)
 |-  ( ( A. x  e.  A  ( ph  \/  ps 
 \/  ch )  /\ EXMID )  ->  ( E. x  e.  A  ph  \/  E. x  e.  A  ps  \/  A. x  e.  A  ch ) )
 
11-Aug-2024nndc 837 Double negation of decidability of a formula. Intuitionistic logic refutes the negation of decidability (but does not prove decidability) of any formula.

This should not trick the reader into thinking that  -.  -. EXMID is provable in intuitionistic logic. Indeed, if we could quantify over formula metavariables, then generalizing nnexmid 836 over  ph would give " |-  A. ph -.  -. DECID  ph", but EXMID is " A. phDECID 
ph", so proving 
-.  -. EXMID would amount to proving " -.  -.  A. phDECID  ph", which is not implied by the above theorem. Indeed, the converse of nnal 1629 does not hold. Since our system does not allow quantification over formula metavariables, we can reproduce this argument by representing formulas as subsets of  ~P 1o, like we do in our definition of EXMID (df-exmid 4157): then, we can prove  A. x  e. 
~P 1o -.  -. DECID  x  =  1o but we cannot prove  -.  -.  A. x  e.  ~P 1oDECID  x  =  1o because the converse of nnral 2447 does not hold.

Actually,  -.  -. EXMID is not provable in intuitionistic logic since intuitionistic logic has models satisfying  -. EXMID and noncontradiction holds (pm3.24 683). (Contributed by BJ, 9-Oct-2019.) Add explanation on non-provability of  -. 
-. EXMID. (Revised by BJ, 11-Aug-2024.)

 |- 
 -.  -. DECID  ph
 
10-Aug-2024exmidontriim 7161 Excluded middle implies ordinal trichotomy. Lemma 10.4.1 of [HoTT], p. (varies). The proof follows the proof from the HoTT book fairly closely. (Contributed by Jim Kingdon, 10-Aug-2024.)
 |-  (EXMID 
 ->  A. x  e.  On  A. y  e.  On  ( x  e.  y  \/  x  =  y  \/  y  e.  x )
 )
 
10-Aug-2024exmidontriimlem4 7160 Lemma for exmidontriim 7161. The induction step for the induction on  A. (Contributed by Jim Kingdon, 10-Aug-2024.)
 |-  ( ph  ->  A  e.  On )   &    |-  ( ph  ->  B  e.  On )   &    |-  ( ph  -> EXMID
 )   &    |-  ( ph  ->  A. z  e.  A  A. y  e. 
 On  ( z  e.  y  \/  z  =  y  \/  y  e.  z ) )   =>    |-  ( ph  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A )
 )
 
10-Aug-2024exmidontriimlem3 7159 Lemma for exmidontriim 7161. What we get to do based on induction on both  A and  B. (Contributed by Jim Kingdon, 10-Aug-2024.)
 |-  ( ph  ->  A  e.  On )   &    |-  ( ph  ->  B  e.  On )   &    |-  ( ph  -> EXMID
 )   &    |-  ( ph  ->  A. z  e.  A  A. y  e. 
 On  ( z  e.  y  \/  z  =  y  \/  y  e.  z ) )   &    |-  ( ph  ->  A. y  e.  B  ( A  e.  y  \/  A  =  y  \/  y  e.  A ) )   =>    |-  ( ph  ->  ( A  e.  B  \/  A  =  B  \/  B  e.  A )
 )
 
10-Aug-2024nnnninf2 7071 Canonical embedding of  suc  om into ℕ. (Contributed by BJ, 10-Aug-2024.)
 |-  ( N  e.  suc  om 
 ->  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  e. )
 
10-Aug-2024infnninf 7068 The point at infinity in ℕ is the constant sequence equal to  1o. Note that with our encoding of functions, that constant function can also be expressed as  ( om  X.  { 1o } ), as fconstmpt 4634 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)
 |-  ( i  e.  om  |->  1o )  e.
 
9-Aug-2024ss1o0el1o 6858 Reformulation of ss1o0el1 4159 using  1o instead of 
{ (/) }. (Contributed by BJ, 9-Aug-2024.)
 |-  ( A  C_  1o  ->  ( (/)  e.  A  <->  A  =  1o ) )
 
9-Aug-2024pw1dc0el 6857 Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.)
 |-  (EXMID  <->  A. x  e.  ~P  1oDECID  (/)  e.  x )
 
9-Aug-2024ss1o0el1 4159 A subclass of  { (/) } contains the empty set if and only if it equals  { (/) }. (Contributed by BJ and Jim Kingdon, 9-Aug-2024.)
 |-  ( A  C_  { (/) }  ->  ( (/)  e.  A  <->  A  =  { (/)
 } ) )
 
8-Aug-2024pw1dc1 6859 If, in the set of truth values (the powerset of 1o), equality to 1o is decidable, then excluded middle holds (and conversely). (Contributed by BJ and Jim Kingdon, 8-Aug-2024.)
 |-  (EXMID  <->  A. x  e.  ~P  1oDECID  x  =  1o )
 
7-Aug-2024pw1fin 6856 Excluded middle is equivalent to the power set of  1o being finite. (Contributed by SN and Jim Kingdon, 7-Aug-2024.)
 |-  (EXMID  <->  ~P 1o  e.  Fin )
 
7-Aug-2024elomssom 4565 A natural number ordinal is, as a set, included in the set of natural number ordinals. (Contributed by NM, 21-Jun-1998.) Extract this result from the previous proof of elnn 4566. (Revised by BJ, 7-Aug-2024.)
 |-  ( A  e.  om  ->  A  C_  om )
 
6-Aug-2024bj-charfunbi 13428 In an ambient set  X, if membership in  A is stable, then it is decidable if and only if  A has a characteristic function.

This characterization can be applied to singletons when the set  X has stable equality, which is the case as soon as it has a tight apartness relation. (Contributed by BJ, 6-Aug-2024.)

 |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  A. x  e.  X STAB  x  e.  A )   =>    |-  ( ph  ->  ( A. x  e.  X DECID  x  e.  A 
 <-> 
 E. f  e.  ( 2o  ^m  X ) (
 A. x  e.  ( X  i^i  A ) ( f `  x )  =  1o  /\  A. x  e.  ( X  \  A ) ( f `
  x )  =  (/) ) ) )
 
6-Aug-2024bj-charfunr 13427 If a class  A has a "weak" characteristic function on a class  X, then negated membership in 
A is decidable (in other words, membership in  A is testable) in  X.

The hypothesis imposes that 
X be a set. As usual, it could be formulated as  |-  ( ph  ->  ( F : X --> om  /\  ... ) ) to deal with general classes, but that extra generality would not make the theorem much more useful.

The theorem would still hold if the codomain of  f were any class with testable equality to the point where  ( X  \  A ) is sent. (Contributed by BJ, 6-Aug-2024.)

 |-  ( ph  ->  E. f  e.  ( om  ^m  X ) (
 A. x  e.  ( X  i^i  A ) ( f `  x )  =/=  (/)  /\  A. x  e.  ( X  \  A ) ( f `  x )  =  (/) ) )   =>    |-  ( ph  ->  A. x  e.  X DECID 
 -.  x  e.  A )
 
6-Aug-2024bj-charfundc 13425 Properties of the characteristic function on the class  X of the class  A, provided membership in  A is decidable in  X. (Contributed by BJ, 6-Aug-2024.)
 |-  ( ph  ->  F  =  ( x  e.  X  |->  if ( x  e.  A ,  1o ,  (/) ) ) )   &    |-  ( ph  ->  A. x  e.  X DECID  x  e.  A )   =>    |-  ( ph  ->  ( F : X --> 2o  /\  ( A. x  e.  ( X  i^i  A ) ( F `  x )  =  1o  /\  A. x  e.  ( X  \  A ) ( F `
  x )  =  (/) ) ) )
 
6-Aug-2024prodssdc 11490 Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.) (Revised by Jim Kingdon, 6-Aug-2024.)
 |-  ( ph  ->  A  C_  B )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  C  e.  CC )   &    |-  ( ph  ->  E. n  e.  ( ZZ>=
 `  M ) E. y ( y #  0 
 /\  seq n (  x. 
 ,  ( k  e.  ( ZZ>= `  M )  |->  if ( k  e.  B ,  C , 
 1 ) ) )  ~~>  y ) )   &    |-  ( ph  ->  A. j  e.  ( ZZ>=
 `  M )DECID  j  e.  A )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  (
 ( ph  /\  k  e.  ( B  \  A ) )  ->  C  =  1 )   &    |-  ( ph  ->  B 
 C_  ( ZZ>= `  M ) )   &    |-  ( ph  ->  A. j  e.  ( ZZ>= `  M )DECID  j  e.  B )   =>    |-  ( ph  ->  prod_ k  e.  A  C  =  prod_ k  e.  B  C )
 
5-Aug-2024fnmptd 13421 The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.)
 |-  ( ph  ->  F  =  ( x  e.  A  |->  B ) )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  B  e.  V )   =>    |-  ( ph  ->  F  Fn  A )
 
5-Aug-2024funmptd 13420 The maps-to notation defines a function (deduction form).

Note: one should similarly prove a deduction form of funopab4 5208, then prove funmptd 13420 from it, and then prove funmpt 5209 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.)

 |-  ( ph  ->  F  =  ( x  e.  A  |->  B ) )   =>    |-  ( ph  ->  Fun  F )
 
5-Aug-20242ssom 13419 The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.)
 |-  2o  C_ 
 om
 
5-Aug-2024bj-dcfal 13369 The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.)
 |- DECID F.
 
5-Aug-2024bj-dctru 13367 The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.)
 |- DECID T.
 
5-Aug-2024bj-stfal 13359 The false truth value is stable. (Contributed by BJ, 5-Aug-2024.)
 |- STAB F.
 
5-Aug-2024bj-sttru 13357 The true truth value is stable. (Contributed by BJ, 5-Aug-2024.)
 |- STAB T.
 
5-Aug-2024prod1dc 11487 Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.)
 |-  ( ( ( M  e.  ZZ  /\  A  C_  ( ZZ>= `  M )  /\  A. j  e.  ( ZZ>=
 `  M )DECID  j  e.  A )  \/  A  e.  Fin )  ->  prod_ k  e.  A  1  =  1 )
 
2-Aug-2024onntri52 7180 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
 |-  ( -.  -. EXMID  ->  -.  -.  A. x  e.  On  A. y  e.  On  ( x  C_  y  \/  y  C_  x ) )
 
2-Aug-2024onntri24 7178 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
 |-  ( -.  -.  A. x  e.  On  A. y  e.  On  ( x  C_  y  \/  y  C_  x )  ->  A. x  e.  On  A. y  e.  On  -.  -.  ( x  C_  y  \/  y  C_  x ) )
 
2-Aug-2024onntri45 7177 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
 |-  ( A. x  e. 
 On  A. y  e.  On  -. 
 -.  ( x  C_  y  \/  y  C_  x )  ->  -.  -. EXMID )
 
2-Aug-2024onntri51 7176 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
 |-  ( -.  -. EXMID  ->  -.  -.  A. x  e.  On  A. y  e.  On  ( x  e.  y  \/  x  =  y  \/  y  e.  x )
 )
 
2-Aug-2024onntri13 7174 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
 |-  ( -.  -.  A. x  e.  On  A. y  e.  On  ( x  e.  y  \/  x  =  y  \/  y  e.  x )  ->  A. x  e.  On  A. y  e. 
 On  -.  -.  ( x  e.  y  \/  x  =  y  \/  y  e.  x )
 )
 
2-Aug-2024onntri35 7173 Double negated ordinal trichotomy.

There are five equivalent statements: (1)  -.  -.  A. x  e.  On A. y  e.  On ( x  e.  y  \/  x  =  y  \/  y  e.  x ), (2)  -.  -.  A. x  e.  On A. y  e.  On ( x  C_  y  \/  y  C_  x ), (3)  A. x  e.  On A. y  e.  On -.  -.  (
x  e.  y  \/  x  =  y  \/  y  e.  x ), (4)  A. x  e.  On A. y  e.  On -.  -.  (
x  C_  y  \/  y  C_  x ), and (5)  -.  -. EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7174), (3) implies (5) (onntri35 7173), (5) implies (1) (onntri51 7176), (2) implies (4) (onntri24 7178), (4) implies (5) (onntri45 7177), and (5) implies (2) (onntri52 7180).

Another way of stating this is that EXMID is equivalent to trichotomy, either the  x  e.  y  \/  x  =  y  \/  y  e.  x or the  x  C_  y  \/  y  C_  x form, as shown in exmidontri 7175 and exmidontri2or 7179, respectively. Thus  -.  -. EXMID is equivalent to (1) or (2). In addition, 
-.  -. EXMID is equivalent to (3) by onntri3or 7181 and (4) by onntri2or 7182.

(Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)

 |-  ( A. x  e. 
 On  A. y  e.  On  -. 
 -.  ( x  e.  y  \/  x  =  y  \/  y  e.  x )  ->  -.  -. EXMID )
 
1-Aug-2024nnral 2447 The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1629. (Contributed by Jim Kingdon, 1-Aug-2024.)
 |-  ( -.  -.  A. x  e.  A  ph  ->  A. x  e.  A  -.  -.  ph )
 
31-Jul-20243nsssucpw1 7172 Negated excluded middle implies that  3o is not a subset of the successor of the power set of 
1o. (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
 |-  ( -. EXMID  ->  -.  3o  C_  suc  ~P 1o )
 
31-Jul-2024sucpw1nss3 7171 Negated excluded middle implies that the successor of the power set of  1o is not a subset of  3o. (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
 |-  ( -. EXMID  ->  -.  suc  ~P 1o  C_ 
 3o )
 
30-Jul-20243nelsucpw1 7170 Three is not an element of the successor of the power set of  1o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
 |- 
 -.  3o  e.  suc  ~P 1o
 
30-Jul-2024sucpw1nel3 7169 The successor of the power set of 
1o is not an element of  3o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
 |- 
 -.  suc  ~P 1o  e.  3o
 
30-Jul-2024sucpw1ne3 7168 Negated excluded middle implies that the successor of the power set of  1o is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
 |-  ( -. EXMID  ->  suc  ~P 1o  =/=  3o )
 
30-Jul-2024pw1nel3 7167 Negated excluded middle implies that the power set of  1o is not an element of  3o. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
 |-  ( -. EXMID  ->  -.  ~P 1o  e.  3o )
 
30-Jul-2024pw1ne3 7166 The power set of  1o is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
 |- 
 ~P 1o  =/=  3o
 
30-Jul-2024pw1ne1 7165 The power set of  1o is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)
 |- 
 ~P 1o  =/=  1o
 
30-Jul-2024pw1ne0 7164 The power set of  1o is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)
 |- 
 ~P 1o  =/=  (/)
 
29-Jul-2024pw1on 7162 The power set of  1o is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)
 |- 
 ~P 1o  e.  On
 
28-Jul-2024exmidpweq 6855 Excluded middle is equivalent to the power set of  1o being  2o. (Contributed by Jim Kingdon, 28-Jul-2024.)
 |-  (EXMID  <->  ~P 1o  =  2o )
 
27-Jul-2024dcapnconstALT 13674 Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 13673 by means of dceqnconst 13672. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
 |-  ( A. x  e.  RR DECID  x #  0 
 ->  E. f ( f : RR --> ZZ  /\  ( f `  0
 )  =  0  /\  A. x  e.  RR+  ( f `
  x )  =/=  0 ) )
 
27-Jul-2024reap0 13671 Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.)
 |-  ( A. x  e.  RR  A. y  e.  RR  ( x  <  y  \/  x  =  y  \/  y  <  x )  <->  A. z  e.  RR DECID  z #  0 )
 
26-Jul-2024nconstwlpolemgt0 13676 Lemma for nconstwlpo 13678. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
 |-  ( ph  ->  G : NN --> { 0 ,  1 } )   &    |-  A  =  sum_ i  e.  NN  ( ( 1  /  ( 2 ^ i ) )  x.  ( G `  i ) )   &    |-  ( ph  ->  E. x  e.  NN  ( G `  x )  =  1 )   =>    |-  ( ph  ->  0  <  A )
 
26-Jul-2024nconstwlpolem0 13675 Lemma for nconstwlpo 13678. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.)
 |-  ( ph  ->  G : NN --> { 0 ,  1 } )   &    |-  A  =  sum_ i  e.  NN  ( ( 1  /  ( 2 ^ i ) )  x.  ( G `  i ) )   &    |-  ( ph  ->  A. x  e.  NN  ( G `  x )  =  0 )   =>    |-  ( ph  ->  A  =  0 )
 
24-Jul-2024tridceq 13669 Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 13656 and redcwlpo 13668). Thus, this is an analytic analogue to lpowlpo 7112. (Contributed by Jim Kingdon, 24-Jul-2024.)
 |-  ( A. x  e.  RR  A. y  e.  RR  ( x  <  y  \/  x  =  y  \/  y  <  x )  ->  A. x  e.  RR  A. y  e. 
 RR DECID  x  =  y )
 
24-Jul-2024iswomni0 13664 Weak omniscience stated in terms of equality with  0. Like iswomninn 13663 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.)
 |-  ( A  e.  V  ->  ( A  e. WOmni  <->  A. f  e.  ( { 0 ,  1 }  ^m  A )DECID  A. x  e.  A  (
 f `  x )  =  0 ) )
 
24-Jul-2024lpowlpo 7112 LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7111. There is an analogue in terms of analytic omniscience principles at tridceq 13669. (Contributed by Jim Kingdon, 24-Jul-2024.)
 |-  ( om  e. Omni  ->  om  e. WOmni )
 
23-Jul-2024nconstwlpolem 13677 Lemma for nconstwlpo 13678. (Contributed by Jim Kingdon, 23-Jul-2024.)
 |-  ( ph  ->  F : RR --> ZZ )   &    |-  ( ph  ->  ( F `  0 )  =  0 )   &    |-  (
 ( ph  /\  x  e.  RR+ )  ->  ( F `
  x )  =/=  0 )   &    |-  ( ph  ->  G : NN --> { 0 ,  1 } )   &    |-  A  =  sum_ i  e.  NN  ( ( 1  /  ( 2 ^ i
 ) )  x.  ( G `  i ) )   =>    |-  ( ph  ->  ( A. y  e.  NN  ( G `  y )  =  0  \/  -.  A. y  e.  NN  ( G `  y )  =  0 ) )
 
23-Jul-2024dceqnconst 13672 Decidability of real number equality implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See redcwlpo 13668 for more discussion of decidability of real number equality. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) (Revised by Jim Kingdon, 23-Jul-2024.)
 |-  ( A. x  e.  RR DECID  x  =  0  ->  E. f
 ( f : RR --> ZZ  /\  ( f `  0 )  =  0  /\  A. x  e.  RR+  ( f `  x )  =/=  0 ) )
 
23-Jul-2024redc0 13670 Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.)
 |-  ( A. x  e.  RR  A. y  e.  RR DECID  x  =  y 
 <-> 
 A. z  e.  RR DECID  z  =  0 )
 
23-Jul-2024canth 5779 No set  A is equinumerous to its power set (Cantor's theorem), i.e., no function can map  A onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1480 if you want the form  -.  E. f
f : A -onto-> ~P A.) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.)
 |-  A  e.  _V   =>    |-  -.  F : A -onto-> ~P A
 
22-Jul-2024nconstwlpo 13678 Existence of a certain non-constant function from reals to integers implies  om  e. WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.)
 |-  ( ph  ->  F : RR --> ZZ )   &    |-  ( ph  ->  ( F `  0 )  =  0 )   &    |-  (
 ( ph  /\  x  e.  RR+ )  ->  ( F `
  x )  =/=  0 )   =>    |-  ( ph  ->  om  e. WOmni )
 
15-Jul-2024fprodseq 11484 The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)
 |-  ( k  =  ( F `  n ) 
 ->  B  =  C )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 M ) -1-1-onto-> A )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  (
 ( ph  /\  n  e.  ( 1 ... M ) )  ->  ( G `
  n )  =  C )   =>    |-  ( ph  ->  prod_ k  e.  A  B  =  ( 
 seq 1 (  x. 
 ,  ( n  e. 
 NN  |->  if ( n  <_  M ,  ( G `  n ) ,  1 ) ) ) `  M ) )
 
14-Jul-2024rexbid2 2462 Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
 |- 
 F/ x ph   &    |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  B  /\  ch )
 ) )   =>    |-  ( ph  ->  ( E. x  e.  A  ps 
 <-> 
 E. x  e.  B  ch ) )
 
14-Jul-2024ralbid2 2461 Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.)
 |- 
 F/ x ph   &    |-  ( ph  ->  ( ( x  e.  A  ->  ps )  <->  ( x  e.  B  ->  ch )
 ) )   =>    |-  ( ph  ->  ( A. x  e.  A  ps 
 <-> 
 A. x  e.  B  ch ) )
 
12-Jul-20242irrexpqap 13337 There exist real numbers  a and  b which are irrational (in the sense of being apart from any rational number) such that  ( a ^ b ) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. This is a constructive proof because it is based on two explicitly named irrational numbers  ( sqr `  2 ) and  ( 2 logb  9 ), see sqrt2irrap 12059, 2logb9irrap 13336 and sqrt2cxp2logb9e3 13334. Therefore, this proof is acceptable/usable in intuitionistic logic. (Contributed by Jim Kingdon, 12-Jul-2024.)
 |- 
 E. a  e.  RR  E. b  e.  RR  ( A. p  e.  QQ  a #  p  /\  A. q  e.  QQ  b #  q  /\  ( a  ^c  b )  e.  QQ )
 
12-Jul-20242logb9irrap 13336 Example for logbgcd1irrap 13329. The logarithm of nine to base two is irrational (in the sense of being apart from any rational number). (Contributed by Jim Kingdon, 12-Jul-2024.)
 |-  ( Q  e.  QQ  ->  ( 2 logb  9 ) #  Q )
 
11-Jul-2024logbgcd1irraplemexp 13327 Lemma for logbgcd1irrap 13329. Apartness of  X ^ N and  B ^ M. (Contributed by Jim Kingdon, 11-Jul-2024.)
 |-  ( ph  ->  X  e.  ( ZZ>= `  2 )
 )   &    |-  ( ph  ->  B  e.  ( ZZ>= `  2 )
 )   &    |-  ( ph  ->  ( X  gcd  B )  =  1 )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( X ^ N ) #  ( B ^ M ) )
 
11-Jul-2024reapef 13141 Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.)
 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A #  B  <->  ( exp `  A ) #  ( exp `  B )
 ) )
 
10-Jul-2024apcxp2 13300 Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.)
 |-  ( ( ( A  e.  RR+  /\  A #  1
 )  /\  ( B  e.  RR  /\  C  e.  RR ) )  ->  ( B #  C  <->  ( A  ^c  B ) #  ( A 
 ^c  C ) ) )
 
9-Jul-2024logbgcd1irraplemap 13328 Lemma for logbgcd1irrap 13329. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.)
 |-  ( ph  ->  X  e.  ( ZZ>= `  2 )
 )   &    |-  ( ph  ->  B  e.  ( ZZ>= `  2 )
 )   &    |-  ( ph  ->  ( X  gcd  B )  =  1 )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( B logb  X ) #  ( M  /  N ) )
 
9-Jul-2024apexp1 10596 Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.)
 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  N  e.  NN )  ->  ( ( A ^ N ) #  ( B ^ N )  ->  A #  B ) )
 
5-Jul-2024logrpap0 13240 The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.)
 |-  ( ( A  e.  RR+  /\  A #  1 )  ->  ( log `  A ) #  0 )
 
3-Jul-2024rplogbval 13304 Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by Jim Kingdon, 3-Jul-2024.)
 |-  ( ( B  e.  RR+  /\  B #  1  /\  X  e.  RR+ )  ->  ( B logb  X )  =  (
 ( log `  X )  /  ( log `  B ) ) )
 
3-Jul-2024logrpap0d 13241 Deduction form of logrpap0 13240. (Contributed by Jim Kingdon, 3-Jul-2024.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  A #  1 )   =>    |-  ( ph  ->  ( log `  A ) #  0 )
 
3-Jul-2024logrpap0b 13239 The logarithm is apart from 0 if and only if its argument is apart from 1. (Contributed by Jim Kingdon, 3-Jul-2024.)
 |-  ( A  e.  RR+  ->  ( A #  1  <->  ( log `  A ) #  0 ) )
 
28-Jun-20242o01f 13610 Mapping zero and one between  om and  NN0 style integers. (Contributed by Jim Kingdon, 28-Jun-2024.)
 |-  G  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   =>    |-  ( G  |`  2o ) : 2o --> { 0 ,  1 }
 
28-Jun-2024012of 13609 Mapping zero and one between  NN0 and  om style integers. (Contributed by Jim Kingdon, 28-Jun-2024.)
 |-  G  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   =>    |-  ( `' G  |`  { 0 ,  1 } ) : { 0 ,  1 } --> 2o
 
27-Jun-2024iooreen 13648 An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.)
 |-  (
 0 (,) 1 )  ~~  RR
 
27-Jun-2024iooref1o 13647 A one-to-one mapping from the real numbers onto the open unit interval. (Contributed by Jim Kingdon, 27-Jun-2024.)
 |-  F  =  ( x  e.  RR  |->  ( 1  /  (
 1  +  ( exp `  x ) ) ) )   =>    |-  F : RR -1-1-onto-> ( 0 (,) 1
 )
 
25-Jun-2024neapmkvlem 13679 Lemma for neapmkv 13680. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
 |-  ( ph  ->  F : NN --> { 0 ,  1 } )   &    |-  A  =  sum_ i  e.  NN  ( ( 1  /  ( 2 ^ i ) )  x.  ( F `  i ) )   &    |-  (
 ( ph  /\  A  =/=  1 )  ->  A #  1
 )   =>    |-  ( ph  ->  ( -.  A. x  e.  NN  ( F `  x )  =  1  ->  E. x  e.  NN  ( F `  x )  =  0
 ) )
 
25-Jun-2024ismkvnn 13666 The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.)
 |-  ( A  e.  V  ->  ( A  e. Markov  <->  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( -.  A. x  e.  A  ( f `  x )  =  1  ->  E. x  e.  A  ( f `  x )  =  0 )
 ) )
 
25-Jun-2024ismkvnnlem 13665 Lemma for ismkvnn 13666. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.)
 |-  G  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   =>    |-  ( A  e.  V  ->  ( A  e. Markov  <->  A. f  e.  ( { 0 ,  1 }  ^m  A ) ( -.  A. x  e.  A  ( f `  x )  =  1  ->  E. x  e.  A  ( f `  x )  =  0 )
 ) )
 
25-Jun-2024enmkvlem 7105 Lemma for enmkv 7106. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.)
 |-  ( A  ~~  B  ->  ( A  e. Markov  ->  B  e. Markov ) )
 
24-Jun-2024neapmkv 13680 If negated equality for real numbers implies apartness, Markov's Principle follows. Exercise 11.10 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 24-Jun-2024.)
 |-  ( A. x  e.  RR  A. y  e.  RR  ( x  =/=  y  ->  x #  y )  ->  om  e. Markov )
 
24-Jun-2024dcapnconst 13673 Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See trilpo 13656 for more discussion of decidability of real number apartness.

This is a weaker form of dceqnconst 13672 and in fact this theorem can be proved using dceqnconst 13672 as shown at dcapnconstALT 13674. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.)

 |-  ( A. x  e.  RR DECID  x #  0 
 ->  E. f ( f : RR --> ZZ  /\  ( f `  0
 )  =  0  /\  A. x  e.  RR+  ( f `
  x )  =/=  0 ) )
 
24-Jun-2024enmkv 7106 Being Markov is invariant with respect to equinumerosity. For example, this means that we can express the Markov's Principle as either  om  e. Markov or  NN0  e. Markov. The former is a better match to conventional notation in the sense that df2o3 6378 says that  2o  =  { (/)
,  1o } whereas the corresponding relationship does not exist between  2 and  { 0 ,  1 }. (Contributed by Jim Kingdon, 24-Jun-2024.)
 |-  ( A  ~~  B  ->  ( A  e. Markov  <->  B  e. Markov ) )
 
21-Jun-2024redcwlpolemeq1 13667 Lemma for redcwlpo 13668. A biconditionalized version of trilpolemeq1 13653. (Contributed by Jim Kingdon, 21-Jun-2024.)
 |-  ( ph  ->  F : NN --> { 0 ,  1 } )   &    |-  A  =  sum_ i  e.  NN  ( ( 1  /  ( 2 ^ i ) )  x.  ( F `  i ) )   =>    |-  ( ph  ->  ( A  =  1  <->  A. x  e.  NN  ( F `  x )  =  1 ) )
 
20-Jun-2024redcwlpo 13668 Decidability of real number equality implies the Weak Limited Principle of Omniscience (WLPO). We expect that we'd need some form of countable choice to prove the converse.

Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence is all ones or it is not. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. This real number will equal one if and only if the sequence is all ones (redcwlpolemeq1 13667). Therefore decidability of real number equality would imply decidability of whether the sequence is all ones.

Because of this theorem, decidability of real number equality is sometimes called "analytic WLPO".

WLPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qdceq 10150 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.)

 |-  ( A. x  e.  RR  A. y  e.  RR DECID  x  =  y  ->  om  e. WOmni )
 
20-Jun-2024iswomninn 13663 Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7110 but it will sometimes be more convenient to use  0 and  1 rather than  (/) and  1o. (Contributed by Jim Kingdon, 20-Jun-2024.)
 |-  ( A  e.  V  ->  ( A  e. WOmni  <->  A. f  e.  ( { 0 ,  1 }  ^m  A )DECID  A. x  e.  A  (
 f `  x )  =  1 ) )
 
20-Jun-2024iswomninnlem 13662 Lemma for iswomnimap 7110. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.)
 |-  G  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   =>    |-  ( A  e.  V  ->  ( A  e. WOmni  <->  A. f  e.  ( { 0 ,  1 }  ^m  A )DECID  A. x  e.  A  (
 f `  x )  =  1 ) )
 
20-Jun-2024enwomni 7114 Weak omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Weak Limited Principle of Omniscience as either  om  e. WOmni or  NN0  e. WOmni. The former is a better match to conventional notation in the sense that df2o3 6378 says that  2o  =  { (/)
,  1o } whereas the corresponding relationship does not exist between  2 and  { 0 ,  1 }. (Contributed by Jim Kingdon, 20-Jun-2024.)
 |-  ( A  ~~  B  ->  ( A  e. WOmni  <->  B  e. WOmni ) )
 
20-Jun-2024enwomnilem 7113 Lemma for enwomni 7114. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.)
 |-  ( A  ~~  B  ->  ( A  e. WOmni  ->  B  e. WOmni ) )
 
19-Jun-2024rpabscxpbnd 13301 Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Jim Kingdon, 19-Jun-2024.)
 |-  ( ph  ->  A  e.  RR+ )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  0  <  ( Re `  B ) )   &    |-  ( ph  ->  M  e.  RR )   &    |-  ( ph  ->  ( abs `  A )  <_  M )   =>    |-  ( ph  ->  ( abs `  ( A  ^c  B ) )  <_  ( ( M  ^c  ( Re `  B ) )  x.  ( exp `  (
 ( abs `  B )  x.  pi ) ) ) )
 
16-Jun-2024rpcxpsqrt 13284 The exponential function with exponent 
1  /  2 exactly matches the square root function, and thus serves as a suitable generalization to other  n-th roots and irrational roots. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 16-Jun-2024.)
 |-  ( A  e.  RR+  ->  ( A  ^c  ( 1  /  2 ) )  =  ( sqr `  A ) )
 
13-Jun-2024rpcxpadd 13268 Sum of exponents law for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 13-Jun-2024.)
 |-  ( ( A  e.  RR+  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  ^c 
 ( B  +  C ) )  =  (
 ( A  ^c  B )  x.  ( A  ^c  C ) ) )
 
12-Jun-2024cxpap0 13267 Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
 |-  ( ( A  e.  RR+  /\  B  e.  CC )  ->  ( A  ^c  B ) #  0 )
 
12-Jun-2024rpcncxpcl 13265 Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.)
 |-  ( ( A  e.  RR+  /\  B  e.  CC )  ->  ( A  ^c  B )  e.  CC )
 
12-Jun-2024rpcxp0 13261 Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
 |-  ( A  e.  RR+  ->  ( A  ^c  0 )  =  1 )
 
12-Jun-2024cxpexpnn 13259 Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
 |-  ( ( A  e.  NN  /\  B  e.  ZZ )  ->  ( A  ^c  B )  =  ( A ^ B ) )
 
12-Jun-2024cxpexprp 13258 Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
 |-  ( ( A  e.  RR+  /\  B  e.  ZZ )  ->  ( A  ^c  B )  =  ( A ^ B ) )
 
12-Jun-2024rpcxpef 13257 Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
 |-  ( ( A  e.  RR+  /\  B  e.  CC )  ->  ( A  ^c  B )  =  ( exp `  ( B  x.  ( log `  A )
 ) ) )
 
12-Jun-2024df-rpcxp 13222 Define the power function on complex numbers. Because df-relog 13221 is only defined on positive reals, this definition only allows for a base which is a positive real. (Contributed by Jim Kingdon, 12-Jun-2024.)
 |- 
 ^c  =  ( x  e.  RR+ ,  y  e.  CC  |->  ( exp `  (
 y  x.  ( log `  x ) ) ) )
 
10-Jun-2024trirec0xor 13658 Version of trirec0 13657 with exclusive-or.

The definition of a discrete field is sometimes stated in terms of exclusive-or but as proved here, this is equivalent to inclusive-or because the two disjuncts cannot be simultaneously true. (Contributed by Jim Kingdon, 10-Jun-2024.)

 |-  ( A. x  e.  RR  A. y  e.  RR  ( x  <  y  \/  x  =  y  \/  y  <  x )  <->  A. x  e.  RR  ( E. z  e.  RR  ( x  x.  z
 )  =  1  \/_  x  =  0 )
 )
 
10-Jun-2024trirec0 13657 Every real number having a reciprocal or equaling zero is equivalent to real number trichotomy.

This is the key part of the definition of what is known as a discrete field, so "the real numbers are a discrete field" can be taken as an equivalent way to state real trichotomy (see further discussion at trilpo 13656). (Contributed by Jim Kingdon, 10-Jun-2024.)

 |-  ( A. x  e.  RR  A. y  e.  RR  ( x  <  y  \/  x  =  y  \/  y  <  x )  <->  A. x  e.  RR  ( E. z  e.  RR  ( x  x.  z
 )  =  1  \/  x  =  0 ) )
 
9-Jun-2024omniwomnimkv 7111 A set is omniscient if and only if it is weakly omniscient and Markov. The case  A  =  om says that LPO  <-> WLPO  /\ MP which is a remark following Definition 2.5 of [Pierik], p. 9. (Contributed by Jim Kingdon, 9-Jun-2024.)
 |-  ( A  e. Omni  <->  ( A  e. WOmni  /\  A  e. Markov ) )
 
9-Jun-2024iswomnimap 7110 The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.)
 |-  ( A  e.  V  ->  ( A  e. WOmni  <->  A. f  e.  ( 2o  ^m  A )DECID  A. x  e.  A  ( f `  x )  =  1o ) )
 
9-Jun-2024iswomni 7109 The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.)
 |-  ( A  e.  V  ->  ( A  e. WOmni  <->  A. f ( f : A --> 2o  -> DECID  A. x  e.  A  ( f `  x )  =  1o ) ) )
 
9-Jun-2024df-womni 7108 A weakly omniscient set is one where we can decide whether a predicate (here represented by a function  f) holds (is equal to  1o) for all elements or not. Generalization of definition 2.4 of [Pierik], p. 9.

In particular,  om  e. WOmni is known as the Weak Limited Principle of Omniscience (WLPO).

The term WLPO is common in the literature; there appears to be no widespread term for what we are calling a weakly omniscient set. (Contributed by Jim Kingdon, 9-Jun-2024.)

 |- WOmni  =  { y  |  A. f ( f : y --> 2o  -> DECID  A. x  e.  y  ( f `  x )  =  1o ) }
 
29-May-2024pw1nct 13617 A condition which ensures that the powerset of a singleton is not countable. The antecedent here can be referred to as the uniformity principle. Based on Mastodon posts by Andrej Bauer and Rahul Chhabra. (Contributed by Jim Kingdon, 29-May-2024.)
 |-  ( A. r ( r  C_  ( ~P 1o  X.  om )  ->  ( A. p  e.  ~P  1o E. n  e.  om  p r n 
 ->  E. m  e.  om  A. q  e.  ~P  1o q r m ) )  ->  -.  E. f  f : om -onto-> ( ~P 1o 1o ) )
 
28-May-2024sssneq 13616 Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.)
 |-  ( A  C_  { B }  ->  A. y  e.  A  A. z  e.  A  y  =  z )
 
26-May-2024elpwi2 4120 Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.)
 |-  B  e.  V   &    |-  A  C_  B   =>    |-  A  e.  ~P B
 
24-May-2024dvmptcjx 13128 Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.)
 |-  ( ( ph  /\  x  e.  X )  ->  A  e.  CC )   &    |-  ( ( ph  /\  x  e.  X ) 
 ->  B  e.  V )   &    |-  ( ph  ->  ( RR  _D  ( x  e.  X  |->  A ) )  =  ( x  e.  X  |->  B ) )   &    |-  ( ph  ->  X  C_  RR )   =>    |-  ( ph  ->  ( RR  _D  ( x  e.  X  |->  ( * `  A ) ) )  =  ( x  e.  X  |->  ( * `  B ) ) )
 
22-May-2024efltlemlt 13137 Lemma for eflt 13138. The converse of efltim 11599 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  ( exp `  A )  <  ( exp `  B ) )   &    |-  ( ph  ->  D  e.  RR+ )   &    |-  ( ph  ->  ( ( abs `  ( A  -  B ) )  <  D  ->  ( abs `  ( ( exp `  A )  -  ( exp `  B ) ) )  <  ( ( exp `  B )  -  ( exp `  A ) ) ) )   =>    |-  ( ph  ->  A  <  B )
 
21-May-2024eflt 13138 The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 21-May-2024.)
 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <-> 
 ( exp `  A )  <  ( exp `  B ) ) )
 
19-May-2024apdifflemr 13660 Lemma for apdiff 13661. (Contributed by Jim Kingdon, 19-May-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  S  e.  QQ )   &    |-  ( ph  ->  ( abs `  ( A  -  -u 1 ) ) #  ( abs `  ( A  -  1 ) ) )   &    |-  ( ( ph  /\  S  =/=  0 ) 
 ->  ( abs `  ( A  -  0 ) ) #  ( abs `  ( A  -  ( 2  x.  S ) ) ) )   =>    |-  ( ph  ->  A #  S )
 
18-May-2024apdifflemf 13659 Lemma for apdiff 13661. Being apart from the point halfway between  Q and  R suffices for  A to be a different distance from  Q and from  R. (Contributed by Jim Kingdon, 18-May-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  Q  e.  QQ )   &    |-  ( ph  ->  R  e.  QQ )   &    |-  ( ph  ->  Q  <  R )   &    |-  ( ph  ->  (
 ( Q  +  R )  /  2 ) #  A )   =>    |-  ( ph  ->  ( abs `  ( A  -  Q ) ) #  ( abs `  ( A  -  R ) ) )
 
17-May-2024apdiff 13661 The irrationals (reals apart from any rational) are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 17-May-2024.)
 |-  ( A  e.  RR  ->  (
 A. q  e.  QQ  A #  q  <->  A. q  e.  QQ  A. r  e.  QQ  (
 q  =/=  r  ->  ( abs `  ( A  -  q ) ) #  ( abs `  ( A  -  r ) ) ) ) )
 
15-May-2024reeff1oleme 13135 Lemma for reeff1o 13136. (Contributed by Jim Kingdon, 15-May-2024.)
 |-  ( U  e.  (
 0 (,) _e )  ->  E. x  e.  RR  ( exp `  x )  =  U )
 
14-May-2024df-relog 13221 Define the natural logarithm function. Defining the logarithm on complex numbers is similar to square root - there are ways to define it but they tend to make use of excluded middle. Therefore, we merely define logarithms on positive reals. See http://en.wikipedia.org/wiki/Natural_logarithm and https://en.wikipedia.org/wiki/Complex_logarithm. (Contributed by Jim Kingdon, 14-May-2024.)
 |- 
 log  =  `' ( exp  |`  RR )
 
7-May-2024ioocosf1o 13217 The cosine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014.) (Revised by Jim Kingdon, 7-May-2024.)
 |-  ( cos  |`  ( 0 (,) pi ) ) : ( 0 (,)
 pi ) -1-1-onto-> ( -u 1 (,) 1
 )
 
7-May-2024cos0pilt1 13215 Cosine is between minus one and one on the open interval between zero and  pi. (Contributed by Jim Kingdon, 7-May-2024.)
 |-  ( A  e.  (
 0 (,) pi )  ->  ( cos `  A )  e.  ( -u 1 (,) 1
 ) )
 
6-May-2024cos11 13216 Cosine is one-to-one over the closed interval from  0 to  pi. (Contributed by Paul Chapman, 16-Mar-2008.) (Revised by Jim Kingdon, 6-May-2024.)
 |-  ( ( A  e.  ( 0 [,] pi )  /\  B  e.  (
 0 [,] pi ) ) 
 ->  ( A  =  B  <->  ( cos `  A )  =  ( cos `  B ) ) )
 
5-May-2024omiunct 12215 The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 12211 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ( ph  /\  x  e.  om )  ->  E. g  g : om -onto-> ( B 1o )
 )   =>    |-  ( ph  ->  E. h  h : om -onto-> ( U_ x  e.  om  B 1o )
 )
 
5-May-2024ctiunctal 12212 Variation of ctiunct 12211 which allows  x to be present in  ph. (Contributed by Jim Kingdon, 5-May-2024.)
 |-  ( ph  ->  F : om -onto-> ( A 1o )
 )   &    |-  ( ph  ->  A. x  e.  A  G : om -onto->
 ( B 1o ) )   =>    |-  ( ph  ->  E. h  h : om -onto-> ( U_ x  e.  A  B 1o ) )
 
3-May-2024cc4n 7192 Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7191, the hypotheses only require an A(n) for each value of  n, not a single set  A which suffices for every 
n  e.  om. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  A. n  e.  N  { x  e.  A  |  ps }  e.  V )   &    |-  ( ph  ->  N  ~~  om )   &    |-  ( x  =  ( f `  n ) 
 ->  ( ps  <->  ch ) )   &    |-  ( ph  ->  A. n  e.  N  E. x  e.  A  ps )   =>    |-  ( ph  ->  E. f
 ( f  Fn  N  /\  A. n  e.  N  ch ) )
 
3-May-2024cc4f 7190 Countable choice by showing the existence of a function  f which can choose a value at each index 
n such that  ch holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  A  e.  V )   &    |-  F/_ n A   &    |-  ( ph  ->  N  ~~ 
 om )   &    |-  ( x  =  ( f `  n )  ->  ( ps  <->  ch ) )   &    |-  ( ph  ->  A. n  e.  N  E. x  e.  A  ps )   =>    |-  ( ph  ->  E. f
 ( f : N --> A  /\  A. n  e.  N  ch ) )
 
1-May-2024cc4 7191 Countable choice by showing the existence of a function  f which can choose a value at each index 
n such that  ch holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 1-May-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  N  ~~  om )   &    |-  ( x  =  ( f `  n ) 
 ->  ( ps  <->  ch ) )   &    |-  ( ph  ->  A. n  e.  N  E. x  e.  A  ps )   =>    |-  ( ph  ->  E. f
 ( f : N --> A  /\  A. n  e.  N  ch ) )
 
29-Apr-2024cc3 7189 Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  A. n  e.  N  F  e.  _V )   &    |-  ( ph  ->  A. n  e.  N  E. w  w  e.  F )   &    |-  ( ph  ->  N  ~~ 
 om )   =>    |-  ( ph  ->  E. f
 ( f  Fn  N  /\  A. n  e.  N  ( f `  n )  e.  F )
 )
 
27-Apr-2024cc2 7188 Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  F  Fn  om )   &    |-  ( ph  ->  A. x  e.  om  E. w  w  e.  ( F `  x ) )   =>    |-  ( ph  ->  E. g
 ( g  Fn  om  /\ 
 A. n  e.  om  ( g `  n )  e.  ( F `  n ) ) )
 
27-Apr-2024cc2lem 7187 Lemma for cc2 7188. (Contributed by Jim Kingdon, 27-Apr-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ph  ->  F  Fn  om )   &    |-  ( ph  ->  A. x  e.  om  E. w  w  e.  ( F `  x ) )   &    |-  A  =  ( n  e.  om  |->  ( { n }  X.  ( F `  n ) ) )   &    |-  G  =  ( n  e.  om  |->  ( 2nd `  (
 f `  ( A `  n ) ) ) )   =>    |-  ( ph  ->  E. g
 ( g  Fn  om  /\ 
 A. n  e.  om  ( g `  n )  e.  ( F `  n ) ) )
 
27-Apr-2024cc1 7186 Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.)
 |-  (CCHOICE 
 ->  A. x ( ( x  ~~  om  /\  A. z  e.  x  E. w  w  e.  z
 )  ->  E. f A. z  e.  x  ( f `  z
 )  e.  z ) )
 
19-Apr-2024omctfn 12214 Using countable choice to find a sequence of enumerations for a collection of countable sets. Lemma 8.1.27 of [AczelRathjen], p. 77. (Contributed by Jim Kingdon, 19-Apr-2024.)
 |-  ( ph  -> CCHOICE )   &    |-  ( ( ph  /\  x  e.  om )  ->  E. g  g : om -onto-> ( B 1o )
 )   =>    |-  ( ph  ->  E. f
 ( f  Fn  om  /\ 
 A. x  e.  om  ( f `  x ) : om -onto-> ( B 1o ) ) )
 
13-Apr-2024prodmodclem2 11478 Lemma for prodmodc 11479. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 13-Apr-2024.)
 |-  F  =  ( k  e.  ZZ  |->  if (
 k  e.  A ,  B ,  1 )
 )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  G  =  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  [_ ( f `  j
 )  /  k ]_ B ,  1 )
 )   =>    |-  ( ( ph  /\  E. m  e.  ZZ  (
 ( A  C_  ( ZZ>=
 `  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A ) 
 /\  ( E. n  e.  ( ZZ>= `  m ) E. y ( y #  0 
 /\  seq n (  x. 
 ,  F )  ~~>  y )  /\  seq m (  x. 
 ,  F )  ~~>  x )
 ) )  ->  ( E. m  e.  NN  E. f ( f : ( 1 ... m )
 -1-1-onto-> A  /\  z  =  ( 
 seq 1 (  x. 
 ,  G ) `  m ) )  ->  x  =  z )
 )
 
11-Apr-2024prodmodclem2a 11477 Lemma for prodmodc 11479. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.)
 |-  F  =  ( k  e.  ZZ  |->  if (
 k  e.  A ,  B ,  1 )
 )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  G  =  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  [_ ( f `  j
 )  /  k ]_ B ,  1 )
 )   &    |-  H  =  ( j  e.  NN  |->  if (
 j  <_  ( `  A ) ,  [_ ( K `
  j )  /  k ]_ B ,  1 ) )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  -> DECID  k  e.  A )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  A  C_  ( ZZ>= `  M )
 )   &    |-  ( ph  ->  f : ( 1 ...
 N ) -1-1-onto-> A )   &    |-  ( ph  ->  K 
 Isom  <  ,  <  (
 ( 1 ... ( `  A ) ) ,  A ) )   =>    |-  ( ph  ->  seq
 M (  x.  ,  F )  ~~>  (  seq 1
 (  x.  ,  G ) `  N ) )
 
11-Apr-2024prodmodclem3 11476 Lemma for prodmodc 11479. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.)
 |-  F  =  ( k  e.  ZZ  |->  if (
 k  e.  A ,  B ,  1 )
 )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  G  =  ( j  e.  NN  |->  if ( j  <_  ( `  A ) ,  [_ ( f `  j
 )  /  k ]_ B ,  1 )
 )   &    |-  H  =  ( j  e.  NN  |->  if (
 j  <_  ( `  A ) ,  [_ ( K `
  j )  /  k ]_ B ,  1 ) )   &    |-  ( ph  ->  ( M  e.  NN  /\  N  e.  NN )
 )   &    |-  ( ph  ->  f : ( 1 ...
 M ) -1-1-onto-> A )   &    |-  ( ph  ->  K : ( 1 ...
 N ) -1-1-onto-> A )   =>    |-  ( ph  ->  (  seq 1 (  x.  ,  G ) `  M )  =  (  seq 1 (  x.  ,  H ) `  N ) )
 
10-Apr-2024jcnd 642 Deduction joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Apr-2024.)
 |-  ( ph  ->  ps )   &    |-  ( ph  ->  -.  ch )   =>    |-  ( ph  ->  -.  ( ps  ->  ch ) )
 
4-Apr-2024prodrbdclem 11472 Lemma for prodrbdc 11475. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.)
 |-  F  =  ( k  e.  ZZ  |->  if (
 k  e.  A ,  B ,  1 )
 )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  -> DECID  k  e.  A )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   =>    |-  ( ( ph  /\  A  C_  ( ZZ>= `  N )
 )  ->  (  seq M (  x.  ,  F )  |`  ( ZZ>= `  N ) )  =  seq N (  x.  ,  F ) )
 
24-Mar-2024prodfdivap 11448 The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( G `  k )  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( G `  k ) #  0 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( H `  k )  =  ( ( F `  k
 )  /  ( G `  k ) ) )   =>    |-  ( ph  ->  (  seq M (  x.  ,  H ) `  N )  =  ( (  seq M (  x.  ,  F ) `
  N )  /  (  seq M (  x. 
 ,  G ) `  N ) ) )
 
24-Mar-2024prodfrecap 11447 The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( M ... N ) )  ->  ( F `
  k ) #  0 )   &    |-  ( ( ph  /\  k  e.  ( M
 ... N ) ) 
 ->  ( G `  k
 )  =  ( 1 
 /  ( F `  k ) ) )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( G `  k )  e.  CC )   =>    |-  ( ph  ->  (  seq M (  x.  ,  G ) `  N )  =  ( 1  /  (  seq M (  x.  ,  F ) `
  N ) ) )
 
23-Mar-2024prodfap0 11446 The product of finitely many terms apart from zero is apart from zero. (Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon, 23-Mar-2024.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( M ... N ) )  ->  ( F `
  k ) #  0 )   =>    |-  ( ph  ->  (  seq M (  x.  ,  F ) `  N ) #  0 )
 
22-Mar-2024prod3fmul 11442 The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( G `  k )  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( H `  k )  =  ( ( F `  k
 )  x.  ( G `
  k ) ) )   =>    |-  ( ph  ->  (  seq M (  x.  ,  H ) `  N )  =  ( (  seq M (  x.  ,  F ) `  N )  x.  (  seq M (  x.  ,  G ) `
  N ) ) )
 
21-Mar-2024df-proddc 11452 Define the product of a series with an index set of integers  A. This definition takes most of the aspects of df-sumdc 11255 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 21-Mar-2024.)
 |- 
 prod_ k  e.  A  B  =  ( iota x ( E. m  e. 
 ZZ  ( ( A 
 C_  ( ZZ>= `  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A )  /\  ( E. n  e.  ( ZZ>=
 `  m ) E. y ( y #  0 
 /\  seq n (  x. 
 ,  ( k  e. 
 ZZ  |->  if ( k  e.  A ,  B , 
 1 ) ) )  ~~>  y )  /\  seq m (  x.  ,  ( k  e.  ZZ  |->  if (
 k  e.  A ,  B ,  1 )
 ) )  ~~>  x )
 )  \/  E. m  e.  NN  E. f ( f : ( 1
 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  x.  ,  ( n  e.  NN  |->  if ( n  <_  m ,  [_ ( f `  n )  /  k ]_ B ,  1 ) ) ) `  m ) ) ) )
 
19-Mar-2024cos02pilt1 13214 Cosine is less than one between zero and  2  x.  pi. (Contributed by Jim Kingdon, 19-Mar-2024.)
 |-  ( A  e.  (
 0 (,) ( 2  x.  pi ) )  ->  ( cos `  A )  <  1 )
 
19-Mar-2024cosq34lt1 13213 Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.)
 |-  ( A  e.  ( pi [,) ( 2  x.  pi ) )  ->  ( cos `  A )  <  1 )
 
14-Mar-2024coseq0q4123 13197 Location of the zeroes of cosine in  ( -u (
pi  /  2 ) (,) ( 3  x.  ( pi  /  2
) ) ). (Contributed by Jim Kingdon, 14-Mar-2024.)
 |-  ( A  e.  ( -u ( pi  /  2
 ) (,) ( 3  x.  ( pi  /  2
 ) ) )  ->  ( ( cos `  A )  =  0  <->  A  =  ( pi  /  2 ) ) )
 
14-Mar-2024cosq23lt0 13196 The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.)
 |-  ( A  e.  (
 ( pi  /  2
 ) (,) ( 3  x.  ( pi  /  2
 ) ) )  ->  ( cos `  A )  <  0 )
 
9-Mar-2024pilem3 13146 Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.)
 |-  ( pi  e.  (
 2 (,) 4 )  /\  ( sin `  pi )  =  0 )
 
9-Mar-2024exmidonfin 7130 If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 6818 and nnon 4570. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
 |-  ( om  =  ( On  i^i  Fin )  -> EXMID )
 
9-Mar-2024exmidonfinlem 7129 Lemma for exmidonfin 7130. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
 |-  A  =  { { x  e.  { (/) }  |  ph
 } ,  { x  e.  { (/) }  |  -.  ph
 } }   =>    |-  ( om  =  ( On  i^i  Fin )  -> DECID  ph )
 
8-Mar-2024sin0pilem2 13145 Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
 |- 
 E. q  e.  (
 2 (,) 4 ) ( ( sin `  q
 )  =  0  /\  A. x  e.  ( 0 (,) q ) 0  <  ( sin `  x ) )
 
8-Mar-2024sin0pilem1 13144 Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
 |- 
 E. p  e.  (
 1 (,) 2 ) ( ( cos `  p )  =  0  /\  A. x  e.  ( p (,) ( 2  x.  p ) ) 0  <  ( sin `  x ) )
 
7-Mar-2024cosz12 13143 Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.)
 |- 
 E. p  e.  (
 1 (,) 2 ) ( cos `  p )  =  0
 
6-Mar-2024cos12dec 11668 Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.)
 |-  ( ( A  e.  ( 1 [,] 2
 )  /\  B  e.  ( 1 [,] 2
 )  /\  A  <  B )  ->  ( cos `  B )  <  ( cos `  A ) )
 
25-Feb-2024mul2lt0pn 9672 The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  0
 )   &    |-  ( ph  ->  0  <  B )   =>    |-  ( ph  ->  ( B  x.  A )  < 
 0 )
 
25-Feb-2024mul2lt0np 9671 The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  0
 )   &    |-  ( ph  ->  0  <  B )   =>    |-  ( ph  ->  ( A  x.  B )  < 
 0 )
 
25-Feb-2024lt0ap0 8524 A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
 |-  ( ( A  e.  RR  /\  A  <  0
 )  ->  A #  0
 )
 
25-Feb-2024negap0d 8507 The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A #  0 )   =>    |-  ( ph  ->  -u A #  0 )
 
24-Feb-2024lt0ap0d 8525 A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  0 )   =>    |-  ( ph  ->  A #  0 )
 
20-Feb-2024ivthdec 13064 The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  B )  <  U  /\  U  <  ( F `  A ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  y )  <  ( F `  x ) )   =>    |-  ( ph  ->  E. c  e.  ( A (,) B ) ( F `  c )  =  U )
 
20-Feb-2024ivthinclemex 13062 Lemma for ivthinc 13063. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  A )  <  U  /\  U  <  ( F `  B ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  x )  <  ( F `  y ) )   &    |-  L  =  { w  e.  ( A [,] B )  |  ( F `  w )  <  U }   &    |-  R  =  { w  e.  ( A [,] B )  |  U  <  ( F `
  w ) }   =>    |-  ( ph  ->  E! z  e.  ( A (,) B ) ( A. q  e.  L  q  <  z  /\  A. r  e.  R  z  <  r ) )
 
19-Feb-2024ivthinclemuopn 13058 Lemma for ivthinc 13063. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  A )  <  U  /\  U  <  ( F `  B ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  x )  <  ( F `  y ) )   &    |-  L  =  { w  e.  ( A [,] B )  |  ( F `  w )  <  U }   &    |-  R  =  { w  e.  ( A [,] B )  |  U  <  ( F `
  w ) }   &    |-  ( ph  ->  S  e.  R )   =>    |-  ( ph  ->  E. q  e.  R  q  <  S )
 
19-Feb-2024dedekindicc 13053 A Dedekind cut identifies a unique real number. Similar to df-inp 7387 except that the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 19-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  L  C_  ( A [,] B ) )   &    |-  ( ph  ->  U  C_  ( A [,] B ) )   &    |-  ( ph  ->  E. q  e.  ( A [,] B ) q  e.  L )   &    |-  ( ph  ->  E. r  e.  ( A [,] B ) r  e.  U )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) ( q  e.  L  <->  E. r  e.  L  q  <  r ) )   &    |-  ( ph  ->  A. r  e.  ( A [,] B ) ( r  e.  U  <->  E. q  e.  U  q  <  r ) )   &    |-  ( ph  ->  ( L  i^i  U )  =  (/) )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) A. r  e.  ( A [,] B ) ( q  <  r  ->  ( q  e.  L  \/  r  e.  U ) ) )   &    |-  ( ph  ->  A  <  B )   =>    |-  ( ph  ->  E! x  e.  ( A (,) B ) ( A. q  e.  L  q  <  x  /\  A. r  e.  U  x  <  r
 ) )
 
18-Feb-2024ivthinclemloc 13061 Lemma for ivthinc 13063. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  A )  <  U  /\  U  <  ( F `  B ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  x )  <  ( F `  y ) )   &    |-  L  =  { w  e.  ( A [,] B )  |  ( F `  w )  <  U }   &    |-  R  =  { w  e.  ( A [,] B )  |  U  <  ( F `
  w ) }   =>    |-  ( ph  ->  A. q  e.  ( A [,] B ) A. r  e.  ( A [,] B ) ( q  <  r  ->  (
 q  e.  L  \/  r  e.  R )
 ) )
 
18-Feb-2024ivthinclemdisj 13060 Lemma for ivthinc 13063. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  A )  <  U  /\  U  <  ( F `  B ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  x )  <  ( F `  y ) )   &    |-  L  =  { w  e.  ( A [,] B )  |  ( F `  w )  <  U }   &    |-  R  =  { w  e.  ( A [,] B )  |  U  <  ( F `
  w ) }   =>    |-  ( ph  ->  ( L  i^i  R )  =  (/) )
 
18-Feb-2024ivthinclemur 13059 Lemma for ivthinc 13063. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  A )  <  U  /\  U  <  ( F `  B ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  x )  <  ( F `  y ) )   &    |-  L  =  { w  e.  ( A [,] B )  |  ( F `  w )  <  U }   &    |-  R  =  { w  e.  ( A [,] B )  |  U  <  ( F `
  w ) }   =>    |-  ( ph  ->  A. r  e.  ( A [,] B ) ( r  e.  R  <->  E. q  e.  R  q  <  r ) )
 
18-Feb-2024ivthinclemlr 13057 Lemma for ivthinc 13063. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  A )  <  U  /\  U  <  ( F `  B ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  x )  <  ( F `  y ) )   &    |-  L  =  { w  e.  ( A [,] B )  |  ( F `  w )  <  U }   &    |-  R  =  { w  e.  ( A [,] B )  |  U  <  ( F `
  w ) }   =>    |-  ( ph  ->  A. q  e.  ( A [,] B ) ( q  e.  L  <->  E. r  e.  L  q  <  r ) )
 
18-Feb-2024ivthinclemum 13055 Lemma for ivthinc 13063. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  A )  <  U  /\  U  <  ( F `  B ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  x )  <  ( F `  y ) )   &    |-  L  =  { w  e.  ( A [,] B )  |  ( F `  w )  <  U }   &    |-  R  =  { w  e.  ( A [,] B )  |  U  <  ( F `
  w ) }   =>    |-  ( ph  ->  E. r  e.  ( A [,] B ) r  e.  R )
 
18-Feb-2024ivthinclemlm 13054 Lemma for ivthinc 13063. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  A )  <  U  /\  U  <  ( F `  B ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  x )  <  ( F `  y ) )   &    |-  L  =  { w  e.  ( A [,] B )  |  ( F `  w )  <  U }   &    |-  R  =  { w  e.  ( A [,] B )  |  U  <  ( F `
  w ) }   =>    |-  ( ph  ->  E. q  e.  ( A [,] B ) q  e.  L )
 
15-Feb-2024dedekindicclemeu 13051 Lemma for dedekindicc 13053. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  L  C_  ( A [,] B ) )   &    |-  ( ph  ->  U  C_  ( A [,] B ) )   &    |-  ( ph  ->  E. q  e.  ( A [,] B ) q  e.  L )   &    |-  ( ph  ->  E. r  e.  ( A [,] B ) r  e.  U )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) ( q  e.  L  <->  E. r  e.  L  q  <  r ) )   &    |-  ( ph  ->  A. r  e.  ( A [,] B ) ( r  e.  U  <->  E. q  e.  U  q  <  r ) )   &    |-  ( ph  ->  ( L  i^i  U )  =  (/) )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) A. r  e.  ( A [,] B ) ( q  <  r  ->  ( q  e.  L  \/  r  e.  U ) ) )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  C  e.  ( A [,] B ) )   &    |-  ( ph  ->  (
 A. q  e.  L  q  <  C  /\  A. r  e.  U  C  <  r ) )   &    |-  ( ph  ->  D  e.  ( A [,] B ) )   &    |-  ( ph  ->  ( A. q  e.  L  q  <  D  /\  A. r  e.  U  D  <  r
 ) )   &    |-  ( ph  ->  C  <  D )   =>    |-  ( ph  -> F.  )
 
15-Feb-2024dedekindicclemlu 13050 Lemma for dedekindicc 13053. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  L  C_  ( A [,] B ) )   &    |-  ( ph  ->  U  C_  ( A [,] B ) )   &    |-  ( ph  ->  E. q  e.  ( A [,] B ) q  e.  L )   &    |-  ( ph  ->  E. r  e.  ( A [,] B ) r  e.  U )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) ( q  e.  L  <->  E. r  e.  L  q  <  r ) )   &    |-  ( ph  ->  A. r  e.  ( A [,] B ) ( r  e.  U  <->  E. q  e.  U  q  <  r ) )   &    |-  ( ph  ->  ( L  i^i  U )  =  (/) )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) A. r  e.  ( A [,] B ) ( q  <  r  ->  ( q  e.  L  \/  r  e.  U ) ) )   &    |-  ( ph  ->  A  <  B )   =>    |-  ( ph  ->  E. x  e.  ( A [,] B ) ( A. q  e.  L  q  <  x  /\  A. r  e.  U  x  <  r ) )
 
15-Feb-2024dedekindicclemlub 13049 Lemma for dedekindicc 13053. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  L  C_  ( A [,] B ) )   &    |-  ( ph  ->  U  C_  ( A [,] B ) )   &    |-  ( ph  ->  E. q  e.  ( A [,] B ) q  e.  L )   &    |-  ( ph  ->  E. r  e.  ( A [,] B ) r  e.  U )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) ( q  e.  L  <->  E. r  e.  L  q  <  r ) )   &    |-  ( ph  ->  A. r  e.  ( A [,] B ) ( r  e.  U  <->  E. q  e.  U  q  <  r ) )   &    |-  ( ph  ->  ( L  i^i  U )  =  (/) )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) A. r  e.  ( A [,] B ) ( q  <  r  ->  ( q  e.  L  \/  r  e.  U ) ) )   &    |-  ( ph  ->  A  <  B )   =>    |-  ( ph  ->  E. x  e.  ( A [,] B ) ( A. y  e.  L  -.  x  < 
 y  /\  A. y  e.  ( A [,] B ) ( y  < 
 x  ->  E. z  e.  L  y  <  z
 ) ) )
 
15-Feb-2024dedekindicclemloc 13048 Lemma for dedekindicc 13053. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  L  C_  ( A [,] B ) )   &    |-  ( ph  ->  U  C_  ( A [,] B ) )   &    |-  ( ph  ->  E. q  e.  ( A [,] B ) q  e.  L )   &    |-  ( ph  ->  E. r  e.  ( A [,] B ) r  e.  U )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) ( q  e.  L  <->  E. r  e.  L  q  <  r ) )   &    |-  ( ph  ->  A. r  e.  ( A [,] B ) ( r  e.  U  <->  E. q  e.  U  q  <  r ) )   &    |-  ( ph  ->  ( L  i^i  U )  =  (/) )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) A. r  e.  ( A [,] B ) ( q  <  r  ->  ( q  e.  L  \/  r  e.  U ) ) )   =>    |-  ( ph  ->  A. x  e.  ( A [,] B ) A. y  e.  ( A [,] B ) ( x  <  y  ->  ( E. z  e.  L  x  <  z  \/  A. z  e.  L  z  <  y ) ) )
 
15-Feb-2024dedekindicclemub 13047 Lemma for dedekindicc 13053. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  L  C_  ( A [,] B ) )   &    |-  ( ph  ->  U  C_  ( A [,] B ) )   &    |-  ( ph  ->  E. q  e.  ( A [,] B ) q  e.  L )   &    |-  ( ph  ->  E. r  e.  ( A [,] B ) r  e.  U )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) ( q  e.  L  <->  E. r  e.  L  q  <  r ) )   &    |-  ( ph  ->  A. r  e.  ( A [,] B ) ( r  e.  U  <->  E. q  e.  U  q  <  r ) )   &    |-  ( ph  ->  ( L  i^i  U )  =  (/) )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) A. r  e.  ( A [,] B ) ( q  <  r  ->  ( q  e.  L  \/  r  e.  U ) ) )   =>    |-  ( ph  ->  E. x  e.  ( A [,] B ) A. y  e.  L  y  <  x )
 
15-Feb-2024dedekindicclemuub 13046 Lemma for dedekindicc 13053. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 15-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  L  C_  ( A [,] B ) )   &    |-  ( ph  ->  U  C_  ( A [,] B ) )   &    |-  ( ph  ->  E. q  e.  ( A [,] B ) q  e.  L )   &    |-  ( ph  ->  E. r  e.  ( A [,] B ) r  e.  U )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) ( q  e.  L  <->  E. r  e.  L  q  <  r ) )   &    |-  ( ph  ->  A. r  e.  ( A [,] B ) ( r  e.  U  <->  E. q  e.  U  q  <  r ) )   &    |-  ( ph  ->  ( L  i^i  U )  =  (/) )   &    |-  ( ph  ->  A. q  e.  ( A [,] B ) A. r  e.  ( A [,] B ) ( q  <  r  ->  ( q  e.  L  \/  r  e.  U ) ) )   &    |-  ( ph  ->  C  e.  U )   =>    |-  ( ph  ->  A. z  e.  L  z  <  C )
 
14-Feb-2024suplociccex 13045 An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7951 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
 |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  B  <  C )   &    |-  ( ph  ->  A  C_  ( B [,] C ) )   &    |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  A. x  e.  ( B [,] C ) A. y  e.  ( B [,] C ) ( x  <  y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )   =>    |-  ( ph  ->  E. x  e.  ( B [,] C ) ( A. y  e.  A  -.  x  < 
 y  /\  A. y  e.  ( B [,] C ) ( y  < 
 x  ->  E. z  e.  A  y  <  z
 ) ) )
 
14-Feb-2024suplociccreex 13044 An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7951 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
 |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  C  e.  RR )   &    |-  ( ph  ->  B  <  C )   &    |-  ( ph  ->  A  C_  ( B [,] C ) )   &    |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  A. x  e.  ( B [,] C ) A. y  e.  ( B [,] C ) ( x  <  y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )   =>    |-  ( ph  ->  E. x  e.  RR  ( A. y  e.  A  -.  x  < 
 y  /\  A. y  e. 
 RR  ( y  < 
 x  ->  E. z  e.  A  y  <  z
 ) ) )
 
6-Feb-2024ivthinclemlopn 13056 Lemma for ivthinc 13063. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  A )  <  U  /\  U  <  ( F `  B ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  x )  <  ( F `  y ) )   &    |-  L  =  { w  e.  ( A [,] B )  |  ( F `  w )  <  U }   &    |-  R  =  { w  e.  ( A [,] B )  |  U  <  ( F `
  w ) }   &    |-  ( ph  ->  Q  e.  L )   =>    |-  ( ph  ->  E. r  e.  L  Q  <  r
 )
 
5-Feb-2024ivthinc 13063 The intermediate value theorem, increasing case, for a strictly monotonic function. Theorem 5.5 of [Bauer], p. 494. This is Metamath 100 proof #79. (Contributed by Jim Kingdon, 5-Feb-2024.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  U  e.  RR )   &    |-  ( ph  ->  A  <  B )   &    |-  ( ph  ->  ( A [,] B ) 
 C_  D )   &    |-  ( ph  ->  F  e.  ( D -cn-> CC ) )   &    |-  (
 ( ph  /\  x  e.  ( A [,] B ) )  ->  ( F `
  x )  e. 
 RR )   &    |-  ( ph  ->  ( ( F `  A )  <  U  /\  U  <  ( F `  B ) ) )   &    |-  (
 ( ( ph  /\  x  e.  ( A [,] B ) )  /\  ( y  e.  ( A [,] B )  /\  x  < 
 y ) )  ->  ( F `  x )  <  ( F `  y ) )   =>    |-  ( ph  ->  E. c  e.  ( A (,) B ) ( F `  c )  =  U )
 
2-Feb-2024dedekindeulemuub 13037 Lemma for dedekindeu 13043. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
 |-  ( ph  ->  L  C_ 
 RR )   &    |-  ( ph  ->  U 
 C_  RR )   &    |-  ( ph  ->  E. q  e.  RR  q  e.  L )   &    |-  ( ph  ->  E. r  e.  RR  r  e.  U )   &    |-  ( ph  ->  A. q  e.  RR  (
 q  e.  L  <->  E. r  e.  L  q  <  r ) )   &    |-  ( ph  ->  A. r  e. 
 RR  ( r  e.  U  <->  E. q  e.  U  q  <  r ) )   &    |-  ( ph  ->  ( L  i^i  U )  =  (/) )   &    |-  ( ph  ->  A. q  e.  RR  A. r  e. 
 RR  ( q  < 
 r  ->  ( q  e.  L  \/  r  e.  U ) ) )   &    |-  ( ph  ->  A  e.  U )   =>    |-  ( ph  ->  A. z  e.  L  z  <  A )
 
31-Jan-2024dedekindeulemeu 13042 Lemma for dedekindeu 13043. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.)
 |-  ( ph  ->  L  C_ 
 RR )   &    |-  ( ph  ->  U 
 C_  RR )   &    |-  ( ph  ->  E. q  e.  RR  q  e.  L )   &    |-  ( ph  ->  E. r  e.  RR  r  e.  U )   &    |-  ( ph  ->  A. q  e.  RR  (
 q  e.  L  <->  E. r  e.  L  q  <  r ) )   &    |-  ( ph  ->  A. r  e. 
 RR  ( r  e.  U  <->  E. q  e.  U  q  <  r ) )   &    |-  ( ph  ->  ( L  i^i  U )  =  (/) )   &    |-  ( ph  ->  A. q  e.  RR  A. r  e. 
 RR  ( q  < 
 r  ->  ( q  e.  L  \/  r  e.  U ) ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  (
 A. q  e.  L  q  <  A  /\  A. r  e.  U  A  <  r ) )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  ( A. q  e.  L  q  <  B  /\  A. r  e.  U  B  <  r ) )   &    |-  ( ph  ->  A  <  B )   =>    |-  ( ph  -> F.  )
 
31-Jan-2024dedekindeulemlu 13041 Lemma for dedekindeu 13043. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
 |-  ( ph  ->  L  C_ 
 RR )   &    |-  ( ph  ->  U 
 C_  RR )   &    |-