Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isgbow Structured version   Visualization version   GIF version

Theorem isgbow 43421
Description: The predicate "is a weak odd Goldbach number". A weak odd Goldbach number is an odd integer having a Goldbach partition, i.e. which can be written as a sum of three primes. (Contributed by AV, 20-Jul-2020.)
Assertion
Ref Expression
isgbow (𝑍 ∈ GoldbachOddW ↔ (𝑍 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟)))
Distinct variable group:   𝑍,𝑝,𝑞,𝑟

Proof of Theorem isgbow
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2801 . . . 4 (𝑧 = 𝑍 → (𝑧 = ((𝑝 + 𝑞) + 𝑟) ↔ 𝑍 = ((𝑝 + 𝑞) + 𝑟)))
21rexbidv 3262 . . 3 (𝑧 = 𝑍 → (∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟) ↔ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟)))
322rexbidv 3265 . 2 (𝑧 = 𝑍 → (∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟) ↔ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟)))
4 df-gbow 43418 . 2 GoldbachOddW = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)}
53, 4elrab2 3624 1 (𝑍 ∈ GoldbachOddW ↔ (𝑍 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟)))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1525  wcel 2083  wrex 3108  (class class class)co 7023   + caddc 10393  cprime 15848   Odd codd 43294   GoldbachOddW cgbow 43415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-rex 3113  df-rab 3116  df-v 3442  df-gbow 43418
This theorem is referenced by:  gbowodd  43424  gbogbow  43425  gbowpos  43428  gbowgt5  43431  gbowge7  43432  7gbow  43441  sbgoldbwt  43446  sbgoldbm  43453  nnsum4primesodd  43465
  Copyright terms: Public domain W3C validator