Metamath Proof Explorer


Theorem nnsum4primesgbe

Description: Any even Goldbach number is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020) (Proof shortened by AV, 2-Aug-2020)

Ref Expression
Assertion nnsum4primesgbe N GoldbachEven d f 1 d d 4 N = k = 1 d f k

Proof

Step Hyp Ref Expression
1 nnsum3primesgbe N GoldbachEven 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 GoldbachEven d f 1 d d 4 N = k = 1 d f k