P. 168 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16701-16800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	vdwlem10 16701*	Lemma for vdw 16705. Set up secondary induction on 𝑀. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(⟨𝑀, 𝐾⟩ PolyAP 𝑓 ∨ (𝐾 + 1) MonoAP 𝑓))
Theorem	vdwlem11 16702*	Lemma for vdw 16705. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(𝐾 + 1) MonoAP 𝑓)
Theorem	vdwlem12 16703	Lemma for vdw 16705. 𝐾 = 2 base case of induction. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:(1...((♯‘𝑅) + 1))⟶𝑅)    &   ⊢ (𝜑 → ¬ 2 MonoAP 𝐹)    ⇒   ⊢ ¬ 𝜑
Theorem	vdwlem13 16704*	Lemma for vdw 16705. Main induction on 𝐾; 𝐾 = 0, 𝐾 = 1 base cases. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))𝐾 MonoAP 𝑓)
Theorem	vdw 16705*	Van der Waerden's theorem. For any finite coloring 𝑅 and integer 𝐾, there is an 𝑁 such that every coloring function from 1...𝑁 to 𝑅 contains a monochromatic arithmetic progression (which written out in full means that there is a color 𝑐 and base, increment values 𝑎, 𝑑 such that all the numbers 𝑎, 𝑎 + 𝑑, ..., 𝑎 + (𝑘 − 1)𝑑 lie in the preimage of {𝑐}, i.e. they are all in 1...𝑁 and 𝑓 evaluated at each one yields 𝑐). (Contributed by Mario Carneiro, 13-Sep-2014.)
⊢ ((𝑅 ∈ Fin ∧ 𝐾 ∈ ℕ0) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝑓 “ {𝑐}))
Theorem	vdwnnlem1 16706*	Corollary of vdw 16705, and lemma for vdwnn 16709. If 𝐹 is a coloring of the integers, then there are arbitrarily long monochromatic APs in 𝐹. (Contributed by Mario Carneiro, 13-Sep-2014.)
⊢ ((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅 ∧ 𝐾 ∈ ℕ0) → ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))
Theorem	vdwnnlem2 16707*	Lemma for vdwnn 16709. The set of all "bad" 𝑘 for the theorem is upwards-closed, because a long AP implies a short AP. (Contributed by Mario Carneiro, 13-Sep-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑅)    &   ⊢ 𝑆 = {𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})}    ⇒   ⊢ ((𝜑 ∧ 𝐵 ∈ (ℤ≥‘𝐴)) → (𝐴 ∈ 𝑆 → 𝐵 ∈ 𝑆))
Theorem	vdwnnlem3 16708*	Lemma for vdwnn 16709. (Contributed by Mario Carneiro, 13-Sep-2014.) (Proof shortened by AV, 27-Sep-2020.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑅)    &   ⊢ 𝑆 = {𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})}    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝑅 𝑆 ≠ ∅)    ⇒   ⊢ ¬ 𝜑
Theorem	vdwnn 16709*	Van der Waerden's theorem, infinitary version. For any finite coloring 𝐹 of the positive integers, there is a color 𝑐 that contains arbitrarily long arithmetic progressions. (Contributed by Mario Carneiro, 13-Sep-2014.)
⊢ ((𝑅 ∈ Fin ∧ 𝐹:ℕ⟶𝑅) → ∃𝑐 ∈ 𝑅 ∀𝑘 ∈ ℕ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))
6.2.14  Ramsey's theorem
Syntax	cram 16710	Extend class notation with the Ramsey number function.
class Ramsey
Theorem	ramtlecl 16711*	The set 𝑇 of numbers with the Ramsey number property is upward-closed. (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → 𝜑)}    ⇒   ⊢ (𝑀 ∈ 𝑇 → (ℤ≥‘𝑀) ⊆ 𝑇)
Definition	df-ram 16712*	Define the Ramsey number function. The input is a number 𝑚 for the size of the edges of the hypergraph, and a tuple 𝑟 from the finite color set to lower bounds for each color. The Ramsey number (𝑀 Ramsey 𝑅) is the smallest number such that for any set 𝑆 with (𝑀 Ramsey 𝑅) ≤ ♯𝑆 and any coloring 𝐹 of the set of 𝑀-element subsets of 𝑆 (with color set dom 𝑅), there is a color 𝑐 ∈ dom 𝑅 and a subset 𝑥 ⊆ 𝑆 such that 𝑅(𝑐) ≤ ♯𝑥 and all the hyperedges of 𝑥 (that is, subsets of 𝑥 of size 𝑀) have color 𝑐. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
⊢ Ramsey = (𝑚 ∈ ℕ0, 𝑟 ∈ V ↦ inf({𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (dom 𝑟 ↑m {𝑦 ∈ 𝒫 𝑠 ∣ (♯‘𝑦) = 𝑚})∃𝑐 ∈ dom 𝑟∃𝑥 ∈ 𝒫 𝑠((𝑟‘𝑐) ≤ (♯‘𝑥) ∧ ∀𝑦 ∈ 𝒫 𝑥((♯‘𝑦) = 𝑚 → (𝑓‘𝑦) = 𝑐)))}, ℝ*, < ))
Theorem	hashbcval 16713*	Value of the "binomial set", the set of all 𝑁-element subsets of 𝐴. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐴𝐶𝑁) = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑁})
Theorem	hashbccl 16714*	The binomial set is a finite set. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0) → (𝐴𝐶𝑁) ∈ Fin)
Theorem	hashbcss 16715*	Subset relation for the binomial set. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0) → (𝐵𝐶𝑁) ⊆ (𝐴𝐶𝑁))
Theorem	hashbc0 16716*	The set of subsets of size zero is the singleton of the empty set. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐴𝐶0) = {∅})
Theorem	hashbc2 16717*	The size of the binomial set is the binomial coefficient. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0) → (♯‘(𝐴𝐶𝑁)) = ((♯‘𝐴)C𝑁))
Theorem	0hashbc 16718*	There are no subsets of the empty set with size greater than zero. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ (𝑁 ∈ ℕ → (∅𝐶𝑁) = ∅)
Theorem	ramval 16719*	The value of the Ramsey number function. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by AV, 14-Sep-2020.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))}    ⇒   ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) = inf(𝑇, ℝ*, < ))
Theorem	ramcl2lem 16720*	Lemma for extended real closure of the Ramsey number function. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))}    ⇒   ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) = if(𝑇 = ∅, +∞, inf(𝑇, ℝ, < )))
Theorem	ramtcl 16721*	The Ramsey number has the Ramsey number property if any number does. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))}    ⇒   ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → ((𝑀 Ramsey 𝐹) ∈ 𝑇 ↔ 𝑇 ≠ ∅))
Theorem	ramtcl2 16722*	The Ramsey number is an integer iff there is a number with the Ramsey number property. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))}    ⇒   ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → ((𝑀 Ramsey 𝐹) ∈ ℕ0 ↔ 𝑇 ≠ ∅))
Theorem	ramtub 16723*	The Ramsey number is a lower bound on the set of all numbers with the Ramsey number property. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))}    ⇒   ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ 𝐴 ∈ 𝑇) → (𝑀 Ramsey 𝐹) ≤ 𝐴)
Theorem	ramub 16724*	The Ramsey number is a lower bound on the set of all numbers with the Ramsey number property. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑅⟶ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ (𝑁 ≤ (♯‘𝑠) ∧ 𝑓:(𝑠𝐶𝑀)⟶𝑅)) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))    ⇒   ⊢ (𝜑 → (𝑀 Ramsey 𝐹) ≤ 𝑁)
Theorem	ramub2 16725*	It is sufficient to check the Ramsey property on finite sets of size equal to the upper bound. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑅⟶ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ ((𝜑 ∧ ((♯‘𝑠) = 𝑁 ∧ 𝑓:(𝑠𝐶𝑀)⟶𝑅)) → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))    ⇒   ⊢ (𝜑 → (𝑀 Ramsey 𝐹) ≤ 𝑁)
Theorem	rami 16726*	The defining property of a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑅⟶ℕ0)    &   ⊢ (𝜑 → (𝑀 Ramsey 𝐹) ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑀 Ramsey 𝐹) ≤ (♯‘𝑆))    &   ⊢ (𝜑 → 𝐺:(𝑆𝐶𝑀)⟶𝑅)    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐})))
Theorem	ramcl2 16727	The Ramsey number is either a nonnegative integer or plus infinity. (Contributed by Mario Carneiro, 20-Apr-2015.) (Revised by AV, 14-Sep-2020.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) ∈ (ℕ0 ∪ {+∞}))
Theorem	ramxrcl 16728	The Ramsey number is an extended real number. (This theorem does not imply Ramsey's theorem, unlike ramcl 16740.) (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) ∈ ℝ*)
Theorem	ramubcl 16729	If the Ramsey number is upper bounded, then it is an integer. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝐴 ∈ ℕ0 ∧ (𝑀 Ramsey 𝐹) ≤ 𝐴)) → (𝑀 Ramsey 𝐹) ∈ ℕ0)
Theorem	ramlb 16730*	Establish a lower bound on a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑅⟶ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐺:((1...𝑁)𝐶𝑀)⟶𝑅)    &   ⊢ ((𝜑 ∧ (𝑐 ∈ 𝑅 ∧ 𝑥 ⊆ (1...𝑁))) → ((𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐}) → (♯‘𝑥) < (𝐹‘𝑐)))    ⇒   ⊢ (𝜑 → 𝑁 < (𝑀 Ramsey 𝐹))
Theorem	0ram 16731*	The Ramsey number when 𝑀 = 0. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → (0 Ramsey 𝐹) = sup(ran 𝐹, ℝ, < ))
Theorem	0ram2 16732	The Ramsey number when 𝑀 = 0. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → (0 Ramsey 𝐹) = sup(ran 𝐹, ℝ, < ))
Theorem	ram0 16733	The Ramsey number when 𝑅 = ∅. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ (𝑀 ∈ ℕ0 → (𝑀 Ramsey ∅) = 𝑀)
Theorem	0ramcl 16734	Lemma for ramcl 16740: Existence of the Ramsey number when 𝑀 = 0. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) → (0 Ramsey 𝐹) ∈ ℕ0)
Theorem	ramz2 16735	The Ramsey number when 𝐹 has value zero for some color 𝐶. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝐶 ∈ 𝑅 ∧ (𝐹‘𝐶) = 0)) → (𝑀 Ramsey 𝐹) = 0)
Theorem	ramz 16736	The Ramsey number when 𝐹 is the zero function. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)
Theorem	ramub1lem1 16737*	Lemma for ramub1 16739. (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 16738*	Lemma for ramub1 16739. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝑅⟶ℕ)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦)))))    &   ⊢ (𝜑 → 𝐺:𝑅⟶ℕ0)    &   ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℕ0)    &   ⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → (♯‘𝑆) = (((𝑀 − 1) Ramsey 𝐺) + 1))    &   ⊢ (𝜑 → 𝐾:(𝑆𝐶𝑀)⟶𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (◡𝐾 “ {𝑐})))
Theorem	ramub1 16739*	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 16740	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 16741*	Ramsey's theorem with the definition of Ramsey (df-ram 16712) 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 16742	Extend class notation to include the primorial of nonnegative integers.
class #p
Definition	df-prmo 16743*	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 28831). In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 26337, 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 16744*	Value of the primorial function for nonnegative integers. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1))
Theorem	prmocl 16745	Closure of the primorial function. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ∈ ℕ)
Theorem	prmone0 16746	The primorial function is nonzero. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ≠ 0)
Theorem	prmo0 16747	The primorial of 0. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘0) = 1
Theorem	prmo1 16748	The primorial of 1. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘1) = 1
Theorem	prmop1 16749	The primorial of a successor. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘(𝑁 + 1)) = if((𝑁 + 1) ∈ ℙ, ((#p‘𝑁) · (𝑁 + 1)), (#p‘𝑁)))
Theorem	prmonn2 16750	Value of the primorial function expressed recursively. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ → (#p‘𝑁) = if(𝑁 ∈ ℙ, ((#p‘(𝑁 − 1)) · 𝑁), (#p‘(𝑁 − 1))))
Theorem	prmo2 16751	The primorial of 2. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘2) = 2
Theorem	prmo3 16752	The primorial of 3. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘3) = 6
Theorem	prmdvdsprmo 16753*	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 16754*	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 16755*	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 16756*	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 16757	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 16758	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 16759	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 16770. Instead of using the factorial of n (see df-fac 13998), 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 16771, or the primorial n# (the product of all prime numbers less than or equal to n), see prmgapprmo 16773, are such functions, which provide smaller values than the factorial function (see lcmflefac 16363 and prmolefac 16757 resp. prmolelcmf 16759): "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 16760	Lemma for prmgap 16770: 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 16761	Lemma for prmgap 16770: 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 16762	Lemma for prmgaplcm 16771: 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 16763	Lemma for prmgaplcm 16771: 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 16764*	Lemma for prmgap 16770. (Contributed by AV, 9-Aug-2020.)
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁}    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘3) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)
Theorem	prmgaplem4 16765*	Lemma for prmgap 16770. (Contributed by AV, 10-Aug-2020.)
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)}    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	prmgaplem5 16766*	Lemma for prmgap 16770: 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 16767*	Lemma for prmgap 16770: 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 16768*	Lemma for prmgap 16770. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m ℕ))    &   ⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
Theorem	prmgaplem8 16769*	Lemma for prmgap 16770. (Contributed by AV, 13-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m ℕ))    &   ⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖))    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑁 ≤ (𝑞 − 𝑝) ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ))
Theorem	prmgap 16770*	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 16771*	Alternate proof of prmgap 16770: in contrast to prmgap 16770, 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 16772	Lemma for prmgapprmo 16773: 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 16773*	Alternate proof of prmgap 16770: in contrast to prmgap 16770, 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 16774	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    &   ⊢ 𝐷 = (𝐶 + 1)    ⇒   ⊢ ¬ 2 ∥ ;𝐴𝐷
Theorem	dec5dvds 16775	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐵
Theorem	dec5dvds2 16776	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    &   ⊢ (5 + 𝐵) = 𝐶    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐶
Theorem	dec5nprm 16777	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ ¬ ;𝐴5 ∈ ℙ
Theorem	dec2nprm 16778	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    ⇒   ⊢ ¬ ;𝐴𝐶 ∈ ℙ
Theorem	modxai 16779	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 16780	Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (2 · 𝐵) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modxp1i 16781	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 16782	Version of mod2xi 16780 with a negative mod value. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝐿 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐿 mod 𝑁)    &   ⊢ (2 · 𝐵) = 𝐸    &   ⊢ (𝐿 + 𝐾) = 𝑁    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modsubi 16783	Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝐴 mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (𝑀 + 𝐵) = 𝐾    ⇒   ⊢ ((𝐴 − 𝐵) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	gcdi 16784	Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ (𝑁 gcd 𝑅) = 𝐺    &   ⊢ ((𝐾 · 𝑁) + 𝑅) = 𝑀    ⇒   ⊢ (𝑀 gcd 𝑁) = 𝐺
Theorem	gcdmodi 16785	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 16786	Calculate a power of two. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 2) = 𝑁    ⇒   ⊢ ((4 · (2↑𝑀)) + 0) = (2↑𝑁)
Theorem	numexp0 16787	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑0) = 1
Theorem	numexp1 16788	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑1) = 𝐴
Theorem	numexpp1 16789	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 1) = 𝑁    &   ⊢ ((𝐴↑𝑀) · 𝐴) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	numexp2x 16790	Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (2 · 𝑀) = 𝑁    &   ⊢ (𝐴↑𝑀) = 𝐷    &   ⊢ (𝐷 · 𝐷) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	decsplit0b 16791	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 16792	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 16793	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 16794	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 16795	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 12512. (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 16796	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑4) = ;16
Theorem	2exp5 16797	Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑5) = ;32
Theorem	2exp6 16798	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 16799	Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑7) = ;;128
Theorem	2exp8 16800	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑8) = ;;256