Metamath Proof Explorer

Theorem nnsum4primeseven

Description: If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of 4 primes. (Contributed by AV, 25-Jul-2020)

Ref Expression
Assertion nnsum4primeseven 
|- ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )

Proof

Step Hyp Ref Expression
1 evengpop3 
 |-  ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> E. o e. GoldbachOddW N = ( o + 3 ) ) )
2 1 imp 
 |-  ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) -> E. o e. GoldbachOddW N = ( o + 3 ) )
3 simplll 
 |-  ( ( ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) /\ o e. GoldbachOddW ) /\ N = ( o + 3 ) ) -> A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) )
4 6nn 
 |-  6 e. NN
5 4 nnzi 
 |-  6 e. ZZ
6 5 a1i 
 |-  ( N e. ( ZZ>= ` 9 ) -> 6 e. ZZ )
7 3z 
 |-  3 e. ZZ
8 7 a1i 
 |-  ( N e. ( ZZ>= ` 9 ) -> 3 e. ZZ )
9 6p3e9 
 |-  ( 6 + 3 ) = 9
10 9 eqcomi 
 |-  9 = ( 6 + 3 )
11 10 fveq2i 
 |-  ( ZZ>= ` 9 ) = ( ZZ>= ` ( 6 + 3 ) )
12 11 eleq2i 
 |-  ( N e. ( ZZ>= ` 9 ) <-> N e. ( ZZ>= ` ( 6 + 3 ) ) )
13 12 biimpi 
 |-  ( N e. ( ZZ>= ` 9 ) -> N e. ( ZZ>= ` ( 6 + 3 ) ) )
14 eluzsub 
 |-  ( ( 6 e. ZZ /\ 3 e. ZZ /\ N e. ( ZZ>= ` ( 6 + 3 ) ) ) -> ( N - 3 ) e. ( ZZ>= ` 6 ) )
15 6 8 13 14 syl3anc 
 |-  ( N e. ( ZZ>= ` 9 ) -> ( N - 3 ) e. ( ZZ>= ` 6 ) )
16 15 adantr 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> ( N - 3 ) e. ( ZZ>= ` 6 ) )
17 16 ad3antlr 
 |-  ( ( ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) /\ o e. GoldbachOddW ) /\ N = ( o + 3 ) ) -> ( N - 3 ) e. ( ZZ>= ` 6 ) )
18 3odd 
 |-  3 e. Odd
19 18 a1i 
 |-  ( N e. ( ZZ>= ` 9 ) -> 3 e. Odd )
20 19 anim1i 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> ( 3 e. Odd /\ N e. Even ) )
21 20 adantl 
 |-  ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) -> ( 3 e. Odd /\ N e. Even ) )
22 21 ancomd 
 |-  ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) -> ( N e. Even /\ 3 e. Odd ) )
23 22 adantr 
 |-  ( ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) /\ o e. GoldbachOddW ) -> ( N e. Even /\ 3 e. Odd ) )
24 23 adantr 
 |-  ( ( ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) /\ o e. GoldbachOddW ) /\ N = ( o + 3 ) ) -> ( N e. Even /\ 3 e. Odd ) )
25 emoo 
 |-  ( ( N e. Even /\ 3 e. Odd ) -> ( N - 3 ) e. Odd )
26 24 25 syl 
 |-  ( ( ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) /\ o e. GoldbachOddW ) /\ N = ( o + 3 ) ) -> ( N - 3 ) e. Odd )
27 nnsum4primesodd 
 |-  ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> ( ( ( N - 3 ) e. ( ZZ>= ` 6 ) /\ ( N - 3 ) e. Odd ) -> E. g e. ( Prime ^m ( 1 ... 3 ) ) ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) ) )
28 27 imp 
 |-  ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( ( N - 3 ) e. ( ZZ>= ` 6 ) /\ ( N - 3 ) e. Odd ) ) -> E. g e. ( Prime ^m ( 1 ... 3 ) ) ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) )
29 3 17 26 28 syl12anc 
 |-  ( ( ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) /\ o e. GoldbachOddW ) /\ N = ( o + 3 ) ) -> E. g e. ( Prime ^m ( 1 ... 3 ) ) ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) )
30 simpr 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> g : ( 1 ... 3 ) --> Prime )
31 4z 
 |-  4 e. ZZ
32 fzonel 
 |-  -. 4 e. ( 1 ..^ 4 )
33 fzoval 
 |-  ( 4 e. ZZ -> ( 1 ..^ 4 ) = ( 1 ... ( 4 - 1 ) ) )
34 31 33 ax-mp 
 |-  ( 1 ..^ 4 ) = ( 1 ... ( 4 - 1 ) )
35 4cn 
 |-  4 e. CC
36 ax-1cn 
 |-  1 e. CC
37 3cn 
 |-  3 e. CC
38 35 36 37 3pm3.2i 
 |-  ( 4 e. CC /\ 1 e. CC /\ 3 e. CC )
39 3p1e4 
 |-  ( 3 + 1 ) = 4
40 subadd2 
 |-  ( ( 4 e. CC /\ 1 e. CC /\ 3 e. CC ) -> ( ( 4 - 1 ) = 3 <-> ( 3 + 1 ) = 4 ) )
41 39 40 mpbiri 
 |-  ( ( 4 e. CC /\ 1 e. CC /\ 3 e. CC ) -> ( 4 - 1 ) = 3 )
42 38 41 ax-mp 
 |-  ( 4 - 1 ) = 3
43 42 oveq2i 
 |-  ( 1 ... ( 4 - 1 ) ) = ( 1 ... 3 )
44 34 43 eqtri 
 |-  ( 1 ..^ 4 ) = ( 1 ... 3 )
45 44 eqcomi 
 |-  ( 1 ... 3 ) = ( 1 ..^ 4 )
46 45 eleq2i 
 |-  ( 4 e. ( 1 ... 3 ) <-> 4 e. ( 1 ..^ 4 ) )
47 32 46 mtbir 
 |-  -. 4 e. ( 1 ... 3 )
48 31 47 pm3.2i 
 |-  ( 4 e. ZZ /\ -. 4 e. ( 1 ... 3 ) )
49 48 a1i 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( 4 e. ZZ /\ -. 4 e. ( 1 ... 3 ) ) )
50 3prm 
 |-  3 e. Prime
51 50 a1i 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> 3 e. Prime )
52 fsnunf 
 |-  ( ( g : ( 1 ... 3 ) --> Prime /\ ( 4 e. ZZ /\ -. 4 e. ( 1 ... 3 ) ) /\ 3 e. Prime ) -> ( g u. { <. 4 , 3 >. } ) : ( ( 1 ... 3 ) u. { 4 } ) --> Prime )
53 30 49 51 52 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( g u. { <. 4 , 3 >. } ) : ( ( 1 ... 3 ) u. { 4 } ) --> Prime )
54 fzval3 
 |-  ( 4 e. ZZ -> ( 1 ... 4 ) = ( 1 ..^ ( 4 + 1 ) ) )
55 31 54 ax-mp 
 |-  ( 1 ... 4 ) = ( 1 ..^ ( 4 + 1 ) )
56 1z 
 |-  1 e. ZZ
57 1re 
 |-  1 e. RR
58 4re 
 |-  4 e. RR
59 1lt4 
 |-  1 < 4
60 57 58 59 ltleii 
 |-  1 <_ 4
61 eluz2 
 |-  ( 4 e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ 4 e. ZZ /\ 1 <_ 4 ) )
62 56 31 60 61 mpbir3an 
 |-  4 e. ( ZZ>= ` 1 )
63 fzosplitsn 
 |-  ( 4 e. ( ZZ>= ` 1 ) -> ( 1 ..^ ( 4 + 1 ) ) = ( ( 1 ..^ 4 ) u. { 4 } ) )
64 62 63 ax-mp 
 |-  ( 1 ..^ ( 4 + 1 ) ) = ( ( 1 ..^ 4 ) u. { 4 } )
65 44 uneq1i 
 |-  ( ( 1 ..^ 4 ) u. { 4 } ) = ( ( 1 ... 3 ) u. { 4 } )
66 55 64 65 3eqtri 
 |-  ( 1 ... 4 ) = ( ( 1 ... 3 ) u. { 4 } )
67 66 feq2i 
 |-  ( ( g u. { <. 4 , 3 >. } ) : ( 1 ... 4 ) --> Prime <-> ( g u. { <. 4 , 3 >. } ) : ( ( 1 ... 3 ) u. { 4 } ) --> Prime )
68 53 67 sylibr 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( g u. { <. 4 , 3 >. } ) : ( 1 ... 4 ) --> Prime )
69 prmex 
 |-  Prime e. _V
70 ovex 
 |-  ( 1 ... 4 ) e. _V
71 69 70 pm3.2i 
 |-  ( Prime e. _V /\ ( 1 ... 4 ) e. _V )
72 elmapg 
 |-  ( ( Prime e. _V /\ ( 1 ... 4 ) e. _V ) -> ( ( g u. { <. 4 , 3 >. } ) e. ( Prime ^m ( 1 ... 4 ) ) <-> ( g u. { <. 4 , 3 >. } ) : ( 1 ... 4 ) --> Prime ) )
73 71 72 mp1i 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( g u. { <. 4 , 3 >. } ) e. ( Prime ^m ( 1 ... 4 ) ) <-> ( g u. { <. 4 , 3 >. } ) : ( 1 ... 4 ) --> Prime ) )
74 68 73 mpbird 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( g u. { <. 4 , 3 >. } ) e. ( Prime ^m ( 1 ... 4 ) ) )
75 74 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) ) -> ( g u. { <. 4 , 3 >. } ) e. ( Prime ^m ( 1 ... 4 ) ) )
76 fveq1 
 |-  ( f = ( g u. { <. 4 , 3 >. } ) -> ( f ` k ) = ( ( g u. { <. 4 , 3 >. } ) ` k ) )
77 76 adantr 
 |-  ( ( f = ( g u. { <. 4 , 3 >. } ) /\ k e. ( 1 ... 4 ) ) -> ( f ` k ) = ( ( g u. { <. 4 , 3 >. } ) ` k ) )
78 77 sumeq2dv 
 |-  ( f = ( g u. { <. 4 , 3 >. } ) -> sum_ k e. ( 1 ... 4 ) ( f ` k ) = sum_ k e. ( 1 ... 4 ) ( ( g u. { <. 4 , 3 >. } ) ` k ) )
79 78 eqeq2d 
 |-  ( f = ( g u. { <. 4 , 3 >. } ) -> ( N = sum_ k e. ( 1 ... 4 ) ( f ` k ) <-> N = sum_ k e. ( 1 ... 4 ) ( ( g u. { <. 4 , 3 >. } ) ` k ) ) )
80 79 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) ) /\ f = ( g u. { <. 4 , 3 >. } ) ) -> ( N = sum_ k e. ( 1 ... 4 ) ( f ` k ) <-> N = sum_ k e. ( 1 ... 4 ) ( ( g u. { <. 4 , 3 >. } ) ` k ) ) )
81 62 a1i 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> 4 e. ( ZZ>= ` 1 ) )
82 66 eleq2i 
 |-  ( k e. ( 1 ... 4 ) <-> k e. ( ( 1 ... 3 ) u. { 4 } ) )
83 elun 
 |-  ( k e. ( ( 1 ... 3 ) u. { 4 } ) <-> ( k e. ( 1 ... 3 ) \/ k e. { 4 } ) )
84 velsn 
 |-  ( k e. { 4 } <-> k = 4 )
85 84 orbi2i 
 |-  ( ( k e. ( 1 ... 3 ) \/ k e. { 4 } ) <-> ( k e. ( 1 ... 3 ) \/ k = 4 ) )
86 82 83 85 3bitri 
 |-  ( k e. ( 1 ... 4 ) <-> ( k e. ( 1 ... 3 ) \/ k = 4 ) )
87 elfz2 
 |-  ( k e. ( 1 ... 3 ) <-> ( ( 1 e. ZZ /\ 3 e. ZZ /\ k e. ZZ ) /\ ( 1 <_ k /\ k <_ 3 ) ) )
88 3re 
 |-  3 e. RR
89 88 58 pm3.2i 
 |-  ( 3 e. RR /\ 4 e. RR )
90 3lt4 
 |-  3 < 4
91 ltnle 
 |-  ( ( 3 e. RR /\ 4 e. RR ) -> ( 3 < 4 <-> -. 4 <_ 3 ) )
92 90 91 mpbii 
 |-  ( ( 3 e. RR /\ 4 e. RR ) -> -. 4 <_ 3 )
93 89 92 ax-mp 
 |-  -. 4 <_ 3
94 breq1 
 |-  ( k = 4 -> ( k <_ 3 <-> 4 <_ 3 ) )
95 94 eqcoms 
 |-  ( 4 = k -> ( k <_ 3 <-> 4 <_ 3 ) )
96 93 95 mtbiri 
 |-  ( 4 = k -> -. k <_ 3 )
97 96 a1i 
 |-  ( k e. ZZ -> ( 4 = k -> -. k <_ 3 ) )
98 97 necon2ad 
 |-  ( k e. ZZ -> ( k <_ 3 -> 4 =/= k ) )
99 98 adantld 
 |-  ( k e. ZZ -> ( ( 1 <_ k /\ k <_ 3 ) -> 4 =/= k ) )
100 99 3ad2ant3 
 |-  ( ( 1 e. ZZ /\ 3 e. ZZ /\ k e. ZZ ) -> ( ( 1 <_ k /\ k <_ 3 ) -> 4 =/= k ) )
101 100 imp 
 |-  ( ( ( 1 e. ZZ /\ 3 e. ZZ /\ k e. ZZ ) /\ ( 1 <_ k /\ k <_ 3 ) ) -> 4 =/= k )
102 87 101 sylbi 
 |-  ( k e. ( 1 ... 3 ) -> 4 =/= k )
103 102 adantr 
 |-  ( ( k e. ( 1 ... 3 ) /\ g : ( 1 ... 3 ) --> Prime ) -> 4 =/= k )
104 fvunsn 
 |-  ( 4 =/= k -> ( ( g u. { <. 4 , 3 >. } ) ` k ) = ( g ` k ) )
105 103 104 syl 
 |-  ( ( k e. ( 1 ... 3 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) = ( g ` k ) )
106 ffvelrn 
 |-  ( ( g : ( 1 ... 3 ) --> Prime /\ k e. ( 1 ... 3 ) ) -> ( g ` k ) e. Prime )
107 106 ancoms 
 |-  ( ( k e. ( 1 ... 3 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( g ` k ) e. Prime )
108 prmz 
 |-  ( ( g ` k ) e. Prime -> ( g ` k ) e. ZZ )
109 107 108 syl 
 |-  ( ( k e. ( 1 ... 3 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( g ` k ) e. ZZ )
110 109 zcnd 
 |-  ( ( k e. ( 1 ... 3 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( g ` k ) e. CC )
111 105 110 eqeltrd 
 |-  ( ( k e. ( 1 ... 3 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) e. CC )
112 111 ex 
 |-  ( k e. ( 1 ... 3 ) -> ( g : ( 1 ... 3 ) --> Prime -> ( ( g u. { <. 4 , 3 >. } ) ` k ) e. CC ) )
113 112 adantld 
 |-  ( k e. ( 1 ... 3 ) -> ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) e. CC ) )
114 fveq2 
 |-  ( k = 4 -> ( ( g u. { <. 4 , 3 >. } ) ` k ) = ( ( g u. { <. 4 , 3 >. } ) ` 4 ) )
115 31 a1i 
 |-  ( g : ( 1 ... 3 ) --> Prime -> 4 e. ZZ )
116 7 a1i 
 |-  ( g : ( 1 ... 3 ) --> Prime -> 3 e. ZZ )
117 fdm 
 |-  ( g : ( 1 ... 3 ) --> Prime -> dom g = ( 1 ... 3 ) )
118 eleq2 
 |-  ( dom g = ( 1 ... 3 ) -> ( 4 e. dom g <-> 4 e. ( 1 ... 3 ) ) )
119 47 118 mtbiri 
 |-  ( dom g = ( 1 ... 3 ) -> -. 4 e. dom g )
120 117 119 syl 
 |-  ( g : ( 1 ... 3 ) --> Prime -> -. 4 e. dom g )
121 fsnunfv 
 |-  ( ( 4 e. ZZ /\ 3 e. ZZ /\ -. 4 e. dom g ) -> ( ( g u. { <. 4 , 3 >. } ) ` 4 ) = 3 )
122 115 116 120 121 syl3anc 
 |-  ( g : ( 1 ... 3 ) --> Prime -> ( ( g u. { <. 4 , 3 >. } ) ` 4 ) = 3 )
123 122 adantl 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( g u. { <. 4 , 3 >. } ) ` 4 ) = 3 )
124 114 123 sylan9eq 
 |-  ( ( k = 4 /\ ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) = 3 )
125 124 37 eqeltrdi 
 |-  ( ( k = 4 /\ ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) e. CC )
126 125 ex 
 |-  ( k = 4 -> ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) e. CC ) )
127 113 126 jaoi 
 |-  ( ( k e. ( 1 ... 3 ) \/ k = 4 ) -> ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) e. CC ) )
128 127 com12 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( k e. ( 1 ... 3 ) \/ k = 4 ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) e. CC ) )
129 86 128 syl5bi 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( k e. ( 1 ... 4 ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) e. CC ) )
130 129 imp 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ k e. ( 1 ... 4 ) ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) e. CC )
131 81 130 114 fsumm1 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> sum_ k e. ( 1 ... 4 ) ( ( g u. { <. 4 , 3 >. } ) ` k ) = ( sum_ k e. ( 1 ... ( 4 - 1 ) ) ( ( g u. { <. 4 , 3 >. } ) ` k ) + ( ( g u. { <. 4 , 3 >. } ) ` 4 ) ) )
132 131 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) ) -> sum_ k e. ( 1 ... 4 ) ( ( g u. { <. 4 , 3 >. } ) ` k ) = ( sum_ k e. ( 1 ... ( 4 - 1 ) ) ( ( g u. { <. 4 , 3 >. } ) ` k ) + ( ( g u. { <. 4 , 3 >. } ) ` 4 ) ) )
133 42 eqcomi 
 |-  3 = ( 4 - 1 )
134 133 oveq2i 
 |-  ( 1 ... 3 ) = ( 1 ... ( 4 - 1 ) )
135 134 a1i 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( 1 ... 3 ) = ( 1 ... ( 4 - 1 ) ) )
136 102 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ k e. ( 1 ... 3 ) ) -> 4 =/= k )
137 136 104 syl 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ k e. ( 1 ... 3 ) ) -> ( ( g u. { <. 4 , 3 >. } ) ` k ) = ( g ` k ) )
138 137 eqcomd 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ k e. ( 1 ... 3 ) ) -> ( g ` k ) = ( ( g u. { <. 4 , 3 >. } ) ` k ) )
139 135 138 sumeq12dv 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> sum_ k e. ( 1 ... 3 ) ( g ` k ) = sum_ k e. ( 1 ... ( 4 - 1 ) ) ( ( g u. { <. 4 , 3 >. } ) ` k ) )
140 139 eqeq2d 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) <-> ( N - 3 ) = sum_ k e. ( 1 ... ( 4 - 1 ) ) ( ( g u. { <. 4 , 3 >. } ) ` k ) ) )
141 140 biimpa 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) ) -> ( N - 3 ) = sum_ k e. ( 1 ... ( 4 - 1 ) ) ( ( g u. { <. 4 , 3 >. } ) ` k ) )
142 141 eqcomd 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) ) -> sum_ k e. ( 1 ... ( 4 - 1 ) ) ( ( g u. { <. 4 , 3 >. } ) ` k ) = ( N - 3 ) )
143 142 oveq1d 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) ) -> ( sum_ k e. ( 1 ... ( 4 - 1 ) ) ( ( g u. { <. 4 , 3 >. } ) ` k ) + ( ( g u. { <. 4 , 3 >. } ) ` 4 ) ) = ( ( N - 3 ) + ( ( g u. { <. 4 , 3 >. } ) ` 4 ) ) )
144 31 a1i 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> 4 e. ZZ )
145 7 a1i 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> 3 e. ZZ )
146 120 adantl 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> -. 4 e. dom g )
147 144 145 146 121 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( g u. { <. 4 , 3 >. } ) ` 4 ) = 3 )
148 147 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( N - 3 ) + ( ( g u. { <. 4 , 3 >. } ) ` 4 ) ) = ( ( N - 3 ) + 3 ) )
149 eluzelcn 
 |-  ( N e. ( ZZ>= ` 9 ) -> N e. CC )
150 37 a1i 
 |-  ( N e. ( ZZ>= ` 9 ) -> 3 e. CC )
151 149 150 npcand 
 |-  ( N e. ( ZZ>= ` 9 ) -> ( ( N - 3 ) + 3 ) = N )
152 151 adantr 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( N - 3 ) + 3 ) = N )
153 148 152 eqtrd 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( N - 3 ) + ( ( g u. { <. 4 , 3 >. } ) ` 4 ) ) = N )
154 153 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) ) -> ( ( N - 3 ) + ( ( g u. { <. 4 , 3 >. } ) ` 4 ) ) = N )
155 132 143 154 3eqtrrd 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) ) -> N = sum_ k e. ( 1 ... 4 ) ( ( g u. { <. 4 , 3 >. } ) ` k ) )
156 75 80 155 rspcedvd 
 |-  ( ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) /\ ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) )
157 156 ex 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ g : ( 1 ... 3 ) --> Prime ) -> ( ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )
158 157 expcom 
 |-  ( g : ( 1 ... 3 ) --> Prime -> ( N e. ( ZZ>= ` 9 ) -> ( ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) ) )
159 elmapi 
 |-  ( g e. ( Prime ^m ( 1 ... 3 ) ) -> g : ( 1 ... 3 ) --> Prime )
160 158 159 syl11 
 |-  ( N e. ( ZZ>= ` 9 ) -> ( g e. ( Prime ^m ( 1 ... 3 ) ) -> ( ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) ) )
161 160 rexlimdv 
 |-  ( N e. ( ZZ>= ` 9 ) -> ( E. g e. ( Prime ^m ( 1 ... 3 ) ) ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )
162 161 adantr 
 |-  ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> ( E. g e. ( Prime ^m ( 1 ... 3 ) ) ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )
163 162 ad3antlr 
 |-  ( ( ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) /\ o e. GoldbachOddW ) /\ N = ( o + 3 ) ) -> ( E. g e. ( Prime ^m ( 1 ... 3 ) ) ( N - 3 ) = sum_ k e. ( 1 ... 3 ) ( g ` k ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )
164 29 163 mpd 
 |-  ( ( ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) /\ o e. GoldbachOddW ) /\ N = ( o + 3 ) ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) )
165 164 rexlimdva2 
 |-  ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) -> ( E. o e. GoldbachOddW N = ( o + 3 ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )
166 2 165 mpd 
 |-  ( ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) /\ ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) )
167 166 ex 
 |-  ( A. m e. Odd ( 5 < m -> m e. GoldbachOddW ) -> ( ( N e. ( ZZ>= ` 9 ) /\ N e. Even ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )