Metamath Proof Explorer

Theorem evengpop3

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)

Ref Expression
Assertion evengpop3 ⊢ ∀ m ∈ Odd 5 < m → m ∈ GoldbachOddW → N ∈ ℤ ≥ 9 ∧ N ∈ Even → ∃ o ∈ GoldbachOddW N = o + 3

Proof

Step Hyp Ref Expression
1 3odd ⊢ 3 ∈ Odd
2 1 a1i ⊢ N ∈ ℤ ≥ 9 → 3 ∈ Odd
3 2 anim1i ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even → 3 ∈ Odd ∧ N ∈ Even
4 3 ancomd ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even → N ∈ Even ∧ 3 ∈ Odd
5 emoo ⊢ N ∈ Even ∧ 3 ∈ Odd → N − 3 ∈ Odd
6 4 5 syl ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even → N − 3 ∈ Odd
7 breq2 ⊢ m = N − 3 → 5 < m ↔ 5 < N − 3
8 eleq1 ⊢ m = N − 3 → m ∈ GoldbachOddW ↔ N − 3 ∈ GoldbachOddW
9 7 8 imbi12d ⊢ m = N − 3 → 5 < m → m ∈ GoldbachOddW ↔ 5 < N − 3 → N − 3 ∈ GoldbachOddW
10 9 adantl ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even ∧ m = N − 3 → 5 < m → m ∈ GoldbachOddW ↔ 5 < N − 3 → N − 3 ∈ GoldbachOddW
11 6 10 rspcdv ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even → ∀ m ∈ Odd 5 < m → m ∈ GoldbachOddW → 5 < N − 3 → N − 3 ∈ GoldbachOddW
12 eluz2 ⊢ N ∈ ℤ ≥ 9 ↔ 9 ∈ ℤ ∧ N ∈ ℤ ∧ 9 ≤ N
13 5p3e8 ⊢ 5 + 3 = 8
14 8p1e9 ⊢ 8 + 1 = 9
15 9cn ⊢ 9 ∈ ℂ
16 ax-1cn ⊢ 1 ∈ ℂ
17 8cn ⊢ 8 ∈ ℂ
18 15 16 17 subadd2i ⊢ 9 − 1 = 8 ↔ 8 + 1 = 9
19 14 18 mpbir ⊢ 9 − 1 = 8
20 13 19 eqtr4i ⊢ 5 + 3 = 9 − 1
21 zlem1lt ⊢ 9 ∈ ℤ ∧ N ∈ ℤ → 9 ≤ N ↔ 9 − 1 < N
22 21 biimp3a ⊢ 9 ∈ ℤ ∧ N ∈ ℤ ∧ 9 ≤ N → 9 − 1 < N
23 20 22 eqbrtrid ⊢ 9 ∈ ℤ ∧ N ∈ ℤ ∧ 9 ≤ N → 5 + 3 < N
24 5re ⊢ 5 ∈ ℝ
25 24 a1i ⊢ N ∈ ℤ → 5 ∈ ℝ
26 3re ⊢ 3 ∈ ℝ
27 26 a1i ⊢ N ∈ ℤ → 3 ∈ ℝ
28 zre ⊢ N ∈ ℤ → N ∈ ℝ
29 25 27 28 3jca ⊢ N ∈ ℤ → 5 ∈ ℝ ∧ 3 ∈ ℝ ∧ N ∈ ℝ
30 29 3ad2ant2 ⊢ 9 ∈ ℤ ∧ N ∈ ℤ ∧ 9 ≤ N → 5 ∈ ℝ ∧ 3 ∈ ℝ ∧ N ∈ ℝ
31 ltaddsub ⊢ 5 ∈ ℝ ∧ 3 ∈ ℝ ∧ N ∈ ℝ → 5 + 3 < N ↔ 5 < N − 3
32 30 31 syl ⊢ 9 ∈ ℤ ∧ N ∈ ℤ ∧ 9 ≤ N → 5 + 3 < N ↔ 5 < N − 3
33 23 32 mpbid ⊢ 9 ∈ ℤ ∧ N ∈ ℤ ∧ 9 ≤ N → 5 < N − 3
34 12 33 sylbi ⊢ N ∈ ℤ ≥ 9 → 5 < N − 3
35 34 adantr ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even → 5 < N − 3
36 simpr ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even ∧ N − 3 ∈ GoldbachOddW → N − 3 ∈ GoldbachOddW
37 oveq1 ⊢ o = N − 3 → o + 3 = N - 3 + 3
38 37 eqeq2d ⊢ o = N − 3 → N = o + 3 ↔ N = N - 3 + 3
39 38 adantl ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even ∧ N − 3 ∈ GoldbachOddW ∧ o = N − 3 → N = o + 3 ↔ N = N - 3 + 3
40 eluzelcn ⊢ N ∈ ℤ ≥ 9 → N ∈ ℂ
41 3cn ⊢ 3 ∈ ℂ
42 41 a1i ⊢ N ∈ ℤ ≥ 9 → 3 ∈ ℂ
43 40 42 jca ⊢ N ∈ ℤ ≥ 9 → N ∈ ℂ ∧ 3 ∈ ℂ
44 43 adantr ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even → N ∈ ℂ ∧ 3 ∈ ℂ
45 44 adantr ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even ∧ N − 3 ∈ GoldbachOddW → N ∈ ℂ ∧ 3 ∈ ℂ
46 npcan ⊢ N ∈ ℂ ∧ 3 ∈ ℂ → N - 3 + 3 = N
47 46 eqcomd ⊢ N ∈ ℂ ∧ 3 ∈ ℂ → N = N - 3 + 3
48 45 47 syl ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even ∧ N − 3 ∈ GoldbachOddW → N = N - 3 + 3
49 36 39 48 rspcedvd ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even ∧ N − 3 ∈ GoldbachOddW → ∃ o ∈ GoldbachOddW N = o + 3
50 49 ex ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even → N − 3 ∈ GoldbachOddW → ∃ o ∈ GoldbachOddW N = o + 3
51 35 50 embantd ⊢ N ∈ ℤ ≥ 9 ∧ N ∈ Even → 5 < N − 3 → N − 3 ∈ GoldbachOddW → ∃ o ∈ GoldbachOddW N = o + 3
52 11 51 syldc ⊢ ∀ m ∈ Odd 5 < m → m ∈ GoldbachOddW → N ∈ ℤ ≥ 9 ∧ N ∈ Even → ∃ o ∈ GoldbachOddW N = o + 3