HomeHome Intuitionistic Logic Explorer
Theorem List (p. 122 of 137)
< 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 - 12101-12200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremphiprmpw 12101 Value of the Euler  phi function at a prime power. Theorem 2.5(a) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
 |-  ( ( P  e.  Prime  /\  K  e.  NN )  ->  ( phi `  ( P ^ K ) )  =  ( ( P ^ ( K  -  1 ) )  x.  ( P  -  1
 ) ) )
 
Theoremphiprm 12102 Value of the Euler  phi function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.)
 |-  ( P  e.  Prime  ->  ( phi `  P )  =  ( P  -  1
 ) )
 
Theoremcrth 12103* The Chinese Remainder Theorem: the function that maps  x to its remainder classes  mod  M and  mod  N is 1-1 and onto when  M and  N are coprime. (Contributed by Mario Carneiro, 24-Feb-2014.) (Proof shortened by Mario Carneiro, 2-May-2016.)
 |-  S  =  ( 0..^ ( M  x.  N ) )   &    |-  T  =  ( ( 0..^ M )  X.  ( 0..^ N ) )   &    |-  F  =  ( x  e.  S  |->  <.
 ( x  mod  M ) ,  ( x  mod  N ) >. )   &    |-  ( ph  ->  ( M  e.  NN  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )
 )   =>    |-  ( ph  ->  F : S -1-1-onto-> T )
 
Theoremphimullem 12104* Lemma for phimul 12105. (Contributed by Mario Carneiro, 24-Feb-2014.)
 |-  S  =  ( 0..^ ( M  x.  N ) )   &    |-  T  =  ( ( 0..^ M )  X.  ( 0..^ N ) )   &    |-  F  =  ( x  e.  S  |->  <.
 ( x  mod  M ) ,  ( x  mod  N ) >. )   &    |-  ( ph  ->  ( M  e.  NN  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )
 )   &    |-  U  =  { y  e.  ( 0..^ M )  |  ( y  gcd  M )  =  1 }   &    |-  V  =  { y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  W  =  { y  e.  S  |  ( y 
 gcd  ( M  x.  N ) )  =  1 }   =>    |-  ( ph  ->  ( phi `  ( M  x.  N ) )  =  ( ( phi `  M )  x.  ( phi `  N ) ) )
 
Theoremphimul 12105 The Euler  phi function is a multiplicative function, meaning that it distributes over multiplication at relatively prime arguments. Theorem 2.5(c) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
 |-  ( ( M  e.  NN  /\  N  e.  NN  /\  ( M  gcd  N )  =  1 )  ->  ( phi `  ( M  x.  N ) )  =  ( ( phi `  M )  x.  ( phi `  N ) ) )
 
Theoremeulerthlem1 12106* Lemma for eulerth 12112. (Contributed by Mario Carneiro, 8-May-2015.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  T  =  ( 1 ... ( phi `  N ) )   &    |-  ( ph  ->  F : T
 -1-1-onto-> S )   &    |-  G  =  ( x  e.  T  |->  ( ( A  x.  ( F `  x ) ) 
 mod  N ) )   =>    |-  ( ph  ->  G : T --> S )
 
Theoremeulerthlemfi 12107* Lemma for eulerth 12112. The set  S is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   =>    |-  ( ph  ->  S  e.  Fin )
 
Theoremeulerthlemrprm 12108* Lemma for eulerth 12112. 
N and  prod_ x  e.  ( 1 ... ( phi `  N ) ) ( F `  x
) are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  ( ph  ->  F : ( 1 ... ( phi `  N ) ) -1-1-onto-> S )   =>    |-  ( ph  ->  ( N  gcd  prod_ x  e.  (
 1 ... ( phi `  N ) ) ( F `
  x ) )  =  1 )
 
Theoremeulerthlema 12109* Lemma for eulerth 12112. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  ( ph  ->  F : ( 1 ... ( phi `  N ) ) -1-1-onto-> S )   =>    |-  ( ph  ->  ( (
 ( A ^ ( phi `  N ) )  x.  prod_ x  e.  (
 1 ... ( phi `  N ) ) ( F `
  x ) ) 
 mod  N )  =  (
 prod_ x  e.  (
 1 ... ( phi `  N ) ) ( ( A  x.  ( F `
  x ) ) 
 mod  N )  mod  N ) )
 
Theoremeulerthlemh 12110* Lemma for eulerth 12112. A permutation of  ( 1 ... ( phi `  N ) ). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  ( ph  ->  F : ( 1 ... ( phi `  N ) ) -1-1-onto-> S )   &    |-  H  =  ( `' F  o.  ( y  e.  ( 1 ... ( phi `  N ) ) 
 |->  ( ( A  x.  ( F `  y ) )  mod  N ) ) )   =>    |-  ( ph  ->  H : ( 1 ... ( phi `  N ) ) -1-1-onto-> ( 1 ... ( phi `  N ) ) )
 
Theoremeulerthlemth 12111* Lemma for eulerth 12112. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
 |-  ( ph  ->  ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 ) )   &    |-  S  =  {
 y  e.  ( 0..^ N )  |  ( y  gcd  N )  =  1 }   &    |-  ( ph  ->  F : ( 1 ... ( phi `  N ) ) -1-1-onto-> S )   =>    |-  ( ph  ->  ( ( A ^ ( phi `  N ) )  mod  N )  =  ( 1  mod 
 N ) )
 
Theoremeulerth 12112 Euler's theorem, a generalization of Fermat's little theorem. If  A and  N are coprime, then  A ^ phi ( N )  ==  1 (mod  N). This is Metamath 100 proof #10. Also called Euler-Fermat theorem, see theorem 5.17 in [ApostolNT] p. 113. (Contributed by Mario Carneiro, 28-Feb-2014.)
 |-  ( ( N  e.  NN  /\  A  e.  ZZ  /\  ( A  gcd  N )  =  1 )  ->  ( ( A ^
 ( phi `  N ) )  mod  N )  =  ( 1  mod 
 N ) )
 
Theoremfermltl 12113 Fermat's little theorem. When  P is prime,  A ^ P  ==  A (mod  P) for any  A, see theorem 5.19 in [ApostolNT] p. 114. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 19-Mar-2022.)
 |-  ( ( P  e.  Prime  /\  A  e.  ZZ )  ->  ( ( A ^ P )  mod  P )  =  ( A 
 mod  P ) )
 
Theoremprmdiv 12114 Show an explicit expression for the modular inverse of  A  mod  P. (Contributed by Mario Carneiro, 24-Jan-2015.)
 |-  R  =  ( ( A ^ ( P  -  2 ) ) 
 mod  P )   =>    |-  ( ( P  e.  Prime  /\  A  e.  ZZ  /\ 
 -.  P  ||  A )  ->  ( R  e.  ( 1 ... ( P  -  1 ) ) 
 /\  P  ||  (
 ( A  x.  R )  -  1 ) ) )
 
Theoremprmdiveq 12115 The modular inverse of  A  mod  P is unique. (Contributed by Mario Carneiro, 24-Jan-2015.)
 |-  R  =  ( ( A ^ ( P  -  2 ) ) 
 mod  P )   =>    |-  ( ( P  e.  Prime  /\  A  e.  ZZ  /\ 
 -.  P  ||  A )  ->  ( ( S  e.  ( 0 ... ( P  -  1
 ) )  /\  P  ||  ( ( A  x.  S )  -  1
 ) )  <->  S  =  R ) )
 
Theoremprmdivdiv 12116 The (modular) inverse of the inverse of a number is itself. (Contributed by Mario Carneiro, 24-Jan-2015.)
 |-  R  =  ( ( A ^ ( P  -  2 ) ) 
 mod  P )   =>    |-  ( ( P  e.  Prime  /\  A  e.  (
 1 ... ( P  -  1 ) ) ) 
 ->  A  =  ( ( R ^ ( P  -  2 ) ) 
 mod  P ) )
 
Theoremhashgcdlem 12117* A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
 |-  A  =  { y  e.  ( 0..^ ( M 
 /  N ) )  |  ( y  gcd  ( M  /  N ) )  =  1 }   &    |-  B  =  { z  e.  ( 0..^ M )  |  ( z  gcd  M )  =  N }   &    |-  F  =  ( x  e.  A  |->  ( x  x.  N ) )   =>    |-  ( ( M  e.  NN  /\  N  e.  NN  /\  N  ||  M )  ->  F : A -1-1-onto-> B )
 
Theoremhashgcdeq 12118* Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.)
 |-  ( ( M  e.  NN  /\  N  e.  NN )  ->  ( `  { x  e.  ( 0..^ M )  |  ( x  gcd  M )  =  N }
 )  =  if ( N  ||  M ,  ( phi `  ( M  /  N ) ) ,  0 ) )
 
Theoremphisum 12119* The divisor sum identity of the totient function. Theorem 2.2 in [ApostolNT] p. 26. (Contributed by Stefan O'Rear, 12-Sep-2015.)
 |-  ( N  e.  NN  -> 
 sum_ d  e.  { x  e.  NN  |  x  ||  N }  ( phi `  d )  =  N )
 
Theoremodzval 12120* Value of the order function. This is a function of functions; the inner argument selects the base (i.e., mod  N for some  N, often prime) and the outer argument selects the integer or equivalence class (if you want to think about it that way) from the integers mod  N. In order to ensure the supremum is well-defined, we only define the expression when  A and  N are coprime. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by AV, 26-Sep-2020.)
 |-  ( ( N  e.  NN  /\  A  e.  ZZ  /\  ( A  gcd  N )  =  1 )  ->  ( ( odZ `  N ) `  A )  = inf ( { n  e.  NN  |  N  ||  ( ( A ^ n )  -  1
 ) } ,  RR ,  <  ) )
 
Theoremodzcllem 12121 - Lemma for odzcl 12122, showing existence of a recurrent point for the exponential. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 26-Sep-2020.)
 |-  ( ( N  e.  NN  /\  A  e.  ZZ  /\  ( A  gcd  N )  =  1 )  ->  ( ( ( odZ `  N ) `  A )  e.  NN  /\  N  ||  ( ( A ^ ( ( odZ `  N ) `  A ) )  -  1 ) ) )
 
Theoremodzcl 12122 The order of a group element is an integer. (Contributed by Mario Carneiro, 28-Feb-2014.)
 |-  ( ( N  e.  NN  /\  A  e.  ZZ  /\  ( A  gcd  N )  =  1 )  ->  ( ( odZ `  N ) `  A )  e.  NN )
 
Theoremodzid 12123 Any element raised to the power of its order is  1. (Contributed by Mario Carneiro, 28-Feb-2014.)
 |-  ( ( N  e.  NN  /\  A  e.  ZZ  /\  ( A  gcd  N )  =  1 )  ->  N  ||  ( ( A ^ ( ( odZ `  N ) `  A ) )  -  1 ) )
 
Theoremodzdvds 12124 The only powers of  A that are congruent to  1 are the multiples of the order of  A. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 26-Sep-2020.)
 |-  ( ( ( N  e.  NN  /\  A  e.  ZZ  /\  ( A 
 gcd  N )  =  1 )  /\  K  e.  NN0 )  ->  ( N  ||  ( ( A ^ K )  -  1
 ) 
 <->  ( ( odZ `  N ) `  A )  ||  K ) )
 
Theoremodzphi 12125 The order of any group element is a divisor of the Euler  phi function. (Contributed by Mario Carneiro, 28-Feb-2014.)
 |-  ( ( N  e.  NN  /\  A  e.  ZZ  /\  ( A  gcd  N )  =  1 )  ->  ( ( odZ `  N ) `  A )  ||  ( phi `  N ) )
 
5.2.6  Arithmetic modulo a prime number
 
Theoremmodprm1div 12126 A prime number divides an integer minus 1 iff the integer modulo the prime number is 1. (Contributed by Alexander van der Vekens, 17-May-2018.) (Proof shortened by AV, 30-May-2023.)
 |-  ( ( P  e.  Prime  /\  A  e.  ZZ )  ->  ( ( A 
 mod  P )  =  1  <->  P  ||  ( A  -  1 ) ) )
 
Theoremm1dvdsndvds 12127 If an integer minus 1 is divisible by a prime number, the integer itself is not divisible by this prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
 |-  ( ( P  e.  Prime  /\  A  e.  ZZ )  ->  ( P  ||  ( A  -  1
 )  ->  -.  P  ||  A ) )
 
Theoremmodprminv 12128 Show an explicit expression for the modular inverse of  A  mod  P. This is an application of prmdiv 12114. (Contributed by Alexander van der Vekens, 15-May-2018.)
 |-  R  =  ( ( A ^ ( P  -  2 ) ) 
 mod  P )   =>    |-  ( ( P  e.  Prime  /\  A  e.  ZZ  /\ 
 -.  P  ||  A )  ->  ( R  e.  ( 1 ... ( P  -  1 ) ) 
 /\  ( ( A  x.  R )  mod  P )  =  1 ) )
 
Theoremmodprminveq 12129 The modular inverse of  A  mod  P is unique. (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  R  =  ( ( A ^ ( P  -  2 ) ) 
 mod  P )   =>    |-  ( ( P  e.  Prime  /\  A  e.  ZZ  /\ 
 -.  P  ||  A )  ->  ( ( S  e.  ( 0 ... ( P  -  1
 ) )  /\  (
 ( A  x.  S )  mod  P )  =  1 )  <->  S  =  R ) )
 
Theoremvfermltl 12130 Variant of Fermat's little theorem if  A is not a multiple of  P, see theorem 5.18 in [ApostolNT] p. 113. (Contributed by AV, 21-Aug-2020.) (Proof shortened by AV, 5-Sep-2020.)
 |-  ( ( P  e.  Prime  /\  A  e.  ZZ  /\ 
 -.  P  ||  A )  ->  ( ( A ^ ( P  -  1 ) )  mod  P )  =  1 )
 
Theorempowm2modprm 12131 If an integer minus 1 is divisible by a prime number, then the integer to the power of the prime number minus 2 is 1 modulo the prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
 |-  ( ( P  e.  Prime  /\  A  e.  ZZ )  ->  ( P  ||  ( A  -  1
 )  ->  ( ( A ^ ( P  -  2 ) )  mod  P )  =  1 ) )
 
Theoremreumodprminv 12132* For any prime number and for any positive integer less than this prime number, there is a unique modular inverse of this positive integer. (Contributed by Alexander van der Vekens, 12-May-2018.)
 |-  ( ( P  e.  Prime  /\  N  e.  (
 1..^ P ) ) 
 ->  E! i  e.  (
 1 ... ( P  -  1 ) ) ( ( N  x.  i
 )  mod  P )  =  1 )
 
Theoremmodprm0 12133* For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  ( ( P  e.  Prime  /\  N  e.  (
 1..^ P )  /\  I  e.  ( 1..^ P ) )  ->  E. j  e.  (
 0..^ P ) ( ( I  +  (
 j  x.  N ) )  mod  P )  =  0 )
 
Theoremnnnn0modprm0 12134* For a positive integer and a nonnegative integer both less than a given prime number there is always a second nonnegative integer (less than the given prime number) so that the sum of this second nonnegative integer multiplied with the positive integer and the first nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 8-Nov-2018.)
 |-  ( ( P  e.  Prime  /\  N  e.  (
 1..^ P )  /\  I  e.  ( 0..^ P ) )  ->  E. j  e.  (
 0..^ P ) ( ( I  +  (
 j  x.  N ) )  mod  P )  =  0 )
 
Theoremmodprmn0modprm0 12135* For an integer not being 0 modulo a given prime number and a nonnegative integer less than the prime number, there is always a second nonnegative integer (less than the given prime number) so that the sum of this second nonnegative integer multiplied with the integer and the first nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 10-Nov-2018.)
 |-  ( ( P  e.  Prime  /\  N  e.  ZZ  /\  ( N  mod  P )  =/=  0 )  ->  ( I  e.  (
 0..^ P )  ->  E. j  e.  (
 0..^ P ) ( ( I  +  (
 j  x.  N ) )  mod  P )  =  0 ) )
 
5.2.7  Pythagorean Triples
 
Theoremcoprimeprodsq 12136 If three numbers are coprime, and the square of one is the product of the other two, then there is a formula for the other two in terms of  gcd and square. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  NN0  /\  B  e.  ZZ  /\  C  e.  NN0 )  /\  ( ( A 
 gcd  B )  gcd  C )  =  1 )  ->  ( ( C ^
 2 )  =  ( A  x.  B ) 
 ->  A  =  ( ( A  gcd  C ) ^ 2 ) ) )
 
Theoremcoprimeprodsq2 12137 If three numbers are coprime, and the square of one is the product of the other two, then there is a formula for the other two in terms of  gcd and square. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  ZZ  /\  B  e.  NN0  /\  C  e.  NN0 )  /\  ( ( A  gcd  B ) 
 gcd  C )  =  1 )  ->  ( ( C ^ 2 )  =  ( A  x.  B )  ->  B  =  ( ( B  gcd  C ) ^ 2 ) ) )
 
Theoremoddprm 12138 A prime not equal to  2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 10-Jul-2022.)
 |-  ( N  e.  ( Prime  \  { 2 } )  ->  ( ( N  -  1 )  / 
 2 )  e.  NN )
 
Theoremnnoddn2prm 12139 A prime not equal to  2 is an odd positive integer. (Contributed by AV, 28-Jun-2021.)
 |-  ( N  e.  ( Prime  \  { 2 } )  ->  ( N  e.  NN  /\  -.  2  ||  N ) )
 
Theoremoddn2prm 12140 A prime not equal to  2 is odd. (Contributed by AV, 28-Jun-2021.)
 |-  ( N  e.  ( Prime  \  { 2 } )  ->  -.  2  ||  N )
 
Theoremnnoddn2prmb 12141 A number is a prime number not equal to  2 iff it is an odd prime number. Conversion theorem for two representations of odd primes. (Contributed by AV, 14-Jul-2021.)
 |-  ( N  e.  ( Prime  \  { 2 } )  <->  ( N  e.  Prime  /\  -.  2  ||  N ) )
 
Theoremprm23lt5 12142 A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021.)
 |-  ( ( P  e.  Prime  /\  P  <  5
 )  ->  ( P  =  2  \/  P  =  3 ) )
 
Theoremprm23ge5 12143 A prime is either 2 or 3 or greater than or equal to 5. (Contributed by AV, 5-Jul-2021.)
 |-  ( P  e.  Prime  ->  ( P  =  2  \/  P  =  3  \/  P  e.  ( ZZ>= `  5 ) ) )
 
Theorempythagtriplem1 12144* Lemma for pythagtrip 12162. Prove a weaker version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( E. n  e. 
 NN  E. m  e.  NN  E. k  e.  NN  ( A  =  ( k  x.  ( ( m ^
 2 )  -  ( n ^ 2 ) ) )  /\  B  =  ( k  x.  (
 2  x.  ( m  x.  n ) ) )  /\  C  =  ( k  x.  (
 ( m ^ 2
 )  +  ( n ^ 2 ) ) ) )  ->  (
 ( A ^ 2
 )  +  ( B ^ 2 ) )  =  ( C ^
 2 ) )
 
Theorempythagtriplem2 12145* Lemma for pythagtrip 12162. Prove the full version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( A  e.  NN  /\  B  e.  NN )  ->  ( E. n  e.  NN  E. m  e. 
 NN  E. k  e.  NN  ( { A ,  B }  =  { (
 k  x.  ( ( m ^ 2 )  -  ( n ^
 2 ) ) ) ,  ( k  x.  ( 2  x.  ( m  x.  n ) ) ) }  /\  C  =  ( k  x.  (
 ( m ^ 2
 )  +  ( n ^ 2 ) ) ) )  ->  (
 ( A ^ 2
 )  +  ( B ^ 2 ) )  =  ( C ^
 2 ) ) )
 
Theorempythagtriplem3 12146 Lemma for pythagtrip 12162. Show that  C and 
B are relatively prime under some conditions. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  ( B  gcd  C )  =  1 )
 
Theorempythagtriplem4 12147 Lemma for pythagtrip 12162. Show that  C  -  B and  C  +  B are relatively prime. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  ( ( C  -  B )  gcd  ( C  +  B ) )  =  1 )
 
Theorempythagtriplem10 12148 Lemma for pythagtrip 12162. Show that  C  -  B is positive. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 ) )  ->  0  <  ( C  -  B ) )
 
Theorempythagtriplem6 12149 Lemma for pythagtrip 12162. Calculate  ( sqr `  ( C  -  B ) ). (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  ( sqr `  ( C  -  B ) )  =  ( ( C  -  B )  gcd  A ) )
 
Theorempythagtriplem7 12150 Lemma for pythagtrip 12162. Calculate  ( sqr `  ( C  +  B ) ). (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  ( sqr `  ( C  +  B ) )  =  ( ( C  +  B )  gcd  A ) )
 
Theorempythagtriplem8 12151 Lemma for pythagtrip 12162. Show that  ( sqr `  ( C  -  B ) ) is a positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  ( sqr `  ( C  -  B ) )  e. 
 NN )
 
Theorempythagtriplem9 12152 Lemma for pythagtrip 12162. Show that  ( sqr `  ( C  +  B ) ) is a positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  ( sqr `  ( C  +  B ) )  e. 
 NN )
 
Theorempythagtriplem11 12153 Lemma for pythagtrip 12162. Show that  M (which will eventually be closely related to the  m in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  M  =  ( ( ( sqr `  ( C  +  B )
 )  +  ( sqr `  ( C  -  B ) ) )  / 
 2 )   =>    |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  M  e.  NN )
 
Theorempythagtriplem12 12154 Lemma for pythagtrip 12162. Calculate the square of  M. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  M  =  ( ( ( sqr `  ( C  +  B )
 )  +  ( sqr `  ( C  -  B ) ) )  / 
 2 )   =>    |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  ( M ^ 2 )  =  ( ( C  +  A )  / 
 2 ) )
 
Theorempythagtriplem13 12155 Lemma for pythagtrip 12162. Show that  N (which will eventually be closely related to the  n in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  N  =  ( ( ( sqr `  ( C  +  B )
 )  -  ( sqr `  ( C  -  B ) ) )  / 
 2 )   =>    |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  N  e.  NN )
 
Theorempythagtriplem14 12156 Lemma for pythagtrip 12162. Calculate the square of  N. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  N  =  ( ( ( sqr `  ( C  +  B )
 )  -  ( sqr `  ( C  -  B ) ) )  / 
 2 )   =>    |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  ( N ^ 2 )  =  ( ( C  -  A )  / 
 2 ) )
 
Theorempythagtriplem15 12157 Lemma for pythagtrip 12162. Show the relationship between  M,  N, and  A. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  M  =  ( ( ( sqr `  ( C  +  B )
 )  +  ( sqr `  ( C  -  B ) ) )  / 
 2 )   &    |-  N  =  ( ( ( sqr `  ( C  +  B )
 )  -  ( sqr `  ( C  -  B ) ) )  / 
 2 )   =>    |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  A  =  ( ( M ^ 2 )  -  ( N ^ 2 ) ) )
 
Theorempythagtriplem16 12158 Lemma for pythagtrip 12162. Show the relationship between  M,  N, and  B. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  M  =  ( ( ( sqr `  ( C  +  B )
 )  +  ( sqr `  ( C  -  B ) ) )  / 
 2 )   &    |-  N  =  ( ( ( sqr `  ( C  +  B )
 )  -  ( sqr `  ( C  -  B ) ) )  / 
 2 )   =>    |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  B  =  ( 2  x.  ( M  x.  N ) ) )
 
Theorempythagtriplem17 12159 Lemma for pythagtrip 12162. Show the relationship between  M,  N, and  C. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  M  =  ( ( ( sqr `  ( C  +  B )
 )  +  ( sqr `  ( C  -  B ) ) )  / 
 2 )   &    |-  N  =  ( ( ( sqr `  ( C  +  B )
 )  -  ( sqr `  ( C  -  B ) ) )  / 
 2 )   =>    |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  C  =  ( ( M ^ 2 )  +  ( N ^ 2 ) ) )
 
Theorempythagtriplem18 12160* Lemma for pythagtrip 12162. Wrap the previous  M and  N up in quantifiers. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  ( ( A  gcd  B )  =  1  /\  -.  2  ||  A ) )  ->  E. n  e.  NN  E. m  e.  NN  ( A  =  ( ( m ^ 2 )  -  ( n ^ 2 ) )  /\  B  =  ( 2  x.  ( m  x.  n ) ) 
 /\  C  =  ( ( m ^ 2
 )  +  ( n ^ 2 ) ) ) )
 
Theorempythagtriplem19 12161* Lemma for pythagtrip 12162. Introduce  k and remove the relative primality requirement. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 |-  ( ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  /\  ( ( A ^ 2 )  +  ( B ^
 2 ) )  =  ( C ^ 2
 )  /\  -.  2  ||  ( A  /  ( A  gcd  B ) ) )  ->  E. n  e.  NN  E. m  e. 
 NN  E. k  e.  NN  ( A  =  (
 k  x.  ( ( m ^ 2 )  -  ( n ^
 2 ) ) ) 
 /\  B  =  ( k  x.  ( 2  x.  ( m  x.  n ) ) ) 
 /\  C  =  ( k  x.  ( ( m ^ 2 )  +  ( n ^
 2 ) ) ) ) )
 
Theorempythagtrip 12162* Parameterize the Pythagorean triples. If  A,  B, and  C are naturals, then they obey the Pythagorean triple formula iff they are parameterized by three naturals. This proof follows the Isabelle proof at http://afp.sourceforge.net/entries/Fermat3_4.shtml. This is Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014.)
 |-  ( ( A  e.  NN  /\  B  e.  NN  /\  C  e.  NN )  ->  ( ( ( A ^ 2 )  +  ( B ^ 2 ) )  =  ( C ^ 2 )  <->  E. n  e.  NN  E. m  e.  NN  E. k  e.  NN  ( { A ,  B }  =  { ( k  x.  ( ( m ^
 2 )  -  ( n ^ 2 ) ) ) ,  ( k  x.  ( 2  x.  ( m  x.  n ) ) ) }  /\  C  =  ( k  x.  ( ( m ^ 2 )  +  ( n ^ 2 ) ) ) ) ) )
 
5.3  Cardinality of real and complex number subsets
 
5.3.1  Countability of integers and rationals
 
Theoremoddennn 12163 There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.)
 |- 
 { z  e.  NN  |  -.  2  ||  z }  ~~  NN
 
Theoremevenennn 12164 There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.)
 |- 
 { z  e.  NN  |  2  ||  z }  ~~  NN
 
Theoremxpnnen 12165 The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.)
 |-  ( NN  X.  NN )  ~~  NN
 
Theoremxpomen 12166 The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.)
 |-  ( om  X.  om )  ~~  om
 
Theoremxpct 12167 The cartesian product of two sets dominated by  om is dominated by  om. (Contributed by Thierry Arnoux, 24-Sep-2017.)
 |-  ( ( A  ~<_  om  /\  B 
 ~<_  om )  ->  ( A  X.  B )  ~<_  om )
 
Theoremunennn 12168 The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.)
 |-  ( ( A  ~~  NN  /\  B  ~~  NN  /\  ( A  i^i  B )  =  (/) )  ->  ( A  u.  B )  ~~  NN )
 
Theoremznnen 12169 The set of integers and the set of positive integers are equinumerous. Corollary 8.1.23 of [AczelRathjen], p. 75. (Contributed by NM, 31-Jul-2004.)
 |- 
 ZZ  ~~  NN
 
Theoremennnfonelemdc 12170* Lemma for ennnfone 12196. A direct consequence of fidcenumlemrk 6899. (Contributed by Jim Kingdon, 15-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  P  e.  om )   =>    |-  ( ph  -> DECID  ( F `
  P )  e.  ( F " P ) )
 
Theoremennnfonelemk 12171* Lemma for ennnfone 12196. (Contributed by Jim Kingdon, 15-Jul-2023.)
 |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  K  e.  om )   &    |-  ( ph  ->  N  e.  om )   &    |-  ( ph  ->  A. j  e.  suc  N ( F `
  K )  =/=  ( F `  j
 ) )   =>    |-  ( ph  ->  N  e.  K )
 
Theoremennnfonelemj0 12172* Lemma for ennnfone 12196. Initial state for  J. (Contributed by Jim Kingdon, 20-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   =>    |-  ( ph  ->  ( J `  0 )  e. 
 { g  e.  ( A  ^pm  om )  | 
 dom  g  e.  om } )
 
Theoremennnfonelemjn 12173* Lemma for ennnfone 12196. Non-initial state for  J. (Contributed by Jim Kingdon, 20-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   =>    |-  ( ( ph  /\  f  e.  ( ZZ>= `  ( 0  +  1 ) ) )  ->  ( J `  f )  e.  om )
 
Theoremennnfonelemg 12174* Lemma for ennnfone 12196. Closure for  G. (Contributed by Jim Kingdon, 20-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   =>    |-  ( ( ph  /\  (
 f  e.  { g  e.  ( A  ^pm  om )  |  dom  g  e.  om } 
 /\  j  e.  om ) )  ->  ( f G j )  e. 
 { g  e.  ( A  ^pm  om )  | 
 dom  g  e.  om } )
 
Theoremennnfonelemh 12175* Lemma for ennnfone 12196. (Contributed by Jim Kingdon, 8-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   =>    |-  ( ph  ->  H : NN0 --> ( A  ^pm  om ) )
 
Theoremennnfonelem0 12176* Lemma for ennnfone 12196. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   =>    |-  ( ph  ->  ( H `  0 )  =  (/) )
 
Theoremennnfonelemp1 12177* Lemma for ennnfone 12196. Value of  H at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  ( ph  ->  P  e.  NN0 )   =>    |-  ( ph  ->  ( H `  ( P  +  1 ) )  =  if ( ( F `
  ( `' N `  P ) )  e.  ( F " ( `' N `  P ) ) ,  ( H `
  P ) ,  ( ( H `  P )  u.  { <. dom  ( H `  P ) ,  ( F `  ( `' N `  P ) ) >. } ) ) )
 
Theoremennnfonelem1 12178* Lemma for ennnfone 12196. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   =>    |-  ( ph  ->  ( H `  1 )  =  { <. (/) ,  ( F `
  (/) ) >. } )
 
Theoremennnfonelemom 12179* Lemma for ennnfone 12196. 
H yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  ( ph  ->  P  e.  NN0 )   =>    |-  ( ph  ->  dom  ( H `  P )  e. 
 om )
 
Theoremennnfonelemhdmp1 12180* Lemma for ennnfone 12196. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  ( ph  ->  P  e.  NN0 )   &    |-  ( ph  ->  -.  ( F `  ( `' N `  P ) )  e.  ( F
 " ( `' N `  P ) ) )   =>    |-  ( ph  ->  dom  ( H `
  ( P  +  1 ) )  = 
 suc  dom  ( H `  P ) )
 
Theoremennnfonelemss 12181* Lemma for ennnfone 12196. We only add elements to  H as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  ( ph  ->  P  e.  NN0 )   =>    |-  ( ph  ->  ( H `  P )  C_  ( H `  ( P  +  1 ) ) )
 
Theoremennnfoneleminc 12182* Lemma for ennnfone 12196. We only add elements to  H as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  ( ph  ->  P  e.  NN0 )   &    |-  ( ph  ->  Q  e.  NN0 )   &    |-  ( ph  ->  P 
 <_  Q )   =>    |-  ( ph  ->  ( H `  P )  C_  ( H `  Q ) )
 
Theoremennnfonelemkh 12183* Lemma for ennnfone 12196. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  ( ph  ->  P  e.  NN0 )   =>    |-  ( ph  ->  dom  ( H `  P )  C_  ( `' N `  P ) )
 
Theoremennnfonelemhf1o 12184* Lemma for ennnfone 12196. Each of the functions in  H is one to one and onto an image of  F. (Contributed by Jim Kingdon, 17-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  ( ph  ->  P  e.  NN0 )   =>    |-  ( ph  ->  ( H `  P ) : dom  ( H `  P ) -1-1-onto-> ( F " ( `' N `  P ) ) )
 
Theoremennnfonelemex 12185* Lemma for ennnfone 12196. Extending the sequence  ( H `  P ) to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  ( ph  ->  P  e.  NN0 )   =>    |-  ( ph  ->  E. i  e.  NN0  dom  ( H `  P )  e.  dom  ( H `  i ) )
 
Theoremennnfonelemhom 12186* Lemma for ennnfone 12196. The sequences in  H increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  ( ph  ->  M  e.  om )   =>    |-  ( ph  ->  E. i  e.  NN0  M  e.  dom  ( H `  i ) )
 
Theoremennnfonelemrnh 12187* Lemma for ennnfone 12196. A consequence of ennnfonelemss 12181. (Contributed by Jim Kingdon, 16-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  ( ph  ->  X  e.  ran  H )   &    |-  ( ph  ->  Y  e.  ran  H )   =>    |-  ( ph  ->  ( X  C_  Y  \/  Y  C_  X ) )
 
Theoremennnfonelemfun 12188* Lemma for ennnfone 12196. 
L is a function. (Contributed by Jim Kingdon, 16-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  L  =  U_ i  e.  NN0  ( H `  i )   =>    |-  ( ph  ->  Fun  L )
 
Theoremennnfonelemf1 12189* Lemma for ennnfone 12196. 
L is one-to-one. (Contributed by Jim Kingdon, 16-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  L  =  U_ i  e.  NN0  ( H `  i )   =>    |-  ( ph  ->  L : dom  L -1-1-> A )
 
Theoremennnfonelemrn 12190* Lemma for ennnfone 12196. 
L is onto  A. (Contributed by Jim Kingdon, 16-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  L  =  U_ i  e.  NN0  ( H `  i )   =>    |-  ( ph  ->  ran  L  =  A )
 
Theoremennnfonelemdm 12191* Lemma for ennnfone 12196. The function  L is defined everywhere. (Contributed by Jim Kingdon, 16-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  L  =  U_ i  e.  NN0  ( H `  i )   =>    |-  ( ph  ->  dom  L  =  om )
 
Theoremennnfonelemen 12192* Lemma for ennnfone 12196. The result. (Contributed by Jim Kingdon, 16-Jul-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `
  k )  =/=  ( F `  j
 ) )   &    |-  G  =  ( x  e.  ( A 
 ^pm  om ) ,  y  e.  om  |->  if ( ( F `
  y )  e.  ( F " y
 ) ,  x ,  ( x  u.  { <. dom 
 x ,  ( F `
  y ) >. } ) ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/)
 ,  ( `' N `  ( x  -  1
 ) ) ) )   &    |-  H  =  seq 0
 ( G ,  J )   &    |-  L  =  U_ i  e.  NN0  ( H `  i )   =>    |-  ( ph  ->  A  ~~ 
 NN )
 
Theoremennnfonelemnn0 12193* Lemma for ennnfone 12196. A version of ennnfonelemen 12192 expressed in terms of  NN0 instead of  om. (Contributed by Jim Kingdon, 27-Oct-2022.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : NN0
 -onto-> A )   &    |-  ( ph  ->  A. n  e.  NN0  E. k  e.  NN0  A. j  e.  (
 0 ... n ) ( F `  k )  =/=  ( F `  j ) )   &    |-  N  = frec ( ( x  e. 
 ZZ  |->  ( x  +  1 ) ) ,  0 )   =>    |-  ( ph  ->  A  ~~ 
 NN )
 
Theoremennnfonelemr 12194* Lemma for ennnfone 12196. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  F : NN0
 -onto-> A )   &    |-  ( ph  ->  A. n  e.  NN0  E. k  e.  NN0  A. j  e.  (
 0 ... n ) ( F `  k )  =/=  ( F `  j ) )   =>    |-  ( ph  ->  A 
 ~~  NN )
 
Theoremennnfonelemim 12195* Lemma for ennnfone 12196. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.)
 |-  ( A  ~~  NN  ->  ( A. x  e.  A  A. y  e.  A DECID  x  =  y  /\  E. f ( f :
 NN0 -onto-> A  /\  A. n  e.  NN0  E. k  e. 
 NN0  A. j  e.  (
 0 ... n ) ( f `  k )  =/=  ( f `  j ) ) ) )
 
Theoremennnfone 12196* A condition for a set being countably infinite. Corollary 8.1.13 of [AczelRathjen], p. 73. Roughly speaking, the condition says that 
A is countable (that's the  f : NN0 -onto-> A part, as seen in theorems like ctm 7054), infinite (that's the part about being able to find an element of  A distinct from any mapping of a natural number via  f), and has decidable equality. (Contributed by Jim Kingdon, 27-Oct-2022.)
 |-  ( A  ~~  NN  <->  ( A. x  e.  A  A. y  e.  A DECID  x  =  y  /\  E. f
 ( f : NN0 -onto-> A 
 /\  A. n  e.  NN0  E. k  e.  NN0  A. j  e.  ( 0 ... n ) ( f `  k )  =/=  (
 f `  j )
 ) ) )
 
Theoremexmidunben 12197* If any unbounded set of positive integers is equinumerous to  NN, then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.)
 |-  ( ( A. x ( ( x  C_  NN  /\  A. m  e. 
 NN  E. n  e.  x  m  <  n )  ->  x  ~~  NN )  /\  om  e. Omni )  -> EXMID )
 
Theoremctinfomlemom 12198* Lemma for ctinfom 12199. Converting between  om and  NN0. (Contributed by Jim Kingdon, 10-Aug-2023.)
 |-  N  = frec ( ( x  e.  ZZ  |->  ( x  +  1 ) ) ,  0 )   &    |-  G  =  ( F  o.  `' N )   &    |-  ( ph  ->  F : om -onto-> A )   &    |-  ( ph  ->  A. n  e. 
 om  E. k  e.  om  -.  ( F `  k
 )  e.  ( F
 " n ) )   =>    |-  ( ph  ->  ( G : NN0 -onto-> A  /\  A. m  e.  NN0  E. j  e. 
 NN0  A. i  e.  (
 0 ... m ) ( G `  j )  =/=  ( G `  i ) ) )
 
Theoremctinfom 12199* A condition for a set being countably infinite. Restates ennnfone 12196 in terms of  om and function image. Like ennnfone 12196 the condition can be summarized as  A being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.)
 |-  ( A  ~~  NN  <->  ( A. x  e.  A  A. y  e.  A DECID  x  =  y  /\  E. f
 ( f : om -onto-> A  /\  A. n  e. 
 om  E. k  e.  om  -.  ( f `  k
 )  e.  ( f
 " n ) ) ) )
 
Theoreminffinp1 12200* An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  om  ~<_  A )   &    |-  ( ph  ->  B  C_  A )   &    |-  ( ph  ->  B  e.  Fin )   =>    |-  ( ph  ->  E. x  e.  A  -.  x  e.  B )
    < 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-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13694
  Copyright terms: Public domain < Previous  Next >