Metamath Proof Explorer

Definition df-gbo

Description: Define the set of (strong) odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of threeodd primes. By this definition, the strong ternary Goldbach conjecture can be expressed as A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) . (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion df-gbo ⊢ GoldbachOdd = z ∈ Odd | ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ z = p + q + r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgbo class GoldbachOdd
1 vz setvar z
2 codd class Odd
3 vp setvar p
4 cprime class ℙ
5 vq setvar q
6 vr setvar r
7 3 cv setvar p
8 7 2 wcel wff p ∈ Odd
9 5 cv setvar q
10 9 2 wcel wff q ∈ Odd
11 6 cv setvar r
12 11 2 wcel wff r ∈ Odd
13 8 10 12 w3a wff p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd
14 1 cv setvar z
15 caddc class +
16 7 9 15 co class p + q
17 16 11 15 co class p + q + r
18 14 17 wceq wff z = p + q + r
19 13 18 wa wff p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ z = p + q + r
20 19 6 4 wrex wff ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ z = p + q + r
21 20 5 4 wrex wff ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ z = p + q + r
22 21 3 4 wrex wff ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ z = p + q + r
23 22 1 2 crab class z ∈ Odd | ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ z = p + q + r
24 0 23 wceq wff GoldbachOdd = z ∈ Odd | ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ z = p + q + r