Metamath Proof Explorer

Theorem stoweidlem34

Description: This lemma proves that for all t in T there is a j as in the proof of BrosowskiDeutsh p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem34.1 ⊢ Ⅎ 𝑡 𝐹
stoweidlem34.2 ⊢ Ⅎ 𝑗 𝜑
stoweidlem34.3 ⊢ Ⅎ 𝑡 𝜑
stoweidlem34.4 ⊢ 𝐷 = ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
stoweidlem34.5 ⊢ 𝐵 = ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
stoweidlem34.6 ⊢ 𝐽 = ( 𝑡 ∈ 𝑇 ↦ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
stoweidlem34.7 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
stoweidlem34.8 ⊢ ( 𝜑 → 𝑇 ∈ V )
stoweidlem34.9 ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
stoweidlem34.10 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝐹 ‘ 𝑡 ) )
stoweidlem34.11 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) < ( ( 𝑁 − 1 ) · 𝐸 ) )
stoweidlem34.12 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem34.13 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
stoweidlem34.14 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑗 ) : 𝑇 ⟶ ℝ )
stoweidlem34.15 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) )
stoweidlem34.16 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
stoweidlem34.17 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
stoweidlem34.18 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) )
Assertion stoweidlem34 ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem34.1 ⊢ Ⅎ 𝑡 𝐹
2 stoweidlem34.2 ⊢ Ⅎ 𝑗 𝜑
3 stoweidlem34.3 ⊢ Ⅎ 𝑡 𝜑
4 stoweidlem34.4 ⊢ 𝐷 = ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
5 stoweidlem34.5 ⊢ 𝐵 = ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
6 stoweidlem34.6 ⊢ 𝐽 = ( 𝑡 ∈ 𝑇 ↦ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
7 stoweidlem34.7 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8 stoweidlem34.8 ⊢ ( 𝜑 → 𝑇 ∈ V )
9 stoweidlem34.9 ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
10 stoweidlem34.10 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝐹 ‘ 𝑡 ) )
11 stoweidlem34.11 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) < ( ( 𝑁 − 1 ) · 𝐸 ) )
12 stoweidlem34.12 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
13 stoweidlem34.13 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
14 stoweidlem34.14 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑗 ) : 𝑇 ⟶ ℝ )
15 stoweidlem34.15 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) )
16 stoweidlem34.16 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
17 stoweidlem34.17 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
18 stoweidlem34.18 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
20 ovex ⊢ ( 1 ... 𝑁 ) ∈ V
21 20 rabex ⊢ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } ∈ V
22 6 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } ∈ V ) → ( 𝐽 ‘ 𝑡 ) = { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
23 19 21 22 sylancl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐽 ‘ 𝑡 ) = { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
24 ssrab2 ⊢ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } ⊆ ( 1 ... 𝑁 )
25 23 24 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐽 ‘ 𝑡 ) ⊆ ( 1 ... 𝑁 ) )
26 elfznn ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 𝑥 ∈ ℕ )
27 26 ssriv ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
28 25 27 sstrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐽 ‘ 𝑡 ) ⊆ ℕ )
29 nnssre ⊢ ℕ ⊆ ℝ
30 28 29 sstrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐽 ‘ 𝑡 ) ⊆ ℝ )
31 7 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ℕ )
32 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
33 31 32 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
34 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
35 33 34 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
36 3re ⊢ 3 ∈ ℝ
37 3ne0 ⊢ 3 ≠ 0
38 36 37 rereccli ⊢ ( 1 / 3 ) ∈ ℝ
39 38 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 / 3 ) ∈ ℝ )
40 1red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 1 ∈ ℝ )
41 31 nnred ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ℝ )
42 1lt3 ⊢ 1 < 3
43 36 42 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 1 < 3 )
44 recgt1i ⊢ ( ( 3 ∈ ℝ ∧ 1 < 3 ) → ( 0 < ( 1 / 3 ) ∧ ( 1 / 3 ) < 1 ) )
45 44 simprd ⊢ ( ( 3 ∈ ℝ ∧ 1 < 3 ) → ( 1 / 3 ) < 1 )
46 43 45 mp1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 / 3 ) < 1 )
47 39 40 41 46 ltsub2dd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑁 − 1 ) < ( 𝑁 − ( 1 / 3 ) ) )
48 41 40 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑁 − 1 ) ∈ ℝ )
49 41 39 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑁 − ( 1 / 3 ) ) ∈ ℝ )
50 12 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝐸 ∈ ℝ )
52 12 rpgt0d ⊢ ( 𝜑 → 0 < 𝐸 )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 < 𝐸 )
54 ltmul1 ⊢ ( ( ( 𝑁 − 1 ) ∈ ℝ ∧ ( 𝑁 − ( 1 / 3 ) ) ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( ( 𝑁 − 1 ) < ( 𝑁 − ( 1 / 3 ) ) ↔ ( ( 𝑁 − 1 ) · 𝐸 ) < ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) )
55 48 49 51 53 54 syl112anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑁 − 1 ) < ( 𝑁 − ( 1 / 3 ) ) ↔ ( ( 𝑁 − 1 ) · 𝐸 ) < ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) )
56 47 55 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑁 − 1 ) · 𝐸 ) < ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) )
57 11 56 jca ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐹 ‘ 𝑡 ) < ( ( 𝑁 − 1 ) · 𝐸 ) ∧ ( ( 𝑁 − 1 ) · 𝐸 ) < ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) )
58 9 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
59 48 51 remulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑁 − 1 ) · 𝐸 ) ∈ ℝ )
60 49 51 remulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
61 lttr ⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) · 𝐸 ) ∈ ℝ ∧ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑡 ) < ( ( 𝑁 − 1 ) · 𝐸 ) ∧ ( ( 𝑁 − 1 ) · 𝐸 ) < ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) → ( 𝐹 ‘ 𝑡 ) < ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) )
62 ltle ⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑡 ) < ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) → ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) )
63 62 3adant2 ⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) · 𝐸 ) ∈ ℝ ∧ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝑡 ) < ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) → ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) )
64 61 63 syld ⊢ ( ( ( 𝐹 ‘ 𝑡 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) · 𝐸 ) ∈ ℝ ∧ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑡 ) < ( ( 𝑁 − 1 ) · 𝐸 ) ∧ ( ( 𝑁 − 1 ) · 𝐸 ) < ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) → ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) )
65 58 59 60 64 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝐹 ‘ 𝑡 ) < ( ( 𝑁 − 1 ) · 𝐸 ) ∧ ( ( 𝑁 − 1 ) · 𝐸 ) < ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) → ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) )
66 57 65 mpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) )
67 rabid ⊢ ( 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) } ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) )
68 19 66 67 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) } )
69 oveq1 ⊢ ( 𝑗 = 𝑁 → ( 𝑗 − ( 1 / 3 ) ) = ( 𝑁 − ( 1 / 3 ) ) )
70 69 oveq1d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) = ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) )
71 70 breq2d ⊢ ( 𝑗 = 𝑁 → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) ) )
72 71 rabbidv ⊢ ( 𝑗 = 𝑁 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) } )
73 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
74 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
75 73 74 eleqtrdi ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
76 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 𝑁 ∈ ( 0 ... 𝑁 ) )
77 7 75 76 3syl ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
78 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
79 8 78 syl ⊢ ( 𝜑 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
80 4 72 77 79 fvmptd3 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) } )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐷 ‘ 𝑁 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑁 − ( 1 / 3 ) ) · 𝐸 ) } )
82 68 81 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ ( 𝐷 ‘ 𝑁 ) )
83 nfcv ⊢ Ⅎ 𝑗 𝑁
84 nfcv ⊢ Ⅎ 𝑗 ( 1 ... 𝑁 )
85 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
86 4 85 nfcxfr ⊢ Ⅎ 𝑗 𝐷
87 86 83 nffv ⊢ Ⅎ 𝑗 ( 𝐷 ‘ 𝑁 )
88 87 nfcri ⊢ Ⅎ 𝑗 𝑡 ∈ ( 𝐷 ‘ 𝑁 )
89 fveq2 ⊢ ( 𝑗 = 𝑁 → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑁 ) )
90 89 eleq2d ⊢ ( 𝑗 = 𝑁 → ( 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ↔ 𝑡 ∈ ( 𝐷 ‘ 𝑁 ) ) )
91 83 84 88 90 elrabf ⊢ ( 𝑁 ∈ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } ↔ ( 𝑁 ∈ ( 1 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑁 ) ) )
92 35 82 91 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
93 92 23 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ( 𝐽 ‘ 𝑡 ) )
94 ne0i ⊢ ( 𝑁 ∈ ( 𝐽 ‘ 𝑡 ) → ( 𝐽 ‘ 𝑡 ) ≠ ∅ )
95 93 94 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐽 ‘ 𝑡 ) ≠ ∅ )
96 nnwo ⊢ ( ( ( 𝐽 ‘ 𝑡 ) ⊆ ℕ ∧ ( 𝐽 ‘ 𝑡 ) ≠ ∅ ) → ∃ 𝑖 ∈ ( 𝐽 ‘ 𝑡 ) ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑖 ≤ 𝑘 )
97 nfcv ⊢ Ⅎ 𝑖 ( 𝐽 ‘ 𝑡 )
98 nfcv ⊢ Ⅎ 𝑗 𝑇
99 nfrab1 ⊢ Ⅎ 𝑗 { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) }
100 98 99 nfmpt ⊢ Ⅎ 𝑗 ( 𝑡 ∈ 𝑇 ↦ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
101 6 100 nfcxfr ⊢ Ⅎ 𝑗 𝐽
102 nfcv ⊢ Ⅎ 𝑗 𝑡
103 101 102 nffv ⊢ Ⅎ 𝑗 ( 𝐽 ‘ 𝑡 )
104 nfv ⊢ Ⅎ 𝑗 𝑖 ≤ 𝑘
105 103 104 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑖 ≤ 𝑘
106 nfv ⊢ Ⅎ 𝑖 ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘
107 breq1 ⊢ ( 𝑖 = 𝑗 → ( 𝑖 ≤ 𝑘 ↔ 𝑗 ≤ 𝑘 ) )
108 107 ralbidv ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑖 ≤ 𝑘 ↔ ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 ) )
109 97 103 105 106 108 cbvrexfw ⊢ ( ∃ 𝑖 ∈ ( 𝐽 ‘ 𝑡 ) ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑖 ≤ 𝑘 ↔ ∃ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 )
110 96 109 sylib ⊢ ( ( ( 𝐽 ‘ 𝑡 ) ⊆ ℕ ∧ ( 𝐽 ‘ 𝑡 ) ≠ ∅ ) → ∃ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 )
111 28 95 110 syl2anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 )
112 nfv ⊢ Ⅎ 𝑗 𝑡 ∈ 𝑇
113 2 112 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑡 ∈ 𝑇 )
114 23 eleq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ↔ 𝑗 ∈ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } ) )
115 114 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → 𝑗 ∈ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
116 rabid ⊢ ( 𝑗 ∈ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } ↔ ( 𝑗 ∈ ( 1 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) )
117 115 116 sylib ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) )
118 117 simprd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
119 118 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 ) → 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
120 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) )
121 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → 𝜑 )
122 noel ⊢ ¬ 𝑡 ∈ ∅
123 oveq1 ⊢ ( 𝑗 = 1 → ( 𝑗 − 1 ) = ( 1 − 1 ) )
124 1m1e0 ⊢ ( 1 − 1 ) = 0
125 123 124 eqtrdi ⊢ ( 𝑗 = 1 → ( 𝑗 − 1 ) = 0 )
126 125 fveq2d ⊢ ( 𝑗 = 1 → ( 𝐷 ‘ ( 𝑗 − 1 ) ) = ( 𝐷 ‘ 0 ) )
127 36 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 3 ∈ ℝ )
128 37 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 3 ≠ 0 )
129 40 127 128 redivcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 / 3 ) ∈ ℝ )
130 129 renegcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → - ( 1 / 3 ) ∈ ℝ )
131 130 51 remulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( - ( 1 / 3 ) · 𝐸 ) ∈ ℝ )
132 0red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ∈ ℝ )
133 3pos ⊢ 0 < 3
134 36 133 recgt0ii ⊢ 0 < ( 1 / 3 )
135 lt0neg2 ⊢ ( ( 1 / 3 ) ∈ ℝ → ( 0 < ( 1 / 3 ) ↔ - ( 1 / 3 ) < 0 ) )
136 38 135 ax-mp ⊢ ( 0 < ( 1 / 3 ) ↔ - ( 1 / 3 ) < 0 )
137 134 136 mpbi ⊢ - ( 1 / 3 ) < 0
138 ltmul1 ⊢ ( ( - ( 1 / 3 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( - ( 1 / 3 ) < 0 ↔ ( - ( 1 / 3 ) · 𝐸 ) < ( 0 · 𝐸 ) ) )
139 130 132 51 53 138 syl112anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( - ( 1 / 3 ) < 0 ↔ ( - ( 1 / 3 ) · 𝐸 ) < ( 0 · 𝐸 ) ) )
140 137 139 mpbii ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( - ( 1 / 3 ) · 𝐸 ) < ( 0 · 𝐸 ) )
141 mul02lem2 ⊢ ( 𝐸 ∈ ℝ → ( 0 · 𝐸 ) = 0 )
142 51 141 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 · 𝐸 ) = 0 )
143 140 142 breqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( - ( 1 / 3 ) · 𝐸 ) < 0 )
144 131 132 58 143 10 ltletrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( - ( 1 / 3 ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) )
145 131 58 ltnled ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( - ( 1 / 3 ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) ) )
146 144 145 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) )
147 nan ⊢ ( ( 𝜑 → ¬ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) ) ) ↔ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) ) )
148 146 147 mpbir ⊢ ( 𝜑 → ¬ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) ) )
149 rabid ⊢ ( 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) } ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) ) )
150 148 149 sylnibr ⊢ ( 𝜑 → ¬ 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) } )
151 oveq1 ⊢ ( 𝑗 = 0 → ( 𝑗 − ( 1 / 3 ) ) = ( 0 − ( 1 / 3 ) ) )
152 df-neg ⊢ - ( 1 / 3 ) = ( 0 − ( 1 / 3 ) )
153 151 152 eqtr4di ⊢ ( 𝑗 = 0 → ( 𝑗 − ( 1 / 3 ) ) = - ( 1 / 3 ) )
154 153 oveq1d ⊢ ( 𝑗 = 0 → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) = ( - ( 1 / 3 ) · 𝐸 ) )
155 154 breq2d ⊢ ( 𝑗 = 0 → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) ) )
156 155 rabbidv ⊢ ( 𝑗 = 0 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) } )
157 7 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
158 elnn0uz ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
159 157 158 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
160 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑁 ) )
161 159 160 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
162 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) } ∈ V )
163 8 162 syl ⊢ ( 𝜑 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) } ∈ V )
164 4 156 161 163 fvmptd3 ⊢ ( 𝜑 → ( 𝐷 ‘ 0 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( - ( 1 / 3 ) · 𝐸 ) } )
165 150 164 neleqtrrd ⊢ ( 𝜑 → ¬ 𝑡 ∈ ( 𝐷 ‘ 0 ) )
166 3 165 alrimi ⊢ ( 𝜑 → ∀ 𝑡 ¬ 𝑡 ∈ ( 𝐷 ‘ 0 ) )
167 nfcv ⊢ Ⅎ 𝑡 ( 0 ... 𝑁 )
168 nfrab1 ⊢ Ⅎ 𝑡 { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) }
169 167 168 nfmpt ⊢ Ⅎ 𝑡 ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
170 4 169 nfcxfr ⊢ Ⅎ 𝑡 𝐷
171 nfcv ⊢ Ⅎ 𝑡 0
172 170 171 nffv ⊢ Ⅎ 𝑡 ( 𝐷 ‘ 0 )
173 172 eq0f ⊢ ( ( 𝐷 ‘ 0 ) = ∅ ↔ ∀ 𝑡 ¬ 𝑡 ∈ ( 𝐷 ‘ 0 ) )
174 166 173 sylibr ⊢ ( 𝜑 → ( 𝐷 ‘ 0 ) = ∅ )
175 126 174 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑗 = 1 ) → ( 𝐷 ‘ ( 𝑗 − 1 ) ) = ∅ )
176 175 eleq2d ⊢ ( ( 𝜑 ∧ 𝑗 = 1 ) → ( 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ↔ 𝑡 ∈ ∅ ) )
177 122 176 mtbiri ⊢ ( ( 𝜑 ∧ 𝑗 = 1 ) → ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) )
178 177 ex ⊢ ( 𝜑 → ( 𝑗 = 1 → ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) )
179 178 con2d ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) → ¬ 𝑗 = 1 ) )
180 121 120 179 sylc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ¬ 𝑗 = 1 )
181 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ ¬ 𝑗 = 1 ) → 𝜑 )
182 114 116 bitrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ↔ ( 𝑗 ∈ ( 1 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ) )
183 182 simprbda ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
184 7 32 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
185 184 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
186 elfzp12 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 = 1 ∨ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) ) )
187 185 186 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 = 1 ∨ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) ) )
188 187 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 = 1 ∨ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) ) )
189 183 188 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → ( 𝑗 = 1 ∨ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) )
190 189 orcanai ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ ¬ 𝑗 = 1 ) → 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) )
191 fzssp1 ⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) )
192 7 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
193 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
194 192 193 npcand ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
195 194 oveq2d ⊢ ( 𝜑 → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) )
196 191 195 sseqtrid ⊢ ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
197 196 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) )
198 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) )
199 1z ⊢ 1 ∈ ℤ
200 zaddcl ⊢ ( ( 1 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 1 + 1 ) ∈ ℤ )
201 199 199 200 mp2an ⊢ ( 1 + 1 ) ∈ ℤ
202 201 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 1 + 1 ) ∈ ℤ )
203 7 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
204 203 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → 𝑁 ∈ ℤ )
205 elfzelz ⊢ ( 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) → 𝑗 ∈ ℤ )
206 205 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → 𝑗 ∈ ℤ )
207 1zzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → 1 ∈ ℤ )
208 fzsubel ⊢ ( ( ( ( 1 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑗 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↔ ( 𝑗 − 1 ) ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) ) )
209 202 204 206 207 208 syl22anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ↔ ( 𝑗 − 1 ) ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) ) )
210 198 209 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑗 − 1 ) ∈ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) )
211 ax-1cn ⊢ 1 ∈ ℂ
212 211 211 pncan3oi ⊢ ( ( 1 + 1 ) − 1 ) = 1
213 212 oveq1i ⊢ ( ( ( 1 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) = ( 1 ... ( 𝑁 − 1 ) )
214 210 213 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑗 − 1 ) ∈ ( 1 ... ( 𝑁 − 1 ) ) )
215 197 214 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) → ( 𝑗 − 1 ) ∈ ( 1 ... 𝑁 ) )
216 181 190 215 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ ¬ 𝑗 = 1 ) → ( 𝑗 − 1 ) ∈ ( 1 ... 𝑁 ) )
217 216 ex ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → ( ¬ 𝑗 = 1 → ( 𝑗 − 1 ) ∈ ( 1 ... 𝑁 ) ) )
218 217 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ( ¬ 𝑗 = 1 → ( 𝑗 − 1 ) ∈ ( 1 ... 𝑁 ) ) )
219 180 218 mpd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ( 𝑗 − 1 ) ∈ ( 1 ... 𝑁 ) )
220 fveq2 ⊢ ( 𝑖 = ( 𝑗 − 1 ) → ( 𝐷 ‘ 𝑖 ) = ( 𝐷 ‘ ( 𝑗 − 1 ) ) )
221 220 eleq2d ⊢ ( 𝑖 = ( 𝑗 − 1 ) → ( 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) ↔ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) )
222 221 elrab3 ⊢ ( ( 𝑗 − 1 ) ∈ ( 1 ... 𝑁 ) → ( ( 𝑗 − 1 ) ∈ { 𝑖 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) } ↔ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) )
223 219 222 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ( ( 𝑗 − 1 ) ∈ { 𝑖 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) } ↔ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) )
224 120 223 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ( 𝑗 − 1 ) ∈ { 𝑖 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) } )
225 nfcv ⊢ Ⅎ 𝑖 ( 1 ... 𝑁 )
226 nfv ⊢ Ⅎ 𝑖 𝑡 ∈ ( 𝐷 ‘ 𝑗 )
227 nfcv ⊢ Ⅎ 𝑗 𝑖
228 86 227 nffv ⊢ Ⅎ 𝑗 ( 𝐷 ‘ 𝑖 )
229 228 nfcri ⊢ Ⅎ 𝑗 𝑡 ∈ ( 𝐷 ‘ 𝑖 )
230 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑖 ) )
231 230 eleq2d ⊢ ( 𝑗 = 𝑖 → ( 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ↔ 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) ) )
232 84 225 226 229 231 cbvrabw ⊢ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } = { 𝑖 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) }
233 224 232 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ( 𝑗 − 1 ) ∈ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
234 23 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ( 𝐽 ‘ 𝑡 ) = { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
235 233 234 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ( 𝑗 − 1 ) ∈ ( 𝐽 ‘ 𝑡 ) )
236 elfzelz ⊢ ( 𝑗 ∈ ( 1 ... 𝑁 ) → 𝑗 ∈ ℤ )
237 zre ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ℝ )
238 183 236 237 3syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → 𝑗 ∈ ℝ )
239 238 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → 𝑗 ∈ ℝ )
240 peano2rem ⊢ ( 𝑗 ∈ ℝ → ( 𝑗 − 1 ) ∈ ℝ )
241 ltm1 ⊢ ( 𝑗 ∈ ℝ → ( 𝑗 − 1 ) < 𝑗 )
242 241 adantr ⊢ ( ( 𝑗 ∈ ℝ ∧ ( 𝑗 − 1 ) ∈ ℝ ) → ( 𝑗 − 1 ) < 𝑗 )
243 ltnle ⊢ ( ( ( 𝑗 − 1 ) ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( ( 𝑗 − 1 ) < 𝑗 ↔ ¬ 𝑗 ≤ ( 𝑗 − 1 ) ) )
244 243 ancoms ⊢ ( ( 𝑗 ∈ ℝ ∧ ( 𝑗 − 1 ) ∈ ℝ ) → ( ( 𝑗 − 1 ) < 𝑗 ↔ ¬ 𝑗 ≤ ( 𝑗 − 1 ) ) )
245 242 244 mpbid ⊢ ( ( 𝑗 ∈ ℝ ∧ ( 𝑗 − 1 ) ∈ ℝ ) → ¬ 𝑗 ≤ ( 𝑗 − 1 ) )
246 239 240 245 syl2anc2 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ¬ 𝑗 ≤ ( 𝑗 − 1 ) )
247 breq2 ⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( 𝑗 ≤ 𝑘 ↔ 𝑗 ≤ ( 𝑗 − 1 ) ) )
248 247 notbid ⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( ¬ 𝑗 ≤ 𝑘 ↔ ¬ 𝑗 ≤ ( 𝑗 − 1 ) ) )
249 248 rspcev ⊢ ( ( ( 𝑗 − 1 ) ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑗 ≤ ( 𝑗 − 1 ) ) → ∃ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) ¬ 𝑗 ≤ 𝑘 )
250 235 246 249 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ∃ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) ¬ 𝑗 ≤ 𝑘 )
251 rexnal ⊢ ( ∃ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) ¬ 𝑗 ≤ 𝑘 ↔ ¬ ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 )
252 250 251 sylib ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ¬ ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 )
253 252 3expia ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → ( 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) → ¬ ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 ) )
254 253 con2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → ( ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 → ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) )
255 254 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 ) → ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) )
256 119 255 eldifd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 ) → 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) )
257 256 exp31 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) → ( ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 → 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) )
258 113 257 reximdai ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ∃ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∀ 𝑘 ∈ ( 𝐽 ‘ 𝑡 ) 𝑗 ≤ 𝑘 → ∃ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) )
259 111 258 mpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) )
260 df-rex ⊢ ( ∃ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ↔ ∃ 𝑗 ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) )
261 259 260 sylib ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑗 ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) )
262 simprl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) )
263 eldifn ⊢ ( 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) )
264 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → 𝑡 ∈ 𝑇 )
265 simpll ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → 𝜑 )
266 183 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
267 simprr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) )
268 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 − ( 1 / 3 ) ) = ( 𝑘 − ( 1 / 3 ) ) )
269 268 oveq1d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) = ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) )
270 269 breq2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) ) )
271 270 rabbidv ⊢ ( 𝑗 = 𝑘 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) } )
272 271 cbvmptv ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ) = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) } )
273 4 272 eqtri ⊢ 𝐷 = ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) } )
274 oveq1 ⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( 𝑘 − ( 1 / 3 ) ) = ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) )
275 274 oveq1d ⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) = ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) )
276 275 breq2d ⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) )
277 276 rabbidv ⊢ ( 𝑘 = ( 𝑗 − 1 ) → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) } = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } )
278 fzssp1 ⊢ ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( ( 𝑁 − 1 ) + 1 ) )
279 194 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 0 ... 𝑁 ) )
280 278 279 sseqtrid ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
281 280 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
282 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
283 1zzd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℤ )
284 203 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
285 236 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ℤ )
286 fzsubel ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑗 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
287 283 284 285 283 286 syl22anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
288 282 287 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑗 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) )
289 124 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 1 ) = 0 )
290 289 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) ) )
291 288 290 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
292 281 291 sseldd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ... 𝑁 ) )
293 8 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑇 ∈ V )
294 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
295 293 294 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
296 273 277 292 295 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ ( 𝑗 − 1 ) ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } )
297 296 eleq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ↔ 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } ) )
298 297 notbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ↔ ¬ 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } ) )
299 298 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) → ¬ 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } )
300 265 266 267 299 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ¬ 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } )
301 rabid ⊢ ( 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) )
302 238 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → 𝑗 ∈ ℝ )
303 recn ⊢ ( 𝑗 ∈ ℝ → 𝑗 ∈ ℂ )
304 1cnd ⊢ ( 𝑗 ∈ ℝ → 1 ∈ ℂ )
305 1re ⊢ 1 ∈ ℝ
306 305 36 37 3pm3.2i ⊢ ( 1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0 )
307 redivcl ⊢ ( ( 1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0 ) → ( 1 / 3 ) ∈ ℝ )
308 recn ⊢ ( ( 1 / 3 ) ∈ ℝ → ( 1 / 3 ) ∈ ℂ )
309 306 307 308 mp2b ⊢ ( 1 / 3 ) ∈ ℂ
310 309 a1i ⊢ ( 𝑗 ∈ ℝ → ( 1 / 3 ) ∈ ℂ )
311 303 304 310 subsub4d ⊢ ( 𝑗 ∈ ℝ → ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) = ( 𝑗 − ( 1 + ( 1 / 3 ) ) ) )
312 3cn ⊢ 3 ∈ ℂ
313 312 211 312 37 divdiri ⊢ ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
314 3p1e4 ⊢ ( 3 + 1 ) = 4
315 314 oveq1i ⊢ ( ( 3 + 1 ) / 3 ) = ( 4 / 3 )
316 312 37 dividi ⊢ ( 3 / 3 ) = 1
317 316 oveq1i ⊢ ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
318 313 315 317 3eqtr3i ⊢ ( 4 / 3 ) = ( 1 + ( 1 / 3 ) )
319 318 a1i ⊢ ( 𝑗 ∈ ℝ → ( 4 / 3 ) = ( 1 + ( 1 / 3 ) ) )
320 319 oveq2d ⊢ ( 𝑗 ∈ ℝ → ( 𝑗 − ( 4 / 3 ) ) = ( 𝑗 − ( 1 + ( 1 / 3 ) ) ) )
321 311 320 eqtr4d ⊢ ( 𝑗 ∈ ℝ → ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) = ( 𝑗 − ( 4 / 3 ) ) )
322 321 oveq1d ⊢ ( 𝑗 ∈ ℝ → ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) = ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) )
323 302 322 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) = ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) )
324 323 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ) )
325 324 anbi2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ( ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ) ) )
326 301 325 syl5bb ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ( 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝑗 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ) ) )
327 300 326 mtbid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ¬ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ) )
328 imnan ⊢ ( ( 𝑡 ∈ 𝑇 → ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ) ↔ ¬ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ) )
329 327 328 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ( 𝑡 ∈ 𝑇 → ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ) )
330 264 329 mpd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ¬ 𝑡 ∈ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) )
331 263 330 sylanr2 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) )
332 238 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 𝑗 ∈ ℝ )
333 4re ⊢ 4 ∈ ℝ
334 333 a1i ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 4 ∈ ℝ )
335 36 a1i ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 3 ∈ ℝ )
336 37 a1i ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 3 ≠ 0 )
337 334 335 336 redivcld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( 4 / 3 ) ∈ ℝ )
338 332 337 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( 𝑗 − ( 4 / 3 ) ) ∈ ℝ )
339 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 𝐸 ∈ ℝ )
340 remulcl ⊢ ( ( ( 𝑗 − ( 4 / 3 ) ) ∈ ℝ ∧ 𝐸 ∈ ℝ ) → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ∈ ℝ )
341 340 rexrd ⊢ ( ( ( 𝑗 − ( 4 / 3 ) ) ∈ ℝ ∧ 𝐸 ∈ ℝ ) → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ∈ ℝ* )
342 338 339 341 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ∈ ℝ* )
343 58 rexrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ* )
344 343 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ* )
345 xrltnle ⊢ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑡 ) ∈ ℝ* ) → ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ) )
346 342 344 345 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) ) )
347 331 346 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) )
348 simpl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) )
349 simprr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) )
350 349 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
351 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → 𝜑 )
352 183 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
353 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
354 oveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 − ( 1 / 3 ) ) = ( 𝑗 − ( 1 / 3 ) ) )
355 354 oveq1d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) = ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) )
356 355 breq2d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) )
357 356 rabbidv ⊢ ( 𝑘 = 𝑗 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑘 − ( 1 / 3 ) ) · 𝐸 ) } = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
358 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
359 358 sseli ⊢ ( 𝑗 ∈ ( 1 ... 𝑁 ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
360 359 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
361 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
362 293 361 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
363 273 357 360 362 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑗 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
364 363 eleq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ↔ 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ) )
365 364 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
366 351 352 353 365 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
367 rabid ⊢ ( 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) )
368 366 367 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) )
369 368 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) )
370 348 262 350 369 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) )
371 347 370 jca ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) )
372 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 𝑁 ∈ ℕ )
373 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 𝑡 ∈ 𝑇 )
374 183 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
375 nfv ⊢ Ⅎ 𝑗 𝑖 ∈ ( 0 ... 𝑁 )
376 2 375 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) )
377 nfv ⊢ Ⅎ 𝑗 ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ
378 376 377 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
379 eleq1w ⊢ ( 𝑗 = 𝑖 → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ 𝑖 ∈ ( 0 ... 𝑁 ) ) )
380 379 anbi2d ⊢ ( 𝑗 = 𝑖 → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) ) )
381 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑋 ‘ 𝑗 ) = ( 𝑋 ‘ 𝑖 ) )
382 381 feq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑋 ‘ 𝑗 ) : 𝑇 ⟶ ℝ ↔ ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) )
383 380 382 imbi12d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑗 ) : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ ) ) )
384 378 383 14 chvarfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
385 384 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
386 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝜑 )
387 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
388 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑡 ∈ 𝑇 )
389 2 375 112 nf3an ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 )
390 nfv ⊢ Ⅎ 𝑗 ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1
391 389 390 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 )
392 379 3anbi2d ⊢ ( 𝑗 = 𝑖 → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) ↔ ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) ) )
393 381 fveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) = ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
394 393 breq1d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ↔ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) )
395 392 394 imbi12d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
396 391 395 16 chvarfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 )
397 386 387 388 396 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 )
398 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝜑 )
399 0zd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 0 ∈ ℤ )
400 elfzel2 ⊢ ( 𝑖 ∈ ( 𝑗 ... 𝑁 ) → 𝑁 ∈ ℤ )
401 400 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
402 elfzelz ⊢ ( 𝑖 ∈ ( 𝑗 ... 𝑁 ) → 𝑖 ∈ ℤ )
403 402 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ℤ )
404 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 0 ∈ ℝ )
405 elfzel1 ⊢ ( 𝑖 ∈ ( 𝑗 ... 𝑁 ) → 𝑗 ∈ ℤ )
406 405 zred ⊢ ( 𝑖 ∈ ( 𝑗 ... 𝑁 ) → 𝑗 ∈ ℝ )
407 406 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑗 ∈ ℝ )
408 402 zred ⊢ ( 𝑖 ∈ ( 𝑗 ... 𝑁 ) → 𝑖 ∈ ℝ )
409 408 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ℝ )
410 0red ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → 0 ∈ ℝ )
411 1red ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → 1 ∈ ℝ )
412 0le1 ⊢ 0 ≤ 1
413 412 a1i ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → 0 ≤ 1 )
414 elfzle1 ⊢ ( 𝑗 ∈ ( 1 ... 𝑁 ) → 1 ≤ 𝑗 )
415 183 414 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → 1 ≤ 𝑗 )
416 410 411 238 413 415 letrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) → 0 ≤ 𝑗 )
417 416 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 0 ≤ 𝑗 )
418 elfzle1 ⊢ ( 𝑖 ∈ ( 𝑗 ... 𝑁 ) → 𝑗 ≤ 𝑖 )
419 418 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑗 ≤ 𝑖 )
420 404 407 409 417 419 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 0 ≤ 𝑖 )
421 elfzle2 ⊢ ( 𝑖 ∈ ( 𝑗 ... 𝑁 ) → 𝑖 ≤ 𝑁 )
422 421 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ≤ 𝑁 )
423 399 401 403 420 422 elfzd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
424 423 adantlrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
425 simpll ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) )
426 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) )
427 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) )
428 427 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
429 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ( 𝑗 ... 𝑁 ) )
430 simpl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) )
431 430 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑡 ∈ 𝑇 )
432 430 58 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
433 406 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑗 ∈ ℝ )
434 38 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 1 / 3 ) ∈ ℝ )
435 433 434 resubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝑗 − ( 1 / 3 ) ) ∈ ℝ )
436 simpl1l ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝜑 )
437 436 50 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝐸 ∈ ℝ )
438 435 437 remulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
439 408 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ℝ )
440 38 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 1 / 3 ) ∈ ℝ )
441 439 440 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝑖 − ( 1 / 3 ) ) ∈ ℝ )
442 50 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝐸 ∈ ℝ )
443 441 442 remulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
444 436 443 sylancom ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
445 simpl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
446 simpl2 ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) )
447 430 446 183 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑗 ∈ ( 1 ... 𝑁 ) )
448 436 447 363 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑗 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
449 445 448 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
450 449 367 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) )
451 450 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) )
452 408 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ℝ )
453 418 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑗 ≤ 𝑖 )
454 433 452 434 453 lesub1dd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝑗 − ( 1 / 3 ) ) ≤ ( 𝑖 − ( 1 / 3 ) ) )
455 436 441 sylancom ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝑖 − ( 1 / 3 ) ) ∈ ℝ )
456 12 rpregt0d ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
457 436 456 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
458 lemul1 ⊢ ( ( ( 𝑗 − ( 1 / 3 ) ) ∈ ℝ ∧ ( 𝑖 − ( 1 / 3 ) ) ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) ≤ ( 𝑖 − ( 1 / 3 ) ) ↔ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) ) )
459 435 455 457 458 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) ≤ ( 𝑖 − ( 1 / 3 ) ) ↔ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) ) )
460 454 459 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) )
461 432 438 444 451 460 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) )
462 rabid ⊢ ( 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) } ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) ) )
463 431 461 462 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) } )
464 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ( 𝑗 ... 𝑁 ) )
465 0zd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 0 ∈ ℤ )
466 400 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
467 402 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ℤ )
468 465 466 467 3jca ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ) )
469 420 422 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) )
470 469 3impa ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) )
471 elfz2 ⊢ ( 𝑖 ∈ ( 0 ... 𝑁 ) ↔ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ) ∧ ( 0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
472 468 470 471 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
473 430 446 464 472 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
474 oveq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 − ( 1 / 3 ) ) = ( 𝑖 − ( 1 / 3 ) ) )
475 474 oveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) = ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) )
476 475 breq2d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) ) )
477 476 rabbidv ⊢ ( 𝑗 = 𝑖 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) } )
478 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
479 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
480 8 479 syl ⊢ ( 𝜑 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
481 480 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
482 4 477 478 481 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑖 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) } )
483 436 473 482 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑖 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑖 − ( 1 / 3 ) ) · 𝐸 ) } )
484 463 483 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) )
485 425 426 428 429 484 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) )
486 2 375 229 nf3an ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) )
487 nfv ⊢ Ⅎ 𝑗 ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 )
488 486 487 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
489 379 231 3anbi23d ⊢ ( 𝑗 = 𝑖 → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) ↔ ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) ) ) )
490 393 breq1d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) )
491 489 490 imbi12d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) ) )
492 488 491 17 chvarfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑖 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
493 398 424 485 492 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
494 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 𝐸 ∈ ℝ+ )
495 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → 𝐸 < ( 1 / 3 ) )
496 372 373 374 385 397 493 494 495 stoweidlem11 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )
497 eleq1w ⊢ ( 𝑙 = 𝑗 → ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ↔ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ) )
498 fveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐷 ‘ 𝑙 ) = ( 𝐷 ‘ 𝑗 ) )
499 oveq1 ⊢ ( 𝑙 = 𝑗 → ( 𝑙 − 1 ) = ( 𝑗 − 1 ) )
500 499 fveq2d ⊢ ( 𝑙 = 𝑗 → ( 𝐷 ‘ ( 𝑙 − 1 ) ) = ( 𝐷 ‘ ( 𝑗 − 1 ) ) )
501 498 500 difeq12d ⊢ ( 𝑙 = 𝑗 → ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) = ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) )
502 501 eleq2d ⊢ ( 𝑙 = 𝑗 → ( 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ↔ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) )
503 497 502 anbi12d ⊢ ( 𝑙 = 𝑗 → ( ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ↔ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) )
504 503 anbi2d ⊢ ( 𝑙 = 𝑗 → ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) ) )
505 oveq1 ⊢ ( 𝑙 = 𝑗 → ( 𝑙 − ( 4 / 3 ) ) = ( 𝑗 − ( 4 / 3 ) ) )
506 505 oveq1d ⊢ ( 𝑙 = 𝑗 → ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) = ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) )
507 506 breq1d ⊢ ( 𝑙 = 𝑗 → ( ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ↔ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) )
508 504 507 imbi12d ⊢ ( 𝑙 = 𝑗 → ( ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ↔ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )
509 eleq1w ⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∈ 𝑇 ↔ 𝑡 ∈ 𝑇 ) )
510 509 anbi2d ⊢ ( 𝑠 = 𝑡 → ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ↔ ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ) )
511 fveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝐽 ‘ 𝑠 ) = ( 𝐽 ‘ 𝑡 ) )
512 511 eleq2d ⊢ ( 𝑠 = 𝑡 → ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ↔ 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ) )
513 eleq1w ⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ↔ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) )
514 512 513 anbi12d ⊢ ( 𝑠 = 𝑡 → ( ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ↔ ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) )
515 510 514 anbi12d ⊢ ( 𝑠 = 𝑡 → ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) ↔ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) ) )
516 fveq2 ⊢ ( 𝑠 = 𝑡 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑠 ) = ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) )
517 516 breq2d ⊢ ( 𝑠 = 𝑡 → ( ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑠 ) ↔ ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) )
518 515 517 imbi12d ⊢ ( 𝑠 = 𝑡 → ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑠 ) ) ↔ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )
519 nfv ⊢ Ⅎ 𝑗 𝑠 ∈ 𝑇
520 2 519 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑠 ∈ 𝑇 )
521 nfcv ⊢ Ⅎ 𝑗 𝑠
522 101 521 nffv ⊢ Ⅎ 𝑗 ( 𝐽 ‘ 𝑠 )
523 522 nfcri ⊢ Ⅎ 𝑗 𝑙 ∈ ( 𝐽 ‘ 𝑠 )
524 nfcv ⊢ Ⅎ 𝑗 𝑙
525 86 524 nffv ⊢ Ⅎ 𝑗 ( 𝐷 ‘ 𝑙 )
526 nfcv ⊢ Ⅎ 𝑗 ( 𝑙 − 1 )
527 86 526 nffv ⊢ Ⅎ 𝑗 ( 𝐷 ‘ ( 𝑙 − 1 ) )
528 525 527 nfdif ⊢ Ⅎ 𝑗 ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) )
529 528 nfcri ⊢ Ⅎ 𝑗 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) )
530 523 529 nfan ⊢ Ⅎ 𝑗 ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) )
531 520 530 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) )
532 nfv ⊢ Ⅎ 𝑡 𝑠 ∈ 𝑇
533 3 532 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑠 ∈ 𝑇 )
534 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
535 6 534 nfcxfr ⊢ Ⅎ 𝑡 𝐽
536 nfcv ⊢ Ⅎ 𝑡 𝑠
537 535 536 nffv ⊢ Ⅎ 𝑡 ( 𝐽 ‘ 𝑠 )
538 537 nfcri ⊢ Ⅎ 𝑡 𝑙 ∈ ( 𝐽 ‘ 𝑠 )
539 nfcv ⊢ Ⅎ 𝑡 𝑙
540 170 539 nffv ⊢ Ⅎ 𝑡 ( 𝐷 ‘ 𝑙 )
541 nfcv ⊢ Ⅎ 𝑡 ( 𝑙 − 1 )
542 170 541 nffv ⊢ Ⅎ 𝑡 ( 𝐷 ‘ ( 𝑙 − 1 ) )
543 540 542 nfdif ⊢ Ⅎ 𝑡 ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) )
544 543 nfcri ⊢ Ⅎ 𝑡 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) )
545 538 544 nfan ⊢ Ⅎ 𝑡 ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) )
546 533 545 nfan ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) )
547 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → 𝑁 ∈ ℕ )
548 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → 𝑇 ∈ V )
549 20 rabex ⊢ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) } ∈ V
550 nfcv ⊢ Ⅎ 𝑡 𝑗
551 170 550 nffv ⊢ Ⅎ 𝑡 ( 𝐷 ‘ 𝑗 )
552 551 nfcri ⊢ Ⅎ 𝑡 𝑠 ∈ ( 𝐷 ‘ 𝑗 )
553 nfcv ⊢ Ⅎ 𝑡 ( 1 ... 𝑁 )
554 552 553 nfrabw ⊢ Ⅎ 𝑡 { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) }
555 eleq1w ⊢ ( 𝑡 = 𝑠 → ( 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ↔ 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) ) )
556 555 rabbidv ⊢ ( 𝑡 = 𝑠 → { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } = { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) } )
557 536 554 556 6 fvmptf ⊢ ( ( 𝑠 ∈ 𝑇 ∧ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) } ∈ V ) → ( 𝐽 ‘ 𝑠 ) = { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) } )
558 549 557 mpan2 ⊢ ( 𝑠 ∈ 𝑇 → ( 𝐽 ‘ 𝑠 ) = { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) } )
559 558 eleq2d ⊢ ( 𝑠 ∈ 𝑇 → ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ↔ 𝑙 ∈ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) } ) )
560 559 biimpa ⊢ ( ( 𝑠 ∈ 𝑇 ∧ 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ) → 𝑙 ∈ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) } )
561 525 nfcri ⊢ Ⅎ 𝑗 𝑠 ∈ ( 𝐷 ‘ 𝑙 )
562 fveq2 ⊢ ( 𝑗 = 𝑙 → ( 𝐷 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑙 ) )
563 562 eleq2d ⊢ ( 𝑗 = 𝑙 → ( 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) ↔ 𝑠 ∈ ( 𝐷 ‘ 𝑙 ) ) )
564 524 84 561 563 elrabf ⊢ ( 𝑙 ∈ { 𝑗 ∈ ( 1 ... 𝑁 ) ∣ 𝑠 ∈ ( 𝐷 ‘ 𝑗 ) } ↔ ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ( 𝐷 ‘ 𝑙 ) ) )
565 560 564 sylib ⊢ ( ( 𝑠 ∈ 𝑇 ∧ 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ) → ( 𝑙 ∈ ( 1 ... 𝑁 ) ∧ 𝑠 ∈ ( 𝐷 ‘ 𝑙 ) ) )
566 565 simpld ⊢ ( ( 𝑠 ∈ 𝑇 ∧ 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ) → 𝑙 ∈ ( 1 ... 𝑁 ) )
567 566 ad2ant2lr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → 𝑙 ∈ ( 1 ... 𝑁 ) )
568 simprr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) )
569 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → 𝐹 : 𝑇 ⟶ ℝ )
570 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → 𝐸 ∈ ℝ+ )
571 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → 𝐸 < ( 1 / 3 ) )
572 384 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
573 simp1ll ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → 𝜑 )
574 nfv ⊢ Ⅎ 𝑗 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 )
575 389 574 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
576 393 breq2d ⊢ ( 𝑗 = 𝑖 → ( 0 ≤ ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) ↔ 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
577 392 576 imbi12d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
578 575 577 15 chvarfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
579 573 578 syld3an1 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
580 simp1ll ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ) → 𝜑 )
581 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
582 5 581 nfcxfr ⊢ Ⅎ 𝑗 𝐵
583 582 227 nffv ⊢ Ⅎ 𝑗 ( 𝐵 ‘ 𝑖 )
584 583 nfcri ⊢ Ⅎ 𝑗 𝑡 ∈ ( 𝐵 ‘ 𝑖 )
585 2 375 584 nf3an ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) )
586 nfv ⊢ Ⅎ 𝑗 ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 )
587 585 586 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
588 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐵 ‘ 𝑗 ) = ( 𝐵 ‘ 𝑖 ) )
589 588 eleq2d ⊢ ( 𝑗 = 𝑖 → ( 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ↔ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ) )
590 379 589 3anbi23d ⊢ ( 𝑗 = 𝑖 → ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) ↔ ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ) ) )
591 393 breq2d ⊢ ( 𝑗 = 𝑖 → ( ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) ↔ ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
592 590 591 imbi12d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑗 ) ‘ 𝑡 ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
593 587 592 18 chvarfv ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
594 580 593 syld3an1 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
595 1 531 546 4 5 547 548 567 568 569 570 571 572 579 594 stoweidlem26 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑠 ) ∧ 𝑠 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑠 ) )
596 518 595 vtoclg ⊢ ( 𝑡 ∈ 𝑇 → ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) )
597 596 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) )
598 597 pm2.43i ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑙 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑙 ) ∖ ( 𝐷 ‘ ( 𝑙 − 1 ) ) ) ) ) → ( ( 𝑙 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) )
599 508 598 vtoclg ⊢ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) → ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) )
600 599 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) )
601 600 pm2.43i ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) )
602 496 601 jca ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) )
603 262 371 602 3jca ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) ) → ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )
604 603 ex ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
605 113 604 eximd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ∃ 𝑗 ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ 𝑡 ∈ ( ( 𝐷 ‘ 𝑗 ) ∖ ( 𝐷 ‘ ( 𝑗 − 1 ) ) ) ) → ∃ 𝑗 ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
606 261 605 mpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑗 ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )
607 3anass ⊢ ( ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ↔ ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
608 607 exbii ⊢ ( ∃ 𝑗 ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ↔ ∃ 𝑗 ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
609 606 608 sylib ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑗 ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
610 df-rex ⊢ ( ∃ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ↔ ∃ 𝑗 ( 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ∧ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
611 609 610 sylibr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )
612 nfcv ⊢ Ⅎ 𝑗 ℝ
613 103 612 ssrexf ⊢ ( ( 𝐽 ‘ 𝑡 ) ⊆ ℝ → ( ∃ 𝑗 ∈ ( 𝐽 ‘ 𝑡 ) ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) → ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
614 30 611 613 sylc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )
615 614 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 → ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
616 3 615 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )