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

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 ( 𝑍 ∈ GoldbachOdd → 𝑍 ∈ GoldbachOddW )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
2 1 reximi ⊢ ( ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
3 2 reximi ⊢ ( ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
4 3 reximi ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
5 4 anim2i ⊢ ( ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) → ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
6 isgbo ⊢ ( 𝑍 ∈ GoldbachOdd ↔ ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
7 isgbow ⊢ ( 𝑍 ∈ GoldbachOddW ↔ ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
8 5 6 7 3imtr4i ⊢ ( 𝑍 ∈ GoldbachOdd → 𝑍 ∈ GoldbachOddW )