P. 170 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16901-17000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gzabssqcl 16901	The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → ((abs‘𝐴)↑2) ∈ ℕ0)
Theorem	4sqlem5 16902	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ))
Theorem	4sqlem6 16903	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2)))
Theorem	4sqlem7 16904	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (𝐵↑2) ≤ (((𝑀↑2) / 2) / 2))
Theorem	4sqlem8 16905	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐵↑2)))
Theorem	4sqlem9 16906	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (𝐴↑2))
Theorem	4sqlem10 16907	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ ((𝜑 ∧ 𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))
Theorem	4sqlem1 16908*	Lemma for 4sq 16924. The set 𝑆 is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that 𝑆 = ℕ0; here we show one subset direction. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ 𝑆 ⊆ ℕ0
Theorem	4sqlem2 16909*	Lemma for 4sq 16924. Change bound variables in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
Theorem	4sqlem3 16910*	Lemma for 4sq 16924. Sufficient condition to be in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) ∈ 𝑆)
Theorem	4sqlem4a 16911*	Lemma for 4sqlem4 16912. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ 𝑆)
Theorem	4sqlem4 16912*	Lemma for 4sq 16924. We can express the four-square property more compactly in terms of gaussian integers, because the norms of gaussian integers are exactly sums of two squares. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2)))
Theorem	mul4sqlem 16913*	Lemma for mul4sq 16914: algebraic manipulations. The extra assumptions involving 𝑀 are for a part of 4sqlem17 16921 which needs to know not just that the product is a sum of squares, but also that it preserves divisibility by 𝑀. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ[i])    &   ⊢ (𝜑 → 𝐵 ∈ ℤ[i])    &   ⊢ (𝜑 → 𝐶 ∈ ℤ[i])    &   ⊢ (𝜑 → 𝐷 ∈ ℤ[i])    &   ⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2))    &   ⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i])    &   ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i])    &   ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆)
Theorem	mul4sq 16914*	Euler's four-square identity: The product of two sums of four squares is also a sum of four squares. This is usually quoted as an explicit formula involving eight real variables; we save some time by working with complex numbers (gaussian integers) instead, so that we only have to work with four variables, and also hiding the actual formula for the product in the proof of mul4sqlem 16913. (For the curious, the explicit formula that is used is ( ∣ 𝑎 ∣ ↑2 + ∣ 𝑏 ∣ ↑2)( ∣ 𝑐 ∣ ↑2 + ∣ 𝑑 ∣ ↑2) = ∣ 𝑎∗ · 𝑐 + 𝑏 · 𝑑∗ ∣ ↑2 + ∣ 𝑎∗ · 𝑑 − 𝑏 · 𝑐∗ ∣ ↑2.) (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 · 𝐵) ∈ 𝑆)
Theorem	4sqlem11 16915*	Lemma for 4sq 16924. Use the pigeonhole principle to show that the sets {𝑚↑2 ∣ 𝑚 ∈ (0...𝑁)} and {-1 − 𝑛↑2 ∣ 𝑛 ∈ (0...𝑁)} have a common element, mod 𝑃. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   ⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅)
Theorem	4sqlem12 16916*	Lemma for 4sq 16924. For any odd prime 𝑃, there is a 𝑘 < 𝑃 such that 𝑘𝑃 − 1 is a sum of two squares. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))
Theorem	4sqlem13 16917*	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    ⇒   ⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))
Theorem	4sqlem14 16918*	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)    &   ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))    ⇒   ⊢ (𝜑 → 𝑅 ∈ ℕ0)
Theorem	4sqlem15 16919*	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)    &   ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))    ⇒   ⊢ ((𝜑 ∧ 𝑅 = 𝑀) → ((((((𝑀↑2) / 2) / 2) − (𝐸↑2)) = 0 ∧ ((((𝑀↑2) / 2) / 2) − (𝐹↑2)) = 0) ∧ (((((𝑀↑2) / 2) / 2) − (𝐺↑2)) = 0 ∧ ((((𝑀↑2) / 2) / 2) − (𝐻↑2)) = 0)))
Theorem	4sqlem16 16920*	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)    &   ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))    ⇒   ⊢ (𝜑 → (𝑅 ≤ 𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
Theorem	4sqlem17 16921*	Lemma for 4sq 16924. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)    &   ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))    ⇒   ⊢ ¬ 𝜑
Theorem	4sqlem18 16922*	Lemma for 4sq 16924. Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝑆)
Theorem	4sqlem19 16923*	Lemma for 4sq 16924. The proof is by strong induction - we show that if all the integers less than 𝑘 are in 𝑆, then 𝑘 is as well. In this part of the proof we do the induction argument and dispense with all the cases except the odd prime case, which is sent to 4sqlem18 16922. If 𝑘 is 0, 1, 2, we show 𝑘 ∈ 𝑆 directly; otherwise if 𝑘 is composite, 𝑘 is the product of two numbers less than it (and hence in 𝑆 by assumption), so by mul4sq 16914 𝑘 ∈ 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ℕ0 = 𝑆
Theorem	4sq 16924*	Lagrange's four-square theorem, or Bachet's conjecture: every nonnegative integer is expressible as a sum of four squares. This is Metamath 100 proof #19. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝐴 ∈ ℕ0 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
6.2.13  Van der Waerden's theorem
Syntax	cvdwa 16925	The arithmetic progression function.
class AP
Syntax	cvdwm 16926	The monochromatic arithmetic progression predicate.
class MonoAP
Syntax	cvdwp 16927	The polychromatic arithmetic progression predicate.
class PolyAP
Definition	df-vdwap 16928*	Define the arithmetic progression function, which takes as input a length 𝑘, a start point 𝑎, and a step 𝑑 and outputs the set of points in this progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ AP = (𝑘 ∈ ℕ0 ↦ (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝑘 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))
Definition	df-vdwmc 16929*	Define the "contains a monochromatic AP" predicate. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ MonoAP = {⟨𝑘, 𝑓⟩ ∣ ∃𝑐(ran (AP‘𝑘) ∩ 𝒫 (◡𝑓 “ {𝑐})) ≠ ∅}
Definition	df-vdwpc 16930*	Define the "contains a polychromatic collection of APs" predicate. See vdwpc 16940 for more information. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ PolyAP = {⟨⟨𝑚, 𝑘⟩, 𝑓⟩ ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)}
Theorem	vdwapfval 16931*	Define the arithmetic progression function, which takes as input a length 𝑘, a start point 𝑎, and a step 𝑑 and outputs the set of points in this progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ (𝐾 ∈ ℕ0 → (AP‘𝐾) = (𝑎 ∈ ℕ, 𝑑 ∈ ℕ ↦ ran (𝑚 ∈ (0...(𝐾 − 1)) ↦ (𝑎 + (𝑚 · 𝑑)))))
Theorem	vdwapf 16932	The arithmetic progression function is a function. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ (𝐾 ∈ ℕ0 → (AP‘𝐾):(ℕ × ℕ)⟶𝒫 ℕ)
Theorem	vdwapval 16933*	Value of the arithmetic progression function. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑋 ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑋 = (𝐴 + (𝑚 · 𝐷))))
Theorem	vdwapun 16934	Remove the first element of an arithmetic progression. (Contributed by Mario Carneiro, 11-Sep-2014.)
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴(AP‘(𝐾 + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘𝐾)𝐷)))
Theorem	vdwapid1 16935	The first element of an arithmetic progression. (Contributed by Mario Carneiro, 12-Sep-2014.)
⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷))
Theorem	vdwap0 16936	Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴(AP‘0)𝐷) = ∅)
Theorem	vdwap1 16937	Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴(AP‘1)𝐷) = {𝐴})
Theorem	vdwmc 16938*	The predicate " The ⟨𝑅, 𝑁⟩-coloring 𝐹 contains a monochromatic AP of length 𝐾". (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ 𝑋 ∈ V    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑅)    ⇒   ⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐})))
Theorem	vdwmc2 16939*	Expand out the definition of an arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ 𝑋 ∈ V    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})))
Theorem	vdwpc 16940*	The predicate " The coloring 𝐹 contains a polychromatic 𝑀-tuple of AP's of length 𝐾". A polychromatic 𝑀-tuple of AP's is a set of AP's with the same base point but different step lengths, such that each individual AP is monochromatic, but the AP's all have mutually distinct colors. (The common basepoint is not required to have the same color as any of the AP's.) (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ 𝑋 ∈ V    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑅)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐽 = (1...𝑀)    ⇒   ⊢ (𝜑 → (⟨𝑀, 𝐾⟩ PolyAP 𝐹 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m 𝐽)(∀𝑖 ∈ 𝐽 ((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ 𝐽 ↦ (𝐹‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)))
Theorem	vdwlem1 16941*	Lemma for vdw 16954. (Contributed by Mario Carneiro, 12-Sep-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑊)⟶𝑅)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷:(1...𝑀)⟶ℕ)    &   ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}))    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑀))    &   ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘(𝐴 + (𝐷‘𝐼))))    ⇒   ⊢ (𝜑 → (𝐾 + 1) MonoAP 𝐹)
Theorem	vdwlem2 16942*	Lemma for vdw 16954. (Contributed by Mario Carneiro, 12-Sep-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑊 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝑅)    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑊 + 𝑁)))    &   ⊢ 𝐺 = (𝑥 ∈ (1...𝑊) ↦ (𝐹‘(𝑥 + 𝑁)))    ⇒   ⊢ (𝜑 → (𝐾 MonoAP 𝐺 → 𝐾 MonoAP 𝐹))
Theorem	vdwlem3 16943	Lemma for vdw 16954. (Contributed by Mario Carneiro, 13-Sep-2014.)
⊢ (𝜑 → 𝑉 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ (1...𝑉))    &   ⊢ (𝜑 → 𝐵 ∈ (1...𝑊))    ⇒   ⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))))
Theorem	vdwlem4 16944*	Lemma for vdw 16954. (Contributed by Mario Carneiro, 12-Sep-2014.)
⊢ (𝜑 → 𝑉 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))    ⇒   ⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑m (1...𝑊)))
Theorem	vdwlem5 16945*	Lemma for vdw 16954. (Contributed by Mario Carneiro, 12-Sep-2014.)
⊢ (𝜑 → 𝑉 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐺}))    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐸:(1...𝑀)⟶ℕ)    &   ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))    &   ⊢ 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸‘𝑖))))    &   ⊢ (𝜑 → (♯‘ran 𝐽) = 𝑀)    &   ⊢ 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)))    &   ⊢ 𝑃 = (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)))    ⇒   ⊢ (𝜑 → 𝑇 ∈ ℕ)
Theorem	vdwlem6 16946*	Lemma for vdw 16954. (Contributed by Mario Carneiro, 13-Sep-2014.)
⊢ (𝜑 → 𝑉 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐺}))    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐸:(1...𝑀)⟶ℕ)    &   ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))    &   ⊢ 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸‘𝑖))))    &   ⊢ (𝜑 → (♯‘ran 𝐽) = 𝑀)    &   ⊢ 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)))    &   ⊢ 𝑃 = (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)))    ⇒   ⊢ (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))
Theorem	vdwlem7 16947*	Lemma for vdw 16954. (Contributed by Mario Carneiro, 12-Sep-2014.)
⊢ (𝜑 → 𝑉 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐺}))    ⇒   ⊢ (𝜑 → (⟨𝑀, 𝐾⟩ PolyAP 𝐺 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺)))
Theorem	vdwlem8 16948*	Lemma for vdw 16954. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝑊 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...(2 · 𝑊))⟶𝑅)    &   ⊢ 𝐶 ∈ V    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐺 “ {𝐶}))    &   ⊢ 𝐺 = (𝑥 ∈ (1...𝑊) ↦ (𝐹‘(𝑥 + 𝑊)))    ⇒   ⊢ (𝜑 → ⟨1, 𝐾⟩ PolyAP 𝐹)
Theorem	vdwlem9 16949*	Lemma for vdw 16954. (Contributed by Mario Carneiro, 12-Sep-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑊 ∈ ℕ)    &   ⊢ (𝜑 → ∀𝑔 ∈ (𝑅 ↑m (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))    &   ⊢ (𝜑 → 𝑉 ∈ ℕ)    &   ⊢ (𝜑 → ∀𝑓 ∈ ((𝑅 ↑m (1...𝑊)) ↑m (1...𝑉))𝐾 MonoAP 𝑓)    &   ⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))    ⇒   ⊢ (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))
Theorem	vdwlem10 16950*	Lemma for vdw 16954. 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 16951*	Lemma for vdw 16954. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(𝐾 + 1) MonoAP 𝑓)
Theorem	vdwlem12 16952	Lemma for vdw 16954. 𝐾 = 2 base case of induction. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:(1...((♯‘𝑅) + 1))⟶𝑅)    &   ⊢ (𝜑 → ¬ 2 MonoAP 𝐹)    ⇒   ⊢ ¬ 𝜑
Theorem	vdwlem13 16953*	Lemma for vdw 16954. Main induction on 𝐾; 𝐾 = 0, 𝐾 = 1 base cases. (Contributed by Mario Carneiro, 18-Aug-2014.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))𝐾 MonoAP 𝑓)
Theorem	vdw 16954*	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 16955*	Corollary of vdw 16954, and lemma for vdwnn 16958. 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 16956*	Lemma for vdwnn 16958. 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 16957*	Lemma for vdwnn 16958. (Contributed by Mario Carneiro, 13-Sep-2014.) (Proof shortened by AV, 27-Sep-2020.)
⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑅)    &   ⊢ 𝑆 = {𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})}    &   ⊢ (𝜑 → ∀𝑐 ∈ 𝑅 𝑆 ≠ ∅)    ⇒   ⊢ ¬ 𝜑
Theorem	vdwnn 16958*	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 16959	Extend class notation with the Ramsey number function.
class Ramsey
Theorem	ramtlecl 16960*	The set 𝑇 of numbers with the Ramsey number property is upward-closed. (Contributed by Mario Carneiro, 21-Apr-2015.)
⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → 𝜑)}    ⇒   ⊢ (𝑀 ∈ 𝑇 → (ℤ≥‘𝑀) ⊆ 𝑇)
Definition	df-ram 16961*	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 16962*	Value of the "binomial set", the set of all 𝑁-element subsets of 𝐴. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐴𝐶𝑁) = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑁})
Theorem	hashbccl 16963*	The binomial set is a finite set. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0) → (𝐴𝐶𝑁) ∈ Fin)
Theorem	hashbcss 16964*	Subset relation for the binomial set. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0) → (𝐵𝐶𝑁) ⊆ (𝐴𝐶𝑁))
Theorem	hashbc0 16965*	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 16966*	The size of the binomial set is the binomial coefficient. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0) → (♯‘(𝐴𝐶𝑁)) = ((♯‘𝐴)C𝑁))
Theorem	0hashbc 16967*	There are no subsets of the empty set with size greater than zero. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    ⇒   ⊢ (𝑁 ∈ ℕ → (∅𝐶𝑁) = ∅)
Theorem	ramval 16968*	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 16969*	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 16970*	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 16971*	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 16972*	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 16973*	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 16974*	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 16975*	The defining property of a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑅⟶ℕ0)    &   ⊢ (𝜑 → (𝑀 Ramsey 𝐹) ∈ ℕ0)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑀 Ramsey 𝐹) ≤ (♯‘𝑆))    &   ⊢ (𝜑 → 𝐺:(𝑆𝐶𝑀)⟶𝑅)    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐})))
Theorem	ramcl2 16976	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 16977	The Ramsey number is an extended real number. (This theorem does not imply Ramsey's theorem, unlike ramcl 16989.) (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) ∈ ℝ*)
Theorem	ramubcl 16978	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 16979*	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 16980*	The Ramsey number when 𝑀 = 0. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → (0 Ramsey 𝐹) = sup(ran 𝐹, ℝ, < ))
Theorem	0ram2 16981	The Ramsey number when 𝑀 = 0. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → (0 Ramsey 𝐹) = sup(ran 𝐹, ℝ, < ))
Theorem	ram0 16982	The Ramsey number when 𝑅 = ∅. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ (𝑀 ∈ ℕ0 → (𝑀 Ramsey ∅) = 𝑀)
Theorem	0ramcl 16983	Lemma for ramcl 16989: Existence of the Ramsey number when 𝑀 = 0. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) → (0 Ramsey 𝐹) ∈ ℕ0)
Theorem	ramz2 16984	The Ramsey number when 𝐹 has value zero for some color 𝐶. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝐶 ∈ 𝑅 ∧ (𝐹‘𝐶) = 0)) → (𝑀 Ramsey 𝐹) = 0)
Theorem	ramz 16985	The Ramsey number when 𝐹 is the zero function. (Contributed by Mario Carneiro, 22-Apr-2015.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0)
Theorem	ramub1lem1 16986*	Lemma for ramub1 16988. (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 16987*	Lemma for ramub1 16988. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝑅⟶ℕ)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦)))))    &   ⊢ (𝜑 → 𝐺:𝑅⟶ℕ0)    &   ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℕ0)    &   ⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖})    &   ⊢ (𝜑 → 𝑆 ∈ Fin)    &   ⊢ (𝜑 → (♯‘𝑆) = (((𝑀 − 1) Ramsey 𝐺) + 1))    &   ⊢ (𝜑 → 𝐾:(𝑆𝐶𝑀)⟶𝑅)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋})))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (◡𝐾 “ {𝑐})))
Theorem	ramub1 16988*	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 16989	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 16990*	Ramsey's theorem with the definition of Ramsey (df-ram 16961) 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 16991	Extend class notation to include the primorial of nonnegative integers.
class #p
Definition	df-prmo 16992*	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 30517). In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 27129, 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 16993*	Value of the primorial function for nonnegative integers. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1))
Theorem	prmocl 16994	Closure of the primorial function. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ∈ ℕ)
Theorem	prmone0 16995	The primorial function is nonzero. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ≠ 0)
Theorem	prmo0 16996	The primorial of 0. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘0) = 1
Theorem	prmo1 16997	The primorial of 1. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘1) = 1
Theorem	prmop1 16998	The primorial of a successor. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ0 → (#p‘(𝑁 + 1)) = if((𝑁 + 1) ∈ ℙ, ((#p‘𝑁) · (𝑁 + 1)), (#p‘𝑁)))
Theorem	prmonn2 16999	Value of the primorial function expressed recursively. (Contributed by AV, 28-Aug-2020.)
⊢ (𝑁 ∈ ℕ → (#p‘𝑁) = if(𝑁 ∈ ℙ, ((#p‘(𝑁 − 1)) · 𝑁), (#p‘(𝑁 − 1))))
Theorem	prmo2 17000	The primorial of 2. (Contributed by AV, 28-Aug-2020.)
⊢ (#p‘2) = 2