Theorem bgoldbtbndlem2

Description: Lemma 2 for bgoldbtbnd . (Contributed by AV, 1-Aug-2020)

	Ref	Expression
Hypotheses	bgoldbtbnd.m	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ ; 1 1 ) )
	bgoldbtbnd.n	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ; 1 1 ) )
	bgoldbtbnd.b	⊢ ( 𝜑 → ∀ 𝑛 ∈ Even ( ( 4 < 𝑛 ∧ 𝑛 < 𝑁 ) → 𝑛 ∈ GoldbachEven ) )
	bgoldbtbnd.d	⊢ ( 𝜑 → 𝐷 ∈ ( ℤ≥ ‘ 3 ) )
	bgoldbtbnd.f	⊢ ( 𝜑 → 𝐹 ∈ ( RePart ‘ 𝐷 ) )
	bgoldbtbnd.i	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝐷 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ) )
	bgoldbtbnd.0	⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 7 )
	bgoldbtbnd.1	⊢ ( 𝜑 → ( 𝐹 ‘ 1 ) = ; 1 3 )
	bgoldbtbnd.l	⊢ ( 𝜑 → 𝑀 < ( 𝐹 ‘ 𝐷 ) )
	bgoldbtbndlem2.s	⊢ 𝑆 = ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) )
Assertion	bgoldbtbndlem2	⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) → ( 𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆 ) ) )

Proof

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