![]() |
Metamath
Proof Explorer Theorem List (p. 170 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-vdwap 16901* | 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 16902* | Define the "contains a monochromatic AP" predicate. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ MonoAP = {β¨π, πβ© β£ βπ(ran (APβπ) β© π« (β‘π β {π})) β β } | ||
Definition | df-vdwpc 16903* | Define the "contains a polychromatic collection of APs" predicate. See vdwpc 16913 for more information. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ PolyAP = {β¨β¨π, πβ©, πβ© β£ βπ β β βπ β (β βm (1...π))(βπ β (1...π)((π + (πβπ))(APβπ)(πβπ)) β (β‘π β {(πβ(π + (πβπ)))}) β§ (β―βran (π β (1...π) β¦ (πβ(π + (πβπ))))) = π)} | ||
Theorem | vdwapfval 16904* | 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 16905 | The arithmetic progression function is a function. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ (πΎ β β0 β (APβπΎ):(β Γ β)βΆπ« β) | ||
Theorem | vdwapval 16906* | Value of the arithmetic progression function. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ ((πΎ β β0 β§ π΄ β β β§ π· β β) β (π β (π΄(APβπΎ)π·) β βπ β (0...(πΎ β 1))π = (π΄ + (π Β· π·)))) | ||
Theorem | vdwapun 16907 | Remove the first element of an arithmetic progression. (Contributed by Mario Carneiro, 11-Sep-2014.) |
β’ ((πΎ β β0 β§ π΄ β β β§ π· β β) β (π΄(APβ(πΎ + 1))π·) = ({π΄} βͺ ((π΄ + π·)(APβπΎ)π·))) | ||
Theorem | vdwapid1 16908 | The first element of an arithmetic progression. (Contributed by Mario Carneiro, 12-Sep-2014.) |
β’ ((πΎ β β β§ π΄ β β β§ π· β β) β π΄ β (π΄(APβπΎ)π·)) | ||
Theorem | vdwap0 16909 | Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ ((π΄ β β β§ π· β β) β (π΄(APβ0)π·) = β ) | ||
Theorem | vdwap1 16910 | Value of a length-1 arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ ((π΄ β β β§ π· β β) β (π΄(APβ1)π·) = {π΄}) | ||
Theorem | vdwmc 16911* | The predicate " The β¨π , πβ©-coloring πΉ contains a monochromatic AP of length πΎ". (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ π β V & β’ (π β πΎ β β0) & β’ (π β πΉ:πβΆπ ) β β’ (π β (πΎ MonoAP πΉ β βπβπ β β βπ β β (π(APβπΎ)π) β (β‘πΉ β {π}))) | ||
Theorem | vdwmc2 16912* | Expand out the definition of an arithmetic progression. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ π β V & β’ (π β πΎ β β0) & β’ (π β πΉ:πβΆπ ) & β’ (π β π΄ β π) β β’ (π β (πΎ MonoAP πΉ β βπ β π βπ β β βπ β β βπ β (0...(πΎ β 1))(π + (π Β· π)) β (β‘πΉ β {π}))) | ||
Theorem | vdwpc 16913* | 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 16914* | Lemma for vdw 16927. (Contributed by Mario Carneiro, 12-Sep-2014.) |
β’ (π β π β Fin) & β’ (π β πΎ β β) & β’ (π β π β β) & β’ (π β πΉ:(1...π)βΆπ ) & β’ (π β π΄ β β) & β’ (π β π β β) & β’ (π β π·:(1...π)βΆβ) & β’ (π β βπ β (1...π)((π΄ + (π·βπ))(APβπΎ)(π·βπ)) β (β‘πΉ β {(πΉβ(π΄ + (π·βπ)))})) & β’ (π β πΌ β (1...π)) & β’ (π β (πΉβπ΄) = (πΉβ(π΄ + (π·βπΌ)))) β β’ (π β (πΎ + 1) MonoAP πΉ) | ||
Theorem | vdwlem2 16915* | Lemma for vdw 16927. (Contributed by Mario Carneiro, 12-Sep-2014.) |
β’ (π β π β Fin) & β’ (π β πΎ β β0) & β’ (π β π β β) & β’ (π β π β β) & β’ (π β πΉ:(1...π)βΆπ ) & β’ (π β π β (β€β₯β(π + π))) & β’ πΊ = (π₯ β (1...π) β¦ (πΉβ(π₯ + π))) β β’ (π β (πΎ MonoAP πΊ β πΎ MonoAP πΉ)) | ||
Theorem | vdwlem3 16916 | Lemma for vdw 16927. (Contributed by Mario Carneiro, 13-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π΄ β (1...π)) & β’ (π β π΅ β (1...π)) β β’ (π β (π΅ + (π Β· ((π΄ β 1) + π))) β (1...(π Β· (2 Β· π)))) | ||
Theorem | vdwlem4 16917* | Lemma for vdw 16927. (Contributed by Mario Carneiro, 12-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β Fin) & β’ (π β π»:(1...(π Β· (2 Β· π)))βΆπ ) & β’ πΉ = (π₯ β (1...π) β¦ (π¦ β (1...π) β¦ (π»β(π¦ + (π Β· ((π₯ β 1) + π)))))) β β’ (π β πΉ:(1...π)βΆ(π βm (1...π))) | ||
Theorem | vdwlem5 16918* | Lemma for vdw 16927. (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 16919* | Lemma for vdw 16927. (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 16920* | Lemma for vdw 16927. (Contributed by Mario Carneiro, 12-Sep-2014.) |
β’ (π β π β β) & β’ (π β π β β) & β’ (π β π β Fin) & β’ (π β π»:(1...(π Β· (2 Β· π)))βΆπ ) & β’ πΉ = (π₯ β (1...π) β¦ (π¦ β (1...π) β¦ (π»β(π¦ + (π Β· ((π₯ β 1) + π)))))) & β’ (π β π β β) & β’ (π β πΊ:(1...π)βΆπ ) & β’ (π β πΎ β (β€β₯β2)) & β’ (π β π΄ β β) & β’ (π β π· β β) & β’ (π β (π΄(APβπΎ)π·) β (β‘πΉ β {πΊ})) β β’ (π β (β¨π, πΎβ© PolyAP πΊ β (β¨(π + 1), πΎβ© PolyAP π» β¨ (πΎ + 1) MonoAP πΊ))) | ||
Theorem | vdwlem8 16921* | Lemma for vdw 16927. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ (π β π β Fin) & β’ (π β πΎ β (β€β₯β2)) & β’ (π β π β β) & β’ (π β πΉ:(1...(2 Β· π))βΆπ ) & β’ πΆ β V & β’ (π β π΄ β β) & β’ (π β π· β β) & β’ (π β (π΄(APβπΎ)π·) β (β‘πΊ β {πΆ})) & β’ πΊ = (π₯ β (1...π) β¦ (πΉβ(π₯ + π))) β β’ (π β β¨1, πΎβ© PolyAP πΉ) | ||
Theorem | vdwlem9 16922* | Lemma for vdw 16927. (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 16923* | Lemma for vdw 16927. 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 16924* | Lemma for vdw 16927. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ (π β π β Fin) & β’ (π β πΎ β (β€β₯β2)) & β’ (π β βπ β Fin βπ β β βπ β (π βm (1...π))πΎ MonoAP π) β β’ (π β βπ β β βπ β (π βm (1...π))(πΎ + 1) MonoAP π) | ||
Theorem | vdwlem12 16925 | Lemma for vdw 16927. πΎ = 2 base case of induction. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ (π β π β Fin) & β’ (π β πΉ:(1...((β―βπ ) + 1))βΆπ ) & β’ (π β Β¬ 2 MonoAP πΉ) β β’ Β¬ π | ||
Theorem | vdwlem13 16926* | Lemma for vdw 16927. Main induction on πΎ; πΎ = 0, πΎ = 1 base cases. (Contributed by Mario Carneiro, 18-Aug-2014.) |
β’ (π β π β Fin) & β’ (π β πΎ β β0) β β’ (π β βπ β β βπ β (π βm (1...π))πΎ MonoAP π) | ||
Theorem | vdw 16927* | 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 16928* | Corollary of vdw 16927, and lemma for vdwnn 16931. 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 16929* | Lemma for vdwnn 16931. 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 16930* | Lemma for vdwnn 16931. (Contributed by Mario Carneiro, 13-Sep-2014.) (Proof shortened by AV, 27-Sep-2020.) |
β’ (π β π β Fin) & β’ (π β πΉ:ββΆπ ) & β’ π = {π β β β£ Β¬ βπ β β βπ β β βπ β (0...(π β 1))(π + (π Β· π)) β (β‘πΉ β {π})} & β’ (π β βπ β π π β β ) β β’ Β¬ π | ||
Theorem | vdwnn 16931* | 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 16932 | Extend class notation with the Ramsey number function. |
class Ramsey | ||
Theorem | ramtlecl 16933* | The set π of numbers with the Ramsey number property is upward-closed. (Contributed by Mario Carneiro, 21-Apr-2015.) |
β’ π = {π β β0 β£ βπ (π β€ (β―βπ ) β π)} β β’ (π β π β (β€β₯βπ) β π) | ||
Definition | df-ram 16934* | 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 16935* | Value of the "binomial set", the set of all π-element subsets of π΄. (Contributed by Mario Carneiro, 20-Apr-2015.) |
β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) β β’ ((π΄ β π β§ π β β0) β (π΄πΆπ) = {π₯ β π« π΄ β£ (β―βπ₯) = π}) | ||
Theorem | hashbccl 16936* | The binomial set is a finite set. (Contributed by Mario Carneiro, 20-Apr-2015.) |
β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) β β’ ((π΄ β Fin β§ π β β0) β (π΄πΆπ) β Fin) | ||
Theorem | hashbcss 16937* | Subset relation for the binomial set. (Contributed by Mario Carneiro, 20-Apr-2015.) |
β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) β β’ ((π΄ β π β§ π΅ β π΄ β§ π β β0) β (π΅πΆπ) β (π΄πΆπ)) | ||
Theorem | hashbc0 16938* | 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 16939* | The size of the binomial set is the binomial coefficient. (Contributed by Mario Carneiro, 20-Apr-2015.) |
β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) β β’ ((π΄ β Fin β§ π β β0) β (β―β(π΄πΆπ)) = ((β―βπ΄)Cπ)) | ||
Theorem | 0hashbc 16940* | There are no subsets of the empty set with size greater than zero. (Contributed by Mario Carneiro, 22-Apr-2015.) |
β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) β β’ (π β β β (β πΆπ) = β ) | ||
Theorem | ramval 16941* | 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 16942* | 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 16943* | 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 16944* | 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 16945* | 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 16946* | 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 16947* | 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 16948* | The defining property of a Ramsey number. (Contributed by Mario Carneiro, 22-Apr-2015.) |
β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) & β’ (π β π β β0) & β’ (π β π β π) & β’ (π β πΉ:π βΆβ0) & β’ (π β (π Ramsey πΉ) β β0) & β’ (π β π β π) & β’ (π β (π Ramsey πΉ) β€ (β―βπ)) & β’ (π β πΊ:(ππΆπ)βΆπ ) β β’ (π β βπ β π βπ₯ β π« π((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘πΊ β {π}))) | ||
Theorem | ramcl2 16949 | 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 16950 | The Ramsey number is an extended real number. (This theorem does not imply Ramsey's theorem, unlike ramcl 16962.) (Contributed by Mario Carneiro, 20-Apr-2015.) |
β’ ((π β β0 β§ π β π β§ πΉ:π βΆβ0) β (π Ramsey πΉ) β β*) | ||
Theorem | ramubcl 16951 | 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 16952* | 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 16953* | The Ramsey number when π = 0. (Contributed by Mario Carneiro, 22-Apr-2015.) |
β’ (((π β π β§ π β β β§ πΉ:π βΆβ0) β§ βπ₯ β β€ βπ¦ β ran πΉ π¦ β€ π₯) β (0 Ramsey πΉ) = sup(ran πΉ, β, < )) | ||
Theorem | 0ram2 16954 | The Ramsey number when π = 0. (Contributed by Mario Carneiro, 22-Apr-2015.) |
β’ ((π β Fin β§ π β β β§ πΉ:π βΆβ0) β (0 Ramsey πΉ) = sup(ran πΉ, β, < )) | ||
Theorem | ram0 16955 | The Ramsey number when π = β . (Contributed by Mario Carneiro, 22-Apr-2015.) |
β’ (π β β0 β (π Ramsey β ) = π) | ||
Theorem | 0ramcl 16956 | Lemma for ramcl 16962: Existence of the Ramsey number when π = 0. (Contributed by Mario Carneiro, 23-Apr-2015.) |
β’ ((π β Fin β§ πΉ:π βΆβ0) β (0 Ramsey πΉ) β β0) | ||
Theorem | ramz2 16957 | The Ramsey number when πΉ has value zero for some color πΆ. (Contributed by Mario Carneiro, 22-Apr-2015.) |
β’ (((π β β β§ π β π β§ πΉ:π βΆβ0) β§ (πΆ β π β§ (πΉβπΆ) = 0)) β (π Ramsey πΉ) = 0) | ||
Theorem | ramz 16958 | The Ramsey number when πΉ is the zero function. (Contributed by Mario Carneiro, 22-Apr-2015.) |
β’ ((π β β0 β§ π β π β§ π β β ) β (π Ramsey (π Γ {0})) = 0) | ||
Theorem | ramub1lem1 16959* | Lemma for ramub1 16961. (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 16960* | Lemma for ramub1 16961. (Contributed by Mario Carneiro, 23-Apr-2015.) |
β’ (π β π β β) & β’ (π β π β Fin) & β’ (π β πΉ:π βΆβ) & β’ πΊ = (π₯ β π β¦ (π Ramsey (π¦ β π β¦ if(π¦ = π₯, ((πΉβπ₯) β 1), (πΉβπ¦))))) & β’ (π β πΊ:π βΆβ0) & β’ (π β ((π β 1) Ramsey πΊ) β β0) & β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) & β’ (π β π β Fin) & β’ (π β (β―βπ) = (((π β 1) Ramsey πΊ) + 1)) & β’ (π β πΎ:(ππΆπ)βΆπ ) & β’ (π β π β π) & β’ π» = (π’ β ((π β {π})πΆ(π β 1)) β¦ (πΎβ(π’ βͺ {π}))) β β’ (π β βπ β π βπ§ β π« π((πΉβπ) β€ (β―βπ§) β§ (π§πΆπ) β (β‘πΎ β {π}))) | ||
Theorem | ramub1 16961* | 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 16962 | 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 16963* | Ramsey's theorem with the definition of Ramsey (df-ram 16934) 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 16964 | Extend class notation to include the primorial of nonnegative integers. |
class #p | ||
Definition | df-prmo 16965* |
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 29712).
In the literature, the primorial function is written as a postscript hash: 6# = 30. In contrast to prmorcht 26682, 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 16966* | Value of the primorial function for nonnegative integers. (Contributed by AV, 28-Aug-2020.) |
β’ (π β β0 β (#pβπ) = βπ β (1...π)if(π β β, π, 1)) | ||
Theorem | prmocl 16967 | Closure of the primorial function. (Contributed by AV, 28-Aug-2020.) |
β’ (π β β0 β (#pβπ) β β) | ||
Theorem | prmone0 16968 | The primorial function is nonzero. (Contributed by AV, 28-Aug-2020.) |
β’ (π β β0 β (#pβπ) β 0) | ||
Theorem | prmo0 16969 | The primorial of 0. (Contributed by AV, 28-Aug-2020.) |
β’ (#pβ0) = 1 | ||
Theorem | prmo1 16970 | The primorial of 1. (Contributed by AV, 28-Aug-2020.) |
β’ (#pβ1) = 1 | ||
Theorem | prmop1 16971 | The primorial of a successor. (Contributed by AV, 28-Aug-2020.) |
β’ (π β β0 β (#pβ(π + 1)) = if((π + 1) β β, ((#pβπ) Β· (π + 1)), (#pβπ))) | ||
Theorem | prmonn2 16972 | Value of the primorial function expressed recursively. (Contributed by AV, 28-Aug-2020.) |
β’ (π β β β (#pβπ) = if(π β β, ((#pβ(π β 1)) Β· π), (#pβ(π β 1)))) | ||
Theorem | prmo2 16973 | The primorial of 2. (Contributed by AV, 28-Aug-2020.) |
β’ (#pβ2) = 2 | ||
Theorem | prmo3 16974 | The primorial of 3. (Contributed by AV, 28-Aug-2020.) |
β’ (#pβ3) = 6 | ||
Theorem | prmdvdsprmo 16975* | 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 16976* | 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 16977* | 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 16978* | 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 16979 | 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 16980 | 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 16981 | 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 16992. Instead of using the factorial of n (see df-fac 14234), 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 16993, or the primorial n# (the product of all prime numbers less than or equal to n), see prmgapprmo 16995, are such functions, which provide smaller values than the factorial function (see lcmflefac 16585 and prmolefac 16979 resp. prmolelcmf 16981): "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 16982 | Lemma for prmgap 16992: 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 16983 | Lemma for prmgap 16992: 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 16984 | Lemma for prmgaplcm 16993: 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 16985 | Lemma for prmgaplcm 16993: 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 16986* | Lemma for prmgap 16992. (Contributed by AV, 9-Aug-2020.) |
β’ π΄ = {π β β β£ π < π} β β’ (π β (β€β₯β3) β βπ₯ β π΄ βπ¦ β π΄ π¦ β€ π₯) | ||
Theorem | prmgaplem4 16987* | Lemma for prmgap 16992. (Contributed by AV, 10-Aug-2020.) |
β’ π΄ = {π β β β£ (π < π β§ π β€ π)} β β’ ((π β β β§ π β β β§ π < π) β βπ₯ β π΄ βπ¦ β π΄ π₯ β€ π¦) | ||
Theorem | prmgaplem5 16988* | Lemma for prmgap 16992: 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 16989* | Lemma for prmgap 16992: 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 16990* | Lemma for prmgap 16992. (Contributed by AV, 12-Aug-2020.) (Proof shortened by AV, 10-Jul-2022.) |
β’ (π β π β β) & β’ (π β πΉ β (β βm β)) & β’ (π β βπ β (2...π)1 < (((πΉβπ) + π) gcd π)) β β’ (π β βπ β β βπ β β (π < ((πΉβπ) + 2) β§ ((πΉβπ) + π) < π β§ βπ§ β ((π + 1)..^π)π§ β β)) | ||
Theorem | prmgaplem8 16991* | Lemma for prmgap 16992. (Contributed by AV, 13-Aug-2020.) |
β’ (π β π β β) & β’ (π β πΉ β (β βm β)) & β’ (π β βπ β (2...π)1 < (((πΉβπ) + π) gcd π)) β β’ (π β βπ β β βπ β β (π β€ (π β π) β§ βπ§ β ((π + 1)..^π)π§ β β)) | ||
Theorem | prmgap 16992* | 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 16993* | Alternate proof of prmgap 16992: in contrast to prmgap 16992, 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 16994 | Lemma for prmgapprmo 16995: 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 16995* | Alternate proof of prmgap 16992: in contrast to prmgap 16992, 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 16996 | Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
β’ π΄ β β0 & β’ π΅ β β0 & β’ (π΅ Β· 2) = πΆ & β’ π· = (πΆ + 1) β β’ Β¬ 2 β₯ ;π΄π· | ||
Theorem | dec5dvds 16997 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
β’ π΄ β β0 & β’ π΅ β β & β’ π΅ < 5 β β’ Β¬ 5 β₯ ;π΄π΅ | ||
Theorem | dec5dvds2 16998 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
β’ π΄ β β0 & β’ π΅ β β & β’ π΅ < 5 & β’ (5 + π΅) = πΆ β β’ Β¬ 5 β₯ ;π΄πΆ | ||
Theorem | dec5nprm 16999 | Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
β’ π΄ β β β β’ Β¬ ;π΄5 β β | ||
Theorem | dec2nprm 17000 | Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.) |
β’ π΄ β β & β’ π΅ β β0 & β’ (π΅ Β· 2) = πΆ β β’ Β¬ ;π΄πΆ β β |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |