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 ) ) )