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

Metamath Proof Explorer

Theorem gbepos

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

Ref Expression
Assertion gbepos ( 𝑍 ∈ GoldbachEven → 𝑍 ∈ ℕ )

Proof

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