Metamath Proof Explorer

Theorem stgoldbnnsum4prm

Description: If the (strong) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes. (Contributed by AV, 27-Jul-2020)

Ref Expression
Assertion stgoldbnnsum4prm 
|- ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> A. n e. ( ZZ>= ` 2 ) 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 stgoldbwt 
 |-  ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) )
2 wtgoldbnnsum4prm 
 |-  ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> A. n e. ( ZZ>= ` 2 ) E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
3 1 2 syl 
 |-  ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> A. n e. ( ZZ>= ` 2 ) E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 4 /\ n = sum_ k e. ( 1 ... d ) ( f ` k ) ) )