P. 171 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17001-17100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0ramcl 17001	Lemma for ramcl 17007: Existence of the Ramsey number when 𝑀 = 0. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) → (0 Ramsey 𝐹) ∈ ℕ0)
Theorem	ramz2 17002	The Ramsey number when 𝐹 has value zero for some color 𝐶. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝐶 ∈ 𝑅 ∧ (𝐹‘𝐶) = 0)) → (𝑀 Ramsey 𝐹) = 0)
Theorem	ramz 17003	The Ramsey number when 𝐹 is the zero function. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)
Theorem	ramub1lem1 17004*	Lemma for ramub1 17006. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝑅⟶ℕ)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦)))))    &   ⊢ (𝜑 → 𝐺:𝑅⟶ℕ0)    &   ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℕ0)    &   ⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → (♯‘𝑆) = (((𝑀 − 1) Ramsey 𝐺) + 1))    &   ⊢ (𝜑 → 𝐾:(𝑆𝐶𝑀)⟶𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑊 ⊆ (𝑆 ∖ {𝑋}))    &   ⊢ (𝜑 → (𝐺‘𝐷) ≤ (♯‘𝑊))    &   ⊢ (𝜑 → (𝑊𝐶(𝑀 − 1)) ⊆ (◡𝐻 “ {𝐷}))    &   ⊢ (𝜑 → 𝐸 ∈ 𝑅)    &   ⊢ (𝜑 → 𝑉 ⊆ 𝑊)    &   ⊢ (𝜑 → if(𝐸 = 𝐷, ((𝐹‘𝐷) − 1), (𝐹‘𝐸)) ≤ (♯‘𝑉))    &   ⊢ (𝜑 → (𝑉𝐶𝑀) ⊆ (◡𝐾 “ {𝐸}))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝐸) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (◡𝐾 “ {𝐸})))
Theorem	ramub1lem2 17005*	Lemma for ramub1 17006. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝑅⟶ℕ)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦)))))    &   ⊢ (𝜑 → 𝐺:𝑅⟶ℕ0)    &   ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℕ0)    &   ⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → (♯‘𝑆) = (((𝑀 − 1) Ramsey 𝐺) + 1))    &   ⊢ (𝜑 → 𝐾:(𝑆𝐶𝑀)⟶𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (◡𝐾 “ {𝑐})))
Theorem	ramub1 17006*	Inductive step for Ramsey's theorem, in the form of an explicit upper bound. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝑅⟶ℕ)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦)))))    &   ⊢ (𝜑 → 𝐺:𝑅⟶ℕ0)    &   ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑀 Ramsey 𝐹) ≤ (((𝑀 − 1) Ramsey 𝐺) + 1))
Theorem	ramcl 17007	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 17008*	Ramsey's theorem with the definition of Ramsey (df-ram 16979) 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 (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐}))))
6.2.15  Primorial function 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 17009	Extend class notation to include the primorial of nonnegative integers.
class #p
Definition	df-prmo 17010*	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 30395). In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 27095, 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 17011*	Value of the primorial function for nonnegative integers. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1))
Theorem	prmocl 17012	Closure of the primorial function. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ∈ ℕ)
Theorem	prmone0 17013	The primorial function is nonzero. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ≠ 0)
Theorem	prmo0 17014	The primorial of 0. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘0) = 1
Theorem	prmo1 17015	The primorial of 1. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘1) = 1
Theorem	prmop1 17016	The primorial of a successor. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘(𝑁 + 1)) = if((𝑁 + 1) ∈ ℙ, ((#p‘𝑁) · (𝑁 + 1)), (#p‘𝑁)))
Theorem	prmonn2 17017	Value of the primorial function expressed recursively. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ → (#p‘𝑁) = if(𝑁 ∈ ℙ, ((#p‘(𝑁 − 1)) · 𝑁), (#p‘(𝑁 − 1))))
Theorem	prmo2 17018	The primorial of 2. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘2) = 2
Theorem	prmo3 17019	The primorial of 3. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘3) = 6
Theorem	prmdvdsprmo 17020*	The primorial of a number is divisible by each prime less than or equal to the number. (Contributed by AV, 15-Aug-2020.) (Revised by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ → ∀𝑝 ∈ ℙ (𝑝 ≤ 𝑁 → 𝑝 ∥ (#p‘𝑁)))
Theorem	prmdvdsprmop 17021*	The primorial of a number plus an integer greater than 1 and less than or equal to the number is divisible by a prime less than or equal to the number. (Contributed by AV, 15-Aug-2020.) (Revised by AV, 28-Aug-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (2...𝑁)) → ∃𝑝 ∈ ℙ (𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼 ∧ 𝑝 ∥ ((#p‘𝑁) + 𝐼)))
Theorem	fvprmselelfz 17022*	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 17023*	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 17024	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 17025	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 17026	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...𝑁)))
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 17037. Instead of using the factorial of n (see df-fac 14246), 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 17038, or the primorial n# (the product of all prime numbers less than or equal to n), see prmgapprmo 17040, are such functions, which provide smaller values than the factorial function (see lcmflefac 16625 and prmolefac 17024 resp. prmolelcmf 17026): "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 17027	Lemma for prmgap 17037: The factorial of a number plus an integer greater than 1 and less than or equal to the number is divisible by that integer. (Contributed by AV, 13-Aug-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (2...𝑁)) → 𝐼 ∥ ((!‘𝑁) + 𝐼))
Theorem	prmgaplem2 17028	Lemma for prmgap 17037: The factorial of a number plus an integer greater than 1 and less than or equal to the number are not coprime. (Contributed by AV, 13-Aug-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (2...𝑁)) → 1 < (((!‘𝑁) + 𝐼) gcd 𝐼))
Theorem	prmgaplcmlem1 17029	Lemma for prmgaplcm 17038: The least common multiple of all positive integers less than or equal to a number plus an integer greater than 1 and less than 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 17030	Lemma for prmgaplcm 17038: The least common multiple of all positive integers less than or equal to a number plus an integer greater than 1 and less than 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 17031*	Lemma for prmgap 17037. (Contributed by AV, 9-Aug-2020.)
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁}    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘3) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
Theorem	prmgaplem4 17032*	Lemma for prmgap 17037. (Contributed by AV, 10-Aug-2020.)
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)}    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	prmgaplem5 17033*	Lemma for prmgap 17037: 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 17034*	Lemma for prmgap 17037: 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 17035*	Lemma for prmgap 17037. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m ℕ))    &   ⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
Theorem	prmgaplem8 17036*	Lemma for prmgap 17037. (Contributed by AV, 13-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m ℕ))    &   ⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑁 ≤ (𝑞 − 𝑝) ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
Theorem	prmgap 17037*	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 17038*	Alternate proof of prmgap 17037: in contrast to prmgap 17037, 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 17039	Lemma for prmgapprmo 17040: The primorial of a number plus an integer greater than 1 and less than 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 17040*	Alternate proof of prmgap 17037: in contrast to prmgap 17037, 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)..^𝑞)𝑧 ∉ ℙ)
6.2.17  Decimal arithmetic (cont.)
Theorem	dec2dvds 17041	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    &   ⊢ 𝐷 = (𝐶 + 1)    ⇒   ⊢ ¬ 2 ∥ ;𝐴𝐷
Theorem	dec5dvds 17042	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐵
Theorem	dec5dvds2 17043	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    &   ⊢ (5 + 𝐵) = 𝐶    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐶
Theorem	dec5nprm 17044	A decimal number greater than 10 and ending with five is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ ¬ ;𝐴5 ∈ ℙ
Theorem	dec2nprm 17045	A decimal number greater than 10 and ending with an even digit is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    ⇒   ⊢ ¬ ;𝐴𝐶 ∈ ℙ
Theorem	modxai 17046	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 17047	Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (2 · 𝐵) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modxp1i 17048	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 17049	Version of mod2xi 17047 with a negative mod value. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝐿 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐿 mod 𝑁)    &   ⊢ (2 · 𝐵) = 𝐸    &   ⊢ (𝐿 + 𝐾) = 𝑁    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modsubi 17050	Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝐴 mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (𝑀 + 𝐵) = 𝐾    ⇒   ⊢ ((𝐴 − 𝐵) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	gcdi 17051	Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ (𝑁 gcd 𝑅) = 𝐺    &   ⊢ ((𝐾 · 𝑁) + 𝑅) = 𝑀    ⇒   ⊢ (𝑀 gcd 𝑁) = 𝐺
Theorem	gcdmodi 17052	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	numexp0 17053	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑0) = 1
Theorem	numexp1 17054	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑1) = 𝐴
Theorem	numexpp1 17055	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 1) = 𝑁    &   ⊢ ((𝐴↑𝑀) · 𝐴) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	numexp2x 17056	Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (2 · 𝑀) = 𝑁    &   ⊢ (𝐴↑𝑀) = 𝐷    &   ⊢ (𝐷 · 𝐷) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	decsplit0b 17057	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 17058	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 17059	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 17060	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 17061	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 12721. (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 17062	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑4) = ;16
Theorem	2exp5 17063	Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑5) = ;32
Theorem	2exp6 17064	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 17065	Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑7) = ;;128
Theorem	2exp8 17066	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑8) = ;;256
Theorem	2exp11 17067	Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑;11) = ;;;2048
Theorem	2exp16 17068	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑;16) = ;;;;65536
Theorem	3exp3 17069	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (3↑3) = ;27
Theorem	2expltfac 17070	The factorial grows faster than two to the power 𝑁. (Contributed by Mario Carneiro, 15-Sep-2016.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (2↑𝑁) < (!‘𝑁))
6.2.18  Cyclical shifts of words (cont.)
Theorem	cshwsidrepsw 17071	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 17072	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 17073*	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 17074*	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 17075*	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 17076*	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 17077*	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 17078*	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 17079*	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 17080*	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 17081*	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 17082*	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))
6.2.19  Specific prime numbers
Theorem	prmlem0 17083*	Lemma for prmlem1 17085 and prmlem2 17097. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ((¬ 2 ∥ 𝑀 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))    &   ⊢ (𝐾 ∈ ℙ → ¬ 𝐾 ∥ 𝑁)    &   ⊢ (𝐾 + 2) = 𝑀    ⇒   ⊢ ((¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
Theorem	prmlem1a 17084*	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 17085	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 17086	5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 5 ∈ ℙ
Theorem	6nprm 17087	6 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 6 ∈ ℙ
Theorem	7prm 17088	7 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 7 ∈ ℙ
Theorem	8nprm 17089	8 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 8 ∈ ℙ
Theorem	9nprm 17090	9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 9 ∈ ℙ
Theorem	10nprm 17091	10 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ ¬ ;10 ∈ ℙ
Theorem	11prm 17092	11 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;11 ∈ ℙ
Theorem	13prm 17093	13 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;13 ∈ ℙ
Theorem	17prm 17094	17 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;17 ∈ ℙ
Theorem	19prm 17095	19 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;19 ∈ ℙ
Theorem	23prm 17096	23 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;23 ∈ ℙ
Theorem	prmlem2 17097	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 17113). 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 17098	37 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;37 ∈ ℙ
Theorem	43prm 17099	43 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;43 ∈ ℙ
Theorem	83prm 17100	83 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;83 ∈ ℙ