Metamath Proof Explorer


Theorem nnsum3primesgbe

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

Ref Expression
Assertion nnsum3primesgbe N GoldbachEven d f 1 d d 3 N = k = 1 d f k

Proof

Step Hyp Ref Expression
1 isgbe N GoldbachEven N Even p q p Odd q Odd N = p + q
2 2nn 2
3 2 a1i p q p Odd q Odd N = p + q 2
4 oveq2 d = 2 1 d = 1 2
5 df-2 2 = 1 + 1
6 5 oveq2i 1 2 = 1 1 + 1
7 1z 1
8 fzpr 1 1 1 + 1 = 1 1 + 1
9 7 8 ax-mp 1 1 + 1 = 1 1 + 1
10 1p1e2 1 + 1 = 2
11 10 preq2i 1 1 + 1 = 1 2
12 6 9 11 3eqtri 1 2 = 1 2
13 4 12 eqtrdi d = 2 1 d = 1 2
14 13 oveq2d d = 2 1 d = 1 2
15 breq1 d = 2 d 3 2 3
16 13 sumeq1d d = 2 k = 1 d f k = k 1 2 f k
17 16 eqeq2d d = 2 N = k = 1 d f k N = k 1 2 f k
18 15 17 anbi12d d = 2 d 3 N = k = 1 d f k 2 3 N = k 1 2 f k
19 14 18 rexeqbidv d = 2 f 1 d d 3 N = k = 1 d f k f 1 2 2 3 N = k 1 2 f k
20 19 adantl p q p Odd q Odd N = p + q d = 2 f 1 d d 3 N = k = 1 d f k f 1 2 2 3 N = k 1 2 f k
21 1ne2 1 2
22 1ex 1 V
23 2ex 2 V
24 vex p V
25 vex q V
26 22 23 24 25 fpr 1 2 1 p 2 q : 1 2 p q
27 21 26 mp1i p q 1 p 2 q : 1 2 p q
28 prssi p q p q
29 27 28 fssd p q 1 p 2 q : 1 2
30 prmex V
31 prex 1 2 V
32 30 31 pm3.2i V 1 2 V
33 elmapg V 1 2 V 1 p 2 q 1 2 1 p 2 q : 1 2
34 32 33 mp1i p q 1 p 2 q 1 2 1 p 2 q : 1 2
35 29 34 mpbird p q 1 p 2 q 1 2
36 fveq1 f = 1 p 2 q f k = 1 p 2 q k
37 36 adantr f = 1 p 2 q k 1 2 f k = 1 p 2 q k
38 37 sumeq2dv f = 1 p 2 q k 1 2 f k = k 1 2 1 p 2 q k
39 38 eqeq1d f = 1 p 2 q k 1 2 f k = p + q k 1 2 1 p 2 q k = p + q
40 39 anbi2d f = 1 p 2 q 2 3 k 1 2 f k = p + q 2 3 k 1 2 1 p 2 q k = p + q
41 40 adantl p q f = 1 p 2 q 2 3 k 1 2 f k = p + q 2 3 k 1 2 1 p 2 q k = p + q
42 prmz p p
43 prmz q q
44 fveq2 k = 1 1 p 2 q k = 1 p 2 q 1
45 22 24 fvpr1 1 2 1 p 2 q 1 = p
46 21 45 ax-mp 1 p 2 q 1 = p
47 44 46 eqtrdi k = 1 1 p 2 q k = p
48 fveq2 k = 2 1 p 2 q k = 1 p 2 q 2
49 23 25 fvpr2 1 2 1 p 2 q 2 = q
50 21 49 ax-mp 1 p 2 q 2 = q
51 48 50 eqtrdi k = 2 1 p 2 q k = q
52 zcn p p
53 zcn q q
54 52 53 anim12i p q p q
55 7 2 pm3.2i 1 2
56 55 a1i p q 1 2
57 21 a1i p q 1 2
58 47 51 54 56 57 sumpr p q k 1 2 1 p 2 q k = p + q
59 42 43 58 syl2an p q k 1 2 1 p 2 q k = p + q
60 2re 2
61 3re 3
62 2lt3 2 < 3
63 60 61 62 ltleii 2 3
64 59 63 jctil p q 2 3 k 1 2 1 p 2 q k = p + q
65 35 41 64 rspcedvd p q f 1 2 2 3 k 1 2 f k = p + q
66 65 adantr p q p Odd q Odd N = p + q f 1 2 2 3 k 1 2 f k = p + q
67 eqeq1 N = p + q N = k 1 2 f k p + q = k 1 2 f k
68 eqcom p + q = k 1 2 f k k 1 2 f k = p + q
69 67 68 bitrdi N = p + q N = k 1 2 f k k 1 2 f k = p + q
70 69 anbi2d N = p + q 2 3 N = k 1 2 f k 2 3 k 1 2 f k = p + q
71 70 rexbidv N = p + q f 1 2 2 3 N = k 1 2 f k f 1 2 2 3 k 1 2 f k = p + q
72 71 3ad2ant3 p Odd q Odd N = p + q f 1 2 2 3 N = k 1 2 f k f 1 2 2 3 k 1 2 f k = p + q
73 72 adantl p q p Odd q Odd N = p + q f 1 2 2 3 N = k 1 2 f k f 1 2 2 3 k 1 2 f k = p + q
74 66 73 mpbird p q p Odd q Odd N = p + q f 1 2 2 3 N = k 1 2 f k
75 3 20 74 rspcedvd p q p Odd q Odd N = p + q d f 1 d d 3 N = k = 1 d f k
76 75 a1d p q p Odd q Odd N = p + q N Even d f 1 d d 3 N = k = 1 d f k
77 76 ex p q p Odd q Odd N = p + q N Even d f 1 d d 3 N = k = 1 d f k
78 77 rexlimivv p q p Odd q Odd N = p + q N Even d f 1 d d 3 N = k = 1 d f k
79 78 impcom N Even p q p Odd q Odd N = p + q d f 1 d d 3 N = k = 1 d f k
80 1 79 sylbi N GoldbachEven d f 1 d d 3 N = k = 1 d f k