Theorem gbowpos

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

	Ref	Expression
Assertion	gbowpos	⊢ ( 𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ )

Proof

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