Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gbo Structured version   Visualization version   GIF version

Definition df-gbo 43922
 Description: Define the set of (strong) odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of three odd primes. By this definition, the strong ternary Goldbach conjecture can be expressed as ∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ). (Contributed by AV, 26-Jul-2020.)
Assertion
Ref Expression
df-gbo GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
Distinct variable group:   𝑧,𝑝,𝑞,𝑟

Detailed syntax breakdown of Definition df-gbo
StepHypRef Expression
1 cgbo 43919 . 2 class GoldbachOdd
2 vp . . . . . . . . . 10 setvar 𝑝
32cv 1536 . . . . . . . . 9 class 𝑝
4 codd 43797 . . . . . . . . 9 class Odd
53, 4wcel 2114 . . . . . . . 8 wff 𝑝 ∈ Odd
6 vq . . . . . . . . . 10 setvar 𝑞
76cv 1536 . . . . . . . . 9 class 𝑞
87, 4wcel 2114 . . . . . . . 8 wff 𝑞 ∈ Odd
9 vr . . . . . . . . . 10 setvar 𝑟
109cv 1536 . . . . . . . . 9 class 𝑟
1110, 4wcel 2114 . . . . . . . 8 wff 𝑟 ∈ Odd
125, 8, 11w3a 1083 . . . . . . 7 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )
13 vz . . . . . . . . 9 setvar 𝑧
1413cv 1536 . . . . . . . 8 class 𝑧
15 caddc 10542 . . . . . . . . . 10 class +
163, 7, 15co 7158 . . . . . . . . 9 class (𝑝 + 𝑞)
1716, 10, 15co 7158 . . . . . . . 8 class ((𝑝 + 𝑞) + 𝑟)
1814, 17wceq 1537 . . . . . . 7 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1912, 18wa 398 . . . . . 6 wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
20 cprime 16017 . . . . . 6 class
2119, 9, 20wrex 3141 . . . . 5 wff 𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2221, 6, 20wrex 3141 . . . 4 wff 𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2322, 2, 20wrex 3141 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2423, 13, 4crab 3144 . 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
251, 24wceq 1537 1 wff GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
 Colors of variables: wff setvar class This definition is referenced by:  isgbo  43925  tgoldbachgtALTV  43984
 Copyright terms: Public domain W3C validator