gbepos

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

		Ref	Expression
	Assertion	gbepos	$⊢ Z \in GoldbachEven \to Z \in ℕ$

Step	Hyp	Ref	Expression
1		isgbe	$⊢ Z \in GoldbachEven \leftrightarrow (Z \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land Z = p + q))$
2		prmnn	$⊢ p \in ℙ \to p \in ℕ$
3		prmnn	$⊢ q \in ℙ \to q \in ℕ$
4		nnaddcl	$⊢ (p \in ℕ \land q \in ℕ) \to p + q \in ℕ$
5	2 3 4	syl2an	$⊢ (p \in ℙ \land q \in ℙ) \to p + q \in ℕ$
6		eleq1	$⊢ Z = p + q \to (Z \in ℕ \leftrightarrow p + q \in ℕ)$
7	5 6	imbitrrid	$⊢ Z = p + q \to ((p \in ℙ \land q \in ℙ) \to Z \in ℕ)$
8	7	3ad2ant3	$⊢ (p \in Odd \land q \in Odd \land Z = p + q) \to ((p \in ℙ \land q \in ℙ) \to Z \in ℕ)$
9	8	com12	$⊢ (p \in ℙ \land q \in ℙ) \to ((p \in Odd \land q \in Odd \land Z = p + q) \to Z \in ℕ)$
10	9	a1i	$⊢ Z \in Even \to ((p \in ℙ \land q \in ℙ) \to ((p \in Odd \land q \in Odd \land Z = p + q) \to Z \in ℕ))$
11	10	rexlimdvv	$⊢ Z \in Even \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land Z = p + q) \to Z \in ℕ)$
12	11	imp	$⊢ (Z \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land Z = p + q)) \to Z \in ℕ$
13	1 12	sylbi	$⊢ Z \in GoldbachEven \to Z \in ℕ$

Metamath Proof Explorer