bgoldbtbndlem2

	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		eluz3nn	\|- ( 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 ) ) )

Metamath Proof Explorer

Theorem bgoldbtbndlem2

Proof