Users' Mathboxes 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 47090
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 47087 . 2 class GoldbachOdd
2 vp . . . . . . . . . 10 setvar 𝑝
32cv 1533 . . . . . . . . 9 class 𝑝
4 codd 46965 . . . . . . . . 9 class Odd
53, 4wcel 2099 . . . . . . . 8 wff 𝑝 ∈ Odd
6 vq . . . . . . . . . 10 setvar 𝑞
76cv 1533 . . . . . . . . 9 class 𝑞
87, 4wcel 2099 . . . . . . . 8 wff 𝑞 ∈ Odd
9 vr . . . . . . . . . 10 setvar 𝑟
109cv 1533 . . . . . . . . 9 class 𝑟
1110, 4wcel 2099 . . . . . . . 8 wff 𝑟 ∈ Odd
125, 8, 11w3a 1085 . . . . . . 7 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )
13 vz . . . . . . . . 9 setvar 𝑧
1413cv 1533 . . . . . . . 8 class 𝑧
15 caddc 11142 . . . . . . . . . 10 class +
163, 7, 15co 7420 . . . . . . . . 9 class (𝑝 + 𝑞)
1716, 10, 15co 7420 . . . . . . . 8 class ((𝑝 + 𝑞) + 𝑟)
1814, 17wceq 1534 . . . . . . 7 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1912, 18wa 395 . . . . . 6 wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
20 cprime 16642 . . . . . 6 class
2119, 9, 20wrex 3067 . . . . 5 wff 𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2221, 6, 20wrex 3067 . . . 4 wff 𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2322, 2, 20wrex 3067 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2423, 13, 4crab 3429 . 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
251, 24wceq 1534 1 wff GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
Colors of variables: wff setvar class
This definition is referenced by:  isgbo  47093  tgoldbachgtALTV  47152
  Copyright terms: Public domain W3C validator