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 ) ) )