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

Proof

Step Hyp Ref Expression
1 3odd ⊢ 3 ∈ Odd
2 1 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) → 3 ∈ Odd )
3 2 anim1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) → ( 3 ∈ Odd ∧ 𝑁 ∈ Even ) )
4 3 ancomd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) → ( 𝑁 ∈ Even ∧ 3 ∈ Odd ) )
5 emoo ⊢ ( ( 𝑁 ∈ Even ∧ 3 ∈ Odd ) → ( 𝑁 − 3 ) ∈ Odd )
6 4 5 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) → ( 𝑁 − 3 ) ∈ Odd )
7 breq2 ⊢ ( 𝑚 = ( 𝑁 − 3 ) → ( 5 < 𝑚 ↔ 5 < ( 𝑁 − 3 ) ) )
8 eleq1 ⊢ ( 𝑚 = ( 𝑁 − 3 ) → ( 𝑚 ∈ GoldbachOddW ↔ ( 𝑁 − 3 ) ∈ GoldbachOddW ) )
9 7 8 imbi12d ⊢ ( 𝑚 = ( 𝑁 − 3 ) → ( ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ↔ ( 5 < ( 𝑁 − 3 ) → ( 𝑁 − 3 ) ∈ GoldbachOddW ) ) )
10 9 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) ∧ 𝑚 = ( 𝑁 − 3 ) ) → ( ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ↔ ( 5 < ( 𝑁 − 3 ) → ( 𝑁 − 3 ) ∈ GoldbachOddW ) ) )
11 6 10 rspcdv ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) → ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ( 5 < ( 𝑁 − 3 ) → ( 𝑁 − 3 ) ∈ GoldbachOddW ) ) )
12 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ↔ ( 9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁 ) )
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 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 9 ≤ 𝑁 ↔ ( 9 − 1 ) < 𝑁 ) )
22 21 biimp3a ⊢ ( ( 9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁 ) → ( 9 − 1 ) < 𝑁 )
23 20 22 eqbrtrid ⊢ ( ( 9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁 ) → ( 5 + 3 ) < 𝑁 )
24 5re ⊢ 5 ∈ ℝ
25 24 a1i ⊢ ( 𝑁 ∈ ℤ → 5 ∈ ℝ )
26 3re ⊢ 3 ∈ ℝ
27 26 a1i ⊢ ( 𝑁 ∈ ℤ → 3 ∈ ℝ )
28 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
29 25 27 28 3jca ⊢ ( 𝑁 ∈ ℤ → ( 5 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
30 29 3ad2ant2 ⊢ ( ( 9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁 ) → ( 5 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
31 ltaddsub ⊢ ( ( 5 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 5 + 3 ) < 𝑁 ↔ 5 < ( 𝑁 − 3 ) ) )
32 30 31 syl ⊢ ( ( 9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁 ) → ( ( 5 + 3 ) < 𝑁 ↔ 5 < ( 𝑁 − 3 ) ) )
33 23 32 mpbid ⊢ ( ( 9 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 9 ≤ 𝑁 ) → 5 < ( 𝑁 − 3 ) )
34 12 33 sylbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) → 5 < ( 𝑁 − 3 ) )
35 34 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) → 5 < ( 𝑁 − 3 ) )
36 simpr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) ∧ ( 𝑁 − 3 ) ∈ GoldbachOddW ) → ( 𝑁 − 3 ) ∈ GoldbachOddW )
37 oveq1 ⊢ ( 𝑜 = ( 𝑁 − 3 ) → ( 𝑜 + 3 ) = ( ( 𝑁 − 3 ) + 3 ) )
38 37 eqeq2d ⊢ ( 𝑜 = ( 𝑁 − 3 ) → ( 𝑁 = ( 𝑜 + 3 ) ↔ 𝑁 = ( ( 𝑁 − 3 ) + 3 ) ) )
39 38 adantl ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) ∧ ( 𝑁 − 3 ) ∈ GoldbachOddW ) ∧ 𝑜 = ( 𝑁 − 3 ) ) → ( 𝑁 = ( 𝑜 + 3 ) ↔ 𝑁 = ( ( 𝑁 − 3 ) + 3 ) ) )
40 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) → 𝑁 ∈ ℂ )
41 3cn ⊢ 3 ∈ ℂ
42 41 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) → 3 ∈ ℂ )
43 40 42 jca ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) → ( 𝑁 ∈ ℂ ∧ 3 ∈ ℂ ) )
44 43 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) → ( 𝑁 ∈ ℂ ∧ 3 ∈ ℂ ) )
45 44 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) ∧ ( 𝑁 − 3 ) ∈ GoldbachOddW ) → ( 𝑁 ∈ ℂ ∧ 3 ∈ ℂ ) )
46 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 3 ∈ ℂ ) → ( ( 𝑁 − 3 ) + 3 ) = 𝑁 )
47 46 eqcomd ⊢ ( ( 𝑁 ∈ ℂ ∧ 3 ∈ ℂ ) → 𝑁 = ( ( 𝑁 − 3 ) + 3 ) )
48 45 47 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) ∧ ( 𝑁 − 3 ) ∈ GoldbachOddW ) → 𝑁 = ( ( 𝑁 − 3 ) + 3 ) )
49 36 39 48 rspcedvd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) ∧ ( 𝑁 − 3 ) ∈ GoldbachOddW ) → ∃ 𝑜 ∈ GoldbachOddW 𝑁 = ( 𝑜 + 3 ) )
50 49 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) → ( ( 𝑁 − 3 ) ∈ GoldbachOddW → ∃ 𝑜 ∈ GoldbachOddW 𝑁 = ( 𝑜 + 3 ) ) )
51 35 50 embantd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) → ( ( 5 < ( 𝑁 − 3 ) → ( 𝑁 − 3 ) ∈ GoldbachOddW ) → ∃ 𝑜 ∈ GoldbachOddW 𝑁 = ( 𝑜 + 3 ) ) )
52 11 51 syldc ⊢ ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) → ∃ 𝑜 ∈ GoldbachOddW 𝑁 = ( 𝑜 + 3 ) ) )