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 71 117 syl ⊢ ( 𝑁 ∈ ℤ → ( 𝑋 ∈ Odd → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) ) ) )
119 2 70 118 3syl ⊢ ( 𝜑 → ( 𝑋 ∈ Odd → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) ) ) )
120 119 imp ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) ) )
121 120 3adant3 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) ) )
122 69 121 syl5com ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ℤ → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) ) )
123 67 68 122 3syl ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) ) )
124 66 123 mpcom ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) )
125 50 124 syl5com ⊢ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℤ → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) )
126 48 49 125 3syl ⊢ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) )
127 126 impcom ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) )
128 47 127 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) )
129 128 expcom ⊢ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) )
130 129 com23 ⊢ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) → ( ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) ) )
131 130 imp ⊢ ( ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) )
132 131 3adant3 ⊢ ( ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) ) )
133 132 impcom ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) → ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) )
134 133 com12 ⊢ ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 → ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) )
135 134 adantl ⊢ ( ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) → ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 ) )
136 135 impcom ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < 𝑁 )
137 10 136 eqbrtrid ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → 𝑆 < 𝑁 )
138 76 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → 4 ∈ ℝ )
139 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
140 fzoss1 ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ..^ 𝐷 ) ⊆ ( 0 ..^ 𝐷 ) )
141 139 140 mp1i ⊢ ( 𝜑 → ( 1 ..^ 𝐷 ) ⊆ ( 0 ..^ 𝐷 ) )
142 141 sselda ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → 𝐼 ∈ ( 0 ..^ 𝐷 ) )
143 fvoveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝐹 ‘ ( 𝑖 + 1 ) ) = ( 𝐹 ‘ ( 𝐼 + 1 ) ) )
144 143 56 oveq12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) = ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) )
145 144 breq1d ⊢ ( 𝑖 = 𝐼 → ( ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ↔ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) )
146 144 breq2d ⊢ ( 𝑖 = 𝐼 → ( 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ↔ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) )
147 57 145 146 3anbi123d ⊢ ( 𝑖 = 𝐼 → ( ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ) ↔ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) )
148 147 rspcv ⊢ ( 𝐼 ∈ ( 0 ..^ 𝐷 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝐷 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) )
149 142 148 syl ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝐷 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) )
150 68 zred ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ℙ → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
151 67 150 syl ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
152 151 3ad2ant1 ⊢ ( ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
153 149 152 syl6 ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝐷 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) )
154 153 ex ⊢ ( 𝜑 → ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝐷 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) )
155 6 154 mpid ⊢ ( 𝜑 → ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) )
156 155 imp ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
157 156 3adant2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
158 157 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
159 49 zred ⊢ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℙ → ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ )
160 48 159 syl ⊢ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) → ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ )
161 160 3ad2ant1 ⊢ ( ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) → ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ )
162 161 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ )
163 158 162 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ∈ ℝ )
164 73 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → 𝑋 ∈ ℝ )
165 resubcl ⊢ ( ( 𝑋 ∈ ℝ ∧ ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ℝ ) → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ∈ ℝ )
166 164 161 165 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ∈ ℝ )
167 166 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ∈ ℝ )
168 40 42 syl ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ( 𝐼 − 1 ) + 1 ) = 𝐼 )
169 168 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝐼 − 1 ) + 1 ) = 𝐼 )
170 169 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) = ( 𝐹 ‘ 𝐼 ) )
171 170 oveq1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) = ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) )
172 171 breq2d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ↔ 4 < ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) )
173 172 biimpcd ⊢ ( 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → 4 < ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) )
174 173 3ad2ant3 ⊢ ( ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → 4 < ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) )
175 174 impcom ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) → 4 < ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) )
176 175 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → 4 < ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) )
177 164 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → 𝑋 ∈ ℝ )
178 eluzge3nn ⊢ ( 𝐷 ∈ ( ℤ≥ ‘ 3 ) → 𝐷 ∈ ℕ )
179 4 178 syl ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
180 179 adantr ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → 𝐷 ∈ ℕ )
181 5 adantr ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → 𝐹 ∈ ( RePart ‘ 𝐷 ) )
182 139 140 mp1i ⊢ ( 𝐷 ∈ ( ℤ≥ ‘ 3 ) → ( 1 ..^ 𝐷 ) ⊆ ( 0 ..^ 𝐷 ) )
183 fzossfz ⊢ ( 0 ..^ 𝐷 ) ⊆ ( 0 ... 𝐷 )
184 182 183 sstrdi ⊢ ( 𝐷 ∈ ( ℤ≥ ‘ 3 ) → ( 1 ..^ 𝐷 ) ⊆ ( 0 ... 𝐷 ) )
185 4 184 syl ⊢ ( 𝜑 → ( 1 ..^ 𝐷 ) ⊆ ( 0 ... 𝐷 ) )
186 185 sselda ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → 𝐼 ∈ ( 0 ... 𝐷 ) )
187 180 181 186 iccpartxr ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ* )
188 fzofzp1 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝐷 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝐷 ) )
189 142 188 syl ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝐷 ) )
190 180 181 189 iccpartxr ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
191 187 190 jca ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) )
192 191 3adant2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) )
193 elico1 ⊢ ( ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ) )
194 192 193 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ) )
195 simp2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 )
196 194 195 syl6bi ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 ) )
197 196 adantrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) → ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 ) )
198 197 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) → ( ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) → ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 ) )
199 198 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 )
200 158 177 162 199 lesub1dd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → ( ( 𝐹 ‘ 𝐼 ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ≤ ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) )
201 138 163 167 176 200 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → 4 < ( 𝑋 − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) )
202 201 10 breqtrrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → 4 < 𝑆 )
203 39 137 202 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) ) → ( 𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆 ) )
204 203 ex ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 − 1 ) ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( ( 𝐼 − 1 ) + 1 ) ) − ( 𝐹 ‘ ( 𝐼 − 1 ) ) ) ) ) → ( ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) → ( 𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆 ) ) )
205 31 204 mpdan ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ≤ 4 ) → ( 𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆 ) ) )