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 40929
Description: Define the set of odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of three primes. By this definition, the (weak) ternary Goldbach conjecture can be expressed as 𝑚 ∈ Odd (5 < 𝑚𝑚 ∈ GoldbachOdd ). (Contributed by AV, 14-Jun-2020.)
Assertion
Ref Expression
df-gbo GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}
Distinct variable group:   𝑧,𝑝,𝑞,𝑟

Detailed syntax breakdown of Definition df-gbo
StepHypRef Expression
1 cgbo 40926 . 2 class GoldbachOdd
2 vz . . . . . . . 8 setvar 𝑧
32cv 1479 . . . . . . 7 class 𝑧
4 vp . . . . . . . . . 10 setvar 𝑝
54cv 1479 . . . . . . . . 9 class 𝑝
6 vq . . . . . . . . . 10 setvar 𝑞
76cv 1479 . . . . . . . . 9 class 𝑞
8 caddc 9883 . . . . . . . . 9 class +
95, 7, 8co 6604 . . . . . . . 8 class (𝑝 + 𝑞)
10 vr . . . . . . . . 9 setvar 𝑟
1110cv 1479 . . . . . . . 8 class 𝑟
129, 11, 8co 6604 . . . . . . 7 class ((𝑝 + 𝑞) + 𝑟)
133, 12wceq 1480 . . . . . 6 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
14 cprime 15309 . . . . . 6 class
1513, 10, 14wrex 2908 . . . . 5 wff 𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1615, 6, 14wrex 2908 . . . 4 wff 𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1716, 4, 14wrex 2908 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
18 codd 40834 . . 3 class Odd
1917, 2, 18crab 2911 . 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}
201, 19wceq 1480 1 wff GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}
Colors of variables: wff setvar class
This definition is referenced by:  isgbo  40932
  Copyright terms: Public domain W3C validator