gbowpos

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

		Ref	Expression
	Assertion	gbowpos	$⊢ Z \in GoldbachOddW \to Z \in ℕ$

Step	Hyp	Ref	Expression
1		isgbow	$⊢ Z \in GoldbachOddW \leftrightarrow (Z \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ Z = p + q + r)$
2		prmnn	$⊢ p \in ℙ \to p \in ℕ$
3		prmnn	$⊢ q \in ℙ \to q \in ℕ$
4	2 3	anim12i	$⊢ (p \in ℙ \land q \in ℙ) \to (p \in ℕ \land q \in ℕ)$
5	4	adantr	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to (p \in ℕ \land q \in ℕ)$
6		nnaddcl	$⊢ (p \in ℕ \land q \in ℕ) \to p + q \in ℕ$
7	5 6	syl	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to p + q \in ℕ$
8		prmnn	$⊢ r \in ℙ \to r \in ℕ$
9	8	adantl	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to r \in ℕ$
10	7 9	nnaddcld	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to p + q + r \in ℕ$
11		eleq1	$⊢ Z = p + q + r \to (Z \in ℕ \leftrightarrow p + q + r \in ℕ)$
12	10 11	syl5ibrcom	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to (Z = p + q + r \to Z \in ℕ)$
13	12	rexlimdva	$⊢ (p \in ℙ \land q \in ℙ) \to (\exists r \in ℙ Z = p + q + r \to Z \in ℕ)$
14	13	a1i	$⊢ Z \in Odd \to ((p \in ℙ \land q \in ℙ) \to (\exists r \in ℙ Z = p + q + r \to Z \in ℕ))$
15	14	rexlimdvv	$⊢ Z \in Odd \to (\exists p \in ℙ \exists q \in ℙ \exists r \in ℙ Z = p + q + r \to Z \in ℕ)$
16	15	imp	$⊢ (Z \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ Z = p + q + r) \to Z \in ℕ$
17	1 16	sylbi	$⊢ Z \in GoldbachOddW \to Z \in ℕ$

Metamath Proof Explorer