Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gbe Structured version   Visualization version   GIF version

Definition df-gbe 40170
 Description: Define the set of (even) Goldbach numbers, which are positive even integers that can be expressed as the sum of two odd primes. By this definition, the binary Goldbach conjecture can be expressed as ∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ). (Contributed by AV, 14-Jun-2020.)
Assertion
Ref Expression
df-gbe GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
Distinct variable group:   𝑧,𝑝,𝑞

Detailed syntax breakdown of Definition df-gbe
StepHypRef Expression
1 cgbe 40167 . 2 class GoldbachEven
2 vp . . . . . . . 8 setvar 𝑝
32cv 1474 . . . . . . 7 class 𝑝
4 codd 40076 . . . . . . 7 class Odd
53, 4wcel 1977 . . . . . 6 wff 𝑝 ∈ Odd
6 vq . . . . . . . 8 setvar 𝑞
76cv 1474 . . . . . . 7 class 𝑞
87, 4wcel 1977 . . . . . 6 wff 𝑞 ∈ Odd
9 vz . . . . . . . 8 setvar 𝑧
109cv 1474 . . . . . . 7 class 𝑧
11 caddc 9818 . . . . . . . 8 class +
123, 7, 11co 6549 . . . . . . 7 class (𝑝 + 𝑞)
1310, 12wceq 1475 . . . . . 6 wff 𝑧 = (𝑝 + 𝑞)
145, 8, 13w3a 1031 . . . . 5 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
15 cprime 15223 . . . . 5 class
1614, 6, 15wrex 2897 . . . 4 wff 𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
1716, 2, 15wrex 2897 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
18 ceven 40075 . . 3 class Even
1917, 9, 18crab 2900 . 2 class {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
201, 19wceq 1475 1 wff GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
 Colors of variables: wff setvar class This definition is referenced by:  isgbe  40173
 Copyright terms: Public domain W3C validator