![]() |
Metamath
Proof Explorer Theorem List (p. 171 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | prmo3 17001 | The primorial of 3. (Contributed by AV, 28-Aug-2020.) |
โข (#pโ3) = 6 | ||
Theorem | prmdvdsprmo 17002* | 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.) |
โข (๐ โ โ โ โ๐ โ โ (๐ โค ๐ โ ๐ โฅ (#pโ๐))) | ||
Theorem | prmdvdsprmop 17003* | 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.) |
โข ((๐ โ โ โง ๐ผ โ (2...๐)) โ โ๐ โ โ (๐ โค ๐ โง ๐ โฅ ๐ผ โง ๐ โฅ ((#pโ๐) + ๐ผ))) | ||
Theorem | fvprmselelfz 17004* | 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.) |
โข ๐น = (๐ โ โ โฆ if(๐ โ โ, ๐, 1)) โ โข ((๐ โ โ โง ๐ โ (1...๐)) โ (๐นโ๐) โ (1...๐)) | ||
Theorem | fvprmselgcd1 17005* | The greatest common divisor of two values of the prime selection function for different arguments is 1. (Contributed by AV, 19-Aug-2020.) |
โข ๐น = (๐ โ โ โฆ if(๐ โ โ, ๐, 1)) โ โข ((๐ โ (1...๐) โง ๐ โ (1...๐) โง ๐ โ ๐) โ ((๐นโ๐) gcd (๐นโ๐)) = 1) | ||
Theorem | prmolefac 17006 | 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.) |
โข (๐ โ โ0 โ (#pโ๐) โค (!โ๐)) | ||
Theorem | prmodvdslcmf 17007 | 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.) |
โข (๐ โ โ0 โ (#pโ๐) โฅ (lcmโ(1...๐))) | ||
Theorem | prmolelcmf 17008 | 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.) |
โข (๐ โ โ0 โ (#pโ๐) โค (lcmโ(1...๐))) | ||
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 17019. Instead of using the factorial of n (see df-fac 14257), 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 17020, or the primorial n# (the product of all prime numbers less than or equal to n), see prmgapprmo 17022, are such functions, which provide smaller values than the factorial function (see lcmflefac 16610 and prmolefac 17006 resp. prmolelcmf 17008): "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 17009 | Lemma for prmgap 17019: 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.) |
โข ((๐ โ โ โง ๐ผ โ (2...๐)) โ ๐ผ โฅ ((!โ๐) + ๐ผ)) | ||
Theorem | prmgaplem2 17010 | Lemma for prmgap 17019: 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.) |
โข ((๐ โ โ โง ๐ผ โ (2...๐)) โ 1 < (((!โ๐) + ๐ผ) gcd ๐ผ)) | ||
Theorem | prmgaplcmlem1 17011 | Lemma for prmgaplcm 17020: 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.) |
โข ((๐ โ โ โง ๐ผ โ (2...๐)) โ ๐ผ โฅ ((lcmโ(1...๐)) + ๐ผ)) | ||
Theorem | prmgaplcmlem2 17012 | Lemma for prmgaplcm 17020: 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.) |
โข ((๐ โ โ โง ๐ผ โ (2...๐)) โ 1 < (((lcmโ(1...๐)) + ๐ผ) gcd ๐ผ)) | ||
Theorem | prmgaplem3 17013* | Lemma for prmgap 17019. (Contributed by AV, 9-Aug-2020.) |
โข ๐ด = {๐ โ โ โฃ ๐ < ๐} โ โข (๐ โ (โคโฅโ3) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) | ||
Theorem | prmgaplem4 17014* | Lemma for prmgap 17019. (Contributed by AV, 10-Aug-2020.) |
โข ๐ด = {๐ โ โ โฃ (๐ < ๐ โง ๐ โค ๐)} โ โข ((๐ โ โ โง ๐ โ โ โง ๐ < ๐) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) | ||
Theorem | prmgaplem5 17015* | Lemma for prmgap 17019: 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.) |
โข (๐ โ (โคโฅโ3) โ โ๐ โ โ (๐ < ๐ โง โ๐ง โ ((๐ + 1)..^๐)๐ง โ โ)) | ||
Theorem | prmgaplem6 17016* | Lemma for prmgap 17019: 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.) |
โข (๐ โ โ โ โ๐ โ โ (๐ < ๐ โง โ๐ง โ ((๐ + 1)..^๐)๐ง โ โ)) | ||
Theorem | prmgaplem7 17017* | Lemma for prmgap 17019. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐น โ (โ โm โ)) & โข (๐ โ โ๐ โ (2...๐)1 < (((๐นโ๐) + ๐) gcd ๐)) โ โข (๐ โ โ๐ โ โ โ๐ โ โ (๐ < ((๐นโ๐) + 2) โง ((๐นโ๐) + ๐) < ๐ โง โ๐ง โ ((๐ + 1)..^๐)๐ง โ โ)) | ||
Theorem | prmgaplem8 17018* | Lemma for prmgap 17019. (Contributed by AV, 13-Aug-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐น โ (โ โm โ)) & โข (๐ โ โ๐ โ (2...๐)1 < (((๐นโ๐) + ๐) gcd ๐)) โ โข (๐ โ โ๐ โ โ โ๐ โ โ (๐ โค (๐ โ ๐) โง โ๐ง โ ((๐ + 1)..^๐)๐ง โ โ)) | ||
Theorem | prmgap 17019* | 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.) |
โข โ๐ โ โ โ๐ โ โ โ๐ โ โ (๐ โค (๐ โ ๐) โง โ๐ง โ ((๐ + 1)..^๐)๐ง โ โ) | ||
Theorem | prmgaplcm 17020* | Alternate proof of prmgap 17019: in contrast to prmgap 17019, 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.) |
โข โ๐ โ โ โ๐ โ โ โ๐ โ โ (๐ โค (๐ โ ๐) โง โ๐ง โ ((๐ + 1)..^๐)๐ง โ โ) | ||
Theorem | prmgapprmolem 17021 | Lemma for prmgapprmo 17022: 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.) |
โข ((๐ โ โ โง ๐ผ โ (2...๐)) โ 1 < (((#pโ๐) + ๐ผ) gcd ๐ผ)) | ||
Theorem | prmgapprmo 17022* | Alternate proof of prmgap 17019: in contrast to prmgap 17019, 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.) |
โข โ๐ โ โ โ๐ โ โ โ๐ โ โ (๐ โค (๐ โ ๐) โง โ๐ง โ ((๐ + 1)..^๐)๐ง โ โ) | ||
Theorem | dec2dvds 17023 | Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข (๐ต ยท 2) = ๐ถ & โข ๐ท = (๐ถ + 1) โ โข ยฌ 2 โฅ ;๐ด๐ท | ||
Theorem | dec5dvds 17024 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ต โ โ & โข ๐ต < 5 โ โข ยฌ 5 โฅ ;๐ด๐ต | ||
Theorem | dec5dvds2 17025 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ต โ โ & โข ๐ต < 5 & โข (5 + ๐ต) = ๐ถ โ โข ยฌ 5 โฅ ;๐ด๐ถ | ||
Theorem | dec5nprm 17026 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ โ โข ยฌ ;๐ด5 โ โ | ||
Theorem | dec2nprm 17027 | Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ & โข ๐ต โ โ0 & โข (๐ต ยท 2) = ๐ถ โ โข ยฌ ;๐ด๐ถ โ โ | ||
Theorem | modxai 17028 | Add exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) (Revised by Mario Carneiro, 5-Feb-2015.) |
โข ๐ โ โ & โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ท โ โค & โข ๐พ โ โ0 & โข ๐ โ โ0 & โข ๐ถ โ โ0 & โข ๐ฟ โ โ0 & โข ((๐ดโ๐ต) mod ๐) = (๐พ mod ๐) & โข ((๐ดโ๐ถ) mod ๐) = (๐ฟ mod ๐) & โข (๐ต + ๐ถ) = ๐ธ & โข ((๐ท ยท ๐) + ๐) = (๐พ ยท ๐ฟ) โ โข ((๐ดโ๐ธ) mod ๐) = (๐ mod ๐) | ||
Theorem | mod2xi 17029 | Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) |
โข ๐ โ โ & โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ท โ โค & โข ๐พ โ โ0 & โข ๐ โ โ0 & โข ((๐ดโ๐ต) mod ๐) = (๐พ mod ๐) & โข (2 ยท ๐ต) = ๐ธ & โข ((๐ท ยท ๐) + ๐) = (๐พ ยท ๐พ) โ โข ((๐ดโ๐ธ) mod ๐) = (๐ mod ๐) | ||
Theorem | modxp1i 17030 | Add one to an exponent in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) |
โข ๐ โ โ & โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ท โ โค & โข ๐พ โ โ0 & โข ๐ โ โ0 & โข ((๐ดโ๐ต) mod ๐) = (๐พ mod ๐) & โข (๐ต + 1) = ๐ธ & โข ((๐ท ยท ๐) + ๐) = (๐พ ยท ๐ด) โ โข ((๐ดโ๐ธ) mod ๐) = (๐ mod ๐) | ||
Theorem | mod2xnegi 17031 | Version of mod2xi 17029 with a negative mod value. (Contributed by Mario Carneiro, 21-Feb-2014.) |
โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ท โ โค & โข ๐พ โ โ & โข ๐ โ โ0 & โข ๐ฟ โ โ0 & โข ((๐ดโ๐ต) mod ๐) = (๐ฟ mod ๐) & โข (2 ยท ๐ต) = ๐ธ & โข (๐ฟ + ๐พ) = ๐ & โข ((๐ท ยท ๐) + ๐) = (๐พ ยท ๐พ) โ โข ((๐ดโ๐ธ) mod ๐) = (๐ mod ๐) | ||
Theorem | modsubi 17032 | Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ & โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข (๐ด mod ๐) = (๐พ mod ๐) & โข (๐ + ๐ต) = ๐พ โ โข ((๐ด โ ๐ต) mod ๐) = (๐ mod ๐) | ||
Theorem | gcdi 17033 | Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.) |
โข ๐พ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข (๐ gcd ๐ ) = ๐บ & โข ((๐พ ยท ๐) + ๐ ) = ๐ โ โข (๐ gcd ๐) = ๐บ | ||
Theorem | gcdmodi 17034 | Calculate a GCD via Euclid's algorithm. Theorem 5.6 in [ApostolNT] p. 109. (Contributed by Mario Carneiro, 19-Feb-2014.) |
โข ๐พ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ & โข (๐พ mod ๐) = (๐ mod ๐) & โข (๐ gcd ๐ ) = ๐บ โ โข (๐พ gcd ๐) = ๐บ | ||
Theorem | decexp2 17035 | Calculate a power of two. (Contributed by Mario Carneiro, 19-Feb-2014.) |
โข ๐ โ โ0 & โข (๐ + 2) = ๐ โ โข ((4 ยท (2โ๐)) + 0) = (2โ๐) | ||
Theorem | numexp0 17036 | Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
โข ๐ด โ โ0 โ โข (๐ดโ0) = 1 | ||
Theorem | numexp1 17037 | Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
โข ๐ด โ โ0 โ โข (๐ดโ1) = ๐ด | ||
Theorem | numexpp1 17038 | Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ โ โ0 & โข (๐ + 1) = ๐ & โข ((๐ดโ๐) ยท ๐ด) = ๐ถ โ โข (๐ดโ๐) = ๐ถ | ||
Theorem | numexp2x 17039 | Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ โ โ0 & โข (2 ยท ๐) = ๐ & โข (๐ดโ๐) = ๐ท & โข (๐ท ยท ๐ท) = ๐ถ โ โข (๐ดโ๐) = ๐ถ | ||
Theorem | decsplit0b 17040 | Split a decimal number into two parts. Base case: ๐ = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.) |
โข ๐ด โ โ0 โ โข ((๐ด ยท (;10โ0)) + ๐ต) = (๐ด + ๐ต) | ||
Theorem | decsplit0 17041 | Split a decimal number into two parts. Base case: ๐ = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.) |
โข ๐ด โ โ0 โ โข ((๐ด ยท (;10โ0)) + 0) = ๐ด | ||
Theorem | decsplit1 17042 | Split a decimal number into two parts. Base case: ๐ = 1. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.) |
โข ๐ด โ โ0 โ โข ((๐ด ยท (;10โ1)) + ๐ต) = ;๐ด๐ต | ||
Theorem | decsplit 17043 | Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ท โ โ0 & โข ๐ โ โ0 & โข (๐ + 1) = ๐ & โข ((๐ด ยท (;10โ๐)) + ๐ต) = ๐ถ โ โข ((๐ด ยท (;10โ๐)) + ;๐ต๐ท) = ;๐ถ๐ท | ||
Theorem | karatsuba 17044 | The Karatsuba multiplication algorithm. If ๐ and ๐ are decomposed into two groups of digits of length ๐ (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 ๐๐ 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 12764. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 9-Sep-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข (๐ด ยท ๐ถ) = ๐ & โข (๐ต ยท ๐ท) = ๐ & โข ((๐ด + ๐ต) ยท (๐ถ + ๐ท)) = ((๐ + ๐) + ๐) & โข ((๐ด ยท (;10โ๐)) + ๐ต) = ๐ & โข ((๐ถ ยท (;10โ๐)) + ๐ท) = ๐ & โข ((๐ ยท (;10โ๐)) + ๐) = ๐ & โข ((๐ ยท (;10โ๐)) + ๐) = ๐ โ โข (๐ ยท ๐) = ๐ | ||
Theorem | 2exp4 17045 | Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.) |
โข (2โ4) = ;16 | ||
Theorem | 2exp5 17046 | Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.) |
โข (2โ5) = ;32 | ||
Theorem | 2exp6 17047 | Two to the sixth power is 64. (Contributed by Mario Carneiro, 20-Apr-2015.) (Proof shortened by OpenAI, 25-Mar-2020.) |
โข (2โ6) = ;64 | ||
Theorem | 2exp7 17048 | Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.) |
โข (2โ7) = ;;128 | ||
Theorem | 2exp8 17049 | Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.) |
โข (2โ8) = ;;256 | ||
Theorem | 2exp11 17050 | Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.) |
โข (2โ;11) = ;;;2048 | ||
Theorem | 2exp16 17051 | Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.) |
โข (2โ;16) = ;;;;65536 | ||
Theorem | 3exp3 17052 | Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.) |
โข (3โ3) = ;27 | ||
Theorem | 2expltfac 17053 | The factorial grows faster than two to the power ๐. (Contributed by Mario Carneiro, 15-Sep-2016.) |
โข (๐ โ (โคโฅโ4) โ (2โ๐) < (!โ๐)) | ||
Theorem | cshwsidrepsw 17054 | 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.) |
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ ((๐ฟ โ โค โง (๐ฟ mod (โฏโ๐)) โ 0 โง (๐ cyclShift ๐ฟ) = ๐) โ ๐ = ((๐โ0) repeatS (โฏโ๐)))) | ||
Theorem | cshwsidrepswmod0 17055 | 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.) |
โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ โง ๐ฟ โ โค) โ ((๐ cyclShift ๐ฟ) = ๐ โ ((๐ฟ mod (โฏโ๐)) = 0 โจ ๐ = ((๐โ0) repeatS (โฏโ๐))))) | ||
Theorem | cshwshashlem1 17056* | 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.) |
โข (๐ โ (๐ โ Word ๐ โง (โฏโ๐) โ โ)) โ โข ((๐ โง โ๐ โ (0..^(โฏโ๐))(๐โ๐) โ (๐โ0) โง ๐ฟ โ (1..^(โฏโ๐))) โ (๐ cyclShift ๐ฟ) โ ๐) | ||
Theorem | cshwshashlem2 17057* | 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.) |
โข (๐ โ (๐ โ Word ๐ โง (โฏโ๐) โ โ)) โ โข ((๐ โง โ๐ โ (0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ ((๐ฟ โ (0..^(โฏโ๐)) โง ๐พ โ (0..^(โฏโ๐)) โง ๐พ < ๐ฟ) โ (๐ cyclShift ๐ฟ) โ (๐ cyclShift ๐พ))) | ||
Theorem | cshwshashlem3 17058* | 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.) |
โข (๐ โ (๐ โ Word ๐ โง (โฏโ๐) โ โ)) โ โข ((๐ โง โ๐ โ (0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ ((๐ฟ โ (0..^(โฏโ๐)) โง ๐พ โ (0..^(โฏโ๐)) โง ๐พ โ ๐ฟ) โ (๐ cyclShift ๐ฟ) โ (๐ cyclShift ๐พ))) | ||
Theorem | cshwsdisj 17059* | 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.) |
โข (๐ โ (๐ โ Word ๐ โง (โฏโ๐) โ โ)) โ โข ((๐ โง โ๐ โ (0..^(โฏโ๐))(๐โ๐) โ (๐โ0)) โ Disj ๐ โ (0..^(โฏโ๐)){(๐ cyclShift ๐)}) | ||
Theorem | cshwsiun 17060* | 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.) |
โข ๐ = {๐ค โ Word ๐ โฃ โ๐ โ (0..^(โฏโ๐))(๐ cyclShift ๐) = ๐ค} โ โข (๐ โ Word ๐ โ ๐ = โช ๐ โ (0..^(โฏโ๐)){(๐ cyclShift ๐)}) | ||
Theorem | cshwsex 17061* | 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.) |
โข ๐ = {๐ค โ Word ๐ โฃ โ๐ โ (0..^(โฏโ๐))(๐ cyclShift ๐) = ๐ค} โ โข (๐ โ Word ๐ โ ๐ โ V) | ||
Theorem | cshws0 17062* | The size of the set of (different!) words resulting by cyclically shifting an empty word is 0. (Contributed by AV, 8-Nov-2018.) |
โข ๐ = {๐ค โ Word ๐ โฃ โ๐ โ (0..^(โฏโ๐))(๐ cyclShift ๐) = ๐ค} โ โข (๐ = โ โ (โฏโ๐) = 0) | ||
Theorem | cshwrepswhash1 17063* | 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.) |
โข ๐ = {๐ค โ Word ๐ โฃ โ๐ โ (0..^(โฏโ๐))(๐ cyclShift ๐) = ๐ค} โ โข ((๐ด โ ๐ โง ๐ โ โ โง ๐ = (๐ด repeatS ๐)) โ (โฏโ๐) = 1) | ||
Theorem | cshwshashnsame 17064* | 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.) |
โข ๐ = {๐ค โ Word ๐ โฃ โ๐ โ (0..^(โฏโ๐))(๐ cyclShift ๐) = ๐ค} โ โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ (โ๐ โ (0..^(โฏโ๐))(๐โ๐) โ (๐โ0) โ (โฏโ๐) = (โฏโ๐))) | ||
Theorem | cshwshash 17065* | 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.) |
โข ๐ = {๐ค โ Word ๐ โฃ โ๐ โ (0..^(โฏโ๐))(๐ cyclShift ๐) = ๐ค} โ โข ((๐ โ Word ๐ โง (โฏโ๐) โ โ) โ ((โฏโ๐) = (โฏโ๐) โจ (โฏโ๐) = 1)) | ||
Theorem | prmlem0 17066* | Lemma for prmlem1 17068 and prmlem2 17080. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ((ยฌ 2 โฅ ๐ โง ๐ฅ โ (โคโฅโ๐)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) & โข (๐พ โ โ โ ยฌ ๐พ โฅ ๐) & โข (๐พ + 2) = ๐ โ โข ((ยฌ 2 โฅ ๐พ โง ๐ฅ โ (โคโฅโ๐พ)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) | ||
Theorem | prmlem1a 17067* | A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ & โข 1 < ๐ & โข ยฌ 2 โฅ ๐ & โข ยฌ 3 โฅ ๐ & โข ((ยฌ 2 โฅ 5 โง ๐ฅ โ (โคโฅโ5)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) โ โข ๐ โ โ | ||
Theorem | prmlem1 17068 | A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ & โข 1 < ๐ & โข ยฌ 2 โฅ ๐ & โข ยฌ 3 โฅ ๐ & โข ๐ < ;25 โ โข ๐ โ โ | ||
Theorem | 5prm 17069 | 5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข 5 โ โ | ||
Theorem | 6nprm 17070 | 6 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ยฌ 6 โ โ | ||
Theorem | 7prm 17071 | 7 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข 7 โ โ | ||
Theorem | 8nprm 17072 | 8 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ยฌ 8 โ โ | ||
Theorem | 9nprm 17073 | 9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ยฌ 9 โ โ | ||
Theorem | 10nprm 17074 | 10 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ยฌ ;10 โ โ | ||
Theorem | 11prm 17075 | 11 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ;11 โ โ | ||
Theorem | 13prm 17076 | 13 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ;13 โ โ | ||
Theorem | 17prm 17077 | 17 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ;17 โ โ | ||
Theorem | 19prm 17078 | 19 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ;19 โ โ | ||
Theorem | 23prm 17079 | 23 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ;23 โ โ | ||
Theorem | prmlem2 17080 |
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 to cover the numbers less than
5โ2 = 25. 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 29โ2 = 841, 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 17096).
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.) |
โข ๐ โ โ & โข ๐ < ;;841 & โข 1 < ๐ & โข ยฌ 2 โฅ ๐ & โข ยฌ 3 โฅ ๐ & โข ยฌ 5 โฅ ๐ & โข ยฌ 7 โฅ ๐ & โข ยฌ ;11 โฅ ๐ & โข ยฌ ;13 โฅ ๐ & โข ยฌ ;17 โฅ ๐ & โข ยฌ ;19 โฅ ๐ & โข ยฌ ;23 โฅ ๐ โ โข ๐ โ โ | ||
Theorem | 37prm 17081 | 37 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;37 โ โ | ||
Theorem | 43prm 17082 | 43 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;43 โ โ | ||
Theorem | 83prm 17083 | 83 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;83 โ โ | ||
Theorem | 139prm 17084 | 139 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;;139 โ โ | ||
Theorem | 163prm 17085 | 163 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;;163 โ โ | ||
Theorem | 317prm 17086 | 317 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;;317 โ โ | ||
Theorem | 631prm 17087 | 631 is a prime number. (Contributed by Mario Carneiro, 1-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;;631 โ โ | ||
Theorem | prmo4 17088 | The primorial of 4. (Contributed by AV, 28-Aug-2020.) |
โข (#pโ4) = 6 | ||
Theorem | prmo5 17089 | The primorial of 5. (Contributed by AV, 28-Aug-2020.) |
โข (#pโ5) = ;30 | ||
Theorem | prmo6 17090 | The primorial of 6. (Contributed by AV, 28-Aug-2020.) |
โข (#pโ6) = ;30 | ||
Theorem | 1259lem1 17091 | Lemma for 1259prm 17096. Calculate a power mod. In decimal, we calculate 2โ16 = 52๐ + 68โก68 and 2โ17โก68 ยท 2 = 136 in this lemma. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.) |
โข ๐ = ;;;1259 โ โข ((2โ;17) mod ๐) = (;;136 mod ๐) | ||
Theorem | 1259lem2 17092 | Lemma for 1259prm 17096. Calculate a power mod. In decimal, we calculate 2โ34 = (2โ17)โ2โก136โ2โก14๐ + 870. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.) |
โข ๐ = ;;;1259 โ โข ((2โ;34) mod ๐) = (;;870 mod ๐) | ||
Theorem | 1259lem3 17093 | Lemma for 1259prm 17096. Calculate a power mod. In decimal, we calculate 2โ38 = 2โ34 ยท 2โ4โก870 ยท 16 = 11๐ + 71 and 2โ76 = (2โ34)โ2โก71โ2 = 4๐ + 5โก5. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.) |
โข ๐ = ;;;1259 โ โข ((2โ;76) mod ๐) = (5 mod ๐) | ||
Theorem | 1259lem4 17094 | Lemma for 1259prm 17096. Calculate a power mod. In decimal, we calculate 2โ306 = (2โ76)โ4 ยท 4โก5โ4 ยท 4 = 2๐ โ 18, 2โ612 = (2โ306)โ2โก18โ2 = 324, 2โ629 = 2โ612 ยท 2โ17โก324 ยท 136 = 35๐ โ 1 and finally 2โ(๐ โ 1) = (2โ629)โ2โก1โ2 = 1. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.) |
โข ๐ = ;;;1259 โ โข ((2โ(๐ โ 1)) mod ๐) = (1 mod ๐) | ||
Theorem | 1259lem5 17095 | Lemma for 1259prm 17096. Calculate the GCD of 2โ34 โ 1โก869 with ๐ = 1259. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ๐ = ;;;1259 โ โข (((2โ;34) โ 1) gcd ๐) = 1 | ||
Theorem | 1259prm 17096 | 1259 is a prime number. (Contributed by Mario Carneiro, 22-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ๐ = ;;;1259 โ โข ๐ โ โ | ||
Theorem | 2503lem1 17097 | Lemma for 2503prm 17100. Calculate a power mod. In decimal, we calculate 2โ18 = 512โ2 = 104๐ + 1832โก1832. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.) |
โข ๐ = ;;;2503 โ โข ((2โ;18) mod ๐) = (;;;1832 mod ๐) | ||
Theorem | 2503lem2 17098 | Lemma for 2503prm 17100. Calculate a power mod. We calculate 2โ19 = 2โ18 ยท 2โก1832 ยท 2 = ๐ + 1161, 2โ38 = (2โ19)โ2โก1161โ2 = 538๐ + 1307, 2โ39 = 2โ38 ยท 2โก1307 ยท 2 = ๐ + 111, 2โ78 = (2โ39)โ2โก111โ2 = 5๐ โ 194, 2โ156 = (2โ78)โ2โก194โ2 = 15๐ + 91, 2โ312 = (2โ156)โ2โก91โ2 = 3๐ + 772, 2โ624 = (2โ312)โ2โก772โ2 = 238๐ + 270, 2โ1248 = (2โ624)โ2โก270โ2 = 29๐ + 313, 2โ1251 = 2โ1248 ยท 8โก313 ยท 8 = ๐ + 1 and finally 2โ(๐ โ 1) = (2โ1251)โ2โก1โ2 = 1. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.) |
โข ๐ = ;;;2503 โ โข ((2โ(๐ โ 1)) mod ๐) = (1 mod ๐) | ||
Theorem | 2503lem3 17099 | Lemma for 2503prm 17100. Calculate the GCD of 2โ18 โ 1โก1831 with ๐ = 2503. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.) |
โข ๐ = ;;;2503 โ โข (((2โ;18) โ 1) gcd ๐) = 1 | ||
Theorem | 2503prm 17100 | 2503 is a prime number. (Contributed by Mario Carneiro, 3-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ๐ = ;;;2503 โ โข ๐ โ โ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |