Metamath Proof Explorer

Theorem bgoldbtbnd

Description: If the binary Goldbach conjecture is valid up to an integer N , and there is a series ("ladder") of primes with a difference of at most N up to an integer M , then the strong ternary Goldbach conjecture is valid up to M , see section 1.2.2 in Helfgott p. 4 with N = 4 x 10^18, taken from OeSilva, and M = 8.875 x 10^30. (Contributed by AV, 1-Aug-2020)

Ref Expression
Hypotheses bgoldbtbnd.m 
|- ( ph -> M e. ( ZZ>= ` ; 1 1 ) )
bgoldbtbnd.n 
|- ( ph -> N e. ( ZZ>= ` ; 1 1 ) )
bgoldbtbnd.b 
|- ( ph -> A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) )
bgoldbtbnd.d 
|- ( ph -> D e. ( ZZ>= ` 3 ) )
bgoldbtbnd.f 
|- ( ph -> F e. ( RePart ` D ) )
bgoldbtbnd.i 
|- ( ph -> A. i e. ( 0 ..^ D ) ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) )
bgoldbtbnd.0 
|- ( ph -> ( F ` 0 ) = 7 )
bgoldbtbnd.1 
|- ( ph -> ( F ` 1 ) = ; 1 3 )
bgoldbtbnd.l 
|- ( ph -> M < ( F ` D ) )
bgoldbtbnd.r 
|- ( ph -> ( F ` D ) e. RR )
Assertion bgoldbtbnd 
|- ( ph -> A. n e. Odd ( ( 7 < n /\ n < M ) -> n e. GoldbachOdd ) )

Proof

Step Hyp Ref Expression
1 bgoldbtbnd.m 
 |-  ( ph -> M e. ( ZZ>= ` ; 1 1 ) )
2 bgoldbtbnd.n 
 |-  ( ph -> N e. ( ZZ>= ` ; 1 1 ) )
3 bgoldbtbnd.b 
 |-  ( ph -> A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) )
4 bgoldbtbnd.d 
 |-  ( ph -> D e. ( ZZ>= ` 3 ) )
5 bgoldbtbnd.f 
 |-  ( ph -> F e. ( RePart ` D ) )
6 bgoldbtbnd.i 
 |-  ( ph -> A. i e. ( 0 ..^ D ) ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) )
7 bgoldbtbnd.0 
 |-  ( ph -> ( F ` 0 ) = 7 )
8 bgoldbtbnd.1 
 |-  ( ph -> ( F ` 1 ) = ; 1 3 )
9 bgoldbtbnd.l 
 |-  ( ph -> M < ( F ` D ) )
10 bgoldbtbnd.r 
 |-  ( ph -> ( F ` D ) e. RR )
11 simprl 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. Odd )
12 eluzge3nn 
 |-  ( D e. ( ZZ>= ` 3 ) -> D e. NN )
13 4 12 syl 
 |-  ( ph -> D e. NN )
14 iccelpart 
 |-  ( D e. NN -> A. f e. ( RePart ` D ) ( n e. ( ( f ` 0 ) [,) ( f ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) ) )
15 13 14 syl 
 |-  ( ph -> A. f e. ( RePart ` D ) ( n e. ( ( f ` 0 ) [,) ( f ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) ) )
16 fveq1 
 |-  ( f = F -> ( f ` 0 ) = ( F ` 0 ) )
17 fveq1 
 |-  ( f = F -> ( f ` D ) = ( F ` D ) )
18 16 17 oveq12d 
 |-  ( f = F -> ( ( f ` 0 ) [,) ( f ` D ) ) = ( ( F ` 0 ) [,) ( F ` D ) ) )
19 18 eleq2d 
 |-  ( f = F -> ( n e. ( ( f ` 0 ) [,) ( f ` D ) ) <-> n e. ( ( F ` 0 ) [,) ( F ` D ) ) ) )
20 fveq1 
 |-  ( f = F -> ( f ` j ) = ( F ` j ) )
21 fveq1 
 |-  ( f = F -> ( f ` ( j + 1 ) ) = ( F ` ( j + 1 ) ) )
22 20 21 oveq12d 
 |-  ( f = F -> ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) = ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) )
23 22 eleq2d 
 |-  ( f = F -> ( n e. ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) <-> n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) ) )
24 23 rexbidv 
 |-  ( f = F -> ( E. j e. ( 0 ..^ D ) n e. ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) <-> E. j e. ( 0 ..^ D ) n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) ) )
25 19 24 imbi12d 
 |-  ( f = F -> ( ( n e. ( ( f ` 0 ) [,) ( f ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) ) <-> ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) ) ) )
26 25 rspcv 
 |-  ( F e. ( RePart ` D ) -> ( A. f e. ( RePart ` D ) ( n e. ( ( f ` 0 ) [,) ( f ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) ) -> ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) ) ) )
27 5 26 syl 
 |-  ( ph -> ( A. f e. ( RePart ` D ) ( n e. ( ( f ` 0 ) [,) ( f ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) ) -> ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) ) ) )
28 oddz 
 |-  ( n e. Odd -> n e. ZZ )
29 28 zred 
 |-  ( n e. Odd -> n e. RR )
30 29 rexrd 
 |-  ( n e. Odd -> n e. RR* )
31 30 ad2antrl 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. RR* )
32 7re 
 |-  7 e. RR
33 ltle 
 |-  ( ( 7 e. RR /\ n e. RR ) -> ( 7 < n -> 7 <_ n ) )
34 32 29 33 sylancr 
 |-  ( n e. Odd -> ( 7 < n -> 7 <_ n ) )
35 34 com12 
 |-  ( 7 < n -> ( n e. Odd -> 7 <_ n ) )
36 35 adantr 
 |-  ( ( 7 < n /\ n < M ) -> ( n e. Odd -> 7 <_ n ) )
37 36 impcom 
 |-  ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> 7 <_ n )
38 37 adantl 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> 7 <_ n )
39 eluzelre 
 |-  ( M e. ( ZZ>= ` ; 1 1 ) -> M e. RR )
40 39 rexrd 
 |-  ( M e. ( ZZ>= ` ; 1 1 ) -> M e. RR* )
41 1 40 syl 
 |-  ( ph -> M e. RR* )
42 41 adantr 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> M e. RR* )
43 10 rexrd 
 |-  ( ph -> ( F ` D ) e. RR* )
44 43 adantr 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( F ` D ) e. RR* )
45 simprrr 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n < M )
46 9 adantr 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> M < ( F ` D ) )
47 31 42 44 45 46 xrlttrd 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n < ( F ` D ) )
48 7 oveq1d 
 |-  ( ph -> ( ( F ` 0 ) [,) ( F ` D ) ) = ( 7 [,) ( F ` D ) ) )
49 48 eleq2d 
 |-  ( ph -> ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) <-> n e. ( 7 [,) ( F ` D ) ) ) )
50 49 adantr 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) <-> n e. ( 7 [,) ( F ` D ) ) ) )
51 32 rexri 
 |-  7 e. RR*
52 elico1 
 |-  ( ( 7 e. RR* /\ ( F ` D ) e. RR* ) -> ( n e. ( 7 [,) ( F ` D ) ) <-> ( n e. RR* /\ 7 <_ n /\ n < ( F ` D ) ) ) )
53 51 44 52 sylancr 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( 7 [,) ( F ` D ) ) <-> ( n e. RR* /\ 7 <_ n /\ n < ( F ` D ) ) ) )
54 50 53 bitrd 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) <-> ( n e. RR* /\ 7 <_ n /\ n < ( F ` D ) ) ) )
55 31 38 47 54 mpbir3and 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. ( ( F ` 0 ) [,) ( F ` D ) ) )
56 fzo0sn0fzo1 
 |-  ( D e. NN -> ( 0 ..^ D ) = ( { 0 } u. ( 1 ..^ D ) ) )
57 56 eleq2d 
 |-  ( D e. NN -> ( j e. ( 0 ..^ D ) <-> j e. ( { 0 } u. ( 1 ..^ D ) ) ) )
58 elun 
 |-  ( j e. ( { 0 } u. ( 1 ..^ D ) ) <-> ( j e. { 0 } \/ j e. ( 1 ..^ D ) ) )
59 57 58 bitrdi 
 |-  ( D e. NN -> ( j e. ( 0 ..^ D ) <-> ( j e. { 0 } \/ j e. ( 1 ..^ D ) ) ) )
60 13 59 syl 
 |-  ( ph -> ( j e. ( 0 ..^ D ) <-> ( j e. { 0 } \/ j e. ( 1 ..^ D ) ) ) )
61 60 adantr 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( j e. ( 0 ..^ D ) <-> ( j e. { 0 } \/ j e. ( 1 ..^ D ) ) ) )
62 velsn 
 |-  ( j e. { 0 } <-> j = 0 )
63 fveq2 
 |-  ( j = 0 -> ( F ` j ) = ( F ` 0 ) )
64 fv0p1e1 
 |-  ( j = 0 -> ( F ` ( j + 1 ) ) = ( F ` 1 ) )
65 63 64 oveq12d 
 |-  ( j = 0 -> ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) = ( ( F ` 0 ) [,) ( F ` 1 ) ) )
66 7 8 oveq12d 
 |-  ( ph -> ( ( F ` 0 ) [,) ( F ` 1 ) ) = ( 7 [,) ; 1 3 ) )
67 66 adantr 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( F ` 0 ) [,) ( F ` 1 ) ) = ( 7 [,) ; 1 3 ) )
68 65 67 sylan9eq 
 |-  ( ( j = 0 /\ ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) ) -> ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) = ( 7 [,) ; 1 3 ) )
69 68 eleq2d 
 |-  ( ( j = 0 /\ ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) <-> n e. ( 7 [,) ; 1 3 ) ) )
70 11 adantr 
 |-  ( ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ n e. ( 7 [,) ; 1 3 ) ) -> n e. Odd )
71 simprrl 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> 7 < n )
72 71 adantr 
 |-  ( ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ n e. ( 7 [,) ; 1 3 ) ) -> 7 < n )
73 simpr 
 |-  ( ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ n e. ( 7 [,) ; 1 3 ) ) -> n e. ( 7 [,) ; 1 3 ) )
74 bgoldbtbndlem1 
 |-  ( ( n e. Odd /\ 7 < n /\ n e. ( 7 [,) ; 1 3 ) ) -> n e. GoldbachOdd )
75 70 72 73 74 syl3anc 
 |-  ( ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ n e. ( 7 [,) ; 1 3 ) ) -> n e. GoldbachOdd )
76 isgbo 
 |-  ( n e. GoldbachOdd <-> ( n e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
77 75 76 sylib 
 |-  ( ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ n e. ( 7 [,) ; 1 3 ) ) -> ( n e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
78 77 simprd 
 |-  ( ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ n e. ( 7 [,) ; 1 3 ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) )
79 78 ex 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( 7 [,) ; 1 3 ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
80 79 adantl 
 |-  ( ( j = 0 /\ ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) ) -> ( n e. ( 7 [,) ; 1 3 ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
81 69 80 sylbid 
 |-  ( ( j = 0 /\ ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
82 81 ex 
 |-  ( j = 0 -> ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
83 62 82 sylbi 
 |-  ( j e. { 0 } -> ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
84 fzo0ss1 
 |-  ( 1 ..^ D ) C_ ( 0 ..^ D )
85 84 sseli 
 |-  ( j e. ( 1 ..^ D ) -> j e. ( 0 ..^ D ) )
86 fveq2 
 |-  ( i = j -> ( F ` i ) = ( F ` j ) )
87 86 eleq1d 
 |-  ( i = j -> ( ( F ` i ) e. ( Prime \ { 2 } ) <-> ( F ` j ) e. ( Prime \ { 2 } ) ) )
88 fvoveq1 
 |-  ( i = j -> ( F ` ( i + 1 ) ) = ( F ` ( j + 1 ) ) )
89 88 86 oveq12d 
 |-  ( i = j -> ( ( F ` ( i + 1 ) ) - ( F ` i ) ) = ( ( F ` ( j + 1 ) ) - ( F ` j ) ) )
90 89 breq1d 
 |-  ( i = j -> ( ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) <-> ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) ) )
91 89 breq2d 
 |-  ( i = j -> ( 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) <-> 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) )
92 87 90 91 3anbi123d 
 |-  ( i = j -> ( ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) <-> ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) )
93 92 rspcv 
 |-  ( j e. ( 0 ..^ D ) -> ( A. i e. ( 0 ..^ D ) ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) -> ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) )
94 85 93 syl 
 |-  ( j e. ( 1 ..^ D ) -> ( A. i e. ( 0 ..^ D ) ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) -> ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) )
95 6 94 mpan9 
 |-  ( ( ph /\ j e. ( 1 ..^ D ) ) -> ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) )
96 1 2 3 4 5 6 7 8 9 10 bgoldbtbndlem4 
 |-  ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ n e. Odd ) -> ( ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) /\ ( n - ( F ` j ) ) <_ 4 ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
97 96 ad2ant2r 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) /\ ( n - ( F ` j ) ) <_ 4 ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
98 97 expcomd 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( n - ( F ` j ) ) <_ 4 -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
99 simplll 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ph )
100 simprl 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. Odd )
101 simpllr 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> j e. ( 1 ..^ D ) )
102 eqid 
 |-  ( n - ( F ` j ) ) = ( n - ( F ` j ) )
103 1 2 3 4 5 6 7 8 9 10 102 bgoldbtbndlem3 
 |-  ( ( ph /\ n e. Odd /\ j e. ( 1 ..^ D ) ) -> ( ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) /\ 4 < ( n - ( F ` j ) ) ) -> ( ( n - ( F ` j ) ) e. Even /\ ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) ) )
104 99 100 101 103 syl3anc 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) /\ 4 < ( n - ( F ` j ) ) ) -> ( ( n - ( F ` j ) ) e. Even /\ ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) ) )
105 breq2 
 |-  ( n = m -> ( 4 < n <-> 4 < m ) )
106 breq1 
 |-  ( n = m -> ( n < N <-> m < N ) )
107 105 106 anbi12d 
 |-  ( n = m -> ( ( 4 < n /\ n < N ) <-> ( 4 < m /\ m < N ) ) )
108 eleq1 
 |-  ( n = m -> ( n e. GoldbachEven <-> m e. GoldbachEven ) )
109 107 108 imbi12d 
 |-  ( n = m -> ( ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) <-> ( ( 4 < m /\ m < N ) -> m e. GoldbachEven ) ) )
110 109 cbvralvw 
 |-  ( A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) <-> A. m e. Even ( ( 4 < m /\ m < N ) -> m e. GoldbachEven ) )
111 breq2 
 |-  ( m = ( n - ( F ` j ) ) -> ( 4 < m <-> 4 < ( n - ( F ` j ) ) ) )
112 breq1 
 |-  ( m = ( n - ( F ` j ) ) -> ( m < N <-> ( n - ( F ` j ) ) < N ) )
113 111 112 anbi12d 
 |-  ( m = ( n - ( F ` j ) ) -> ( ( 4 < m /\ m < N ) <-> ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) ) )
114 eleq1 
 |-  ( m = ( n - ( F ` j ) ) -> ( m e. GoldbachEven <-> ( n - ( F ` j ) ) e. GoldbachEven ) )
115 113 114 imbi12d 
 |-  ( m = ( n - ( F ` j ) ) -> ( ( ( 4 < m /\ m < N ) -> m e. GoldbachEven ) <-> ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) -> ( n - ( F ` j ) ) e. GoldbachEven ) ) )
116 115 rspcv 
 |-  ( ( n - ( F ` j ) ) e. Even -> ( A. m e. Even ( ( 4 < m /\ m < N ) -> m e. GoldbachEven ) -> ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) -> ( n - ( F ` j ) ) e. GoldbachEven ) ) )
117 110 116 syl5bi 
 |-  ( ( n - ( F ` j ) ) e. Even -> ( A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) -> ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) -> ( n - ( F ` j ) ) e. GoldbachEven ) ) )
118 pm3.35 
 |-  ( ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) /\ ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) -> ( n - ( F ` j ) ) e. GoldbachEven ) ) -> ( n - ( F ` j ) ) e. GoldbachEven )
119 isgbe 
 |-  ( ( n - ( F ` j ) ) e. GoldbachEven <-> ( ( n - ( F ` j ) ) e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) ) )
120 eldifi 
 |-  ( ( F ` j ) e. ( Prime \ { 2 } ) -> ( F ` j ) e. Prime )
121 120 3ad2ant1 
 |-  ( ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) -> ( F ` j ) e. Prime )
122 121 adantl 
 |-  ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( F ` j ) e. Prime )
123 122 ad5antlr 
 |-  ( ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) ) -> ( F ` j ) e. Prime )
124 eleq1 
 |-  ( r = ( F ` j ) -> ( r e. Odd <-> ( F ` j ) e. Odd ) )
125 124 3anbi3d 
 |-  ( r = ( F ` j ) -> ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) <-> ( p e. Odd /\ q e. Odd /\ ( F ` j ) e. Odd ) ) )
126 oveq2 
 |-  ( r = ( F ` j ) -> ( ( p + q ) + r ) = ( ( p + q ) + ( F ` j ) ) )
127 126 eqeq2d 
 |-  ( r = ( F ` j ) -> ( n = ( ( p + q ) + r ) <-> n = ( ( p + q ) + ( F ` j ) ) ) )
128 125 127 anbi12d 
 |-  ( r = ( F ` j ) -> ( ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) <-> ( ( p e. Odd /\ q e. Odd /\ ( F ` j ) e. Odd ) /\ n = ( ( p + q ) + ( F ` j ) ) ) ) )
129 128 adantl 
 |-  ( ( ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) ) /\ r = ( F ` j ) ) -> ( ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) <-> ( ( p e. Odd /\ q e. Odd /\ ( F ` j ) e. Odd ) /\ n = ( ( p + q ) + ( F ` j ) ) ) ) )
130 oddprmALTV 
 |-  ( ( F ` j ) e. ( Prime \ { 2 } ) -> ( F ` j ) e. Odd )
131 130 3ad2ant1 
 |-  ( ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) -> ( F ` j ) e. Odd )
132 131 adantl 
 |-  ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( F ` j ) e. Odd )
133 132 ad4antlr 
 |-  ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) -> ( F ` j ) e. Odd )
134 3simpa 
 |-  ( ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) -> ( p e. Odd /\ q e. Odd ) )
135 133 134 anim12ci 
 |-  ( ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) ) -> ( ( p e. Odd /\ q e. Odd ) /\ ( F ` j ) e. Odd ) )
136 df-3an 
 |-  ( ( p e. Odd /\ q e. Odd /\ ( F ` j ) e. Odd ) <-> ( ( p e. Odd /\ q e. Odd ) /\ ( F ` j ) e. Odd ) )
137 135 136 sylibr 
 |-  ( ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) ) -> ( p e. Odd /\ q e. Odd /\ ( F ` j ) e. Odd ) )
138 28 zcnd 
 |-  ( n e. Odd -> n e. CC )
139 138 ad2antrl 
 |-  ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. CC )
140 prmz 
 |-  ( ( F ` j ) e. Prime -> ( F ` j ) e. ZZ )
141 140 zcnd 
 |-  ( ( F ` j ) e. Prime -> ( F ` j ) e. CC )
142 120 141 syl 
 |-  ( ( F ` j ) e. ( Prime \ { 2 } ) -> ( F ` j ) e. CC )
143 142 3ad2ant1 
 |-  ( ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) -> ( F ` j ) e. CC )
144 143 adantl 
 |-  ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( F ` j ) e. CC )
145 144 ad2antlr 
 |-  ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( F ` j ) e. CC )
146 139 145 npcand 
 |-  ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( n - ( F ` j ) ) + ( F ` j ) ) = n )
147 146 adantr 
 |-  ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) -> ( ( n - ( F ` j ) ) + ( F ` j ) ) = n )
148 147 ad2antrl 
 |-  ( ( ( p e. Odd /\ q e. Odd ) /\ ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) ) -> ( ( n - ( F ` j ) ) + ( F ` j ) ) = n )
149 oveq1 
 |-  ( ( n - ( F ` j ) ) = ( p + q ) -> ( ( n - ( F ` j ) ) + ( F ` j ) ) = ( ( p + q ) + ( F ` j ) ) )
150 148 149 sylan9req 
 |-  ( ( ( ( p e. Odd /\ q e. Odd ) /\ ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) ) /\ ( n - ( F ` j ) ) = ( p + q ) ) -> n = ( ( p + q ) + ( F ` j ) ) )
151 150 exp31 
 |-  ( ( p e. Odd /\ q e. Odd ) -> ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( n - ( F ` j ) ) = ( p + q ) -> n = ( ( p + q ) + ( F ` j ) ) ) ) )
152 151 com23 
 |-  ( ( p e. Odd /\ q e. Odd ) -> ( ( n - ( F ` j ) ) = ( p + q ) -> ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) -> n = ( ( p + q ) + ( F ` j ) ) ) ) )
153 152 3impia 
 |-  ( ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) -> ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) -> n = ( ( p + q ) + ( F ` j ) ) ) )
154 153 impcom 
 |-  ( ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) ) -> n = ( ( p + q ) + ( F ` j ) ) )
155 137 154 jca 
 |-  ( ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) ) -> ( ( p e. Odd /\ q e. Odd /\ ( F ` j ) e. Odd ) /\ n = ( ( p + q ) + ( F ` j ) ) ) )
156 123 129 155 rspcedvd 
 |-  ( ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) /\ ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) ) -> E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) )
157 156 ex 
 |-  ( ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) /\ q e. Prime ) -> ( ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) -> E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
158 157 reximdva 
 |-  ( ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ p e. Prime ) -> ( E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) -> E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
159 158 reximdva 
 |-  ( ( ( ( ( n - ( F ` j ) ) e. Even /\ ph ) /\ ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
160 159 exp41 
 |-  ( ( n - ( F ` j ) ) e. Even -> ( ph -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) )
161 160 com25 
 |-  ( ( n - ( F ` j ) ) e. Even -> ( E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) )
162 161 imp 
 |-  ( ( ( n - ( F ` j ) ) e. Even /\ E. p e. Prime E. q e. Prime ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) ) -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) )
163 119 162 sylbi 
 |-  ( ( n - ( F ` j ) ) e. GoldbachEven -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) )
164 163 a1d 
 |-  ( ( n - ( F ` j ) ) e. GoldbachEven -> ( ( n - ( F ` j ) ) e. Even -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) )
165 118 164 syl 
 |-  ( ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) /\ ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) -> ( n - ( F ` j ) ) e. GoldbachEven ) ) -> ( ( n - ( F ` j ) ) e. Even -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) )
166 165 ex 
 |-  ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) -> ( ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) -> ( n - ( F ` j ) ) e. GoldbachEven ) -> ( ( n - ( F ` j ) ) e. Even -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) ) )
167 166 ancoms 
 |-  ( ( ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) -> ( ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) -> ( n - ( F ` j ) ) e. GoldbachEven ) -> ( ( n - ( F ` j ) ) e. Even -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) ) )
168 167 com13 
 |-  ( ( n - ( F ` j ) ) e. Even -> ( ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) -> ( n - ( F ` j ) ) e. GoldbachEven ) -> ( ( ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) ) )
169 117 168 syld 
 |-  ( ( n - ( F ` j ) ) e. Even -> ( A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) -> ( ( ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) ) )
170 169 com23 
 |-  ( ( n - ( F ` j ) ) e. Even -> ( ( ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) -> ( A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) ) )
171 170 3impib 
 |-  ( ( ( n - ( F ` j ) ) e. Even /\ ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) -> ( A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ph -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) )
172 171 com15 
 |-  ( ph -> ( A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ( ( n - ( F ` j ) ) e. Even /\ ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) ) )
173 3 172 mpd 
 |-  ( ph -> ( ( j e. ( 1 ..^ D ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ( ( n - ( F ` j ) ) e. Even /\ ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) )
174 173 impl 
 |-  ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ( ( n - ( F ` j ) ) e. Even /\ ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
175 174 imp 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( ( n - ( F ` j ) ) e. Even /\ ( n - ( F ` j ) ) < N /\ 4 < ( n - ( F ` j ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
176 104 175 syld 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) /\ 4 < ( n - ( F ` j ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
177 176 expcomd 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( 4 < ( n - ( F ` j ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
178 29 ad2antrl 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. RR )
179 140 zred 
 |-  ( ( F ` j ) e. Prime -> ( F ` j ) e. RR )
180 120 179 syl 
 |-  ( ( F ` j ) e. ( Prime \ { 2 } ) -> ( F ` j ) e. RR )
181 180 3ad2ant1 
 |-  ( ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) -> ( F ` j ) e. RR )
182 181 ad2antlr 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( F ` j ) e. RR )
183 178 182 resubcld 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n - ( F ` j ) ) e. RR )
184 4re 
 |-  4 e. RR
185 lelttric 
 |-  ( ( ( n - ( F ` j ) ) e. RR /\ 4 e. RR ) -> ( ( n - ( F ` j ) ) <_ 4 \/ 4 < ( n - ( F ` j ) ) ) )
186 183 184 185 sylancl 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( n - ( F ` j ) ) <_ 4 \/ 4 < ( n - ( F ` j ) ) ) )
187 98 177 186 mpjaod 
 |-  ( ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
188 187 ex 
 |-  ( ( ( ph /\ j e. ( 1 ..^ D ) ) /\ ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
189 95 188 mpdan 
 |-  ( ( ph /\ j e. ( 1 ..^ D ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
190 189 expcom 
 |-  ( j e. ( 1 ..^ D ) -> ( ph -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) ) )
191 190 impd 
 |-  ( j e. ( 1 ..^ D ) -> ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
192 83 191 jaoi 
 |-  ( ( j e. { 0 } \/ j e. ( 1 ..^ D ) ) -> ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
193 192 com12 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( j e. { 0 } \/ j e. ( 1 ..^ D ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
194 61 193 sylbid 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( j e. ( 0 ..^ D ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
195 194 rexlimdv 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( E. j e. ( 0 ..^ D ) n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
196 55 195 embantd 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
197 196 ex 
 |-  ( ph -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> ( ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
198 197 com23 
 |-  ( ph -> ( ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
199 27 198 syld 
 |-  ( ph -> ( A. f e. ( RePart ` D ) ( n e. ( ( f ` 0 ) [,) ( f ` D ) ) -> E. j e. ( 0 ..^ D ) n e. ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) ) -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) ) )
200 15 199 mpd 
 |-  ( ph -> ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
201 200 imp 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) )
202 11 201 jca 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. Odd /\ E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ n = ( ( p + q ) + r ) ) ) )
203 202 76 sylibr 
 |-  ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. GoldbachOdd )
204 203 exp32 
 |-  ( ph -> ( n e. Odd -> ( ( 7 < n /\ n < M ) -> n e. GoldbachOdd ) ) )
205 204 ralrimiv 
 |-  ( ph -> A. n e. Odd ( ( 7 < n /\ n < M ) -> n e. GoldbachOdd ) )