Metamath Proof Explorer


Definition df-gbow

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 A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) . (Contributed by AV, 14-Jun-2020)

Ref Expression
Assertion df-gbow GoldbachOddW = { 𝑧 ∈ Odd ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgbow GoldbachOddW
1 vz 𝑧
2 codd Odd
3 vp 𝑝
4 cprime
5 vq 𝑞
6 vr 𝑟
7 1 cv 𝑧
8 3 cv 𝑝
9 caddc +
10 5 cv 𝑞
11 8 10 9 co ( 𝑝 + 𝑞 )
12 6 cv 𝑟
13 11 12 9 co ( ( 𝑝 + 𝑞 ) + 𝑟 )
14 7 13 wceq 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 )
15 14 6 4 wrex 𝑟 ∈ ℙ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 )
16 15 5 4 wrex 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 )
17 16 3 4 wrex 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 )
18 17 1 2 crab { 𝑧 ∈ Odd ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) }
19 0 18 wceq GoldbachOddW = { 𝑧 ∈ Odd ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) }