Metamath Proof Explorer


Theorem bgoldbtbndlem3

Description: Lemma 3 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 ) )
bgoldbtbnd.r
|- ( ph -> ( F ` D ) e. RR )
bgoldbtbndlem3.s
|- S = ( X - ( F ` I ) )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 bgoldbtbnd.m
 |-  ( ph -> M e. ( ZZ>= ` ; 1 1 ) )
2 bgoldbtbnd.n
 |-  ( ph -> N e. ( ZZ>= ` ; 1 1 ) )
3 bgoldbtbnd.b
 |-  ( ph -> A. n e. Even ( ( 4 < n /\ n < N ) -> n e. GoldbachEven ) )
4 bgoldbtbnd.d
 |-  ( ph -> D e. ( ZZ>= ` 3 ) )
5 bgoldbtbnd.f
 |-  ( ph -> F e. ( RePart ` D ) )
6 bgoldbtbnd.i
 |-  ( ph -> A. i e. ( 0 ..^ D ) ( ( F ` i ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) ) )
7 bgoldbtbnd.0
 |-  ( ph -> ( F ` 0 ) = 7 )
8 bgoldbtbnd.1
 |-  ( ph -> ( F ` 1 ) = ; 1 3 )
9 bgoldbtbnd.l
 |-  ( ph -> M < ( F ` D ) )
10 bgoldbtbnd.r
 |-  ( ph -> ( F ` D ) e. RR )
11 bgoldbtbndlem3.s
 |-  S = ( X - ( F ` I ) )
12 fzo0ss1
 |-  ( 1 ..^ D ) C_ ( 0 ..^ D )
13 12 sseli
 |-  ( I e. ( 1 ..^ D ) -> I e. ( 0 ..^ D ) )
14 fveq2
 |-  ( i = I -> ( F ` i ) = ( F ` I ) )
15 14 eleq1d
 |-  ( i = I -> ( ( F ` i ) e. ( Prime \ { 2 } ) <-> ( F ` I ) e. ( Prime \ { 2 } ) ) )
16 fvoveq1
 |-  ( i = I -> ( F ` ( i + 1 ) ) = ( F ` ( I + 1 ) ) )
17 16 14 oveq12d
 |-  ( i = I -> ( ( F ` ( i + 1 ) ) - ( F ` i ) ) = ( ( F ` ( I + 1 ) ) - ( F ` I ) ) )
18 17 breq1d
 |-  ( i = I -> ( ( ( F ` ( i + 1 ) ) - ( F ` i ) ) < ( N - 4 ) <-> ( ( F ` ( I + 1 ) ) - ( F ` I ) ) < ( N - 4 ) ) )
19 17 breq2d
 |-  ( i = I -> ( 4 < ( ( F ` ( i + 1 ) ) - ( F ` i ) ) <-> 4 < ( ( F ` ( I + 1 ) ) - ( F ` I ) ) ) )
20 15 18 19 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 ) ) ) ) )
21 20 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 ) ) ) ) )
22 13 6 21 syl2imc
 |-  ( ph -> ( I e. ( 1 ..^ D ) -> ( ( F ` I ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( I + 1 ) ) - ( F ` I ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( I + 1 ) ) - ( F ` I ) ) ) ) )
23 22 a1d
 |-  ( 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 ) ) ) ) ) )
24 23 3imp
 |-  ( ( 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 ) ) ) )
25 simp2
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> X e. Odd )
26 oddprmALTV
 |-  ( ( F ` I ) e. ( Prime \ { 2 } ) -> ( F ` I ) e. Odd )
27 26 3ad2ant1
 |-  ( ( ( F ` I ) e. ( Prime \ { 2 } ) /\ ( ( F ` ( I + 1 ) ) - ( F ` I ) ) < ( N - 4 ) /\ 4 < ( ( F ` ( I + 1 ) ) - ( F ` I ) ) ) -> ( F ` I ) e. Odd )
28 25 27 anim12i
 |-  ( ( ( 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 ) )
29 28 adantr
 |-  ( ( ( ( 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 ) )
30 omoeALTV
 |-  ( ( X e. Odd /\ ( F ` I ) e. Odd ) -> ( X - ( F ` I ) ) e. Even )
31 29 30 syl
 |-  ( ( ( ( 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 )
32 11 31 eqeltrid
 |-  ( ( ( ( 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 )
33 eldifi
 |-  ( ( F ` I ) e. ( Prime \ { 2 } ) -> ( F ` I ) e. Prime )
34 prmz
 |-  ( ( F ` I ) e. Prime -> ( F ` I ) e. ZZ )
35 34 zred
 |-  ( ( F ` I ) e. Prime -> ( F ` I ) e. RR )
36 fzofzp1
 |-  ( I e. ( 1 ..^ D ) -> ( I + 1 ) e. ( 1 ... D ) )
37 elfzo2
 |-  ( I e. ( 1 ..^ D ) <-> ( I e. ( ZZ>= ` 1 ) /\ D e. ZZ /\ I < D ) )
38 1zzd
 |-  ( ( I e. ( ZZ>= ` 1 ) /\ D e. ZZ /\ I < D ) -> 1 e. ZZ )
39 simp2
 |-  ( ( I e. ( ZZ>= ` 1 ) /\ D e. ZZ /\ I < D ) -> D e. ZZ )
40 eluz2
 |-  ( I e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ I e. ZZ /\ 1 <_ I ) )
41 zre
 |-  ( 1 e. ZZ -> 1 e. RR )
42 zre
 |-  ( I e. ZZ -> I e. RR )
43 zre
 |-  ( D e. ZZ -> D e. RR )
44 leltletr
 |-  ( ( 1 e. RR /\ I e. RR /\ D e. RR ) -> ( ( 1 <_ I /\ I < D ) -> 1 <_ D ) )
45 41 42 43 44 syl3an
 |-  ( ( 1 e. ZZ /\ I e. ZZ /\ D e. ZZ ) -> ( ( 1 <_ I /\ I < D ) -> 1 <_ D ) )
46 45 exp5o
 |-  ( 1 e. ZZ -> ( I e. ZZ -> ( D e. ZZ -> ( 1 <_ I -> ( I < D -> 1 <_ D ) ) ) ) )
47 46 com34
 |-  ( 1 e. ZZ -> ( I e. ZZ -> ( 1 <_ I -> ( D e. ZZ -> ( I < D -> 1 <_ D ) ) ) ) )
48 47 3imp
 |-  ( ( 1 e. ZZ /\ I e. ZZ /\ 1 <_ I ) -> ( D e. ZZ -> ( I < D -> 1 <_ D ) ) )
49 40 48 sylbi
 |-  ( I e. ( ZZ>= ` 1 ) -> ( D e. ZZ -> ( I < D -> 1 <_ D ) ) )
50 49 3imp
 |-  ( ( I e. ( ZZ>= ` 1 ) /\ D e. ZZ /\ I < D ) -> 1 <_ D )
51 eluz2
 |-  ( D e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ D e. ZZ /\ 1 <_ D ) )
52 38 39 50 51 syl3anbrc
 |-  ( ( I e. ( ZZ>= ` 1 ) /\ D e. ZZ /\ I < D ) -> D e. ( ZZ>= ` 1 ) )
53 37 52 sylbi
 |-  ( I e. ( 1 ..^ D ) -> D e. ( ZZ>= ` 1 ) )
54 fzisfzounsn
 |-  ( D e. ( ZZ>= ` 1 ) -> ( 1 ... D ) = ( ( 1 ..^ D ) u. { D } ) )
55 53 54 syl
 |-  ( I e. ( 1 ..^ D ) -> ( 1 ... D ) = ( ( 1 ..^ D ) u. { D } ) )
56 55 eleq2d
 |-  ( I e. ( 1 ..^ D ) -> ( ( I + 1 ) e. ( 1 ... D ) <-> ( I + 1 ) e. ( ( 1 ..^ D ) u. { D } ) ) )
57 elun
 |-  ( ( I + 1 ) e. ( ( 1 ..^ D ) u. { D } ) <-> ( ( I + 1 ) e. ( 1 ..^ D ) \/ ( I + 1 ) e. { D } ) )
58 56 57 bitrdi
 |-  ( I e. ( 1 ..^ D ) -> ( ( I + 1 ) e. ( 1 ... D ) <-> ( ( I + 1 ) e. ( 1 ..^ D ) \/ ( I + 1 ) e. { D } ) ) )
59 eluzge3nn
 |-  ( D e. ( ZZ>= ` 3 ) -> D e. NN )
60 4 59 syl
 |-  ( ph -> D e. NN )
61 60 ad2antrl
 |-  ( ( ( I e. ( 1 ..^ D ) /\ ( I + 1 ) e. ( 1 ..^ D ) ) /\ ( ph /\ X e. Odd ) ) -> D e. NN )
62 5 ad2antrl
 |-  ( ( ( I e. ( 1 ..^ D ) /\ ( I + 1 ) e. ( 1 ..^ D ) ) /\ ( ph /\ X e. Odd ) ) -> F e. ( RePart ` D ) )
63 simplr
 |-  ( ( ( I e. ( 1 ..^ D ) /\ ( I + 1 ) e. ( 1 ..^ D ) ) /\ ( ph /\ X e. Odd ) ) -> ( I + 1 ) e. ( 1 ..^ D ) )
64 61 62 63 iccpartipre
 |-  ( ( ( I e. ( 1 ..^ D ) /\ ( I + 1 ) e. ( 1 ..^ D ) ) /\ ( ph /\ X e. Odd ) ) -> ( F ` ( I + 1 ) ) e. RR )
65 64 exp31
 |-  ( I e. ( 1 ..^ D ) -> ( ( I + 1 ) e. ( 1 ..^ D ) -> ( ( ph /\ X e. Odd ) -> ( F ` ( I + 1 ) ) e. RR ) ) )
66 elsni
 |-  ( ( I + 1 ) e. { D } -> ( I + 1 ) = D )
67 10 ad2antrl
 |-  ( ( ( I + 1 ) = D /\ ( ph /\ X e. Odd ) ) -> ( F ` D ) e. RR )
68 fveq2
 |-  ( ( I + 1 ) = D -> ( F ` ( I + 1 ) ) = ( F ` D ) )
69 68 eleq1d
 |-  ( ( I + 1 ) = D -> ( ( F ` ( I + 1 ) ) e. RR <-> ( F ` D ) e. RR ) )
70 69 adantr
 |-  ( ( ( I + 1 ) = D /\ ( ph /\ X e. Odd ) ) -> ( ( F ` ( I + 1 ) ) e. RR <-> ( F ` D ) e. RR ) )
71 67 70 mpbird
 |-  ( ( ( I + 1 ) = D /\ ( ph /\ X e. Odd ) ) -> ( F ` ( I + 1 ) ) e. RR )
72 71 ex
 |-  ( ( I + 1 ) = D -> ( ( ph /\ X e. Odd ) -> ( F ` ( I + 1 ) ) e. RR ) )
73 66 72 syl
 |-  ( ( I + 1 ) e. { D } -> ( ( ph /\ X e. Odd ) -> ( F ` ( I + 1 ) ) e. RR ) )
74 73 a1i
 |-  ( I e. ( 1 ..^ D ) -> ( ( I + 1 ) e. { D } -> ( ( ph /\ X e. Odd ) -> ( F ` ( I + 1 ) ) e. RR ) ) )
75 65 74 jaod
 |-  ( I e. ( 1 ..^ D ) -> ( ( ( I + 1 ) e. ( 1 ..^ D ) \/ ( I + 1 ) e. { D } ) -> ( ( ph /\ X e. Odd ) -> ( F ` ( I + 1 ) ) e. RR ) ) )
76 58 75 sylbid
 |-  ( I e. ( 1 ..^ D ) -> ( ( I + 1 ) e. ( 1 ... D ) -> ( ( ph /\ X e. Odd ) -> ( F ` ( I + 1 ) ) e. RR ) ) )
77 36 76 mpd
 |-  ( I e. ( 1 ..^ D ) -> ( ( ph /\ X e. Odd ) -> ( F ` ( I + 1 ) ) e. RR ) )
78 77 com12
 |-  ( ( ph /\ X e. Odd ) -> ( I e. ( 1 ..^ D ) -> ( F ` ( I + 1 ) ) e. RR ) )
79 78 3impia
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( F ` ( I + 1 ) ) e. RR )
80 eluzelre
 |-  ( N e. ( ZZ>= ` ; 1 1 ) -> N e. RR )
81 2 80 syl
 |-  ( ph -> N e. RR )
82 oddz
 |-  ( X e. Odd -> X e. ZZ )
83 82 zred
 |-  ( X e. Odd -> X e. RR )
84 rexr
 |-  ( ( F ` ( I + 1 ) ) e. RR -> ( F ` ( I + 1 ) ) e. RR* )
85 rexr
 |-  ( ( F ` I ) e. RR -> ( F ` I ) e. RR* )
86 84 85 anim12ci
 |-  ( ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) -> ( ( F ` I ) e. RR* /\ ( F ` ( I + 1 ) ) e. RR* ) )
87 86 adantl
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) -> ( ( F ` I ) e. RR* /\ ( F ` ( I + 1 ) ) e. RR* ) )
88 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 ) ) ) ) )
89 87 88 syl
 |-  ( ( ( 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 ) ) ) ) )
90 simpllr
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) /\ X < ( F ` ( I + 1 ) ) ) -> X e. RR )
91 simplrl
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) /\ X < ( F ` ( I + 1 ) ) ) -> ( F ` ( I + 1 ) ) e. RR )
92 simplrr
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) /\ X < ( F ` ( I + 1 ) ) ) -> ( F ` I ) e. RR )
93 simpr
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) /\ X < ( F ` ( I + 1 ) ) ) -> X < ( F ` ( I + 1 ) ) )
94 90 91 92 93 ltsub1dd
 |-  ( ( ( ( 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 ) ) )
95 simplr
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) -> X e. RR )
96 simprr
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) -> ( F ` I ) e. RR )
97 95 96 resubcld
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) -> ( X - ( F ` I ) ) e. RR )
98 97 adantr
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) /\ X < ( F ` ( I + 1 ) ) ) -> ( X - ( F ` I ) ) e. RR )
99 91 92 resubcld
 |-  ( ( ( ( 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 )
100 simplll
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) /\ X < ( F ` ( I + 1 ) ) ) -> N e. RR )
101 4re
 |-  4 e. RR
102 101 a1i
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) /\ X < ( F ` ( I + 1 ) ) ) -> 4 e. RR )
103 100 102 resubcld
 |-  ( ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) /\ X < ( F ` ( I + 1 ) ) ) -> ( N - 4 ) e. RR )
104 lttr
 |-  ( ( ( 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 ) ) )
105 98 99 103 104 syl3anc
 |-  ( ( ( ( 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 ) ) )
106 94 105 mpand
 |-  ( ( ( ( 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 ) ) )
107 106 impr
 |-  ( ( ( ( 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 ) )
108 4pos
 |-  0 < 4
109 101 a1i
 |-  ( ( N e. RR /\ X e. RR ) -> 4 e. RR )
110 simpl
 |-  ( ( N e. RR /\ X e. RR ) -> N e. RR )
111 109 110 ltsubposd
 |-  ( ( N e. RR /\ X e. RR ) -> ( 0 < 4 <-> ( N - 4 ) < N ) )
112 108 111 mpbii
 |-  ( ( N e. RR /\ X e. RR ) -> ( N - 4 ) < N )
113 112 adantr
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) -> ( N - 4 ) < N )
114 113 adantr
 |-  ( ( ( ( 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 )
115 simpll
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) -> N e. RR )
116 101 a1i
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) -> 4 e. RR )
117 115 116 resubcld
 |-  ( ( ( N e. RR /\ X e. RR ) /\ ( ( F ` ( I + 1 ) ) e. RR /\ ( F ` I ) e. RR ) ) -> ( N - 4 ) e. RR )
118 lttr
 |-  ( ( ( X - ( F ` I ) ) e. RR /\ ( N - 4 ) e. RR /\ N e. RR ) -> ( ( ( X - ( F ` I ) ) < ( N - 4 ) /\ ( N - 4 ) < N ) -> ( X - ( F ` I ) ) < N ) )
119 97 117 115 118 syl3anc
 |-  ( ( ( 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 ) )
120 119 adantr
 |-  ( ( ( ( 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 ) )
121 107 114 120 mp2and
 |-  ( ( ( ( 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 )
122 121 exp32
 |-  ( ( ( 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 ) ) )
123 122 com12
 |-  ( 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 ) ) )
124 123 3ad2ant3
 |-  ( ( 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 ) ) )
125 124 com12
 |-  ( ( ( 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 ) ) )
126 89 125 sylbid
 |-  ( ( ( 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 ) ) )
127 126 com23
 |-  ( ( ( 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 ) ) )
128 127 exp32
 |-  ( ( 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 ) ) ) ) )
129 128 com34
 |-  ( ( 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 ) ) ) ) )
130 81 83 129 syl2an
 |-  ( ( 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 ) ) ) ) )
131 130 3adant3
 |-  ( ( 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 ) ) ) ) )
132 79 131 mpd
 |-  ( ( 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 ) ) ) )
133 132 com13
 |-  ( ( 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 ) ) ) )
134 33 35 133 3syl
 |-  ( ( 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 ) ) ) )
135 134 imp
 |-  ( ( ( 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 ) ) )
136 135 3adant3
 |-  ( ( ( 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 ) ) )
137 136 impcom
 |-  ( ( ( 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 ) )
138 137 imp
 |-  ( ( ( ( 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 )
139 138 adantrr
 |-  ( ( ( ( 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 )
140 11 139 eqbrtrid
 |-  ( ( ( ( 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 )
141 simprr
 |-  ( ( ( ( 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 )
142 32 140 141 3jca
 |-  ( ( ( ( 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 ) )
143 142 ex
 |-  ( ( ( 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 ) ) )
144 24 143 mpdan
 |-  ( ( ph /\ X e. Odd /\ I e. ( 1 ..^ D ) ) -> ( ( X e. ( ( F ` I ) [,) ( F ` ( I + 1 ) ) ) /\ 4 < S ) -> ( S e. Even /\ S < N /\ 4 < S ) ) )