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

Theorem evengpop3 46092
Description: If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of an odd Goldbach number and 3. (Contributed by AV, 24-Jul-2020.)
Assertion
Ref Expression
evengpop3 (∀𝑚 ∈ Odd (5 < 𝑚𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3)))
Distinct variable groups:   𝑚,𝑁   𝑜,𝑁

Proof of Theorem evengpop3
StepHypRef Expression
1 3odd 46002 . . . . . . 7 3 ∈ Odd
21a1i 11 . . . . . 6 (𝑁 ∈ (ℤ‘9) → 3 ∈ Odd )
32anim1i 616 . . . . 5 ((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) → (3 ∈ Odd ∧ 𝑁 ∈ Even ))
43ancomd 463 . . . 4 ((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) → (𝑁 ∈ Even ∧ 3 ∈ Odd ))
5 emoo 45998 . . . 4 ((𝑁 ∈ Even ∧ 3 ∈ Odd ) → (𝑁 − 3) ∈ Odd )
64, 5syl 17 . . 3 ((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) → (𝑁 − 3) ∈ Odd )
7 breq2 5115 . . . . 5 (𝑚 = (𝑁 − 3) → (5 < 𝑚 ↔ 5 < (𝑁 − 3)))
8 eleq1 2821 . . . . 5 (𝑚 = (𝑁 − 3) → (𝑚 ∈ GoldbachOddW ↔ (𝑁 − 3) ∈ GoldbachOddW ))
97, 8imbi12d 345 . . . 4 (𝑚 = (𝑁 − 3) → ((5 < 𝑚𝑚 ∈ GoldbachOddW ) ↔ (5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOddW )))
109adantl 483 . . 3 (((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) ∧ 𝑚 = (𝑁 − 3)) → ((5 < 𝑚𝑚 ∈ GoldbachOddW ) ↔ (5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOddW )))
116, 10rspcdv 3575 . 2 ((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) → (∀𝑚 ∈ Odd (5 < 𝑚𝑚 ∈ GoldbachOddW ) → (5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOddW )))
12 eluz2 12779 . . . . 5 (𝑁 ∈ (ℤ‘9) ↔ (9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁))
13 5p3e8 12320 . . . . . . . 8 (5 + 3) = 8
14 8p1e9 12313 . . . . . . . . 9 (8 + 1) = 9
15 9cn 12263 . . . . . . . . . 10 9 ∈ ℂ
16 ax-1cn 11119 . . . . . . . . . 10 1 ∈ ℂ
17 8cn 12260 . . . . . . . . . 10 8 ∈ ℂ
1815, 16, 17subadd2i 11499 . . . . . . . . 9 ((9 − 1) = 8 ↔ (8 + 1) = 9)
1914, 18mpbir 230 . . . . . . . 8 (9 − 1) = 8
2013, 19eqtr4i 2763 . . . . . . 7 (5 + 3) = (9 − 1)
21 zlem1lt 12565 . . . . . . . 8 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (9 ≤ 𝑁 ↔ (9 − 1) < 𝑁))
2221biimp3a 1470 . . . . . . 7 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁) → (9 − 1) < 𝑁)
2320, 22eqbrtrid 5146 . . . . . 6 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁) → (5 + 3) < 𝑁)
24 5re 12250 . . . . . . . . . 10 5 ∈ ℝ
2524a1i 11 . . . . . . . . 9 (𝑁 ∈ ℤ → 5 ∈ ℝ)
26 3re 12243 . . . . . . . . . 10 3 ∈ ℝ
2726a1i 11 . . . . . . . . 9 (𝑁 ∈ ℤ → 3 ∈ ℝ)
28 zre 12513 . . . . . . . . 9 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
2925, 27, 283jca 1129 . . . . . . . 8 (𝑁 ∈ ℤ → (5 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ))
30293ad2ant2 1135 . . . . . . 7 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁) → (5 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ))
31 ltaddsub 11639 . . . . . . 7 ((5 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((5 + 3) < 𝑁 ↔ 5 < (𝑁 − 3)))
3230, 31syl 17 . . . . . 6 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁) → ((5 + 3) < 𝑁 ↔ 5 < (𝑁 − 3)))
3323, 32mpbid 231 . . . . 5 ((9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁) → 5 < (𝑁 − 3))
3412, 33sylbi 216 . . . 4 (𝑁 ∈ (ℤ‘9) → 5 < (𝑁 − 3))
3534adantr 482 . . 3 ((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) → 5 < (𝑁 − 3))
36 simpr 486 . . . . 5 (((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOddW ) → (𝑁 − 3) ∈ GoldbachOddW )
37 oveq1 7370 . . . . . . 7 (𝑜 = (𝑁 − 3) → (𝑜 + 3) = ((𝑁 − 3) + 3))
3837eqeq2d 2743 . . . . . 6 (𝑜 = (𝑁 − 3) → (𝑁 = (𝑜 + 3) ↔ 𝑁 = ((𝑁 − 3) + 3)))
3938adantl 483 . . . . 5 ((((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOddW ) ∧ 𝑜 = (𝑁 − 3)) → (𝑁 = (𝑜 + 3) ↔ 𝑁 = ((𝑁 − 3) + 3)))
40 eluzelcn 12785 . . . . . . . . 9 (𝑁 ∈ (ℤ‘9) → 𝑁 ∈ ℂ)
41 3cn 12244 . . . . . . . . . 10 3 ∈ ℂ
4241a1i 11 . . . . . . . . 9 (𝑁 ∈ (ℤ‘9) → 3 ∈ ℂ)
4340, 42jca 513 . . . . . . . 8 (𝑁 ∈ (ℤ‘9) → (𝑁 ∈ ℂ ∧ 3 ∈ ℂ))
4443adantr 482 . . . . . . 7 ((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) → (𝑁 ∈ ℂ ∧ 3 ∈ ℂ))
4544adantr 482 . . . . . 6 (((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOddW ) → (𝑁 ∈ ℂ ∧ 3 ∈ ℂ))
46 npcan 11420 . . . . . . 7 ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ) → ((𝑁 − 3) + 3) = 𝑁)
4746eqcomd 2738 . . . . . 6 ((𝑁 ∈ ℂ ∧ 3 ∈ ℂ) → 𝑁 = ((𝑁 − 3) + 3))
4845, 47syl 17 . . . . 5 (((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOddW ) → 𝑁 = ((𝑁 − 3) + 3))
4936, 39, 48rspcedvd 3585 . . . 4 (((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) ∧ (𝑁 − 3) ∈ GoldbachOddW ) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3))
5049ex 414 . . 3 ((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) → ((𝑁 − 3) ∈ GoldbachOddW → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3)))
5135, 50embantd 59 . 2 ((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) → ((5 < (𝑁 − 3) → (𝑁 − 3) ∈ GoldbachOddW ) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3)))
5211, 51syldc 48 1 (∀𝑚 ∈ Odd (5 < 𝑚𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ‘9) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3061  wrex 3070   class class class wbr 5111  cfv 6502  (class class class)co 7363  cc 11059  cr 11060  1c1 11062   + caddc 11064   < clt 11199  cle 11200  cmin 11395  3c3 12219  5c5 12221  8c8 12224  9c9 12225  cz 12509  cuz 12773   Even ceven 45918   Odd codd 45919   GoldbachOddW cgbow 46040
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2703  ax-sep 5262  ax-nul 5269  ax-pow 5326  ax-pr 5390  ax-un 7678  ax-cnex 11117  ax-resscn 11118  ax-1cn 11119  ax-icn 11120  ax-addcl 11121  ax-addrcl 11122  ax-mulcl 11123  ax-mulrcl 11124  ax-mulcom 11125  ax-addass 11126  ax-mulass 11127  ax-distr 11128  ax-i2m1 11129  ax-1ne0 11130  ax-1rid 11131  ax-rnegex 11132  ax-rrecex 11133  ax-cnre 11134  ax-pre-lttri 11135  ax-pre-lttrn 11136  ax-pre-ltadd 11137  ax-pre-mulgt0 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4289  df-if 4493  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4872  df-iun 4962  df-br 5112  df-opab 5174  df-mpt 5195  df-tr 5229  df-id 5537  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5594  df-we 5596  df-xp 5645  df-rel 5646  df-cnv 5647  df-co 5648  df-dm 5649  df-rn 5650  df-res 5651  df-ima 5652  df-pred 6259  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7319  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7809  df-2nd 7928  df-frecs 8218  df-wrecs 8249  df-recs 8323  df-rdg 8362  df-er 8656  df-en 8892  df-dom 8893  df-sdom 8894  df-pnf 11201  df-mnf 11202  df-xr 11203  df-ltxr 11204  df-le 11205  df-sub 11397  df-neg 11398  df-div 11823  df-nn 12164  df-2 12226  df-3 12227  df-4 12228  df-5 12229  df-6 12230  df-7 12231  df-8 12232  df-9 12233  df-n0 12424  df-z 12510  df-uz 12774  df-even 45920  df-odd 45921
This theorem is referenced by:  nnsum4primeseven  46094
  Copyright terms: Public domain W3C validator