Home | Metamath
Proof Explorer Theorem List (p. 164 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vdwapid1 16301 | The first element of an arithmetic progression. (Contributed by Mario Carneiro, 12-Sep-2014.) |
⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷)) | ||
Theorem | vdwap0 16302 | Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴(AP‘0)𝐷) = ∅) | ||
Theorem | vdwap1 16303 | Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴(AP‘1)𝐷) = {𝐴}) | ||
Theorem | vdwmc 16304* | The predicate " The 〈𝑅, 𝑁〉-coloring 𝐹 contains a monochromatic AP of length 𝐾". (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ 𝑋 ∈ V & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑅) ⇒ ⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑐}))) | ||
Theorem | vdwmc2 16305* | Expand out the definition of an arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ 𝑋 ∈ V & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑅) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑐 ∈ 𝑅 ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝐾 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐}))) | ||
Theorem | vdwpc 16306* | 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 16307* | Lemma for vdw 16320. (Contributed by Mario Carneiro, 12-Sep-2014.) |
⊢ (𝜑 → 𝑅 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑊)⟶𝑅) & ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐷:(1...𝑀)⟶ℕ) & ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))})) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑀)) & ⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘(𝐴 + (𝐷‘𝐼)))) ⇒ ⊢ (𝜑 → (𝐾 + 1) MonoAP 𝐹) | ||
Theorem | vdwlem2 16308* | Lemma for vdw 16320. (Contributed by Mario Carneiro, 12-Sep-2014.) |
⊢ (𝜑 → 𝑅 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → 𝑊 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...𝑀)⟶𝑅) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑊 + 𝑁))) & ⊢ 𝐺 = (𝑥 ∈ (1...𝑊) ↦ (𝐹‘(𝑥 + 𝑁))) ⇒ ⊢ (𝜑 → (𝐾 MonoAP 𝐺 → 𝐾 MonoAP 𝐹)) | ||
Theorem | vdwlem3 16309 | Lemma for vdw 16320. (Contributed by Mario Carneiro, 13-Sep-2014.) |
⊢ (𝜑 → 𝑉 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ (1...𝑉)) & ⊢ (𝜑 → 𝐵 ∈ (1...𝑊)) ⇒ ⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉)))) | ||
Theorem | vdwlem4 16310* | Lemma for vdw 16320. (Contributed by Mario Carneiro, 12-Sep-2014.) |
⊢ (𝜑 → 𝑉 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ Fin) & ⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) & ⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))))) ⇒ ⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑m (1...𝑊))) | ||
Theorem | vdwlem5 16311* | Lemma for vdw 16320. (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 16312* | Lemma for vdw 16320. (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 16313* | Lemma for vdw 16320. (Contributed by Mario Carneiro, 12-Sep-2014.) |
⊢ (𝜑 → 𝑉 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ Fin) & ⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) & ⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))))) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐺})) ⇒ ⊢ (𝜑 → (〈𝑀, 𝐾〉 PolyAP 𝐺 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))) | ||
Theorem | vdwlem8 16314* | Lemma for vdw 16320. (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ (𝜑 → 𝑅 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑊 ∈ ℕ) & ⊢ (𝜑 → 𝐹:(1...(2 · 𝑊))⟶𝑅) & ⊢ 𝐶 ∈ V & ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐺 “ {𝐶})) & ⊢ 𝐺 = (𝑥 ∈ (1...𝑊) ↦ (𝐹‘(𝑥 + 𝑊))) ⇒ ⊢ (𝜑 → 〈1, 𝐾〉 PolyAP 𝐹) | ||
Theorem | vdwlem9 16315* | Lemma for vdw 16320. (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 16316* | Lemma for vdw 16320. 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 16317* | Lemma for vdw 16320. (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ (𝜑 → 𝑅 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠 ↑m (1...𝑛))𝐾 MonoAP 𝑓) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))(𝐾 + 1) MonoAP 𝑓) | ||
Theorem | vdwlem12 16318 | Lemma for vdw 16320. 𝐾 = 2 base case of induction. (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ (𝜑 → 𝑅 ∈ Fin) & ⊢ (𝜑 → 𝐹:(1...((♯‘𝑅) + 1))⟶𝑅) & ⊢ (𝜑 → ¬ 2 MonoAP 𝐹) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | vdwlem13 16319* | Lemma for vdw 16320. Main induction on 𝐾; 𝐾 = 0, 𝐾 = 1 base cases. (Contributed by Mario Carneiro, 18-Aug-2014.) |
⊢ (𝜑 → 𝑅 ∈ Fin) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅 ↑m (1...𝑛))𝐾 MonoAP 𝑓) | ||
Theorem | vdw 16320* | 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 16321* | Corollary of vdw 16320, and lemma for vdwnn 16324. 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 16322* | Lemma for vdwnn 16324. 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 16323* | Lemma for vdwnn 16324. (Contributed by Mario Carneiro, 13-Sep-2014.) (Proof shortened by AV, 27-Sep-2020.) |
⊢ (𝜑 → 𝑅 ∈ Fin) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑅) & ⊢ 𝑆 = {𝑘 ∈ ℕ ∣ ¬ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ ∀𝑚 ∈ (0...(𝑘 − 1))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})} & ⊢ (𝜑 → ∀𝑐 ∈ 𝑅 𝑆 ≠ ∅) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | vdwnn 16324* | 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))(𝑎 + (𝑚 · 𝑑)) ∈ (◡𝐹 “ {𝑐})) | ||
Syntax | cram 16325 | Extend class notation with the Ramsey number function. |
class Ramsey | ||
Theorem | ramtlecl 16326* | The set 𝑇 of numbers with the Ramsey number property is upward-closed. (Contributed by Mario Carneiro, 21-Apr-2015.) |
⊢ 𝑇 = {𝑛 ∈ ℕ0 ∣ ∀𝑠(𝑛 ≤ (♯‘𝑠) → 𝜑)} ⇒ ⊢ (𝑀 ∈ 𝑇 → (ℤ≥‘𝑀) ⊆ 𝑇) | ||
Definition | df-ram 16327* | 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 16328* | Value of the "binomial set", the set of all 𝑁-element subsets of 𝐴. (Contributed by Mario Carneiro, 20-Apr-2015.) |
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐴𝐶𝑁) = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑁}) | ||
Theorem | hashbccl 16329* | The binomial set is a finite set. (Contributed by Mario Carneiro, 20-Apr-2015.) |
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) ⇒ ⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0) → (𝐴𝐶𝑁) ∈ Fin) | ||
Theorem | hashbcss 16330* | Subset relation for the binomial set. (Contributed by Mario Carneiro, 20-Apr-2015.) |
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑁 ∈ ℕ0) → (𝐵𝐶𝑁) ⊆ (𝐴𝐶𝑁)) | ||
Theorem | hashbc0 16331* | 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 16332* | The size of the binomial set is the binomial coefficient. (Contributed by Mario Carneiro, 20-Apr-2015.) |
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) ⇒ ⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ0) → (♯‘(𝐴𝐶𝑁)) = ((♯‘𝐴)C𝑁)) | ||
Theorem | 0hashbc 16333* | There are no subsets of the empty set with size greater than zero. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) ⇒ ⊢ (𝑁 ∈ ℕ → (∅𝐶𝑁) = ∅) | ||
Theorem | ramval 16334* | 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 16335* | 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 16336* | 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 16337* | 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 16338* | 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 16339* | 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 16340* | 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 16341* | The defining property of a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝑅⟶ℕ0) & ⊢ (𝜑 → (𝑀 Ramsey 𝐹) ∈ ℕ0) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → (𝑀 Ramsey 𝐹) ≤ (♯‘𝑆)) & ⊢ (𝜑 → 𝐺:(𝑆𝐶𝑀)⟶𝑅) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝐺 “ {𝑐}))) | ||
Theorem | ramcl2 16342 | 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 16343 | The Ramsey number is an extended real number. (This theorem does not imply Ramsey's theorem, unlike ramcl 16355.) (Contributed by Mario Carneiro, 20-Apr-2015.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) → (𝑀 Ramsey 𝐹) ∈ ℝ*) | ||
Theorem | ramubcl 16344 | 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 16345* | 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 16346* | The Ramsey number when 𝑀 = 0. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ ran 𝐹 𝑦 ≤ 𝑥) → (0 Ramsey 𝐹) = sup(ran 𝐹, ℝ, < )) | ||
Theorem | 0ram2 16347 | The Ramsey number when 𝑀 = 0. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ ((𝑅 ∈ Fin ∧ 𝑅 ≠ ∅ ∧ 𝐹:𝑅⟶ℕ0) → (0 Ramsey 𝐹) = sup(ran 𝐹, ℝ, < )) | ||
Theorem | ram0 16348 | The Ramsey number when 𝑅 = ∅. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ (𝑀 ∈ ℕ0 → (𝑀 Ramsey ∅) = 𝑀) | ||
Theorem | 0ramcl 16349 | Lemma for ramcl 16355: Existence of the Ramsey number when 𝑀 = 0. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ ((𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) → (0 Ramsey 𝐹) ∈ ℕ0) | ||
Theorem | ramz2 16350 | The Ramsey number when 𝐹 has value zero for some color 𝐶. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ (((𝑀 ∈ ℕ ∧ 𝑅 ∈ 𝑉 ∧ 𝐹:𝑅⟶ℕ0) ∧ (𝐶 ∈ 𝑅 ∧ (𝐹‘𝐶) = 0)) → (𝑀 Ramsey 𝐹) = 0) | ||
Theorem | ramz 16351 | The Ramsey number when 𝐹 is the zero function. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ 𝑉 ∧ 𝑅 ≠ ∅) → (𝑀 Ramsey (𝑅 × {0})) = 0) | ||
Theorem | ramub1lem1 16352* | Lemma for ramub1 16354. (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 16353* | Lemma for ramub1 16354. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝑅⟶ℕ) & ⊢ 𝐺 = (𝑥 ∈ 𝑅 ↦ (𝑀 Ramsey (𝑦 ∈ 𝑅 ↦ if(𝑦 = 𝑥, ((𝐹‘𝑥) − 1), (𝐹‘𝑦))))) & ⊢ (𝜑 → 𝐺:𝑅⟶ℕ0) & ⊢ (𝜑 → ((𝑀 − 1) Ramsey 𝐺) ∈ ℕ0) & ⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ (𝜑 → (♯‘𝑆) = (((𝑀 − 1) Ramsey 𝐺) + 1)) & ⊢ (𝜑 → 𝐾:(𝑆𝐶𝑀)⟶𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ 𝐻 = (𝑢 ∈ ((𝑆 ∖ {𝑋})𝐶(𝑀 − 1)) ↦ (𝐾‘(𝑢 ∪ {𝑋}))) ⇒ ⊢ (𝜑 → ∃𝑐 ∈ 𝑅 ∃𝑧 ∈ 𝒫 𝑆((𝐹‘𝑐) ≤ (♯‘𝑧) ∧ (𝑧𝐶𝑀) ⊆ (◡𝐾 “ {𝑐}))) | ||
Theorem | ramub1 16354* | 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 16355 | 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 16356* | Ramsey's theorem with the definition Ramsey eliminated. If 𝑀 is an integer, 𝑅 is a specified finite set of colors, and 𝐹:𝑅⟶ℕ0 is a set of lower bounds for each color, then there is an 𝑛 such that for every set 𝑠 of size greater than 𝑛 and every coloring 𝑓 of the set (𝑠𝐶𝑀) of all 𝑀-element subsets of 𝑠, there is a color 𝑐 and a subset 𝑥 ⊆ 𝑠 such that 𝑥 is larger than 𝐹(𝑐) and the 𝑀-element subsets of 𝑥 are monochromatic with color 𝑐. This is the hypergraph version of Ramsey's theorem; the version for simple graphs is the case 𝑀 = 2. This is Metamath 100 proof #31. (Contributed by Mario Carneiro, 23-Apr-2015.) |
⊢ 𝐶 = (𝑎 ∈ V, 𝑖 ∈ ℕ0 ↦ {𝑏 ∈ 𝒫 𝑎 ∣ (♯‘𝑏) = 𝑖}) ⇒ ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑅 ∈ Fin ∧ 𝐹:𝑅⟶ℕ0) → ∃𝑛 ∈ ℕ0 ∀𝑠(𝑛 ≤ (♯‘𝑠) → ∀𝑓 ∈ (𝑅 ↑m (𝑠𝐶𝑀))∃𝑐 ∈ 𝑅 ∃𝑥 ∈ 𝒫 𝑠((𝐹‘𝑐) ≤ (♯‘𝑥) ∧ (𝑥𝐶𝑀) ⊆ (◡𝑓 “ {𝑐})))) | ||
According to Wikipedia "Primorial", https://en.wikipedia.org/wiki/Primorial (28-Aug-2020): "In mathematics, and more particularly in number theory, primorial, denoted by "#", is a function from natural numbers to natural numbers similar to the factorial function, but rather than successively multiplying [all] positive integers [less than or equal to a given number], the function only multiplies [the] prime numbers [less than or equal to the given number]. The name "primorial", coined by Harvey Dubner, draws an analogy to primes similar to the way the name "factorial" relates to factors." | ||
Syntax | cprmo 16357 | Extend class notation to include the primorial of nonnegative integers. |
class #p | ||
Definition | df-prmo 16358* |
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 28166).
In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 25683, 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 16359* | Value of the primorial function for nonnegative integers. (Contributed by AV, 28-Aug-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) = ∏𝑘 ∈ (1...𝑁)if(𝑘 ∈ ℙ, 𝑘, 1)) | ||
Theorem | prmocl 16360 | Closure of the primorial function. (Contributed by AV, 28-Aug-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ∈ ℕ) | ||
Theorem | prmone0 16361 | The primorial function is nonzero. (Contributed by AV, 28-Aug-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ≠ 0) | ||
Theorem | prmo0 16362 | The primorial of 0. (Contributed by AV, 28-Aug-2020.) |
⊢ (#p‘0) = 1 | ||
Theorem | prmo1 16363 | The primorial of 1. (Contributed by AV, 28-Aug-2020.) |
⊢ (#p‘1) = 1 | ||
Theorem | prmop1 16364 | The primorial of a successor. (Contributed by AV, 28-Aug-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#p‘(𝑁 + 1)) = if((𝑁 + 1) ∈ ℙ, ((#p‘𝑁) · (𝑁 + 1)), (#p‘𝑁))) | ||
Theorem | prmonn2 16365 | Value of the primorial function expressed recursively. (Contributed by AV, 28-Aug-2020.) |
⊢ (𝑁 ∈ ℕ → (#p‘𝑁) = if(𝑁 ∈ ℙ, ((#p‘(𝑁 − 1)) · 𝑁), (#p‘(𝑁 − 1)))) | ||
Theorem | prmo2 16366 | The primorial of 2. (Contributed by AV, 28-Aug-2020.) |
⊢ (#p‘2) = 2 | ||
Theorem | prmo3 16367 | The primorial of 3. (Contributed by AV, 28-Aug-2020.) |
⊢ (#p‘3) = 6 | ||
Theorem | prmdvdsprmo 16368* | 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 16369* | 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 16370* | 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 16371* | 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 16372 | 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 16373 | 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 16374 | The primorial of a positive integer is less than or equal to the least common multiple of all positive integers less than or equal to the integer. (Contributed by AV, 19-Aug-2020.) (Revised by AV, 29-Aug-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#p‘𝑁) ≤ (lcm‘(1...𝑁))) | ||
According to Wikipedia "Prime gap", https://en.wikipedia.org/wiki/Prime_gap (16-Aug-2020): "A prime gap is the difference between two successive prime numbers. The n-th prime gap, denoted gn or g(pn) is the difference between the (n+1)-th and the n-th prime numbers, i.e. gn = pn+1 - pn . We have g1 = 1, g2 = g3 = 2, and g4 = 4." It can be proven that there are arbitrary large gaps, usually by showing that "in the sequence n!+2, n!+3, ..., n!+n the first term is divisible by 2, the second term is divisible by 3, and so on. Thus, this is a sequence of n-1 consecutive composite integers, and it must belong to a gap between primes having length at least n.", see prmgap 16385. Instead of using the factorial of n (see df-fac 13624), 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 16386, or the primorial n# (the product of all prime numbers less than or equal to n), see prmgapprmo 16388, are such functions, which provide smaller values than the factorial function (see lcmflefac 15982 and prmolefac 16372 resp. prmolelcmf 16374): "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 16375 | Lemma for prmgap 16385: 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 16376 | Lemma for prmgap 16385: 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 16377 | Lemma for prmgaplcm 16386: 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 16378 | Lemma for prmgaplcm 16386: 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 16379* | Lemma for prmgap 16385. (Contributed by AV, 9-Aug-2020.) |
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ 𝑝 < 𝑁} ⇒ ⊢ (𝑁 ∈ (ℤ≥‘3) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) | ||
Theorem | prmgaplem4 16380* | Lemma for prmgap 16385. (Contributed by AV, 10-Aug-2020.) |
⊢ 𝐴 = {𝑝 ∈ ℙ ∣ (𝑁 < 𝑝 ∧ 𝑝 ≤ 𝑃)} ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑁 < 𝑃) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | prmgaplem5 16381* | Lemma for prmgap 16385: 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 16382* | Lemma for prmgap 16385: 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 16383* | Lemma for prmgap 16385. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m ℕ)) & ⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖)) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 < ((𝐹‘𝑁) + 2) ∧ ((𝐹‘𝑁) + 𝑁) < 𝑞 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) | ||
Theorem | prmgaplem8 16384* | Lemma for prmgap 16385. (Contributed by AV, 13-Aug-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐹 ∈ (ℕ ↑m ℕ)) & ⊢ (𝜑 → ∀𝑖 ∈ (2...𝑁)1 < (((𝐹‘𝑁) + 𝑖) gcd 𝑖)) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑁 ≤ (𝑞 − 𝑝) ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ)) | ||
Theorem | prmgap 16385* | 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 16386* | Alternate proof of prmgap 16385: in contrast to prmgap 16385, 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 16387 | Lemma for prmgapprmo 16388: 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 16388* | Alternate proof of prmgap 16385: in contrast to prmgap 16385, where the gap starts at n! , the factorial of n, the gap starts at n#, the primorial of n. (Contributed by AV, 15-Aug-2020.) (Revised by AV, 29-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∀𝑛 ∈ ℕ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑛 ≤ (𝑞 − 𝑝) ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑞)𝑧 ∉ ℙ) | ||
Theorem | dec2dvds 16389 | Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ (𝐵 · 2) = 𝐶 & ⊢ 𝐷 = (𝐶 + 1) ⇒ ⊢ ¬ 2 ∥ ;𝐴𝐷 | ||
Theorem | dec5dvds 16390 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐵 < 5 ⇒ ⊢ ¬ 5 ∥ ;𝐴𝐵 | ||
Theorem | dec5dvds2 16391 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ & ⊢ 𝐵 < 5 & ⊢ (5 + 𝐵) = 𝐶 ⇒ ⊢ ¬ 5 ∥ ;𝐴𝐶 | ||
Theorem | dec5nprm 16392 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ ¬ ;𝐴5 ∈ ℙ | ||
Theorem | dec2nprm 16393 | Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ (𝐵 · 2) = 𝐶 ⇒ ⊢ ¬ ;𝐴𝐶 ∈ ℙ | ||
Theorem | modxai 16394 | 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 16395 | Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) |
⊢ 𝑁 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁) & ⊢ (2 · 𝐵) = 𝐸 & ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾) ⇒ ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁) | ||
Theorem | modxp1i 16396 | 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 16397 | Version of mod2xi 16395 with a negative mod value. (Contributed by Mario Carneiro, 21-Feb-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐷 ∈ ℤ & ⊢ 𝐾 ∈ ℕ & ⊢ 𝑀 ∈ ℕ0 & ⊢ 𝐿 ∈ ℕ0 & ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐿 mod 𝑁) & ⊢ (2 · 𝐵) = 𝐸 & ⊢ (𝐿 + 𝐾) = 𝑁 & ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾) ⇒ ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁) | ||
Theorem | modsubi 16398 | Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑁 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ (𝐴 mod 𝑁) = (𝐾 mod 𝑁) & ⊢ (𝑀 + 𝐵) = 𝐾 ⇒ ⊢ ((𝐴 − 𝐵) mod 𝑁) = (𝑀 mod 𝑁) | ||
Theorem | gcdi 16399 | Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.) |
⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑅 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ (𝑁 gcd 𝑅) = 𝐺 & ⊢ ((𝐾 · 𝑁) + 𝑅) = 𝑀 ⇒ ⊢ (𝑀 gcd 𝑁) = 𝐺 | ||
Theorem | gcdmodi 16400 | 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 𝑁) = 𝐺 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |