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 47675
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 47672 . 2 class GoldbachOdd
2 vp . . . . . . . . . 10 setvar 𝑝
32cv 1536 . . . . . . . . 9 class 𝑝
4 codd 47550 . . . . . . . . 9 class Odd
53, 4wcel 2106 . . . . . . . 8 wff 𝑝 ∈ Odd
6 vq . . . . . . . . . 10 setvar 𝑞
76cv 1536 . . . . . . . . 9 class 𝑞
87, 4wcel 2106 . . . . . . . 8 wff 𝑞 ∈ Odd
9 vr . . . . . . . . . 10 setvar 𝑟
109cv 1536 . . . . . . . . 9 class 𝑟
1110, 4wcel 2106 . . . . . . . 8 wff 𝑟 ∈ Odd
125, 8, 11w3a 1086 . . . . . . 7 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )
13 vz . . . . . . . . 9 setvar 𝑧
1413cv 1536 . . . . . . . 8 class 𝑧
15 caddc 11156 . . . . . . . . . 10 class +
163, 7, 15co 7431 . . . . . . . . 9 class (𝑝 + 𝑞)
1716, 10, 15co 7431 . . . . . . . 8 class ((𝑝 + 𝑞) + 𝑟)
1814, 17wceq 1537 . . . . . . 7 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1912, 18wa 395 . . . . . 6 wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
20 cprime 16705 . . . . . 6 class
2119, 9, 20wrex 3068 . . . . 5 wff 𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2221, 6, 20wrex 3068 . . . 4 wff 𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2322, 2, 20wrex 3068 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2423, 13, 4crab 3433 . 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  47678  tgoldbachgtALTV  47737
  Copyright terms: Public domain W3C validator