Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bgoldbtbndlem3 Structured version   Unicode version

Theorem bgoldbtbndlem3 38772
Description: Lemma 3 for bgoldbtbnd 38774. (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 )
bgoldbtbndlem3.s  |-  S  =  ( X  -  ( F `  I )
)
Assertion
Ref Expression
bgoldbtbndlem3  |-  ( (
ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  -> 
( ( X  e.  ( ( F `  I ) [,) ( F `  ( I  +  1 ) ) )  /\  4  < 
S )  ->  ( S  e. Even  /\  S  < 
N  /\  4  <  S ) ) )
Distinct variable groups:    D, i    i, F    i, I    i, N
Allowed substitution hints:    ph( i, n)    D( n)    S( i, n)    F( n)    I( n)    M( i, n)    N( n)    X( i, n)

Proof of Theorem bgoldbtbndlem3
StepHypRef Expression
1 bgoldbtbnd.i . . . . 5  |-  ( ph  ->  A. i  e.  ( 0..^ D ) ( ( F `  i
)  e.  ( Prime  \  { 2 } )  /\  ( ( F `
 ( i  +  1 ) )  -  ( F `  i ) )  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( i  +  1 ) )  -  ( F `  i ) ) ) )
2 fzo0ss1 11955 . . . . . . 7  |-  ( 1..^ D )  C_  (
0..^ D )
32sseli 3460 . . . . . 6  |-  ( I  e.  ( 1..^ D )  ->  I  e.  ( 0..^ D ) )
4 fveq2 5881 . . . . . . . . 9  |-  ( i  =  I  ->  ( F `  i )  =  ( F `  I ) )
54eleq1d 2491 . . . . . . . 8  |-  ( i  =  I  ->  (
( F `  i
)  e.  ( Prime  \  { 2 } )  <-> 
( F `  I
)  e.  ( Prime  \  { 2 } ) ) )
6 oveq1 6312 . . . . . . . . . . 11  |-  ( i  =  I  ->  (
i  +  1 )  =  ( I  + 
1 ) )
76fveq2d 5885 . . . . . . . . . 10  |-  ( i  =  I  ->  ( F `  ( i  +  1 ) )  =  ( F `  ( I  +  1
) ) )
87, 4oveq12d 6323 . . . . . . . . 9  |-  ( i  =  I  ->  (
( F `  (
i  +  1 ) )  -  ( F `
 i ) )  =  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) )
98breq1d 4433 . . . . . . . 8  |-  ( i  =  I  ->  (
( ( F `  ( i  +  1 ) )  -  ( F `  i )
)  <  ( N  -  4 )  <->  ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 ) ) )
108breq2d 4435 . . . . . . . 8  |-  ( i  =  I  ->  (
4  <  ( ( F `  ( i  +  1 ) )  -  ( F `  i ) )  <->  4  <  ( ( F `  (
I  +  1 ) )  -  ( F `
 I ) ) ) )
115, 9, 103anbi123d 1335 . . . . . . 7  |-  ( i  =  I  ->  (
( ( F `  i )  e.  ( Prime  \  { 2 } )  /\  (
( F `  (
i  +  1 ) )  -  ( F `
 i ) )  <  ( N  - 
4 )  /\  4  <  ( ( F `  ( i  +  1 ) )  -  ( F `  i )
) )  <->  ( ( F `  I )  e.  ( Prime  \  { 2 } )  /\  (
( F `  (
I  +  1 ) )  -  ( F `
 I ) )  <  ( N  - 
4 )  /\  4  <  ( ( F `  ( I  +  1
) )  -  ( F `  I )
) ) ) )
1211rspcv 3178 . . . . . 6  |-  ( I  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 `  I
)  e.  ( Prime  \  { 2 } )  /\  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) ) )
133, 12syl 17 . . . . 5  |-  ( I  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 `  I
)  e.  ( Prime  \  { 2 } )  /\  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) ) )
141, 13syl5com 31 . . . 4  |-  ( ph  ->  ( I  e.  ( 1..^ D )  -> 
( ( F `  I )  e.  ( Prime  \  { 2 } )  /\  (
( F `  (
I  +  1 ) )  -  ( F `
 I ) )  <  ( N  - 
4 )  /\  4  <  ( ( F `  ( I  +  1
) )  -  ( F `  I )
) ) ) )
1514a1d 26 . . 3  |-  ( ph  ->  ( X  e. Odd  ->  ( I  e.  ( 1..^ D )  ->  (
( F `  I
)  e.  ( Prime  \  { 2 } )  /\  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) ) ) )
16153imp 1199 . 2  |-  ( (
ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  -> 
( ( F `  I )  e.  ( Prime  \  { 2 } )  /\  (
( F `  (
I  +  1 ) )  -  ( F `
 I ) )  <  ( N  - 
4 )  /\  4  <  ( ( F `  ( I  +  1
) )  -  ( F `  I )
) ) )
17 bgoldbtbndlem3.s . . . . 5  |-  S  =  ( X  -  ( F `  I )
)
18 simp2 1006 . . . . . . . 8  |-  ( (
ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  ->  X  e. Odd  )
19 oddprmALTV 38686 . . . . . . . . 9  |-  ( ( F `  I )  e.  ( Prime  \  {
2 } )  -> 
( F `  I
)  e. Odd  )
20193ad2ant1 1026 . . . . . . . 8  |-  ( ( ( F `  I
)  e.  ( Prime  \  { 2 } )  /\  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) )  ->  ( F `  I )  e. Odd  )
2118, 20anim12i 568 . . . . . . 7  |-  ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `
 I )  e.  ( Prime  \  { 2 } )  /\  (
( F `  (
I  +  1 ) )  -  ( F `
 I ) )  <  ( N  - 
4 )  /\  4  <  ( ( F `  ( I  +  1
) )  -  ( F `  I )
) ) )  -> 
( X  e. Odd  /\  ( F `  I )  e. Odd  ) )
2221adantr 466 . . . . . 6  |-  ( ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `  I )  e.  ( Prime  \  {
2 } )  /\  ( ( F `  ( I  +  1
) )  -  ( F `  I )
)  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) )  /\  ( X  e.  (
( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  /\  4  <  S
) )  ->  ( X  e. Odd  /\  ( F `
 I )  e. Odd 
) )
23 omoeALTV 38684 . . . . . 6  |-  ( ( X  e. Odd  /\  ( F `  I )  e. Odd  )  ->  ( X  -  ( F `  I ) )  e. Even 
)
2422, 23syl 17 . . . . 5  |-  ( ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `  I )  e.  ( Prime  \  {
2 } )  /\  ( ( F `  ( I  +  1
) )  -  ( F `  I )
)  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) )  /\  ( X  e.  (
( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  /\  4  <  S
) )  ->  ( X  -  ( F `  I ) )  e. Even 
)
2517, 24syl5eqel 2511 . . . 4  |-  ( ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `  I )  e.  ( Prime  \  {
2 } )  /\  ( ( F `  ( I  +  1
) )  -  ( F `  I )
)  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) )  /\  ( X  e.  (
( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  /\  4  <  S
) )  ->  S  e. Even  )
26 eldifi 3587 . . . . . . . . . . 11  |-  ( ( F `  I )  e.  ( Prime  \  {
2 } )  -> 
( F `  I
)  e.  Prime )
27 prmz 14625 . . . . . . . . . . . 12  |-  ( ( F `  I )  e.  Prime  ->  ( F `
 I )  e.  ZZ )
2827zred 11047 . . . . . . . . . . 11  |-  ( ( F `  I )  e.  Prime  ->  ( F `
 I )  e.  RR )
29 fzofzp1 12014 . . . . . . . . . . . . . . . 16  |-  ( I  e.  ( 1..^ D )  ->  ( I  +  1 )  e.  ( 1 ... D
) )
30 elfzo2 11930 . . . . . . . . . . . . . . . . . . . . 21  |-  ( I  e.  ( 1..^ D )  <->  ( I  e.  ( ZZ>= `  1 )  /\  D  e.  ZZ  /\  I  <  D ) )
31 1zzd 10975 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( I  e.  ( ZZ>= ` 
1 )  /\  D  e.  ZZ  /\  I  < 
D )  ->  1  e.  ZZ )
32 simp2 1006 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( I  e.  ( ZZ>= ` 
1 )  /\  D  e.  ZZ  /\  I  < 
D )  ->  D  e.  ZZ )
33 eluz2 11172 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( I  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  I  e.  ZZ  /\  1  <_  I ) )
34 zre 10948 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 1  e.  ZZ  ->  1  e.  RR )
35 zre 10948 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( I  e.  ZZ  ->  I  e.  RR )
36 zre 10948 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( D  e.  ZZ  ->  D  e.  RR )
37 leltletr 38584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 1  e.  RR  /\  I  e.  RR  /\  D  e.  RR )  ->  (
( 1  <_  I  /\  I  <  D )  ->  1  <_  D
) )
3834, 35, 36, 37syl3an 1306 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 1  e.  ZZ  /\  I  e.  ZZ  /\  D  e.  ZZ )  ->  (
( 1  <_  I  /\  I  <  D )  ->  1  <_  D
) )
3938exp5o 1224 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 1  e.  ZZ  ->  (
I  e.  ZZ  ->  ( D  e.  ZZ  ->  ( 1  <_  I  ->  ( I  <  D  -> 
1  <_  D )
) ) ) )
4039com34 86 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1  e.  ZZ  ->  (
I  e.  ZZ  ->  ( 1  <_  I  ->  ( D  e.  ZZ  ->  ( I  <  D  -> 
1  <_  D )
) ) ) )
41403imp 1199 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 1  e.  ZZ  /\  I  e.  ZZ  /\  1  <_  I )  ->  ( D  e.  ZZ  ->  ( I  <  D  -> 
1  <_  D )
) )
4233, 41sylbi 198 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( I  e.  ( ZZ>= `  1
)  ->  ( D  e.  ZZ  ->  ( I  <  D  ->  1  <_  D ) ) )
43423imp 1199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( I  e.  ( ZZ>= ` 
1 )  /\  D  e.  ZZ  /\  I  < 
D )  ->  1  <_  D )
44 eluz2 11172 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  D  e.  ZZ  /\  1  <_  D ) )
4531, 32, 43, 44syl3anbrc 1189 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( I  e.  ( ZZ>= ` 
1 )  /\  D  e.  ZZ  /\  I  < 
D )  ->  D  e.  ( ZZ>= `  1 )
)
4630, 45sylbi 198 . . . . . . . . . . . . . . . . . . . 20  |-  ( I  e.  ( 1..^ D )  ->  D  e.  ( ZZ>= `  1 )
)
47 fzisfzounsn 12026 . . . . . . . . . . . . . . . . . . . 20  |-  ( D  e.  ( ZZ>= `  1
)  ->  ( 1 ... D )  =  ( ( 1..^ D )  u.  { D } ) )
4846, 47syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( I  e.  ( 1..^ D )  ->  ( 1 ... D )  =  ( ( 1..^ D )  u.  { D } ) )
4948eleq2d 2492 . . . . . . . . . . . . . . . . . 18  |-  ( I  e.  ( 1..^ D )  ->  ( (
I  +  1 )  e.  ( 1 ... D )  <->  ( I  +  1 )  e.  ( ( 1..^ D )  u.  { D } ) ) )
50 elun 3606 . . . . . . . . . . . . . . . . . 18  |-  ( ( I  +  1 )  e.  ( ( 1..^ D )  u.  { D } )  <->  ( (
I  +  1 )  e.  ( 1..^ D )  \/  ( I  +  1 )  e. 
{ D } ) )
5149, 50syl6bb 264 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  ( 1..^ D )  ->  ( (
I  +  1 )  e.  ( 1 ... D )  <->  ( (
I  +  1 )  e.  ( 1..^ D )  \/  ( I  +  1 )  e. 
{ D } ) ) )
52 bgoldbtbnd.d . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  D  e.  ( ZZ>= ` 
3 ) )
53 eluzge3nn 11207 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D  e.  ( ZZ>= `  3
)  ->  D  e.  NN )
5452, 53syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  D  e.  NN )
5554ad2antrl 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( I  e.  ( 1..^ D )  /\  ( I  +  1
)  e.  ( 1..^ D ) )  /\  ( ph  /\  X  e. Odd 
) )  ->  D  e.  NN )
56 bgoldbtbnd.f . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F  e.  (RePart `  D ) )
5756ad2antrl 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( I  e.  ( 1..^ D )  /\  ( I  +  1
)  e.  ( 1..^ D ) )  /\  ( ph  /\  X  e. Odd 
) )  ->  F  e.  (RePart `  D )
)
58 simplr 760 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( I  e.  ( 1..^ D )  /\  ( I  +  1
)  e.  ( 1..^ D ) )  /\  ( ph  /\  X  e. Odd 
) )  ->  (
I  +  1 )  e.  ( 1..^ D ) )
5955, 57, 58iccpartipre 38605 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( I  e.  ( 1..^ D )  /\  ( I  +  1
)  e.  ( 1..^ D ) )  /\  ( ph  /\  X  e. Odd 
) )  ->  ( F `  ( I  +  1 ) )  e.  RR )
6059exp31 607 . . . . . . . . . . . . . . . . . 18  |-  ( I  e.  ( 1..^ D )  ->  ( (
I  +  1 )  e.  ( 1..^ D )  ->  ( ( ph  /\  X  e. Odd  )  ->  ( F `  (
I  +  1 ) )  e.  RR ) ) )
61 elsni 4023 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( I  +  1 )  e.  { D }  ->  ( I  +  1 )  =  D )
62 bgoldbtbnd.r . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( F `  D
)  e.  RR )
6362ad2antrl 732 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( I  +  1 )  =  D  /\  ( ph  /\  X  e. Odd 
) )  ->  ( F `  D )  e.  RR )
64 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( I  +  1 )  =  D  ->  ( F `  ( I  +  1 ) )  =  ( F `  D ) )
6564eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( I  +  1 )  =  D  ->  (
( F `  (
I  +  1 ) )  e.  RR  <->  ( F `  D )  e.  RR ) )
6665adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( I  +  1 )  =  D  /\  ( ph  /\  X  e. Odd 
) )  ->  (
( F `  (
I  +  1 ) )  e.  RR  <->  ( F `  D )  e.  RR ) )
6763, 66mpbird 235 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( I  +  1 )  =  D  /\  ( ph  /\  X  e. Odd 
) )  ->  ( F `  ( I  +  1 ) )  e.  RR )
6867ex 435 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( I  +  1 )  =  D  ->  (
( ph  /\  X  e. Odd 
)  ->  ( F `  ( I  +  1 ) )  e.  RR ) )
6961, 68syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( I  +  1 )  e.  { D }  ->  ( ( ph  /\  X  e. Odd  )  ->  ( F `  ( I  +  1 ) )  e.  RR ) )
7069a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( I  e.  ( 1..^ D )  ->  ( (
I  +  1 )  e.  { D }  ->  ( ( ph  /\  X  e. Odd  )  ->  ( F `  ( I  +  1 ) )  e.  RR ) ) )
7160, 70jaod 381 . . . . . . . . . . . . . . . . 17  |-  ( I  e.  ( 1..^ D )  ->  ( (
( I  +  1 )  e.  ( 1..^ D )  \/  (
I  +  1 )  e.  { D }
)  ->  ( ( ph  /\  X  e. Odd  )  ->  ( F `  (
I  +  1 ) )  e.  RR ) ) )
7251, 71sylbid 218 . . . . . . . . . . . . . . . 16  |-  ( I  e.  ( 1..^ D )  ->  ( (
I  +  1 )  e.  ( 1 ... D )  ->  (
( ph  /\  X  e. Odd 
)  ->  ( F `  ( I  +  1 ) )  e.  RR ) ) )
7329, 72mpd 15 . . . . . . . . . . . . . . 15  |-  ( I  e.  ( 1..^ D )  ->  ( ( ph  /\  X  e. Odd  )  ->  ( F `  (
I  +  1 ) )  e.  RR ) )
7473com12 32 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  X  e. Odd  )  ->  ( I  e.  ( 1..^ D )  ->  ( F `  ( I  +  1
) )  e.  RR ) )
75743impia 1202 . . . . . . . . . . . . 13  |-  ( (
ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  -> 
( F `  (
I  +  1 ) )  e.  RR )
76 bgoldbtbnd.n . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  ( ZZ>= ` ; 1 1 ) )
77 eluzelre 11176 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= ` ; 1 1 )  ->  N  e.  RR )
7876, 77syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  RR )
79 oddz 38630 . . . . . . . . . . . . . . . 16  |-  ( X  e. Odd  ->  X  e.  ZZ )
8079zred 11047 . . . . . . . . . . . . . . 15  |-  ( X  e. Odd  ->  X  e.  RR )
81 rexr 9693 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  ( I  +  1 ) )  e.  RR  ->  ( F `  ( I  +  1 ) )  e.  RR* )
82 rexr 9693 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  I )  e.  RR  ->  ( F `  I )  e.  RR* )
8381, 82anim12ci 569 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR )  -> 
( ( F `  I )  e.  RR*  /\  ( F `  (
I  +  1 ) )  e.  RR* )
)
8483adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( ( F `  I )  e.  RR*  /\  ( F `  (
I  +  1 ) )  e.  RR* )
)
85 elico1 11686 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( F `  I
)  e.  RR*  /\  ( F `  ( I  +  1 ) )  e.  RR* )  ->  ( X  e.  ( ( F `  I ) [,) ( F `  (
I  +  1 ) ) )  <->  ( X  e.  RR*  /\  ( F `
 I )  <_  X  /\  X  <  ( F `  ( I  +  1 ) ) ) ) )
8684, 85syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( X  e.  ( ( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  <-> 
( X  e.  RR*  /\  ( F `  I
)  <_  X  /\  X  <  ( F `  ( I  +  1
) ) ) ) )
87 simpllr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  X  e.  RR )
88 simplrl 768 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  ( F `  ( I  +  1 ) )  e.  RR )
89 simplrr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  ( F `  I )  e.  RR )
90 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  X  <  ( F `  ( I  +  1 ) ) )
9187, 88, 89, 90ltsub1dd 10232 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  ( X  -  ( F `  I ) )  < 
( ( F `  ( I  +  1
) )  -  ( F `  I )
) )
92 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  ->  X  e.  RR )
93 simprr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( F `  I
)  e.  RR )
9492, 93resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( X  -  ( F `  I )
)  e.  RR )
9594adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  ( X  -  ( F `  I ) )  e.  RR )
9688, 89resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  e.  RR )
97 simplll 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  N  e.  RR )
98 4re 10693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  4  e.  RR
9998a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  4  e.  RR )
10097, 99resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  ( N  -  4 )  e.  RR )
101 lttr 9717 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( X  -  ( F `  I )
)  e.  RR  /\  ( ( F `  ( I  +  1
) )  -  ( F `  I )
)  e.  RR  /\  ( N  -  4
)  e.  RR )  ->  ( ( ( X  -  ( F `
 I ) )  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  /\  ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 ) )  ->  ( X  -  ( F `  I ) )  < 
( N  -  4 ) ) )
10295, 96, 100, 101syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  ( (
( X  -  ( F `  I )
)  <  ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  /\  ( ( F `  ( I  +  1
) )  -  ( F `  I )
)  <  ( N  -  4 ) )  ->  ( X  -  ( F `  I ) )  <  ( N  -  4 ) ) )
10391, 102mpand 679 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  X  <  ( F `  ( I  +  1 ) ) )  ->  ( (
( F `  (
I  +  1 ) )  -  ( F `
 I ) )  <  ( N  - 
4 )  ->  ( X  -  ( F `  I ) )  < 
( N  -  4 ) ) )
104103impr 623 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  ( X  < 
( F `  (
I  +  1 ) )  /\  ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 ) ) )  -> 
( X  -  ( F `  I )
)  <  ( N  -  4 ) )
105 4pos 10712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  <  4
10698a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  e.  RR  /\  X  e.  RR )  ->  4  e.  RR )
107 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( N  e.  RR  /\  X  e.  RR )  ->  N  e.  RR )
108106, 107ltsubposd 10206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( N  e.  RR  /\  X  e.  RR )  ->  ( 0  <  4  <->  ( N  -  4 )  <  N ) )
109105, 108mpbii 214 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( N  e.  RR  /\  X  e.  RR )  ->  ( N  -  4 )  <  N )
110109adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( N  -  4 )  <  N )
111110adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  ( X  < 
( F `  (
I  +  1 ) )  /\  ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 ) ) )  -> 
( N  -  4 )  <  N )
112 simpll 758 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  ->  N  e.  RR )
11398a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
4  e.  RR )
114112, 113resubcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( N  -  4 )  e.  RR )
115 lttr 9717 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( X  -  ( F `  I )
)  e.  RR  /\  ( N  -  4
)  e.  RR  /\  N  e.  RR )  ->  ( ( ( X  -  ( F `  I ) )  < 
( N  -  4 )  /\  ( N  -  4 )  < 
N )  ->  ( X  -  ( F `  I ) )  < 
N ) )
11694, 114, 112, 115syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( ( ( X  -  ( F `  I ) )  < 
( N  -  4 )  /\  ( N  -  4 )  < 
N )  ->  ( X  -  ( F `  I ) )  < 
N ) )
117116adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  ( X  < 
( F `  (
I  +  1 ) )  /\  ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 ) ) )  -> 
( ( ( X  -  ( F `  I ) )  < 
( N  -  4 )  /\  ( N  -  4 )  < 
N )  ->  ( X  -  ( F `  I ) )  < 
N ) )
118104, 111, 117mp2and 683 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  /\  ( X  < 
( F `  (
I  +  1 ) )  /\  ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 ) ) )  -> 
( X  -  ( F `  I )
)  <  N )
119118exp32 608 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( X  <  ( F `  ( I  +  1 ) )  ->  ( ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 )  ->  ( X  -  ( F `  I ) )  < 
N ) ) )
120119com12 32 . . . . . . . . . . . . . . . . . . . . 21  |-  ( X  <  ( F `  ( I  +  1
) )  ->  (
( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  ->  ( ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 )  ->  ( X  -  ( F `  I ) )  < 
N ) ) )
1211203ad2ant3 1028 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( X  e.  RR*  /\  ( F `  I )  <_  X  /\  X  < 
( F `  (
I  +  1 ) ) )  ->  (
( ( N  e.  RR  /\  X  e.  RR )  /\  (
( F `  (
I  +  1 ) )  e.  RR  /\  ( F `  I )  e.  RR ) )  ->  ( ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 )  ->  ( X  -  ( F `  I ) )  < 
N ) ) )
122121com12 32 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( ( X  e. 
RR*  /\  ( F `  I )  <_  X  /\  X  <  ( F `
 ( I  + 
1 ) ) )  ->  ( ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 )  ->  ( X  -  ( F `  I ) )  < 
N ) ) )
12386, 122sylbid 218 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( X  e.  ( ( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  ->  ( ( ( F `  ( I  +  1 ) )  -  ( F `  I ) )  < 
( N  -  4 )  ->  ( X  -  ( F `  I ) )  < 
N ) ) )
124123com23 81 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  RR  /\  X  e.  RR )  /\  ( ( F `
 ( I  + 
1 ) )  e.  RR  /\  ( F `
 I )  e.  RR ) )  -> 
( ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  -> 
( X  e.  ( ( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  ->  ( X  -  ( F `  I ) )  <  N ) ) )
125124exp32 608 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  RR  /\  X  e.  RR )  ->  ( ( F `  ( I  +  1
) )  e.  RR  ->  ( ( F `  I )  e.  RR  ->  ( ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  -> 
( X  e.  ( ( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  ->  ( X  -  ( F `  I ) )  <  N ) ) ) ) )
126125com34 86 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  RR  /\  X  e.  RR )  ->  ( ( F `  ( I  +  1
) )  e.  RR  ->  ( ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  -> 
( ( F `  I )  e.  RR  ->  ( X  e.  ( ( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  ->  ( X  -  ( F `  I ) )  <  N ) ) ) ) )
12778, 80, 126syl2an 479 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  X  e. Odd  )  ->  ( ( F `
 ( I  + 
1 ) )  e.  RR  ->  ( (
( F `  (
I  +  1 ) )  -  ( F `
 I ) )  <  ( N  - 
4 )  ->  (
( F `  I
)  e.  RR  ->  ( X  e.  ( ( F `  I ) [,) ( F `  ( I  +  1
) ) )  -> 
( X  -  ( F `  I )
)  <  N )
) ) ) )
1281273adant3 1025 . . . . . . . . . . . . 13  |-  ( (
ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  -> 
( ( F `  ( I  +  1
) )  e.  RR  ->  ( ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  -> 
( ( F `  I )  e.  RR  ->  ( X  e.  ( ( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  ->  ( X  -  ( F `  I ) )  <  N ) ) ) ) )
12975, 128mpd 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  -> 
( ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  -> 
( ( F `  I )  e.  RR  ->  ( X  e.  ( ( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  ->  ( X  -  ( F `  I ) )  <  N ) ) ) )
130129com13 83 . . . . . . . . . . 11  |-  ( ( F `  I )  e.  RR  ->  (
( ( F `  ( I  +  1
) )  -  ( F `  I )
)  <  ( N  -  4 )  -> 
( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  ->  ( X  e.  ( ( F `  I ) [,) ( F `  ( I  +  1 ) ) )  ->  ( X  -  ( F `  I ) )  < 
N ) ) ) )
13126, 28, 1303syl 18 . . . . . . . . . 10  |-  ( ( F `  I )  e.  ( Prime  \  {
2 } )  -> 
( ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  -> 
( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  ->  ( X  e.  ( ( F `  I ) [,) ( F `  ( I  +  1 ) ) )  ->  ( X  -  ( F `  I ) )  < 
N ) ) ) )
132131imp 430 . . . . . . . . 9  |-  ( ( ( F `  I
)  e.  ( Prime  \  { 2 } )  /\  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 ) )  ->  ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  ->  ( X  e.  ( ( F `  I ) [,) ( F `  ( I  +  1 ) ) )  ->  ( X  -  ( F `  I ) )  < 
N ) ) )
1331323adant3 1025 . . . . . . . 8  |-  ( ( ( F `  I
)  e.  ( Prime  \  { 2 } )  /\  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) )  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) )  ->  (
( ph  /\  X  e. Odd  /\  I  e.  (
1..^ D ) )  ->  ( X  e.  ( ( F `  I ) [,) ( F `  ( I  +  1 ) ) )  ->  ( X  -  ( F `  I ) )  < 
N ) ) )
134133impcom 431 . . . . . . 7  |-  ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `
 I )  e.  ( Prime  \  { 2 } )  /\  (
( F `  (
I  +  1 ) )  -  ( F `
 I ) )  <  ( N  - 
4 )  /\  4  <  ( ( F `  ( I  +  1
) )  -  ( F `  I )
) ) )  -> 
( X  e.  ( ( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  ->  ( X  -  ( F `  I ) )  <  N ) )
135134imp 430 . . . . . 6  |-  ( ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `  I )  e.  ( Prime  \  {
2 } )  /\  ( ( F `  ( I  +  1
) )  -  ( F `  I )
)  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) )  /\  X  e.  ( ( F `  I ) [,) ( F `  (
I  +  1 ) ) ) )  -> 
( X  -  ( F `  I )
)  <  N )
136135adantrr 721 . . . . 5  |-  ( ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `  I )  e.  ( Prime  \  {
2 } )  /\  ( ( F `  ( I  +  1
) )  -  ( F `  I )
)  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) )  /\  ( X  e.  (
( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  /\  4  <  S
) )  ->  ( X  -  ( F `  I ) )  < 
N )
13717, 136syl5eqbr 4457 . . . 4  |-  ( ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `  I )  e.  ( Prime  \  {
2 } )  /\  ( ( F `  ( I  +  1
) )  -  ( F `  I )
)  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) )  /\  ( X  e.  (
( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  /\  4  <  S
) )  ->  S  <  N )
138 simprr 764 . . . 4  |-  ( ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `  I )  e.  ( Prime  \  {
2 } )  /\  ( ( F `  ( I  +  1
) )  -  ( F `  I )
)  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) )  /\  ( X  e.  (
( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  /\  4  <  S
) )  ->  4  <  S )
13925, 137, 1383jca 1185 . . 3  |-  ( ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `  I )  e.  ( Prime  \  {
2 } )  /\  ( ( F `  ( I  +  1
) )  -  ( F `  I )
)  <  ( N  -  4 )  /\  4  <  ( ( F `
 ( I  + 
1 ) )  -  ( F `  I ) ) ) )  /\  ( X  e.  (
( F `  I
) [,) ( F `
 ( I  + 
1 ) ) )  /\  4  <  S
) )  ->  ( S  e. Even  /\  S  < 
N  /\  4  <  S ) )
140139ex 435 . 2  |-  ( ( ( ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  /\  ( ( F `
 I )  e.  ( Prime  \  { 2 } )  /\  (
( F `  (
I  +  1 ) )  -  ( F `
 I ) )  <  ( N  - 
4 )  /\  4  <  ( ( F `  ( I  +  1
) )  -  ( F `  I )
) ) )  -> 
( ( X  e.  ( ( F `  I ) [,) ( F `  ( I  +  1 ) ) )  /\  4  < 
S )  ->  ( S  e. Even  /\  S  < 
N  /\  4  <  S ) ) )
14116, 140mpdan 672 1  |-  ( (
ph  /\  X  e. Odd  /\  I  e.  ( 1..^ D ) )  -> 
( ( X  e.  ( ( F `  I ) [,) ( F `  ( I  +  1 ) ) )  /\  4  < 
S )  ->  ( S  e. Even  /\  S  < 
N  /\  4  <  S ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1872   A.wral 2771    \ cdif 3433    u. cun 3434   {csn 3998   class class class wbr 4423   ` cfv 5601  (class class class)co 6305   RRcr 9545   0cc0 9546   1c1 9547    + caddc 9549   RR*cxr 9681    < clt 9682    <_ cle 9683    - cmin 9867   NNcn 10616   2c2 10666   3c3 10667   4c4 10668   7c7 10671   ZZcz 10944  ;cdc 11058   ZZ>=cuz 11166   [,)cico 11644   ...cfz 11791  ..^cfzo 11922   Primecprime 14621  RePartciccp 38597   Even ceven 38623   Odd codd 38624   GoldbachEven cgbe 38716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-addrcl 9607  ax-mulcl 9608  ax-mulrcl 9609  ax-mulcom 9610  ax-addass 9611  ax-mulass 9612  ax-distr 9613  ax-i2m1 9614  ax-1ne0 9615  ax-1rid 9616  ax-rnegex 9617  ax-rrecex 9618  ax-cnre 9619  ax-pre-lttri 9620  ax-pre-lttrn 9621  ax-pre-ltadd 9622  ax-pre-mulgt0 9623
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-2o 7194  df-oadd 7197  df-er 7374  df-map 7485  df-en 7581  df-dom 7582  df-sdom 7583  df-fin 7584  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-sub 9869  df-neg 9870  df-div 10277  df-nn 10617  df-2 10675  df-3 10676  df-4 10677  df-n0 10877  df-z 10945  df-uz 11167  df-ico 11648  df-fz 11792  df-fzo 11923  df-dvds 14305  df-prm 14622  df-iccp 38598  df-even 38625  df-odd 38626
This theorem is referenced by:  bgoldbtbnd  38774
  Copyright terms: Public domain W3C validator