Metamath Proof Explorer

Theorem bgoldbtbndlem3

Description: Lemma 3 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 ⊢ ( 𝜑 → 𝑀 < ( 𝐹 ‘ 𝐷 ) )
bgoldbtbnd.r ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐷 ) ∈ ℝ )
bgoldbtbndlem3.s ⊢ 𝑆 = ( 𝑋 − ( 𝐹 ‘ 𝐼 ) )
Assertion bgoldbtbndlem3 ( ( 𝜑 ∧ 𝑋 ∈ 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 bgoldbtbnd.r ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐷 ) ∈ ℝ )
11 bgoldbtbndlem3.s ⊢ 𝑆 = ( 𝑋 − ( 𝐹 ‘ 𝐼 ) )
12 fzo0ss1 ⊢ ( 1 ..^ 𝐷 ) ⊆ ( 0 ..^ 𝐷 )
13 12 sseli ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → 𝐼 ∈ ( 0 ..^ 𝐷 ) )
14 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝐼 ) )
15 14 eleq1d ⊢ ( 𝑖 = 𝐼 → ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ) )
16 fvoveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝐹 ‘ ( 𝑖 + 1 ) ) = ( 𝐹 ‘ ( 𝐼 + 1 ) ) )
17 16 14 oveq12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) = ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) )
18 17 breq1d ⊢ ( 𝑖 = 𝐼 → ( ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ↔ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) )
19 17 breq2d ⊢ ( 𝑖 = 𝐼 → ( 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ↔ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) )
20 15 18 19 3anbi123d ⊢ ( 𝑖 = 𝐼 → ( ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ) ↔ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) )
21 20 rspcv ⊢ ( 𝐼 ∈ ( 0 ..^ 𝐷 ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝐷 ) ( ( 𝐹 ‘ 𝑖 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) − ( 𝐹 ‘ 𝑖 ) ) ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) )
22 13 6 21 syl2imc ⊢ ( 𝜑 → ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) )
23 22 a1d ⊢ ( 𝜑 → ( 𝑋 ∈ Odd → ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) ) )
24 23 3imp ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) )
25 simp2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → 𝑋 ∈ Odd )
26 oddprmALTV ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) → ( 𝐹 ‘ 𝐼 ) ∈ Odd )
27 26 3ad2ant1 ⊢ ( ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) → ( 𝐹 ‘ 𝐼 ) ∈ Odd )
28 25 27 anim12i ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) → ( 𝑋 ∈ Odd ∧ ( 𝐹 ‘ 𝐼 ) ∈ Odd ) )
29 28 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ 4 < 𝑆 ) ) → ( 𝑋 ∈ Odd ∧ ( 𝐹 ‘ 𝐼 ) ∈ Odd ) )
30 omoeALTV ⊢ ( ( 𝑋 ∈ Odd ∧ ( 𝐹 ‘ 𝐼 ) ∈ Odd ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ∈ Even )
31 29 30 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ 4 < 𝑆 ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ∈ Even )
32 11 31 eqeltrid ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ 4 < 𝑆 ) ) → 𝑆 ∈ Even )
33 eldifi ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) → ( 𝐹 ‘ 𝐼 ) ∈ ℙ )
34 prmz ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ℙ → ( 𝐹 ‘ 𝐼 ) ∈ ℤ )
35 34 zred ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ℙ → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
36 fzofzp1 ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( 𝐼 + 1 ) ∈ ( 1 ... 𝐷 ) )
37 elfzo2 ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) ↔ ( 𝐼 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐷 ∈ ℤ ∧ 𝐼 < 𝐷 ) )
38 1zzd ⊢ ( ( 𝐼 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐷 ∈ ℤ ∧ 𝐼 < 𝐷 ) → 1 ∈ ℤ )
39 simp2 ⊢ ( ( 𝐼 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐷 ∈ ℤ ∧ 𝐼 < 𝐷 ) → 𝐷 ∈ ℤ )
40 eluz2 ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 1 ≤ 𝐼 ) )
41 zre ⊢ ( 1 ∈ ℤ → 1 ∈ ℝ )
42 zre ⊢ ( 𝐼 ∈ ℤ → 𝐼 ∈ ℝ )
43 zre ⊢ ( 𝐷 ∈ ℤ → 𝐷 ∈ ℝ )
44 leltletr ⊢ ( ( 1 ∈ ℝ ∧ 𝐼 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( ( 1 ≤ 𝐼 ∧ 𝐼 < 𝐷 ) → 1 ≤ 𝐷 ) )
45 41 42 43 44 syl3an ⊢ ( ( 1 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ( 1 ≤ 𝐼 ∧ 𝐼 < 𝐷 ) → 1 ≤ 𝐷 ) )
46 45 exp5o ⊢ ( 1 ∈ ℤ → ( 𝐼 ∈ ℤ → ( 𝐷 ∈ ℤ → ( 1 ≤ 𝐼 → ( 𝐼 < 𝐷 → 1 ≤ 𝐷 ) ) ) ) )
47 46 com34 ⊢ ( 1 ∈ ℤ → ( 𝐼 ∈ ℤ → ( 1 ≤ 𝐼 → ( 𝐷 ∈ ℤ → ( 𝐼 < 𝐷 → 1 ≤ 𝐷 ) ) ) ) )
48 47 3imp ⊢ ( ( 1 ∈ ℤ ∧ 𝐼 ∈ ℤ ∧ 1 ≤ 𝐼 ) → ( 𝐷 ∈ ℤ → ( 𝐼 < 𝐷 → 1 ≤ 𝐷 ) ) )
49 40 48 sylbi ⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 1 ) → ( 𝐷 ∈ ℤ → ( 𝐼 < 𝐷 → 1 ≤ 𝐷 ) ) )
50 49 3imp ⊢ ( ( 𝐼 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐷 ∈ ℤ ∧ 𝐼 < 𝐷 ) → 1 ≤ 𝐷 )
51 eluz2 ⊢ ( 𝐷 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 1 ≤ 𝐷 ) )
52 38 39 50 51 syl3anbrc ⊢ ( ( 𝐼 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐷 ∈ ℤ ∧ 𝐼 < 𝐷 ) → 𝐷 ∈ ( ℤ≥ ‘ 1 ) )
53 37 52 sylbi ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → 𝐷 ∈ ( ℤ≥ ‘ 1 ) )
54 fzisfzounsn ⊢ ( 𝐷 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... 𝐷 ) = ( ( 1 ..^ 𝐷 ) ∪ { 𝐷 } ) )
55 53 54 syl ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( 1 ... 𝐷 ) = ( ( 1 ..^ 𝐷 ) ∪ { 𝐷 } ) )
56 55 eleq2d ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ( 𝐼 + 1 ) ∈ ( 1 ... 𝐷 ) ↔ ( 𝐼 + 1 ) ∈ ( ( 1 ..^ 𝐷 ) ∪ { 𝐷 } ) ) )
57 elun ⊢ ( ( 𝐼 + 1 ) ∈ ( ( 1 ..^ 𝐷 ) ∪ { 𝐷 } ) ↔ ( ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝐷 ) ∨ ( 𝐼 + 1 ) ∈ { 𝐷 } ) )
58 56 57 bitrdi ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ( 𝐼 + 1 ) ∈ ( 1 ... 𝐷 ) ↔ ( ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝐷 ) ∨ ( 𝐼 + 1 ) ∈ { 𝐷 } ) ) )
59 eluzge3nn ⊢ ( 𝐷 ∈ ( ℤ≥ ‘ 3 ) → 𝐷 ∈ ℕ )
60 4 59 syl ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
61 60 ad2antrl ⊢ ( ( ( 𝐼 ∈ ( 1 ..^ 𝐷 ) ∧ ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝐷 ) ) ∧ ( 𝜑 ∧ 𝑋 ∈ Odd ) ) → 𝐷 ∈ ℕ )
62 5 ad2antrl ⊢ ( ( ( 𝐼 ∈ ( 1 ..^ 𝐷 ) ∧ ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝐷 ) ) ∧ ( 𝜑 ∧ 𝑋 ∈ Odd ) ) → 𝐹 ∈ ( RePart ‘ 𝐷 ) )
63 simplr ⊢ ( ( ( 𝐼 ∈ ( 1 ..^ 𝐷 ) ∧ ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝐷 ) ) ∧ ( 𝜑 ∧ 𝑋 ∈ Odd ) ) → ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝐷 ) )
64 61 62 63 iccpartipre ⊢ ( ( ( 𝐼 ∈ ( 1 ..^ 𝐷 ) ∧ ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝐷 ) ) ∧ ( 𝜑 ∧ 𝑋 ∈ Odd ) ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
65 64 exp31 ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝐷 ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ) )
66 elsni ⊢ ( ( 𝐼 + 1 ) ∈ { 𝐷 } → ( 𝐼 + 1 ) = 𝐷 )
67 10 ad2antrl ⊢ ( ( ( 𝐼 + 1 ) = 𝐷 ∧ ( 𝜑 ∧ 𝑋 ∈ Odd ) ) → ( 𝐹 ‘ 𝐷 ) ∈ ℝ )
68 fveq2 ⊢ ( ( 𝐼 + 1 ) = 𝐷 → ( 𝐹 ‘ ( 𝐼 + 1 ) ) = ( 𝐹 ‘ 𝐷 ) )
69 68 eleq1d ⊢ ( ( 𝐼 + 1 ) = 𝐷 → ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐷 ) ∈ ℝ ) )
70 69 adantr ⊢ ( ( ( 𝐼 + 1 ) = 𝐷 ∧ ( 𝜑 ∧ 𝑋 ∈ Odd ) ) → ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐷 ) ∈ ℝ ) )
71 67 70 mpbird ⊢ ( ( ( 𝐼 + 1 ) = 𝐷 ∧ ( 𝜑 ∧ 𝑋 ∈ Odd ) ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
72 71 ex ⊢ ( ( 𝐼 + 1 ) = 𝐷 → ( ( 𝜑 ∧ 𝑋 ∈ Odd ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) )
73 66 72 syl ⊢ ( ( 𝐼 + 1 ) ∈ { 𝐷 } → ( ( 𝜑 ∧ 𝑋 ∈ Odd ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) )
74 73 a1i ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ( 𝐼 + 1 ) ∈ { 𝐷 } → ( ( 𝜑 ∧ 𝑋 ∈ Odd ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ) )
75 65 74 jaod ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ( ( 𝐼 + 1 ) ∈ ( 1 ..^ 𝐷 ) ∨ ( 𝐼 + 1 ) ∈ { 𝐷 } ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ) )
76 58 75 sylbid ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ( 𝐼 + 1 ) ∈ ( 1 ... 𝐷 ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) ) )
77 36 76 mpd ⊢ ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) )
78 77 com12 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ) → ( 𝐼 ∈ ( 1 ..^ 𝐷 ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ) )
79 78 3impia ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
80 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 1 ) → 𝑁 ∈ ℝ )
81 2 80 syl ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
82 oddz ⊢ ( 𝑋 ∈ Odd → 𝑋 ∈ ℤ )
83 82 zred ⊢ ( 𝑋 ∈ Odd → 𝑋 ∈ ℝ )
84 rexr ⊢ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
85 rexr ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( 𝐹 ‘ 𝐼 ) ∈ ℝ* )
86 84 85 anim12ci ⊢ ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) )
87 86 adantl ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) )
88 elico1 ⊢ ( ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ) )
89 87 88 syl ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ) )
90 simpllr ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → 𝑋 ∈ ℝ )
91 simplrl ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ )
92 simplrr ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
93 simpr ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) )
94 90 91 92 93 ltsub1dd ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) )
95 simplr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → 𝑋 ∈ ℝ )
96 simprr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝐼 ) ∈ ℝ )
97 95 96 resubcld ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ∈ ℝ )
98 97 adantr ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ∈ ℝ )
99 91 92 resubcld ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ∈ ℝ )
100 simplll ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → 𝑁 ∈ ℝ )
101 4re ⊢ 4 ∈ ℝ
102 101 a1i ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → 4 ∈ ℝ )
103 100 102 resubcld ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑁 − 4 ) ∈ ℝ )
104 lttr ⊢ ( ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ∈ ℝ ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ∈ ℝ ∧ ( 𝑁 − 4 ) ∈ ℝ ) → ( ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) )
105 98 99 103 104 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) )
106 94 105 mpand ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) )
107 106 impr ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ ( 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) )
108 4pos ⊢ 0 < 4
109 101 a1i ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → 4 ∈ ℝ )
110 simpl ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → 𝑁 ∈ ℝ )
111 109 110 ltsubposd ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 0 < 4 ↔ ( 𝑁 − 4 ) < 𝑁 ) )
112 108 111 mpbii ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( 𝑁 − 4 ) < 𝑁 )
113 112 adantr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( 𝑁 − 4 ) < 𝑁 )
114 113 adantr ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ ( 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) ) → ( 𝑁 − 4 ) < 𝑁 )
115 simpll ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → 𝑁 ∈ ℝ )
116 101 a1i ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → 4 ∈ ℝ )
117 115 116 resubcld ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( 𝑁 − 4 ) ∈ ℝ )
118 lttr ⊢ ( ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) ∈ ℝ ∧ ( 𝑁 − 4 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ ( 𝑁 − 4 ) < 𝑁 ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) )
119 97 117 115 118 syl3anc ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ ( 𝑁 − 4 ) < 𝑁 ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) )
120 119 adantr ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ ( 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) ) → ( ( ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ ( 𝑁 − 4 ) < 𝑁 ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) )
121 107 114 120 mp2and ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) ∧ ( 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 )
122 121 exp32 ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) )
123 122 com12 ⊢ ( 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) → ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) )
124 123 3ad2ant3 ⊢ ( ( 𝑋 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) )
125 124 com12 ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( ( 𝑋 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐼 ) ≤ 𝑋 ∧ 𝑋 < ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) )
126 89 125 sylbid ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) )
127 126 com23 ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐼 ) ∈ ℝ ) ) → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) )
128 127 exp32 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) ) ) )
129 128 com34 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ ) → ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) ) ) )
130 81 83 129 syl2an ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ) → ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) ) ) )
131 130 3adant3 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) ∈ ℝ → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) ) ) )
132 79 131 mpd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) ) )
133 132 com13 ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ℝ → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) ) )
134 33 35 133 3syl ⊢ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) → ( ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) ) )
135 134 imp ⊢ ( ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) )
136 135 3adant3 ⊢ ( ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) → ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) ) )
137 136 impcom ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) → ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 ) )
138 137 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) ∧ 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 )
139 138 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ 4 < 𝑆 ) ) → ( 𝑋 − ( 𝐹 ‘ 𝐼 ) ) < 𝑁 )
140 11 139 eqbrtrid ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ 4 < 𝑆 ) ) → 𝑆 < 𝑁 )
141 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ 4 < 𝑆 ) ) → 4 < 𝑆 )
142 32 140 141 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) ∧ ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ 4 < 𝑆 ) ) → ( 𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆 ) )
143 142 ex ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) ∧ ( ( 𝐹 ‘ 𝐼 ) ∈ ( ℙ ∖ { 2 } ) ∧ ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) < ( 𝑁 − 4 ) ∧ 4 < ( ( 𝐹 ‘ ( 𝐼 + 1 ) ) − ( 𝐹 ‘ 𝐼 ) ) ) ) → ( ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ 4 < 𝑆 ) → ( 𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆 ) ) )
144 24 143 mpdan ⊢ ( ( 𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ ( 1 ..^ 𝐷 ) ) → ( ( 𝑋 ∈ ( ( 𝐹 ‘ 𝐼 ) [,) ( 𝐹 ‘ ( 𝐼 + 1 ) ) ) ∧ 4 < 𝑆 ) → ( 𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆 ) ) )