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 22-Oct-2021 at 12:36 PM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
20-Oct-2021onunsnss 6355 Adding a singleton to create an ordinal. (Contributed by Jim Kingdon, 20-Oct-2021.)
 |-  ( ( B  e.  V  /\  ( A  u.  { B } )  e. 
 On )  ->  B  C_  A )
 
19-Oct-2021snon0 6356 An ordinal which is a singleton is  { (/) }. (Contributed by Jim Kingdon, 19-Oct-2021.)
 |-  ( ( A  e.  V  /\  { A }  e.  On )  ->  A  =  (/) )
 
18-Oct-2021qdencn 10123 The set of complex numbers whose real and imaginary parts are rational is dense in the complex plane. This is a two dimensional analogue to qdenre 9798 (and also would hold for  RR  X.  RR with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  Q  =  { z  e.  CC  |  ( ( Re `  z )  e.  QQ  /\  ( Im `  z
 )  e.  QQ ) }   =>    |-  ( ( A  e.  CC  /\  B  e.  RR+ )  ->  E. x  e.  Q  ( abs `  ( x  -  A ) )  <  B )
 
18-Oct-2021modqmulnn 9184 Move a positive integer in and out of a floor in the first argument of a modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( ( N  e.  NN  /\  A  e.  QQ  /\  M  e.  NN )  ->  ( ( N  x.  ( |_ `  A ) )  mod  ( N  x.  M ) ) 
 <_  ( ( |_ `  ( N  x.  A ) ) 
 mod  ( N  x.  M ) ) )
 
18-Oct-2021intqfrac 9181 Break a number into its integer part and its fractional part. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( A  e.  QQ  ->  A  =  ( ( |_ `  A )  +  ( A  mod  1 ) ) )
 
18-Oct-2021flqmod 9180 The floor function expressed in terms of the modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( |_ `  A )  =  ( A  -  ( A  mod  1
 ) ) )
 
18-Oct-2021modqfrac 9179 The fractional part of a number is the number modulo 1. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( A  mod  1
 )  =  ( A  -  ( |_ `  A ) ) )
 
18-Oct-2021modqdifz 9178 The modulo operation differs from 
A by an integer multiple of  B. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  ( ( A  -  ( A  mod  B ) )  /  B )  e.  ZZ )
 
18-Oct-2021modqdiffl 9177 The modulo operation differs from 
A by an integer multiple of  B. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  ( ( A  -  ( A  mod  B ) )  /  B )  =  ( |_ `  ( A  /  B ) ) )
 
18-Oct-2021modqelico 9176 Modular reduction produces a half-open interval. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  ( A  mod  B )  e.  ( 0 [,) B ) )
 
18-Oct-2021modqlt 9175 The modulo operation is less than its second argument. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  ( A  mod  B )  <  B )
 
18-Oct-2021modqge0 9174 The modulo operation is nonnegative. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  0  <_  ( A 
 mod  B ) )
 
18-Oct-2021negqmod0 9173  A is divisible by  B iff its negative is. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  ( ( A  mod  B )  =  0  <->  ( -u A  mod  B )  =  0 ) )
 
18-Oct-2021mulqmod0 9172 The product of an integer and a positive rational number is 0 modulo the positive real number. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( ( A  e.  ZZ  /\  M  e.  QQ  /\  0  <  M ) 
 ->  ( ( A  x.  M )  mod  M )  =  0 )
 
18-Oct-2021flqdiv 9163 Cancellation of the embedded floor of a real divided by an integer. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  N  e.  NN )  ->  ( |_ `  (
 ( |_ `  A )  /  N ) )  =  ( |_ `  ( A  /  N ) ) )
 
18-Oct-2021intqfrac2 9161 Decompose a real into integer and fractional parts. (Contributed by Jim Kingdon, 18-Oct-2021.)
 |-  Z  =  ( |_ `  A )   &    |-  F  =  ( A  -  Z )   =>    |-  ( A  e.  QQ  ->  ( 0  <_  F  /\  F  <  1  /\  A  =  ( Z  +  F ) ) )
 
17-Oct-2021modq0 9171  A  mod  B is zero iff  A is evenly divisible by  B. (Contributed by Jim Kingdon, 17-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  ( ( A  mod  B )  =  0  <->  ( A  /  B )  e.  ZZ ) )
 
16-Oct-2021modqcld 9170 Closure law for the modulo operation. (Contributed by Jim Kingdon, 16-Oct-2021.)
 |-  ( ph  ->  A  e.  QQ )   &    |-  ( ph  ->  B  e.  QQ )   &    |-  ( ph  ->  0  <  B )   =>    |-  ( ph  ->  ( A  mod  B )  e. 
 QQ )
 
16-Oct-2021flqpmodeq 9169 Partition of a division into its integer part and the remainder. (Contributed by Jim Kingdon, 16-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  ( ( ( |_ `  ( A  /  B ) )  x.  B )  +  ( A  mod  B ) )  =  A )
 
16-Oct-2021modqcl 9168 Closure law for the modulo operation. (Contributed by Jim Kingdon, 16-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  ( A  mod  B )  e.  QQ )
 
16-Oct-2021modqvalr 9167 The value of the modulo operation (multiplication in reversed order). (Contributed by Jim Kingdon, 16-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  ( A  mod  B )  =  ( A  -  ( ( |_ `  ( A  /  B ) )  x.  B ) ) )
 
16-Oct-2021modqval 9166 The value of the modulo operation. The modulo congruence notation of number theory,  J  ==  K (modulo  N), can be expressed in our notation as  ( J  mod  N )  =  ( K  mod  N ). Definition 1 in Knuth, The Art of Computer Programming, Vol. I (1972), p. 38. Knuth uses "mod" for the operation and "modulo" for the congruence. Unlike Knuth, we restrict the second argument to positive numbers to simplify certain theorems. (This also gives us future flexibility to extend it to any one of several different conventions for a zero or negative second argument, should there be an advantage in doing so.) As with flqcl 9117 we only prove this for rationals although other particular kinds of real numbers may be possible. (Contributed by Jim Kingdon, 16-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  0  <  B ) 
 ->  ( A  mod  B )  =  ( A  -  ( B  x.  ( |_ `  ( A  /  B ) ) ) ) )
 
15-Oct-2021qdenre 9798 The rational numbers are dense in 
RR: any real number can be approximated with arbitrary precision by a rational number. For order theoretic density, see qbtwnre 9111. (Contributed by BJ, 15-Oct-2021.)
 |-  ( ( A  e.  RR  /\  B  e.  RR+ )  ->  E. x  e.  QQ  ( abs `  ( x  -  A ) )  <  B )
 
14-Oct-2021qbtwnrelemcalc 9110 Lemma for qbtwnre 9111. Calculations involved in showing the constructed rational number is less than 
B. (Contributed by Jim Kingdon, 14-Oct-2021.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  M  <  ( A  x.  ( 2  x.  N ) ) )   &    |-  ( ph  ->  ( 1  /  N )  <  ( B  -  A ) )   =>    |-  ( ph  ->  ( ( M  +  2 )  /  ( 2  x.  N ) )  <  B )
 
13-Oct-2021rebtwn2z 9109 A real number can be bounded by integers above and below which are two apart.

The proof starts by finding two integers which are less than and greater than the given real number. Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on weak linearity, and iterating until the range consists of integers which are two apart. (Contributed by Jim Kingdon, 13-Oct-2021.)

 |-  ( A  e.  RR  ->  E. x  e.  ZZ  ( x  <  A  /\  A  <  ( x  +  2 ) ) )
 
13-Oct-2021rebtwn2zlemshrink 9108 Lemma for rebtwn2z 9109. Shrinking the range around the given real number. (Contributed by Jim Kingdon, 13-Oct-2021.)
 |-  ( ( A  e.  RR  /\  J  e.  ( ZZ>=
 `  2 )  /\  E. m  e.  ZZ  ( m  <  A  /\  A  <  ( m  +  J ) ) )  ->  E. x  e.  ZZ  ( x  <  A  /\  A  <  ( x  +  2 ) ) )
 
13-Oct-2021rebtwn2zlemstep 9107 Lemma for rebtwn2z 9109. Induction step. (Contributed by Jim Kingdon, 13-Oct-2021.)
 |-  ( ( K  e.  ( ZZ>= `  2 )  /\  A  e.  RR  /\  E. m  e.  ZZ  ( m  <  A  /\  A  <  ( m  +  ( K  +  1 )
 ) ) )  ->  E. m  e.  ZZ  ( m  <  A  /\  A  <  ( m  +  K ) ) )
 
11-Oct-2021flqeqceilz 9160 A rational number is an integer iff its floor equals its ceiling. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( A  e.  ZZ  <->  ( |_ `  A )  =  ( `  A )
 ) )
 
11-Oct-2021flqleceil 9159 The floor of a rational number is less than or equal to its ceiling. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( |_ `  A )  <_  ( `  A )
 )
 
11-Oct-2021ceilqidz 9158 A rational number equals its ceiling iff it is an integer. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( A  e.  ZZ  <->  ( `  A )  =  A ) )
 
11-Oct-2021ceilqle 9156 The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  ZZ  /\  A  <_  B )  ->  ( `  A )  <_  B )
 
11-Oct-2021ceiqle 9155 The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  ZZ  /\  A  <_  B )  -> 
 -u ( |_ `  -u A )  <_  B )
 
11-Oct-2021ceilqm1lt 9154 One less than the ceiling of a real number is strictly less than that number. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( ( `  A )  -  1 )  <  A )
 
11-Oct-2021ceiqm1l 9153 One less than the ceiling of a real number is strictly less than that number. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( -u ( |_ `  -u A )  -  1 )  <  A )
 
11-Oct-2021ceilqge 9152 The ceiling of a real number is greater than or equal to that number. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( A  e.  QQ  ->  A  <_  ( `  A ) )
 
11-Oct-2021ceiqge 9151 The ceiling of a real number is greater than or equal to that number. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( A  e.  QQ  ->  A  <_  -u ( |_ `  -u A ) )
 
11-Oct-2021ceilqcl 9150 Closure of the ceiling function. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( `  A )  e.  ZZ )
 
11-Oct-2021ceiqcl 9149 The ceiling function returns an integer (closure law). (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( A  e.  QQ  -> 
 -u ( |_ `  -u A )  e.  ZZ )
 
11-Oct-2021qdceq 9102 Equality of rationals is decidable. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ )  -> DECID  A  =  B )
 
11-Oct-2021qltlen 8575 Rational 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7621 which is a similar result for real numbers. (Contributed by Jim Kingdon, 11-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ )  ->  ( A  <  B  <-> 
 ( A  <_  B  /\  B  =/=  A ) ) )
 
10-Oct-2021ceilqval 9148 The value of the ceiling function. (Contributed by Jim Kingdon, 10-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( `  A )  =  -u ( |_ `  -u A ) )
 
10-Oct-2021flqmulnn0 9141 Move a nonnegative integer in and out of a floor. (Contributed by Jim Kingdon, 10-Oct-2021.)
 |-  ( ( N  e.  NN0  /\  A  e.  QQ )  ->  ( N  x.  ( |_ `  A ) ) 
 <_  ( |_ `  ( N  x.  A ) ) )
 
10-Oct-2021flqzadd 9140 An integer can be moved in and out of the floor of a sum. (Contributed by Jim Kingdon, 10-Oct-2021.)
 |-  ( ( N  e.  ZZ  /\  A  e.  QQ )  ->  ( |_ `  ( N  +  A )
 )  =  ( N  +  ( |_ `  A ) ) )
 
10-Oct-2021flqaddz 9139 An integer can be moved in and out of the floor of a sum. (Contributed by Jim Kingdon, 10-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  N  e.  ZZ )  ->  ( |_ `  ( A  +  N )
 )  =  ( ( |_ `  A )  +  N ) )
 
10-Oct-2021flqge1nn 9136 The floor of a number greater than or equal to 1 is a positive integer. (Contributed by Jim Kingdon, 10-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  1  <_  A )  ->  ( |_ `  A )  e.  NN )
 
10-Oct-2021flqge0nn0 9135 The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by Jim Kingdon, 10-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  0  <_  A )  ->  ( |_ `  A )  e.  NN0 )
 
10-Oct-20214ap0 8015 The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
 |-  4 #  0
 
10-Oct-20213ap0 8012 The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.)
 |-  3 #  0
 
9-Oct-2021flqbi2 9133 A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.)
 |-  ( ( N  e.  ZZ  /\  F  e.  QQ )  ->  ( ( |_ `  ( N  +  F ) )  =  N  <->  ( 0  <_  F  /\  F  <  1 ) ) )
 
9-Oct-2021flqbi 9132 A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  ZZ )  ->  ( ( |_ `  A )  =  B  <->  ( B  <_  A  /\  A  <  ( B  +  1 ) ) ) )
 
9-Oct-2021flqword2 9131 Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  A  <_  B )  ->  ( |_ `  B )  e.  ( ZZ>= `  ( |_ `  A ) ) )
 
9-Oct-2021flqwordi 9130 Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ  /\  A  <_  B )  ->  ( |_ `  A )  <_  ( |_ `  B ) )
 
9-Oct-2021flqltnz 9129 If A is not an integer, then the floor of A is less than A. (Contributed by Jim Kingdon, 9-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  -.  A  e.  ZZ )  ->  ( |_ `  A )  <  A )
 
9-Oct-2021flqidz 9128 A rational number equals its floor iff it is an integer. (Contributed by Jim Kingdon, 9-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( ( |_ `  A )  =  A  <->  A  e.  ZZ ) )
 
8-Oct-2021flqidm 9127 The floor function is idempotent. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( |_ `  ( |_ `  A ) )  =  ( |_ `  A ) )
 
8-Oct-2021flqlt 9125 The floor function value is less than the next integer. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  ZZ )  ->  ( A  <  B  <-> 
 ( |_ `  A )  <  B ) )
 
8-Oct-2021flqge 9124 The floor function value is the greatest integer less than or equal to its argument. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  ZZ )  ->  ( B  <_  A  <->  B  <_  ( |_ `  A ) ) )
 
8-Oct-2021qfracge0 9123 The fractional part of a rational number is nonnegative. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( A  e.  QQ  ->  0  <_  ( A  -  ( |_ `  A ) ) )
 
8-Oct-2021qfraclt1 9122 The fractional part of a rational number is less than one. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( A  -  ( |_ `  A ) )  <  1 )
 
8-Oct-2021flqltp1 9121 A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( A  e.  QQ  ->  A  <  ( ( |_ `  A )  +  1 ) )
 
8-Oct-2021flqle 9120 A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( |_ `  A )  <_  A )
 
8-Oct-2021flqcld 9119 The floor (greatest integer) function is an integer (closure law). (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( ph  ->  A  e.  QQ )   =>    |-  ( ph  ->  ( |_ `  A )  e. 
 ZZ )
 
8-Oct-2021flqlelt 9118 A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( ( |_ `  A )  <_  A  /\  A  <  ( ( |_ `  A )  +  1 )
 ) )
 
8-Oct-2021flqcl 9117 The floor (greatest integer) function yields an integer when applied to a rational (closure law). It would presumably be possible to prove a similar result for some real numbers (for example, those apart from any integer), but not real numbers in general. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( A  e.  QQ  ->  ( |_ `  A )  e.  ZZ )
 
8-Oct-2021qbtwnz 9106 There is a unique greatest integer less than or equal to a rational number. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( A  e.  QQ  ->  E! x  e.  ZZ  ( x  <_  A  /\  A  <  ( x  +  1 ) ) )
 
8-Oct-2021qbtwnzlemex 9105 Lemma for qbtwnz 9106. Existence of the integer.

The proof starts by finding two integers which are less than and greater than the given rational number. Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on rational number trichotomy, and iterating until the range consists of two consecutive integers. (Contributed by Jim Kingdon, 8-Oct-2021.)

 |-  ( A  e.  QQ  ->  E. x  e.  ZZ  ( x  <_  A  /\  A  <  ( x  +  1 ) ) )
 
8-Oct-2021qbtwnzlemshrink 9104 Lemma for qbtwnz 9106. Shrinking the range around the given rational number. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  J  e.  NN  /\ 
 E. m  e.  ZZ  ( m  <_  A  /\  A  <  ( m  +  J ) ) ) 
 ->  E. x  e.  ZZ  ( x  <_  A  /\  A  <  ( x  +  1 ) ) )
 
8-Oct-2021qbtwnzlemstep 9103 Lemma for qbtwnz 9106. Induction step. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( ( K  e.  NN  /\  A  e.  QQ  /\ 
 E. m  e.  ZZ  ( m  <_  A  /\  A  <  ( m  +  ( K  +  1
 ) ) ) ) 
 ->  E. m  e.  ZZ  ( m  <_  A  /\  A  <  ( m  +  K ) ) )
 
8-Oct-2021qltnle 9101 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 8-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ )  ->  ( A  <  B  <->  -.  B  <_  A )
 )
 
7-Oct-2021qlelttric 9100 Rational trichotomy. (Contributed by Jim Kingdon, 7-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ )  ->  ( A  <_  B  \/  B  <  A ) )
 
6-Oct-2021qletric 9099 Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.)
 |-  ( ( A  e.  QQ  /\  B  e.  QQ )  ->  ( A  <_  B  \/  B  <_  A ) )
 
6-Oct-2021qtri3or 9098 Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.)
 |-  ( ( M  e.  QQ  /\  N  e.  QQ )  ->  ( M  <  N  \/  M  =  N  \/  N  <  M ) )
 
3-Oct-2021reg3exmid 4304 If any inhabited set satisfying df-wetr 4071 for  _E has a minimal element, excluded middle follows. (Contributed by Jim Kingdon, 3-Oct-2021.)
 |-  ( (  _E  We  z  /\  E. w  w  e.  z )  ->  E. x  e.  z  A. y  e.  z  x  C_  y )   =>    |-  ( ph  \/  -.  ph )
 
3-Oct-2021reg3exmidlemwe 4303 Lemma for reg3exmid 4304. Our counterexample  A satisfies  We. (Contributed by Jim Kingdon, 3-Oct-2021.)
 |-  A  =  { x  e.  { (/) ,  { (/) } }  |  ( x  =  { (/)
 }  \/  ( x  =  (/)  /\  ph ) ) }   =>    |- 
 _E  We  A
 
2-Oct-2021reg2exmid 4261 If any inhabited set has a minimal element (when expressed by  C_), excluded middle follows. (Contributed by Jim Kingdon, 2-Oct-2021.)
 |- 
 A. z ( E. w  w  e.  z  ->  E. x  e.  z  A. y  e.  z  x  C_  y )   =>    |-  ( ph  \/  -.  ph )
 
2-Oct-2021reg2exmidlema 4259 Lemma for reg2exmid 4261. If  A has a minimal element (expressed by  C_), excluded middle follows. (Contributed by Jim Kingdon, 2-Oct-2021.)
 |-  A  =  { x  e.  { (/) ,  { (/) } }  |  ( x  =  { (/)
 }  \/  ( x  =  (/)  /\  ph ) ) }   =>    |-  ( E. u  e.  A  A. v  e.  A  u  C_  v  ->  ( ph  \/  -.  ph ) )
 
30-Sep-2021fin0or 6343 A finite set is either empty or inhabited. (Contributed by Jim Kingdon, 30-Sep-2021.)
 |-  ( A  e.  Fin  ->  ( A  =  (/)  \/  E. x  x  e.  A ) )
 
30-Sep-2021wessep 4302 A subset of a set well-ordered by set membership is well-ordered by set membership. (Contributed by Jim Kingdon, 30-Sep-2021.)
 |-  ( (  _E  We  A  /\  B  C_  A )  ->  _E  We  B )
 
28-Sep-2021frind 4089 Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   &    |-  (
 ( ch  /\  x  e.  A )  ->  ( A. y  e.  A  ( y R x 
 ->  ps )  ->  ph )
 )   &    |-  ( ch  ->  R  Fr  A )   &    |-  ( ch  ->  A  e.  V )   =>    |-  ( ( ch 
 /\  x  e.  A )  ->  ph )
 
26-Sep-2021wetriext 4301 A trichotomous well-order is extensional. (Contributed by Jim Kingdon, 26-Sep-2021.)
 |-  ( ph  ->  R  We  A )   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  A. a  e.  A  A. b  e.  A  ( a R b  \/  a  =  b  \/  b R a ) )   &    |-  ( ph  ->  B  e.  A )   &    |-  ( ph  ->  C  e.  A )   &    |-  ( ph  ->  A. z  e.  A  ( z R B  <->  z R C ) )   =>    |-  ( ph  ->  B  =  C )
 
25-Sep-2021nnwetri 6354 A natural number is well-ordered by 
_E. More specifically, this order both satisfies  We and is trichotomous. (Contributed by Jim Kingdon, 25-Sep-2021.)
 |-  ( A  e.  om  ->  (  _E  We  A  /\  A. x  e.  A  A. y  e.  A  ( x  _E  y  \/  x  =  y  \/  y  _E  x ) ) )
 
23-Sep-2021wepo 4096 A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.)
 |-  ( ( R  We  A  /\  A  e.  V )  ->  R  Po  A )
 
23-Sep-2021df-wetr 4071 Define the well-ordering predicate. It is unusual to define "well-ordering" in the absence of excluded middle, but we mean an ordering which is like the ordering which we have for ordinals (for example, it does not entail trichotomy because ordinals don't have that as seen at ordtriexmid 4247). Given excluded middle, well-ordering is usually defined to require trichotomy (and the defintion of  Fr is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.)
 |-  ( R  We  A  <->  ( R  Fr  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( ( x R y  /\  y R z )  ->  x R z ) ) )
 
22-Sep-2021frforeq3 4084 Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
 |-  ( S  =  T  ->  (FrFor  R A S  <-> FrFor  R A T ) )
 
22-Sep-2021frforeq2 4082 Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
 |-  ( A  =  B  ->  (FrFor  R A T  <-> FrFor  R B T ) )
 
22-Sep-2021frforeq1 4080 Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
 |-  ( R  =  S  ->  (FrFor  R A T  <-> FrFor  S A T ) )
 
22-Sep-2021df-frfor 4068 Define the well-founded relation predicate where  A might be a proper class. By passing in  S we allow it potentially to be a proper class rather than a set. (Contributed by Jim Kingdon and Mario Carneiro, 22-Sep-2021.)
 |-  (FrFor  R A S  <->  (
 A. x  e.  A  ( A. y  e.  A  ( y R x 
 ->  y  e.  S )  ->  x  e.  S )  ->  A  C_  S ) )
 
21-Sep-2021frirrg 4087 A well-founded relation is irreflexive. This is the case where  A exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
 |-  ( ( R  Fr  A  /\  A  e.  V  /\  B  e.  A ) 
 ->  -.  B R B )
 
21-Sep-2021df-frind 4069 Define the well-founded relation predicate. In the presence of excluded middle, there are a variety of equivalent ways to define this. In our case, this definition, in terms of an inductive principle, works better than one along the lines of "there is an element which is minimal when A is ordered by R". Because  s is constrained to be a set (not a proper class) here, sometimes it may be necessary to use FrFor directly rather than via  Fr. (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.)
 |-  ( R  Fr  A  <->  A. sFrFor  R A s )
 
17-Sep-2021ontr2exmid 4250 An ordinal transitivity law which implies excluded middle. (Contributed by Jim Kingdon, 17-Sep-2021.)
 |- 
 A. x  e.  On  A. y A. z  e. 
 On  ( ( x 
 C_  y  /\  y  e.  z )  ->  x  e.  z )   =>    |-  ( ph  \/  -.  ph )
 
16-Sep-2021nnsseleq 6079 For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.)
 |-  ( ( A  e.  om 
 /\  B  e.  om )  ->  ( A  C_  B 
 <->  ( A  e.  B  \/  A  =  B ) ) )
 
15-Sep-2021fientri3 6353 Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.)
 |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( A  ~<_  B  \/  B 
 ~<_  A ) )
 
15-Sep-2021nntri2or2 6076 A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.)
 |-  ( ( A  e.  om 
 /\  B  e.  om )  ->  ( A  C_  B  \/  B  C_  A ) )
 
14-Sep-2021findcard2sd 6349 Deduction form of finite set induction . (Contributed by Jim Kingdon, 14-Sep-2021.)
 |-  ( x  =  (/)  ->  ( ps  <->  ch ) )   &    |-  ( x  =  y  ->  ( ps  <->  th ) )   &    |-  ( x  =  ( y  u.  { z } )  ->  ( ps  <->  ta ) )   &    |-  ( x  =  A  ->  ( ps  <->  et ) )   &    |-  ( ph  ->  ch )   &    |-  ( ( (
 ph  /\  y  e.  Fin )  /\  ( y 
 C_  A  /\  z  e.  ( A  \  y
 ) ) )  ->  ( th  ->  ta )
 )   &    |-  ( ph  ->  A  e.  Fin )   =>    |-  ( ph  ->  et )
 
13-Sep-2021php5fin 6339 A finite set is not equinumerous to a set which adds one element. (Contributed by Jim Kingdon, 13-Sep-2021.)
 |-  ( ( A  e.  Fin  /\  B  e.  ( _V  \  A ) )  ->  -.  A  ~~  ( A  u.  { B }
 ) )
 
13-Sep-2021fiunsnnn 6338 Adding one element to a finite set which is equinumerous to a natural number. (Contributed by Jim Kingdon, 13-Sep-2021.)
 |-  ( ( ( A  e.  Fin  /\  B  e.  ( _V  \  A ) )  /\  ( N  e.  om  /\  A  ~~  N ) )  ->  ( A  u.  { B } )  ~~  suc  N )
 
12-Sep-2021fisbth 6340 Schroeder-Bernstein Theorem for finite sets. (Contributed by Jim Kingdon, 12-Sep-2021.)
 |-  ( ( ( A  e.  Fin  /\  B  e.  Fin )  /\  ( A  ~<_  B  /\  B  ~<_  A ) )  ->  A  ~~  B )
 
11-Sep-2021diffisn 6350 Subtracting a singleton from a finite set produces a finite set. (Contributed by Jim Kingdon, 11-Sep-2021.)
 |-  ( ( A  e.  Fin  /\  B  e.  A ) 
 ->  ( A  \  { B } )  e.  Fin )
 
10-Sep-2021fin0 6342 A nonempty finite set has at least one element. (Contributed by Jim Kingdon, 10-Sep-2021.)
 |-  ( A  e.  Fin  ->  ( A  =/=  (/)  <->  E. x  x  e.  A ) )
 
9-Sep-2021fidifsnid 6332 If we remove a single element from a finite set then put it back in, we end up with the original finite set. This strengthens difsnss 3510 from subset to equality when the set is finite. (Contributed by Jim Kingdon, 9-Sep-2021.)
 |-  ( ( A  e.  Fin  /\  B  e.  A ) 
 ->  ( ( A  \  { B } )  u. 
 { B } )  =  A )
 
9-Sep-2021fidifsnen 6331 All decrements of a finite set are equinumerous. (Contributed by Jim Kingdon, 9-Sep-2021.)
 |-  ( ( X  e.  Fin  /\  A  e.  X  /\  B  e.  X )  ->  ( X  \  { A } )  ~~  ( X  \  { B }
 ) )
 
8-Sep-2021diffifi 6351 Subtracting one finite set from another produces a finite set. (Contributed by Jim Kingdon, 8-Sep-2021.)
 |-  ( ( A  e.  Fin  /\  B  e.  Fin  /\  B  C_  A )  ->  ( A  \  B )  e.  Fin )
 
8-Sep-2021diffitest 6344 If subtracting any set from a finite set gives a finite set, any proposition of the form  -.  ph is decidable. This is not a proof of full excluded middle, but it is close enough to show we won't be able to prove  A  e.  Fin  ->  ( A  \  B
)  e.  Fin. (Contributed by Jim Kingdon, 8-Sep-2021.)
 |- 
 A. a  e.  Fin  A. b ( a  \  b )  e.  Fin   =>    |-  ( -.  ph  \/  -.  -.  ph )
 
6-Sep-2021phpelm 6328 Pigeonhole Principle. A natural number is not equinumerous to an element of itself. (Contributed by Jim Kingdon, 6-Sep-2021.)
 |-  ( ( A  e.  om 
 /\  B  e.  A )  ->  -.  A  ~~  B )
 
5-Sep-2021fidceq 6330 Equality of members of a finite set is decidable. This may be counterintuitive: cannot any two sets be elements of a finite set? Well, to show, for example, that  { B ,  C } is finite would require showing it is equinumerous to  1o or to  2o but to show that you'd need to know  B  =  C or  -.  B  =  C, respectively. (Contributed by Jim Kingdon, 5-Sep-2021.)
 |-  ( ( A  e.  Fin  /\  B  e.  A  /\  C  e.  A )  -> DECID  B  =  C )
 
5-Sep-2021phplem4on 6329 Equinumerosity of successors of an ordinal and a natural number implies equinumerosity of the originals. (Contributed by Jim Kingdon, 5-Sep-2021.)
 |-  ( ( A  e.  On  /\  B  e.  om )  ->  ( suc  A  ~~ 
 suc  B  ->  A  ~~  B ) )
 
4-Sep-2021ex-ceil 9896 Example for df-ceil 9115. (Contributed by AV, 4-Sep-2021.)
 |-  ( ( `  (
 3  /  2 )
 )  =  2  /\  ( `  -u ( 3  / 
 2 ) )  =  -u 1 )
 
3-Sep-20210elsucexmid 4289 If the successor of any ordinal class contains the empty set, excluded middle follows. (Contributed by Jim Kingdon, 3-Sep-2021.)
 |- 
 A. x  e.  On  (/) 
 e.  suc  x   =>    |-  ( ph  \/  -.  ph )
 
1-Sep-2021php5dom 6325 A natural number does not dominate its successor. (Contributed by Jim Kingdon, 1-Sep-2021.)
 |-  ( A  e.  om  ->  -.  suc  A  ~<_  A )
 
1-Sep-2021phplem4dom 6324 Dominance of successors implies dominance of the original natural numbers. (Contributed by Jim Kingdon, 1-Sep-2021.)
 |-  ( ( A  e.  om 
 /\  B  e.  om )  ->  ( suc  A  ~<_  suc  B  ->  A  ~<_  B ) )
 
1-Sep-2021snnen2oprc 6323 A singleton  { A } is never equinumerous with the ordinal number 2. If  A is a set, see snnen2og 6322. (Contributed by Jim Kingdon, 1-Sep-2021.)
 |-  ( -.  A  e.  _V 
 ->  -.  { A }  ~~  2o )
 
1-Sep-2021snnen2og 6322 A singleton  { A } is never equinumerous with the ordinal number 2. If  A is a proper class, see snnen2oprc 6323. (Contributed by Jim Kingdon, 1-Sep-2021.)
 |-  ( A  e.  V  ->  -.  { A }  ~~  2o )
 
1-Sep-2021phplem3g 6319 A natural number is equinumerous to its successor minus any element of the successor. Version of phplem3 6317 with unnecessary hypotheses removed. (Contributed by Jim Kingdon, 1-Sep-2021.)
 |-  ( ( A  e.  om 
 /\  B  e.  suc  A )  ->  A  ~~  ( suc  A  \  { B } ) )
 
31-Aug-2021nndifsnid 6080 If we remove a single element from a natural number then put it back in, we end up with the original natural number. This strengthens difsnss 3510 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
 |-  ( ( A  e.  om 
 /\  B  e.  A )  ->  ( ( A 
 \  { B }
 )  u.  { B } )  =  A )
 
30-Aug-2021carden2bex 6369 If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.)
 |-  ( ( A  ~~  B  /\  E. x  e. 
 On  x  ~~  A )  ->  ( card `  A )  =  ( card `  B ) )
 
30-Aug-2021cardval3ex 6365 The value of  ( card `  A
). (Contributed by Jim Kingdon, 30-Aug-2021.)
 |-  ( E. x  e. 
 On  x  ~~  A  ->  ( card `  A )  =  |^| { y  e. 
 On  |  y  ~~  A } )
 
30-Aug-2021cardcl 6361 The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.)
 |-  ( E. y  e. 
 On  y  ~~  A  ->  ( card `  A )  e.  On )
 
30-Aug-2021onintrab2im 4244 An existence condition which implies an intersection is an ordinal number. (Contributed by Jim Kingdon, 30-Aug-2021.)
 |-  ( E. x  e. 
 On  ph  ->  |^| { x  e.  On  |  ph }  e.  On )
 
30-Aug-2021onintonm 4243 The intersection of an inhabited collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by Mario Carneiro and Jim Kingdon, 30-Aug-2021.)
 |-  ( ( A  C_  On  /\  E. x  x  e.  A )  ->  |^| A  e.  On )
 
29-Aug-2021onintexmid 4297 If the intersection (infimum) of an inhabited class of ordinal numbers belongs to the class, excluded middle follows. The hypothesis would be provable given excluded middle. (Contributed by Mario Carneiro and Jim Kingdon, 29-Aug-2021.)
 |-  ( ( y  C_  On  /\  E. x  x  e.  y )  ->  |^| y  e.  y
 )   =>    |-  ( ph  \/  -.  ph )
 
29-Aug-2021ordtri2or2exmid 4296 Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 29-Aug-2021.)
 |- 
 A. x  e.  On  A. y  e.  On  ( x  C_  y  \/  y  C_  x )   =>    |-  ( ph  \/  -.  ph )
 
29-Aug-2021ordtri2or2exmidlem 4251 A set which is  2o if  ph or  (/) if  -.  ph is an ordinal. (Contributed by Jim Kingdon, 29-Aug-2021.)
 |- 
 { x  e.  { (/)
 ,  { (/) } }  |  ph }  e.  On
 
29-Aug-20212ordpr 4249 Version of 2on 6009 with the definition of  2o expanded and expressed in terms of  Ord. (Contributed by Jim Kingdon, 29-Aug-2021.)
 |- 
 Ord  { (/) ,  { (/) } }
 
25-Aug-2021nnap0d 7959 A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.)
 |-  ( ph  ->  A  e.  NN )   =>    |-  ( ph  ->  A #  0 )
 
24-Aug-2021climcaucn 9870 A converging sequence of complex numbers is a Cauchy sequence. This is like climcau 9866 but adds the part that  ( F `  k ) is complex. (Contributed by Jim Kingdon, 24-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( ( M  e.  ZZ  /\  F  e.  dom  ~~>  ) 
 ->  A. x  e.  RR+  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ( ( F `  k )  e.  CC  /\  ( abs `  ( ( F `
  k )  -  ( F `  j ) ) )  <  x ) )
 
24-Aug-2021climcvg1nlem 9868 Lemma for climcvg1n 9869. We construct sequences of the real and imaginary parts of each term of  F, show those converge, and use that to show that  F converges. (Contributed by Jim Kingdon, 24-Aug-2021.)
 |-  ( ph  ->  F : NN --> CC )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( abs `  ( ( F `  k )  -  ( F `  n ) ) )  <  ( C  /  n ) )   &    |-  G  =  ( x  e.  NN  |->  ( Re `  ( F `  x ) ) )   &    |-  H  =  ( x  e.  NN  |->  ( Im `  ( F `
  x ) ) )   &    |-  J  =  ( x  e.  NN  |->  ( _i  x.  ( H `
  x ) ) )   =>    |-  ( ph  ->  F  e.  dom  ~~>  )
 
23-Aug-2021climcvg1n 9869 A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within  C  /  n of the nth term, where  C is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
 |-  ( ph  ->  F : NN --> CC )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( abs `  ( ( F `  k )  -  ( F `  n ) ) )  <  ( C  /  n ) )   =>    |-  ( ph  ->  F  e.  dom  ~~>  )
 
23-Aug-2021climrecvg1n 9867 A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within  C  /  n of the nth term, where  C is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)
 |-  ( ph  ->  F : NN --> RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( abs `  ( ( F `  k )  -  ( F `  n ) ) )  <  ( C  /  n ) )   =>    |-  ( ph  ->  F  e.  dom  ~~>  )
 
22-Aug-2021climserile 9865 The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by Jim Kingdon, 22-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  N  e.  Z )   &    |-  ( ph  ->  seq M (  +  ,  F ,  CC )  ~~>  A )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  0  <_  ( F `  k
 ) )   =>    |-  ( ph  ->  (  seq M (  +  ,  F ,  CC ) `  N )  <_  A )
 
22-Aug-2021iserige0 9863 The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  seq M (  +  ,  F ,  CC )  ~~>  A )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  0  <_  ( F `  k
 ) )   =>    |-  ( ph  ->  0  <_  A )
 
22-Aug-2021iserile 9862 Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  seq M (  +  ,  F ,  CC )  ~~>  A )   &    |-  ( ph  ->  seq
 M (  +  ,  G ,  CC )  ~~>  B )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  e.  RR )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( G `  k )  e. 
 RR )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( F `  k
 )  <_  ( G `  k ) )   =>    |-  ( ph  ->  A 
 <_  B )
 
22-Aug-2021serile 9253 Comparison of partial sums of two infinite series of reals. (Contributed by Jim Kingdon, 22-Aug-2021.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  e.  RR )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( G `  k )  e.  RR )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  <_  ( G `  k ) )   =>    |-  ( ph  ->  (  seq M (  +  ,  F ,  CC ) `  N )  <_  (  seq M (  +  ,  G ,  CC ) `  N ) )
 
22-Aug-2021serige0 9252 A finite sum of nonnegative terms is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  e.  RR )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  0  <_  ( F `  k ) )   =>    |-  ( ph  ->  0  <_  (  seq M (  +  ,  F ,  CC ) `  N ) )
 
21-Aug-2021clim2iser2 9858 The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  N  e.  Z )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ph  ->  seq ( N  +  1 ) (  +  ,  F ,  CC )  ~~>  A )   =>    |-  ( ph  ->  seq M (  +  ,  F ,  CC )  ~~>  ( A  +  (  seq M (  +  ,  F ,  CC ) `  N ) ) )
 
21-Aug-2021iseqdistr 9249 The distributive property for series. (Contributed by Jim Kingdon, 21-Aug-2021.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( C T ( x  .+  y ) )  =  ( ( C T x )  .+  ( C T y ) ) )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( G `  x )  e.  S )   &    |-  (
 ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  =  ( C T ( G `
  x ) ) )   &    |-  ( ph  ->  S  e.  V )   &    |-  (
 ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x T y )  e.  S )   &    |-  (
 ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  S )   &    |-  ( ph  ->  C  e.  S )   =>    |-  ( ph  ->  (  seq M (  .+  ,  F ,  S ) `  N )  =  ( C T (  seq M (  .+  ,  G ,  S ) `  N ) ) )
 
21-Aug-2021iseqhomo 9248 Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 21-Aug-2021.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  S )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( H `
  ( x  .+  y ) )  =  ( ( H `  x ) Q ( H `  y ) ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( H `  ( F `
  x ) )  =  ( G `  x ) )   &    |-  (
 ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( G `  x )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x Q y )  e.  S )   =>    |-  ( ph  ->  ( H `  (  seq M (  .+  ,  F ,  S ) `  N ) )  =  (  seq M ( Q ,  G ,  S ) `  N ) )
 
20-Aug-2021clim2iser 9857 The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  N  e.  Z )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ph  ->  seq
 M (  +  ,  F ,  CC )  ~~>  A )   =>    |-  ( ph  ->  seq ( N  +  1 )
 (  +  ,  F ,  CC )  ~~>  ( A  -  (  seq M (  +  ,  F ,  CC ) `  N ) ) )
 
20-Aug-2021iseqex 9213 Existence of the sequence builder operation. (Contributed by Jim Kingdon, 20-Aug-2021.)
 |- 
 seq M (  .+  ,  F ,  S )  e.  _V
 
20-Aug-2021frecex 5981 Finite recursion produces a set. (Contributed by Jim Kingdon, 20-Aug-2021.)
 |- frec
 ( F ,  A )  e.  _V
 
20-Aug-2021tfrfun 5955 Transfinite recursion produces a function. (Contributed by Jim Kingdon, 20-Aug-2021.)
 |- 
 Fun recs ( F )
 
19-Aug-2021iserclim0 9826 The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.)
 |-  ( M  e.  ZZ  ->  seq M (  +  ,  ( ( ZZ>= `  M )  X.  { 0 } ) ,  CC )  ~~>  0 )
 
19-Aug-2021shftval4g 9438 Value of a sequence shifted by  -u A. (Contributed by Jim Kingdon, 19-Aug-2021.)
 |-  ( ( F  e.  V  /\  A  e.  CC  /\  B  e.  CC )  ->  ( ( F  shift  -u A ) `  B )  =  ( F `  ( A  +  B ) ) )
 
19-Aug-2021iser0f 9251 A zero-valued infinite series is equal to the constant zero function. (Contributed by Jim Kingdon, 19-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( M  e.  ZZ  ->  seq M (  +  ,  ( Z  X.  {
 0 } ) ,  CC )  =  ( Z  X.  { 0 } ) )
 
19-Aug-2021iser0 9250 The value of the partial sums in a zero-valued infinite series. (Contributed by Jim Kingdon, 19-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( N  e.  Z  ->  (  seq M (  +  ,  ( Z  X.  { 0 } ) ,  CC ) `  N )  =  0 )
 
19-Aug-2021ovexg 5539 Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.)
 |-  ( ( A  e.  V  /\  F  e.  W  /\  B  e.  X ) 
 ->  ( A F B )  e.  _V )
 
18-Aug-2021iseqid3s 9246 A sequence that consists of zeroes up to  N sums to zero at 
N. In this case by "zero" we mean whatever the identity  Z is for the operation  .+). (Contributed by Jim Kingdon, 18-Aug-2021.)
 |-  ( ph  ->  ( Z  .+  Z )  =  Z )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   &    |-  ( ( ph  /\  x  e.  ( M
 ... N ) ) 
 ->  ( F `  x )  =  Z )   &    |-  ( ph  ->  Z  e.  S )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( F `  x )  e.  S )   &    |-  (
 ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x  .+  y )  e.  S )   =>    |-  ( ph  ->  ( 
 seq M (  .+  ,  F ,  S ) `
  N )  =  Z )
 
18-Aug-2021iseqid3 9245 A sequence that consists entirely of zeroes (or whatever the identity  Z is for operation  .+) sums to zero. (Contributed by Jim Kingdon, 18-Aug-2021.)
 |-  ( ph  ->  ( Z  .+  Z )  =  Z )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( F `  x )  =  Z )   &    |-  ( ph  ->  Z  e.  V )   =>    |-  ( ph  ->  (  seq M (  .+  ,  F ,  { Z } ) `  N )  =  Z )
 
18-Aug-2021iseqss 9226 Specifying a larger universe for 
seq. As long as  F and  .+ are closed over  S, then any set which contains  S can be used as the last argument to  seq. This theorem does not allow  T to be a proper class, however. It also currently requires that  .+ be closed over  T (as well as  S). (Contributed by Jim Kingdon, 18-Aug-2021.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  T  e.  V )   &    |-  ( ph  ->  S  C_  T )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  T  /\  y  e.  T )
 )  ->  ( x  .+  y )  e.  T )   =>    |-  ( ph  ->  seq M (  .+  ,  F ,  S )  =  seq M (  .+  ,  F ,  T ) )
 
17-Aug-2021iseqcaopr 9242 The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Jim Kingdon, 17-Aug-2021.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  =  ( y  .+  x ) )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S ) )  ->  ( ( x  .+  y ) 
 .+  z )  =  ( x  .+  (
 y  .+  z )
 ) )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  ->  ( F `  k )  e.  S )   &    |-  (
 ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( G `  k )  e.  S )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( H `  k )  =  ( ( F `  k
 )  .+  ( G `  k ) ) )   &    |-  ( ph  ->  S  e.  V )   =>    |-  ( ph  ->  (  seq M (  .+  ,  H ,  S ) `  N )  =  ( (  seq M ( 
 .+  ,  F ,  S ) `  N )  .+  (  seq M (  .+  ,  G ,  S ) `  N ) ) )
 
16-Aug-2021iseqcaopr3 9240 Lemma for iseqcaopr2 . (Contributed by Jim Kingdon, 16-Aug-2021.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x Q y )  e.  S )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  ->  ( F `  k )  e.  S )   &    |-  (
 ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( G `  k )  e.  S )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( H `  k )  =  ( ( F `  k
 ) Q ( G `
  k ) ) )   &    |-  ( ( ph  /\  n  e.  ( M..^ N ) )  ->  ( ( (  seq M (  .+  ,  F ,  S ) `  n ) Q (  seq M (  .+  ,  G ,  S ) `  n ) )  .+  ( ( F `  ( n  +  1 ) ) Q ( G `  ( n  +  1
 ) ) ) )  =  ( ( ( 
 seq M (  .+  ,  F ,  S ) `
  n )  .+  ( F `  ( n  +  1 ) ) ) Q ( ( 
 seq M (  .+  ,  G ,  S ) `
  n )  .+  ( G `  ( n  +  1 ) ) ) ) )   &    |-  ( ph  ->  S  e.  V )   =>    |-  ( ph  ->  (  seq M (  .+  ,  H ,  S ) `  N )  =  ( (  seq M ( 
 .+  ,  F ,  S ) `  N ) Q (  seq M (  .+  ,  G ,  S ) `  N ) ) )
 
16-Aug-2021iseq1p 9239 Removing the first term from a sequence. (Contributed by Jim Kingdon, 16-Aug-2021.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S )
 )  ->  ( ( x  .+  y )  .+  z )  =  ( x  .+  ( y  .+  z ) ) )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1 ) ) )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  S )   =>    |-  ( ph  ->  (  seq M (  .+  ,  F ,  S ) `  N )  =  ( ( F `  M )  .+  (  seq ( M  +  1 )
 (  .+  ,  F ,  S ) `  N ) ) )
 
16-Aug-2021iseqsplit 9238 Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S )
 )  ->  ( ( x  .+  y )  .+  z )  =  ( x  .+  ( y  .+  z ) ) )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1 ) ) )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  M  e.  ( ZZ>=
 `  K ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  K )
 )  ->  ( F `  x )  e.  S )   =>    |-  ( ph  ->  (  seq K (  .+  ,  F ,  S ) `  N )  =  ( (  seq K ( 
 .+  ,  F ,  S ) `  M )  .+  (  seq ( M  +  1 )
 (  .+  ,  F ,  S ) `  N ) ) )
 
15-Aug-2021shftfibg 9421 Value of a fiber of the relation  F. (Contributed by Jim Kingdon, 15-Aug-2021.)
 |-  ( ( F  e.  V  /\  A  e.  CC  /\  B  e.  CC )  ->  ( ( F  shift  A ) " { B } )  =  ( F " { ( B  -  A ) }
 ) )
 
15-Aug-2021ovshftex 9420 Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.)
 |-  ( ( F  e.  V  /\  A  e.  CC )  ->  ( F  shift  A )  e.  _V )
 
15-Aug-2021isermono 9237 The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by Jim Kingdon, 15-Aug-2021.)
 |-  ( ph  ->  K  e.  ( ZZ>= `  M )
 )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  K )
 )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  RR )   &    |-  ( ( ph  /\  x  e.  ( ( K  +  1 ) ... N ) )  ->  0  <_  ( F `  x ) )   =>    |-  ( ph  ->  (  seq M (  +  ,  F ,  RR ) `  K )  <_  (  seq M (  +  ,  F ,  RR ) `  N ) )
 
15-Aug-2021iserf 9233 An infinite series of complex terms is a function from  NN to  CC. (Contributed by Jim Kingdon, 15-Aug-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   =>    |-  ( ph  ->  seq M (  +  ,  F ,  CC ) : Z --> CC )
 
15-Aug-2021iseqshft2 9232 Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ph  ->  K  e.  ZZ )   &    |-  ( ( ph  /\  k  e.  ( M
 ... N ) ) 
 ->  ( F `  k
 )  =  ( G `
  ( k  +  K ) ) )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( F `  x )  e.  S )   &    |-  (
 ( ph  /\  x  e.  ( ZZ>= `  ( M  +  K ) ) ) 
 ->  ( G `  x )  e.  S )   &    |-  (
 ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x  .+  y )  e.  S )   =>    |-  ( ph  ->  ( 
 seq M (  .+  ,  F ,  S ) `
  N )  =  (  seq ( M  +  K ) ( 
 .+  ,  G ,  S ) `  ( N  +  K )
 ) )
 
15-Aug-2021iseqfeq 9231 Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  S  e.  V )   &    |-  (
 ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  S )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  =  ( G `  k ) )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x 
 .+  y )  e.  S )   =>    |-  ( ph  ->  seq M (  .+  ,  F ,  S )  =  seq M (  .+  ,  G ,  S ) )
 
13-Aug-2021absdivapd 9791 Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  B #  0 )   =>    |-  ( ph  ->  ( abs `  ( A  /  B ) )  =  ( ( abs `  A )  /  ( abs `  B ) ) )
 
13-Aug-2021absrpclapd 9784 The absolute value of a complex number apart from zero is a positive real. (Contributed by Jim Kingdon, 13-Aug-2021.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A #  0 )   =>    |-  ( ph  ->  ( abs `  A )  e.  RR+ )
 
13-Aug-2021absdivapzi 9750 Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
 |-  A  e.  CC   &    |-  B  e.  CC   =>    |-  ( B #  0  ->  ( abs `  ( A  /  B ) )  =  ( ( abs `  A )  /  ( abs `  B ) ) )
 
13-Aug-2021absgt0ap 9695 The absolute value of a number apart from zero is positive. (Contributed by Jim Kingdon, 13-Aug-2021.)
 |-  ( A  e.  CC  ->  ( A #  0  <->  0  <  ( abs `  A ) ) )
 
13-Aug-2021recvalap 9693 Reciprocal expressed with a real denominator. (Contributed by Jim Kingdon, 13-Aug-2021.)
 |-  ( ( A  e.  CC  /\  A #  0 ) 
 ->  ( 1  /  A )  =  ( ( * `  A )  /  ( ( abs `  A ) ^ 2 ) ) )
 
13-Aug-2021sqap0 9320 A number is apart from zero iff its square is apart from zero. (Contributed by Jim Kingdon, 13-Aug-2021.)
 |-  ( A  e.  CC  ->  ( ( A ^
 2 ) #  0  <->  A #  0 )
 )
 
13-Aug-2021leltapd 7628 '<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   =>    |-  ( ph  ->  ( A  <  B  <->  B #  A )
 )
 
13-Aug-2021leltap 7615 '<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.)
 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <_  B )  ->  ( A  <  B  <->  B #  A ) )
 
12-Aug-2021abssubap0 9686 If the absolute value of a complex number is less than a real, its difference from the real is apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  ( ( A  e.  CC  /\  B  e.  RR  /\  ( abs `  A )  <  B )  ->  ( B  -  A ) #  0 )
 
12-Aug-2021ltabs 9683 A number which is less than its absolute value is negative. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  ( ( A  e.  RR  /\  A  <  ( abs `  A ) ) 
 ->  A  <  0 )
 
12-Aug-2021absext 9661 Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( abs `  A ) #  ( abs `  B )  ->  A #  B ) )
 
12-Aug-2021sq11ap 9414 Analogue to sq11 9326 but for apartness. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  ( B  e.  RR  /\  0  <_  B ) )  ->  ( ( A ^
 2 ) #  ( B ^ 2 )  <->  A #  B )
 )
 
12-Aug-2021subap0d 7631 Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  A #  B )   =>    |-  ( ph  ->  ( A  -  B ) #  0 )
 
12-Aug-2021ltapd 7627 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   =>    |-  ( ph  ->  A #  B )
 
12-Aug-2021gtapd 7626 'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <  B )   =>    |-  ( ph  ->  B #  A )
 
12-Aug-2021ltapi 7625 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  A  e.  RR   &    |-  B  e.  RR   =>    |-  ( A  <  B  ->  B #  A )
 
12-Aug-2021ltapii 7624 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  A  e.  RR   &    |-  B  e.  RR   &    |-  A  <  B   =>    |-  A #  B
 
12-Aug-2021gtapii 7623 'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  A  e.  RR   &    |-  B  e.  RR   &    |-  A  <  B   =>    |-  B #  A
 
12-Aug-2021ltap 7622 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  A  <  B ) 
 ->  B #  A )
 
11-Aug-2021absexpzap 9676 Absolute value of integer exponentiation. (Contributed by Jim Kingdon, 11-Aug-2021.)
 |-  ( ( A  e.  CC  /\  A #  0  /\  N  e.  ZZ )  ->  ( abs `  ( A ^ N ) )  =  ( ( abs `  A ) ^ N ) )
 
11-Aug-2021absdivap 9668 Absolute value distributes over division. (Contributed by Jim Kingdon, 11-Aug-2021.)
 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  B #  0 )  ->  ( abs `  ( A  /  B ) )  =  ( ( abs `  A )  /  ( abs `  B ) ) )
 
11-Aug-2021abs00ap 9660 The absolute value of a number is apart from zero iff the number is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
 |-  ( A  e.  CC  ->  ( ( abs `  A ) #  0  <->  A #  0 )
 )
 
11-Aug-2021absrpclap 9659 The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.)
 |-  ( ( A  e.  CC  /\  A #  0 ) 
 ->  ( abs `  A )  e.  RR+ )
 
11-Aug-2021sqrt11ap 9636 Analogue to sqrt11 9637 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.)
 |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  ( B  e.  RR  /\  0  <_  B ) )  ->  ( ( sqr `  A ) #  ( sqr `  B ) 
 <->  A #  B ) )
 
11-Aug-2021cjap0d 9548 A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A #  0 )   =>    |-  ( ph  ->  ( * `  A ) #  0 )
 
11-Aug-2021ap0gt0d 7630 A nonzero nonnegative number is positive. (Contributed by Jim Kingdon, 11-Aug-2021.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0 
 <_  A )   &    |-  ( ph  ->  A #  0 )   =>    |-  ( ph  ->  0  <  A )
 
11-Aug-2021ap0gt0 7629 A nonnegative number is apart from zero if and only if it is positive. (Contributed by Jim Kingdon, 11-Aug-2021.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  ( A #  0  <->  0  <  A ) )
 
10-Aug-2021rersqrtthlem 9628 Lemma for resqrtth 9629. (Contributed by Jim Kingdon, 10-Aug-2021.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  ( ( ( sqr `  A ) ^ 2 )  =  A  /\  0  <_  ( sqr `  A )
 ) )
 
10-Aug-2021rersqreu 9626 Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  E! x  e. 
 RR  ( ( x ^ 2 )  =  A  /\  0  <_  x ) )
 
10-Aug-2021rsqrmo 9625 Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  E* x  e.  RR  ( ( x ^
 2 )  =  A  /\  0  <_  x ) )
 
9-Aug-2021resqrexlemoverl 9619 Lemma for resqrex 9624. Every term in the sequence is an overestimate compared with the limit 
L. Although this theorem is stated in terms of a particular sequence the proof could be adapted for any decreasing convergent sequence. (Contributed by Jim Kingdon, 9-Aug-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   &    |-  ( ph  ->  L  e.  RR )   &    |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i
 )  +  e ) ) )   &    |-  ( ph  ->  K  e.  NN )   =>    |-  ( ph  ->  L 
 <_  ( F `  K ) )
 
8-Aug-2021resqrexlemga 9621 Lemma for resqrex 9624. The sequence formed by squaring each term of  F converges to  A. (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   &    |-  ( ph  ->  L  e.  RR )   &    |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i
 )  +  e ) ) )   &    |-  G  =  ( x  e.  NN  |->  ( ( F `  x ) ^ 2 ) )   =>    |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( ( G `  k )  <  ( A  +  e )  /\  A  <  ( ( G `  k
 )  +  e ) ) )
 
8-Aug-2021resqrexlemglsq 9620 Lemma for resqrex 9624. The sequence formed by squaring each term of  F converges to  ( L ^
2 ). (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   &    |-  ( ph  ->  L  e.  RR )   &    |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i
 )  +  e ) ) )   &    |-  G  =  ( x  e.  NN  |->  ( ( F `  x ) ^ 2 ) )   =>    |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( ( G `  k )  <  ( ( L ^ 2 )  +  e )  /\  ( L ^ 2 )  < 
 ( ( G `  k )  +  e
 ) ) )
 
8-Aug-2021recvguniqlem 9592 Lemma for recvguniq 9593. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.)
 |-  ( ph  ->  F : NN --> RR )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  K  e.  NN )   &    |-  ( ph  ->  A  <  (
 ( F `  K )  +  ( ( A  -  B )  / 
 2 ) ) )   &    |-  ( ph  ->  ( F `  K )  <  ( B  +  ( ( A  -  B )  / 
 2 ) ) )   =>    |-  ( ph  -> F.  )
 
8-Aug-2021ifcldcd 3358 Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.)
 |-  ( ph  ->  A  e.  C )   &    |-  ( ph  ->  B  e.  C )   &    |-  ( ph  -> DECID  ps )   =>    |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
 
8-Aug-2021ifbothdc 3357 A wff  th containing a conditional operator is true when both of its cases are true. (Contributed by Jim Kingdon, 8-Aug-2021.)
 |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ps  <->  th ) )   &    |-  ( B  =  if ( ph ,  A ,  B )  ->  ( ch 
 <-> 
 th ) )   =>    |-  ( ( ps 
 /\  ch  /\ DECID  ph )  ->  th )
 
7-Aug-2021resqrexlemsqa 9622 Lemma for resqrex 9624. The square of a limit is  A. (Contributed by Jim Kingdon, 7-Aug-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   &    |-  ( ph  ->  L  e.  RR )   &    |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i
 )  +  e ) ) )   =>    |-  ( ph  ->  ( L ^ 2 )  =  A )
 
7-Aug-2021resqrexlemgt0 9618 Lemma for resqrex 9624. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   &    |-  ( ph  ->  L  e.  RR )   &    |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i
 )  +  e ) ) )   =>    |-  ( ph  ->  0  <_  L )
 
7-Aug-2021recvguniq 9593 Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.)
 |-  ( ph  ->  F : NN --> RR )   &    |-  ( ph  ->  L  e.  RR )   &    |-  ( ph  ->  A. x  e.  RR+  E. j  e. 
 NN  A. k  e.  ( ZZ>=
 `  j ) ( ( F `  k
 )  <  ( L  +  x )  /\  L  <  ( ( F `  k )  +  x ) ) )   &    |-  ( ph  ->  M  e.  RR )   &    |-  ( ph  ->  A. x  e.  RR+  E. j  e. 
 NN  A. k  e.  ( ZZ>=
 `  j ) ( ( F `  k
 )  <  ( M  +  x )  /\  M  <  ( ( F `  k )  +  x ) ) )   =>    |-  ( ph  ->  L  =  M )
 
6-Aug-2021resqrexlemcvg 9617 Lemma for resqrex 9624. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ph  ->  E. r  e.  RR  A. x  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( r  +  x )  /\  r  < 
 ( ( F `  i )  +  x ) ) )
 
6-Aug-2021cvg1nlemcxze 9581 Lemma for cvg1n 9585. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.)
 |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  X  e.  RR+ )   &    |-  ( ph  ->  Z  e.  NN )   &    |-  ( ph  ->  E  e.  NN )   &    |-  ( ph  ->  A  e.  NN )   &    |-  ( ph  ->  ( ( ( ( C  x.  2 )  /  X )  /  Z )  +  A )  <  E )   =>    |-  ( ph  ->  ( C  /  ( E  x.  Z ) )  < 
 ( X  /  2
 ) )
 
1-Aug-2021cvg1n 9585 Convergence of real sequences.

This is a version of caucvgre 9580 with a constant multiplier  C on the rate of convergence. That is, all terms after the nth term must be within  C  /  n of the nth term.

(Contributed by Jim Kingdon, 1-Aug-2021.)

 |-  ( ph  ->  F : NN --> RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( ( F `  n )  <  ( ( F `  k )  +  ( C  /  n ) )  /\  ( F `  k )  <  ( ( F `
  n )  +  ( C  /  n ) ) ) )   =>    |-  ( ph  ->  E. y  e.  RR  A. x  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( y  +  x )  /\  y  < 
 ( ( F `  i )  +  x ) ) )
 
1-Aug-2021cvg1nlemres 9584 Lemma for cvg1n 9585. The original sequence  F has a limit (turns out it is the same as the limit of the modified sequence  G). (Contributed by Jim Kingdon, 1-Aug-2021.)
 |-  ( ph  ->  F : NN --> RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( ( F `  n )  <  ( ( F `  k )  +  ( C  /  n ) )  /\  ( F `  k )  <  ( ( F `
  n )  +  ( C  /  n ) ) ) )   &    |-  G  =  ( j  e.  NN  |->  ( F `  ( j  x.  Z ) ) )   &    |-  ( ph  ->  Z  e.  NN )   &    |-  ( ph  ->  C  <  Z )   =>    |-  ( ph  ->  E. y  e.  RR  A. x  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( y  +  x )  /\  y  < 
 ( ( F `  i )  +  x ) ) )
 
1-Aug-2021cvg1nlemcau 9583 Lemma for cvg1n 9585. By selecting spaced out terms for the modified sequence  G, the terms are within  1  /  n (without the constant  C). (Contributed by Jim Kingdon, 1-Aug-2021.)
 |-  ( ph  ->  F : NN --> RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( ( F `  n )  <  ( ( F `  k )  +  ( C  /  n ) )  /\  ( F `  k )  <  ( ( F `
  n )  +  ( C  /  n ) ) ) )   &    |-  G  =  ( j  e.  NN  |->  ( F `  ( j  x.  Z ) ) )   &    |-  ( ph  ->  Z  e.  NN )   &    |-  ( ph  ->  C  <  Z )   =>    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( ( G `  n )  <  ( ( G `  k )  +  ( 1  /  n ) )  /\  ( G `  k )  <  ( ( G `
  n )  +  ( 1  /  n ) ) ) )
 
1-Aug-2021cvg1nlemf 9582 Lemma for cvg1n 9585. The modified sequence  G is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.)
 |-  ( ph  ->  F : NN --> RR )   &    |-  ( ph  ->  C  e.  RR+ )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n )
 ( ( F `  n )  <  ( ( F `  k )  +  ( C  /  n ) )  /\  ( F `  k )  <  ( ( F `
  n )  +  ( C  /  n ) ) ) )   &    |-  G  =  ( j  e.  NN  |->  ( F `  ( j  x.  Z ) ) )   &    |-  ( ph  ->  Z  e.  NN )   &    |-  ( ph  ->  C  <  Z )   =>    |-  ( ph  ->  G : NN --> RR )
 
31-Jul-2021resqrexlemnm 9616 Lemma for resqrex 9624. The difference between two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 31-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  N  <_  M )   =>    |-  ( ph  ->  (
 ( F `  N )  -  ( F `  M ) )  < 
 ( ( ( ( F `  1 ) ^ 2 )  x.  2 )  /  (
 2 ^ ( N  -  1 ) ) ) )
 
31-Jul-2021resqrexlemdecn 9610 Lemma for resqrex 9624. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  N  <  M )   =>    |-  ( ph  ->  ( F `  M )  < 
 ( F `  N ) )
 
30-Jul-2021resqrexlemnmsq 9615 Lemma for resqrex 9624. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  N  <_  M )   =>    |-  ( ph  ->  (
 ( ( F `  N ) ^ 2
 )  -  ( ( F `  M ) ^ 2 ) )  <  ( ( ( F `  1 ) ^ 2 )  /  ( 4 ^ ( N  -  1 ) ) ) )
 
30-Jul-2021divmuldivapd 7806 Multiplication of two ratios. (Contributed by Jim Kingdon, 30-Jul-2021.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  B #  0 )   &    |-  ( ph  ->  D #  0 )   =>    |-  ( ph  ->  (
 ( A  /  B )  x.  ( C  /  D ) )  =  ( ( A  x.  C )  /  ( B  x.  D ) ) )
 
29-Jul-2021resqrexlemcalc3 9614 Lemma for resqrex 9624. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ( ph  /\  N  e.  NN )  ->  (
 ( ( F `  N ) ^ 2
 )  -  A ) 
 <_  ( ( ( F `
  1 ) ^
 2 )  /  (
 4 ^ ( N  -  1 ) ) ) )
 
29-Jul-2021resqrexlemcalc2 9613 Lemma for resqrex 9624. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ( ph  /\  N  e.  NN )  ->  (
 ( ( F `  ( N  +  1
 ) ) ^ 2
 )  -  A ) 
 <_  ( ( ( ( F `  N ) ^ 2 )  -  A )  /  4
 ) )
 
29-Jul-2021resqrexlemcalc1 9612 Lemma for resqrex 9624. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ( ph  /\  N  e.  NN )  ->  (
 ( ( F `  ( N  +  1
 ) ) ^ 2
 )  -  A )  =  ( ( ( ( ( F `  N ) ^ 2
 )  -  A ) ^ 2 )  /  ( 4  x.  (
 ( F `  N ) ^ 2 ) ) ) )
 
29-Jul-2021resqrexlemlo 9611 Lemma for resqrex 9624. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ( ph  /\  N  e.  NN )  ->  (
 1  /  ( 2 ^ N ) )  < 
 ( F `  N ) )
 
29-Jul-2021resqrexlemdec 9609 Lemma for resqrex 9624. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ( ph  /\  N  e.  NN )  ->  ( F `  ( N  +  1 ) )  < 
 ( F `  N ) )
 
28-Jul-2021resqrexlemp1rp 9604 Lemma for resqrex 9624. Applying the recursion rule yields a positive real (expressed in a way that will help apply iseqf 9224 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ( ph  /\  ( B  e.  RR+  /\  C  e.  RR+ ) )  ->  ( B ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) C )  e.  RR+ )
 
28-Jul-2021resqrexlem1arp 9603 Lemma for resqrex 9624.  1  +  A is a positive real (expressed in a way that will help apply iseqf 9224 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ( ph  /\  N  e.  NN )  ->  (
 ( NN  X.  {
 ( 1  +  A ) } ) `  N )  e.  RR+ )
 
28-Jul-2021rpap0d 8628 A positive real is apart from zero. (Contributed by Jim Kingdon, 28-Jul-2021.)
 |-  ( ph  ->  A  e.  RR+ )   =>    |-  ( ph  ->  A #  0 )
 
27-Jul-2021resqrexlemex 9623 Lemma for resqrex 9624. Existence of square root given a sequence which converges to the square root. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ph  ->  E. x  e.  RR  ( 0  <_  x  /\  ( x ^
 2 )  =  A ) )
 
27-Jul-2021resqrexlemover 9608 Lemma for resqrex 9624. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ( ph  /\  N  e.  NN )  ->  A  <  ( ( F `  N ) ^ 2
 ) )
 
27-Jul-2021resqrexlemfp1 9607 Lemma for resqrex 9624. Recursion rule. This sequence is the ancient method for computing square roots, often known as the babylonian method, although known to many ancient cultures. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ( ph  /\  N  e.  NN )  ->  ( F `  ( N  +  1 ) )  =  ( ( ( F `
  N )  +  ( A  /  ( F `  N ) ) )  /  2 ) )
 
27-Jul-2021resqrexlemf1 9606 Lemma for resqrex 9624. Initial value. Although this sequence converges to the square root with any positive initial value, this choice makes various steps in the proof of convergence easier. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ph  ->  ( F `  1 )  =  ( 1  +  A ) )
 
27-Jul-2021resqrexlemf 9605 Lemma for resqrex 9624. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) ,  RR+ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ph  ->  F : NN --> RR+ )
 
23-Jul-2021iseqf 9224 Range of the recursive sequence builder. (Contributed by Jim Kingdon, 23-Jul-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  S  e.  V )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  x  e.  Z )  ->  ( F `  x )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x 
 .+  y )  e.  S )   =>    |-  ( ph  ->  seq M (  .+  ,  F ,  S ) : Z --> S )
 
22-Jul-2021ialgrlemconst 9882 Lemma for ialgr0 9883. Closure of a constant function, in a form suitable for theorems such as iseq1 9222 or iseqfn 9221. (Contributed by Jim Kingdon, 22-Jul-2021.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  A  e.  S )   =>    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( ( Z  X.  { A } ) `  x )  e.  S )
 
22-Jul-2021ialgrlem1st 9881 Lemma for ialgr0 9883. Expressing algrflemg 5851 in a form suitable for theorems such as iseq1 9222 or iseqfn 9221. (Contributed by Jim Kingdon, 22-Jul-2021.)
 |-  ( ph  ->  F : S --> S )   =>    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x ( F  o.  1st ) y )  e.  S )
 
22-Jul-2021algrflemg 5851 Lemma for algrf and related theorems. (Contributed by Jim Kingdon, 22-Jul-2021.)
 |-  ( ( B  e.  V  /\  C  e.  W )  ->  ( B ( F  o.  1st ) C )  =  ( F `  B ) )
 
21-Jul-2021zmod1congr 9183 Two arbitrary integers are congruent modulo 1, see example 4 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.)
 |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( A  mod  1 )  =  ( B  mod  1 ) )
 
20-Jul-2021caucvgrelemcau 9579 Lemma for caucvgre 9580. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.)
 |-  ( ph  ->  F : NN --> RR )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n ) ( ( F `  n )  <  ( ( F `
  k )  +  ( 1  /  n ) )  /\  ( F `
  k )  < 
 ( ( F `  n )  +  (
 1  /  n )
 ) ) )   =>    |-  ( ph  ->  A. n  e.  NN  A. k  e.  NN  ( n  <RR  k  ->  (
 ( F `  n )  <RR  ( ( F `
  k )  +  ( iota_ r  e.  RR  ( n  x.  r
 )  =  1 ) )  /\  ( F `
  k )  <RR  ( ( F `  n )  +  ( iota_ r  e. 
 RR  ( n  x.  r )  =  1
 ) ) ) ) )
 
20-Jul-2021caucvgrelemrec 9578 Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.)
 |-  ( ( A  e.  RR  /\  A #  0 ) 
 ->  ( iota_ r  e.  RR  ( A  x.  r
 )  =  1 )  =  ( 1  /  A ) )
 
19-Jul-2021caucvgre 9580 Convergence of real sequences.

A Cauchy sequence (as defined here, which has a rate of convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within  1  /  n of the nth term.

(Contributed by Jim Kingdon, 19-Jul-2021.)

 |-  ( ph  ->  F : NN --> RR )   &    |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n ) ( ( F `  n )  <  ( ( F `
  k )  +  ( 1  /  n ) )  /\  ( F `
  k )  < 
 ( ( F `  n )  +  (
 1  /  n )
 ) ) )   =>    |-  ( ph  ->  E. y  e.  RR  A. x  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j )
 ( ( F `  i )  <  ( y  +  x )  /\  y  <  ( ( F `
  i )  +  x ) ) )
 
19-Jul-2021ax-caucvg 7004 Completeness. Axiom for real and complex numbers, justified by theorem axcaucvg 6974.

A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within  1  /  n of the nth term.

This axiom should not be used directly; instead use caucvgre 9580 (which is the same, but stated in terms of the  NN and  1  /  n notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.)

 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1
 )  e.  x ) }   &    |-  ( ph  ->  F : N --> RR )   &    |-  ( ph  ->  A. n  e.  N  A. k  e.  N  ( n  <RR  k  ->  (
 ( F `  n )  <RR  ( ( F `
  k )  +  ( iota_ r  e.  RR  ( n  x.  r
 )  =  1 ) )  /\  ( F `
  k )  <RR  ( ( F `  n )  +  ( iota_ r  e. 
 RR  ( n  x.  r )  =  1
 ) ) ) ) )   =>    |-  ( ph  ->  E. y  e.  RR  A. x  e. 
 RR  ( 0  <RR  x 
 ->  E. j  e.  N  A. k  e.  N  ( j  <RR  k  ->  (
 ( F `  k
 )  <RR  ( y  +  x )  /\  y  <RR  ( ( F `  k
 )  +  x ) ) ) ) )
 
18-Jul-2021mulnqpr 6675 Multiplication of fractions embedded into positive reals. One can either multiply the fractions as fractions, or embed them into positive reals and multiply them as positive reals, and get the same result. (Contributed by Jim Kingdon, 18-Jul-2021.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  <. { l  |  l  <Q  ( A  .Q  B ) } ,  { u  |  ( A  .Q  B )  <Q  u } >.  =  ( <. { l  |  l 
 <Q  A } ,  { u  |  A  <Q  u } >.  .P.  <. { l  |  l  <Q  B } ,  { u  |  B  <Q  u } >. ) )
 
18-Jul-2021mulnqprlemfu 6674 Lemma for mulnqpr 6675. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( 2nd `  <. { l  |  l  <Q  ( A  .Q  B ) } ,  { u  |  ( A  .Q  B ) 
 <Q  u } >. )  C_  ( 2nd `  ( <. { l  |  l  <Q  A } ,  { u  |  A  <Q  u } >.  .P.  <. { l  |  l  <Q  B } ,  { u  |  B  <Q  u } >. ) ) )
 
18-Jul-2021mulnqprlemfl 6673 Lemma for mulnqpr 6675. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( 1st `  <. { l  |  l  <Q  ( A  .Q  B ) } ,  { u  |  ( A  .Q  B ) 
 <Q  u } >. )  C_  ( 1st `  ( <. { l  |  l  <Q  A } ,  { u  |  A  <Q  u } >.  .P.  <. { l  |  l  <Q  B } ,  { u  |  B  <Q  u } >. ) ) )
 
18-Jul-2021mulnqprlemru 6672 Lemma for mulnqpr 6675. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( 2nd `  ( <. { l  |  l 
 <Q  A } ,  { u  |  A  <Q  u } >.  .P.  <. { l  |  l  <Q  B } ,  { u  |  B  <Q  u } >. ) ) 
 C_  ( 2nd `  <. { l  |  l  <Q  ( A  .Q  B ) } ,  { u  |  ( A  .Q  B ) 
 <Q  u } >. ) )
 
18-Jul-2021mulnqprlemrl 6671 Lemma for mulnqpr 6675. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( 1st `  ( <. { l  |  l 
 <Q  A } ,  { u  |  A  <Q  u } >.  .P.  <. { l  |  l  <Q  B } ,  { u  |  B  <Q  u } >. ) ) 
 C_  ( 1st `  <. { l  |  l  <Q  ( A  .Q  B ) } ,  { u  |  ( A  .Q  B ) 
 <Q  u } >. ) )
 
18-Jul-2021lt2mulnq 6503 Ordering property of multiplication for positive fractions. (Contributed by Jim Kingdon, 18-Jul-2021.)
 |-  ( ( ( A  e.  Q.  /\  B  e.  Q. )  /\  ( C  e.  Q.  /\  D  e.  Q. ) )  ->  ( ( A  <Q  B 
 /\  C  <Q  D ) 
 ->  ( A  .Q  C )  <Q  ( B  .Q  D ) ) )
 
17-Jul-2021recidpirqlemcalc 6933 Lemma for recidpirq 6934. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.)
 |-  ( ph  ->  A  e.  P. )   &    |-  ( ph  ->  B  e.  P. )   &    |-  ( ph  ->  ( A  .P.  B )  =  1P )   =>    |-  ( ph  ->  ( ( ( ( A  +P.  1P )  .P.  ( B  +P.  1P ) )  +P.  ( 1P  .P.  1P ) ) 
 +P.  1P )  =  ( ( ( ( A 
 +P.  1P )  .P.  1P )  +P.  ( 1P  .P.  ( B  +P.  1P )
 ) )  +P.  ( 1P  +P.  1P ) ) )
 
17-Jul-2021recidpipr 6932 Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.)
 |-  ( N  e.  N.  ->  ( <. { l  |  l  <Q  [ <. N ,  1o >. ]  ~Q  } ,  { u  |  [ <. N ,  1o >. ] 
 ~Q  <Q  u } >.  .P.  <. { l  |  l 
 <Q  ( *Q `  [ <. N ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. N ,  1o >. ]  ~Q  )  <Q  u } >. )  =  1P )
 
15-Jul-2021rereceu 6963 The reciprocal from axprecex 6954 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.)
 |-  ( ( A  e.  RR  /\  0  <RR  A ) 
 ->  E! x  e.  RR  ( A  x.  x )  =  1 )
 
15-Jul-2021recidpirq 6934 A real number times its reciprocal is one, where reciprocal is expressed with  *Q. (Contributed by Jim Kingdon, 15-Jul-2021.)
 |-  ( N  e.  N.  ->  ( <. [ <. ( <. { l  |  l  <Q  [
 <. N ,  1o >. ] 
 ~Q  } ,  { u  |  [ <. N ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  <. [ <. (
 <. { l  |  l 
 <Q  ( *Q `  [ <. N ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. N ,  1o >. ]  ~Q  )  <Q  u } >.  +P. 
 1P ) ,  1P >. ]  ~R  ,  0R >. )  =  1 )
 
15-Jul-2021recnnre 6927 Embedding the reciprocal of a natural number into  RR. (Contributed by Jim Kingdon, 15-Jul-2021.)
 |-  ( N  e.  N.  -> 
 <. [ <. ( <. { l  |  l  <Q  ( *Q ` 
 [ <. N ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. N ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  RR )
 
15-Jul-2021pitore 6926 Embedding from  N. to  RR. Similar to pitonn 6924 but separate in the sense that we have not proved nnssre 7918 yet. (Contributed by Jim Kingdon, 15-Jul-2021.)
 |-  ( N  e.  N.  -> 
 <. [ <. ( <. { l  |  l  <Q  [ <. N ,  1o >. ]  ~Q  } ,  { u  |  [ <. N ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  e.  RR )
 
15-Jul-2021pitoregt0 6925 Embedding from  N. to  RR yields a number greater than zero. (Contributed by Jim Kingdon, 15-Jul-2021.)
 |-  ( N  e.  N.  ->  0  <RR  <. [ <. ( <. { l  |  l  <Q  [
 <. N ,  1o >. ] 
 ~Q  } ,  { u  |  [ <. N ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )
 
14-Jul-2021adddivflid 9134 The floor of a sum of an integer and a fraction is equal to the integer iff the denominator of the fraction is less than the numerator. (Contributed by AV, 14-Jul-2021.)
 |-  ( ( A  e.  ZZ  /\  B  e.  NN0  /\  C  e.  NN )  ->  ( B  <  C  <->  ( |_ `  ( A  +  ( B  /  C ) ) )  =  A ) )
 
14-Jul-2021nnindnn 6967 Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 7930 designed for real number axioms which involve natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1
 )  e.  x ) }   &    |-  ( z  =  1  ->  ( ph  <->  ps ) )   &    |-  ( z  =  k  ->  ( ph  <->  ch ) )   &    |-  ( z  =  ( k  +  1 )  ->  ( ph  <->  th ) )   &    |-  ( z  =  A  ->  ( ph  <->  ta ) )   &    |-  ps   &    |-  ( k  e.  N  ->  ( ch  ->  th ) )   =>    |-  ( A  e.  N  ->  ta )
 
14-Jul-2021peano5nnnn 6966 Peano's inductive postulate. This is a counterpart to peano5nni 7917 designed for real number axioms which involve natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1
 )  e.  x ) }   =>    |-  ( ( 1  e.  A  /\  A. z  e.  A  ( z  +  1 )  e.  A )  ->  N  C_  A )
 
14-Jul-2021peano2nnnn 6929 A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 7926 designed for real number axioms which involve to natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1
 )  e.  x ) }   =>    |-  ( A  e.  N  ->  ( A  +  1 )  e.  N )
 
14-Jul-2021peano1nnnn 6928 One is an element of  NN. This is a counterpart to 1nn 7925 designed for real number axioms which involve natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1
 )  e.  x ) }   =>    |-  1  e.  N
 
14-Jul-2021addvalex 6920 Existence of a sum. This is dependent on how we define  + so once we proceed to real number axioms we will replace it with theorems such as addcl 7006. (Contributed by Jim Kingdon, 14-Jul-2021.)
 |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  +  B )  e.  _V )
 
13-Jul-2021nntopi 6968 Mapping from  NN to  N.. (Contributed by Jim Kingdon, 13-Jul-2021.)
 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1
 )  e.  x ) }   =>    |-  ( A  e.  N  ->  E. z  e.  N.  <. [ <. ( <. { l  |  l  <Q  [ <. z ,  1o >. ]  ~Q  } ,  { u  |  [ <. z ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  =  A )
 
13-Jul-2021ltrennb 6930 Ordering of natural numbers with 
<N or  <RR. (Contributed by Jim Kingdon, 13-Jul-2021.)
 |-  ( ( J  e.  N. 
 /\  K  e.  N. )  ->  ( J  <N  K  <->  <. [ <. ( <. { l  |  l  <Q  [ <. J ,  1o >. ]  ~Q  } ,  { u  |  [ <. J ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  <. [ <. ( <. { l  |  l  <Q  [
 <. K ,  1o >. ] 
 ~Q  } ,  { u  |  [ <. K ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. ) )
 
12-Jul-2021ltrenn 6931 Ordering of natural numbers with 
<N or  <RR. (Contributed by Jim Kingdon, 12-Jul-2021.)
 |-  ( J  <N  K  ->  <. [ <. ( <. { l  |  l  <Q  [ <. J ,  1o >. ]  ~Q  } ,  { u  |  [ <. J ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  <RR  <. [ <. ( <. { l  |  l  <Q  [
 <. K ,  1o >. ] 
 ~Q  } ,  { u  |  [ <. K ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )
 
11-Jul-2021recriota 6964 Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.)
 |-  ( N  e.  N.  ->  ( iota_ r  e.  RR  ( <. [ <. ( <. { l  |  l  <Q  [
 <. N ,  1o >. ] 
 ~Q  } ,  { u  |  [ <. N ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >.  x.  r )  =  1 )  = 
 <. [ <. ( <. { l  |  l  <Q  ( *Q ` 
 [ <. N ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. N ,  1o >. ]  ~Q  )  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )
 
11-Jul-2021elrealeu 6906 The real number mapping in elreal 6905 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.)
 |-  ( A  e.  RR  <->  E! x  e.  R.  <. x ,  0R >.  =  A )
 
10-Jul-2021axcaucvglemres 6973 Lemma for axcaucvg 6974. Mapping the limit from  N. and  R.. (Contributed by Jim Kingdon, 10-Jul-2021.)
 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1
 )  e.  x ) }   &    |-  ( ph  ->  F : N --> RR )   &    |-  ( ph  ->  A. n  e.  N  A. k  e.  N  ( n  <RR  k  ->  (
 ( F `  n )  <RR  ( ( F `
  k )  +  ( iota_ r  e.  RR  ( n  x.  r
 )  =  1 ) )  /\  ( F `
  k )  <RR  ( ( F `  n )  +  ( iota_ r  e. 
 RR  ( n  x.  r )  =  1
 ) ) ) ) )   &    |-  G  =  ( j  e.  N.  |->  (
 iota_ z  e.  R.  ( F `  <. [ <. (
 <. { l  |  l 
 <Q  [ <. j ,  1o >. ]  ~Q  } ,  { u  |  [ <. j ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. z ,  0R >. ) )   =>    |-  ( ph  ->  E. y  e.  RR  A. x  e. 
 RR  ( 0  <RR  x 
 ->  E. j  e.  N  A. k  e.  N  ( j  <RR  k  ->  (
 ( F `  k
 )  <RR  ( y  +  x )  /\  y  <RR  ( ( F `  k
 )  +  x ) ) ) ) )
 
10-Jul-2021axcaucvglemval 6971 Lemma for axcaucvg 6974. Value of sequence when mapping to  N. and  R.. (Contributed by Jim Kingdon, 10-Jul-2021.)
 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1
 )  e.  x ) }   &    |-  ( ph  ->  F : N --> RR )   &    |-  ( ph  ->  A. n  e.  N  A. k  e.  N  ( n  <RR  k  ->  (
 ( F `  n )  <RR  ( ( F `
  k )  +  ( iota_ r  e.  RR  ( n  x.  r
 )  =  1 ) )  /\  ( F `
  k )  <RR  ( ( F `  n )  +  ( iota_ r  e. 
 RR  ( n  x.  r )  =  1
 ) ) ) ) )   &    |-  G  =  ( j  e.  N.  |->  (
 iota_ z  e.  R.  ( F `  <. [ <. (
 <. { l  |  l 
 <Q  [ <. j ,  1o >. ]  ~Q  } ,  { u  |  [ <. j ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. z ,  0R >. ) )   =>    |-  ( ( ph  /\  J  e.  N. )  ->  ( F `  <. [ <. ( <. { l  |  l  <Q  [
 <. J ,  1o >. ] 
 ~Q  } ,  { u  |  [ <. J ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. ( G `  J ) ,  0R >. )
 
10-Jul-2021axcaucvglemcl 6969 Lemma for axcaucvg 6974. Mapping to  N. and  R.. (Contributed by Jim Kingdon, 10-Jul-2021.)
 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1
 )  e.  x ) }   &    |-  ( ph  ->  F : N --> RR )   =>    |-  (
 ( ph  /\  J  e.  N. )  ->  ( iota_ z  e. 
 R.  ( F `  <. [ <. ( <. { l  |  l  <Q  [ <. J ,  1o >. ]  ~Q  } ,  { u  |  [ <. J ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. z ,  0R >. )  e. 
 R. )
 
9-Jul-2021axcaucvglemcau 6972 Lemma for axcaucvg 6974. The result of mapping to  N. and  R. satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.)
 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1
 )  e.  x ) }   &    |-  ( ph  ->  F : N --> RR )   &    |-  ( ph  ->  A. n  e.  N  A. k  e.  N  ( n  <RR  k  ->  (
 ( F `  n )  <RR  ( ( F `
  k )  +  ( iota_ r  e.  RR  ( n  x.  r
 )  =  1 ) )  /\  ( F `
  k )  <RR  ( ( F `  n )  +  ( iota_ r  e. 
 RR  ( n  x.  r )  =  1
 ) ) ) ) )   &    |-  G  =  ( j  e.  N.  |->  (
 iota_ z  e.  R.  ( F `  <. [ <. (
 <. { l  |  l 
 <Q  [ <. j ,  1o >. ]  ~Q  } ,  { u  |  [ <. j ,  1o >. ]  ~Q  <Q  u } >.  +P.  1P ) ,  1P >. ]  ~R  ,  0R >. )  =  <. z ,  0R >. ) )   =>    |-  ( ph  ->  A. n  e. 
 N.  A. k  e.  N.  ( n  <N  k  ->  ( ( G `  n )  <R  ( ( G `  k )  +R  [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P. 
 1P ) ,  1P >. ]  ~R  )  /\  ( G `  k )  <R  ( ( G `  n )  +R  [ <. ( <. { l  |  l  <Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >.  +P. 
 1P ) ,  1P >. ]  ~R  ) ) ) )