This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. GoldbachEven -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )

Proof

Step Hyp Ref Expression
1 isgbe 
 |-  ( N e. GoldbachEven <-> ( N e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) ) )
2 2nn 
 |-  2 e. NN
3 2 a1i 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) ) -> 2 e. NN )
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 e. ZZ
8 fzpr 
 |-  ( 1 e. ZZ -> ( 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 -> ( Prime ^m ( 1 ... d ) ) = ( Prime ^m { 1 , 2 } ) )
15 breq1 
 |-  ( d = 2 -> ( d <_ 3 <-> 2 <_ 3 ) )
16 13 sumeq1d 
 |-  ( d = 2 -> sum_ k e. ( 1 ... d ) ( f ` k ) = sum_ k e. { 1 , 2 } ( f ` k ) )
17 16 eqeq2d 
 |-  ( d = 2 -> ( N = sum_ k e. ( 1 ... d ) ( f ` k ) <-> N = sum_ k e. { 1 , 2 } ( f ` k ) ) )
18 15 17 anbi12d 
 |-  ( d = 2 -> ( ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> ( 2 <_ 3 /\ N = sum_ k e. { 1 , 2 } ( f ` k ) ) ) )
19 14 18 rexeqbidv 
 |-  ( d = 2 -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ N = sum_ k e. { 1 , 2 } ( f ` k ) ) ) )
20 19 adantl 
 |-  ( ( ( ( p e. Prime /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) ) /\ d = 2 ) -> ( E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) <-> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ N = sum_ k e. { 1 , 2 } ( f ` k ) ) ) )
21 1ne2 
 |-  1 =/= 2
22 1ex 
 |-  1 e. _V
23 2ex 
 |-  2 e. _V
24 vex 
 |-  p e. _V
25 vex 
 |-  q e. _V
26 22 23 24 25 fpr 
 |-  ( 1 =/= 2 -> { <. 1 , p >. , <. 2 , q >. } : { 1 , 2 } --> { p , q } )
27 21 26 mp1i 
 |-  ( ( p e. Prime /\ q e. Prime ) -> { <. 1 , p >. , <. 2 , q >. } : { 1 , 2 } --> { p , q } )
28 prssi 
 |-  ( ( p e. Prime /\ q e. Prime ) -> { p , q } C_ Prime )
29 27 28 fssd 
 |-  ( ( p e. Prime /\ q e. Prime ) -> { <. 1 , p >. , <. 2 , q >. } : { 1 , 2 } --> Prime )
30 prmex 
 |-  Prime e. _V
31 prex 
 |-  { 1 , 2 } e. _V
32 30 31 pm3.2i 
 |-  ( Prime e. _V /\ { 1 , 2 } e. _V )
33 elmapg 
 |-  ( ( Prime e. _V /\ { 1 , 2 } e. _V ) -> ( { <. 1 , p >. , <. 2 , q >. } e. ( Prime ^m { 1 , 2 } ) <-> { <. 1 , p >. , <. 2 , q >. } : { 1 , 2 } --> Prime ) )
34 32 33 mp1i 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( { <. 1 , p >. , <. 2 , q >. } e. ( Prime ^m { 1 , 2 } ) <-> { <. 1 , p >. , <. 2 , q >. } : { 1 , 2 } --> Prime ) )
35 29 34 mpbird 
 |-  ( ( p e. Prime /\ q e. Prime ) -> { <. 1 , p >. , <. 2 , q >. } e. ( Prime ^m { 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 e. { 1 , 2 } ) -> ( f ` k ) = ( { <. 1 , p >. , <. 2 , q >. } ` k ) )
38 37 sumeq2dv 
 |-  ( f = { <. 1 , p >. , <. 2 , q >. } -> sum_ k e. { 1 , 2 } ( f ` k ) = sum_ k e. { 1 , 2 } ( { <. 1 , p >. , <. 2 , q >. } ` k ) )
39 38 eqeq1d 
 |-  ( f = { <. 1 , p >. , <. 2 , q >. } -> ( sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) <-> sum_ k e. { 1 , 2 } ( { <. 1 , p >. , <. 2 , q >. } ` k ) = ( p + q ) ) )
40 39 anbi2d 
 |-  ( f = { <. 1 , p >. , <. 2 , q >. } -> ( ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) ) <-> ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( { <. 1 , p >. , <. 2 , q >. } ` k ) = ( p + q ) ) ) )
41 40 adantl 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ f = { <. 1 , p >. , <. 2 , q >. } ) -> ( ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) ) <-> ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( { <. 1 , p >. , <. 2 , q >. } ` k ) = ( p + q ) ) ) )
42 prmz 
 |-  ( p e. Prime -> p e. ZZ )
43 prmz 
 |-  ( q e. Prime -> q e. ZZ )
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 e. ZZ -> p e. CC )
53 zcn 
 |-  ( q e. ZZ -> q e. CC )
54 52 53 anim12i 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> ( p e. CC /\ q e. CC ) )
55 7 2 pm3.2i 
 |-  ( 1 e. ZZ /\ 2 e. NN )
56 55 a1i 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> ( 1 e. ZZ /\ 2 e. NN ) )
57 21 a1i 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> 1 =/= 2 )
58 47 51 54 56 57 sumpr 
 |-  ( ( p e. ZZ /\ q e. ZZ ) -> sum_ k e. { 1 , 2 } ( { <. 1 , p >. , <. 2 , q >. } ` k ) = ( p + q ) )
59 42 43 58 syl2an 
 |-  ( ( p e. Prime /\ q e. Prime ) -> sum_ k e. { 1 , 2 } ( { <. 1 , p >. , <. 2 , q >. } ` k ) = ( p + q ) )
60 2re 
 |-  2 e. RR
61 3re 
 |-  3 e. RR
62 2lt3 
 |-  2 < 3
63 60 61 62 ltleii 
 |-  2 <_ 3
64 59 63 jctil 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( { <. 1 , p >. , <. 2 , q >. } ` k ) = ( p + q ) ) )
65 35 41 64 rspcedvd 
 |-  ( ( p e. Prime /\ q e. Prime ) -> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) ) )
66 65 adantr 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) ) -> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) ) )
67 eqeq1 
 |-  ( N = ( p + q ) -> ( N = sum_ k e. { 1 , 2 } ( f ` k ) <-> ( p + q ) = sum_ k e. { 1 , 2 } ( f ` k ) ) )
68 eqcom 
 |-  ( ( p + q ) = sum_ k e. { 1 , 2 } ( f ` k ) <-> sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) )
69 67 68 bitrdi 
 |-  ( N = ( p + q ) -> ( N = sum_ k e. { 1 , 2 } ( f ` k ) <-> sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) ) )
70 69 anbi2d 
 |-  ( N = ( p + q ) -> ( ( 2 <_ 3 /\ N = sum_ k e. { 1 , 2 } ( f ` k ) ) <-> ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) ) ) )
71 70 rexbidv 
 |-  ( N = ( p + q ) -> ( E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ N = sum_ k e. { 1 , 2 } ( f ` k ) ) <-> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) ) ) )
72 71 3ad2ant3 
 |-  ( ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) -> ( E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ N = sum_ k e. { 1 , 2 } ( f ` k ) ) <-> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) ) ) )
73 72 adantl 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) ) -> ( E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ N = sum_ k e. { 1 , 2 } ( f ` k ) ) <-> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ sum_ k e. { 1 , 2 } ( f ` k ) = ( p + q ) ) ) )
74 66 73 mpbird 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) ) -> E. f e. ( Prime ^m { 1 , 2 } ) ( 2 <_ 3 /\ N = sum_ k e. { 1 , 2 } ( f ` k ) ) )
75 3 20 74 rspcedvd 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
76 75 a1d 
 |-  ( ( ( p e. Prime /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) ) -> ( N e. Even -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
77 76 ex 
 |-  ( ( p e. Prime /\ q e. Prime ) -> ( ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) -> ( N e. Even -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) ) )
78 77 rexlimivv 
 |-  ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) -> ( N e. Even -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) ) )
79 78 impcom 
 |-  ( ( N e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ N = ( p + q ) ) ) -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )
80 1 79 sylbi 
 |-  ( N e. GoldbachEven -> E. d e. NN E. f e. ( Prime ^m ( 1 ... d ) ) ( d <_ 3 /\ N = sum_ k e. ( 1 ... d ) ( f ` k ) ) )