Metamath Proof Explorer

Theorem stoweidlem60

Description: This lemma proves that there exists a function g as in the proof in BrosowskiDeutsh p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all t in T , there is a j such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here F is used to represent f in the paper, and E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem60.1 ⊢ Ⅎ 𝑡 𝐹
stoweidlem60.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem60.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
stoweidlem60.4 ⊢ 𝑇 = ∪ 𝐽
stoweidlem60.5 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
stoweidlem60.6 ⊢ 𝐷 = ( 𝑗 ∈ ( 0 ... 𝑛 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
stoweidlem60.7 ⊢ 𝐵 = ( 𝑗 ∈ ( 0 ... 𝑛 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
stoweidlem60.8 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
stoweidlem60.9 ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
stoweidlem60.10 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
stoweidlem60.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem60.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem60.13 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑦 ) ∈ 𝐴 )
stoweidlem60.14 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
stoweidlem60.15 ⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
stoweidlem60.16 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 0 ≤ ( 𝐹 ‘ 𝑡 ) )
stoweidlem60.17 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem60.18 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
Assertion stoweidlem60 ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem60.1 ⊢ Ⅎ 𝑡 𝐹
2 stoweidlem60.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem60.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
4 stoweidlem60.4 ⊢ 𝑇 = ∪ 𝐽
5 stoweidlem60.5 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
6 stoweidlem60.6 ⊢ 𝐷 = ( 𝑗 ∈ ( 0 ... 𝑛 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
7 stoweidlem60.7 ⊢ 𝐵 = ( 𝑗 ∈ ( 0 ... 𝑛 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
8 stoweidlem60.8 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
9 stoweidlem60.9 ⊢ ( 𝜑 → 𝑇 ≠ ∅ )
10 stoweidlem60.10 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
11 stoweidlem60.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
12 stoweidlem60.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
13 stoweidlem60.13 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑦 ) ∈ 𝐴 )
14 stoweidlem60.14 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
15 stoweidlem60.15 ⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
16 stoweidlem60.16 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 0 ≤ ( 𝐹 ‘ 𝑡 ) )
17 stoweidlem60.17 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
18 stoweidlem60.18 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
19 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ )
21 17 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐸 ∈ ℝ )
23 17 rpne0d ⊢ ( 𝜑 → 𝐸 ≠ 0 )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐸 ≠ 0 )
25 20 22 24 redivcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑚 / 𝐸 ) ∈ ℝ )
26 1red ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 1 ∈ ℝ )
27 25 26 readdcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 / 𝐸 ) + 1 ) ∈ ℝ )
28 27 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) → ( ( 𝑚 / 𝐸 ) + 1 ) ∈ ℝ )
29 arch ⊢ ( ( ( 𝑚 / 𝐸 ) + 1 ) ∈ ℝ → ∃ 𝑛 ∈ ℕ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 )
30 28 29 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) → ∃ 𝑛 ∈ ℕ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 )
31 nfv ⊢ Ⅎ 𝑡 𝑚 ∈ ℕ
32 2 31 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑚 ∈ ℕ )
33 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚
34 32 33 nfan ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 )
35 nfv ⊢ Ⅎ 𝑡 𝑛 ∈ ℕ
36 34 35 nfan ⊢ Ⅎ 𝑡 ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ )
37 nfv ⊢ Ⅎ 𝑡 ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛
38 36 37 nfan ⊢ Ⅎ 𝑡 ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 )
39 simp-5l ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 𝜑 )
40 3 4 5 15 fcnre ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
41 40 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
42 39 41 sylancom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
43 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑚 ∈ ℕ )
44 43 nnred ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑚 ∈ ℝ )
45 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑛 ∈ ℕ )
46 45 nnred ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑛 ∈ ℝ )
47 1red ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 1 ∈ ℝ )
48 46 47 resubcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝑛 − 1 ) ∈ ℝ )
49 39 21 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 𝐸 ∈ ℝ )
50 48 49 remulcld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑛 − 1 ) · 𝐸 ) ∈ ℝ )
51 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 )
52 51 r19.21bi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) < 𝑚 )
53 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 )
54 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 )
55 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → 𝜑 )
56 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → 𝑚 ∈ ℕ )
57 55 56 25 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → ( 𝑚 / 𝐸 ) ∈ ℝ )
58 1red ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → 1 ∈ ℝ )
59 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → 𝑛 ∈ ℕ )
60 59 nnred ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → 𝑛 ∈ ℝ )
61 57 58 60 ltaddsubd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → ( ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ↔ ( 𝑚 / 𝐸 ) < ( 𝑛 − 1 ) ) )
62 54 61 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → ( 𝑚 / 𝐸 ) < ( 𝑛 − 1 ) )
63 19 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝑚 ∈ ℝ )
64 63 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → 𝑚 ∈ ℝ )
65 60 58 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → ( 𝑛 − 1 ) ∈ ℝ )
66 21 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → 𝐸 ∈ ℝ )
67 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → 𝐸 ∈ ℝ )
68 17 rpgt0d ⊢ ( 𝜑 → 0 < 𝐸 )
69 55 68 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → 0 < 𝐸 )
70 ltdivmul2 ⊢ ( ( 𝑚 ∈ ℝ ∧ ( 𝑛 − 1 ) ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( ( 𝑚 / 𝐸 ) < ( 𝑛 − 1 ) ↔ 𝑚 < ( ( 𝑛 − 1 ) · 𝐸 ) ) )
71 64 65 67 69 70 syl112anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → ( ( 𝑚 / 𝐸 ) < ( 𝑛 − 1 ) ↔ 𝑚 < ( ( 𝑛 − 1 ) · 𝐸 ) ) )
72 62 71 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → 𝑚 < ( ( 𝑛 − 1 ) · 𝐸 ) )
73 39 43 45 53 72 syl31anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑚 < ( ( 𝑛 − 1 ) · 𝐸 ) )
74 42 44 50 52 73 lttrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) )
75 74 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → ( 𝑡 ∈ 𝑇 → ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) )
76 38 75 ralrimi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) ∧ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 ) → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) )
77 76 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) ∧ 𝑛 ∈ ℕ ) → ( ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) )
78 77 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) → ( ∃ 𝑛 ∈ ℕ ( ( 𝑚 / 𝐸 ) + 1 ) < 𝑛 → ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) )
79 30 78 mpd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) )
80 1 2 3 8 4 9 5 15 rfcnnnub ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < 𝑚 )
81 79 80 r19.29a ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) )
82 df-rex ⊢ ( ∃ 𝑛 ∈ ℕ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ↔ ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) )
83 81 82 sylib ⊢ ( 𝜑 → ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) )
84 simpr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ) → ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) )
85 2 35 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑛 ∈ ℕ )
86 eqid ⊢ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) } = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) }
87 eqid ⊢ ( 𝑗 ∈ ( 0 ... 𝑛 ) ↦ { 𝑦 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) } ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ) = ( 𝑗 ∈ ( 0 ... 𝑛 ) ↦ { 𝑦 ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) } ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( 𝑦 ‘ 𝑡 ) ) } )
88 8 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐽 ∈ Comp )
89 10 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ⊆ 𝐶 )
90 11 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
91 12 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
92 13 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑦 ) ∈ 𝐴 )
93 14 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
94 15 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐹 ∈ 𝐶 )
95 17 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐸 ∈ ℝ+ )
96 18 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐸 < ( 1 / 3 ) )
97 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
98 1 85 3 4 5 6 7 86 87 88 89 90 91 92 93 94 95 96 97 stoweidlem59 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ∃ 𝑥 ( 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
99 98 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ) → ∃ 𝑥 ( 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
100 19.42v ⊢ ( ∃ 𝑥 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ ( 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ↔ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ ∃ 𝑥 ( 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) )
101 84 99 100 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ) → ∃ 𝑥 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ ( 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) )
102 3anass ⊢ ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ↔ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ ( 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) )
103 102 exbii ⊢ ( ∃ 𝑥 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ↔ ∃ 𝑥 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ ( 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) )
104 101 103 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ) → ∃ 𝑥 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
105 104 ex ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) → ∃ 𝑥 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) )
106 105 eximdv ⊢ ( 𝜑 → ( ∃ 𝑛 ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) → ∃ 𝑛 ∃ 𝑥 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) )
107 83 106 mpd ⊢ ( 𝜑 → ∃ 𝑛 ∃ 𝑥 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
108 simpl ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → 𝜑 )
109 simpr1l ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → 𝑛 ∈ ℕ )
110 simpr2 ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 )
111 nfv ⊢ Ⅎ 𝑡 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴
112 2 35 111 nf3an ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 )
113 simp2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ) → 𝑛 ∈ ℕ )
114 simp3 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ) → 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 )
115 simp1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ) → 𝜑 )
116 115 11 syl3an1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
117 115 12 syl3an1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
118 13 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑦 ) ∈ 𝐴 )
119 17 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ) → 𝐸 ∈ ℝ+ )
120 119 rpred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ) → 𝐸 ∈ ℝ )
121 10 sselda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ 𝐶 )
122 3 4 5 121 fcnre ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
123 122 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ) ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
124 112 113 114 116 117 118 120 123 stoweidlem17 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
125 108 109 110 124 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 )
126 nfv ⊢ Ⅎ 𝑗 𝜑
127 nfv ⊢ Ⅎ 𝑗 ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) )
128 nfv ⊢ Ⅎ 𝑗 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴
129 nfra1 ⊢ Ⅎ 𝑗 ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
130 127 128 129 nf3an ⊢ Ⅎ 𝑗 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) )
131 126 130 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
132 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 )
133 35 132 nfan ⊢ Ⅎ 𝑡 ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) )
134 nfcv ⊢ Ⅎ 𝑡 ( 0 ... 𝑛 )
135 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
136 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 )
137 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 )
138 135 136 137 nf3an ⊢ Ⅎ 𝑡 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
139 134 138 nfralw ⊢ Ⅎ 𝑡 ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
140 133 111 139 nf3an ⊢ Ⅎ 𝑡 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) )
141 2 140 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
142 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ { 𝑗 ∈ ( 1 ... 𝑛 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } ) = ( 𝑡 ∈ 𝑇 ↦ { 𝑗 ∈ ( 1 ... 𝑛 ) ∣ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) } )
143 8 uniexd ⊢ ( 𝜑 → ∪ 𝐽 ∈ V )
144 4 143 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ V )
145 144 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → 𝑇 ∈ V )
146 40 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → 𝐹 : 𝑇 ⟶ ℝ )
147 16 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝐹 ‘ 𝑡 ) )
148 147 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝐹 ‘ 𝑡 ) )
149 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) )
150 149 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) )
151 17 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → 𝐸 ∈ ℝ+ )
152 18 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → 𝐸 < ( 1 / 3 ) )
153 simpll ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → 𝜑 )
154 simplr2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 )
155 simpr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → 𝑗 ∈ ( 0 ... 𝑛 ) )
156 simp1 ⊢ ( ( 𝜑 ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → 𝜑 )
157 ffvelrn ⊢ ( ( 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → ( 𝑥 ‘ 𝑗 ) ∈ 𝐴 )
158 157 3adant1 ⊢ ( ( 𝜑 ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → ( 𝑥 ‘ 𝑗 ) ∈ 𝐴 )
159 10 sselda ⊢ ( ( 𝜑 ∧ ( 𝑥 ‘ 𝑗 ) ∈ 𝐴 ) → ( 𝑥 ‘ 𝑗 ) ∈ 𝐶 )
160 3 4 5 159 fcnre ⊢ ( ( 𝜑 ∧ ( 𝑥 ‘ 𝑗 ) ∈ 𝐴 ) → ( 𝑥 ‘ 𝑗 ) : 𝑇 ⟶ ℝ )
161 156 158 160 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → ( 𝑥 ‘ 𝑗 ) : 𝑇 ⟶ ℝ )
162 153 154 155 161 syl3anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → ( 𝑥 ‘ 𝑗 ) : 𝑇 ⟶ ℝ )
163 simp1r3 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) )
164 r19.26-3 ⊢ ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ↔ ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) )
165 164 simp1bi ⊢ ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) )
166 simpl ⊢ ( ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) → 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
167 166 2ralimi ⊢ ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
168 163 165 167 3syl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
169 simp2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑗 ∈ ( 0 ... 𝑛 ) )
170 simp3 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑇 )
171 rspa ⊢ ( ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → ∀ 𝑡 ∈ 𝑇 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
172 171 r19.21bi ⊢ ( ( ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
173 168 169 170 172 syl21anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
174 simpr ⊢ ( ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) → ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
175 174 2ralimi ⊢ ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
176 163 165 175 3syl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
177 rspa ⊢ ( ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → ∀ 𝑡 ∈ 𝑇 ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
178 177 r19.21bi ⊢ ( ( ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ 𝑇 ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
179 176 169 170 178 syl21anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
180 simp1r3 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) )
181 164 simp2bi ⊢ ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) )
182 180 181 syl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) )
183 simp2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → 𝑗 ∈ ( 0 ... 𝑛 ) )
184 simp3 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
185 rspa ⊢ ( ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) )
186 185 r19.21bi ⊢ ( ( ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) )
187 182 183 184 186 syl21anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) → ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) )
188 simp1r3 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) )
189 164 simp3bi ⊢ ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
190 188 189 syl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
191 simp2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → 𝑗 ∈ ( 0 ... 𝑛 ) )
192 simp3 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) )
193 rspa ⊢ ( ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) → ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
194 193 r19.21bi ⊢ ( ( ( ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
195 190 191 192 194 syl21anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑛 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) )
196 1 131 141 6 7 142 109 145 146 148 150 151 152 162 173 179 187 195 stoweidlem34 ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )
197 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) )
198 197 nfeq2 ⊢ Ⅎ 𝑡 𝑔 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) )
199 fveq1 ⊢ ( 𝑔 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ( 𝑔 ‘ 𝑡 ) = ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) )
200 199 breq1d ⊢ ( 𝑔 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ↔ ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ) )
201 199 breq2d ⊢ ( 𝑔 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ↔ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) )
202 200 201 anbi12d ⊢ ( 𝑔 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ( ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ↔ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) )
203 202 anbi2d ⊢ ( 𝑔 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ( ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ↔ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
204 203 rexbidv ⊢ ( 𝑔 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ( ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ↔ ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
205 198 204 ralbid ⊢ ( 𝑔 = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ( ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ↔ ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) )
206 205 rspcev ⊢ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( 𝐸 · ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) ) ) ) → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) )
207 125 196 206 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) )
208 207 ex ⊢ ( 𝜑 → ( ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) )
209 208 2eximdv ⊢ ( 𝜑 → ( ∃ 𝑛 ∃ 𝑥 ( ( 𝑛 ∈ ℕ ∧ ∀ 𝑡 ∈ 𝑇 ( 𝐹 ‘ 𝑡 ) < ( ( 𝑛 − 1 ) · 𝐸 ) ) ∧ 𝑥 : ( 0 ... 𝑛 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑛 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑛 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑛 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ∃ 𝑛 ∃ 𝑥 ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) )
210 107 209 mpd ⊢ ( 𝜑 → ∃ 𝑛 ∃ 𝑥 ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) )
211 idd ⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) → ∃ 𝑥 ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) )
212 211 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑛 ∃ 𝑥 ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) → ∃ 𝑥 ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) )
213 210 212 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) )
214 idd ⊢ ( 𝜑 → ( ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) )
215 214 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) ) )
216 213 215 mpd ⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ∀ 𝑡 ∈ 𝑇 ∃ 𝑗 ∈ ℝ ( ( ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) ∧ ( ( 𝑔 ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∧ ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝑔 ‘ 𝑡 ) ) ) )