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 46406
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 46403 . 2 class GoldbachEven
2 vp . . . . . . . 8 setvar 𝑝
32cv 1540 . . . . . . 7 class 𝑝
4 codd 46283 . . . . . . 7 class Odd
53, 4wcel 2106 . . . . . 6 wff 𝑝 ∈ Odd
6 vq . . . . . . . 8 setvar 𝑞
76cv 1540 . . . . . . 7 class 𝑞
87, 4wcel 2106 . . . . . 6 wff 𝑞 ∈ Odd
9 vz . . . . . . . 8 setvar 𝑧
109cv 1540 . . . . . . 7 class 𝑧
11 caddc 11112 . . . . . . . 8 class +
123, 7, 11co 7408 . . . . . . 7 class (𝑝 + 𝑞)
1310, 12wceq 1541 . . . . . 6 wff 𝑧 = (𝑝 + 𝑞)
145, 8, 13w3a 1087 . . . . 5 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
15 cprime 16607 . . . . 5 class
1614, 6, 15wrex 3070 . . . 4 wff 𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
1716, 2, 15wrex 3070 . . 3 wff 𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
18 ceven 46282 . . 3 class Even
1917, 9, 18crab 3432 . 2 class {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
201, 19wceq 1541 1 wff GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
Colors of variables: wff setvar class
This definition is referenced by:  isgbe  46409
  Copyright terms: Public domain W3C validator