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 71 117 syl 
 |-  ( N e. ZZ -> ( 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 2 70 118 3syl 
 |-  ( 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 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 ) ) ) ) )
121 120 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 ) ) ) ) )
122 69 121 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 ) ) ) ) )
123 67 68 122 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 ) ) ) ) )
124 66 123 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 ) ) ) )
125 50 124 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 ) ) ) )
126 48 49 125 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 ) ) ) )
127 126 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 ) ) )
128 47 127 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 ) ) )
129 128 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 ) ) ) )
130 129 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 ) ) ) )
131 130 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 ) ) )
132 131 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 ) ) )
133 132 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 ) )
134 133 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 ) )
135 134 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 ) )
136 135 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 )
137 10 136 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 )
138 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 )
139 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
140 fzoss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ..^ D ) C_ ( 0 ..^ D ) )
141 139 140 mp1i 
 |-  ( ph -> ( 1 ..^ D ) C_ ( 0 ..^ D ) )
142 141 sselda 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> I e. ( 0 ..^ D ) )
143 fvoveq1 
 |-  ( i = I -> ( F ` ( i + 1 ) ) = ( F ` ( I + 1 ) ) )
144 143 56 oveq12d 
 |-  ( i = I -> ( ( F ` ( i + 1 ) ) - ( F ` i ) ) = ( ( F ` ( I + 1 ) ) - ( F ` I ) ) )
145 144 breq1d 
 |-  ( i = I -> ( ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) <-> ( ( F ` ( I + 1 ) ) - ( F ` I ) ) < ( N - 4 ) ) )
146 144 breq2d 
 |-  ( i = I -> ( 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) <-> 4 < ( ( F ` ( I + 1 ) ) - ( F ` I ) ) ) )
147 57 145 146 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 ) ) ) ) )
148 147 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 ) ) ) ) )
149 142 148 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 ) ) ) ) )
150 68 zred 
 |-  ( ( F ` I ) e. Prime -> ( F ` I ) e. RR )
151 67 150 syl 
 |-  ( ( F ` I ) e. ( Prime \ { 2 } ) -> ( F ` I ) e. RR )
152 151 3ad2ant1 
 |-  ( ( ( F ` I ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( I + 1 ) ) - ( F ` I ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( I + 1 ) ) - ( F ` I ) ) ) -> ( F ` I ) e. RR )
153 149 152 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 ) )
154 153 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 ) ) )
155 6 154 mpid 
 |-  ( ph -> ( I e. ( 1 ..^ D ) -> ( F ` I ) e. RR ) )
156 155 imp 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( F ` I ) e. RR )
157 156 3adant2 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( F ` I ) e. RR )
158 157 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 )
159 49 zred 
 |-  ( ( F ` ( I - 1 ) ) e. Prime -> ( F ` ( I - 1 ) ) e. RR )
160 48 159 syl 
 |-  ( ( F ` ( I - 1 ) ) e. ( Prime \ { 2 } ) -> ( F ` ( I - 1 ) ) e. RR )
161 160 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 )
162 161 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 )
163 158 162 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 )
164 73 3ad2ant2 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> X e. RR )
165 resubcl 
 |-  ( ( X e. RR /\ ( F ` ( I - 1 ) ) e. RR ) -> ( X - ( F ` ( I - 1 ) ) ) e. RR )
166 164 161 165 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 )
167 166 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 )
168 40 42 syl 
 |-  ( I e. ( 1 ..^ D ) -> ( ( I - 1 ) + 1 ) = I )
169 168 3ad2ant3 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( I - 1 ) + 1 ) = I )
170 169 fveq2d 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( F ` ( ( I - 1 ) + 1 ) ) = ( F ` I ) )
171 170 oveq1d 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) = ( ( F ` I ) - ( F ` ( I - 1 ) ) ) )
172 171 breq2d 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) <-> 4 < ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) )
173 172 biimpcd 
 |-  ( 4 < ( ( F ` ( ( I - 1 ) + 1 ) ) - ( F ` ( I - 1 ) ) ) -> ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> 4 < ( ( F ` I ) - ( F ` ( I - 1 ) ) ) ) )
174 173 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 ) ) ) ) )
175 174 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 ) ) ) )
176 175 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 ) ) ) )
177 164 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 )
178 eluzge3nn 
 |-  ( D e. ( ZZ>= ` 3 ) -> D e. NN )
179 4 178 syl 
 |-  ( ph -> D e. NN )
180 179 adantr 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> D e. NN )
181 5 adantr 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> F e. ( RePart ` D ) )
182 139 140 mp1i 
 |-  ( D e. ( ZZ>= ` 3 ) -> ( 1 ..^ D ) C_ ( 0 ..^ D ) )
183 fzossfz 
 |-  ( 0 ..^ D ) C_ ( 0 ... D )
184 182 183 sstrdi 
 |-  ( D e. ( ZZ>= ` 3 ) -> ( 1 ..^ D ) C_ ( 0 ... D ) )
185 4 184 syl 
 |-  ( ph -> ( 1 ..^ D ) C_ ( 0 ... D ) )
186 185 sselda 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> I e. ( 0 ... D ) )
187 180 181 186 iccpartxr 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( F ` I ) e. RR* )
188 fzofzp1 
 |-  ( I e. ( 0 ..^ D ) -> ( I + 1 ) e. ( 0 ... D ) )
189 142 188 syl 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( I + 1 ) e. ( 0 ... D ) )
190 180 181 189 iccpartxr 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( F ` ( I + 1 ) ) e. RR* )
191 187 190 jca 
 |-  ( ( ph /\ I e. ( 1 ..^ D ) ) -> ( ( F ` I ) e. RR* /\ ( F ` ( I + 1 ) ) e. RR* ) )
192 191 3adant2 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( F ` I ) e. RR* /\ ( F ` ( I + 1 ) ) e. RR* ) )
193 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 ) ) ) ) )
194 192 193 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 ) ) ) ) )
195 simp2 
 |-  ( ( X e. RR* /\ ( F ` I ) <_ X /\ X < ( F ` ( I + 1 ) ) ) -> ( F ` I ) <_ X )
196 194 195 syl6bi 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) -> ( F ` I ) <_ X ) )
197 196 adantrd 
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ ( X - ( F ` I ) ) <_ 4 ) -> ( F ` I ) <_ X ) )
198 197 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 ) )
199 198 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 )
200 158 177 162 199 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 ) ) ) )
201 138 163 167 176 200 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 ) ) ) )
202 201 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 )
203 39 137 202 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 ) )
204 203 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 ) ) )
205 31 204 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 ) ) )