This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isgbe

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

Ref Expression
Assertion isgbe ⊢ Z ∈ GoldbachEven ↔ Z ∈ Even ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ Z = p + q

Proof

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