Metamath Proof Explorer

Theorem isgbow

Description: The predicate "is a weak odd Goldbach number". A weak odd Goldbach number is an odd integer having a Goldbach partition, i.e. which can be written as a sum of three primes. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion isgbow ⊢Z∈GoldbachOddW↔Z∈Odd∧∃p∈ℙ∃q∈ℙ∃r∈ℙZ=p+q+r

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢z=Z→z=p+q+r↔Z=p+q+r
2 1 rexbidv ⊢z=Z→∃r∈ℙz=p+q+r↔∃r∈ℙZ=p+q+r
3 2 2rexbidv ⊢z=Z→∃p∈ℙ∃q∈ℙ∃r∈ℙz=p+q+r↔∃p∈ℙ∃q∈ℙ∃r∈ℙZ=p+q+r
4 df-gbow ⊢GoldbachOddW=z∈Odd|∃p∈ℙ∃q∈ℙ∃r∈ℙz=p+q+r
5 3 4 elrab2 ⊢Z∈GoldbachOddW↔Z∈Odd∧∃p∈ℙ∃q∈ℙ∃r∈ℙZ=p+q+r