![]() |
Metamath
Proof Explorer Theorem List (p. 171 of 485) | < 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-30800) |
![]() (30801-32323) |
![]() (32324-48421) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ramcl 17001 | 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.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) ∈ ℕ0) | ||
Theorem | ramsey 17002* | Ramsey's theorem with the definition of Ramsey (df-ram 16973) eliminated. If 𝑀 is an integer, 𝑅 is a specified finite set of colors, and 𝐹:𝑅⟶ℕ0 is a set of lower bounds for each color, then there is an 𝑛 such that for every set 𝑠 of size greater than 𝑛 and every coloring 𝑓 of the set (𝑠𝐶𝑀) of all 𝑀-element subsets of 𝑠, there is a color 𝑐 and a subset 𝑥 ⊆ 𝑠 such that 𝑥 is larger than 𝐹(𝑐) and the 𝑀 -element subsets of 𝑥 are monochromatic with color 𝑐. This is the hypergraph version of Ramsey's theorem; the version for simple graphs is the case 𝑀 = 2. This is Metamath 100 proof #31. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) ⇒ ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) → ∃𝑛 ∈ ℕ0 ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) | ||
According to Wikipedia "Primorial", https://en.wikipedia.org/wiki/Primorial (28-Aug-2020): "In mathematics, and more particularly in number theory, primorial, denoted by "#", is a function from natural numbers to natural numbers similar to the factorial function, but rather than successively multiplying [all] positive integers [less than or equal to a given number], the function only multiplies [the] prime numbers [less than or equal to the given number]. The name "primorial", coined by Harvey Dubner, draws an analogy to primes similar to the way the name "factorial" relates to factors." | ||
Syntax | cprmo 17003 | Extend class notation to include the primorial of nonnegative integers. |
class #p | ||
Definition | df-prmo 17004* |
Define the primorial function on nonnegative integers as the product of
all prime numbers less than or equal to the integer. For example,
(#p‘10) = 2 · 3 · 5
· 7 = 210 (see ex-prmo 30341).
In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 27155, where the primorial function is defined by using the sequence builder (𝑃 = seq1( · , 𝐹)), the more specialized definition of a product of a series is used here. (Contributed by AV, 28-Aug-2020.) |
⊢ #p = (𝑛 ∈ ℕ0 ↦ ∏𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, 𝑘, 1)) | ||
Theorem | prmoval 17005* | Value of the primorial function for nonnegative integers. (Contributed by AV, 28-Aug-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) | ||
Theorem | prmocl 17006 | Closure of the primorial function. (Contributed by AV, 28-Aug-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ∈ ℕ) | ||
Theorem | prmone0 17007 | The primorial function is nonzero. (Contributed by AV, 28-Aug-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ≠ 0) | ||
Theorem | prmo0 17008 | The primorial of 0. (Contributed by AV, 28-Aug-2020.) |
⊢ (#p‘0) = 1 | ||
Theorem | prmo1 17009 | The primorial of 1. (Contributed by AV, 28-Aug-2020.) |
⊢ (#p‘1) = 1 | ||
Theorem | prmop1 17010 | The primorial of a successor. (Contributed by AV, 28-Aug-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#p‘(𝑁 + 1)) = if((𝑁 + 1) ∈ ℙ, ((#p‘𝑁) · (𝑁 + 1)), (#p‘𝑁))) | ||
Theorem | prmonn2 17011 | Value of the primorial function expressed recursively. (Contributed by AV, 28-Aug-2020.) |
⊢ (𝑁 ∈ ℕ → (#p‘𝑁) = if(𝑁 ∈ ℙ, ((#p‘(𝑁 − 1)) · 𝑁), (#p‘(𝑁 − 1)))) | ||
Theorem | prmo2 17012 | The primorial of 2. (Contributed by AV, 28-Aug-2020.) |
⊢ (#p‘2) = 2 | ||
Theorem | prmo3 17013 | The primorial of 3. (Contributed by AV, 28-Aug-2020.) |
⊢ (#p‘3) = 6 | ||
Theorem | prmdvdsprmo 17014* | 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 17015* | 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 17016* | 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 17017* | 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 17018 | 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 17019 | 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 17020 | 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 17031. Instead of using the factorial of n (see df-fac 14269), 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 17032, or the primorial n# (the product of all prime numbers less than or equal to n), see prmgapprmo 17034, are such functions, which provide smaller values than the factorial function (see lcmflefac 16622 and prmolefac 17018 resp. prmolelcmf 17020): "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 17021 | Lemma for prmgap 17031: 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 17022 | Lemma for prmgap 17031: 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 17023 | Lemma for prmgaplcm 17032: 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 17024 | Lemma for prmgaplcm 17032: 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 17025* | Lemma for prmgap 17031. (Contributed by AV, 9-Aug-2020.) |
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⇒ ⊢ (𝑁 ∈ (ℤ≥‘3) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) | ||
Theorem | prmgaplem4 17026* | Lemma for prmgap 17031. (Contributed by AV, 10-Aug-2020.) |
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | prmgaplem5 17027* | Lemma for prmgap 17031: 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 17028* | Lemma for prmgap 17031: 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 17029* | Lemma for prmgap 17031. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m ℕ)) & ⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖)) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) | ||
Theorem | prmgaplem8 17030* | Lemma for prmgap 17031. (Contributed by AV, 13-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m ℕ)) & ⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖)) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑁 ≤ (𝑞 − 𝑝) ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) | ||
Theorem | prmgap 17031* | 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 17032* | Alternate proof of prmgap 17031: in contrast to prmgap 17031, 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 17033 | Lemma for prmgapprmo 17034: 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 17034* | Alternate proof of prmgap 17031: in contrast to prmgap 17031, 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 17035 | Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ (𝐵 · 2) = 𝐶 & ⊢ 𝐷 = (𝐶 + 1) ⇒ ⊢ ¬ 2 ∥ ;𝐴𝐷 | ||
Theorem | dec5dvds 17036 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐵 < 5 ⇒ ⊢ ¬ 5 ∥ ;𝐴𝐵 | ||
Theorem | dec5dvds2 17037 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐵 < 5 & ⊢ (5 + 𝐵) = 𝐶 ⇒ ⊢ ¬ 5 ∥ ;𝐴𝐶 | ||
Theorem | dec5nprm 17038 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ ¬ ;𝐴5 ∈ ℙ | ||
Theorem | dec2nprm 17039 | Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ (𝐵 · 2) = 𝐶 ⇒ ⊢ ¬ ;𝐴𝐶 ∈ ℙ | ||
Theorem | modxai 17040 | 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 17041 | Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) |
⊢ 𝑁 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁) & ⊢ (2 · 𝐵) = 𝐸 & ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾) ⇒ ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁) | ||
Theorem | modxp1i 17042 | 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 17043 | Version of mod2xi 17041 with a negative mod value. (Contributed by Mario Carneiro, 21-Feb-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐾 ∈ ℕ & ⊢ 𝑀 ∈ ℕ0 & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐿 mod 𝑁) & ⊢ (2 · 𝐵) = 𝐸 & ⊢ (𝐿 + 𝐾) = 𝑁 & ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾) ⇒ ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁) | ||
Theorem | modsubi 17044 | Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑁 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ (𝐴 mod 𝑁) = (𝐾 mod 𝑁) & ⊢ (𝑀 + 𝐵) = 𝐾 ⇒ ⊢ ((𝐴 − 𝐵) mod 𝑁) = (𝑀 mod 𝑁) | ||
Theorem | gcdi 17045 | Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.) |
⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑅 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ (𝑁 gcd 𝑅) = 𝐺 & ⊢ ((𝐾 · 𝑁) + 𝑅) = 𝑀 ⇒ ⊢ (𝑀 gcd 𝑁) = 𝐺 | ||
Theorem | gcdmodi 17046 | 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 17047 | Calculate a power of two. (Contributed by Mario Carneiro, 19-Feb-2014.) |
⊢ 𝑀 ∈ ℕ0 & ⊢ (𝑀 + 2) = 𝑁 ⇒ ⊢ ((4 · (2↑𝑀)) + 0) = (2↑𝑁) | ||
Theorem | numexp0 17048 | Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (𝐴↑0) = 1 | ||
Theorem | numexp1 17049 | Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (𝐴↑1) = 𝐴 | ||
Theorem | numexpp1 17050 | Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ (𝑀 + 1) = 𝑁 & ⊢ ((𝐴↑𝑀) · 𝐴) = 𝐶 ⇒ ⊢ (𝐴↑𝑁) = 𝐶 | ||
Theorem | numexp2x 17051 | Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ (2 · 𝑀) = 𝑁 & ⊢ (𝐴↑𝑀) = 𝐷 & ⊢ (𝐷 · 𝐷) = 𝐶 ⇒ ⊢ (𝐴↑𝑁) = 𝐶 | ||
Theorem | decsplit0b 17052 | 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 17053 | 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 17054 | 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 17055 | 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 17056 | 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 12775. (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 17057 | Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.) |
⊢ (2↑4) = ;16 | ||
Theorem | 2exp5 17058 | Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑5) = ;32 | ||
Theorem | 2exp6 17059 | 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 17060 | Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑7) = ;;128 | ||
Theorem | 2exp8 17061 | Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.) |
⊢ (2↑8) = ;;256 | ||
Theorem | 2exp11 17062 | Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑;11) = ;;;2048 | ||
Theorem | 2exp16 17063 | Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.) |
⊢ (2↑;16) = ;;;;65536 | ||
Theorem | 3exp3 17064 | Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.) |
⊢ (3↑3) = ;27 | ||
Theorem | 2expltfac 17065 | The factorial grows faster than two to the power 𝑁. (Contributed by Mario Carneiro, 15-Sep-2016.) |
⊢ (𝑁 ∈ (ℤ≥‘4) → (2↑𝑁) < (!‘𝑁)) | ||
Theorem | cshwsidrepsw 17066 | 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 17067 | 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 17068* | 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 17069* | 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 17070* | 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 17071* | 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 17072* | 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 17073* | 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 17074* | 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 17075* | 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 17076* | 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 17077* | 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 17078* | Lemma for prmlem1 17080 and prmlem2 17092. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ ((¬ 2 ∥ 𝑀 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) & ⊢ (𝐾 ∈ ℙ → ¬ 𝐾 ∥ 𝑁) & ⊢ (𝐾 + 2) = 𝑀 ⇒ ⊢ ((¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) | ||
Theorem | prmlem1a 17079* | 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 17080 | 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 17081 | 5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
⊢ 5 ∈ ℙ | ||
Theorem | 6nprm 17082 | 6 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ ¬ 6 ∈ ℙ | ||
Theorem | 7prm 17083 | 7 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
⊢ 7 ∈ ℙ | ||
Theorem | 8nprm 17084 | 8 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ ¬ 8 ∈ ℙ | ||
Theorem | 9nprm 17085 | 9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ ¬ 9 ∈ ℙ | ||
Theorem | 10nprm 17086 | 10 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
⊢ ¬ ;10 ∈ ℙ | ||
Theorem | 11prm 17087 | 11 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
⊢ ;11 ∈ ℙ | ||
Theorem | 13prm 17088 | 13 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
⊢ ;13 ∈ ℙ | ||
Theorem | 17prm 17089 | 17 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
⊢ ;17 ∈ ℙ | ||
Theorem | 19prm 17090 | 19 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
⊢ ;19 ∈ ℙ | ||
Theorem | 23prm 17091 | 23 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) |
⊢ ;23 ∈ ℙ | ||
Theorem | prmlem2 17092 |
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 17108).
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 17093 | 37 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
⊢ ;37 ∈ ℙ | ||
Theorem | 43prm 17094 | 43 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
⊢ ;43 ∈ ℙ | ||
Theorem | 83prm 17095 | 83 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
⊢ ;83 ∈ ℙ | ||
Theorem | 139prm 17096 | 139 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
⊢ ;;139 ∈ ℙ | ||
Theorem | 163prm 17097 | 163 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
⊢ ;;163 ∈ ℙ | ||
Theorem | 317prm 17098 | 317 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
⊢ ;;317 ∈ ℙ | ||
Theorem | 631prm 17099 | 631 is a prime number. (Contributed by Mario Carneiro, 1-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.) |
⊢ ;;631 ∈ ℙ | ||
Theorem | prmo4 17100 | The primorial of 4. (Contributed by AV, 28-Aug-2020.) |
⊢ (#p‘4) = 6 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |