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 39954
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 39951 . 2 class GoldbachEven
2 vp . . . . . . . 8 setvar 𝑝
32cv 1473 . . . . . . 7 class 𝑝
4 codd 39860 . . . . . . 7 class Odd
53, 4wcel 1976 . . . . . 6 wff 𝑝 ∈ Odd
6 vq . . . . . . . 8 setvar 𝑞
76cv 1473 . . . . . . 7 class 𝑞
87, 4wcel 1976 . . . . . 6 wff 𝑞 ∈ Odd
9 vz . . . . . . . 8 setvar 𝑧
109cv 1473 . . . . . . 7 class 𝑧
11 caddc 9795 . . . . . . . 8 class +
123, 7, 11co 6526 . . . . . . 7 class (𝑝 + 𝑞)
1310, 12wceq 1474 . . . . . 6 wff 𝑧 = (𝑝 + 𝑞)
145, 8, 13w3a 1030 . . . . 5 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
15 cprime 15171 . . . . 5 class
1614, 6, 15wrex 2896 . . . 4 wff 𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
1716, 2, 15wrex 2896 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
18 ceven 39859 . . 3 class Even
1917, 9, 18crab 2899 . 2 class {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
201, 19wceq 1474 1 wff GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
Colors of variables: wff setvar class
This definition is referenced by:  isgbe  39957
  Copyright terms: Public domain W3C validator