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 syl5bi ( 𝑁 ∈ ℤ → ( 2 < 𝑁 → 3 ≤ 𝑁 ) )
71 52 a1i ( 𝑁 ∈ ℤ → 3 ∈ ℝ )
72 71 62 lenltd ( 𝑁 ∈ ℤ → ( 3 ≤ 𝑁 ↔ ¬ 𝑁 < 3 ) )
73 pm2.21 ( ¬ 𝑁 < 3 → ( 𝑁 < 3 → 𝑁 = 2 ) )
74 72 73 syl6bi ( 𝑁 ∈ ℤ → ( 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 ... 𝑑 ) ( 𝑓𝑘 ) ) )