HomeHome Intuitionistic Logic Explorer
Theorem List (p. 99 of 106)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 9801-9900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremimmul2d 9801 Imaginary part of a product. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  CC )   =>    |-  ( ph  ->  ( Im `  ( A  x.  B ) )  =  ( A  x.  ( Im `  B ) ) )
 
Theoremredivapd 9802 Real part of a division. Related to remul2 9701. (Contributed by Jim Kingdon, 15-Jun-2020.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  A #  0 )   =>    |-  ( ph  ->  ( Re `  ( B  /  A ) )  =  ( ( Re `  B ) 
 /  A ) )
 
Theoremimdivapd 9803 Imaginary part of a division. Related to remul2 9701. (Contributed by Jim Kingdon, 15-Jun-2020.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  A #  0 )   =>    |-  ( ph  ->  ( Im `  ( B  /  A ) )  =  ( ( Im `  B ) 
 /  A ) )
 
Theoremcrred 9804 The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   =>    |-  ( ph  ->  ( Re `  ( A  +  ( _i  x.  B ) ) )  =  A )
 
Theoremcrimd 9805 The imaginary part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by Mario Carneiro, 29-May-2016.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   =>    |-  ( ph  ->  ( Im `  ( A  +  ( _i  x.  B ) ) )  =  B )
 
3.7.3  Sequence convergence
 
Theoremcaucvgrelemrec 9806* 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 ) )
 
Theoremcaucvgrelemcau 9807* Lemma for caucvgre 9808. 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
 ) ) ) ) )
 
Theoremcaucvgre 9808* 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 ) ) )
 
Theoremcvg1nlemcxze 9809 Lemma for cvg1n 9813. 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
 ) )
 
Theoremcvg1nlemf 9810* Lemma for cvg1n 9813. 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 )
 
Theoremcvg1nlemcau 9811* Lemma for cvg1n 9813. 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 ) ) ) )
 
Theoremcvg1nlemres 9812* Lemma for cvg1n 9813. 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 ) ) )
 
Theoremcvg1n 9813* Convergence of real sequences.

This is a version of caucvgre 9808 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 ) ) )
 
Theoremuzin2 9814 The upper integers are closed under intersection. (Contributed by Mario Carneiro, 24-Dec-2013.)
 |-  ( ( A  e.  ran  ZZ>= 
 /\  B  e.  ran  ZZ>= )  ->  ( A  i^i  B )  e.  ran  ZZ>= )
 
Theoremrexanuz 9815* Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 25-Dec-2013.)
 |-  ( E. j  e. 
 ZZ  A. k  e.  ( ZZ>=
 `  j ) (
 ph  /\  ps )  <->  ( E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j ) ph  /\  E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j ) ps ) )
 
Theoremrexfiuz 9816* Combine finitely many different upper integer properties into one. (Contributed by Mario Carneiro, 6-Jun-2014.)
 |-  ( A  e.  Fin  ->  ( E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j ) A. n  e.  A  ph  <->  A. n  e.  A  E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j ) ph )
 )
 
Theoremrexuz3 9817* Restrict the base of the upper integers set to another upper integers set. (Contributed by Mario Carneiro, 26-Dec-2013.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( M  e.  ZZ  ->  ( E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ph 
 <-> 
 E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j ) ph )
 )
 
Theoremrexanuz2 9818* Combine two different upper integer properties into one. (Contributed by Mario Carneiro, 26-Dec-2013.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
 ( ph  /\  ps )  <->  ( E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ph  /\  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ps ) )
 
Theoremr19.29uz 9819* A version of 19.29 1527 for upper integer quantifiers. (Contributed by Mario Carneiro, 10-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( ( A. k  e.  Z  ph  /\  E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ps )  ->  E. j  e.  Z  A. k  e.  ( ZZ>= `  j )
 ( ph  /\  ps )
 )
 
Theoremr19.2uz 9820* A version of r19.2m 3337 for upper integer quantifiers. (Contributed by Mario Carneiro, 15-Feb-2014.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( E. j  e.  Z  A. k  e.  ( ZZ>= `  j ) ph  ->  E. k  e.  Z  ph )
 
Theoremrecvguniqlem 9821 Lemma for recvguniq 9822. 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.  )
 
Theoremrecvguniq 9822* 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 )
 
3.7.4  Square root; absolute value
 
Syntaxcsqrt 9823 Extend class notation to include square root of a complex number.
 class  sqr
 
Syntaxcabs 9824 Extend class notation to include a function for the absolute value (modulus) of a complex number.
 class  abs
 
Definitiondf-rsqrt 9825* Define a function whose value is the square root of a nonnegative real number.

Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root.

(Contributed by Jim Kingdon, 23-Aug-2020.)

 |- 
 sqr  =  ( x  e.  RR  |->  ( iota_ y  e. 
 RR  ( ( y ^ 2 )  =  x  /\  0  <_  y ) ) )
 
Definitiondf-abs 9826 Define the function for the absolute value (modulus) of a complex number. (Contributed by NM, 27-Jul-1999.)
 |- 
 abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  ( * `  x ) ) ) )
 
Theoremsqrtrval 9827* Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.)
 |-  ( A  e.  RR  ->  ( sqr `  A )  =  ( iota_ x  e. 
 RR  ( ( x ^ 2 )  =  A  /\  0  <_  x ) ) )
 
Theoremabsval 9828 The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of [Gleason] p. 133. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
 |-  ( A  e.  CC  ->  ( abs `  A )  =  ( sqr `  ( A  x.  ( * `  A ) ) ) )
 
Theoremrennim 9829 A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013.)
 |-  ( A  e.  RR  ->  ( _i  x.  A )  e/  RR+ )
 
Theoremsqrt0rlem 9830 Lemma for sqrt0 9831. (Contributed by Jim Kingdon, 26-Aug-2020.)
 |-  ( ( A  e.  RR  /\  ( ( A ^ 2 )  =  0  /\  0  <_  A ) )  <->  A  =  0
 )
 
Theoremsqrt0 9831 Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013.)
 |-  ( sqr `  0
 )  =  0
 
Theoremresqrexlem1arp 9832* Lemma for resqrex 9853.  1  +  A is a positive real (expressed in a way that will help apply iseqf 9388 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+ )
 
Theoremresqrexlemp1rp 9833* Lemma for resqrex 9853. Applying the recursion rule yields a positive real (expressed in a way that will help apply iseqf 9388 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+ )
 
Theoremresqrexlemf 9834* Lemma for resqrex 9853. 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+ )
 
Theoremresqrexlemf1 9835* Lemma for resqrex 9853. 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 ) )
 
Theoremresqrexlemfp1 9836* Lemma for resqrex 9853. 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 ) )
 
Theoremresqrexlemover 9837* Lemma for resqrex 9853. 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
 ) )
 
Theoremresqrexlemdec 9838* Lemma for resqrex 9853. 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 ) )
 
Theoremresqrexlemdecn 9839* Lemma for resqrex 9853. 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 ) )
 
Theoremresqrexlemlo 9840* Lemma for resqrex 9853. 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 ) )
 
Theoremresqrexlemcalc1 9841* Lemma for resqrex 9853. 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 ) ) ) )
 
Theoremresqrexlemcalc2 9842* Lemma for resqrex 9853. 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
 ) )
 
Theoremresqrexlemcalc3 9843* Lemma for resqrex 9853. 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 ) ) ) )
 
Theoremresqrexlemnmsq 9844* Lemma for resqrex 9853. 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 ) ) ) )
 
Theoremresqrexlemnm 9845* Lemma for resqrex 9853. 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 ) ) ) )
 
Theoremresqrexlemcvg 9846* Lemma for resqrex 9853. 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 ) ) )
 
Theoremresqrexlemgt0 9847* Lemma for resqrex 9853. 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 )
 
Theoremresqrexlemoverl 9848* Lemma for resqrex 9853. 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 ) )
 
Theoremresqrexlemglsq 9849* Lemma for resqrex 9853. 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
 ) ) )
 
Theoremresqrexlemga 9850* Lemma for resqrex 9853. 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 ) ) )
 
Theoremresqrexlemsqa 9851* Lemma for resqrex 9853. 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 )
 
Theoremresqrexlemex 9852* Lemma for resqrex 9853. 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 ) )
 
Theoremresqrex 9853* Existence of a square root for positive reals. (Contributed by Mario Carneiro, 9-Jul-2013.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  E. x  e.  RR  ( 0  <_  x  /\  ( x ^ 2
 )  =  A ) )
 
Theoremrsqrmo 9854* 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 ) )
 
Theoremrersqreu 9855* 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 ) )
 
Theoremresqrtcl 9856 Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  ( sqr `  A )  e.  RR )
 
Theoremrersqrtthlem 9857 Lemma for resqrtth 9858. (Contributed by Jim Kingdon, 10-Aug-2021.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  ( ( ( sqr `  A ) ^ 2 )  =  A  /\  0  <_  ( sqr `  A )
 ) )
 
Theoremresqrtth 9858 Square root theorem over the reals. Theorem I.35 of [Apostol] p. 29. (Contributed by Mario Carneiro, 9-Jul-2013.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  ( ( sqr `  A ) ^ 2
 )  =  A )
 
Theoremremsqsqrt 9859 Square of square root. (Contributed by Mario Carneiro, 10-Jul-2013.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  ( ( sqr `  A )  x.  ( sqr `  A ) )  =  A )
 
Theoremsqrtge0 9860 The square root function is nonnegative for nonnegative input. (Contributed by NM, 26-May-1999.) (Revised by Mario Carneiro, 9-Jul-2013.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  0  <_  ( sqr `  A ) )
 
Theoremsqrtgt0 9861 The square root function is positive for positive input. (Contributed by Mario Carneiro, 10-Jul-2013.) (Revised by Mario Carneiro, 6-Sep-2013.)
 |-  ( ( A  e.  RR  /\  0  <  A )  ->  0  <  ( sqr `  A ) )
 
Theoremsqrtmul 9862 Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
 |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  ( B  e.  RR  /\  0  <_  B ) )  ->  ( sqr `  ( A  x.  B ) )  =  ( ( sqr `  A )  x.  ( sqr `  B ) ) )
 
Theoremsqrtle 9863 Square root is monotonic. (Contributed by NM, 17-Mar-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
 |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  ( B  e.  RR  /\  0  <_  B ) )  ->  ( A  <_  B  <->  ( sqr `  A )  <_  ( sqr `  B ) ) )
 
Theoremsqrtlt 9864 Square root is strictly monotonic. Closed form of sqrtlti 9964. (Contributed by Scott Fenton, 17-Apr-2014.) (Proof shortened by Mario Carneiro, 29-May-2016.)
 |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  ( B  e.  RR  /\  0  <_  B ) )  ->  ( A  <  B  <->  ( sqr `  A )  <  ( sqr `  B ) ) )
 
Theoremsqrt11ap 9865 Analogue to sqrt11 9866 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 ) )
 
Theoremsqrt11 9866 The square root function is one-to-one. Also see sqrt11ap 9865 which would follow easily from this given excluded middle, but which is proved another way without it. (Contributed by Scott Fenton, 11-Jun-2013.)
 |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  ( B  e.  RR  /\  0  <_  B ) )  ->  ( ( sqr `  A )  =  ( sqr `  B )  <->  A  =  B ) )
 
Theoremsqrt00 9867 A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999.) (Proof shortened by Mario Carneiro, 29-May-2016.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  ( ( sqr `  A )  =  0  <->  A  =  0 )
 )
 
Theoremrpsqrtcl 9868 The square root of a positive real is a positive real. (Contributed by NM, 22-Feb-2008.)
 |-  ( A  e.  RR+  ->  ( sqr `  A )  e.  RR+ )
 
Theoremsqrtdiv 9869 Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016.)
 |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  B  e.  RR+ )  ->  ( sqr `  ( A  /  B ) )  =  ( ( sqr `  A )  /  ( sqr `  B ) ) )
 
Theoremsqrtsq2 9870 Relationship between square root and squares. (Contributed by NM, 31-Jul-1999.) (Revised by Mario Carneiro, 29-May-2016.)
 |-  ( ( ( A  e.  RR  /\  0  <_  A )  /\  ( B  e.  RR  /\  0  <_  B ) )  ->  ( ( sqr `  A )  =  B  <->  A  =  ( B ^ 2 ) ) )
 
Theoremsqrtsq 9871 Square root of square. (Contributed by NM, 14-Jan-2006.) (Revised by Mario Carneiro, 29-May-2016.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  ( sqr `  ( A ^ 2 ) )  =  A )
 
Theoremsqrtmsq 9872 Square root of square. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 29-May-2016.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  ( sqr `  ( A  x.  A ) )  =  A )
 
Theoremsqrt1 9873 The square root of 1 is 1. (Contributed by NM, 31-Jul-1999.)
 |-  ( sqr `  1
 )  =  1
 
Theoremsqrt4 9874 The square root of 4 is 2. (Contributed by NM, 3-Aug-1999.)
 |-  ( sqr `  4
 )  =  2
 
Theoremsqrt9 9875 The square root of 9 is 3. (Contributed by NM, 11-May-2004.)
 |-  ( sqr `  9
 )  =  3
 
Theoremsqrt2gt1lt2 9876 The square root of 2 is bounded by 1 and 2. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 6-Sep-2013.)
 |-  ( 1  <  ( sqr `  2 )  /\  ( sqr `  2 )  <  2 )
 
Theoremabsneg 9877 Absolute value of negative. (Contributed by NM, 27-Feb-2005.)
 |-  ( A  e.  CC  ->  ( abs `  -u A )  =  ( abs `  A ) )
 
Theoremabscl 9878 Real closure of absolute value. (Contributed by NM, 3-Oct-1999.)
 |-  ( A  e.  CC  ->  ( abs `  A )  e.  RR )
 
Theoremabscj 9879 The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by NM, 28-Apr-2005.)
 |-  ( A  e.  CC  ->  ( abs `  ( * `  A ) )  =  ( abs `  A ) )
 
Theoremabsvalsq 9880 Square of value of absolute value function. (Contributed by NM, 16-Jan-2006.)
 |-  ( A  e.  CC  ->  ( ( abs `  A ) ^ 2 )  =  ( A  x.  ( * `  A ) ) )
 
Theoremabsvalsq2 9881 Square of value of absolute value function. (Contributed by NM, 1-Feb-2007.)
 |-  ( A  e.  CC  ->  ( ( abs `  A ) ^ 2 )  =  ( ( ( Re
 `  A ) ^
 2 )  +  (
 ( Im `  A ) ^ 2 ) ) )
 
Theoremsqabsadd 9882 Square of absolute value of sum. Proposition 10-3.7(g) of [Gleason] p. 133. (Contributed by NM, 21-Jan-2007.)
 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( abs `  ( A  +  B ) ) ^ 2
 )  =  ( ( ( ( abs `  A ) ^ 2 )  +  ( ( abs `  B ) ^ 2 ) )  +  ( 2  x.  ( Re `  ( A  x.  ( * `  B ) ) ) ) ) )
 
Theoremsqabssub 9883 Square of absolute value of difference. (Contributed by NM, 21-Jan-2007.)
 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( abs `  ( A  -  B ) ) ^ 2
 )  =  ( ( ( ( abs `  A ) ^ 2 )  +  ( ( abs `  B ) ^ 2 ) )  -  ( 2  x.  ( Re `  ( A  x.  ( * `  B ) ) ) ) ) )
 
Theoremabsval2 9884 Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by NM, 17-Mar-2005.)
 |-  ( A  e.  CC  ->  ( abs `  A )  =  ( sqr `  ( ( ( Re
 `  A ) ^
 2 )  +  (
 ( Im `  A ) ^ 2 ) ) ) )
 
Theoremabs0 9885 The absolute value of 0. (Contributed by NM, 26-Mar-2005.) (Revised by Mario Carneiro, 29-May-2016.)
 |-  ( abs `  0
 )  =  0
 
Theoremabsi 9886 The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005.)
 |-  ( abs `  _i )  =  1
 
Theoremabsge0 9887 Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004.) (Revised by Mario Carneiro, 29-May-2016.)
 |-  ( A  e.  CC  ->  0  <_  ( abs `  A ) )
 
Theoremabsrpclap 9888 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+ )
 
Theoremabs00ap 9889 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 )
 )
 
Theoremabsext 9890 Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.)
 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( abs `  A ) #  ( abs `  B )  ->  A #  B ) )
 
Theoremabs00 9891 The absolute value of a number is zero iff the number is zero. Also see abs00ap 9889 which is similar but for apartness. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by NM, 26-Sep-2005.) (Proof shortened by Mario Carneiro, 29-May-2016.)
 |-  ( A  e.  CC  ->  ( ( abs `  A )  =  0  <->  A  =  0
 ) )
 
Theoremabs00ad 9892 A complex number is zero iff its absolute value is zero. Deduction form of abs00 9891. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  e.  CC )   =>    |-  ( ph  ->  (
 ( abs `  A )  =  0  <->  A  =  0
 ) )
 
Theoremabs00bd 9893 If a complex number is zero, its absolute value is zero. (Contributed by David Moews, 28-Feb-2017.)
 |-  ( ph  ->  A  =  0 )   =>    |-  ( ph  ->  ( abs `  A )  =  0 )
 
Theoremabsreimsq 9894 Square of the absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 1-Feb-2007.)
 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( ( abs `  ( A  +  ( _i  x.  B ) ) ) ^ 2 )  =  ( ( A ^ 2 )  +  ( B ^ 2 ) ) )
 
Theoremabsreim 9895 Absolute value of a number that has been decomposed into real and imaginary parts. (Contributed by NM, 14-Jan-2006.)
 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( abs `  ( A  +  ( _i  x.  B ) ) )  =  ( sqr `  (
 ( A ^ 2
 )  +  ( B ^ 2 ) ) ) )
 
Theoremabsmul 9896 Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( abs `  ( A  x.  B ) )  =  ( ( abs `  A )  x.  ( abs `  B ) ) )
 
Theoremabsdivap 9897 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 ) ) )
 
Theoremabsid 9898 A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 29-May-2016.)
 |-  ( ( A  e.  RR  /\  0  <_  A )  ->  ( abs `  A )  =  A )
 
Theoremabs1 9899 The absolute value of 1. Common special case. (Contributed by David A. Wheeler, 16-Jul-2016.)
 |-  ( abs `  1
 )  =  1
 
Theoremabsnid 9900 A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005.)
 |-  ( ( A  e.  RR  /\  A  <_  0
 )  ->  ( abs `  A )  =  -u A )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10511
  Copyright terms: Public domain < Previous  Next >