Metamath Proof Explorer


Theorem nnsum4primesle9

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

Ref Expression
Assertion nnsum4primesle9 N 2 N 8 d f 1 d d 4 N = k = 1 d f k

Proof

Step Hyp Ref Expression
1 nnsum3primesle9 N 2 N 8 d f 1 d d 3 N = k = 1 d f k
2 3lt4 3 < 4
3 nnre d d
4 3re 3
5 4 a1i d 3
6 4re 4
7 6 a1i d 4
8 leltletr d 3 4 d 3 3 < 4 d 4
9 3 5 7 8 syl3anc d d 3 3 < 4 d 4
10 2 9 mpan2i d d 3 d 4
11 10 anim1d d d 3 N = k = 1 d f k d 4 N = k = 1 d f k
12 11 reximdv d f 1 d d 3 N = k = 1 d f k f 1 d d 4 N = k = 1 d f k
13 12 reximia d f 1 d d 3 N = k = 1 d f k d f 1 d d 4 N = k = 1 d f k
14 1 13 syl N 2 N 8 d f 1 d d 4 N = k = 1 d f k