Metamath Proof Explorer


Theorem bgoldbnnsum3prm

Description: If the binary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 3 primes, showing that Schnirelmann's constant would be equal to 3. (Contributed by AV, 2-Aug-2020)

Ref Expression
Assertion bgoldbnnsum3prm ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ ‘ 2 ) ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 2z 2 ∈ ℤ
2 9nn 9 ∈ ℕ
3 2 nnzi 9 ∈ ℤ
4 2re 2 ∈ ℝ
5 9re 9 ∈ ℝ
6 2lt9 2 < 9
7 4 5 6 ltleii 2 ≤ 9
8 eluz2 ( 9 ∈ ( ℤ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 9 ∈ ℤ ∧ 2 ≤ 9 ) )
9 1 3 7 8 mpbir3an 9 ∈ ( ℤ ‘ 2 )
10 fzouzsplit ( 9 ∈ ( ℤ ‘ 2 ) → ( ℤ ‘ 2 ) = ( ( 2 ..^ 9 ) ∪ ( ℤ ‘ 9 ) ) )
11 10 eleq2d ( 9 ∈ ( ℤ ‘ 2 ) → ( 𝑛 ∈ ( ℤ ‘ 2 ) ↔ 𝑛 ∈ ( ( 2 ..^ 9 ) ∪ ( ℤ ‘ 9 ) ) ) )
12 9 11 ax-mp ( 𝑛 ∈ ( ℤ ‘ 2 ) ↔ 𝑛 ∈ ( ( 2 ..^ 9 ) ∪ ( ℤ ‘ 9 ) ) )
13 elun ( 𝑛 ∈ ( ( 2 ..^ 9 ) ∪ ( ℤ ‘ 9 ) ) ↔ ( 𝑛 ∈ ( 2 ..^ 9 ) ∨ 𝑛 ∈ ( ℤ ‘ 9 ) ) )
14 12 13 bitri ( 𝑛 ∈ ( ℤ ‘ 2 ) ↔ ( 𝑛 ∈ ( 2 ..^ 9 ) ∨ 𝑛 ∈ ( ℤ ‘ 9 ) ) )
15 elfzo2 ( 𝑛 ∈ ( 2 ..^ 9 ) ↔ ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 9 ∈ ℤ ∧ 𝑛 < 9 ) )
16 simp1 ( ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 9 ∈ ℤ ∧ 𝑛 < 9 ) → 𝑛 ∈ ( ℤ ‘ 2 ) )
17 df-9 9 = ( 8 + 1 )
18 17 breq2i ( 𝑛 < 9 ↔ 𝑛 < ( 8 + 1 ) )
19 eluz2nn ( 𝑛 ∈ ( ℤ ‘ 2 ) → 𝑛 ∈ ℕ )
20 8nn 8 ∈ ℕ
21 19 20 jctir ( 𝑛 ∈ ( ℤ ‘ 2 ) → ( 𝑛 ∈ ℕ ∧ 8 ∈ ℕ ) )
22 21 adantr ( ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 9 ∈ ℤ ) → ( 𝑛 ∈ ℕ ∧ 8 ∈ ℕ ) )
23 nnleltp1 ( ( 𝑛 ∈ ℕ ∧ 8 ∈ ℕ ) → ( 𝑛 ≤ 8 ↔ 𝑛 < ( 8 + 1 ) ) )
24 22 23 syl ( ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 9 ∈ ℤ ) → ( 𝑛 ≤ 8 ↔ 𝑛 < ( 8 + 1 ) ) )
25 24 biimprd ( ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 9 ∈ ℤ ) → ( 𝑛 < ( 8 + 1 ) → 𝑛 ≤ 8 ) )
26 18 25 syl5bi ( ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 9 ∈ ℤ ) → ( 𝑛 < 9 → 𝑛 ≤ 8 ) )
27 26 3impia ( ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 9 ∈ ℤ ∧ 𝑛 < 9 ) → 𝑛 ≤ 8 )
28 16 27 jca ( ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 9 ∈ ℤ ∧ 𝑛 < 9 ) → ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 𝑛 ≤ 8 ) )
29 15 28 sylbi ( 𝑛 ∈ ( 2 ..^ 9 ) → ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 𝑛 ≤ 8 ) )
30 nnsum3primesle9 ( ( 𝑛 ∈ ( ℤ ‘ 2 ) ∧ 𝑛 ≤ 8 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )
31 29 30 syl ( 𝑛 ∈ ( 2 ..^ 9 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )
32 31 a1d ( 𝑛 ∈ ( 2 ..^ 9 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
33 breq2 ( 𝑚 = 𝑛 → ( 4 < 𝑚 ↔ 4 < 𝑛 ) )
34 eleq1w ( 𝑚 = 𝑛 → ( 𝑚 ∈ GoldbachEven ↔ 𝑛 ∈ GoldbachEven ) )
35 33 34 imbi12d ( 𝑚 = 𝑛 → ( ( 4 < 𝑚𝑚 ∈ GoldbachEven ) ↔ ( 4 < 𝑛𝑛 ∈ GoldbachEven ) ) )
36 35 rspcv ( 𝑛 ∈ Even → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → ( 4 < 𝑛𝑛 ∈ GoldbachEven ) ) )
37 4re 4 ∈ ℝ
38 37 a1i ( 𝑛 ∈ ( ℤ ‘ 9 ) → 4 ∈ ℝ )
39 5 a1i ( 𝑛 ∈ ( ℤ ‘ 9 ) → 9 ∈ ℝ )
40 eluzelre ( 𝑛 ∈ ( ℤ ‘ 9 ) → 𝑛 ∈ ℝ )
41 38 39 40 3jca ( 𝑛 ∈ ( ℤ ‘ 9 ) → ( 4 ∈ ℝ ∧ 9 ∈ ℝ ∧ 𝑛 ∈ ℝ ) )
42 41 adantl ( ( 𝑛 ∈ Even ∧ 𝑛 ∈ ( ℤ ‘ 9 ) ) → ( 4 ∈ ℝ ∧ 9 ∈ ℝ ∧ 𝑛 ∈ ℝ ) )
43 eluzle ( 𝑛 ∈ ( ℤ ‘ 9 ) → 9 ≤ 𝑛 )
44 43 adantl ( ( 𝑛 ∈ Even ∧ 𝑛 ∈ ( ℤ ‘ 9 ) ) → 9 ≤ 𝑛 )
45 4lt9 4 < 9
46 44 45 jctil ( ( 𝑛 ∈ Even ∧ 𝑛 ∈ ( ℤ ‘ 9 ) ) → ( 4 < 9 ∧ 9 ≤ 𝑛 ) )
47 ltletr ( ( 4 ∈ ℝ ∧ 9 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 4 < 9 ∧ 9 ≤ 𝑛 ) → 4 < 𝑛 ) )
48 42 46 47 sylc ( ( 𝑛 ∈ Even ∧ 𝑛 ∈ ( ℤ ‘ 9 ) ) → 4 < 𝑛 )
49 pm2.27 ( 4 < 𝑛 → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven ) )
50 48 49 syl ( ( 𝑛 ∈ Even ∧ 𝑛 ∈ ( ℤ ‘ 9 ) ) → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven ) )
51 50 ex ( 𝑛 ∈ Even → ( 𝑛 ∈ ( ℤ ‘ 9 ) → ( ( 4 < 𝑛𝑛 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven ) ) )
52 36 51 syl5d ( 𝑛 ∈ Even → ( 𝑛 ∈ ( ℤ ‘ 9 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven ) ) )
53 52 impcom ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Even ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven ) )
54 nnsum3primesgbe ( 𝑛 ∈ GoldbachEven → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )
55 53 54 syl6 ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Even ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
56 3nn 3 ∈ ℕ
57 56 a1i ( ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜𝑜 ∈ GoldbachOddW ) ) → 3 ∈ ℕ )
58 oveq2 ( 𝑑 = 3 → ( 1 ... 𝑑 ) = ( 1 ... 3 ) )
59 58 oveq2d ( 𝑑 = 3 → ( ℙ ↑m ( 1 ... 𝑑 ) ) = ( ℙ ↑m ( 1 ... 3 ) ) )
60 breq1 ( 𝑑 = 3 → ( 𝑑 ≤ 3 ↔ 3 ≤ 3 ) )
61 58 sumeq1d ( 𝑑 = 3 → Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) )
62 61 eqeq2d ( 𝑑 = 3 → ( 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ↔ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
63 60 62 anbi12d ( 𝑑 = 3 → ( ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ↔ ( 3 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) ) )
64 59 63 rexeqbidv ( 𝑑 = 3 → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) ) )
65 64 adantl ( ( ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜𝑜 ∈ GoldbachOddW ) ) ∧ 𝑑 = 3 ) → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) ) )
66 3re 3 ∈ ℝ
67 66 leidi 3 ≤ 3
68 67 a1i ( ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜𝑜 ∈ GoldbachOddW ) ) → 3 ≤ 3 )
69 6nn 6 ∈ ℕ
70 69 nnzi 6 ∈ ℤ
71 6re 6 ∈ ℝ
72 6lt9 6 < 9
73 71 5 72 ltleii 6 ≤ 9
74 eluzuzle ( ( 6 ∈ ℤ ∧ 6 ≤ 9 ) → ( 𝑛 ∈ ( ℤ ‘ 9 ) → 𝑛 ∈ ( ℤ ‘ 6 ) ) )
75 70 73 74 mp2an ( 𝑛 ∈ ( ℤ ‘ 9 ) → 𝑛 ∈ ( ℤ ‘ 6 ) )
76 75 anim1i ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Odd ) → ( 𝑛 ∈ ( ℤ ‘ 6 ) ∧ 𝑛 ∈ Odd ) )
77 nnsum4primesodd ( ∀ 𝑜 ∈ Odd ( 5 < 𝑜𝑜 ∈ GoldbachOddW ) → ( ( 𝑛 ∈ ( ℤ ‘ 6 ) ∧ 𝑛 ∈ Odd ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
78 76 77 mpan9 ( ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜𝑜 ∈ GoldbachOddW ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) )
79 r19.42v ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) ↔ ( 3 ≤ 3 ∧ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
80 68 78 79 sylanbrc ( ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜𝑜 ∈ GoldbachOddW ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
81 57 65 80 rspcedvd ( ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜𝑜 ∈ GoldbachOddW ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )
82 81 expcom ( ∀ 𝑜 ∈ Odd ( 5 < 𝑜𝑜 ∈ GoldbachOddW ) → ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Odd ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
83 sbgoldbwt ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → ∀ 𝑜 ∈ Odd ( 5 < 𝑜𝑜 ∈ GoldbachOddW ) )
84 82 83 syl11 ( ( 𝑛 ∈ ( ℤ ‘ 9 ) ∧ 𝑛 ∈ Odd ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
85 eluzelz ( 𝑛 ∈ ( ℤ ‘ 9 ) → 𝑛 ∈ ℤ )
86 zeoALTV ( 𝑛 ∈ ℤ → ( 𝑛 ∈ Even ∨ 𝑛 ∈ Odd ) )
87 85 86 syl ( 𝑛 ∈ ( ℤ ‘ 9 ) → ( 𝑛 ∈ Even ∨ 𝑛 ∈ Odd ) )
88 55 84 87 mpjaodan ( 𝑛 ∈ ( ℤ ‘ 9 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
89 32 88 jaoi ( ( 𝑛 ∈ ( 2 ..^ 9 ) ∨ 𝑛 ∈ ( ℤ ‘ 9 ) ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
90 14 89 sylbi ( 𝑛 ∈ ( ℤ ‘ 2 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
91 90 impcom ( ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) ∧ 𝑛 ∈ ( ℤ ‘ 2 ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )
92 91 ralrimiva ( ∀ 𝑚 ∈ Even ( 4 < 𝑚𝑚 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ ‘ 2 ) ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )