Metamath Proof Explorer


Theorem nnsum4primesevenALTV

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

Ref Expression
Assertion nnsum4primesevenALTV
|- ( A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) -> ( ( N e. ( ZZ>= ` ; 1 2 ) /\ N e. Even ) -> E. f e. ( Prime ^m ( 1 ... 4 ) ) N = sum_ k e. ( 1 ... 4 ) ( f ` k ) ) )

Proof

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