Metamath Proof Explorer

Theorem evengpoap3

Description: If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of an odd Goldbach number and 3. (Contributed by AV, 27-Jul-2020) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Assertion evengpoap3 ⊢ ∀ m ∈ Odd 7 < m → m ∈ GoldbachOdd → N ∈ ℤ ≥ 12 ∧ N ∈ Even → ∃ o ∈ GoldbachOdd N = o + 3

Proof

Step Hyp Ref Expression
1 3odd ⊢ 3 ∈ Odd
2 1 a1i ⊢ N ∈ ℤ ≥ 12 → 3 ∈ Odd
3 2 anim1i ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even → 3 ∈ Odd ∧ N ∈ Even
4 3 ancomd ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even → N ∈ Even ∧ 3 ∈ Odd
5 emoo ⊢ N ∈ Even ∧ 3 ∈ Odd → N − 3 ∈ Odd
6 4 5 syl ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even → N − 3 ∈ Odd
7 breq2 ⊢ m = N − 3 → 7 < m ↔ 7 < N − 3
8 eleq1 ⊢ m = N − 3 → m ∈ GoldbachOdd ↔ N − 3 ∈ GoldbachOdd
9 7 8 imbi12d ⊢ m = N − 3 → 7 < m → m ∈ GoldbachOdd ↔ 7 < N − 3 → N − 3 ∈ GoldbachOdd
10 9 adantl ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even ∧ m = N − 3 → 7 < m → m ∈ GoldbachOdd ↔ 7 < N − 3 → N − 3 ∈ GoldbachOdd
11 6 10 rspcdv ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even → ∀ m ∈ Odd 7 < m → m ∈ GoldbachOdd → 7 < N − 3 → N − 3 ∈ GoldbachOdd
12 eluz2 ⊢ N ∈ ℤ ≥ 12 ↔ 12 ∈ ℤ ∧ N ∈ ℤ ∧ 12 ≤ N
13 7p3e10 ⊢ 7 + 3 = 10
14 1nn0 ⊢ 1 ∈ ℕ 0
15 0nn0 ⊢ 0 ∈ ℕ 0
16 2nn ⊢ 2 ∈ ℕ
17 2pos ⊢ 0 < 2
18 14 15 16 17 declt ⊢ 10 < 12
19 13 18 eqbrtri ⊢ 7 + 3 < 12
20 7re ⊢ 7 ∈ ℝ
21 3re ⊢ 3 ∈ ℝ
22 20 21 readdcli ⊢ 7 + 3 ∈ ℝ
23 2nn0 ⊢ 2 ∈ ℕ 0
24 14 23 deccl ⊢ 12 ∈ ℕ 0
25 24 nn0rei ⊢ 12 ∈ ℝ
26 zre ⊢ N ∈ ℤ → N ∈ ℝ
27 ltletr ⊢ 7 + 3 ∈ ℝ ∧ 12 ∈ ℝ ∧ N ∈ ℝ → 7 + 3 < 12 ∧ 12 ≤ N → 7 + 3 < N
28 22 25 26 27 mp3an12i ⊢ N ∈ ℤ → 7 + 3 < 12 ∧ 12 ≤ N → 7 + 3 < N
29 19 28 mpani ⊢ N ∈ ℤ → 12 ≤ N → 7 + 3 < N
30 29 imp ⊢ N ∈ ℤ ∧ 12 ≤ N → 7 + 3 < N
31 30 3adant1 ⊢ 12 ∈ ℤ ∧ N ∈ ℤ ∧ 12 ≤ N → 7 + 3 < N
32 20 a1i ⊢ 12 ∈ ℤ ∧ N ∈ ℤ ∧ 12 ≤ N → 7 ∈ ℝ
33 21 a1i ⊢ 12 ∈ ℤ ∧ N ∈ ℤ ∧ 12 ≤ N → 3 ∈ ℝ
34 26 3ad2ant2 ⊢ 12 ∈ ℤ ∧ N ∈ ℤ ∧ 12 ≤ N → N ∈ ℝ
35 32 33 34 ltaddsubd ⊢ 12 ∈ ℤ ∧ N ∈ ℤ ∧ 12 ≤ N → 7 + 3 < N ↔ 7 < N − 3
36 31 35 mpbid ⊢ 12 ∈ ℤ ∧ N ∈ ℤ ∧ 12 ≤ N → 7 < N − 3
37 12 36 sylbi ⊢ N ∈ ℤ ≥ 12 → 7 < N − 3
38 37 adantr ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even → 7 < N − 3
39 simpr ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even ∧ N − 3 ∈ GoldbachOdd → N − 3 ∈ GoldbachOdd
40 oveq1 ⊢ o = N − 3 → o + 3 = N - 3 + 3
41 40 eqeq2d ⊢ o = N − 3 → N = o + 3 ↔ N = N - 3 + 3
42 41 adantl ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even ∧ N − 3 ∈ GoldbachOdd ∧ o = N − 3 → N = o + 3 ↔ N = N - 3 + 3
43 eluzelcn ⊢ N ∈ ℤ ≥ 12 → N ∈ ℂ
44 3cn ⊢ 3 ∈ ℂ
45 43 44 jctir ⊢ N ∈ ℤ ≥ 12 → N ∈ ℂ ∧ 3 ∈ ℂ
46 45 adantr ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even → N ∈ ℂ ∧ 3 ∈ ℂ
47 46 adantr ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even ∧ N − 3 ∈ GoldbachOdd → N ∈ ℂ ∧ 3 ∈ ℂ
48 npcan ⊢ N ∈ ℂ ∧ 3 ∈ ℂ → N - 3 + 3 = N
49 48 eqcomd ⊢ N ∈ ℂ ∧ 3 ∈ ℂ → N = N - 3 + 3
50 47 49 syl ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even ∧ N − 3 ∈ GoldbachOdd → N = N - 3 + 3
51 39 42 50 rspcedvd ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even ∧ N − 3 ∈ GoldbachOdd → ∃ o ∈ GoldbachOdd N = o + 3
52 51 ex ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even → N − 3 ∈ GoldbachOdd → ∃ o ∈ GoldbachOdd N = o + 3
53 38 52 embantd ⊢ N ∈ ℤ ≥ 12 ∧ N ∈ Even → 7 < N − 3 → N − 3 ∈ GoldbachOdd → ∃ o ∈ GoldbachOdd N = o + 3
54 11 53 syldc ⊢ ∀ m ∈ Odd 7 < m → m ∈ GoldbachOdd → N ∈ ℤ ≥ 12 ∧ N ∈ Even → ∃ o ∈ GoldbachOdd N = o + 3