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 N 2 N 8 d f 1 d d 3 N = k = 1 d f k

Proof

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