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

Metamath Proof Explorer

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