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 )