Metamath Proof Explorer

Theorem gbogbow

Description: A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion gbogbow ⊢ Z ∈ GoldbachOdd → Z ∈ GoldbachOddW

Proof

Step Hyp Ref Expression
1 simpr ⊢ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ Z = p + q + r → Z = p + q + r
2 1 reximi ⊢ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ Z = p + q + r → ∃ r ∈ ℙ Z = p + q + r
3 2 reximi ⊢ ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ Z = p + q + r → ∃ q ∈ ℙ ∃ r ∈ ℙ Z = p + q + r
4 3 reximi ⊢ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ Z = p + q + r → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ Z = p + q + r
5 4 anim2i ⊢ Z ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ Z = p + q + r → Z ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ Z = p + q + r
6 isgbo ⊢ Z ∈ GoldbachOdd ↔ Z ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ Z = p + q + r
7 isgbow ⊢ Z ∈ GoldbachOddW ↔ Z ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ Z = p + q + r
8 5 6 7 3imtr4i ⊢ Z ∈ GoldbachOdd → Z ∈ GoldbachOddW