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 ⊢∀m∈Even4<m→m∈GoldbachEven→∀n∈ℤ≥2∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k

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→n∈ℤ≥2↔n∈2..^9∪ℤ≥9
12 9 11 ax-mp ⊢n∈ℤ≥2↔n∈2..^9∪ℤ≥9
13 elun ⊢n∈2..^9∪ℤ≥9↔n∈2..^9∨n∈ℤ≥9
14 12 13 bitri ⊢n∈ℤ≥2↔n∈2..^9∨n∈ℤ≥9
15 elfzo2 ⊢n∈2..^9↔n∈ℤ≥2∧9∈ℤ∧n<9
16 simp1 ⊢n∈ℤ≥2∧9∈ℤ∧n<9→n∈ℤ≥2
17 df-9 ⊢9=8+1
18 17 breq2i ⊢n<9↔n<8+1
19 eluz2nn ⊢n∈ℤ≥2→n∈ℕ
20 8nn ⊢8∈ℕ
21 19 20 jctir ⊢n∈ℤ≥2→n∈ℕ∧8∈ℕ
22 21 adantr ⊢n∈ℤ≥2∧9∈ℤ→n∈ℕ∧8∈ℕ
23 nnleltp1 ⊢n∈ℕ∧8∈ℕ→n≤8↔n<8+1
24 22 23 syl ⊢n∈ℤ≥2∧9∈ℤ→n≤8↔n<8+1
25 24 biimprd ⊢n∈ℤ≥2∧9∈ℤ→n<8+1→n≤8
26 18 25 biimtrid ⊢n∈ℤ≥2∧9∈ℤ→n<9→n≤8
27 26 3impia ⊢n∈ℤ≥2∧9∈ℤ∧n<9→n≤8
28 16 27 jca ⊢n∈ℤ≥2∧9∈ℤ∧n<9→n∈ℤ≥2∧n≤8
29 15 28 sylbi ⊢n∈2..^9→n∈ℤ≥2∧n≤8
30 nnsum3primesle9 ⊢n∈ℤ≥2∧n≤8→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
31 29 30 syl ⊢n∈2..^9→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
32 31 a1d ⊢n∈2..^9→∀m∈Even4<m→m∈GoldbachEven→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
33 breq2 ⊢m=n→4<m↔4<n
34 eleq1w ⊢m=n→m∈GoldbachEven↔n∈GoldbachEven
35 33 34 imbi12d ⊢m=n→4<m→m∈GoldbachEven↔4<n→n∈GoldbachEven
36 35 rspcv ⊢n∈Even→∀m∈Even4<m→m∈GoldbachEven→4<n→n∈GoldbachEven
37 4re ⊢4∈ℝ
38 37 a1i ⊢n∈ℤ≥9→4∈ℝ
39 5 a1i ⊢n∈ℤ≥9→9∈ℝ
40 eluzelre ⊢n∈ℤ≥9→n∈ℝ
41 38 39 40 3jca ⊢n∈ℤ≥9→4∈ℝ∧9∈ℝ∧n∈ℝ
42 41 adantl ⊢n∈Even∧n∈ℤ≥9→4∈ℝ∧9∈ℝ∧n∈ℝ
43 eluzle ⊢n∈ℤ≥9→9≤n
44 43 adantl ⊢n∈Even∧n∈ℤ≥9→9≤n
45 4lt9 ⊢4<9
46 44 45 jctil ⊢n∈Even∧n∈ℤ≥9→4<9∧9≤n
47 ltletr ⊢4∈ℝ∧9∈ℝ∧n∈ℝ→4<9∧9≤n→4<n
48 42 46 47 sylc ⊢n∈Even∧n∈ℤ≥9→4<n
49 pm2.27 ⊢4<n→4<n→n∈GoldbachEven→n∈GoldbachEven
50 48 49 syl ⊢n∈Even∧n∈ℤ≥9→4<n→n∈GoldbachEven→n∈GoldbachEven
51 50 ex ⊢n∈Even→n∈ℤ≥9→4<n→n∈GoldbachEven→n∈GoldbachEven
52 36 51 syl5d ⊢n∈Even→n∈ℤ≥9→∀m∈Even4<m→m∈GoldbachEven→n∈GoldbachEven
53 52 impcom ⊢n∈ℤ≥9∧n∈Even→∀m∈Even4<m→m∈GoldbachEven→n∈GoldbachEven
54 nnsum3primesgbe ⊢n∈GoldbachEven→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
55 53 54 syl6 ⊢n∈ℤ≥9∧n∈Even→∀m∈Even4<m→m∈GoldbachEven→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
56 3nn ⊢3∈ℕ
57 56 a1i ⊢n∈ℤ≥9∧n∈Odd∧∀o∈Odd5<o→o∈GoldbachOddW→3∈ℕ
58 oveq2 ⊢d=3→1…d=1…3
59 58 oveq2d ⊢d=3→ℙ1…d=ℙ1…3
60 breq1 ⊢d=3→d≤3↔3≤3
61 58 sumeq1d ⊢d=3→∑k=1df⁡k=∑k=13f⁡k
62 61 eqeq2d ⊢d=3→n=∑k=1df⁡k↔n=∑k=13f⁡k
63 60 62 anbi12d ⊢d=3→d≤3∧n=∑k=1df⁡k↔3≤3∧n=∑k=13f⁡k
64 59 63 rexeqbidv ⊢d=3→∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k↔∃f∈ℙ1…33≤3∧n=∑k=13f⁡k
65 64 adantl ⊢n∈ℤ≥9∧n∈Odd∧∀o∈Odd5<o→o∈GoldbachOddW∧d=3→∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k↔∃f∈ℙ1…33≤3∧n=∑k=13f⁡k
66 3re ⊢3∈ℝ
67 66 leidi ⊢3≤3
68 67 a1i ⊢n∈ℤ≥9∧n∈Odd∧∀o∈Odd5<o→o∈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→n∈ℤ≥9→n∈ℤ≥6
75 70 73 74 mp2an ⊢n∈ℤ≥9→n∈ℤ≥6
76 75 anim1i ⊢n∈ℤ≥9∧n∈Odd→n∈ℤ≥6∧n∈Odd
77 nnsum4primesodd ⊢∀o∈Odd5<o→o∈GoldbachOddW→n∈ℤ≥6∧n∈Odd→∃f∈ℙ1…3n=∑k=13f⁡k
78 76 77 mpan9 ⊢n∈ℤ≥9∧n∈Odd∧∀o∈Odd5<o→o∈GoldbachOddW→∃f∈ℙ1…3n=∑k=13f⁡k
79 r19.42v ⊢∃f∈ℙ1…33≤3∧n=∑k=13f⁡k↔3≤3∧∃f∈ℙ1…3n=∑k=13f⁡k
80 68 78 79 sylanbrc ⊢n∈ℤ≥9∧n∈Odd∧∀o∈Odd5<o→o∈GoldbachOddW→∃f∈ℙ1…33≤3∧n=∑k=13f⁡k
81 57 65 80 rspcedvd ⊢n∈ℤ≥9∧n∈Odd∧∀o∈Odd5<o→o∈GoldbachOddW→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
82 81 expcom ⊢∀o∈Odd5<o→o∈GoldbachOddW→n∈ℤ≥9∧n∈Odd→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
83 sbgoldbwt ⊢∀m∈Even4<m→m∈GoldbachEven→∀o∈Odd5<o→o∈GoldbachOddW
84 82 83 syl11 ⊢n∈ℤ≥9∧n∈Odd→∀m∈Even4<m→m∈GoldbachEven→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
85 eluzelz ⊢n∈ℤ≥9→n∈ℤ
86 zeoALTV ⊢n∈ℤ→n∈Even∨n∈Odd
87 85 86 syl ⊢n∈ℤ≥9→n∈Even∨n∈Odd
88 55 84 87 mpjaodan ⊢n∈ℤ≥9→∀m∈Even4<m→m∈GoldbachEven→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
89 32 88 jaoi ⊢n∈2..^9∨n∈ℤ≥9→∀m∈Even4<m→m∈GoldbachEven→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
90 14 89 sylbi ⊢n∈ℤ≥2→∀m∈Even4<m→m∈GoldbachEven→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
91 90 impcom ⊢∀m∈Even4<m→m∈GoldbachEven∧n∈ℤ≥2→∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k
92 91 ralrimiva ⊢∀m∈Even4<m→m∈GoldbachEven→∀n∈ℤ≥2∃d∈ℕ∃f∈ℙ1…dd≤3∧n=∑k=1df⁡k