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 e. GoldbachEven -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )

Proof

Step Hyp Ref Expression
1 nnsum3primesgbe 
 |-  ( N e. GoldbachEven -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
2 3lt4 
 |-  3 < 4
3 nnre 
 |-  ( d e. NN -> d e. RR )
4 3re 
 |-  3 e. RR
5 4 a1i 
 |-  ( d e. NN -> 3 e. RR )
6 4re 
 |-  4 e. RR
7 6 a1i 
 |-  ( d e. NN -> 4 e. RR )
8 leltletr 
 |-  ( ( d e. RR /\ 3 e. RR /\ 4 e. RR ) -> ( ( d <_ 3 /\ 3 < 4 ) -> d <_ 4 ) )
9 3 5 7 8 syl3anc 
 |-  ( d e. NN -> ( ( d <_ 3 /\ 3 < 4 ) -> d <_ 4 ) )
10 2 9 mpan2i 
 |-  ( d e. NN -> ( d <_ 3 -> d <_ 4 ) )
11 10 anim1d 
 |-  ( d e. NN -> ( ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) -> ( d <_ 4 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
12 11 reximdv 
 |-  ( d e. NN -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) -> E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
13 12 reximia 
 |-  ( E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
14 1 13 syl 
 |-  ( N e. GoldbachEven -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )