Metamath Proof Explorer

Theorem gbowpos

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

Ref Expression
Assertion gbowpos ⊢ Z ∈ GoldbachOddW → Z ∈ ℕ

Proof

Step Hyp Ref Expression
1 isgbow ⊢ Z ∈ GoldbachOddW ↔ Z ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ Z = p + q + r
2 prmnn ⊢ p ∈ ℙ → p ∈ ℕ
3 prmnn ⊢ q ∈ ℙ → q ∈ ℕ
4 2 3 anim12i ⊢ p ∈ ℙ ∧ q ∈ ℙ → p ∈ ℕ ∧ q ∈ ℕ
5 4 adantr ⊢ p ∈ ℙ ∧ q ∈ ℙ ∧ r ∈ ℙ → p ∈ ℕ ∧ q ∈ ℕ
6 nnaddcl ⊢ p ∈ ℕ ∧ q ∈ ℕ → p + q ∈ ℕ
7 5 6 syl ⊢ p ∈ ℙ ∧ q ∈ ℙ ∧ r ∈ ℙ → p + q ∈ ℕ
8 prmnn ⊢ r ∈ ℙ → r ∈ ℕ
9 8 adantl ⊢ p ∈ ℙ ∧ q ∈ ℙ ∧ r ∈ ℙ → r ∈ ℕ
10 7 9 nnaddcld ⊢ p ∈ ℙ ∧ q ∈ ℙ ∧ r ∈ ℙ → p + q + r ∈ ℕ
11 eleq1 ⊢ Z = p + q + r → Z ∈ ℕ ↔ p + q + r ∈ ℕ
12 10 11 syl5ibrcom ⊢ p ∈ ℙ ∧ q ∈ ℙ ∧ r ∈ ℙ → Z = p + q + r → Z ∈ ℕ
13 12 rexlimdva ⊢ p ∈ ℙ ∧ q ∈ ℙ → ∃ r ∈ ℙ Z = p + q + r → Z ∈ ℕ
14 13 a1i ⊢ Z ∈ Odd → p ∈ ℙ ∧ q ∈ ℙ → ∃ r ∈ ℙ Z = p + q + r → Z ∈ ℕ
15 14 rexlimdvv ⊢ Z ∈ Odd → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ Z = p + q + r → Z ∈ ℕ
16 15 imp ⊢ Z ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ Z = p + q + r → Z ∈ ℕ
17 1 16 sylbi ⊢ Z ∈ GoldbachOddW → Z ∈ ℕ