This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnsum3primesle9

Description: Every integer greater than 1 and less than or equal to 8 is the sum of at most 3 primes. (Contributed by AV, 2-Aug-2020)

Ref Expression
Assertion nnsum3primesle9 ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ≤ 8 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℝ )
2 8re ⊢ 8 ∈ ℝ
3 2 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 8 ∈ ℝ )
4 1 3 leloed ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 8 ↔ ( 𝑁 < 8 ∨ 𝑁 = 8 ) ) )
5 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℤ )
6 7nn ⊢ 7 ∈ ℕ
7 6 nnzi ⊢ 7 ∈ ℤ
8 zleltp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 7 ∈ ℤ ) → ( 𝑁 ≤ 7 ↔ 𝑁 < ( 7 + 1 ) ) )
9 5 7 8 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 7 ↔ 𝑁 < ( 7 + 1 ) ) )
10 7re ⊢ 7 ∈ ℝ
11 10 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 7 ∈ ℝ )
12 1 11 leloed ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 7 ↔ ( 𝑁 < 7 ∨ 𝑁 = 7 ) ) )
13 7p1e8 ⊢ ( 7 + 1 ) = 8
14 13 breq2i ⊢ ( 𝑁 < ( 7 + 1 ) ↔ 𝑁 < 8 )
15 14 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < ( 7 + 1 ) ↔ 𝑁 < 8 ) )
16 9 12 15 3bitr3rd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 8 ↔ ( 𝑁 < 7 ∨ 𝑁 = 7 ) ) )
17 6nn ⊢ 6 ∈ ℕ
18 17 nnzi ⊢ 6 ∈ ℤ
19 zleltp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 6 ∈ ℤ ) → ( 𝑁 ≤ 6 ↔ 𝑁 < ( 6 + 1 ) ) )
20 5 18 19 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 6 ↔ 𝑁 < ( 6 + 1 ) ) )
21 6re ⊢ 6 ∈ ℝ
22 21 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 6 ∈ ℝ )
23 1 22 leloed ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 6 ↔ ( 𝑁 < 6 ∨ 𝑁 = 6 ) ) )
24 6p1e7 ⊢ ( 6 + 1 ) = 7
25 24 breq2i ⊢ ( 𝑁 < ( 6 + 1 ) ↔ 𝑁 < 7 )
26 25 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < ( 6 + 1 ) ↔ 𝑁 < 7 ) )
27 20 23 26 3bitr3rd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 7 ↔ ( 𝑁 < 6 ∨ 𝑁 = 6 ) ) )
28 5nn ⊢ 5 ∈ ℕ
29 28 nnzi ⊢ 5 ∈ ℤ
30 zleltp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 5 ∈ ℤ ) → ( 𝑁 ≤ 5 ↔ 𝑁 < ( 5 + 1 ) ) )
31 5 29 30 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 5 ↔ 𝑁 < ( 5 + 1 ) ) )
32 5re ⊢ 5 ∈ ℝ
33 32 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 5 ∈ ℝ )
34 1 33 leloed ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 5 ↔ ( 𝑁 < 5 ∨ 𝑁 = 5 ) ) )
35 5p1e6 ⊢ ( 5 + 1 ) = 6
36 35 breq2i ⊢ ( 𝑁 < ( 5 + 1 ) ↔ 𝑁 < 6 )
37 36 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < ( 5 + 1 ) ↔ 𝑁 < 6 ) )
38 31 34 37 3bitr3rd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 6 ↔ ( 𝑁 < 5 ∨ 𝑁 = 5 ) ) )
39 4z ⊢ 4 ∈ ℤ
40 zleltp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 4 ∈ ℤ ) → ( 𝑁 ≤ 4 ↔ 𝑁 < ( 4 + 1 ) ) )
41 5 39 40 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 4 ↔ 𝑁 < ( 4 + 1 ) ) )
42 4re ⊢ 4 ∈ ℝ
43 42 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 4 ∈ ℝ )
44 1 43 leloed ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 4 ↔ ( 𝑁 < 4 ∨ 𝑁 = 4 ) ) )
45 4p1e5 ⊢ ( 4 + 1 ) = 5
46 45 breq2i ⊢ ( 𝑁 < ( 4 + 1 ) ↔ 𝑁 < 5 )
47 46 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < ( 4 + 1 ) ↔ 𝑁 < 5 ) )
48 41 44 47 3bitr3rd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 5 ↔ ( 𝑁 < 4 ∨ 𝑁 = 4 ) ) )
49 3z ⊢ 3 ∈ ℤ
50 zleltp1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 3 ∈ ℤ ) → ( 𝑁 ≤ 3 ↔ 𝑁 < ( 3 + 1 ) ) )
51 5 49 50 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 3 ↔ 𝑁 < ( 3 + 1 ) ) )
52 3re ⊢ 3 ∈ ℝ
53 52 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 3 ∈ ℝ )
54 1 53 leloed ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 3 ↔ ( 𝑁 < 3 ∨ 𝑁 = 3 ) ) )
55 3p1e4 ⊢ ( 3 + 1 ) = 4
56 55 breq2i ⊢ ( 𝑁 < ( 3 + 1 ) ↔ 𝑁 < 4 )
57 56 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < ( 3 + 1 ) ↔ 𝑁 < 4 ) )
58 51 54 57 3bitr3rd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 4 ↔ ( 𝑁 < 3 ∨ 𝑁 = 3 ) ) )
59 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) )
60 2re ⊢ 2 ∈ ℝ
61 60 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℝ )
62 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
63 61 62 leloed ⊢ ( 𝑁 ∈ ℤ → ( 2 ≤ 𝑁 ↔ ( 2 < 𝑁 ∨ 2 = 𝑁 ) ) )
64 3m1e2 ⊢ ( 3 − 1 ) = 2
65 64 eqcomi ⊢ 2 = ( 3 − 1 )
66 65 breq1i ⊢ ( 2 < 𝑁 ↔ ( 3 − 1 ) < 𝑁 )
67 zlem1lt ⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 3 ≤ 𝑁 ↔ ( 3 − 1 ) < 𝑁 ) )
68 49 67 mpan ⊢ ( 𝑁 ∈ ℤ → ( 3 ≤ 𝑁 ↔ ( 3 − 1 ) < 𝑁 ) )
69 68 biimprd ⊢ ( 𝑁 ∈ ℤ → ( ( 3 − 1 ) < 𝑁 → 3 ≤ 𝑁 ) )
70 66 69 biimtrid ⊢ ( 𝑁 ∈ ℤ → ( 2 < 𝑁 → 3 ≤ 𝑁 ) )
71 52 a1i ⊢ ( 𝑁 ∈ ℤ → 3 ∈ ℝ )
72 71 62 lenltd ⊢ ( 𝑁 ∈ ℤ → ( 3 ≤ 𝑁 ↔ ¬ 𝑁 < 3 ) )
73 pm2.21 ⊢ ( ¬ 𝑁 < 3 → ( 𝑁 < 3 → 𝑁 = 2 ) )
74 72 73 biimtrdi ⊢ ( 𝑁 ∈ ℤ → ( 3 ≤ 𝑁 → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
75 70 74 syldc ⊢ ( 2 < 𝑁 → ( 𝑁 ∈ ℤ → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
76 eqcom ⊢ ( 2 = 𝑁 ↔ 𝑁 = 2 )
77 76 biimpi ⊢ ( 2 = 𝑁 → 𝑁 = 2 )
78 77 2a1d ⊢ ( 2 = 𝑁 → ( 𝑁 ∈ ℤ → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
79 75 78 jaoi ⊢ ( ( 2 < 𝑁 ∨ 2 = 𝑁 ) → ( 𝑁 ∈ ℤ → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
80 79 com12 ⊢ ( 𝑁 ∈ ℤ → ( ( 2 < 𝑁 ∨ 2 = 𝑁 ) → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
81 63 80 sylbid ⊢ ( 𝑁 ∈ ℤ → ( 2 ≤ 𝑁 → ( 𝑁 < 3 → 𝑁 = 2 ) ) )
82 81 imp ⊢ ( ( 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → ( 𝑁 < 3 → 𝑁 = 2 ) )
83 2lt3 ⊢ 2 < 3
84 breq1 ⊢ ( 𝑁 = 2 → ( 𝑁 < 3 ↔ 2 < 3 ) )
85 83 84 mpbiri ⊢ ( 𝑁 = 2 → 𝑁 < 3 )
86 82 85 impbid1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → ( 𝑁 < 3 ↔ 𝑁 = 2 ) )
87 86 3adant1 ⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤ 𝑁 ) → ( 𝑁 < 3 ↔ 𝑁 = 2 ) )
88 59 87 sylbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 3 ↔ 𝑁 = 2 ) )
89 88 orbi1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 < 3 ∨ 𝑁 = 3 ) ↔ ( 𝑁 = 2 ∨ 𝑁 = 3 ) ) )
90 58 89 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 4 ↔ ( 𝑁 = 2 ∨ 𝑁 = 3 ) ) )
91 90 orbi1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 < 4 ∨ 𝑁 = 4 ) ↔ ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ) )
92 48 91 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 5 ↔ ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ) )
93 92 orbi1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 < 5 ∨ 𝑁 = 5 ) ↔ ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ) )
94 38 93 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 6 ↔ ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ) )
95 94 orbi1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 < 6 ∨ 𝑁 = 6 ) ↔ ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) ) )
96 27 95 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 7 ↔ ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) ) )
97 96 orbi1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 < 7 ∨ 𝑁 = 7 ) ↔ ( ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) ∨ 𝑁 = 7 ) ) )
98 16 97 bitrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 < 8 ↔ ( ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) ∨ 𝑁 = 7 ) ) )
99 98 orbi1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 < 8 ∨ 𝑁 = 8 ) ↔ ( ( ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) ∨ 𝑁 = 7 ) ∨ 𝑁 = 8 ) ) )
100 99 biimpd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 < 8 ∨ 𝑁 = 8 ) → ( ( ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) ∨ 𝑁 = 7 ) ∨ 𝑁 = 8 ) ) )
101 4 100 sylbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ≤ 8 → ( ( ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) ∨ 𝑁 = 7 ) ∨ 𝑁 = 8 ) ) )
102 101 imp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ≤ 8 ) → ( ( ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) ∨ 𝑁 = 7 ) ∨ 𝑁 = 8 ) )
103 2prm ⊢ 2 ∈ ℙ
104 eleq1 ⊢ ( 𝑁 = 2 → ( 𝑁 ∈ ℙ ↔ 2 ∈ ℙ ) )
105 103 104 mpbiri ⊢ ( 𝑁 = 2 → 𝑁 ∈ ℙ )
106 nnsum3primesprm ⊢ ( 𝑁 ∈ ℙ → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
107 105 106 syl ⊢ ( 𝑁 = 2 → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
108 3prm ⊢ 3 ∈ ℙ
109 eleq1 ⊢ ( 𝑁 = 3 → ( 𝑁 ∈ ℙ ↔ 3 ∈ ℙ ) )
110 108 109 mpbiri ⊢ ( 𝑁 = 3 → 𝑁 ∈ ℙ )
111 110 106 syl ⊢ ( 𝑁 = 3 → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
112 107 111 jaoi ⊢ ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
113 nnsum3primes4 ⊢ ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) )
114 eqeq1 ⊢ ( 𝑁 = 4 → ( 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ↔ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
115 114 anbi2d ⊢ ( 𝑁 = 4 → ( ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
116 115 2rexbidv ⊢ ( 𝑁 = 4 → ( ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
117 113 116 mpbiri ⊢ ( 𝑁 = 4 → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
118 112 117 jaoi ⊢ ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
119 5prm ⊢ 5 ∈ ℙ
120 eleq1 ⊢ ( 𝑁 = 5 → ( 𝑁 ∈ ℙ ↔ 5 ∈ ℙ ) )
121 119 120 mpbiri ⊢ ( 𝑁 = 5 → 𝑁 ∈ ℙ )
122 121 106 syl ⊢ ( 𝑁 = 5 → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
123 118 122 jaoi ⊢ ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
124 6gbe ⊢ 6 ∈ GoldbachEven
125 eleq1 ⊢ ( 𝑁 = 6 → ( 𝑁 ∈ GoldbachEven ↔ 6 ∈ GoldbachEven ) )
126 124 125 mpbiri ⊢ ( 𝑁 = 6 → 𝑁 ∈ GoldbachEven )
127 nnsum3primesgbe ⊢ ( 𝑁 ∈ GoldbachEven → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
128 126 127 syl ⊢ ( 𝑁 = 6 → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
129 123 128 jaoi ⊢ ( ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
130 7prm ⊢ 7 ∈ ℙ
131 eleq1 ⊢ ( 𝑁 = 7 → ( 𝑁 ∈ ℙ ↔ 7 ∈ ℙ ) )
132 130 131 mpbiri ⊢ ( 𝑁 = 7 → 𝑁 ∈ ℙ )
133 132 106 syl ⊢ ( 𝑁 = 7 → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
134 129 133 jaoi ⊢ ( ( ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) ∨ 𝑁 = 7 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
135 8gbe ⊢ 8 ∈ GoldbachEven
136 eleq1 ⊢ ( 𝑁 = 8 → ( 𝑁 ∈ GoldbachEven ↔ 8 ∈ GoldbachEven ) )
137 135 136 mpbiri ⊢ ( 𝑁 = 8 → 𝑁 ∈ GoldbachEven )
138 137 127 syl ⊢ ( 𝑁 = 8 → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
139 134 138 jaoi ⊢ ( ( ( ( ( ( ( 𝑁 = 2 ∨ 𝑁 = 3 ) ∨ 𝑁 = 4 ) ∨ 𝑁 = 5 ) ∨ 𝑁 = 6 ) ∨ 𝑁 = 7 ) ∨ 𝑁 = 8 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
140 102 139 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ≤ 8 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )