Users' Mathboxes 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 42161
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 42158 . 2 class GoldbachEven
2 vp . . . . . . . 8 setvar 𝑝
32cv 1630 . . . . . . 7 class 𝑝
4 codd 42063 . . . . . . 7 class Odd
53, 4wcel 2145 . . . . . 6 wff 𝑝 ∈ Odd
6 vq . . . . . . . 8 setvar 𝑞
76cv 1630 . . . . . . 7 class 𝑞
87, 4wcel 2145 . . . . . 6 wff 𝑞 ∈ Odd
9 vz . . . . . . . 8 setvar 𝑧
109cv 1630 . . . . . . 7 class 𝑧
11 caddc 10145 . . . . . . . 8 class +
123, 7, 11co 6796 . . . . . . 7 class (𝑝 + 𝑞)
1310, 12wceq 1631 . . . . . 6 wff 𝑧 = (𝑝 + 𝑞)
145, 8, 13w3a 1071 . . . . 5 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
15 cprime 15592 . . . . 5 class
1614, 6, 15wrex 3062 . . . 4 wff 𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
1716, 2, 15wrex 3062 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
18 ceven 42062 . . 3 class Even
1917, 9, 18crab 3065 . 2 class {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
201, 19wceq 1631 1 wff GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
Colors of variables: wff setvar class
This definition is referenced by:  isgbe  42164
  Copyright terms: Public domain W3C validator