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 46714
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 46711 . 2 class GoldbachEven
2 vp . . . . . . . 8 setvar 𝑝
32cv 1538 . . . . . . 7 class 𝑝
4 codd 46591 . . . . . . 7 class Odd
53, 4wcel 2104 . . . . . 6 wff 𝑝 ∈ Odd
6 vq . . . . . . . 8 setvar 𝑞
76cv 1538 . . . . . . 7 class 𝑞
87, 4wcel 2104 . . . . . 6 wff 𝑞 ∈ Odd
9 vz . . . . . . . 8 setvar 𝑧
109cv 1538 . . . . . . 7 class 𝑧
11 caddc 11115 . . . . . . . 8 class +
123, 7, 11co 7411 . . . . . . 7 class (𝑝 + 𝑞)
1310, 12wceq 1539 . . . . . 6 wff 𝑧 = (𝑝 + 𝑞)
145, 8, 13w3a 1085 . . . . 5 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
15 cprime 16612 . . . . 5 class
1614, 6, 15wrex 3068 . . . 4 wff 𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
1716, 2, 15wrex 3068 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
18 ceven 46590 . . 3 class Even
1917, 9, 18crab 3430 . 2 class {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
201, 19wceq 1539 1 wff GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
Colors of variables: wff setvar class
This definition is referenced by:  isgbe  46717
  Copyright terms: Public domain W3C validator