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 43921
 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 43918 . 2 class GoldbachOddW
2 vz . . . . . . . 8 setvar 𝑧
32cv 1535 . . . . . . 7 class 𝑧
4 vp . . . . . . . . . 10 setvar 𝑝
54cv 1535 . . . . . . . . 9 class 𝑝
6 vq . . . . . . . . . 10 setvar 𝑞
76cv 1535 . . . . . . . . 9 class 𝑞
8 caddc 10543 . . . . . . . . 9 class +
95, 7, 8co 7159 . . . . . . . 8 class (𝑝 + 𝑞)
10 vr . . . . . . . . 9 setvar 𝑟
1110cv 1535 . . . . . . . 8 class 𝑟
129, 11, 8co 7159 . . . . . . 7 class ((𝑝 + 𝑞) + 𝑟)
133, 12wceq 1536 . . . . . 6 wff 𝑧 = ((𝑝 + 𝑞) + 𝑟)
14 cprime 16018 . . . . . 6 class
1513, 10, 14wrex 3142 . . . . 5 wff 𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1615, 6, 14wrex 3142 . . . 4 wff 𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
1716, 4, 14wrex 3142 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)
18 codd 43797 . . 3 class Odd
1917, 2, 18crab 3145 . 2 class {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}
201, 19wceq 1536 1 wff GoldbachOddW = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}
 Colors of variables: wff setvar class This definition is referenced by:  isgbow  43924
 Copyright terms: Public domain W3C validator