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 → 𝑍 ∈ ℕ )