Metamath Proof Explorer

Theorem bgoldbtbndlem2

Description: Lemma 2 for bgoldbtbnd . (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 ) )
bgoldbtbndlem2.s 
|- S = ( X - ( F ` ( I - 1 ) ) )
Assertion bgoldbtbndlem2 
|- ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) -> ( S e. Even /\ S < N /\ 4 < S ) ) )

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 bgoldbtbndlem2.s 
 |-  S = ( X - ( F ` ( I - 1 ) ) )
11 elfzoelz 
 |-  ( I e. ( 1 ..^ D ) -> I e. ZZ )
12 elfzoel2 
 |-  ( I e. ( 1 ..^ D ) -> D e. ZZ )
13 elfzom1b 
 |-  ( ( I e. ZZ /\ D e. ZZ ) -> ( I e. ( 1 ..^ D ) <-> ( I - 1 ) e. ( 0 ..^ ( D - 1 ) ) ) )
14 fzossrbm1 
 |-  ( D e. ZZ -> ( 0 ..^ ( D - 1 ) ) C_ ( 0 ..^ D ) )
15 14 adantl 
 |-  ( ( I e. ZZ /\ D e. ZZ ) -> ( 0 ..^ ( D - 1 ) ) C_ ( 0 ..^ D ) )
16 15 sseld 
 |-  ( ( I e. ZZ /\ D e. ZZ ) -> ( ( I - 1 ) e. ( 0 ..^ ( D - 1 ) ) -> ( I - 1 ) e. ( 0 ..^ D ) ) )
17 13 16 sylbid 
 |-  ( ( I e. ZZ /\ D e. ZZ ) -> ( I e. ( 1 ..^ D ) -> ( I - 1 ) e. ( 0 ..^ D ) ) )
18 17 com12 
 |-  ( I e. ( 1 ..^ D ) -> ( ( I e. ZZ /\ D e. ZZ ) -> ( I - 1 ) e. ( 0 ..^ D ) ) )
19 11 12 18 mp2and 
 |-  ( I e. ( 1 ..^ D ) -> ( I - 1 ) e. ( 0 ..^ D ) )
20 fveq2 
 |-  ( i = ( I - 1 ) -> ( F ` i ) = ( F ` ( I - 1 ) ) )
21 20 eleq1d 
 |-  ( i = ( I - 1 ) -> ( ( F ` i ) e. ( Prime \ { 2 } ) <-> ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) ) )
22 fvoveq1 
 |-  ( i = ( I - 1 ) -> ( F ` ( i + 1 ) ) = ( F ` ( ( I - 1 ) + 1 ) ) )
23 22 20 oveq12d 
 |-  ( i = ( I - 1 ) -> ( ( F ` ( i + 1 ) ) - ( F ` i ) ) = ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) )
24 23 breq1d 
 |-  ( i = ( I - 1 ) -> ( ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) <-> ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) )
25 23 breq2d 
 |-  ( i = ( I - 1 ) -> ( 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) <-> 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) )
26 21 24 25 3anbi123d 
 |-  ( i = ( I - 1 ) -> ( ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) <-> ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) )
27 26 rspcv 
 |-  ( ( I - 1 ) 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 - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) )
28 19 27 syl 
 |-  ( 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 - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) )
29 6 28 syl5com 
 |-  ( ph -> ( I e. ( 1 ..^ D ) -> ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) )
30 29 a1d 
 |-  ( ph -> ( X e. Odd -> ( I e. ( 1 ..^ D ) -> ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) ) )
31 30 3imp 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) )
32 simp2 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> X e. Odd )
33 oddprmALTV 
 |-  ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) -> ( F ` ( I - 1 ) ) e. Odd )
34 33 3ad2ant1 
 |-  ( ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) -> ( F ` ( I - 1 ) ) e. Odd )
35 32 34 anim12i 
 |-  ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) -> ( X e. Odd /\ ( F ` ( I - 1 ) ) e. Odd ) )
36 35 adantr 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> ( X e. Odd /\ ( F ` ( I - 1 ) ) e. Odd ) )
37 omoeALTV 
 |-  ( ( X e. Odd /\ ( F ` ( I - 1 ) ) e. Odd ) -> ( X - ( F ` ( I - 1 ) ) ) e. Even )
38 36 37 syl 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> ( X - ( F ` ( I - 1 ) ) ) e. Even )
39 10 38 eqeltrid 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> S e. Even )
40 11 zcnd 
 |-  ( I e. ( 1 ..^ D ) -> I e. CC )
41 40 3ad2ant3 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> I e. CC )
42 npcan1 
 |-  ( I e. CC -> ( ( I - 1 ) + 1 ) = I )
43 41 42 syl 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( I - 1 ) + 1 ) = I )
44 43 fveq2d 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( F ` ( ( I - 1 ) + 1 ) ) = ( F ` I ) )
45 44 oveq1d 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) = ( ( F ` I ) - ( F ` ( I - 1 ) ) ) )
46 45 breq1d 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) <-> ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) )
47 46 adantr 
 |-  ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) ) -> ( ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) <-> ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) )
48 eldifi 
 |-  ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) -> ( F ` ( I - 1 ) ) e. Prime )
49 prmz 
 |-  ( ( F ` ( I - 1 ) ) e. Prime -> ( F ` ( I - 1 ) ) e. ZZ )
50 zre 
 |-  ( ( F ` ( I - 1 ) ) e. ZZ -> ( F ` ( I - 1 ) ) e. RR )
51 simp1 
 |-  ( ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) -> ( F ` i ) e. ( Prime \ { 2 } ) )
52 51 ralimi 
 |-  ( A. i e. ( 0 ..^ D ) ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) -> A. i e. ( 0 ..^ D ) ( F ` i ) e. ( Prime \ { 2 } ) )
53 fzo0ss1 
 |-  ( 1 ..^ D ) C_ ( 0 ..^ D )
54 53 sseli 
 |-  ( I e. ( 1 ..^ D ) -> I e. ( 0 ..^ D ) )
55 54 adantl 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> I e. ( 0 ..^ D ) )
56 fveq2 
 |-  ( i = I -> ( F ` i ) = ( F ` I ) )
57 56 eleq1d 
 |-  ( i = I -> ( ( F ` i ) e. ( Prime \ { 2 } ) <-> ( F ` I ) e. ( Prime \ { 2 } ) ) )
58 57 rspcv 
 |-  ( I e. ( 0 ..^ D ) -> ( A. i e. ( 0 ..^ D ) ( F ` i ) e. ( Prime \ { 2 } ) -> ( F ` I ) e. ( Prime \ { 2 } ) ) )
59 55 58 syl 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( A. i e. ( 0 ..^ D ) ( F ` i ) e. ( Prime \ { 2 } ) -> ( F ` I ) e. ( Prime \ { 2 } ) ) )
60 59 ex 
 |-  ( ph -> ( I e. ( 1 ..^ D ) -> ( A. i e. ( 0 ..^ D ) ( F ` i ) e. ( Prime \ { 2 } ) -> ( F ` I ) e. ( Prime \ { 2 } ) ) ) )
61 60 com23 
 |-  ( ph -> ( A. i e. ( 0 ..^ D ) ( F ` i ) e. ( Prime \ { 2 } ) -> ( I e. ( 1 ..^ D ) -> ( F ` I ) e. ( Prime \ { 2 } ) ) ) )
62 61 a1i 
 |-  ( X e. Odd -> ( ph -> ( A. i e. ( 0 ..^ D ) ( F ` i ) e. ( Prime \ { 2 } ) -> ( I e. ( 1 ..^ D ) -> ( F ` I ) e. ( Prime \ { 2 } ) ) ) ) )
63 62 com13 
 |-  ( A. i e. ( 0 ..^ D ) ( F ` i ) e. ( Prime \ { 2 } ) -> ( ph -> ( X e. Odd -> ( I e. ( 1 ..^ D ) -> ( F ` I ) e. ( Prime \ { 2 } ) ) ) ) )
64 52 63 syl 
 |-  ( A. i e. ( 0 ..^ D ) ( ( 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 ) -> ( F ` I ) e. ( Prime \ { 2 } ) ) ) ) )
65 6 64 mpcom 
 |-  ( ph -> ( X e. Odd -> ( I e. ( 1 ..^ D ) -> ( F ` I ) e. ( Prime \ { 2 } ) ) ) )
66 65 3imp 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( F ` I ) e. ( Prime \ { 2 } ) )
67 eldifi 
 |-  ( ( F ` I ) e. ( Prime \ { 2 } ) -> ( F ` I ) e. Prime )
68 prmz 
 |-  ( ( F ` I ) e. Prime -> ( F ` I ) e. ZZ )
69 zre 
 |-  ( ( F ` I ) e. ZZ -> ( F ` I ) e. RR )
70 eluzelz 
 |-  ( N e. ( ZZ>= ` ; 1 1 ) -> N e. ZZ )
71 zre 
 |-  ( N e. ZZ -> N e. RR )
72 oddz 
 |-  ( X e. Odd -> X e. ZZ )
73 72 zred 
 |-  ( X e. Odd -> X e. RR )
74 simplr 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> X e. RR )
75 simprl 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( F ` I ) e. RR )
76 4re 
 |-  4 e. RR
77 76 a1i 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> 4 e. RR )
78 74 75 77 lesubaddd 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( ( X - ( F ` I ) ) <_ 4 <-> X <_ ( 4 + ( F ` I ) ) ) )
79 simpllr 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> X e. RR )
80 simplrr 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> ( F ` ( I - 1 ) ) e. RR )
81 79 80 resubcld 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> ( X - ( F ` ( I - 1 ) ) ) e. RR )
82 76 a1i 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> 4 e. RR )
83 simplrl 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> ( F ` I ) e. RR )
84 82 83 readdcld 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> ( 4 + ( F ` I ) ) e. RR )
85 84 80 resubcld 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> ( ( 4 + ( F ` I ) ) - ( F ` ( I - 1 ) ) ) e. RR )
86 simplll 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> N e. RR )
87 77 75 readdcld 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( 4 + ( F ` I ) ) e. RR )
88 simprr 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( F ` ( I - 1 ) ) e. RR )
89 74 87 88 lesub1d 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( X <_ ( 4 + ( F ` I ) ) <-> ( X - ( F ` ( I - 1 ) ) ) <_ ( ( 4 + ( F ` I ) ) - ( F ` ( I - 1 ) ) ) ) )
90 89 biimpa 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ X <_ ( 4 + ( F ` I ) ) ) -> ( X - ( F ` ( I - 1 ) ) ) <_ ( ( 4 + ( F ` I ) ) - ( F ` ( I - 1 ) ) ) )
91 90 adantrr 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> ( X - ( F ` ( I - 1 ) ) ) <_ ( ( 4 + ( F ` I ) ) - ( F ` ( I - 1 ) ) ) )
92 resubcl 
 |-  ( ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) -> ( ( F ` I ) - ( F ` ( I - 1 ) ) ) e. RR )
93 92 adantl 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( ( F ` I ) - ( F ` ( I - 1 ) ) ) e. RR )
94 simpll 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> N e. RR )
95 ltaddsub2 
 |-  ( ( 4 e. RR /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) e. RR /\ N e. RR ) -> ( ( 4 + ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) < N <-> ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) )
96 95 bicomd 
 |-  ( ( 4 e. RR /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) e. RR /\ N e. RR ) -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) <-> ( 4 + ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) < N ) )
97 77 93 94 96 syl3anc 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) <-> ( 4 + ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) < N ) )
98 97 biimpd 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( 4 + ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) < N ) )
99 98 adantld 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) -> ( 4 + ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) < N ) )
100 99 imp 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> ( 4 + ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) < N )
101 4cn 
 |-  4 e. CC
102 101 a1i 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> 4 e. CC )
103 75 recnd 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( F ` I ) e. CC )
104 recn 
 |-  ( ( F ` ( I - 1 ) ) e. RR -> ( F ` ( I - 1 ) ) e. CC )
105 104 adantl 
 |-  ( ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) -> ( F ` ( I - 1 ) ) e. CC )
106 105 adantl 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( F ` ( I - 1 ) ) e. CC )
107 102 103 106 addsubassd 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( ( 4 + ( F ` I ) ) - ( F ` ( I - 1 ) ) ) = ( 4 + ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) )
108 107 breq1d 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( ( ( 4 + ( F ` I ) ) - ( F ` ( I - 1 ) ) ) < N <-> ( 4 + ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) < N ) )
109 108 adantr 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> ( ( ( 4 + ( F ` I ) ) - ( F ` ( I - 1 ) ) ) < N <-> ( 4 + ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) < N ) )
110 100 109 mpbird 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> ( ( 4 + ( F ` I ) ) - ( F ` ( I - 1 ) ) ) < N )
111 81 85 86 91 110 lelttrd 
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) /\ ( X <_ ( 4 + ( F ` I ) ) /\ ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) ) -> ( X - ( F ` ( I - 1 ) ) ) < N )
112 111 exp32 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( X <_ ( 4 + ( F ` I ) ) -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) )
113 78 112 sylbid 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) )
114 113 com23 
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` I ) e. RR /\ ( F ` ( I - 1 ) ) e. RR ) ) -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) )
115 114 exp32 
 |-  ( ( N e. RR /\ X e. RR ) -> ( ( F ` I ) e. RR -> ( ( F ` ( I - 1 ) ) e. RR -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) ) )
116 73 115 sylan2 
 |-  ( ( N e. RR /\ X e. Odd ) -> ( ( F ` I ) e. RR -> ( ( F ` ( I - 1 ) ) e. RR -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) ) )
117 116 ex 
 |-  ( N e. RR -> ( X e. Odd -> ( ( F ` I ) e. RR -> ( ( F ` ( I - 1 ) ) e. RR -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) ) ) )
118 2 70 71 117 4syl 
 |-  ( ph -> ( X e. Odd -> ( ( F ` I ) e. RR -> ( ( F ` ( I - 1 ) ) e. RR -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) ) ) )
119 118 imp 
 |-  ( ( ph /\ X e. Odd ) -> ( ( F ` I ) e. RR -> ( ( F ` ( I - 1 ) ) e. RR -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) ) )
120 119 3adant3 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( F ` I ) e. RR -> ( ( F ` ( I - 1 ) ) e. RR -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) ) )
121 69 120 syl5com 
 |-  ( ( F ` I ) e. ZZ -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( F ` ( I - 1 ) ) e. RR -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) ) )
122 67 68 121 3syl 
 |-  ( ( F ` I ) e. ( Prime \ { 2 } ) -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( F ` ( I - 1 ) ) e. RR -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) ) )
123 66 122 mpcom 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( F ` ( I - 1 ) ) e. RR -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) )
124 50 123 syl5com 
 |-  ( ( F ` ( I - 1 ) ) e. ZZ -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) )
125 48 49 124 3syl 
 |-  ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) )
126 125 impcom 
 |-  ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) ) -> ( ( ( F ` I ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) )
127 47 126 sylbid 
 |-  ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) ) -> ( ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) )
128 127 expcom 
 |-  ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) )
129 128 com23 
 |-  ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) -> ( ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) ) )
130 129 imp 
 |-  ( ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) ) -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) )
131 130 3adant3 
 |-  ( ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) ) )
132 131 impcom 
 |-  ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) -> ( ( X - ( F ` I ) ) <_ 4 -> ( X - ( F ` ( I - 1 ) ) ) < N ) )
133 132 com12 
 |-  ( ( X - ( F ` I ) ) <_ 4 -> ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) -> ( X - ( F ` ( I - 1 ) ) ) < N ) )
134 133 adantl 
 |-  ( ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) -> ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) -> ( X - ( F ` ( I - 1 ) ) ) < N ) )
135 134 impcom 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> ( X - ( F ` ( I - 1 ) ) ) < N )
136 10 135 eqbrtrid 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> S < N )
137 76 a1i 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> 4 e. RR )
138 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
139 fzoss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ..^ D ) C_ ( 0 ..^ D ) )
140 138 139 mp1i 
 |-  ( ph -> ( 1 ..^ D ) C_ ( 0 ..^ D ) )
141 140 sselda 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> I e. ( 0 ..^ D ) )
142 fvoveq1 
 |-  ( i = I -> ( F ` ( i + 1 ) ) = ( F ` ( I + 1 ) ) )
143 142 56 oveq12d 
 |-  ( i = I -> ( ( F ` ( i + 1 ) ) - ( F ` i ) ) = ( ( F ` ( I + 1 ) ) - ( F ` I ) ) )
144 143 breq1d 
 |-  ( i = I -> ( ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) <-> ( ( F ` ( I + 1 ) ) - ( F ` I ) ) < ( N - 4 ) ) )
145 143 breq2d 
 |-  ( i = I -> ( 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) <-> 4 < ( ( F ` ( I + 1 ) ) - ( F ` I ) ) ) )
146 57 144 145 3anbi123d 
 |-  ( 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 ) ) ) ) )
147 146 rspcv 
 |-  ( 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 ) ) ) ) )
148 141 147 syl 
 |-  ( ( ph /\ 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 ) ) ) ) )
149 68 zred 
 |-  ( ( F ` I ) e. Prime -> ( F ` I ) e. RR )
150 67 149 syl 
 |-  ( ( F ` I ) e. ( Prime \ { 2 } ) -> ( F ` I ) e. RR )
151 150 3ad2ant1 
 |-  ( ( ( F ` I ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( I + 1 ) ) - ( F ` I ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( I + 1 ) ) - ( F ` I ) ) ) -> ( F ` I ) e. RR )
152 148 151 syl6 
 |-  ( ( ph /\ 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. RR ) )
153 152 ex 
 |-  ( ph -> ( 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. RR ) ) )
154 6 153 mpid 
 |-  ( ph -> ( I e. ( 1 ..^ D ) -> ( F ` I ) e. RR ) )
155 154 imp 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( F ` I ) e. RR )
156 155 3adant2 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( F ` I ) e. RR )
157 156 ad2antrr 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> ( F ` I ) e. RR )
158 49 zred 
 |-  ( ( F ` ( I - 1 ) ) e. Prime -> ( F ` ( I - 1 ) ) e. RR )
159 48 158 syl 
 |-  ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) -> ( F ` ( I - 1 ) ) e. RR )
160 159 3ad2ant1 
 |-  ( ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) -> ( F ` ( I - 1 ) ) e. RR )
161 160 ad2antlr 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> ( F ` ( I - 1 ) ) e. RR )
162 157 161 resubcld 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> ( ( F ` I ) - ( F ` ( I - 1 ) ) ) e. RR )
163 73 3ad2ant2 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> X e. RR )
164 resubcl 
 |-  ( ( X e. RR /\ ( F ` ( I - 1 ) ) e. RR ) -> ( X - ( F ` ( I - 1 ) ) ) e. RR )
165 163 160 164 syl2an 
 |-  ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) -> ( X - ( F ` ( I - 1 ) ) ) e. RR )
166 165 adantr 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> ( X - ( F ` ( I - 1 ) ) ) e. RR )
167 40 42 syl 
 |-  ( I e. ( 1 ..^ D ) -> ( ( I - 1 ) + 1 ) = I )
168 167 3ad2ant3 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( I - 1 ) + 1 ) = I )
169 168 fveq2d 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( F ` ( ( I - 1 ) + 1 ) ) = ( F ` I ) )
170 169 oveq1d 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) = ( ( F ` I ) - ( F ` ( I - 1 ) ) ) )
171 170 breq2d 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) <-> 4 < ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) )
172 171 biimpcd 
 |-  ( 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> 4 < ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) )
173 172 3ad2ant3 
 |-  ( ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> 4 < ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) )
174 173 impcom 
 |-  ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) -> 4 < ( ( F ` I ) - ( F ` ( I - 1 ) ) ) )
175 174 adantr 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> 4 < ( ( F ` I ) - ( F ` ( I - 1 ) ) ) )
176 163 ad2antrr 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> X e. RR )
177 eluzge3nn 
 |-  ( D e. ( ZZ>= ` 3 ) -> D e. NN )
178 4 177 syl 
 |-  ( ph -> D e. NN )
179 178 adantr 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> D e. NN )
180 5 adantr 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> F e. ( RePart ` D ) )
181 138 139 mp1i 
 |-  ( D e. ( ZZ>= ` 3 ) -> ( 1 ..^ D ) C_ ( 0 ..^ D ) )
182 fzossfz 
 |-  ( 0 ..^ D ) C_ ( 0 ... D )
183 181 182 sstrdi 
 |-  ( D e. ( ZZ>= ` 3 ) -> ( 1 ..^ D ) C_ ( 0 ... D ) )
184 4 183 syl 
 |-  ( ph -> ( 1 ..^ D ) C_ ( 0 ... D ) )
185 184 sselda 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> I e. ( 0 ... D ) )
186 179 180 185 iccpartxr 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( F ` I ) e. RR* )
187 fzofzp1 
 |-  ( I e. ( 0 ..^ D ) -> ( I + 1 ) e. ( 0 ... D ) )
188 141 187 syl 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( I + 1 ) e. ( 0 ... D ) )
189 179 180 188 iccpartxr 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( F ` ( I + 1 ) ) e. RR* )
190 186 189 jca 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( ( F ` I ) e. RR* /\ ( F ` ( I + 1 ) ) e. RR* ) )
191 190 3adant2 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( F ` I ) e. RR* /\ ( F ` ( I + 1 ) ) e. RR* ) )
192 elico1 
 |-  ( ( ( 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 ) ) ) ) )
193 191 192 syl 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) <-> ( X e. RR* /\ ( F ` I ) <_ X /\ X < ( F ` ( I + 1 ) ) ) ) )
194 simp2 
 |-  ( ( X e. RR* /\ ( F ` I ) <_ X /\ X < ( F ` ( I + 1 ) ) ) -> ( F ` I ) <_ X )
195 193 194 biimtrdi 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) -> ( F ` I ) <_ X ) )
196 195 adantrd 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) -> ( F ` I ) <_ X ) )
197 196 adantr 
 |-  ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) -> ( ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) -> ( F ` I ) <_ X ) )
198 197 imp 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> ( F ` I ) <_ X )
199 157 176 161 198 lesub1dd 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> ( ( F ` I ) - ( F ` ( I - 1 ) ) ) <_ ( X - ( F ` ( I - 1 ) ) ) )
200 137 162 166 175 199 ltletrd 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> 4 < ( X - ( F ` ( I - 1 ) ) ) )
201 200 10 breqtrrdi 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> 4 < S )
202 39 136 201 3jca 
 |-  ( ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) /\ ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) ) -> ( S e. Even /\ S < N /\ 4 < S ) )
203 202 ex 
 |-  ( ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) /\ ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) ) ) -> ( ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) -> ( S e. Even /\ S < N /\ 4 < S ) ) )
204 31 203 mpdan 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) -> ( S e. Even /\ S < N /\ 4 < S ) ) )