Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gbow Structured version   Visualization version   GIF version

Definition df-gbow 47091
Description: Define the set of weak 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 < 𝑚𝑚 ∈ GoldbachOddW ). (Contributed by AV, 14-Jun-2020.)
Assertion
Ref Expression
df-gbow GoldbachOddW = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}
Distinct variable group:   𝑧,𝑝,𝑞,𝑟

Detailed syntax breakdown of Definition df-gbow
StepHypRef Expression
1 cgbow 47088 . 2 class GoldbachOddW
2 vz . . . . . . . 8 setvar 𝑧
32cv 1532 . . . . . . 7 class 𝑧
4 vp . . . . . . . . . 10 setvar 𝑝
54cv 1532 . . . . . . . . 9 class 𝑝
6 vq . . . . . . . . . 10 setvar 𝑞
76cv 1532 . . . . . . . . 9 class 𝑞
8 caddc 11147 . . . . . . . . 9 class +
95, 7, 8co 7424 . . . . . . . 8 class (𝑝 + 𝑞)
10 vr . . . . . . . . 9 setvar 𝑟
1110cv 1532 . . . . . . . 8 class 𝑟
129, 11, 8co 7424 . . . . . . 7 class ((𝑝 + 𝑞) + 𝑟)
133, 12wceq 1533 . . . . . 6 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
14 cprime 16647 . . . . . 6 class
1513, 10, 14wrex 3066 . . . . 5 wff 𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1615, 6, 14wrex 3066 . . . 4 wff 𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1716, 4, 14wrex 3066 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
18 codd 46967 . . 3 class Odd
1917, 2, 18crab 3428 . 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}
201, 19wceq 1533 1 wff GoldbachOddW = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}
Colors of variables: wff setvar class
This definition is referenced by:  isgbow  47094
  Copyright terms: Public domain W3C validator