Home | Metamath
Proof Explorer Theorem List (p. 458 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gbopos 45701 | Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020.) |
β’ (π β GoldbachOdd β π β β) | ||
Theorem | gbegt5 45702 | Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) |
β’ (π β GoldbachEven β 5 < π) | ||
Theorem | gbowgt5 45703 | Any weak odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) |
β’ (π β GoldbachOddW β 5 < π) | ||
Theorem | gbowge7 45704 | Any weak odd Goldbach number is greater than or equal to 7. Because of 7gbow 45713, this bound is strict. (Contributed by AV, 20-Jul-2020.) |
β’ (π β GoldbachOddW β 7 β€ π) | ||
Theorem | gboge9 45705 | Any odd Goldbach number is greater than or equal to 9. Because of 9gbo 45715, this bound is strict. (Contributed by AV, 26-Jul-2020.) |
β’ (π β GoldbachOdd β 9 β€ π) | ||
Theorem | gbege6 45706 | Any even Goldbach number is greater than or equal to 6. Because of 6gbe 45712, this bound is strict. (Contributed by AV, 20-Jul-2020.) |
β’ (π β GoldbachEven β 6 β€ π) | ||
Theorem | gbpart6 45707 | The Goldbach partition of 6. (Contributed by AV, 20-Jul-2020.) |
β’ 6 = (3 + 3) | ||
Theorem | gbpart7 45708 | The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020.) |
β’ 7 = ((2 + 2) + 3) | ||
Theorem | gbpart8 45709 | The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020.) |
β’ 8 = (3 + 5) | ||
Theorem | gbpart9 45710 | The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020.) |
β’ 9 = ((3 + 3) + 3) | ||
Theorem | gbpart11 45711 | The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020.) |
β’ ;11 = ((3 + 3) + 5) | ||
Theorem | 6gbe 45712 | 6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) |
β’ 6 β GoldbachEven | ||
Theorem | 7gbow 45713 | 7 is a weak odd Goldbach number. (Contributed by AV, 20-Jul-2020.) |
β’ 7 β GoldbachOddW | ||
Theorem | 8gbe 45714 | 8 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) |
β’ 8 β GoldbachEven | ||
Theorem | 9gbo 45715 | 9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020.) |
β’ 9 β GoldbachOdd | ||
Theorem | 11gbo 45716 | 11 is an odd Goldbach number. (Contributed by AV, 29-Jul-2020.) |
β’ ;11 β GoldbachOdd | ||
Theorem | stgoldbwt 45717 | If the strong ternary Goldbach conjecture is valid, then the weak ternary Goldbach conjecture holds, too. (Contributed by AV, 27-Jul-2020.) |
β’ (βπ β Odd (7 < π β π β GoldbachOdd ) β βπ β Odd (5 < π β π β GoldbachOddW )) | ||
Theorem | sbgoldbwt 45718* | If the strong binary Goldbach conjecture is valid, then the (weak) ternary Goldbach conjecture holds, too. (Contributed by AV, 20-Jul-2020.) |
β’ (βπ β Even (4 < π β π β GoldbachEven ) β βπ β Odd (5 < π β π β GoldbachOddW )) | ||
Theorem | sbgoldbst 45719* | If the strong binary Goldbach conjecture is valid, then the (strong) ternary Goldbach conjecture holds, too. (Contributed by AV, 26-Jul-2020.) |
β’ (βπ β Even (4 < π β π β GoldbachEven ) β βπ β Odd (7 < π β π β GoldbachOdd )) | ||
Theorem | sbgoldbaltlem1 45720 | Lemma 1 for sbgoldbalt 45722: If an even number greater than 4 is the sum of two primes, one of the prime summands must be odd, i.e. not 2. (Contributed by AV, 22-Jul-2020.) |
β’ ((π β β β§ π β β) β ((π β Even β§ 4 < π β§ π = (π + π)) β π β Odd )) | ||
Theorem | sbgoldbaltlem2 45721 | Lemma 2 for sbgoldbalt 45722: If an even number greater than 4 is the sum of two primes, the primes must be odd, i.e. not 2. (Contributed by AV, 22-Jul-2020.) |
β’ ((π β β β§ π β β) β ((π β Even β§ 4 < π β§ π = (π + π)) β (π β Odd β§ π β Odd ))) | ||
Theorem | sbgoldbalt 45722* | An alternate (related to the original) formulation of the binary Goldbach conjecture: Every even integer greater than 2 can be expressed as the sum of two primes. (Contributed by AV, 22-Jul-2020.) |
β’ (βπ β Even (4 < π β π β GoldbachEven ) β βπ β Even (2 < π β βπ β β βπ β β π = (π + π))) | ||
Theorem | sbgoldbb 45723* | If the strong binary Goldbach conjecture is valid, the binary Goldbach conjecture is valid. (Contributed by AV, 23-Dec-2021.) |
β’ (βπ β Even (4 < π β π β GoldbachEven ) β βπ β Even (2 < π β βπ β β βπ β β π = (π + π))) | ||
Theorem | sgoldbeven3prm 45724* | If the binary Goldbach conjecture is valid, then an even integer greater than 5 can be expressed as the sum of three primes: Since (π β 2) is even iff π is even, there would be primes π and π with (π β 2) = (π + π), and therefore π = ((π + π) + 2). (Contributed by AV, 24-Dec-2021.) |
β’ (βπ β Even (4 < π β π β GoldbachEven ) β ((π β Even β§ 6 β€ π) β βπ β β βπ β β βπ β β π = ((π + π) + π))) | ||
Theorem | sbgoldbm 45725* | If the strong binary Goldbach conjecture is valid, the modern version of the original formulation of the Goldbach conjecture also holds: Every integer greater than 5 can be expressed as the sum of three primes. (Contributed by AV, 24-Dec-2021.) |
β’ (βπ β Even (4 < π β π β GoldbachEven ) β βπ β (β€β₯β6)βπ β β βπ β β βπ β β π = ((π + π) + π)) | ||
Theorem | mogoldbb 45726* | If the modern version of the original formulation of the Goldbach conjecture is valid, the (weak) binary Goldbach conjecture also holds. (Contributed by AV, 26-Dec-2021.) |
β’ (βπ β (β€β₯β6)βπ β β βπ β β βπ β β π = ((π + π) + π) β βπ β Even (2 < π β βπ β β βπ β β π = (π + π))) | ||
Theorem | sbgoldbmb 45727* | The strong binary Goldbach conjecture and the modern version of the original formulation of the Goldbach conjecture are equivalent. (Contributed by AV, 26-Dec-2021.) |
β’ (βπ β Even (4 < π β π β GoldbachEven ) β βπ β (β€β₯β6)βπ β β βπ β β βπ β β π = ((π + π) + π)) | ||
Theorem | sbgoldbo 45728* | If the strong binary Goldbach conjecture is valid, the original formulation of the Goldbach conjecture also holds: Every integer greater than 2 can be expressed as the sum of three "primes" with regarding 1 to be a prime (as Goldbach did). Original text: "Es scheint wenigstens, dass eine jede Zahl, die groesser ist als 2, ein aggregatum trium numerorum primorum sey." (Goldbach, 1742). (Contributed by AV, 25-Dec-2021.) |
β’ π = ({1} βͺ β) β β’ (βπ β Even (4 < π β π β GoldbachEven ) β βπ β (β€β₯β3)βπ β π βπ β π βπ β π π = ((π + π) + π)) | ||
Theorem | nnsum3primes4 45729* | 4 is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.) |
β’ βπ β β βπ β (β βm (1...π))(π β€ 3 β§ 4 = Ξ£π β (1...π)(πβπ)) | ||
Theorem | nnsum4primes4 45730* | 4 is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) |
β’ βπ β β βπ β (β βm (1...π))(π β€ 4 β§ 4 = Ξ£π β (1...π)(πβπ)) | ||
Theorem | nnsum3primesprm 45731* | Every prime is "the sum of at most 3" (actually one - the prime itself) primes. (Contributed by AV, 2-Aug-2020.) (Proof shortened by AV, 17-Apr-2021.) |
β’ (π β β β βπ β β βπ β (β βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ))) | ||
Theorem | nnsum4primesprm 45732* | Every prime is "the sum of at most 4" (actually one - the prime itself) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) |
β’ (π β β β βπ β β βπ β (β βm (1...π))(π β€ 4 β§ π = Ξ£π β (1...π)(πβπ))) | ||
Theorem | nnsum3primesgbe 45733* | Any even Goldbach number is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.) |
β’ (π β GoldbachEven β βπ β β βπ β (β βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ))) | ||
Theorem | nnsum4primesgbe 45734* | Any even Goldbach number is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) |
β’ (π β GoldbachEven β βπ β β βπ β (β βm (1...π))(π β€ 4 β§ π = Ξ£π β (1...π)(πβπ))) | ||
Theorem | nnsum3primesle9 45735* | Every integer greater than 1 and less than or equal to 8 is the sum of at most 3 primes. (Contributed by AV, 2-Aug-2020.) |
β’ ((π β (β€β₯β2) β§ π β€ 8) β βπ β β βπ β (β βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ))) | ||
Theorem | nnsum4primesle9 45736* | Every integer greater than 1 and less than or equal to 8 is the sum of at most 4 primes. (Contributed by AV, 24-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) |
β’ ((π β (β€β₯β2) β§ π β€ 8) β βπ β β βπ β (β βm (1...π))(π β€ 4 β§ π = Ξ£π β (1...π)(πβπ))) | ||
Theorem | nnsum4primesodd 45737* | If the (weak) ternary Goldbach conjecture is valid, then every odd integer greater than 5 is the sum of 3 primes. (Contributed by AV, 2-Jul-2020.) |
β’ (βπ β Odd (5 < π β π β GoldbachOddW ) β ((π β (β€β₯β6) β§ π β Odd ) β βπ β (β βm (1...3))π = Ξ£π β (1...3)(πβπ))) | ||
Theorem | nnsum4primesoddALTV 45738* | If the (strong) ternary Goldbach conjecture is valid, then every odd integer greater than 7 is the sum of 3 primes. (Contributed by AV, 26-Jul-2020.) |
β’ (βπ β Odd (7 < π β π β GoldbachOdd ) β ((π β (β€β₯β8) β§ π β Odd ) β βπ β (β βm (1...3))π = Ξ£π β (1...3)(πβπ))) | ||
Theorem | evengpop3 45739* | If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of an odd Goldbach number and 3. (Contributed by AV, 24-Jul-2020.) |
β’ (βπ β Odd (5 < π β π β GoldbachOddW ) β ((π β (β€β₯β9) β§ π β Even ) β βπ β GoldbachOddW π = (π + 3))) | ||
Theorem | evengpoap3 45740* | If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of an odd Goldbach number and 3. (Contributed by AV, 27-Jul-2020.) (Proof shortened by AV, 15-Sep-2021.) |
β’ (βπ β Odd (7 < π β π β GoldbachOdd ) β ((π β (β€β₯β;12) β§ π β Even ) β βπ β GoldbachOdd π = (π + 3))) | ||
Theorem | nnsum4primeseven 45741* | If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of 4 primes. (Contributed by AV, 25-Jul-2020.) |
β’ (βπ β Odd (5 < π β π β GoldbachOddW ) β ((π β (β€β₯β9) β§ π β Even ) β βπ β (β βm (1...4))π = Ξ£π β (1...4)(πβπ))) | ||
Theorem | nnsum4primesevenALTV 45742* | If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of 4 primes. (Contributed by AV, 27-Jul-2020.) |
β’ (βπ β Odd (7 < π β π β GoldbachOdd ) β ((π β (β€β₯β;12) β§ π β Even ) β βπ β (β βm (1...4))π = Ξ£π β (1...4)(πβπ))) | ||
Theorem | wtgoldbnnsum4prm 45743* | If the (weak) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes, showing that Schnirelmann's constant would be less than or equal to 4. See corollary 1.1 in [Helfgott] p. 4. (Contributed by AV, 25-Jul-2020.) |
β’ (βπ β Odd (5 < π β π β GoldbachOddW ) β βπ β (β€β₯β2)βπ β β βπ β (β βm (1...π))(π β€ 4 β§ π = Ξ£π β (1...π)(πβπ))) | ||
Theorem | stgoldbnnsum4prm 45744* | If the (strong) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes. (Contributed by AV, 27-Jul-2020.) |
β’ (βπ β Odd (7 < π β π β GoldbachOdd ) β βπ β (β€β₯β2)βπ β β βπ β (β βm (1...π))(π β€ 4 β§ π = Ξ£π β (1...π)(πβπ))) | ||
Theorem | bgoldbnnsum3prm 45745* | If the binary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 3 primes, showing that Schnirelmann's constant would be equal to 3. (Contributed by AV, 2-Aug-2020.) |
β’ (βπ β Even (4 < π β π β GoldbachEven ) β βπ β (β€β₯β2)βπ β β βπ β (β βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ))) | ||
Theorem | bgoldbtbndlem1 45746 | Lemma 1 for bgoldbtbnd 45750: the odd numbers between 7 and 13 (exclusive) are odd Goldbach numbers. (Contributed by AV, 29-Jul-2020.) |
β’ ((π β Odd β§ 7 < π β§ π β (7[,);13)) β π β GoldbachOdd ) | ||
Theorem | bgoldbtbndlem2 45747* | Lemma 2 for bgoldbtbnd 45750. (Contributed by AV, 1-Aug-2020.) |
β’ (π β π β (β€β₯β;11)) & β’ (π β π β (β€β₯β;11)) & β’ (π β βπ β Even ((4 < π β§ π < π) β π β GoldbachEven )) & β’ (π β π· β (β€β₯β3)) & β’ (π β πΉ β (RePartβπ·)) & β’ (π β βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ)))) & β’ (π β (πΉβ0) = 7) & β’ (π β (πΉβ1) = ;13) & β’ (π β π < (πΉβπ·)) & β’ π = (π β (πΉβ(πΌ β 1))) β β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4) β (π β Even β§ π < π β§ 4 < π))) | ||
Theorem | bgoldbtbndlem3 45748* | Lemma 3 for bgoldbtbnd 45750. (Contributed by AV, 1-Aug-2020.) |
β’ (π β π β (β€β₯β;11)) & β’ (π β π β (β€β₯β;11)) & β’ (π β βπ β Even ((4 < π β§ π < π) β π β GoldbachEven )) & β’ (π β π· β (β€β₯β3)) & β’ (π β πΉ β (RePartβπ·)) & β’ (π β βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ)))) & β’ (π β (πΉβ0) = 7) & β’ (π β (πΉβ1) = ;13) & β’ (π β π < (πΉβπ·)) & β’ (π β (πΉβπ·) β β) & β’ π = (π β (πΉβπΌ)) β β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ 4 < π) β (π β Even β§ π < π β§ 4 < π))) | ||
Theorem | bgoldbtbndlem4 45749* | Lemma 4 for bgoldbtbnd 45750. (Contributed by AV, 1-Aug-2020.) |
β’ (π β π β (β€β₯β;11)) & β’ (π β π β (β€β₯β;11)) & β’ (π β βπ β Even ((4 < π β§ π < π) β π β GoldbachEven )) & β’ (π β π· β (β€β₯β3)) & β’ (π β πΉ β (RePartβπ·)) & β’ (π β βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ)))) & β’ (π β (πΉβ0) = 7) & β’ (π β (πΉβ1) = ;13) & β’ (π β π < (πΉβπ·)) & β’ (π β (πΉβπ·) β β) β β’ (((π β§ πΌ β (1..^π·)) β§ π β Odd ) β ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4) β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))) | ||
Theorem | bgoldbtbnd 45750* | If the binary Goldbach conjecture is valid up to an integer π, and there is a series ("ladder") of primes with a difference of at most π up to an integer π, then the strong ternary Goldbach conjecture is valid up to π, see section 1.2.2 in [Helfgott] p. 4 with N = 4 x 10^18, taken from [OeSilva], and M = 8.875 x 10^30. (Contributed by AV, 1-Aug-2020.) |
β’ (π β π β (β€β₯β;11)) & β’ (π β π β (β€β₯β;11)) & β’ (π β βπ β Even ((4 < π β§ π < π) β π β GoldbachEven )) & β’ (π β π· β (β€β₯β3)) & β’ (π β πΉ β (RePartβπ·)) & β’ (π β βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ)))) & β’ (π β (πΉβ0) = 7) & β’ (π β (πΉβ1) = ;13) & β’ (π β π < (πΉβπ·)) & β’ (π β (πΉβπ·) β β) β β’ (π β βπ β Odd ((7 < π β§ π < π) β π β GoldbachOdd )) | ||
Axiom | ax-bgbltosilva 45751 | The binary Goldbach conjecture is valid for all even numbers less than or equal to 4x10^18, see section 2 in [OeSilva] p. 2042. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
β’ ((π β Even β§ 4 < π β§ π β€ (4 Β· (;10β;18))) β π β GoldbachEven ) | ||
Axiom | ax-tgoldbachgt 45752* | Temporary duplicate of tgoldbachgt 33049, provided as "axiom" as long as this theorem is in the mathbox of Thierry Arnoux: Odd integers greater than (;10β;27) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of [Helfgott] p. 70 , expressed using the set πΊ of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021.) |
β’ π = {π§ β β€ β£ Β¬ 2 β₯ π§} & β’ πΊ = {π§ β π β£ βπ β β βπ β β βπ β β ((π β π β§ π β π β§ π β π) β§ π§ = ((π + π) + π))} β β’ βπ β β (π β€ (;10β;27) β§ βπ β π (π < π β π β πΊ)) | ||
Theorem | tgoldbachgtALTV 45753* | Variant of Thierry Arnoux's tgoldbachgt 33049 using the symbols Odd and GoldbachOdd: The ternary Goldbach conjecture is valid for large odd numbers (i.e. for all odd numbers greater than a fixed π). This is proven by Helfgott (see section 7.4 in [Helfgott] p. 70) for π = 10^27. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 15-Jan-2022.) |
β’ βπ β β (π β€ (;10β;27) β§ βπ β Odd (π < π β π β GoldbachOdd )) | ||
Theorem | bgoldbachlt 45754* | The binary Goldbach conjecture is valid for small even numbers (i.e. for all even numbers less than or equal to a fixed big π). This is verified for m = 4 x 10^18 by Oliveira e Silva, see ax-bgbltosilva 45751. (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
β’ βπ β β ((4 Β· (;10β;18)) β€ π β§ βπ β Even ((4 < π β§ π < π) β π β GoldbachEven )) | ||
Axiom | ax-hgprmladder 45755 | There is a partition ("ladder") of primes from 7 to 8.8 x 10^30 with parts ("rungs") having lengths of at least 4 and at most N - 4, see section 1.2.2 in [Helfgott] p. 4. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
β’ βπ β (β€β₯β3)βπ β (RePartβπ)(((πβ0) = 7 β§ (πβ1) = ;13 β§ (πβπ) = (;89 Β· (;10β;29))) β§ βπ β (0..^π)((πβπ) β (β β {2}) β§ ((πβ(π + 1)) β (πβπ)) < ((4 Β· (;10β;18)) β 4) β§ 4 < ((πβ(π + 1)) β (πβπ)))) | ||
Theorem | tgblthelfgott 45756 | The ternary Goldbach conjecture is valid for all odd numbers less than 8.8 x 10^30 (actually 8.875694 x 10^30, see section 1.2.2 in [Helfgott] p. 4, using bgoldbachlt 45754, ax-hgprmladder 45755 and bgoldbtbnd 45750. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
β’ ((π β Odd β§ 7 < π β§ π < (;88 Β· (;10β;29))) β π β GoldbachOdd ) | ||
Theorem | tgoldbachlt 45757* | The ternary Goldbach conjecture is valid for small odd numbers (i.e. for all odd numbers less than a fixed big π greater than 8 x 10^30). This is verified for m = 8.875694 x 10^30 by Helfgott, see tgblthelfgott 45756. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
β’ βπ β β ((8 Β· (;10β;30)) < π β§ βπ β Odd ((7 < π β§ π < π) β π β GoldbachOdd )) | ||
Theorem | tgoldbach 45758 | The ternary Goldbach conjecture is valid. Main theorem in [Helfgott] p. 2. This follows from tgoldbachlt 45757 and ax-tgoldbachgt 45752. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
β’ βπ β Odd (7 < π β π β GoldbachOdd ) | ||
In the following, a general definition of the isomorphy relation for graphs and specializations for simple hypergraphs (isomushgr 45767) and simple pseudographs (isomuspgr 45775) are provided. The latter corresponds to the definition in [Bollobas] p. 3). It is shown that the isomorphy relation for graphs is an equivalence relation (isomgrref 45776, isomgrsym 45777, isomgrtr 45780). Fianlly, isomorphic graphs with different representations are studied (strisomgrop 45781, ushrisomgr 45782). Maybe more important than graph isomorphy is the notion of graph isomorphism, which can be defined as in df-grisom 45761. Then π΄ IsomGr π΅ β βππ β (π΄ GrIsom π΅) resp. π΄ IsomGr π΅ β (π΄ GrIsom π΅) β β . Notice that there can be multiple isomorphisms between two graphs (let β¨{π΄, π΅}, {{π΄, π΅}}β© and β¨{{π, π}, {{π, π}}β© be two graphs with two vertices and one edge, then π΄ β¦ π, π΅ β¦ π and π΄ β¦ π, π΅ β¦ π are two different isomorphisms between these graphs). Another approach could be to define a category of graphs (there are maybe multiple ones), where graph morphisms are couples consisting in a function on vertices and a function on edges with required compatibilities, as used in the definition of GrIsom. And then, a graph isomorphism is defined as an isomorphism in the category of graphs (something like "GraphIsom = ( Iso ` GraphCat )" ). Then general category theory theorems could be used, e.g., to show that graph isomorphy is an equivalence relation. | ||
Syntax | cgrisom 45759 | Extend class notation to include the graph ispmorphisms. |
class GrIsom | ||
Syntax | cisomgr 45760 | Extend class notation to include the isomorphy relation for graphs. |
class IsomGr | ||
Definition | df-grisom 45761* | Define the class of all isomorphisms between two graphs. (Contributed by AV, 11-Dec-2022.) |
β’ GrIsom = (π₯ β V, π¦ β V β¦ {β¨π, πβ© β£ (π:(Vtxβπ₯)β1-1-ontoβ(Vtxβπ¦) β§ π:dom (iEdgβπ₯)β1-1-ontoβdom (iEdgβπ¦) β§ βπ β dom (iEdgβπ₯)(π β ((iEdgβπ₯)βπ)) = ((iEdgβπ¦)β(πβπ)))}) | ||
Definition | df-isomgr 45762* | Define the isomorphy relation for graphs. (Contributed by AV, 11-Nov-2022.) |
β’ IsomGr = {β¨π₯, π¦β© β£ βπ(π:(Vtxβπ₯)β1-1-ontoβ(Vtxβπ¦) β§ βπ(π:dom (iEdgβπ₯)β1-1-ontoβdom (iEdgβπ¦) β§ βπ β dom (iEdgβπ₯)(π β ((iEdgβπ₯)βπ)) = ((iEdgβπ¦)β(πβπ))))} | ||
Theorem | isomgrrel 45763 | The isomorphy relation for graphs is a relation. (Contributed by AV, 11-Nov-2022.) |
β’ Rel IsomGr | ||
Theorem | isomgr 45764* | The isomorphy relation for two graphs. (Contributed by AV, 11-Nov-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΌ = (iEdgβπ΄) & β’ π½ = (iEdgβπ΅) β β’ ((π΄ β π β§ π΅ β π) β (π΄ IsomGr π΅ β βπ(π:πβ1-1-ontoβπ β§ βπ(π:dom πΌβ1-1-ontoβdom π½ β§ βπ β dom πΌ(π β (πΌβπ)) = (π½β(πβπ)))))) | ||
Theorem | isisomgr 45765* | Implications of two graphs being isomorphic. (Contributed by AV, 11-Nov-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΌ = (iEdgβπ΄) & β’ π½ = (iEdgβπ΅) β β’ (π΄ IsomGr π΅ β βπ(π:πβ1-1-ontoβπ β§ βπ(π:dom πΌβ1-1-ontoβdom π½ β§ βπ β dom πΌ(π β (πΌβπ)) = (π½β(πβπ))))) | ||
Theorem | isomgreqve 45766 | A set is isomorphic to a hypergraph if it has the same vertices and the same edges. (Contributed by AV, 11-Nov-2022.) |
β’ (((π΄ β UHGraph β§ π΅ β π) β§ ((Vtxβπ΄) = (Vtxβπ΅) β§ (iEdgβπ΄) = (iEdgβπ΅))) β π΄ IsomGr π΅) | ||
Theorem | isomushgr 45767* | The isomorphy relation for two simple hypergraphs. (Contributed by AV, 28-Nov-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) β β’ ((π΄ β USHGraph β§ π΅ β USHGraph) β (π΄ IsomGr π΅ β βπ(π:πβ1-1-ontoβπ β§ βπ(π:πΈβ1-1-ontoβπΎ β§ βπ β πΈ (π β π) = (πβπ))))) | ||
Theorem | isomuspgrlem1 45768* | Lemma 1 for isomuspgr 45775. (Contributed by AV, 29-Nov-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) β β’ (((((π΄ β USPGraph β§ π΅ β USPGraph) β§ π:πβ1-1-ontoβπ) β§ (π:πΈβ1-1-ontoβπΎ β§ βπ β πΈ (π β π) = (πβπ))) β§ (π β π β§ π β π)) β ({(πβπ), (πβπ)} β πΎ β {π, π} β πΈ)) | ||
Theorem | isomuspgrlem2a 45769* | Lemma 1 for isomuspgrlem2 45774. (Contributed by AV, 29-Nov-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) & β’ πΊ = (π₯ β πΈ β¦ (πΉ β π₯)) β β’ (πΉ β π β βπ β πΈ (πΉ β π) = (πΊβπ)) | ||
Theorem | isomuspgrlem2b 45770* | Lemma 2 for isomuspgrlem2 45774. (Contributed by AV, 29-Nov-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) & β’ πΊ = (π₯ β πΈ β¦ (πΉ β π₯)) & β’ (π β π΄ β USPGraph) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ (π β βπ β π βπ β π ({π, π} β πΈ β {(πΉβπ), (πΉβπ)} β πΎ)) β β’ (π β πΊ:πΈβΆπΎ) | ||
Theorem | isomuspgrlem2c 45771* | Lemma 3 for isomuspgrlem2 45774. (Contributed by AV, 29-Nov-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) & β’ πΊ = (π₯ β πΈ β¦ (πΉ β π₯)) & β’ (π β π΄ β USPGraph) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ (π β βπ β π βπ β π ({π, π} β πΈ β {(πΉβπ), (πΉβπ)} β πΎ)) & β’ (π β πΉ β π) β β’ (π β πΊ:πΈβ1-1βπΎ) | ||
Theorem | isomuspgrlem2d 45772* | Lemma 4 for isomuspgrlem2 45774. (Contributed by AV, 1-Dec-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) & β’ πΊ = (π₯ β πΈ β¦ (πΉ β π₯)) & β’ (π β π΄ β USPGraph) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ (π β βπ β π βπ β π ({π, π} β πΈ β {(πΉβπ), (πΉβπ)} β πΎ)) & β’ (π β πΉ β π) & β’ (π β π΅ β USPGraph) β β’ (π β πΊ:πΈβontoβπΎ) | ||
Theorem | isomuspgrlem2e 45773* | Lemma 5 for isomuspgrlem2 45774. (Contributed by AV, 1-Dec-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) & β’ πΊ = (π₯ β πΈ β¦ (πΉ β π₯)) & β’ (π β π΄ β USPGraph) & β’ (π β πΉ:πβ1-1-ontoβπ) & β’ (π β βπ β π βπ β π ({π, π} β πΈ β {(πΉβπ), (πΉβπ)} β πΎ)) & β’ (π β πΉ β π) & β’ (π β π΅ β USPGraph) β β’ (π β πΊ:πΈβ1-1-ontoβπΎ) | ||
Theorem | isomuspgrlem2 45774* | Lemma 2 for isomuspgr 45775. (Contributed by AV, 1-Dec-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) β β’ (((π΄ β USPGraph β§ π΅ β USPGraph) β§ π:πβ1-1-ontoβπ) β (βπ β π βπ β π ({π, π} β πΈ β {(πβπ), (πβπ)} β πΎ) β βπ(π:πΈβ1-1-ontoβπΎ β§ βπ β πΈ (π β π) = (πβπ)))) | ||
Theorem | isomuspgr 45775* | The isomorphy relation for two simple pseudographs. This corresponds to the definition in [Bollobas] p. 3. (Contributed by AV, 1-Dec-2022.) |
β’ π = (Vtxβπ΄) & β’ π = (Vtxβπ΅) & β’ πΈ = (Edgβπ΄) & β’ πΎ = (Edgβπ΅) β β’ ((π΄ β USPGraph β§ π΅ β USPGraph) β (π΄ IsomGr π΅ β βπ(π:πβ1-1-ontoβπ β§ βπ β π βπ β π ({π, π} β πΈ β {(πβπ), (πβπ)} β πΎ)))) | ||
Theorem | isomgrref 45776 | The isomorphy relation is reflexive for hypergraphs. (Contributed by AV, 11-Nov-2022.) |
β’ (πΊ β UHGraph β πΊ IsomGr πΊ) | ||
Theorem | isomgrsym 45777 | The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) |
β’ ((π΄ β UHGraph β§ π΅ β π) β (π΄ IsomGr π΅ β π΅ IsomGr π΄)) | ||
Theorem | isomgrsymb 45778 | The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022.) |
β’ ((π΄ β UHGraph β§ π΅ β UHGraph) β (π΄ IsomGr π΅ β π΅ IsomGr π΄)) | ||
Theorem | isomgrtrlem 45779* | Lemma for isomgrtr 45780. (Contributed by AV, 5-Dec-2022.) |
β’ (((((π΄ β UHGraph β§ π΅ β UHGraph β§ πΆ β π) β§ π:(Vtxβπ΄)β1-1-ontoβ(Vtxβπ΅) β§ π£:(Vtxβπ΅)β1-1-ontoβ(VtxβπΆ)) β§ (π:dom (iEdgβπ΄)β1-1-ontoβdom (iEdgβπ΅) β§ βπ β dom (iEdgβπ΄)(π β ((iEdgβπ΄)βπ)) = ((iEdgβπ΅)β(πβπ)))) β§ (π€:dom (iEdgβπ΅)β1-1-ontoβdom (iEdgβπΆ) β§ βπ β dom (iEdgβπ΅)(π£ β ((iEdgβπ΅)βπ)) = ((iEdgβπΆ)β(π€βπ)))) β βπ β dom (iEdgβπ΄)((π£ β π) β ((iEdgβπ΄)βπ)) = ((iEdgβπΆ)β((π€ β π)βπ))) | ||
Theorem | isomgrtr 45780 | The isomorphy relation is transitive for hypergraphs. (Contributed by AV, 5-Dec-2022.) |
β’ ((π΄ β UHGraph β§ π΅ β UHGraph β§ πΆ β π) β ((π΄ IsomGr π΅ β§ π΅ IsomGr πΆ) β π΄ IsomGr πΆ)) | ||
Theorem | strisomgrop 45781 | A graph represented as an extensible structure with vertices as base set and indexed edges is isomorphic to a hypergraph represented as ordered pair with the same vertices and edges. (Contributed by AV, 11-Nov-2022.) |
β’ πΊ = β¨π, πΈβ© & β’ π» = {β¨(Baseβndx), πβ©, β¨(.efβndx), πΈβ©} β β’ ((πΊ β UHGraph β§ π β π β§ πΈ β π) β πΊ IsomGr π») | ||
Theorem | ushrisomgr 45782 | A simple hypergraph (with arbitrarily indexed edges) is isomorphic to a graph with the same vertices and the same edges, indexed by the edges themselves. (Contributed by AV, 11-Nov-2022.) |
β’ π = (VtxβπΊ) & β’ πΈ = (EdgβπΊ) & β’ π» = β¨π, ( I βΎ πΈ)β© β β’ (πΊ β USHGraph β πΊ IsomGr π») | ||
Theorem | 1hegrlfgr 45783* | A graph πΊ with one hyperedge joining at least two vertices is a loop-free graph. (Contributed by AV, 23-Feb-2021.) |
β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π΅ β πΆ) & β’ (π β πΈ β π« π) & β’ (π β (iEdgβπΊ) = {β¨π΄, πΈβ©}) & β’ (π β {π΅, πΆ} β πΈ) β β’ (π β (iEdgβπΊ):{π΄}βΆ{π₯ β π« π β£ 2 β€ (β―βπ₯)}) | ||
Syntax | cupwlks 45784 | Extend class notation with walks (of a pseudograph). |
class UPWalks | ||
Definition | df-upwlks 45785* |
Define the set of all walks (in a pseudograph), called "simple walks"
in
the following.
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A walk of length k in a graph is an alternating sequence of vertices and edges, v0 , e0 , v1 , e1 , v2 , ... , v(k-1) , e(k-1) , v(k) which begins and ends with vertices. If the graph is undirected, then the endpoints of e(i) are v(i) and v(i+1)." According to Bollobas: " A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4. Therefore, a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Although this definition is also applicable for arbitrary hypergraphs, it allows only walks consisting of not proper hyperedges (i.e. edges connecting at most two vertices). Therefore, it should be used for pseudographs only. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
β’ UPWalks = (π β V β¦ {β¨π, πβ© β£ (π β Word dom (iEdgβπ) β§ π:(0...(β―βπ))βΆ(Vtxβπ) β§ βπ β (0..^(β―βπ))((iEdgβπ)β(πβπ)) = {(πβπ), (πβ(π + 1))})}) | ||
Theorem | upwlksfval 45786* | The set of simple walks (in an undirected graph). (Contributed by Alexander van der Vekens, 19-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β π β (UPWalksβπΊ) = {β¨π, πβ© β£ (π β Word dom πΌ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΌβ(πβπ)) = {(πβπ), (πβ(π + 1))})}) | ||
Theorem | isupwlk 45787* | Properties of a pair of functions to be a simple walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β π β§ πΉ β π β§ π β π) β (πΉ(UPWalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) | ||
Theorem | isupwlkg 45788* | Generalization of isupwlk 45787: Conditions for two classes to represent a simple walk. (Contributed by AV, 5-Nov-2021.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΊ β π β (πΉ(UPWalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) | ||
Theorem | upwlkbprop 45789 | Basic properties of a simple walk. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 29-Dec-2020.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ (πΉ(UPWalksβπΊ)π β (πΊ β V β§ πΉ β V β§ π β V)) | ||
Theorem | upwlkwlk 45790 | A simple walk is a walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 27-Feb-2021.) |
β’ (πΉ(UPWalksβπΊ)π β πΉ(WalksβπΊ)π) | ||
Theorem | upgrwlkupwlk 45791 | In a pseudograph, a walk is a simple walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 2-Jan-2021.) |
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π) β πΉ(UPWalksβπΊ)π) | ||
Theorem | upgrwlkupwlkb 45792 | In a pseudograph, the definitions for a walk and a simple walk are equivalent. (Contributed by AV, 30-Dec-2020.) |
β’ (πΊ β UPGraph β (πΉ(WalksβπΊ)π β πΉ(UPWalksβπΊ)π)) | ||
Theorem | upgrisupwlkALT 45793* | Alternate proof of upgriswlk 28387 using the definition of UPGraph and related theorems. (Contributed by AV, 2-Jan-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (VtxβπΊ) & β’ πΌ = (iEdgβπΊ) β β’ ((πΊ β UPGraph β§ πΉ β π β§ π β π) β (πΉ(WalksβπΊ)π β (πΉ β Word dom πΌ β§ π:(0...(β―βπΉ))βΆπ β§ βπ β (0..^(β―βπΉ))(πΌβ(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) | ||
Theorem | upgredgssspr 45794 | The set of edges of a pseudograph is a subset of the set of unordered pairs of vertices. (Contributed by AV, 24-Nov-2021.) |
β’ (πΊ β UPGraph β (EdgβπΊ) β (Pairsβ(VtxβπΊ))) | ||
Theorem | uspgropssxp 45795* | The set πΊ of "simple pseudographs" for a fixed set π of vertices is a subset of a Cartesian product. For more details about the class πΊ of all "simple pseudographs" see comments on uspgrbisymrel 45805. (Contributed by AV, 24-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} β β’ (π β π β πΊ β (π Γ π)) | ||
Theorem | uspgrsprfv 45796* | The value of the function πΉ which maps a "simple pseudograph" for a fixed set π of vertices to the set of edges (i.e. range of the edge function) of the graph. Solely for πΊ as defined here, the function πΉ is a bijection between the "simple pseudographs" and the subsets of the set of pairs π over the fixed set π of vertices, see uspgrbispr 45802. (Contributed by AV, 24-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ (π β πΊ β (πΉβπ) = (2nd βπ)) | ||
Theorem | uspgrsprf 45797* | The mapping πΉ is a function from the "simple pseudographs" with a fixed set of vertices π into the subsets of the set of pairs over the set π. (Contributed by AV, 24-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ πΉ:πΊβΆπ | ||
Theorem | uspgrsprf1 45798* | The mapping πΉ is a one-to-one function from the "simple pseudographs" with a fixed set of vertices π into the subsets of the set of pairs over the set π. (Contributed by AV, 25-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ πΉ:πΊβ1-1βπ | ||
Theorem | uspgrsprfo 45799* | The mapping πΉ is a function from the "simple pseudographs" with a fixed set of vertices π onto the subsets of the set of pairs over the set π. (Contributed by AV, 25-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ (π β π β πΉ:πΊβontoβπ) | ||
Theorem | uspgrsprf1o 45800* | The mapping πΉ is a bijection between the "simple pseudographs" with a fixed set of vertices π and the subsets of the set of pairs over the set π. See also the comments on uspgrbisymrel 45805. (Contributed by AV, 25-Nov-2021.) |
β’ π = π« (Pairsβπ) & β’ πΊ = {β¨π£, πβ© β£ (π£ = π β§ βπ β USPGraph ((Vtxβπ) = π£ β§ (Edgβπ) = π))} & β’ πΉ = (π β πΊ β¦ (2nd βπ)) β β’ (π β π β πΉ:πΊβ1-1-ontoβπ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |