Metamath Proof Explorer

Theorem nnsum3primesprm

Description: Every prime is "the sum of at most 3" (actually one - the prime itself) primes. (Contributed by AV, 2-Aug-2020) (Proof shortened by AV, 17-Apr-2021)

Ref Expression
Assertion nnsum3primesprm 
|- ( P e. Prime -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ P = sum_ k e. ( 1 ... d ) ( f ` k ) ) )

Proof

Step Hyp Ref Expression
1 1nn 
 |-  1 e. NN
2 1zzd 
 |-  ( P e. Prime -> 1 e. ZZ )
3 id 
 |-  ( P e. Prime -> P e. Prime )
4 2 3 fsnd 
 |-  ( P e. Prime -> { <. 1 , P >. } : { 1 } --> Prime )
5 prmex 
 |-  Prime e. _V
6 snex 
 |-  { 1 } e. _V
7 5 6 elmap 
 |-  ( { <. 1 , P >. } e. ( Prime ^m { 1 } ) <-> { <. 1 , P >. } : { 1 } --> Prime )
8 4 7 sylibr 
 |-  ( P e. Prime -> { <. 1 , P >. } e. ( Prime ^m { 1 } ) )
9 1re 
 |-  1 e. RR
10 simpl 
 |-  ( ( P e. Prime /\ k e. { 1 } ) -> P e. Prime )
11 fvsng 
 |-  ( ( 1 e. RR /\ P e. Prime ) -> ( { <. 1 , P >. } ` 1 ) = P )
12 9 10 11 sylancr 
 |-  ( ( P e. Prime /\ k e. { 1 } ) -> ( { <. 1 , P >. } ` 1 ) = P )
13 12 sumeq2dv 
 |-  ( P e. Prime -> sum_ k e. { 1 } ( { <. 1 , P >. } ` 1 ) = sum_ k e. { 1 } P )
14 prmz 
 |-  ( P e. Prime -> P e. ZZ )
15 14 zcnd 
 |-  ( P e. Prime -> P e. CC )
16 eqidd 
 |-  ( k = 1 -> P = P )
17 16 sumsn 
 |-  ( ( 1 e. RR /\ P e. CC ) -> sum_ k e. { 1 } P = P )
18 9 15 17 sylancr 
 |-  ( P e. Prime -> sum_ k e. { 1 } P = P )
19 13 18 eqtr2d 
 |-  ( P e. Prime -> P = sum_ k e. { 1 } ( { <. 1 , P >. } ` 1 ) )
20 1le3 
 |-  1 <_ 3
21 19 20 jctil 
 |-  ( P e. Prime -> ( 1 <_ 3 /\ P = sum_ k e. { 1 } ( { <. 1 , P >. } ` 1 ) ) )
22 simpl 
 |-  ( ( f = { <. 1 , P >. } /\ k e. { 1 } ) -> f = { <. 1 , P >. } )
23 elsni 
 |-  ( k e. { 1 } -> k = 1 )
24 23 adantl 
 |-  ( ( f = { <. 1 , P >. } /\ k e. { 1 } ) -> k = 1 )
25 22 24 fveq12d 
 |-  ( ( f = { <. 1 , P >. } /\ k e. { 1 } ) -> ( f ` k ) = ( { <. 1 , P >. } ` 1 ) )
26 25 sumeq2dv 
 |-  ( f = { <. 1 , P >. } -> sum_ k e. { 1 } ( f ` k ) = sum_ k e. { 1 } ( { <. 1 , P >. } ` 1 ) )
27 26 eqeq2d 
 |-  ( f = { <. 1 , P >. } -> ( P = sum_ k e. { 1 } ( f ` k ) <-> P = sum_ k e. { 1 } ( { <. 1 , P >. } ` 1 ) ) )
28 27 anbi2d 
 |-  ( f = { <. 1 , P >. } -> ( ( 1 <_ 3 /\ P = sum_ k e. { 1 } ( f ` k ) ) <-> ( 1 <_ 3 /\ P = sum_ k e. { 1 } ( { <. 1 , P >. } ` 1 ) ) ) )
29 28 rspcev 
 |-  ( ( { <. 1 , P >. } e. ( Prime ^m { 1 } ) /\ ( 1 <_ 3 /\ P = sum_ k e. { 1 } ( { <. 1 , P >. } ` 1 ) ) ) -> E. f e. ( Prime ^m { 1 } ) ( 1 <_ 3 /\ P = sum_ k e. { 1 } ( f ` k ) ) )
30 8 21 29 syl2anc 
 |-  ( P e. Prime -> E. f e. ( Prime ^m { 1 } ) ( 1 <_ 3 /\ P = sum_ k e. { 1 } ( f ` k ) ) )
31 oveq2 
 |-  ( d = 1 -> ( 1 ... d ) = ( 1 ... 1 ) )
32 1z 
 |-  1 e. ZZ
33 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
34 32 33 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
35 31 34 eqtrdi 
 |-  ( d = 1 -> ( 1 ... d ) = { 1 } )
36 35 oveq2d 
 |-  ( d = 1 -> ( Prime ^m ( 1 ... d ) ) = ( Prime ^m { 1 } ) )
37 breq1 
 |-  ( d = 1 -> ( d <_ 3 <-> 1 <_ 3 ) )
38 35 sumeq1d 
 |-  ( d = 1 -> sum_ k e. ( 1 ... d ) ( f ` k ) = sum_ k e. { 1 } ( f ` k ) )
39 38 eqeq2d 
 |-  ( d = 1 -> ( P = sum_ k e. ( 1 ... d ) ( f ` k ) <-> P = sum_ k e. { 1 } ( f ` k ) ) )
40 37 39 anbi12d 
 |-  ( d = 1 -> ( ( d <_ 3 /\ P = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> ( 1 <_ 3 /\ P = sum_ k e. { 1 } ( f ` k ) ) ) )
41 36 40 rexeqbidv 
 |-  ( d = 1 -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ P = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m { 1 } ) ( 1 <_ 3 /\ P = sum_ k e. { 1 } ( f ` k ) ) ) )
42 41 rspcev 
 |-  ( ( 1 e. NN /\ E. f e. ( Prime ^m { 1 } ) ( 1 <_ 3 /\ P = sum_ k e. { 1 } ( f ` k ) ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ P = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
43 1 30 42 sylancr 
 |-  ( P e. Prime -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ P = sum_ k e. ( 1 ... d ) ( f ` k ) ) )