P. 134 of Theorem List - Metamath Proof Explorer

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

Theorem List for Metamath Proof Explorer - 13301-13400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	vdwmc 13301*	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 13302*	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 13303*	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 13304*	Lemma for vdw 13317. (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 13305*	Lemma for vdw 13317. (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 13306	Lemma for vdw 13317. (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 13307*	Lemma for vdw 13317. (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 13308*	Lemma for vdw 13317. (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 13309*	Lemma for vdw 13317. (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 13310*	Lemma for vdw 13317. (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 13311*	Lemma for vdw 13317. (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 13312*	Lemma for vdw 13317. (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 13313*	Lemma for vdw 13317. 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 13314*	Lemma for vdw 13317. (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 13315	Lemma for vdw 13317. 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 13316*	Lemma for vdw 13317. 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 13317*	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 13318*	Corollary of vdw 13317, and lemma for vdwnn 13321. 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 13319*	Lemma for vdwnn 13321. 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 13320*	Lemma for vdwnn 13321. (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 -> A. c e. R S =/= (/) )   =>    |- -. ph
Theorem	vdwnn 13321*	Van der Waerden's theorem, infinitary version. For any finite coloring F of the natural numbers, 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.12  Ramsey's theorem
Syntax	cram 13322	Extend class notation with the Ramsey number function.
class Ramsey
Theorem	ramtlecl 13323*	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 13324*	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.)
|- 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 13325*	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 13326*	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 13327*	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 13328*	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 13329*	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 13330*	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 13331*	The value of the Ramsey number function. (Contributed by Mario Carneiro, 21-Apr-2015.)
|- 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 13332*	Lemma for extended real closure of the Ramsey number function. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- 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 13333*	The Ramsey number has the Ramsey number property if any number does. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- 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 13334*	The Ramsey number is an integer iff there is a number with the Ramsey number property. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- 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 13335*	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.)
|- 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 13336*	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 13337*	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 13338*	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 13339	The Ramsey number is either a nonnegative integer or plus infinity. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. ( NN0 u. { +oo } ) )
Theorem	ramxrcl 13340	The Ramsey number is an extended real number. (This theorem does not imply Ramsey's theorem, unlike ramcl 13352.) (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( ( M e. NN0 /\ R e. V /\ F : R --> NN0 ) -> ( M Ramsey F ) e. RR* )
Theorem	ramubcl 13341	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 13342*	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 13343*	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 13344	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 13345	The Ramsey number when R = (/). (Contributed by Mario Carneiro, 22-Apr-2015.)
|- ( M e. NN0 -> ( M Ramsey (/) ) = M )
Theorem	0ramcl 13346	Lemma for ramcl 13352: 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 13347	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 13348	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 13349*	Lemma for ramub1 13351. (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 13350*	Lemma for ramub1 13351. (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 13351*	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 13352	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 13353*	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. (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.13  Decimal arithmetic (cont.)
Theorem	dec2dvds 13354	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN0   &    |- ( B x. 2 ) = C   &    |- D = ( C + 1 )   =>    |- -. 2 || ; A D
Theorem	dec5dvds 13355	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN   &    |- B < 5   =>    |- -. 5 || ; A B
Theorem	dec5dvds2 13356	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN   &    |- B < 5   &    |- ( 5 + B ) = C   =>    |- -. 5 || ; A C
Theorem	dec5nprm 13357	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN   =>    |- -. ; A 5 e. Prime
Theorem	dec2nprm 13358	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN   &    |- B e. NN0   &    |- ( B x. 2 ) = C   =>    |- -. ; A C e. Prime
Theorem	modxai 13359	Add exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) (Revised by Mario Carneiro, 5-Feb-2015.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN0   &    |- M e. NN0   &    |- C e. NN0   &    |- L e. NN0   &    |- ( ( A ^ B ) mod N ) = ( K mod N )   &    |- ( ( A ^ C ) mod N ) = ( L mod N )   &    |- ( B + C ) = E   &    |- ( ( D x. N ) + M ) = ( K x. L )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	mod2xi 13360	Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN0   &    |- M e. NN0   &    |- ( ( A ^ B ) mod N ) = ( K mod N )   &    |- ( 2 x. B ) = E   &    |- ( ( D x. N ) + M ) = ( K x. K )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	modxp1i 13361	Add one to an exponent in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN0   &    |- M e. NN0   &    |- ( ( A ^ B ) mod N ) = ( K mod N )   &    |- ( B + 1 ) = E   &    |- ( ( D x. N ) + M ) = ( K x. A )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	mod2xnegi 13362	Version of mod2xi 13360 with a negaive mod value. (Contributed by Mario Carneiro, 21-Feb-2014.)
|- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN   &    |- M e. NN0   &    |- L e. NN0   &    |- ( ( A ^ B ) mod N ) = ( L mod N )   &    |- ( 2 x. B ) = E   &    |- ( L + K ) = N   &    |- ( ( D x. N ) + M ) = ( K x. K )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	modsubi 13363	Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- M e. NN0   &    |- ( A mod N ) = ( K mod N )   &    |- ( M + B ) = K   =>    |- ( ( A - B ) mod N ) = ( M mod N )
Theorem	gcdi 13364	Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.)
|- K e. NN0   &    |- R e. NN0   &    |- N e. NN0   &    |- ( N gcd R ) = G   &    |- ( ( K x. N ) + R ) = M   =>    |- ( M gcd N ) = G
Theorem	gcdmodi 13365	Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.)
|- K e. NN0   &    |- R e. NN0   &    |- N e. NN   &    |- ( K mod N ) = ( R mod N )   &    |- ( N gcd R ) = G   =>    |- ( K gcd N ) = G
Theorem	decexp2 13366	Calculate a power of two. (Contributed by Mario Carneiro, 19-Feb-2014.)
|- M e. NN0   &    |- ( M + 2 ) = N   =>    |- ( ( 4 x. ( 2 ^ M ) ) + 0 ) = ( 2 ^ N )
Theorem	numexp0 13367	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 0 ) = 1
Theorem	numexp1 13368	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 1 ) = A
Theorem	numexpp1 13369	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   &    |- M e. NN0   &    |- ( M + 1 ) = N   &    |- ( ( A ^ M ) x. A ) = C   =>    |- ( A ^ N ) = C
Theorem	numexp2x 13370	Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   &    |- M e. NN0   &    |- ( 2 x. M ) = N   &    |- ( A ^ M ) = D   &    |- ( D x. D ) = C   =>    |- ( A ^ N ) = C
Theorem	decsplit0b 13371	Split a decimal number into two parts. Base case: N = 0. (Contributed by Mario Carneiro, 16-Jul-2015.)
|- A e. NN0   =>    |- ( ( A x. ( 10 ^ 0 ) ) + B ) = ( A + B )
Theorem	decsplit0 13372	Split a decimal number into two parts. Base case: N = 0. (Contributed by Mario Carneiro, 16-Jul-2015.)
|- A e. NN0   =>    |- ( ( A x. ( 10 ^ 0 ) ) + 0 ) = A
Theorem	decsplit1 13373	Split a decimal number into two parts. Base case: N = 1. (Contributed by Mario Carneiro, 16-Jul-2015.)
|- A e. NN0   =>    |- ( ( A x. ( 10 ^ 1 ) ) + B ) = ; A B
Theorem	decsplit 13374	Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015.)
|- A e. NN0   &    |- B e. NN0   &    |- D e. NN0   &    |- M e. NN0   &    |- ( M + 1 ) = N   &    |- ( ( A x. ( 10 ^ M ) ) + B ) = C   =>    |- ( ( A x. ( 10 ^ N ) ) + ; B D ) = ; C D
Theorem	karatsuba 13375	The Karatsuba multiplication algorithm. If X and Y are decomposed into two groups of digits of length M (only the lower group is known to be this size but the algorithm is most efficient when the partition is chosen near the middle of the digit string), then X Y can be written in three groups of digits, where each group needs only one multiplication. Thus, we can halve both inputs with only three multiplications on the smaller operands, yielding an asymptotic improvement of n^(log2 3) instead of n^2 for the "naive" algorithm decmul1c 10385. (Contributed by Mario Carneiro, 16-Jul-2015.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- S e. NN0   &    |- M e. NN0   &    |- ( A x. C ) = R   &    |- ( B x. D ) = T   &    |- ( ( A + B ) x. ( C + D ) ) = ( ( R + S ) + T )   &    |- ( ( A x. ( 10 ^ M ) ) + B ) = X   &    |- ( ( C x. ( 10 ^ M ) ) + D ) = Y   &    |- ( ( R x. ( 10 ^ M ) ) + S ) = W   &    |- ( ( W x. ( 10 ^ M ) ) + T ) = Z   =>    |- ( X x. Y ) = Z
Theorem	2exp4 13376	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 4 ) = ; 1 6
Theorem	2exp6 13377	Two to the sixth power is 64. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 6 ) = ; 6 4
Theorem	2exp8 13378	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 8 ) = ;; 2 5 6
Theorem	2exp16 13379	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^; 1 6 ) = ;;;; 6 5 5 3 6
Theorem	3exp3 13380	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 3 ^ 3 ) = ; 2 7
Theorem	2expltfac 13381	The factorial grows faster than two to the power N. (Contributed by Mario Carneiro, 15-Sep-2016.)
|- ( N e. ( ZZ>= ` 4 ) -> ( 2 ^ N ) < ( ! ` N ) )
6.2.14  Specific prime numbers
Theorem	4nprm 13382	4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 18-Feb-2014.)
|- -. 4 e. Prime
Theorem	prmlem0 13383*	Lemma for prmlem1 13385 and prmlem2 13397. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- ( ( -. 2 || M /\ x e. ( ZZ>= ` M ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )   &    |- ( K e. Prime -> -. K || N )   &    |- ( K + 2 ) = M   =>    |- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
Theorem	prmlem1a 13384*	A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- N e. NN   &    |- 1 < N   &    |- -. 2 || N   &    |- -. 3 || N   &    |- ( ( -. 2 || 5 /\ x e. ( ZZ>= ` 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )   =>    |- N e. Prime
Theorem	prmlem1 13385	A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- N e. NN   &    |- 1 < N   &    |- -. 2 || N   &    |- -. 3 || N   &    |- N < ; 2 5   =>    |- N e. Prime
Theorem	5prm 13386	5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- 5 e. Prime
Theorem	6nprm 13387	6 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 6 e. Prime
Theorem	7prm 13388	7 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- 7 e. Prime
Theorem	8nprm 13389	8 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 8 e. Prime
Theorem	9nprm 13390	9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 9 e. Prime
Theorem	10nprm 13391	10 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 10 e. Prime
Theorem	11prm 13392	11 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- ; 1 1 e. Prime
Theorem	13prm 13393	13 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- ; 1 3 e. Prime
Theorem	17prm 13394	17 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- ; 1 7 e. Prime
Theorem	19prm 13395	19 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- ; 1 9 e. Prime
Theorem	23prm 13396	23 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- ; 2 3 e. Prime
Theorem	prmlem2 13397	Our last proving session got as far as 25 because we started with the two "bootstrap" primes 2 and 3, and the next prime is 5, so knowing that 2 and 3 are prime and 4 is not allows us to cover the numbers less than 5 ^ 2 = 2 5. Additionally, nonprimes are "easy", so we can extend this range of known prime/nonprimes all the way until 29, which is the first prime larger than 25. Thus, in this lemma we extend another blanket out to 2 9 ^ 2 = 8 4 1, from which we can prove even more primes. If we wanted, we could keep doing this, but the goal is Bertrand's postulate, and for that we only need a few large primes - we don't need to find them all, as we have been doing thus far. So after this blanket runs out, we'll have to switch to another method (see 1259prm 13410). As a side note, you can see the pattern of the primes in the indentation pattern of this lemma! (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- N e. NN   &    |- N < ;; 8 4 1   &    |- 1 < N   &    |- -. 2 || N   &    |- -. 3 || N   &    |- -. 5 || N   &    |- -. 7 || N   &    |- -. ; 1 1 || N   &    |- -. ; 1 3 || N   &    |- -. ; 1 7 || N   &    |- -. ; 1 9 || N   &    |- -. ; 2 3 || N   =>    |- N e. Prime
Theorem	37prm 13398	37 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ; 3 7 e. Prime
Theorem	43prm 13399	43 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ; 4 3 e. Prime
Theorem	83prm 13400	83 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ; 8 3 e. Prime