Metamath Proof Explorer

Theorem sbgoldbo

Description: If the strong binary Goldbach conjecture is valid, the original formulation of the Goldbach conjecture also holds: Every integer greater than 2 can be expressed as the sum of three "primes" with regarding 1 to be a prime (as Goldbach did). Original text: "Es scheint wenigstens, dass eine jede Zahl, die groesser ist als 2, ein aggregatum trium numerorum primorum sey." (Goldbach, 1742). (Contributed by AV, 25-Dec-2021)

Ref Expression
Hypothesis sbgoldbo.p 
|- P = ( { 1 } u. Prime )
Assertion sbgoldbo 
|- ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. n e. ( ZZ>= ` 3 ) E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )

Proof

Step Hyp Ref Expression
1 sbgoldbo.p 
 |-  P = ( { 1 } u. Prime )
2 nfra1 
 |-  F/ n A. n e. Even ( 4 < n -> n e. GoldbachEven )
3 3z 
 |-  3 e. ZZ
4 6nn 
 |-  6 e. NN
5 4 nnzi 
 |-  6 e. ZZ
6 3re 
 |-  3 e. RR
7 6re 
 |-  6 e. RR
8 3lt6 
 |-  3 < 6
9 6 7 8 ltleii 
 |-  3 <_ 6
10 eluz2 
 |-  ( 6 e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ 6 e. ZZ /\ 3 <_ 6 ) )
11 3 5 9 10 mpbir3an 
 |-  6 e. ( ZZ>= ` 3 )
12 uzsplit 
 |-  ( 6 e. ( ZZ>= ` 3 ) -> ( ZZ>= ` 3 ) = ( ( 3 ... ( 6 - 1 ) ) u. ( ZZ>= ` 6 ) ) )
13 12 eleq2d 
 |-  ( 6 e. ( ZZ>= ` 3 ) -> ( n e. ( ZZ>= ` 3 ) <-> n e. ( ( 3 ... ( 6 - 1 ) ) u. ( ZZ>= ` 6 ) ) ) )
14 11 13 ax-mp 
 |-  ( n e. ( ZZ>= ` 3 ) <-> n e. ( ( 3 ... ( 6 - 1 ) ) u. ( ZZ>= ` 6 ) ) )
15 elun 
 |-  ( n e. ( ( 3 ... ( 6 - 1 ) ) u. ( ZZ>= ` 6 ) ) <-> ( n e. ( 3 ... ( 6 - 1 ) ) \/ n e. ( ZZ>= ` 6 ) ) )
16 6m1e5 
 |-  ( 6 - 1 ) = 5
17 16 oveq2i 
 |-  ( 3 ... ( 6 - 1 ) ) = ( 3 ... 5 )
18 5nn 
 |-  5 e. NN
19 18 nnzi 
 |-  5 e. ZZ
20 5re 
 |-  5 e. RR
21 3lt5 
 |-  3 < 5
22 6 20 21 ltleii 
 |-  3 <_ 5
23 eluz2 
 |-  ( 5 e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ 5 e. ZZ /\ 3 <_ 5 ) )
24 3 19 22 23 mpbir3an 
 |-  5 e. ( ZZ>= ` 3 )
25 fzopredsuc 
 |-  ( 5 e. ( ZZ>= ` 3 ) -> ( 3 ... 5 ) = ( ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) u. { 5 } ) )
26 24 25 ax-mp 
 |-  ( 3 ... 5 ) = ( ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) u. { 5 } )
27 17 26 eqtri 
 |-  ( 3 ... ( 6 - 1 ) ) = ( ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) u. { 5 } )
28 27 eleq2i 
 |-  ( n e. ( 3 ... ( 6 - 1 ) ) <-> n e. ( ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) u. { 5 } ) )
29 elun 
 |-  ( n e. ( ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) u. { 5 } ) <-> ( n e. ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) \/ n e. { 5 } ) )
30 elun 
 |-  ( n e. ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) <-> ( n e. { 3 } \/ n e. ( ( 3 + 1 ) ..^ 5 ) ) )
31 elsni 
 |-  ( n e. { 3 } -> n = 3 )
32 1ex 
 |-  1 e. _V
33 32 snid 
 |-  1 e. { 1 }
34 33 orci 
 |-  ( 1 e. { 1 } \/ 1 e. Prime )
35 elun 
 |-  ( 1 e. ( { 1 } u. Prime ) <-> ( 1 e. { 1 } \/ 1 e. Prime ) )
36 34 35 mpbir 
 |-  1 e. ( { 1 } u. Prime )
37 36 1 eleqtrri 
 |-  1 e. P
38 37 a1i 
 |-  ( n = 3 -> 1 e. P )
39 simpl 
 |-  ( ( n = 3 /\ p = 1 ) -> n = 3 )
40 oveq1 
 |-  ( p = 1 -> ( p + q ) = ( 1 + q ) )
41 40 oveq1d 
 |-  ( p = 1 -> ( ( p + q ) + r ) = ( ( 1 + q ) + r ) )
42 41 adantl 
 |-  ( ( n = 3 /\ p = 1 ) -> ( ( p + q ) + r ) = ( ( 1 + q ) + r ) )
43 39 42 eqeq12d 
 |-  ( ( n = 3 /\ p = 1 ) -> ( n = ( ( p + q ) + r ) <-> 3 = ( ( 1 + q ) + r ) ) )
44 43 2rexbidv 
 |-  ( ( n = 3 /\ p = 1 ) -> ( E. q e. P E. r e. P n = ( ( p + q ) + r ) <-> E. q e. P E. r e. P 3 = ( ( 1 + q ) + r ) ) )
45 oveq2 
 |-  ( q = 1 -> ( 1 + q ) = ( 1 + 1 ) )
46 45 oveq1d 
 |-  ( q = 1 -> ( ( 1 + q ) + r ) = ( ( 1 + 1 ) + r ) )
47 46 eqeq2d 
 |-  ( q = 1 -> ( 3 = ( ( 1 + q ) + r ) <-> 3 = ( ( 1 + 1 ) + r ) ) )
48 47 rexbidv 
 |-  ( q = 1 -> ( E. r e. P 3 = ( ( 1 + q ) + r ) <-> E. r e. P 3 = ( ( 1 + 1 ) + r ) ) )
49 48 adantl 
 |-  ( ( n = 3 /\ q = 1 ) -> ( E. r e. P 3 = ( ( 1 + q ) + r ) <-> E. r e. P 3 = ( ( 1 + 1 ) + r ) ) )
50 df-3 
 |-  3 = ( 2 + 1 )
51 df-2 
 |-  2 = ( 1 + 1 )
52 51 oveq1i 
 |-  ( 2 + 1 ) = ( ( 1 + 1 ) + 1 )
53 50 52 eqtri 
 |-  3 = ( ( 1 + 1 ) + 1 )
54 oveq2 
 |-  ( r = 1 -> ( ( 1 + 1 ) + r ) = ( ( 1 + 1 ) + 1 ) )
55 53 54 eqtr4id 
 |-  ( r = 1 -> 3 = ( ( 1 + 1 ) + r ) )
56 55 adantl 
 |-  ( ( n = 3 /\ r = 1 ) -> 3 = ( ( 1 + 1 ) + r ) )
57 38 56 rspcedeq2vd 
 |-  ( n = 3 -> E. r e. P 3 = ( ( 1 + 1 ) + r ) )
58 38 49 57 rspcedvd 
 |-  ( n = 3 -> E. q e. P E. r e. P 3 = ( ( 1 + q ) + r ) )
59 38 44 58 rspcedvd 
 |-  ( n = 3 -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
60 31 59 syl 
 |-  ( n e. { 3 } -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
61 3p1e4 
 |-  ( 3 + 1 ) = 4
62 df-5 
 |-  5 = ( 4 + 1 )
63 61 62 oveq12i 
 |-  ( ( 3 + 1 ) ..^ 5 ) = ( 4 ..^ ( 4 + 1 ) )
64 4z 
 |-  4 e. ZZ
65 fzval3 
 |-  ( 4 e. ZZ -> ( 4 ... 4 ) = ( 4 ..^ ( 4 + 1 ) ) )
66 64 65 ax-mp 
 |-  ( 4 ... 4 ) = ( 4 ..^ ( 4 + 1 ) )
67 63 66 eqtr4i 
 |-  ( ( 3 + 1 ) ..^ 5 ) = ( 4 ... 4 )
68 67 eleq2i 
 |-  ( n e. ( ( 3 + 1 ) ..^ 5 ) <-> n e. ( 4 ... 4 ) )
69 fzsn 
 |-  ( 4 e. ZZ -> ( 4 ... 4 ) = { 4 } )
70 64 69 ax-mp 
 |-  ( 4 ... 4 ) = { 4 }
71 70 eleq2i 
 |-  ( n e. ( 4 ... 4 ) <-> n e. { 4 } )
72 68 71 bitri 
 |-  ( n e. ( ( 3 + 1 ) ..^ 5 ) <-> n e. { 4 } )
73 elsni 
 |-  ( n e. { 4 } -> n = 4 )
74 2prm 
 |-  2 e. Prime
75 74 olci 
 |-  ( 2 e. { 1 } \/ 2 e. Prime )
76 elun 
 |-  ( 2 e. ( { 1 } u. Prime ) <-> ( 2 e. { 1 } \/ 2 e. Prime ) )
77 75 76 mpbir 
 |-  2 e. ( { 1 } u. Prime )
78 77 1 eleqtrri 
 |-  2 e. P
79 78 a1i 
 |-  ( n = 4 -> 2 e. P )
80 oveq1 
 |-  ( p = 2 -> ( p + q ) = ( 2 + q ) )
81 80 oveq1d 
 |-  ( p = 2 -> ( ( p + q ) + r ) = ( ( 2 + q ) + r ) )
82 81 eqeq2d 
 |-  ( p = 2 -> ( n = ( ( p + q ) + r ) <-> n = ( ( 2 + q ) + r ) ) )
83 82 2rexbidv 
 |-  ( p = 2 -> ( E. q e. P E. r e. P n = ( ( p + q ) + r ) <-> E. q e. P E. r e. P n = ( ( 2 + q ) + r ) ) )
84 83 adantl 
 |-  ( ( n = 4 /\ p = 2 ) -> ( E. q e. P E. r e. P n = ( ( p + q ) + r ) <-> E. q e. P E. r e. P n = ( ( 2 + q ) + r ) ) )
85 37 a1i 
 |-  ( n = 4 -> 1 e. P )
86 oveq2 
 |-  ( q = 1 -> ( 2 + q ) = ( 2 + 1 ) )
87 86 oveq1d 
 |-  ( q = 1 -> ( ( 2 + q ) + r ) = ( ( 2 + 1 ) + r ) )
88 87 eqeq2d 
 |-  ( q = 1 -> ( n = ( ( 2 + q ) + r ) <-> n = ( ( 2 + 1 ) + r ) ) )
89 88 rexbidv 
 |-  ( q = 1 -> ( E. r e. P n = ( ( 2 + q ) + r ) <-> E. r e. P n = ( ( 2 + 1 ) + r ) ) )
90 89 adantl 
 |-  ( ( n = 4 /\ q = 1 ) -> ( E. r e. P n = ( ( 2 + q ) + r ) <-> E. r e. P n = ( ( 2 + 1 ) + r ) ) )
91 simpl 
 |-  ( ( n = 4 /\ r = 1 ) -> n = 4 )
92 df-4 
 |-  4 = ( 3 + 1 )
93 50 oveq1i 
 |-  ( 3 + 1 ) = ( ( 2 + 1 ) + 1 )
94 92 93 eqtri 
 |-  4 = ( ( 2 + 1 ) + 1 )
95 94 a1i 
 |-  ( ( n = 4 /\ r = 1 ) -> 4 = ( ( 2 + 1 ) + 1 ) )
96 oveq2 
 |-  ( r = 1 -> ( ( 2 + 1 ) + r ) = ( ( 2 + 1 ) + 1 ) )
97 96 eqcomd 
 |-  ( r = 1 -> ( ( 2 + 1 ) + 1 ) = ( ( 2 + 1 ) + r ) )
98 97 adantl 
 |-  ( ( n = 4 /\ r = 1 ) -> ( ( 2 + 1 ) + 1 ) = ( ( 2 + 1 ) + r ) )
99 95 98 eqtrd 
 |-  ( ( n = 4 /\ r = 1 ) -> 4 = ( ( 2 + 1 ) + r ) )
100 91 99 eqtrd 
 |-  ( ( n = 4 /\ r = 1 ) -> n = ( ( 2 + 1 ) + r ) )
101 85 100 rspcedeq2vd 
 |-  ( n = 4 -> E. r e. P n = ( ( 2 + 1 ) + r ) )
102 85 90 101 rspcedvd 
 |-  ( n = 4 -> E. q e. P E. r e. P n = ( ( 2 + q ) + r ) )
103 79 84 102 rspcedvd 
 |-  ( n = 4 -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
104 73 103 syl 
 |-  ( n e. { 4 } -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
105 72 104 sylbi 
 |-  ( n e. ( ( 3 + 1 ) ..^ 5 ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
106 60 105 jaoi 
 |-  ( ( n e. { 3 } \/ n e. ( ( 3 + 1 ) ..^ 5 ) ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
107 30 106 sylbi 
 |-  ( n e. ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
108 elsni 
 |-  ( n e. { 5 } -> n = 5 )
109 3prm 
 |-  3 e. Prime
110 109 olci 
 |-  ( 3 e. { 1 } \/ 3 e. Prime )
111 elun 
 |-  ( 3 e. ( { 1 } u. Prime ) <-> ( 3 e. { 1 } \/ 3 e. Prime ) )
112 110 111 mpbir 
 |-  3 e. ( { 1 } u. Prime )
113 112 1 eleqtrri 
 |-  3 e. P
114 113 a1i 
 |-  ( n = 5 -> 3 e. P )
115 oveq1 
 |-  ( p = 3 -> ( p + q ) = ( 3 + q ) )
116 115 oveq1d 
 |-  ( p = 3 -> ( ( p + q ) + r ) = ( ( 3 + q ) + r ) )
117 116 eqeq2d 
 |-  ( p = 3 -> ( n = ( ( p + q ) + r ) <-> n = ( ( 3 + q ) + r ) ) )
118 117 2rexbidv 
 |-  ( p = 3 -> ( E. q e. P E. r e. P n = ( ( p + q ) + r ) <-> E. q e. P E. r e. P n = ( ( 3 + q ) + r ) ) )
119 118 adantl 
 |-  ( ( n = 5 /\ p = 3 ) -> ( E. q e. P E. r e. P n = ( ( p + q ) + r ) <-> E. q e. P E. r e. P n = ( ( 3 + q ) + r ) ) )
120 37 a1i 
 |-  ( n = 5 -> 1 e. P )
121 oveq2 
 |-  ( q = 1 -> ( 3 + q ) = ( 3 + 1 ) )
122 121 oveq1d 
 |-  ( q = 1 -> ( ( 3 + q ) + r ) = ( ( 3 + 1 ) + r ) )
123 122 eqeq2d 
 |-  ( q = 1 -> ( n = ( ( 3 + q ) + r ) <-> n = ( ( 3 + 1 ) + r ) ) )
124 123 rexbidv 
 |-  ( q = 1 -> ( E. r e. P n = ( ( 3 + q ) + r ) <-> E. r e. P n = ( ( 3 + 1 ) + r ) ) )
125 124 adantl 
 |-  ( ( n = 5 /\ q = 1 ) -> ( E. r e. P n = ( ( 3 + q ) + r ) <-> E. r e. P n = ( ( 3 + 1 ) + r ) ) )
126 simpl 
 |-  ( ( n = 5 /\ r = 1 ) -> n = 5 )
127 92 oveq1i 
 |-  ( 4 + 1 ) = ( ( 3 + 1 ) + 1 )
128 62 127 eqtri 
 |-  5 = ( ( 3 + 1 ) + 1 )
129 oveq2 
 |-  ( r = 1 -> ( ( 3 + 1 ) + r ) = ( ( 3 + 1 ) + 1 ) )
130 128 129 eqtr4id 
 |-  ( r = 1 -> 5 = ( ( 3 + 1 ) + r ) )
131 130 adantl 
 |-  ( ( n = 5 /\ r = 1 ) -> 5 = ( ( 3 + 1 ) + r ) )
132 126 131 eqtrd 
 |-  ( ( n = 5 /\ r = 1 ) -> n = ( ( 3 + 1 ) + r ) )
133 120 132 rspcedeq2vd 
 |-  ( n = 5 -> E. r e. P n = ( ( 3 + 1 ) + r ) )
134 120 125 133 rspcedvd 
 |-  ( n = 5 -> E. q e. P E. r e. P n = ( ( 3 + q ) + r ) )
135 114 119 134 rspcedvd 
 |-  ( n = 5 -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
136 108 135 syl 
 |-  ( n e. { 5 } -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
137 107 136 jaoi 
 |-  ( ( n e. ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) \/ n e. { 5 } ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
138 29 137 sylbi 
 |-  ( n e. ( ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) u. { 5 } ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
139 138 a1d 
 |-  ( n e. ( ( { 3 } u. ( ( 3 + 1 ) ..^ 5 ) ) u. { 5 } ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) ) )
140 28 139 sylbi 
 |-  ( n e. ( 3 ... ( 6 - 1 ) ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) ) )
141 sbgoldbm 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) )
142 rspa 
 |-  ( ( A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) /\ n e. ( ZZ>= ` 6 ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) )
143 ssun2 
 |-  Prime C_ ( { 1 } u. Prime )
144 143 1 sseqtrri 
 |-  Prime C_ P
145 rexss 
 |-  ( Prime C_ P -> ( E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) <-> E. p e. P ( p e. Prime /\ E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) ) )
146 144 145 ax-mp 
 |-  ( E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) <-> E. p e. P ( p e. Prime /\ E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) )
147 rexss 
 |-  ( Prime C_ P -> ( E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) <-> E. q e. P ( q e. Prime /\ E. r e. Prime n = ( ( p + q ) + r ) ) ) )
148 144 147 ax-mp 
 |-  ( E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) <-> E. q e. P ( q e. Prime /\ E. r e. Prime n = ( ( p + q ) + r ) ) )
149 rexss 
 |-  ( Prime C_ P -> ( E. r e. Prime n = ( ( p + q ) + r ) <-> E. r e. P ( r e. Prime /\ n = ( ( p + q ) + r ) ) ) )
150 144 149 ax-mp 
 |-  ( E. r e. Prime n = ( ( p + q ) + r ) <-> E. r e. P ( r e. Prime /\ n = ( ( p + q ) + r ) ) )
151 simpr 
 |-  ( ( r e. Prime /\ n = ( ( p + q ) + r ) ) -> n = ( ( p + q ) + r ) )
152 151 reximi 
 |-  ( E. r e. P ( r e. Prime /\ n = ( ( p + q ) + r ) ) -> E. r e. P n = ( ( p + q ) + r ) )
153 150 152 sylbi 
 |-  ( E. r e. Prime n = ( ( p + q ) + r ) -> E. r e. P n = ( ( p + q ) + r ) )
154 153 adantl 
 |-  ( ( q e. Prime /\ E. r e. Prime n = ( ( p + q ) + r ) ) -> E. r e. P n = ( ( p + q ) + r ) )
155 154 reximi 
 |-  ( E. q e. P ( q e. Prime /\ E. r e. Prime n = ( ( p + q ) + r ) ) -> E. q e. P E. r e. P n = ( ( p + q ) + r ) )
156 148 155 sylbi 
 |-  ( E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) -> E. q e. P E. r e. P n = ( ( p + q ) + r ) )
157 156 adantl 
 |-  ( ( p e. Prime /\ E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) -> E. q e. P E. r e. P n = ( ( p + q ) + r ) )
158 157 reximi 
 |-  ( E. p e. P ( p e. Prime /\ E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
159 146 158 sylbi 
 |-  ( E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
160 142 159 syl 
 |-  ( ( A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) /\ n e. ( ZZ>= ` 6 ) ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )
161 160 ex 
 |-  ( A. n e. ( ZZ>= ` 6 ) E. p e. Prime E. q e. Prime E. r e. Prime n = ( ( p + q ) + r ) -> ( n e. ( ZZ>= ` 6 ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) ) )
162 141 161 syl 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( n e. ( ZZ>= ` 6 ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) ) )
163 162 com12 
 |-  ( n e. ( ZZ>= ` 6 ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) ) )
164 140 163 jaoi 
 |-  ( ( n e. ( 3 ... ( 6 - 1 ) ) \/ n e. ( ZZ>= ` 6 ) ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) ) )
165 15 164 sylbi 
 |-  ( n e. ( ( 3 ... ( 6 - 1 ) ) u. ( ZZ>= ` 6 ) ) -> ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) ) )
166 165 com12 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( n e. ( ( 3 ... ( 6 - 1 ) ) u. ( ZZ>= ` 6 ) ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) ) )
167 14 166 biimtrid 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> ( n e. ( ZZ>= ` 3 ) -> E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) ) )
168 2 167 ralrimi 
 |-  ( A. n e. Even ( 4 < n -> n e. GoldbachEven ) -> A. n e. ( ZZ>= ` 3 ) E. p e. P E. q e. P E. r e. P n = ( ( p + q ) + r ) )