Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bgoldbtbnd Structured version   Visualization version   Unicode version
Theorem bgoldbtbnd 41697
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.)
Hypotheses
Ref Expression
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
Ref Expression
bgoldbtbnd |- ( ph -> A. n e. Odd ( ( 7 < n /\ n < M ) -> n e. GoldbachOdd ) )
Distinct variable groups:   D, i   i, F   i, N, n   ph, n
Allowed substitution hints:   ph( i)   D( n)   F( n)   M( i, n)
Proof of Theorem bgoldbtbnd
Dummy variables p q r m f j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprl 794 . . . . 5 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. Odd )
2 bgoldbtbnd.d . . . . . . . . 9 |- ( ph -> D e. ( ZZ>= ` 3 ) )
3 eluzge3nn 11730 . . . . . . . . 9 |- ( D e. ( ZZ>= ` 3 ) -> D e. NN )
42, 3syl 17 . . . . . . . 8 |- ( ph -> D e. NN )
5 iccelpart 41369 . . . . . . . 8 |- ( 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 ) ) ) ) )
64, 5syl 17 . . . . . . 7 |- ( ph -> A. f e. (RePart ` D ) ( n e. ( ( f ` 0 ) [,) ( f ` D ) ) -> E. j e. ( 0..^ D ) n e. ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) ) )
7 bgoldbtbnd.f . . . . . . . . 9 |- ( ph -> F e. (RePart ` D ) )
8 fveq1 6190 . . . . . . . . . . . . 13 |- ( f = F -> ( f ` 0 ) = ( F ` 0 ) )
9 fveq1 6190 . . . . . . . . . . . . 13 |- ( f = F -> ( f ` D ) = ( F ` D ) )
108, 9oveq12d 6668 . . . . . . . . . . . 12 |- ( f = F -> ( ( f ` 0 ) [,) ( f ` D ) ) = ( ( F ` 0 ) [,) ( F ` D ) ) )
1110eleq2d 2687 . . . . . . . . . . 11 |- ( f = F -> ( n e. ( ( f ` 0 ) [,) ( f ` D ) ) <-> n e. ( ( F ` 0 ) [,) ( F ` D ) ) ) )
12 fveq1 6190 . . . . . . . . . . . . . 14 |- ( f = F -> ( f ` j ) = ( F ` j ) )
13 fveq1 6190 . . . . . . . . . . . . . 14 |- ( f = F -> ( f ` ( j + 1 ) ) = ( F ` ( j + 1 ) ) )
1412, 13oveq12d 6668 . . . . . . . . . . . . 13 |- ( f = F -> ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) = ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) )
1514eleq2d 2687 . . . . . . . . . . . 12 |- ( f = F -> ( n e. ( ( f ` j ) [,) ( f ` ( j + 1 ) ) ) <-> n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) ) )
1615rexbidv 3052 . . . . . . . . . . 11 |- ( 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 ) ) ) ) )
1711, 16imbi12d 334 . . . . . . . . . 10 |- ( 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 ) ) ) ) ) )
1817rspcv 3305 . . . . . . . . 9 |- ( 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 ) ) ) ) ) )
197, 18syl 17 . . . . . . . 8 |- ( 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 ) ) ) ) ) )
20 oddz 41544 . . . . . . . . . . . . . . 15 |- ( n e. Odd -> n e. ZZ )
2120zred 11482 . . . . . . . . . . . . . 14 |- ( n e. Odd -> n e. RR )
2221rexrd 10089 . . . . . . . . . . . . 13 |- ( n e. Odd -> n e. RR* )
2322ad2antrl 764 . . . . . . . . . . . 12 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. RR* )
24 7re 11103 . . . . . . . . . . . . . . . . 17 |- 7 e. RR
25 ltle 10126 . . . . . . . . . . . . . . . . 17 |- ( ( 7 e. RR /\ n e. RR ) -> ( 7 < n -> 7 <_ n ) )
2624, 21, 25sylancr 695 . . . . . . . . . . . . . . . 16 |- ( n e. Odd -> ( 7 < n -> 7 <_ n ) )
2726com12 32 . . . . . . . . . . . . . . 15 |- ( 7 < n -> ( n e. Odd -> 7 <_ n ) )
2827adantr 481 . . . . . . . . . . . . . 14 |- ( ( 7 < n /\ n < M ) -> ( n e. Odd -> 7 <_ n ) )
2928impcom 446 . . . . . . . . . . . . 13 |- ( ( n e. Odd /\ ( 7 < n /\ n < M ) ) -> 7 <_ n )
3029adantl 482 . . . . . . . . . . . 12 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> 7 <_ n )
31 bgoldbtbnd.m . . . . . . . . . . . . . . 15 |- ( ph -> M e. ( ZZ>= ` ; 1 1 ) )
32 eluzelre 11698 . . . . . . . . . . . . . . . 16 |- ( M e. ( ZZ>= ` ; 1 1 ) -> M e. RR )
3332rexrd 10089 . . . . . . . . . . . . . . 15 |- ( M e. ( ZZ>= ` ; 1 1 ) -> M e. RR* )
3431, 33syl 17 . . . . . . . . . . . . . 14 |- ( ph -> M e. RR* )
3534adantr 481 . . . . . . . . . . . . 13 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> M e. RR* )
36 bgoldbtbnd.r . . . . . . . . . . . . . . 15 |- ( ph -> ( F ` D ) e. RR )
3736rexrd 10089 . . . . . . . . . . . . . 14 |- ( ph -> ( F ` D ) e. RR* )
3837adantr 481 . . . . . . . . . . . . 13 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( F ` D ) e. RR* )
39 simprrr 805 . . . . . . . . . . . . 13 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n < M )
40 bgoldbtbnd.l . . . . . . . . . . . . . 14 |- ( ph -> M < ( F ` D ) )
4140adantr 481 . . . . . . . . . . . . 13 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> M < ( F ` D ) )
4223, 35, 38, 39, 41xrlttrd 11990 . . . . . . . . . . . 12 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n < ( F ` D ) )
43 bgoldbtbnd.0 . . . . . . . . . . . . . . . 16 |- ( ph -> ( F ` 0 ) = 7 )
4443oveq1d 6665 . . . . . . . . . . . . . . 15 |- ( ph -> ( ( F ` 0 ) [,) ( F ` D ) ) = ( 7 [,) ( F ` D ) ) )
4544eleq2d 2687 . . . . . . . . . . . . . 14 |- ( ph -> ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) <-> n e. ( 7 [,) ( F ` D ) ) ) )
4645adantr 481 . . . . . . . . . . . . 13 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) <-> n e. ( 7 [,) ( F ` D ) ) ) )
4724rexri 10097 . . . . . . . . . . . . . 14 |- 7 e. RR*
48 elico1 12218 . . . . . . . . . . . . . 14 |- ( ( 7 e. RR* /\ ( F ` D ) e. RR* ) -> ( n e. ( 7 [,) ( F ` D ) ) <-> ( n e. RR* /\ 7 <_ n /\ n < ( F ` D ) ) ) )
4947, 38, 48sylancr 695 . . . . . . . . . . . . 13 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( 7 [,) ( F ` D ) ) <-> ( n e. RR* /\ 7 <_ n /\ n < ( F ` D ) ) ) )
5046, 49bitrd 268 . . . . . . . . . . . 12 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( n e. ( ( F ` 0 ) [,) ( F ` D ) ) <-> ( n e. RR* /\ 7 <_ n /\ n < ( F ` D ) ) ) )
5123, 30, 42, 50mpbir3and 1245 . . . . . . . . . . 11 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. ( ( F ` 0 ) [,) ( F ` D ) ) )
52 fzo0sn0fzo1 12557 . . . . . . . . . . . . . . . . 17 |- ( D e. NN -> ( 0..^ D ) = ( { 0 } u. ( 1..^ D ) ) )
5352eleq2d 2687 . . . . . . . . . . . . . . . 16 |- ( D e. NN -> ( j e. ( 0..^ D ) <-> j e. ( { 0 } u. ( 1..^ D ) ) ) )
54 elun 3753 . . . . . . . . . . . . . . . 16 |- ( j e. ( { 0 } u. ( 1..^ D ) ) <-> ( j e. { 0 } \/ j e. ( 1..^ D ) ) )
5553, 54syl6bb 276 . . . . . . . . . . . . . . 15 |- ( D e. NN -> ( j e. ( 0..^ D ) <-> ( j e. { 0 } \/ j e. ( 1..^ D ) ) ) )
564, 55syl 17 . . . . . . . . . . . . . 14 |- ( ph -> ( j e. ( 0..^ D ) <-> ( j e. { 0 } \/ j e. ( 1..^ D ) ) ) )
5756adantr 481 . . . . . . . . . . . . 13 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( j e. ( 0..^ D ) <-> ( j e. { 0 } \/ j e. ( 1..^ D ) ) ) )
58 velsn 4193 . . . . . . . . . . . . . . . 16 |- ( j e. { 0 } <-> j = 0 )
59 fveq2 6191 . . . . . . . . . . . . . . . . . . . . 21 |- ( j = 0 -> ( F ` j ) = ( F ` 0 ) )
60 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = 0 -> ( j + 1 ) = ( 0 + 1 ) )
61 0p1e1 11132 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( 0 + 1 ) = 1
6260, 61syl6eq 2672 . . . . . . . . . . . . . . . . . . . . . 22 |- ( j = 0 -> ( j + 1 ) = 1 )
6362fveq2d 6195 . . . . . . . . . . . . . . . . . . . . 21 |- ( j = 0 -> ( F ` ( j + 1 ) ) = ( F ` 1 ) )
6459, 63oveq12d 6668 . . . . . . . . . . . . . . . . . . . 20 |- ( j = 0 -> ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) = ( ( F ` 0 ) [,) ( F ` 1 ) ) )
65 bgoldbtbnd.1 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( F ` 1 ) = ; 1 3 )
6643, 65oveq12d 6668 . . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( F ` 0 ) [,) ( F ` 1 ) ) = ( 7 [,); 1 3 ) )
6766adantr 481 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> ( ( F ` 0 ) [,) ( F ` 1 ) ) = ( 7 [,); 1 3 ) )
6864, 67sylan9eq 2676 . . . . . . . . . . . . . . . . . . 19 |- ( ( j = 0 /\ ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) ) -> ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) = ( 7 [,); 1 3 ) )
6968eleq2d 2687 . . . . . . . . . . . . . . . . . 18 |- ( ( j = 0 /\ ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) ) -> ( n e. ( ( F ` j ) [,) ( F ` ( j + 1 ) ) ) <-> n e. ( 7 [,); 1 3 ) ) )
701adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ n e. ( 7 [,); 1 3 ) ) -> n e. Odd )
71 simprrl 804 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> 7 < n )
7271adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ n e. ( 7 [,); 1 3 ) ) -> 7 < n )
73 simpr 477 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ n e. ( 7 [,); 1 3 ) ) -> n e. ( 7 [,); 1 3 ) )
74 bgoldbtbndlem1 41693 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( n e. Odd /\ 7 < n /\ n e. ( 7 [,); 1 3 ) ) -> n e. GoldbachOdd )
7570, 72, 73, 74syl3anc 1326 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) /\ n e. ( 7 [,); 1 3 ) ) -> n e. GoldbachOdd )
76 isgbo 41641 . . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) ) )
7775, 76sylib 208 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) ) ) )
7877simprd 479 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) )
7978ex 450 . . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) )
8079adantl 482 . . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) )
8169, 80sylbid 230 . . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) ) )
8281ex 450 . . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) )
8358, 82sylbi 207 . . . . . . . . . . . . . . 15 |- ( 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 bgoldbtbnd.i . . . . . . . . . . . . . . . . . . 19 |- ( ph -> A. i e. ( 0..^ D ) ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) )
85 fzo0ss1 12498 . . . . . . . . . . . . . . . . . . . . 21 |- ( 1..^ D ) C_ ( 0..^ D )
8685sseli 3599 . . . . . . . . . . . . . . . . . . . 20 |- ( j e. ( 1..^ D ) -> j e. ( 0..^ D ) )
87 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( i = j -> ( F ` i ) = ( F ` j ) )
8887eleq1d 2686 . . . . . . . . . . . . . . . . . . . . . 22 |- ( i = j -> ( ( F ` i ) e. ( Prime \ { 2 } ) <-> ( F ` j ) e. ( Prime \ { 2 } ) ) )
89 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( i = j -> ( i + 1 ) = ( j + 1 ) )
9089fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( i = j -> ( F ` ( i + 1 ) ) = ( F ` ( j + 1 ) ) )
9190, 87oveq12d 6668 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( i = j -> ( ( F ` ( i + 1 ) ) - ( F ` i ) ) = ( ( F ` ( j + 1 ) ) - ( F ` j ) ) )
9291breq1d 4663 . . . . . . . . . . . . . . . . . . . . . 22 |- ( i = j -> ( ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) <-> ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) ) )
9391breq2d 4665 . . . . . . . . . . . . . . . . . . . . . 22 |- ( i = j -> ( 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) <-> 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) )
9488, 92, 933anbi123d 1399 . . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) ) ) )
9594rspcv 3305 . . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) ) )
9686, 95syl 17 . . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) ) ) )
9784, 96mpan9 486 . . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. ( 1..^ D ) ) -> ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) )
98 bgoldbtbnd.n . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> N e. ( ZZ>= ` ; 1 1 ) )
99 bgoldbtbnd.b . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) )
10031, 98, 99, 2, 7, 84, 43, 65, 40, 36bgoldbtbndlem4 41696 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 ) ) ) )
101100ad2ant2r 783 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 ) ) ) )
102101expcomd 454 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) ) ) ) )
103 simplll 798 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 )
104 simprl 794 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 )
105 simpllr 799 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) )
106 eqid 2622 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n - ( F ` j ) ) = ( n - ( F ` j ) )
10731, 98, 99, 2, 7, 84, 43, 65, 40, 36, 106bgoldbtbndlem3 41695 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) ) ) ) )
108103, 104, 105, 107syl3anc 1326 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) ) ) ) )
109 breq2 4657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( n = m -> ( 4 < n <-> 4 < m ) )
110 breq1 4656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( n = m -> ( n < N <-> m < N ) )
111109, 110anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( n = m -> ( ( 4 < n /\ n < N ) <-> ( 4 < m /\ m < N ) ) )
112 eleq1 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( n = m -> ( n e. GoldbachEven <-> m e. GoldbachEven ) )
113111, 112imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( n = m -> ( ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) <-> ( ( 4 < m /\ m < N ) -> m e. GoldbachEven ) ) )
114113cbvralv 3171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) <-> A. m e. Even ( ( 4 < m /\ m < N ) -> m e. GoldbachEven ) )
115 breq2 4657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( m = ( n - ( F ` j ) ) -> ( 4 < m <-> 4 < ( n - ( F ` j ) ) ) )
116 breq1 4656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( m = ( n - ( F ` j ) ) -> ( m < N <-> ( n - ( F ` j ) ) < N ) )
117115, 116anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( m = ( n - ( F ` j ) ) -> ( ( 4 < m /\ m < N ) <-> ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) ) )
118 eleq1 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( m = ( n - ( F ` j ) ) -> ( m e. GoldbachEven <-> ( n - ( F ` j ) ) e. GoldbachEven ) )
119117, 118imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( m = ( n - ( F ` j ) ) -> ( ( ( 4 < m /\ m < N ) -> m e. GoldbachEven ) <-> ( ( 4 < ( n - ( F ` j ) ) /\ ( n - ( F ` j ) ) < N ) -> ( n - ( F ` j ) ) e. GoldbachEven ) ) )
120119rspcv 3305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( 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 ) ) )
121114, 120syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 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 ) ) )
122 pm3.35 611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( 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 )
123 isgbe 41639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( 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 ) ) ) )
124 eldifi 3732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( F ` j ) e. ( Prime \ { 2 } ) -> ( F ` j ) e. Prime )
1251243ad2ant1 1082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) -> ( F ` j ) e. Prime )
126125adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( 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 )
127126ad5antlr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( ( ( ( ( ( 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 )
128 eleq1 2689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( r = ( F ` j ) -> ( r e. Odd <-> ( F ` j ) e. Odd ) )
1291283anbi3d 1405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( r = ( F ` j ) -> ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) <-> ( p e. Odd /\ q e. Odd /\ ( F ` j ) e. Odd ) ) )
130 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( r = ( F ` j ) -> ( ( p + q ) + r ) = ( ( p + q ) + ( F ` j ) ) )
131130eqeq2d 2632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( r = ( F ` j ) -> ( n = ( ( p + q ) + r ) <-> n = ( ( p + q ) + ( F ` j ) ) ) )
132129, 131anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( 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 ) ) ) ) )
133132adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( ( ( ( ( ( ( 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 ) ) ) ) )
134 oddprmALTV 41598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( F ` j ) e. ( Prime \ { 2 } ) -> ( F ` j ) e. Odd )
1351343ad2ant1 1082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) -> ( F ` j ) e. Odd )
136135adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( 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 )
137136ad4antlr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( ( ( ( ( ( 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 )
138 3simpa 1058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( p e. Odd /\ q e. Odd /\ ( n - ( F ` j ) ) = ( p + q ) ) -> ( p e. Odd /\ q e. Odd ) )
139137, 138anim12ci 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( ( ( ( ( ( ( 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 ) )
140 df-3an 1039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( p e. Odd /\ q e. Odd /\ ( F ` j ) e. Odd ) <-> ( ( p e. Odd /\ q e. Odd ) /\ ( F ` j ) e. Odd ) )
141139, 140sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ( ( ( ( ( ( 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 ) )
14220zcnd 11483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( n e. Odd -> n e. CC )
143142ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( ( ( ( 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 )
144 prmz 15389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- ( ( F ` j ) e. Prime -> ( F ` j ) e. ZZ )
145144zcnd 11483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- ( ( F ` j ) e. Prime -> ( F ` j ) e. CC )
146124, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- ( ( F ` j ) e. ( Prime \ { 2 } ) -> ( F ` j ) e. CC )
1471463ad2ant1 1082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ( ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) -> ( F ` j ) e. CC )
148147adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ( ( 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 )
149148ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ( ( ( ( ( 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 )
150143, 149npcand 10396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ( ( ( ( ( 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 )
151150adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ( ( ( ( ( ( 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 )
152151ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( ( 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 )
153 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ( ( n - ( F ` j ) ) = ( p + q ) -> ( ( n - ( F ` j ) ) + ( F ` j ) ) = ( ( p + q ) + ( F ` j ) ) )
154152, 153sylan9req 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ( ( ( ( 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 ) ) )
155154exp31 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- ( ( 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 ) ) ) ) )
156155com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ( ( 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 ) ) ) ) )
1571563impia 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ( ( 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 ) ) ) )
158157impcom 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ( ( ( ( ( ( ( ( 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 ) ) )
159141, 158jca 554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ( ( ( ( ( ( ( ( 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 ) ) ) )
160127, 133, 159rspcedvd 3317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- ( ( ( ( ( ( ( ( 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 ) ) )
161160ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ( ( ( ( ( ( ( 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 ) ) ) )
162161reximdva 3017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( ( ( ( ( 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 ) ) ) )
163162reximdva 3017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( ( ( ( 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 ) ) ) )
164163exp41 638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( 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 ) ) ) ) ) ) )
165164com25 99 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( 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 ) ) ) ) ) ) )
166165imp 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( 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 ) ) ) ) ) )
167123, 166sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( 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 ) ) ) ) ) )
168167a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( 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 ) ) ) ) ) ) )
169122, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( 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 ) ) ) ) ) ) )
170169ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 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 ) ) ) ) ) ) ) )
171170ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( 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 ) ) ) ) ) ) ) )
172171com13 88 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 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 ) ) ) ) ) ) ) )
173121, 172syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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 ) ) ) ) ) ) ) )
174173com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 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 ) ) ) ) ) ) ) )
1751743impib 1262 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 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 ) ) ) ) ) ) )
176175com15 101 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 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 ) ) ) ) ) ) )
17799, 176mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 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 ) ) ) ) ) )
178177impl 650 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 ) ) ) ) )
179178imp 445 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 ) ) ) )
180108, 179syld 47 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 ) ) ) )
181180expcomd 454 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) ) ) ) )
18221ad2antrl 764 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 )
183144zred 11482 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F ` j ) e. Prime -> ( F ` j ) e. RR )
184124, 183syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F ` j ) e. ( Prime \ { 2 } ) -> ( F ` j ) e. RR )
1851843ad2ant1 1082 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( F ` j ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( j + 1 ) ) - ( F ` j ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( j + 1 ) ) - ( F ` j ) ) ) -> ( F ` j ) e. RR )
186185ad2antlr 763 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 )
187182, 186resubcld 10458 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 )
188 4re 11097 . . . . . . . . . . . . . . . . . . . . 21 |- 4 e. RR
189 lelttric 10144 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( n - ( F ` j ) ) e. RR /\ 4 e. RR ) -> ( ( n - ( F ` j ) ) <_ 4 \/ 4 < ( n - ( F ` j ) ) ) )
190187, 188, 189sylancl 694 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 ) ) ) )
191102, 181, 190mpjaod 396 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 ) ) ) )
192191ex 450 . . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) ) )
19397, 192mpdan 702 . . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) ) ) )
194193expcom 451 . . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) ) )
195194impd 447 . . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) )
19683, 195jaoi 394 . . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) )
197196com12 32 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) ) )
19857, 197sylbid 230 . . . . . . . . . . . 12 |- ( ( 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 ) ) ) ) )
199198rexlimdv 3030 . . . . . . . . . . 11 |- ( ( 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 ) ) ) )
20051, 199embantd 59 . . . . . . . . . 10 |- ( ( 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 ) ) ) )
201200ex 450 . . . . . . . . 9 |- ( 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 ) ) ) ) )
202201com23 86 . . . . . . . 8 |- ( 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 ) ) ) ) )
20319, 202syld 47 . . . . . . 7 |- ( 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 ) ) ) ) )
2046, 203mpd 15 . . . . . 6 |- ( 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 ) ) ) )
205204imp 445 . . . . 5 |- ( ( 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 ) ) )
2061, 205jca 554 . . . 4 |- ( ( 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 ) ) ) )
207206, 76sylibr 224 . . 3 |- ( ( ph /\ ( n e. Odd /\ ( 7 < n /\ n < M ) ) ) -> n e. GoldbachOdd )
208207exp32 631 . 2 |- ( ph -> ( n e. Odd -> ( ( 7 < n /\ n < M ) -> n e. GoldbachOdd ) ) )
209208ralrimiv 2965 1 |- ( ph -> A. n e. Odd ( ( 7 < n /\ n < M ) -> n e. GoldbachOdd ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   \ cdif 3571   u. cun 3572   {csn 4177   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   NNcn 11020   2c2 11070   3c3 11071   4c4 11072   7c7 11075  ;cdc 11493   ZZ>=cuz 11687   [,)cico 12177  ..^cfzo 12465   Primecprime 15385  RePartciccp 41349   Even ceven 41537   Odd codd 41538   GoldbachEven cgbe 41633   GoldbachOdd cgbo 41635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-ico 12181  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-dvds 14984  df-prm 15386  df-iccp 41350  df-even 41539  df-odd 41540  df-gbe 41636  df-gbo 41638
This theorem is referenced by:  tgblthelfgott  41703  tgblthelfgottOLD  41709
  Copyright terms: Public domain W3C validator