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 ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) → ∃ 𝑜 ∈ GoldbachOdd 𝑁 = ( 𝑜 + 3 ) ) )

Proof

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