Metamath Proof Explorer

Theorem nnsum3primes4

Description: 4 is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 1ne2 
 |-  1 =/= 2
3 1ex 
 |-  1 e. _V
4 2ex 
 |-  2 e. _V
5 3 4 4 4 fpr 
 |-  ( 1 =/= 2 -> { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> { 2 , 2 } )
6 2prm 
 |-  2 e. Prime
7 6 6 pm3.2i 
 |-  ( 2 e. Prime /\ 2 e. Prime )
8 4 4 prss 
 |-  ( ( 2 e. Prime /\ 2 e. Prime ) <-> { 2 , 2 } C_ Prime )
9 7 8 mpbi 
 |-  { 2 , 2 } C_ Prime
10 fss 
 |-  ( ( { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> { 2 , 2 } /\ { 2 , 2 } C_ Prime ) -> { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> Prime )
11 9 10 mpan2 
 |-  ( { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> { 2 , 2 } -> { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> Prime )
12 2 5 11 mp2b 
 |-  { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> Prime
13 prmex 
 |-  Prime e. _V
14 prex 
 |-  { 1 , 2 } e. _V
15 13 14 elmap 
 |-  ( { <. 1 , 2 >. , <. 2 , 2 >. } e. ( Prime ^m { 1 , 2 } ) <-> { <. 1 , 2 >. , <. 2 , 2 >. } : { 1 , 2 } --> Prime )
16 12 15 mpbir 
 |-  { <. 1 , 2 >. , <. 2 , 2 >. } e. ( Prime ^m { 1 , 2 } )
17 2re 
 |-  2 e. RR
18 3re 
 |-  3 e. RR
19 2lt3 
 |-  2 < 3
20 17 18 19 ltleii 
 |-  2 <_ 3
21 2cn 
 |-  2 e. CC
22 fveq2 
 |-  ( k = 1 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 1 ) )
23 3 4 fvpr1 
 |-  ( 1 =/= 2 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 1 ) = 2 )
24 2 23 ax-mp 
 |-  ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 1 ) = 2
25 22 24 eqtrdi 
 |-  ( k = 1 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = 2 )
26 fveq2 
 |-  ( k = 2 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 2 ) )
27 4 4 fvpr2 
 |-  ( 1 =/= 2 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 2 ) = 2 )
28 2 27 ax-mp 
 |-  ( { <. 1 , 2 >. , <. 2 , 2 >. } ` 2 ) = 2
29 26 28 eqtrdi 
 |-  ( k = 2 -> ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = 2 )
30 id 
 |-  ( 2 e. CC -> 2 e. CC )
31 30 ancri 
 |-  ( 2 e. CC -> ( 2 e. CC /\ 2 e. CC ) )
32 3 jctl 
 |-  ( 2 e. CC -> ( 1 e. _V /\ 2 e. CC ) )
33 2 a1i 
 |-  ( 2 e. CC -> 1 =/= 2 )
34 25 29 31 32 33 sumpr 
 |-  ( 2 e. CC -> sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = ( 2 + 2 ) )
35 21 34 ax-mp 
 |-  sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) = ( 2 + 2 )
36 2p2e4 
 |-  ( 2 + 2 ) = 4
37 35 36 eqtr2i 
 |-  4 = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k )
38 20 37 pm3.2i 
 |-  ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) )
39 fveq1 
 |-  ( f = { <. 1 , 2 >. , <. 2 , 2 >. } -> ( f ` k ) = ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) )
40 39 sumeq2sdv 
 |-  ( f = { <. 1 , 2 >. , <. 2 , 2 >. } -> sum_ k e. { 1 , 2 } ( f ` k ) = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) )
41 40 eqeq2d 
 |-  ( f = { <. 1 , 2 >. , <. 2 , 2 >. } -> ( 4 = sum_ k e. { 1 , 2 } ( f ` k ) <-> 4 = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) ) )
42 41 anbi2d 
 |-  ( f = { <. 1 , 2 >. , <. 2 , 2 >. } -> ( ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) <-> ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) ) ) )
43 42 rspcev 
 |-  ( ( { <. 1 , 2 >. , <. 2 , 2 >. } e. ( Prime ^m { 1 , 2 } ) /\ ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( { <. 1 , 2 >. , <. 2 , 2 >. } ` k ) ) ) -> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) )
44 16 38 43 mp2an 
 |-  E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) )
45 oveq2 
 |-  ( d = 2 -> ( 1 ... d ) = ( 1 ... 2 ) )
46 df-2 
 |-  2 = ( 1 + 1 )
47 46 oveq2i 
 |-  ( 1 ... 2 ) = ( 1 ... ( 1 + 1 ) )
48 1z 
 |-  1 e. ZZ
49 fzpr 
 |-  ( 1 e. ZZ -> ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } )
50 48 49 ax-mp 
 |-  ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) }
51 1p1e2 
 |-  ( 1 + 1 ) = 2
52 51 preq2i 
 |-  { 1 , ( 1 + 1 ) } = { 1 , 2 }
53 50 52 eqtri 
 |-  ( 1 ... ( 1 + 1 ) ) = { 1 , 2 }
54 47 53 eqtri 
 |-  ( 1 ... 2 ) = { 1 , 2 }
55 45 54 eqtrdi 
 |-  ( d = 2 -> ( 1 ... d ) = { 1 , 2 } )
56 55 oveq2d 
 |-  ( d = 2 -> ( Prime ^m ( 1 ... d ) ) = ( Prime ^m { 1 , 2 } ) )
57 breq1 
 |-  ( d = 2 -> ( d <_ 3 <-> 2 <_ 3 ) )
58 55 sumeq1d 
 |-  ( d = 2 -> sum_ k e. ( 1 ... d ) ( f ` k ) = sum_ k e. { 1 , 2 } ( f ` k ) )
59 58 eqeq2d 
 |-  ( d = 2 -> ( 4 = sum_ k e. ( 1 ... d ) ( f ` k ) <-> 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) )
60 57 59 anbi12d 
 |-  ( d = 2 -> ( ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) ) )
61 56 60 rexeqbidv 
 |-  ( d = 2 -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) ) )
62 61 rspcev 
 |-  ( ( 2 e. NN /\ E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ 4 = sum_ k e. { 1 , 2 } ( f ` k ) ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
63 1 44 62 mp2an 
 |-  E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ 4 = sum_ k e. ( 1 ... d ) ( f ` k ) )