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

Metamath Proof Explorer

Theorem isgbo

Description: The predicate "is an odd Goldbach number". An odd Goldbach number is an odd integer having a Goldbach partition, i.e. which can be written as sum of three odd primes. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion isgbo ( 𝑍 ∈ GoldbachOdd ↔ ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑧 = 𝑍 → ( 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
2 1 anbi2d ⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
3 2 rexbidv ⊢ ( 𝑧 = 𝑍 → ( ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
4 3 2rexbidv ⊢ ( 𝑧 = 𝑍 → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
5 df-gbo ⊢ GoldbachOdd = { 𝑧 ∈ Odd ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) }
6 4 5 elrab2 ⊢ ( 𝑍 ∈ GoldbachOdd ↔ ( 𝑍 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )