Metamath Proof Explorer

Theorem gbepos

Description: Any even Goldbach number is positive. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion gbepos ⊢ Z ∈ GoldbachEven → Z ∈ ℕ

Proof

Step Hyp Ref Expression
1 isgbe ⊢ Z ∈ GoldbachEven ↔ Z ∈ Even ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ Z = p + q
2 prmnn ⊢ p ∈ ℙ → p ∈ ℕ
3 prmnn ⊢ q ∈ ℙ → q ∈ ℕ
4 nnaddcl ⊢ p ∈ ℕ ∧ q ∈ ℕ → p + q ∈ ℕ
5 2 3 4 syl2an ⊢ p ∈ ℙ ∧ q ∈ ℙ → p + q ∈ ℕ
6 eleq1 ⊢ Z = p + q → Z ∈ ℕ ↔ p + q ∈ ℕ
7 5 6 imbitrrid ⊢ Z = p + q → p ∈ ℙ ∧ q ∈ ℙ → Z ∈ ℕ
8 7 3ad2ant3 ⊢ p ∈ Odd ∧ q ∈ Odd ∧ Z = p + q → p ∈ ℙ ∧ q ∈ ℙ → Z ∈ ℕ
9 8 com12 ⊢ p ∈ ℙ ∧ q ∈ ℙ → p ∈ Odd ∧ q ∈ Odd ∧ Z = p + q → Z ∈ ℕ
10 9 a1i ⊢ Z ∈ Even → p ∈ ℙ ∧ q ∈ ℙ → p ∈ Odd ∧ q ∈ Odd ∧ Z = p + q → Z ∈ ℕ
11 10 rexlimdvv ⊢ Z ∈ Even → ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ Z = p + q → Z ∈ ℕ
12 11 imp ⊢ Z ∈ Even ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ Z = p + q → Z ∈ ℕ
13 1 12 sylbi ⊢ Z ∈ GoldbachEven → Z ∈ ℕ