![]() |
Metamath
Proof Explorer Theorem List (p. 171 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | prmop1 17001 | The primorial of a successor. (Contributed by AV, 28-Aug-2020.) |
โข (๐ โ โ0 โ (#pโ(๐ + 1)) = if((๐ + 1) โ โ, ((#pโ๐) ยท (๐ + 1)), (#pโ๐))) | ||
Theorem | prmonn2 17002 | Value of the primorial function expressed recursively. (Contributed by AV, 28-Aug-2020.) |
โข (๐ โ โ โ (#pโ๐) = if(๐ โ โ, ((#pโ(๐ โ 1)) ยท ๐), (#pโ(๐ โ 1)))) | ||
Theorem | prmo2 17003 | The primorial of 2. (Contributed by AV, 28-Aug-2020.) |
โข (#pโ2) = 2 | ||
Theorem | prmo3 17004 | The primorial of 3. (Contributed by AV, 28-Aug-2020.) |
โข (#pโ3) = 6 | ||
Theorem | prmdvdsprmo 17005* | 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 17006* | 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 17007* | 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 17008* | 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 17009 | 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 17010 | 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 17011 | 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 17022. Instead of using the factorial of n (see df-fac 14260), 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 17023, or the primorial n# (the product of all prime numbers less than or equal to n), see prmgapprmo 17025, are such functions, which provide smaller values than the factorial function (see lcmflefac 16613 and prmolefac 17009 resp. prmolelcmf 17011): "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 17012 | Lemma for prmgap 17022: 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 17013 | Lemma for prmgap 17022: 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 17014 | Lemma for prmgaplcm 17023: 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 17015 | Lemma for prmgaplcm 17023: 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 17016* | Lemma for prmgap 17022. (Contributed by AV, 9-Aug-2020.) |
โข ๐ด = {๐ โ โ โฃ ๐ < ๐} โ โข (๐ โ (โคโฅโ3) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) | ||
Theorem | prmgaplem4 17017* | Lemma for prmgap 17022. (Contributed by AV, 10-Aug-2020.) |
โข ๐ด = {๐ โ โ โฃ (๐ < ๐ โง ๐ โค ๐)} โ โข ((๐ โ โ โง ๐ โ โ โง ๐ < ๐) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) | ||
Theorem | prmgaplem5 17018* | Lemma for prmgap 17022: 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 17019* | Lemma for prmgap 17022: 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 17020* | Lemma for prmgap 17022. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐น โ (โ โm โ)) & โข (๐ โ โ๐ โ (2...๐)1 < (((๐นโ๐) + ๐) gcd ๐)) โ โข (๐ โ โ๐ โ โ โ๐ โ โ (๐ < ((๐นโ๐) + 2) โง ((๐นโ๐) + ๐) < ๐ โง โ๐ง โ ((๐ + 1)..^๐)๐ง โ โ)) | ||
Theorem | prmgaplem8 17021* | Lemma for prmgap 17022. (Contributed by AV, 13-Aug-2020.) |
โข (๐ โ ๐ โ โ) & โข (๐ โ ๐น โ (โ โm โ)) & โข (๐ โ โ๐ โ (2...๐)1 < (((๐นโ๐) + ๐) gcd ๐)) โ โข (๐ โ โ๐ โ โ โ๐ โ โ (๐ โค (๐ โ ๐) โง โ๐ง โ ((๐ + 1)..^๐)๐ง โ โ)) | ||
Theorem | prmgap 17022* | 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 17023* | Alternate proof of prmgap 17022: in contrast to prmgap 17022, 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 17024 | Lemma for prmgapprmo 17025: 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 17025* | Alternate proof of prmgap 17022: in contrast to prmgap 17022, 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 17026 | Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข (๐ต ยท 2) = ๐ถ & โข ๐ท = (๐ถ + 1) โ โข ยฌ 2 โฅ ;๐ด๐ท | ||
Theorem | dec5dvds 17027 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ต โ โ & โข ๐ต < 5 โ โข ยฌ 5 โฅ ;๐ด๐ต | ||
Theorem | dec5dvds2 17028 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ต โ โ & โข ๐ต < 5 & โข (5 + ๐ต) = ๐ถ โ โข ยฌ 5 โฅ ;๐ด๐ถ | ||
Theorem | dec5nprm 17029 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ โ โข ยฌ ;๐ด5 โ โ | ||
Theorem | dec2nprm 17030 | Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
โข ๐ด โ โ & โข ๐ต โ โ0 & โข (๐ต ยท 2) = ๐ถ โ โข ยฌ ;๐ด๐ถ โ โ | ||
Theorem | modxai 17031 | 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 17032 | Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) |
โข ๐ โ โ & โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ท โ โค & โข ๐พ โ โ0 & โข ๐ โ โ0 & โข ((๐ดโ๐ต) mod ๐) = (๐พ mod ๐) & โข (2 ยท ๐ต) = ๐ธ & โข ((๐ท ยท ๐) + ๐) = (๐พ ยท ๐พ) โ โข ((๐ดโ๐ธ) mod ๐) = (๐ mod ๐) | ||
Theorem | modxp1i 17033 | 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 17034 | Version of mod2xi 17032 with a negative mod value. (Contributed by Mario Carneiro, 21-Feb-2014.) |
โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ท โ โค & โข ๐พ โ โ & โข ๐ โ โ0 & โข ๐ฟ โ โ0 & โข ((๐ดโ๐ต) mod ๐) = (๐ฟ mod ๐) & โข (2 ยท ๐ต) = ๐ธ & โข (๐ฟ + ๐พ) = ๐ & โข ((๐ท ยท ๐) + ๐) = (๐พ ยท ๐พ) โ โข ((๐ดโ๐ธ) mod ๐) = (๐ mod ๐) | ||
Theorem | modsubi 17035 | Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ๐ โ โ & โข ๐ด โ โ & โข ๐ต โ โ0 & โข ๐ โ โ0 & โข (๐ด mod ๐) = (๐พ mod ๐) & โข (๐ + ๐ต) = ๐พ โ โข ((๐ด โ ๐ต) mod ๐) = (๐ mod ๐) | ||
Theorem | gcdi 17036 | Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.) |
โข ๐พ โ โ0 & โข ๐ โ โ0 & โข ๐ โ โ0 & โข (๐ gcd ๐ ) = ๐บ & โข ((๐พ ยท ๐) + ๐ ) = ๐ โ โข (๐ gcd ๐) = ๐บ | ||
Theorem | gcdmodi 17037 | 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 17038 | Calculate a power of two. (Contributed by Mario Carneiro, 19-Feb-2014.) |
โข ๐ โ โ0 & โข (๐ + 2) = ๐ โ โข ((4 ยท (2โ๐)) + 0) = (2โ๐) | ||
Theorem | numexp0 17039 | Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
โข ๐ด โ โ0 โ โข (๐ดโ0) = 1 | ||
Theorem | numexp1 17040 | Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
โข ๐ด โ โ0 โ โข (๐ดโ1) = ๐ด | ||
Theorem | numexpp1 17041 | Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ โ โ0 & โข (๐ + 1) = ๐ & โข ((๐ดโ๐) ยท ๐ด) = ๐ถ โ โข (๐ดโ๐) = ๐ถ | ||
Theorem | numexp2x 17042 | Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
โข ๐ด โ โ0 & โข ๐ โ โ0 & โข (2 ยท ๐) = ๐ & โข (๐ดโ๐) = ๐ท & โข (๐ท ยท ๐ท) = ๐ถ โ โข (๐ดโ๐) = ๐ถ | ||
Theorem | decsplit0b 17043 | 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 17044 | 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 17045 | 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 17046 | 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 17047 | 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 12767. (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 17048 | Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.) |
โข (2โ4) = ;16 | ||
Theorem | 2exp5 17049 | Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.) |
โข (2โ5) = ;32 | ||
Theorem | 2exp6 17050 | 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 17051 | Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.) |
โข (2โ7) = ;;128 | ||
Theorem | 2exp8 17052 | Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.) |
โข (2โ8) = ;;256 | ||
Theorem | 2exp11 17053 | Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.) |
โข (2โ;11) = ;;;2048 | ||
Theorem | 2exp16 17054 | Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.) |
โข (2โ;16) = ;;;;65536 | ||
Theorem | 3exp3 17055 | Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.) |
โข (3โ3) = ;27 | ||
Theorem | 2expltfac 17056 | The factorial grows faster than two to the power ๐. (Contributed by Mario Carneiro, 15-Sep-2016.) |
โข (๐ โ (โคโฅโ4) โ (2โ๐) < (!โ๐)) | ||
Theorem | cshwsidrepsw 17057 | 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 17058 | 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 17059* | 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 17060* | 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 17061* | 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 17062* | 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 17063* | 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 17064* | 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 17065* | 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 17066* | 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 17067* | 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 17068* | 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 17069* | Lemma for prmlem1 17071 and prmlem2 17083. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ((ยฌ 2 โฅ ๐ โง ๐ฅ โ (โคโฅโ๐)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) & โข (๐พ โ โ โ ยฌ ๐พ โฅ ๐) & โข (๐พ + 2) = ๐ โ โข ((ยฌ 2 โฅ ๐พ โง ๐ฅ โ (โคโฅโ๐พ)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) | ||
Theorem | prmlem1a 17070* | 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 17071 | 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 17072 | 5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข 5 โ โ | ||
Theorem | 6nprm 17073 | 6 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ยฌ 6 โ โ | ||
Theorem | 7prm 17074 | 7 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข 7 โ โ | ||
Theorem | 8nprm 17075 | 8 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ยฌ 8 โ โ | ||
Theorem | 9nprm 17076 | 9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ยฌ 9 โ โ | ||
Theorem | 10nprm 17077 | 10 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
โข ยฌ ;10 โ โ | ||
Theorem | 11prm 17078 | 11 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ;11 โ โ | ||
Theorem | 13prm 17079 | 13 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ;13 โ โ | ||
Theorem | 17prm 17080 | 17 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ;17 โ โ | ||
Theorem | 19prm 17081 | 19 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ;19 โ โ | ||
Theorem | 23prm 17082 | 23 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
โข ;23 โ โ | ||
Theorem | prmlem2 17083 |
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 17099).
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 17084 | 37 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;37 โ โ | ||
Theorem | 43prm 17085 | 43 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;43 โ โ | ||
Theorem | 83prm 17086 | 83 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;83 โ โ | ||
Theorem | 139prm 17087 | 139 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;;139 โ โ | ||
Theorem | 163prm 17088 | 163 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;;163 โ โ | ||
Theorem | 317prm 17089 | 317 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;;317 โ โ | ||
Theorem | 631prm 17090 | 631 is a prime number. (Contributed by Mario Carneiro, 1-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ;;631 โ โ | ||
Theorem | prmo4 17091 | The primorial of 4. (Contributed by AV, 28-Aug-2020.) |
โข (#pโ4) = 6 | ||
Theorem | prmo5 17092 | The primorial of 5. (Contributed by AV, 28-Aug-2020.) |
โข (#pโ5) = ;30 | ||
Theorem | prmo6 17093 | The primorial of 6. (Contributed by AV, 28-Aug-2020.) |
โข (#pโ6) = ;30 | ||
Theorem | 1259lem1 17094 | Lemma for 1259prm 17099. 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 17095 | Lemma for 1259prm 17099. 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 17096 | Lemma for 1259prm 17099. 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 17097 | Lemma for 1259prm 17099. 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 17098 | Lemma for 1259prm 17099. 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 17099 | 1259 is a prime number. (Contributed by Mario Carneiro, 22-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
โข ๐ = ;;;1259 โ โข ๐ โ โ | ||
Theorem | 2503lem1 17100 | Lemma for 2503prm 17103. 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 ๐) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |