This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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