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

Metamath Proof Explorer

Definition df-gbo

Description: Define the set of (strong) odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of threeodd primes. By this definition, the strong ternary Goldbach conjecture can be expressed as A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) . (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion df-gbo GoldbachOdd = { 𝑧 ∈ Odd ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgbo ⊢ GoldbachOdd
1 vz ⊢ 𝑧
2 codd ⊢ Odd
3 vp ⊢ 𝑝
4 cprime ⊢ ℙ
5 vq ⊢ 𝑞
6 vr ⊢ 𝑟
7 3 cv ⊢ 𝑝
8 7 2 wcel ⊢ 𝑝 ∈ Odd
9 5 cv ⊢ 𝑞
10 9 2 wcel ⊢ 𝑞 ∈ Odd
11 6 cv ⊢ 𝑟
12 11 2 wcel ⊢ 𝑟 ∈ Odd
13 8 10 12 w3a ⊢ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd )
14 1 cv ⊢ 𝑧
15 caddc ⊢ +
16 7 9 15 co ⊢ ( 𝑝 + 𝑞 )
17 16 11 15 co ⊢ ( ( 𝑝 + 𝑞 ) + 𝑟 )
18 14 17 wceq ⊢ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 )
19 13 18 wa ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
20 19 6 4 wrex ⊢ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
21 20 5 4 wrex ⊢ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
22 21 3 4 wrex ⊢ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
23 22 1 2 crab ⊢ { 𝑧 ∈ Odd ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) }
24 0 23 wceq ⊢ GoldbachOdd = { 𝑧 ∈ Odd ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) }