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 d f 1 d d 3 4 = k = 1 d f k

Proof

Step Hyp Ref Expression
1 2nn 2
2 1ne2 1 2
3 1ex 1 V
4 2ex 2 V
5 3 4 4 4 fpr 1 2 1 2 2 2 : 1 2 2 2
6 2prm 2
7 6 6 pm3.2i 2 2
8 4 4 prss 2 2 2 2
9 7 8 mpbi 2 2
10 fss 1 2 2 2 : 1 2 2 2 2 2 1 2 2 2 : 1 2
11 9 10 mpan2 1 2 2 2 : 1 2 2 2 1 2 2 2 : 1 2
12 2 5 11 mp2b 1 2 2 2 : 1 2
13 prmex V
14 prex 1 2 V
15 13 14 elmap 1 2 2 2 1 2 1 2 2 2 : 1 2
16 12 15 mpbir 1 2 2 2 1 2
17 2re 2
18 3re 3
19 2lt3 2 < 3
20 17 18 19 ltleii 2 3
21 2cn 2
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 2
31 30 ancri 2 2 2
32 3 jctl 2 1 V 2
33 2 a1i 2 1 2
34 25 29 31 32 33 sumpr 2 k 1 2 1 2 2 2 k = 2 + 2
35 21 34 ax-mp k 1 2 1 2 2 2 k = 2 + 2
36 2p2e4 2 + 2 = 4
37 35 36 eqtr2i 4 = k 1 2 1 2 2 2 k
38 20 37 pm3.2i 2 3 4 = k 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 k 1 2 f k = k 1 2 1 2 2 2 k
41 40 eqeq2d f = 1 2 2 2 4 = k 1 2 f k 4 = k 1 2 1 2 2 2 k
42 41 anbi2d f = 1 2 2 2 2 3 4 = k 1 2 f k 2 3 4 = k 1 2 1 2 2 2 k
43 42 rspcev 1 2 2 2 1 2 2 3 4 = k 1 2 1 2 2 2 k f 1 2 2 3 4 = k 1 2 f k
44 16 38 43 mp2an f 1 2 2 3 4 = k 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
49 fzpr 1 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 1 d = 1 2
57 breq1 d = 2 d 3 2 3
58 55 sumeq1d d = 2 k = 1 d f k = k 1 2 f k
59 58 eqeq2d d = 2 4 = k = 1 d f k 4 = k 1 2 f k
60 57 59 anbi12d d = 2 d 3 4 = k = 1 d f k 2 3 4 = k 1 2 f k
61 56 60 rexeqbidv d = 2 f 1 d d 3 4 = k = 1 d f k f 1 2 2 3 4 = k 1 2 f k
62 61 rspcev 2 f 1 2 2 3 4 = k 1 2 f k d f 1 d d 3 4 = k = 1 d f k
63 1 44 62 mp2an d f 1 d d 3 4 = k = 1 d f k