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 42424
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 42421 . 2 class GoldbachOdd
2 vp . . . . . . . . . 10 setvar 𝑝
32cv 1652 . . . . . . . . 9 class 𝑝
4 codd 42324 . . . . . . . . 9 class Odd
53, 4wcel 2157 . . . . . . . 8 wff 𝑝 ∈ Odd
6 vq . . . . . . . . . 10 setvar 𝑞
76cv 1652 . . . . . . . . 9 class 𝑞
87, 4wcel 2157 . . . . . . . 8 wff 𝑞 ∈ Odd
9 vr . . . . . . . . . 10 setvar 𝑟
109cv 1652 . . . . . . . . 9 class 𝑟
1110, 4wcel 2157 . . . . . . . 8 wff 𝑟 ∈ Odd
125, 8, 11w3a 1108 . . . . . . 7 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )
13 vz . . . . . . . . 9 setvar 𝑧
1413cv 1652 . . . . . . . 8 class 𝑧
15 caddc 10231 . . . . . . . . . 10 class +
163, 7, 15co 6882 . . . . . . . . 9 class (𝑝 + 𝑞)
1716, 10, 15co 6882 . . . . . . . 8 class ((𝑝 + 𝑞) + 𝑟)
1814, 17wceq 1653 . . . . . . 7 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1912, 18wa 385 . . . . . 6 wff ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
20 cprime 15723 . . . . . 6 class
2119, 9, 20wrex 3094 . . . . 5 wff 𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2221, 6, 20wrex 3094 . . . 4 wff 𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2322, 2, 20wrex 3094 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))
2423, 13, 4crab 3097 . 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
251, 24wceq 1653 1 wff GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
Colors of variables: wff setvar class
This definition is referenced by:  isgbo  42427  tgoldbachgtALTV  42486
  Copyright terms: Public domain W3C validator