P. 151 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	vdwapf 15001	The arithmetic progression function is a function. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( K e. NN0 -> (AP ` K ) : ( NN X. NN ) --> ~P NN )
Theorem	vdwapval 15002*	Value of the arithmetic progression function. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( X e. ( A (AP ` K ) D ) <-> E. m e. ( 0 ... ( K - 1 ) ) X = ( A + ( m x. D ) ) ) )
Theorem	vdwapun 15003	Remove the first element of an arithmetic progression. (Contributed by Mario Carneiro, 11-Sep-2014.)
|- ( ( K e. NN0 /\ A e. NN /\ D e. NN ) -> ( A (AP ` ( K + 1 ) ) D ) = ( { A } u. ( ( A + D ) (AP ` K ) D ) ) )
Theorem	vdwapid1 15004	The first element of an arithmetic progression. (Contributed by Mario Carneiro, 12-Sep-2014.)
|- ( ( K e. NN /\ A e. NN /\ D e. NN ) -> A e. ( A (AP ` K ) D ) )
Theorem	vdwap0 15005	Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ( A e. NN /\ D e. NN ) -> ( A (AP ` 0 ) D ) = (/) )
Theorem	vdwap1 15006	Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ( A e. NN /\ D e. NN ) -> ( A (AP ` 1 ) D ) = { A } )
Theorem	vdwmc 15007*	The predicate " The <. R , N >.-coloring F contains a monochromatic AP of length K". (Contributed by Mario Carneiro, 18-Aug-2014.)
|- X e. _V   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> F : X --> R )   =>    |- ( ph -> ( K MonoAP F <-> E. c E. a e. NN E. d e. NN ( a (AP ` K ) d ) C_ ( `' F " { c } ) ) )
Theorem	vdwmc2 15008*	Expand out the definition of an arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- X e. _V   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> F : X --> R )   &    |- ( ph -> A e. X )   =>    |- ( ph -> ( K MonoAP F <-> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) ) )
Theorem	vdwpc 15009*	The predicate " The coloring F contains a polychromatic M-tuple of AP's of length K". A polychromatic M-tuple of AP's is a set of AP's with the same base point but different step lengths, such that each individual AP is monochromatic, but the AP's all have mutually distinct colors. (The common basepoint is not required to have the same color as any of the AP's.) (Contributed by Mario Carneiro, 18-Aug-2014.)
|- X e. _V   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> F : X --> R )   &    |- ( ph -> M e. NN )   &    |- J = ( 1 ... M )   =>    |- ( ph -> ( <. M , K >. PolyAP F <-> E. a e. NN E. d e. ( NN ^m J ) ( A. i e. J ( ( a + ( d ` i ) ) (AP ` K ) ( d ` i ) ) C_ ( `' F " { ( F ` ( a + ( d ` i ) ) ) } ) /\ ( # ` ran ( i e. J |-> ( F ` ( a + ( d ` i ) ) ) ) ) = M ) ) )
Theorem	vdwlem1 15010*	Lemma for vdw 15023. (Contributed by Mario Carneiro, 12-Sep-2014.)
|- ( ph -> R e. Fin )   &    |- ( ph -> K e. NN )   &    |- ( ph -> W e. NN )   &    |- ( ph -> F : ( 1 ... W ) --> R )   &    |- ( ph -> A e. NN )   &    |- ( ph -> M e. NN )   &    |- ( ph -> D : ( 1 ... M ) --> NN )   &    |- ( ph -> A. i e. ( 1 ... M ) ( ( A + ( D ` i ) ) (AP ` K ) ( D ` i ) ) C_ ( `' F " { ( F ` ( A + ( D ` i ) ) ) } ) )   &    |- ( ph -> I e. ( 1 ... M ) )   &    |- ( ph -> ( F ` A ) = ( F ` ( A + ( D ` I ) ) ) )   =>    |- ( ph -> ( K + 1 ) MonoAP F )
Theorem	vdwlem2 15011*	Lemma for vdw 15023. (Contributed by Mario Carneiro, 12-Sep-2014.)
|- ( ph -> R e. Fin )   &    |- ( ph -> K e. NN0 )   &    |- ( ph -> W e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> F : ( 1 ... M ) --> R )   &    |- ( ph -> M e. ( ZZ>= ` ( W + N ) ) )   &    |- G = ( x e. ( 1 ... W ) |-> ( F ` ( x + N ) ) )   =>    |- ( ph -> ( K MonoAP G -> K MonoAP F ) )
Theorem	vdwlem3 15012	Lemma for vdw 15023. (Contributed by Mario Carneiro, 13-Sep-2014.)
|- ( ph -> V e. NN )   &    |- ( ph -> W e. NN )   &    |- ( ph -> A e. ( 1 ... V ) )   &    |- ( ph -> B e. ( 1 ... W ) )   =>    |- ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) )
Theorem	vdwlem4 15013*	Lemma for vdw 15023. (Contributed by Mario Carneiro, 12-Sep-2014.)
|- ( ph -> V e. NN )   &    |- ( ph -> W e. NN )   &    |- ( ph -> R e. Fin )   &    |- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )   &    |- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )   =>    |- ( ph -> F : ( 1 ... V ) --> ( R ^m ( 1 ... W ) ) )
Theorem	vdwlem5 15014*	Lemma for vdw 15023. (Contributed by Mario Carneiro, 12-Sep-2014.)
|- ( ph -> V e. NN )   &    |- ( ph -> W e. NN )   &    |- ( ph -> R e. Fin )   &    |- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )   &    |- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> G : ( 1 ... W ) --> R )   &    |- ( ph -> K e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. NN )   &    |- ( ph -> D e. NN )   &    |- ( ph -> ( A (AP ` K ) D ) C_ ( `' F " { G } ) )   &    |- ( ph -> B e. NN )   &    |- ( ph -> E : ( 1 ... M ) --> NN )   &    |- ( ph -> A. i e. ( 1 ... M ) ( ( B + ( E ` i ) ) (AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )   &    |- J = ( i e. ( 1 ... M ) |-> ( G ` ( B + ( E ` i ) ) ) )   &    |- ( ph -> ( # ` ran J ) = M )   &    |- T = ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) )   &    |- P = ( j e. ( 1 ... ( M + 1 ) ) |-> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) )   =>    |- ( ph -> T e. NN )
Theorem	vdwlem6 15015*	Lemma for vdw 15023. (Contributed by Mario Carneiro, 13-Sep-2014.)
|- ( ph -> V e. NN )   &    |- ( ph -> W e. NN )   &    |- ( ph -> R e. Fin )   &    |- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )   &    |- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> G : ( 1 ... W ) --> R )   &    |- ( ph -> K e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. NN )   &    |- ( ph -> D e. NN )   &    |- ( ph -> ( A (AP ` K ) D ) C_ ( `' F " { G } ) )   &    |- ( ph -> B e. NN )   &    |- ( ph -> E : ( 1 ... M ) --> NN )   &    |- ( ph -> A. i e. ( 1 ... M ) ( ( B + ( E ` i ) ) (AP ` K ) ( E ` i ) ) C_ ( `' G " { ( G ` ( B + ( E ` i ) ) ) } ) )   &    |- J = ( i e. ( 1 ... M ) |-> ( G ` ( B + ( E ` i ) ) ) )   &    |- ( ph -> ( # ` ran J ) = M )   &    |- T = ( B + ( W x. ( ( A + ( V - D ) ) - 1 ) ) )   &    |- P = ( j e. ( 1 ... ( M + 1 ) ) |-> ( if ( j = ( M + 1 ) , 0 , ( E ` j ) ) + ( W x. D ) ) )   =>    |- ( ph -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) )
Theorem	vdwlem7 15016*	Lemma for vdw 15023. (Contributed by Mario Carneiro, 12-Sep-2014.)
|- ( ph -> V e. NN )   &    |- ( ph -> W e. NN )   &    |- ( ph -> R e. Fin )   &    |- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )   &    |- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> G : ( 1 ... W ) --> R )   &    |- ( ph -> K e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. NN )   &    |- ( ph -> D e. NN )   &    |- ( ph -> ( A (AP ` K ) D ) C_ ( `' F " { G } ) )   =>    |- ( ph -> ( <. M , K >. PolyAP G -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP G ) ) )
Theorem	vdwlem8 15017*	Lemma for vdw 15023. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ph -> R e. Fin )   &    |- ( ph -> K e. ( ZZ>= ` 2 ) )   &    |- ( ph -> W e. NN )   &    |- ( ph -> F : ( 1 ... ( 2 x. W ) ) --> R )   &    |- C e. _V   &    |- ( ph -> A e. NN )   &    |- ( ph -> D e. NN )   &    |- ( ph -> ( A (AP ` K ) D ) C_ ( `' G " { C } ) )   &    |- G = ( x e. ( 1 ... W ) |-> ( F ` ( x + W ) ) )   =>    |- ( ph -> <. 1 , K >. PolyAP F )
Theorem	vdwlem9 15018*	Lemma for vdw 15023. (Contributed by Mario Carneiro, 12-Sep-2014.)
|- ( ph -> R e. Fin )   &    |- ( ph -> K e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f )   &    |- ( ph -> M e. NN )   &    |- ( ph -> W e. NN )   &    |- ( ph -> A. g e. ( R ^m ( 1 ... W ) ) ( <. M , K >. PolyAP g \/ ( K + 1 ) MonoAP g ) )   &    |- ( ph -> V e. NN )   &    |- ( ph -> A. f e. ( ( R ^m ( 1 ... W ) ) ^m ( 1 ... V ) ) K MonoAP f )   &    |- ( ph -> H : ( 1 ... ( W x. ( 2 x. V ) ) ) --> R )   &    |- F = ( x e. ( 1 ... V ) |-> ( y e. ( 1 ... W ) |-> ( H ` ( y + ( W x. ( ( x - 1 ) + V ) ) ) ) ) )   =>    |- ( ph -> ( <. ( M + 1 ) , K >. PolyAP H \/ ( K + 1 ) MonoAP H ) )
Theorem	vdwlem10 15019*	Lemma for vdw 15023. Set up secondary induction on M. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ph -> R e. Fin )   &    |- ( ph -> K e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f )   &    |- ( ph -> M e. NN )   =>    |- ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( <. M , K >. PolyAP f \/ ( K + 1 ) MonoAP f ) )
Theorem	vdwlem11 15020*	Lemma for vdw 15023. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ph -> R e. Fin )   &    |- ( ph -> K e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A. s e. Fin E. n e. NN A. f e. ( s ^m ( 1 ... n ) ) K MonoAP f )   =>    |- ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) ( K + 1 ) MonoAP f )
Theorem	vdwlem12 15021	Lemma for vdw 15023. K = 2 base case of induction. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ph -> R e. Fin )   &    |- ( ph -> F : ( 1 ... ( ( # ` R ) + 1 ) ) --> R )   &    |- ( ph -> -. 2 MonoAP F )   =>    |- -. ph
Theorem	vdwlem13 15022*	Lemma for vdw 15023. Main induction on K; K = 0, K = 1 base cases. (Contributed by Mario Carneiro, 18-Aug-2014.)
|- ( ph -> R e. Fin )   &    |- ( ph -> K e. NN0 )   =>    |- ( ph -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) K MonoAP f )
Theorem	vdw 15023*	Van der Waerden's theorem. For any finite coloring R and integer K, there is an N such that every coloring function from 1 ... N to R contains a monochromatic arithmetic progression (which written out in full means that there is a color c and base, increment values a , d such that all the numbers a , a + d , ... , a + ( k - 1 ) d lie in the preimage of { c }, i.e. they are all in 1 ... N and f evaluated at each one yields c). (Contributed by Mario Carneiro, 13-Sep-2014.)
|- ( ( R e. Fin /\ K e. NN0 ) -> E. n e. NN A. f e. ( R ^m ( 1 ... n ) ) E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' f " { c } ) )
Theorem	vdwnnlem1 15024*	Corollary of vdw 15023, and lemma for vdwnn 15027. If F is a coloring of the integers, then there are arbitrarily long monochromatic APs in F. (Contributed by Mario Carneiro, 13-Sep-2014.)
|- ( ( R e. Fin /\ F : NN --> R /\ K e. NN0 ) -> E. c e. R E. a e. NN E. d e. NN A. m e. ( 0 ... ( K - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
Theorem	vdwnnlem2 15025*	Lemma for vdwnn 15027. The set of all "bad" k for the theorem is upwards-closed, because a long AP implies a short AP. (Contributed by Mario Carneiro, 13-Sep-2014.)
|- ( ph -> R e. Fin )   &    |- ( ph -> F : NN --> R )   &    |- S = { k e. NN | -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) }   =>    |- ( ( ph /\ B e. ( ZZ>= ` A ) ) -> ( A e. S -> B e. S ) )
Theorem	vdwnnlem3 15026*	Lemma for vdwnn 15027. (Contributed by Mario Carneiro, 13-Sep-2014.) (Proof shortened by AV, 27-Sep-2020.)
|- ( ph -> R e. Fin )   &    |- ( ph -> F : NN --> R )   &    |- S = { k e. NN | -. E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) }   &    |- ( ph -> A. c e. R S =/= (/) )   =>    |- -. ph
Theorem	vdwnn 15027*	Van der Waerden's theorem, infinitary version. For any finite coloring F of the positive integers, there is a color c that contains arbitrarily long arithmetic progressions. (Contributed by Mario Carneiro, 13-Sep-2014.)
|- ( ( R e. Fin /\ F : NN --> R ) -> E. c e. R A. k e. NN E. a e. NN E. d e. NN A. m e. ( 0 ... ( k - 1 ) ) ( a + ( m x. d ) ) e. ( `' F " { c } ) )
6.2.14  Ramsey's theorem
Syntax	cram 15028	Extend class notation with the Ramsey number function.
class Ramsey
Syntax	cramold 15029	Extend class notation with the Ramsey number function (old version).
class Ramsey
Theorem	ramtlecl 15030*	The set T of numbers with the Ramsey number property is upward-closed. (Contributed by Mario Carneiro, 21-Apr-2015.)
|- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> ph ) }   =>    |- ( M e. T -> ( ZZ>= ` M ) C_ T )
Definition	df-ram 15031*	Define the Ramsey number function. The input is a number m for the size of the edges of the hypergraph, and a tuple r from the finite color set to lower bounds for each color. The Ramsey number ( M Ramsey R ) is the smallest number such that for any set S with ( M Ramsey R ) <_ # S and any coloring F of the set of M-element subsets of S (with color set dom R), there is a color c e. dom R and a subset x C_ S such that R ( c ) <_ # x and all the hyperedges of x (that is, subsets of x of size M) have color c. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
|- Ramsey = ( m e. NN0 , r e. _V |-> inf ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } , RR* , < ) )
Definition	df-ramOLD 15032*	Define the Ramsey number function. The input is a number m for the size of the edges of the hypergraph, and a tuple r from the finite color set to lower bounds for each color. The Ramsey number ( M Ramsey R ) is the smallest number such that for any set S with ( M Ramsey R ) <_ # S and any coloring F of the set of M-element subsets of S (with color set dom R), there is a color c e. dom R and a subset x C_ S such that R ( c ) <_ # x and all the hyperedges of x (that is, subsets of x of size M) have color c. (Contributed by Mario Carneiro, 20-Apr-2015.) Obsolete version of df-ram 15031 as of 14-Sep-2020. (New usage is discouraged.)
|- Ramsey = ( m e. NN0 , r e. _V |-> sup ( { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( dom r ^m { y e. ~P s | ( # ` y ) = m } ) E. c e. dom r E. x e. ~P s ( ( r ` c ) <_ ( # ` x ) /\ A. y e. ~P x ( ( # ` y ) = m -> ( f ` y ) = c ) ) ) } , RR* , `' < ) )
Theorem	hashbcval 15033*	Value of the "binomial set", the set of all N-element subsets of A. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   =>    |- ( ( A e. V /\ N e. NN0 ) -> ( A C N ) = { x e. ~P A | ( # ` x ) = N } )
Theorem	hashbccl 15034*	The binomial set is a finite set. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   =>    |- ( ( A e. Fin /\ N e. NN0 ) -> ( A C N ) e. Fin )
Theorem	hashbcss 15035*	Subset relation for the binomial set. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   =>    |- ( ( A e. V /\ B C_ A /\ N e. NN0 ) -> ( B C N ) C_ ( A C N ) )
Theorem	hashbc0 15036*	The set of subsets of size zero is the singleton of the empty set. (Contributed by Mario Carneiro, 22-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   =>    |- ( A e. V -> ( A C 0 ) = { (/) } )
Theorem	hashbc2 15037*	The size of the binomial set is the binomial coefficient. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   =>    |- ( ( A e. Fin /\ N e. NN0 ) -> ( # ` ( A C N ) ) = ( ( # ` A ) _C N ) )
Theorem	0hashbc 15038*	There are no subsets of the empty set with size greater than zero. (Contributed by Mario Carneiro, 22-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   =>    |- ( N e. NN -> ( (/) C N ) = (/) )
Theorem	ramval 15039*	The value of the Ramsey number function. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by AV, 14-Sep-2020.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }   =>    |- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = inf ( T , RR* , < ) )
Theorem	ramvalOLD 15040*	The value of the Ramsey number function. (Contributed by Mario Carneiro, 21-Apr-2015.) Obsolete version of ramval 15039 as of 14-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }   =>    |- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = sup ( T , RR* , `' < ) )
Theorem	ramcl2lem 15041*	Lemma for extended real closure of the Ramsey number function. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }   =>    |- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = if ( T = (/) , +oo , inf ( T , RR , < ) ) )
Theorem	ramcl2lemOLD 15042*	Lemma for extended real closure of the Ramsey number function. (Contributed by Mario Carneiro, 20-Apr-2015.) Obsolete version of ramcl2lem 15041 as of 14-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }   =>    |- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) = if ( T = (/) , +oo , sup ( T , RR , `' < ) ) )
Theorem	ramtcl 15043*	The Ramsey number has the Ramsey number property if any number does. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }   =>    |- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. T <-> T =/= (/) ) )
Theorem	ramtclOLD 15044*	The Ramsey number has the Ramsey number property if any number does. (Contributed by Mario Carneiro, 20-Apr-2015.) Obsolete version of ramtcl 15043 as of 14-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }   =>    |- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. T <-> T =/= (/) ) )
Theorem	ramtcl2 15045*	The Ramsey number is an integer iff there is a number with the Ramsey number property. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }   =>    |- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. NN0 <-> T =/= (/) ) )
Theorem	ramtcl2OLD 15046*	The Ramsey number is an integer iff there is a number with the Ramsey number property. (Contributed by Mario Carneiro, 20-Apr-2015.) Obsolete version of ramtcl2 15045 as of 14-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }   =>    |- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( ( M Ramsey F ) e. NN0 <-> T =/= (/) ) )
Theorem	ramtub 15047*	The Ramsey number is a lower bound on the set of all numbers with the Ramsey number property. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }   =>    |- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ A e. T ) -> ( M Ramsey F ) <_ A )
Theorem	ramtubOLD 15048*	The Ramsey number is a lower bound on the set of all numbers with the Ramsey number property. (Contributed by Mario Carneiro, 20-Apr-2015.) Obsolete version of ramtub 15047 as of 14-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- T = { n e. NN0 | A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) }   =>    |- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ A e. T ) -> ( M Ramsey F ) <_ A )
Theorem	ramub 15049*	The Ramsey number is a lower bound on the set of all numbers with the Ramsey number property. (Contributed by Mario Carneiro, 22-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> R e. V )   &    |- ( ph -> F : R --> NN0 )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ ( N <_ ( # ` s ) /\ f : ( s C M ) --> R ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) )   =>    |- ( ph -> ( M Ramsey F ) <_ N )
Theorem	ramub2 15050*	It is sufficient to check the Ramsey property on finite sets of size equal to the upper bound. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> R e. V )   &    |- ( ph -> F : R --> NN0 )   &    |- ( ph -> N e. NN0 )   &    |- ( ( ph /\ ( ( # ` s ) = N /\ f : ( s C M ) --> R ) ) -> E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) )   =>    |- ( ph -> ( M Ramsey F ) <_ N )
Theorem	rami 15051*	The defining property of a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> R e. V )   &    |- ( ph -> F : R --> NN0 )   &    |- ( ph -> ( M Ramsey F ) e. NN0 )   &    |- ( ph -> S e. W )   &    |- ( ph -> ( M Ramsey F ) <_ ( # ` S ) )   &    |- ( ph -> G : ( S C M ) --> R )   =>    |- ( ph -> E. c e. R E. x e. ~P S ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' G " { c } ) ) )
Theorem	ramcl2 15052	The Ramsey number is either a nonnegative integer or plus infinity. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. ( NN0 u. { +oo } ) )
Theorem	ramcl2OLD 15053	The Ramsey number is either a nonnegative integer or plus infinity. (Contributed by Mario Carneiro, 20-Apr-2015.) Obsolete version of ramcl2 15052 as of 14-Sep-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. ( NN0 u. { +oo } ) )
Theorem	ramxrcl 15054	The Ramsey number is an extended real number. (This theorem does not imply Ramsey's theorem, unlike ramcl 15066.) (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. RR* )
Theorem	ramubcl 15055	If the Ramsey number is upper bounded, then it is an integer. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) /\ ( A e. NN0 /\ ( M Ramsey F ) <_ A ) ) -> ( M Ramsey F ) e. NN0 )
Theorem	ramlb 15056*	Establish a lower bound on a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- ( ph -> M e. NN0 )   &    |- ( ph -> R e. V )   &    |- ( ph -> F : R --> NN0 )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> G : ( ( 1 ... N ) C M ) --> R )   &    |- ( ( ph /\ ( c e. R /\ x C_ ( 1 ... N ) ) ) -> ( ( x C M ) C_ ( `' G " { c } ) -> ( # ` x ) < ( F ` c ) ) )   =>    |- ( ph -> N < ( M Ramsey F ) )
Theorem	0ram 15057*	The Ramsey number when M = 0. (Contributed by Mario Carneiro, 22-Apr-2015.)
|- ( ( ( R e. V /\ R =/= (/) /\ F : R --> NN0 ) /\ E. x e. ZZ A. y e. ran F y <_ x ) -> ( 0 Ramsey F ) = sup ( ran F , RR , < ) )
Theorem	0ram2 15058	The Ramsey number when M = 0. (Contributed by Mario Carneiro, 22-Apr-2015.)
|- ( ( R e. Fin /\ R =/= (/) /\ F : R --> NN0 ) -> ( 0 Ramsey F ) = sup ( ran F , RR , < ) )
Theorem	ram0 15059	The Ramsey number when R = (/). (Contributed by Mario Carneiro, 22-Apr-2015.)
|- ( M e. NN0 -> ( M Ramsey (/) ) = M )
Theorem	0ramcl 15060	Lemma for ramcl 15066: Existence of the Ramsey number when M = 0. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ( R e. Fin /\ F : R --> NN0 ) -> ( 0 Ramsey F ) e. NN0 )
Theorem	ramz2 15061	The Ramsey number when F has value zero for some color C. (Contributed by Mario Carneiro, 22-Apr-2015.)
|- ( ( ( M e. NN /\ R e. V /\ F : R --> NN0 ) /\ ( C e. R /\ ( F ` C ) = 0 ) ) -> ( M Ramsey F ) = 0 )
Theorem	ramz 15062	The Ramsey number when F is the zero function. (Contributed by Mario Carneiro, 22-Apr-2015.)
|- ( ( M e. NN0 /\ R e. V /\ R =/= (/) ) -> ( M Ramsey ( R X. { 0 } ) ) = 0 )
Theorem	ramub1lem1 15063*	Lemma for ramub1 15065. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ph -> M e. NN )   &    |- ( ph -> R e. Fin )   &    |- ( ph -> F : R --> NN )   &    |- G = ( x e. R |-> ( M Ramsey ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) ) )   &    |- ( ph -> G : R --> NN0 )   &    |- ( ph -> ( ( M - 1 ) Ramsey G ) e. NN0 )   &    |- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- ( ph -> S e. Fin )   &    |- ( ph -> ( # ` S ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) )   &    |- ( ph -> K : ( S C M ) --> R )   &    |- ( ph -> X e. S )   &    |- H = ( u e. ( ( S \ { X } ) C ( M - 1 ) ) |-> ( K ` ( u u. { X } ) ) )   &    |- ( ph -> D e. R )   &    |- ( ph -> W C_ ( S \ { X } ) )   &    |- ( ph -> ( G ` D ) <_ ( # ` W ) )   &    |- ( ph -> ( W C ( M - 1 ) ) C_ ( `' H " { D } ) )   &    |- ( ph -> E e. R )   &    |- ( ph -> V C_ W )   &    |- ( ph -> if ( E = D , ( ( F ` D ) - 1 ) , ( F ` E ) ) <_ ( # ` V ) )   &    |- ( ph -> ( V C M ) C_ ( `' K " { E } ) )   =>    |- ( ph -> E. z e. ~P S ( ( F ` E ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { E } ) ) )
Theorem	ramub1lem2 15064*	Lemma for ramub1 15065. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ph -> M e. NN )   &    |- ( ph -> R e. Fin )   &    |- ( ph -> F : R --> NN )   &    |- G = ( x e. R |-> ( M Ramsey ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) ) )   &    |- ( ph -> G : R --> NN0 )   &    |- ( ph -> ( ( M - 1 ) Ramsey G ) e. NN0 )   &    |- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   &    |- ( ph -> S e. Fin )   &    |- ( ph -> ( # ` S ) = ( ( ( M - 1 ) Ramsey G ) + 1 ) )   &    |- ( ph -> K : ( S C M ) --> R )   &    |- ( ph -> X e. S )   &    |- H = ( u e. ( ( S \ { X } ) C ( M - 1 ) ) |-> ( K ` ( u u. { X } ) ) )   =>    |- ( ph -> E. c e. R E. z e. ~P S ( ( F ` c ) <_ ( # ` z ) /\ ( z C M ) C_ ( `' K " { c } ) ) )
Theorem	ramub1 15065*	Inductive step for Ramsey's theorem, in the form of an explicit upper bound. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ph -> M e. NN )   &    |- ( ph -> R e. Fin )   &    |- ( ph -> F : R --> NN )   &    |- G = ( x e. R |-> ( M Ramsey ( y e. R |-> if ( y = x , ( ( F ` x ) - 1 ) , ( F ` y ) ) ) ) )   &    |- ( ph -> G : R --> NN0 )   &    |- ( ph -> ( ( M - 1 ) Ramsey G ) e. NN0 )   =>    |- ( ph -> ( M Ramsey F ) <_ ( ( ( M - 1 ) Ramsey G ) + 1 ) )
Theorem	ramcl 15066	Ramsey's theorem: the Ramsey number is an integer for every finite coloring and set of upper bounds. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> ( M Ramsey F ) e. NN0 )
Theorem	ramsey 15067*	Ramsey's theorem with the definition Ramsey eliminated. If M is an integer, R is a specified finite set of colors, and F : R --> NN0 is a set of lower bounds for each color, then there is an n such that for every set s of size greater than n and every coloring f of the set ( s C M ) of all M-element subsets of s, there is a color c and a subset x C_ s such that x is larger than F ( c ) and the M-element subsets of x are monochromatic with color c. This is the hypergraph version of Ramsey's theorem; the version for simple graphs is the case M = 2. This is Metamath 100 proof #31. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- C = ( a e. _V , i e. NN0 |-> { b e. ~P a | ( # ` b ) = i } )   =>    |- ( ( M e. NN0 /\ R e. Fin /\ F : R --> NN0 ) -> E. n e. NN0 A. s ( n <_ ( # ` s ) -> A. f e. ( R ^m ( s C M ) ) E. c e. R E. x e. ~P s ( ( F ` c ) <_ ( # ` x ) /\ ( x C M ) C_ ( `' f " { c } ) ) ) )
6.2.15  Primorial function According to Wikipedia "Primorial", https://en.wikipedia.org/wiki/Primorial (28-Aug-2020): "In mathematics, and more particularly in number theory, primorial, denoted by "#", is a function from natural numbers to natural numbers similar to the factorial function, but rather than successively multiplying [all] positive integers [less than or equal to a given number], the function only multiplies [the] prime numbers [less than or equal to the given number]. The name "primorial", coined by Harvey Dubner, draws an analogy to primes similar to the way the name "factorial" relates to factors."
Syntax	cprmo 15068	Extend class notation to include the primorial of nonnegative integers.
class #p
Definition	df-prmo 15069*	Define the primorial function on nonnegative integers as the product of all prime numbers less than or equal to the integer. For example, (#p ` 6 ) = ; 3 0 because ( 5 x. ( 3 x. 2 ) ) = ; 3 0 (see prmo6 15179). In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 24184, where the primorial function is defined by using the sequence builder ( P = seq 1 ( x. , F )), the more specialized definition of a product of a series is used here. (Contributed by AV, 28-Aug-2020.)
|- #p = ( n e. NN0 |-> prod_ k e. ( 1 ... n ) if ( k e. Prime , k , 1 ) )
Theorem	prmoval 15070*	Value of the primorial function for nonnegative integers. (Contributed by AV, 28-Aug-2020.)
|- ( N e. NN0 -> (#p ` N ) = prod_ k e. ( 1 ... N ) if ( k e. Prime , k , 1 ) )
Theorem	prmocl 15071	Closure of the primorial function. (Contributed by AV, 28-Aug-2020.)
|- ( N e. NN0 -> (#p ` N ) e. NN )
Theorem	prmone0 15072	The primorial function is nonzero. (Contributed by AV, 28-Aug-2020.)
|- ( N e. NN0 -> (#p ` N ) =/= 0 )
Theorem	prmo0 15073	The primorial of 0. (Contributed by AV, 28-Aug-2020.)
|- (#p ` 0 ) = 1
Theorem	prmo1 15074	The primorial of 1. (Contributed by AV, 28-Aug-2020.)
|- (#p ` 1 ) = 1
Theorem	prmop1 15075	The primorial of a successor. (Contributed by AV, 28-Aug-2020.)
|- ( N e. NN0 -> (#p ` ( N + 1 ) ) = if ( ( N + 1 ) e. Prime , ( (#p ` N ) x. ( N + 1 ) ) , (#p ` N ) ) )
Theorem	prmonn2 15076	Value of the primorial function expressed recursively. (Contributed by AV, 28-Aug-2020.)
|- ( N e. NN -> (#p ` N ) = if ( N e. Prime , ( (#p ` ( N - 1 ) ) x. N ) , (#p ` ( N - 1 ) ) ) )
Theorem	prmo2 15077	The primorial of 2. (Contributed by AV, 28-Aug-2020.)
|- (#p ` 2 ) = 2
Theorem	prmo3 15078	The primorial of 3. (Contributed by AV, 28-Aug-2020.)
|- (#p ` 3 ) = 6
Theorem	prmdvdsprmo 15079*	The primorial of a number is divisible by each prime less then or equal to the number. (Contributed by AV, 15-Aug-2020.) (Revised by AV, 28-Aug-2020.)
|- ( N e. NN -> A. p e. Prime ( p <_ N -> p || (#p ` N ) ) )
Theorem	prmdvdsprmop 15080*	The primorial of a number plus an integer greater than 1 and less then or equal to the number is divisible by a prime less then or equal to the number. (Contributed by AV, 15-Aug-2020.) (Revised by AV, 28-Aug-2020.)
|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. p e. Prime ( p <_ N /\ p || I /\ p || ( (#p ` N ) + I ) ) )
Theorem	fvprmselelfz 15081*	The value of the prime selection function is in a finite sequence of integers if the argument is in this finite sequence of integers. (Contributed by AV, 19-Aug-2020.)
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )   =>    |- ( ( N e. NN /\ X e. ( 1 ... N ) ) -> ( F ` X ) e. ( 1 ... N ) )
Theorem	fvprmselgcd1 15082*	The greatest common divisor of two values of the prime selection function for different arguments is 1. (Contributed by AV, 19-Aug-2020.)
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )   =>    |- ( ( X e. ( 1 ... N ) /\ Y e. ( 1 ... N ) /\ X =/= Y ) -> ( ( F ` X ) gcd ( F ` Y ) ) = 1 )
Theorem	prmolefac 15083	The primorial of a positive integer is less than or equal to the factorial of the integer. (Contributed by AV, 15-Aug-2020.) (Revised by AV, 29-Aug-2020.)
|- ( N e. NN0 -> (#p ` N ) <_ ( ! ` N ) )
Theorem	prmodvdslcmf 15084	The primorial of a nonnegative integer divides the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020.) (Revised by AV, 29-Aug-2020.)
|- ( N e. NN0 -> (#p ` N ) || (lcm ` ( 1 ... N ) ) )
Theorem	prmolelcmf 15085	The primorial of a positive integer is less than or equal to the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020.) (Revised by AV, 29-Aug-2020.)
|- ( N e. NN0 -> (#p ` N ) <_ (lcm ` ( 1 ... N ) ) )
6.2.16  Prime gaps According to Wikipedia "Prime gap", https://en.wikipedia.org/wiki/Prime_gap (16-Aug-2020): "A prime gap is the difference between two successive prime numbers. The n-th prime gap, denoted gn or g(pn) is the difference between the (n+1)-th and the n-th prime numbers, i.e. gn = pn+1 - pn . We have g1 = 1, g2 = g3 = 2, and g4 = 4." It can be proven that there are arbitrary large gaps, usually by showing that "in the sequence n!+2, n!+3, ..., n!+n the first term is divisible by 2, the second term is divisible by 3, and so on. Thus, this is a sequence of n-1 consecutive composite integers, and it must belong to a gap between primes having length at least n.", see prmgap 15108. Instead of using the factorial of n (see df-fac 12498), any function can be chosen for which f(n) is not relatively prime to the integers 2, 3, ..., n. For example, the least common multiple of the integers 2, 3, ..., n, see prmgaplcm 15110, or the primorial n# (the product of all prime numbers less than or equal to n), see prmgapprmo 15112, are such functions, which provide smaller values than the factorial function (see lcmflefac 14700 and prmolefac 15083 resp. prmolelcmf 15085): "For instance, the first prime gap of size larger than 14 occurs between the primes 523 and 541, while 15! is the vastly larger number 1307674368000." But the least common multiple of the integers 2, 3, ..., 15 is 360360, and 15# is 30030 (p3248 = 30029 and P3249 = 30047, so g3248 = 18).
Theorem	prmgaplem1 15086	Lemma for prmgap 15108: The factorial of a number plus an integer greater than 1 and less then or equal to the number is divisible by that integer. (Contributed by AV, 13-Aug-2020.)
|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( ( ! ` N ) + I ) )
Theorem	prmgaplem2 15087	Lemma for prmgap 15108: The factorial of a number plus an integer greater than 1 and less then or equal to the number are not coprime. (Contributed by AV, 13-Aug-2020.)
|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( ( ! ` N ) + I ) gcd I ) )
Theorem	prmgaplcmlem1 15088	Lemma for prmgaplcm 15110: The least common multiple of all positive integers less than or equal to a number plus an integer greater than 1 and less then or equal to the number is divisible by that integer. (Contributed by AV, 14-Aug-2020.) (Revised by AV, 27-Aug-2020.)
|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( (lcm ` ( 1 ... N ) ) + I ) )
Theorem	prmgaplcmlem2 15089	Lemma for prmgaplcm 15110: The least common multiple of all positive integers less than or equal to a number plus an integer greater than 1 and less then or equal to the number are not coprime. (Contributed by AV, 14-Aug-2020.) (Revised by AV, 27-Aug-2020.)
|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( (lcm ` ( 1 ... N ) ) + I ) gcd I ) )
Theorem	lcmsmapnnOLD 15090*	The function mapping a positive integer to the least common multiple of all positive integers less than or equal to the integer is a mapping from the positive integers to the positive integers. (Contributed by AV, 14-Aug-2020.) Obsolete as of 27-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( x e. NN |-> sup ( { n e. NN | A. m e. ( 1 ... x ) m || n } , RR , `' < ) )   =>    |- F e. ( NN ^m NN )
Theorem	prmgaplcmlem1OLD 15091*	Lemma for prmgaplcmOLD 15109: The least common multiple of all positive integers less than or equal to a number plus an integer greater than 1 and less then or equal to the number is divisible by that integer. (Contributed by AV, 14-Aug-2020.) Obsolete version of prmgaplcmlem1 15088 as of 27-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( x e. NN |-> sup ( { n e. NN | A. m e. ( 1 ... x ) m || n } , RR , `' < ) )   =>    |- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( ( F ` N ) + I ) )
Theorem	prmgaplcmlem2OLD 15092*	Lemma for prmgaplcmOLD 15109: The least common multiple of all positive integers less than or equal to a number plus an integer greater than 1 and less then or equal to the number are not coprime. (Contributed by AV, 14-Aug-2020.) Obsolete version of prmgaplcmlem2 15089 as of 27-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( x e. NN |-> sup ( { n e. NN | A. m e. ( 1 ... x ) m || n } , RR , `' < ) )   =>    |- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( ( F ` N ) + I ) gcd I ) )
Theorem	prmormapnnOLD 15093*	The primorial function is a mapping from the positive integers to the positive integers. In contrast to prmorcht 24184, where the primorial is defined by using the sequence builder ( P = seq 1 ( x. , F )), the more specialized definition of a product of a series is used here. (Contributed by AV, 14-Aug-2020.) Obsolete as of 29-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )   &    |- P = ( n e. NN |-> prod_ k e. ( 1 ... n ) ( F ` k ) )   =>    |- P e. ( NN ^m NN )
Theorem	prmdvdsprmorOLD 15094*	The primorial of a number is divisible by each prime less then or equal to the number. (Contributed by AV, 15-Aug-2020.) Obsolete version of prmdvdsprmo 15079 as of 29-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )   &    |- P = ( n e. NN |-> prod_ k e. ( 1 ... n ) ( F ` k ) )   =>    |- ( N e. NN -> A. p e. Prime ( p <_ N -> p || ( P ` N ) ) )
Theorem	prmdvdsprmorpOLD 15095*	The primorial of a number plus an integer greater than 1 and less then or equal to the number is divisible by a prime less then or equal to the number. (Contributed by AV, 15-Aug-2020.) Obsolete version of prmdvdsprmop 15080 as of 29-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )   &    |- P = ( n e. NN |-> prod_ k e. ( 1 ... n ) ( F ` k ) )   =>    |- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> E. p e. Prime ( p <_ N /\ p || I /\ p || ( ( P ` N ) + I ) ) )
Theorem	prmgapprmorlemOLD 15096*	Lemma for prmgapprmorOLD 15113: The primorial of a number plus an integer greater than 1 and less then or equal to the number are not coprime. (Contributed by AV, 15-Aug-2020.) Obsolete version of prmgapprmolem 15111 as of 29-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )   &    |- P = ( n e. NN |-> prod_ k e. ( 1 ... n ) ( F ` k ) )   =>    |- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( ( P ` N ) + I ) gcd I ) )
Theorem	prmorlefacOLD 15097*	The primorial of a positive integer is less than or equal to the factorial of the integer. (Contributed by AV, 15-Aug-2020.) Obsolete version of prmolefac 15083 as of 29-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )   &    |- P = ( n e. NN |-> prod_ k e. ( 1 ... n ) ( F ` k ) )   =>    |- ( N e. NN -> ( P ` N ) <_ ( ! ` N ) )
Theorem	prmordvdslcmfOLD 15098*	The primorial of a positive integer divides the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020.) (Revised by AV, 27-Aug-2020.) Obsolete version of prmodvdslcmf 15084 as of 29-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )   &    |- P = ( n e. NN |-> prod_ k e. ( 1 ... n ) ( F ` k ) )   =>    |- ( N e. NN -> ( P ` N ) || (lcm ` ( 1 ... N ) ) )
Theorem	prmorlelcmfOLD 15099*	The primorial of a positive integer is less than or equal to the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020.) (Revised by AV, 27-Aug-2020.) Obsolete version of prmolelcmf 15085 as of 29-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )   &    |- P = ( n e. NN |-> prod_ k e. ( 1 ... n ) ( F ` k ) )   =>    |- ( N e. NN -> ( P ` N ) <_ (lcm ` ( 1 ... N ) ) )
Theorem	prmordvdslcmsOLDOLD 15100*	The primorial of a positive integer divides the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020.) Obsolete version of prmordvdslcmfOLD 15098 as of 27-Aug-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- F = ( m e. NN |-> if ( m e. Prime , m , 1 ) )   &    |- P = ( n e. NN |-> prod_ k e. ( 1 ... n ) ( F ` k ) )   &    |- L = ( x e. NN |-> sup ( { n e. NN | A. m e. ( 1 ... x ) m || n } , RR , `' < ) )   =>    |- ( N e. NN -> ( P ` N ) || ( L ` N ) )