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 47737
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 47734 . 2 class GoldbachOdd
2 vp . . . . . . . . . 10 setvar 𝑝
32cv 1539 . . . . . . . . 9 class 𝑝
4 codd 47612 . . . . . . . . 9 class Odd
53, 4wcel 2108 . . . . . . . 8 wff 𝑝 ∈ Odd
6 vq . . . . . . . . . 10 setvar 𝑞
76cv 1539 . . . . . . . . 9 class 𝑞
87, 4wcel 2108 . . . . . . . 8 wff 𝑞 ∈ Odd
9 vr . . . . . . . . . 10 setvar 𝑟
109cv 1539 . . . . . . . . 9 class 𝑟
1110, 4wcel 2108 . . . . . . . 8 wff 𝑟 ∈ Odd
125, 8, 11w3a 1087 . . . . . . 7 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )
13 vz . . . . . . . . 9 setvar 𝑧
1413cv 1539 . . . . . . . 8 class 𝑧
15 caddc 11158 . . . . . . . . . 10 class +
163, 7, 15co 7431 . . . . . . . . 9 class (𝑝 + 𝑞)
1716, 10, 15co 7431 . . . . . . . 8 class ((𝑝 + 𝑞) + 𝑟)
1814, 17wceq 1540 . . . . . . 7 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1912, 18wa 395 . . . . . 6 wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
20 cprime 16708 . . . . . 6 class
2119, 9, 20wrex 3070 . . . . 5 wff 𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2221, 6, 20wrex 3070 . . . 4 wff 𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2322, 2, 20wrex 3070 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2423, 13, 4crab 3436 . 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
251, 24wceq 1540 1 wff GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
Colors of variables: wff setvar class
This definition is referenced by:  isgbo  47740  tgoldbachgtALTV  47799
  Copyright terms: Public domain W3C validator