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	fvprmselelfz 15001*	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 15002*	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 15003	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 15004	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 15005	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 15028. Instead of using the factorial of n (see df-fac 12466), 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 15030, or the primorial n# (the product of all prime numbers less than or equal to n), see prmgapprmo 15032, are such functions, which provide smaller values than the factorial function (see lcmflefac 14620 and prmolefac 15003 resp. prmolelcmf 15005): "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 15006	Lemma for prmgap 15028: 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 15007	Lemma for prmgap 15028: 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 15008	Lemma for prmgaplcm 15030: 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 15009	Lemma for prmgaplcm 15030: 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 15010*	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 15011*	Lemma for prmgaplcmOLD 15029: 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 15008 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 15012*	Lemma for prmgaplcmOLD 15029: 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 15009 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 15013*	The primorial function is a mapping from the positive integers to the positive integers. In contrast to prmorcht 24103, 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 15014*	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 14999 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 15015*	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 15000 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 15016*	Lemma for prmgapprmorOLD 15033: 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 15031 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 15017*	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 15003 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 15018*	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 15004 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 15019*	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 15005 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 15020*	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 15018 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 ) )
Theorem	prmorlelcmsOLDOLD 15021*	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.) Obsolete version of prmorlelcmfOLD 15019 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 ) )
Theorem	prmgaplem3 15022*	Lemma for prmgap 15028. (Contributed by AV, 9-Aug-2020.)
|- A = { p e. Prime | p < N }   =>    |- ( N e. ( ZZ>= ` 3 ) -> E. x e. A A. y e. A y <_ x )
Theorem	prmgaplem4 15023*	Lemma for prmgap 15028. (Contributed by AV, 10-Aug-2020.)
|- A = { p e. Prime | ( N < p /\ p <_ P ) }   =>    |- ( ( N e. NN /\ P e. Prime /\ N < P ) -> E. x e. A A. y e. A x <_ y )
Theorem	prmgaplem5 15024*	Lemma for prmgap 15028: for each integer greater than 2 there is a smaller prime closest to this integer, i.e. there is a smaller prime and no other prime is between this prime and the integer. (Contributed by AV, 9-Aug-2020.)
|- ( N e. ( ZZ>= ` 3 ) -> E. p e. Prime ( p < N /\ A. z e. ( ( p + 1 )..^ N ) z e/ Prime ) )
Theorem	prmgaplem6 15025*	Lemma for prmgap 15028: for each positive integer there is a greater prime closest to this integer, i.e. there is a greater prime and no other prime is between this prime and the integer. (Contributed by AV, 10-Aug-2020.)
|- ( N e. NN -> E. p e. Prime ( N < p /\ A. z e. ( ( N + 1 )..^ p ) z e/ Prime ) )
Theorem	prmgaplem7 15026*	Lemma for prmgap 15028. (Contributed by AV, 12-Aug-2020.)
|- ( ph -> N e. NN )   &    |- ( ph -> F e. ( NN ^m NN ) )   &    |- ( ph -> A. i e. ( 2 ... N ) 1 < ( ( ( F ` N ) + i ) gcd i ) )   =>    |- ( ph -> E. p e. Prime E. q e. Prime ( p < ( ( F ` N ) + 2 ) /\ ( ( F ` N ) + N ) < q /\ A. z e. ( ( p + 1 )..^ q ) z e/ Prime ) )
Theorem	prmgaplem8 15027*	Lemma for prmgap 15028. (Contributed by AV, 13-Aug-2020.)
|- ( ph -> N e. NN )   &    |- ( ph -> F e. ( NN ^m NN ) )   &    |- ( ph -> A. i e. ( 2 ... N ) 1 < ( ( ( F ` N ) + i ) gcd i ) )   =>    |- ( ph -> E. p e. Prime E. q e. Prime ( N <_ ( q - p ) /\ A. z e. ( ( p + 1 )..^ q ) z e/ Prime ) )
Theorem	prmgap 15028*	The prime gap theorem: for each positive integer there are (at least) two successive primes with a difference ("gap") at least as big as the given integer. (Contributed by AV, 13-Aug-2020.)
|- A. n e. NN E. p e. Prime E. q e. Prime ( n <_ ( q - p ) /\ A. z e. ( ( p + 1 )..^ q ) z e/ Prime )
Theorem	prmgaplcmOLD 15029*	Alternate proof of prmgap 15028: in contrast to prmgap 15028, where the gap starts at n! , the factorial of n, the gap starts at the least common multiple of all positive integers less than or equal to n. (Contributed by AV, 13-Aug-2020.) Obsolete version of prmgaplcm 15030 as of 27-Aug-2020. (Proof modification is discouraged.) (New usage is discouraged.)
|- A. n e. NN E. p e. Prime E. q e. Prime ( n <_ ( q - p ) /\ A. z e. ( ( p + 1 )..^ q ) z e/ Prime )
Theorem	prmgaplcm 15030*	Alternate proof of prmgap 15028: in contrast to prmgap 15028, where the gap starts at n! , the factorial of n, the gap starts at the least common multiple of all positive integers less than or equal to n. (Contributed by AV, 13-Aug-2020.) (Revised by AV, 27-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A. n e. NN E. p e. Prime E. q e. Prime ( n <_ ( q - p ) /\ A. z e. ( ( p + 1 )..^ q ) z e/ Prime )
Theorem	prmgapprmolem 15031	Lemma for prmgapprmo 15032: 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.) (Revised by AV, 29-Aug-2020.)
|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> 1 < ( ( (#p ` N ) + I ) gcd I ) )
Theorem	prmgapprmo 15032*	Alternate proof of prmgap 15028: in contrast to prmgap 15028, where the gap starts at n! , the factorial of n, the gap starts at n#, the primorial of n. (Contributed by AV, 15-Aug-2020.) (Revised by AV, 29-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- A. n e. NN E. p e. Prime E. q e. Prime ( n <_ ( q - p ) /\ A. z e. ( ( p + 1 )..^ q ) z e/ Prime )
Theorem	prmgapprmorOLD 15033*	Alternate proof of prmgap 15028: in contrast to prmgap 15028, where the gap starts at n! , the factorial of n, the gap starts at n#, the primorial of n. (Contributed by AV, 15-Aug-2020.) Obsolete version of prmgapprmo 15032 as of 29-Aug-2020. (Proof modification is discouraged.) (New usage is discouraged.)
|- A. n e. NN E. p e. Prime E. q e. Prime ( n <_ ( q - p ) /\ A. z e. ( ( p + 1 )..^ q ) z e/ Prime )
6.2.17  Decimal arithmetic (cont.)
Theorem	dec2dvds 15034	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 15035	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 15036	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 15037	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN   =>    |- -. ; A 5 e. Prime
Theorem	dec2nprm 15038	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 15039	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 15040	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 15041	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 15042	Version of mod2xi 15040 with a negative 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 15043	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 15044	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 15045	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 15046	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 15047	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 0 ) = 1
Theorem	numexp1 15048	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 1 ) = A
Theorem	numexpp1 15049	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 15050	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 15051	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 15052	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 15053	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 15054	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 15055	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 11105. (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 15056	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 4 ) = ; 1 6
Theorem	2exp6 15057	Two to the sixth power is 64. (Contributed by Mario Carneiro, 20-Apr-2015.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- ( 2 ^ 6 ) = ; 6 4
Theorem	2exp6OLD 15058	Two to the sixth power is 64. (Contributed by Mario Carneiro, 20-Apr-2015.) Obsolete version of 2exp6 15057 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( 2 ^ 6 ) = ; 6 4
Theorem	2exp8 15059	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 8 ) = ;; 2 5 6
Theorem	2exp16 15060	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^; 1 6 ) = ;;;; 6 5 5 3 6
Theorem	3exp3 15061	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 3 ^ 3 ) = ; 2 7
Theorem	2expltfac 15062	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.18  Cyclical shifts of words (cont.)
Theorem	cshwsidrepsw 15063	If cyclically shifting a word of length being a prime number by a number of positions which is not divisible by the prime number results in the word itself, the word is a "repeated symbol word". (Contributed by AV, 18-May-2018.) (Revised by AV, 10-Nov-2018.)
|- ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( L e. ZZ /\ ( L mod ( # ` W ) ) =/= 0 /\ ( W cyclShift L ) = W ) -> W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) )
Theorem	cshwsidrepswmod0 15064	If cyclically shifting a word of length being a prime number results in the word itself, the shift must be either by 0 (modulo the length of the word) or the word must be a "repeated symbol word". (Contributed by AV, 18-May-2018.) (Revised by AV, 10-Nov-2018.)
|- ( ( W e. Word V /\ ( # ` W ) e. Prime /\ L e. ZZ ) -> ( ( W cyclShift L ) = W -> ( ( L mod ( # ` W ) ) = 0 \/ W = ( ( W ` 0 ) repeatS ( # ` W ) ) ) ) )
Theorem	cshwshashlem1 15065*	If cyclically shifting a word of length being a prime number not consisting of identical symbols by at least one position (and not by as many positions as the length of the word), the result will not be the word itself. (Contributed by AV, 19-May-2018.) (Revised by AV, 8-Jun-2018.) (Revised by AV, 10-Nov-2018.)
|- ( ph -> ( W e. Word V /\ ( # ` W ) e. Prime ) )   =>    |- ( ( ph /\ E. i e. ( 0..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) /\ L e. ( 1..^ ( # ` W ) ) ) -> ( W cyclShift L ) =/= W )
Theorem	cshwshashlem2 15066*	If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
|- ( ph -> ( W e. Word V /\ ( # ` W ) e. Prime ) )   =>    |- ( ( ph /\ E. i e. ( 0..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( L e. ( 0..^ ( # ` W ) ) /\ K e. ( 0..^ ( # ` W ) ) /\ K < L ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) )
Theorem	cshwshashlem3 15067*	If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
|- ( ph -> ( W e. Word V /\ ( # ` W ) e. Prime ) )   =>    |- ( ( ph /\ E. i e. ( 0..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> ( ( L e. ( 0..^ ( # ` W ) ) /\ K e. ( 0..^ ( # ` W ) ) /\ K =/= L ) -> ( W cyclShift L ) =/= ( W cyclShift K ) ) )
Theorem	cshwsdisj 15068*	The singletons resulting by cyclically shifting a given word of length being a prime number and not consisting of identical symbols is a disjoint collection. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
|- ( ph -> ( W e. Word V /\ ( # ` W ) e. Prime ) )   =>    |- ( ( ph /\ E. i e. ( 0..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) ) -> Disj n e. ( 0..^ ( # ` W ) ) { ( W cyclShift n ) } )
Theorem	cshwsiun 15069*	The set of (different!) words resulting by cyclically shifting a given word is an indexed union. (Contributed by AV, 19-May-2018.) (Revised by AV, 8-Jun-2018.) (Proof shortened by AV, 8-Nov-2018.)
|- M = { w e. Word V | E. n e. ( 0..^ ( # ` W ) ) ( W cyclShift n ) = w }   =>    |- ( W e. Word V -> M = U_ n e. ( 0..^ ( # ` W ) ) { ( W cyclShift n ) } )
Theorem	cshwsex 15070*	The class of (different!) words resulting by cyclically shifting a given word is a set. (Contributed by AV, 8-Jun-2018.) (Revised by AV, 8-Nov-2018.)
|- M = { w e. Word V | E. n e. ( 0..^ ( # ` W ) ) ( W cyclShift n ) = w }   =>    |- ( W e. Word V -> M e. _V )
Theorem	cshws0 15071*	The size of the set of (different!) words resulting by cyclically shifting an empty word is 0. (Contributed by AV, 8-Nov-2018.)
|- M = { w e. Word V | E. n e. ( 0..^ ( # ` W ) ) ( W cyclShift n ) = w }   =>    |- ( W = (/) -> ( # ` M ) = 0 )
Theorem	cshwrepswhash1 15072*	The size of the set of (different!) words resulting by cyclically shifting a nonempty "repeated symbol word" is 1. (Contributed by AV, 18-May-2018.) (Revised by AV, 8-Nov-2018.)
|- M = { w e. Word V | E. n e. ( 0..^ ( # ` W ) ) ( W cyclShift n ) = w }   =>    |- ( ( A e. V /\ N e. NN /\ W = ( A repeatS N ) ) -> ( # ` M ) = 1 )
Theorem	cshwshashnsame 15073*	If a word (not consisting of identical symbols) has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word. (Contributed by AV, 19-May-2018.) (Revised by AV, 10-Nov-2018.)
|- M = { w e. Word V | E. n e. ( 0..^ ( # ` W ) ) ( W cyclShift n ) = w }   =>    |- ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( E. i e. ( 0..^ ( # ` W ) ) ( W ` i ) =/= ( W ` 0 ) -> ( # ` M ) = ( # ` W ) ) )
Theorem	cshwshash 15074*	If a word has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word or 1. (Contributed by AV, 19-May-2018.) (Revised by AV, 10-Nov-2018.)
|- M = { w e. Word V | E. n e. ( 0..^ ( # ` W ) ) ( W cyclShift n ) = w }   =>    |- ( ( W e. Word V /\ ( # ` W ) e. Prime ) -> ( ( # ` M ) = ( # ` W ) \/ ( # ` M ) = 1 ) )
6.2.19  Specific prime numbers
Theorem	4nprm 15075	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 15076*	Lemma for prmlem1 15078 and prmlem2 15090. (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 15077*	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 15078	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 15079	5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- 5 e. Prime
Theorem	6nprm 15080	6 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 6 e. Prime
Theorem	7prm 15081	7 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- 7 e. Prime
Theorem	8nprm 15082	8 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 8 e. Prime
Theorem	9nprm 15083	9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 9 e. Prime
Theorem	10nprm 15084	10 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 10 e. Prime
Theorem	11prm 15085	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 15086	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 15087	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 15088	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 15089	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 15090	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 15106). 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 15091	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 15092	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 15093	83 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ; 8 3 e. Prime
Theorem	139prm 15094	139 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ;; 1 3 9 e. Prime
Theorem	163prm 15095	163 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ;; 1 6 3 e. Prime
Theorem	317prm 15096	317 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ;; 3 1 7 e. Prime
Theorem	631prm 15097	631 is a prime number. (Contributed by Mario Carneiro, 1-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ;; 6 3 1 e. Prime
Theorem	prmo4 15098	The primorial of 4. (Contributed by AV, 28-Aug-2020.)
|- (#p ` 4 ) = 6
Theorem	prmo5 15099	The primorial of 5. (Contributed by AV, 28-Aug-2020.)
|- (#p ` 5 ) = ; 3 0
Theorem	prmo6 15100	The primorial of 6. (Contributed by AV, 28-Aug-2020.)
|- (#p ` 6 ) = ; 3 0