Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem60 Structured version   Visualization version   GIF version

Theorem stoweidlem60 44547
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 𝑡 in 𝑇, there is a 𝑗 such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here 𝐹 is used to represent f in the paper, and 𝐸 is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
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
Ref Expression
stoweidlem60 (𝜑 → ∃𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))))
Distinct variable groups:   𝑓,𝑔,𝑗,𝑛,𝑡,𝐴,𝑞,𝑟   𝑦,𝑓,𝑗,𝑛,𝑞,𝑟,𝑡,𝐴   𝐵,𝑓,𝑔   𝐷,𝑓,𝑔   𝑓,𝐸,𝑔,𝑗,𝑛,𝑡   𝑓,𝐽,𝑔,𝑟,𝑡   𝑇,𝑓,𝑔,𝑗,𝑛,𝑡   𝜑,𝑓,𝑔,𝑗,𝑛   𝑔,𝐹,𝑗,𝑛   𝐵,𝑞,𝑟,𝑦   𝐷,𝑞,𝑟,𝑦   𝑇,𝑞,𝑟,𝑦   𝜑,𝑞,𝑟,𝑦   𝐸,𝑟,𝑦   𝑡,𝐾
Allowed substitution hints:   𝜑(𝑡)   𝐵(𝑡,𝑗,𝑛)   𝐶(𝑦,𝑡,𝑓,𝑔,𝑗,𝑛,𝑟,𝑞)   𝐷(𝑡,𝑗,𝑛)   𝐸(𝑞)   𝐹(𝑦,𝑡,𝑓,𝑟,𝑞)   𝐽(𝑦,𝑗,𝑛,𝑞)   𝐾(𝑦,𝑓,𝑔,𝑗,𝑛,𝑟,𝑞)

Proof of Theorem stoweidlem60
Dummy variables 𝑖 𝑥 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnre 12201 . . . . . . . . . . . . 13 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
21adantl 482 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
3 stoweidlem60.17 . . . . . . . . . . . . . 14 (𝜑𝐸 ∈ ℝ+)
43rpred 12998 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ)
54adantr 481 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝐸 ∈ ℝ)
63rpne0d 13003 . . . . . . . . . . . . 13 (𝜑𝐸 ≠ 0)
76adantr 481 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ ℕ) → 𝐸 ≠ 0)
82, 5, 7redivcld 12024 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → (𝑚 / 𝐸) ∈ ℝ)
9 1red 11197 . . . . . . . . . . 11 ((𝜑𝑚 ∈ ℕ) → 1 ∈ ℝ)
108, 9readdcld 11225 . . . . . . . . . 10 ((𝜑𝑚 ∈ ℕ) → ((𝑚 / 𝐸) + 1) ∈ ℝ)
1110adantr 481 . . . . . . . . 9 (((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) → ((𝑚 / 𝐸) + 1) ∈ ℝ)
12 arch 12451 . . . . . . . . 9 (((𝑚 / 𝐸) + 1) ∈ ℝ → ∃𝑛 ∈ ℕ ((𝑚 / 𝐸) + 1) < 𝑛)
1311, 12syl 17 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) → ∃𝑛 ∈ ℕ ((𝑚 / 𝐸) + 1) < 𝑛)
14 stoweidlem60.2 . . . . . . . . . . . . . . 15 𝑡𝜑
15 nfv 1917 . . . . . . . . . . . . . . 15 𝑡 𝑚 ∈ ℕ
1614, 15nfan 1902 . . . . . . . . . . . . . 14 𝑡(𝜑𝑚 ∈ ℕ)
17 nfra1 3280 . . . . . . . . . . . . . 14 𝑡𝑡𝑇 (𝐹𝑡) < 𝑚
1816, 17nfan 1902 . . . . . . . . . . . . 13 𝑡((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚)
19 nfv 1917 . . . . . . . . . . . . 13 𝑡 𝑛 ∈ ℕ
2018, 19nfan 1902 . . . . . . . . . . . 12 𝑡(((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ)
21 nfv 1917 . . . . . . . . . . . 12 𝑡((𝑚 / 𝐸) + 1) < 𝑛
2220, 21nfan 1902 . . . . . . . . . . 11 𝑡((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛)
23 simp-5l 783 . . . . . . . . . . . . . 14 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → 𝜑)
24 stoweidlem60.3 . . . . . . . . . . . . . . . 16 𝐾 = (topGen‘ran (,))
25 stoweidlem60.4 . . . . . . . . . . . . . . . 16 𝑇 = 𝐽
26 stoweidlem60.5 . . . . . . . . . . . . . . . 16 𝐶 = (𝐽 Cn 𝐾)
27 stoweidlem60.15 . . . . . . . . . . . . . . . 16 (𝜑𝐹𝐶)
2824, 25, 26, 27fcnre 43478 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝑇⟶ℝ)
2928ffvelcdmda 7071 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
3023, 29sylancom 588 . . . . . . . . . . . . 13 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
31 simp-5r 784 . . . . . . . . . . . . . 14 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → 𝑚 ∈ ℕ)
3231nnred 12209 . . . . . . . . . . . . 13 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → 𝑚 ∈ ℝ)
33 simpllr 774 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → 𝑛 ∈ ℕ)
3433nnred 12209 . . . . . . . . . . . . . . 15 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → 𝑛 ∈ ℝ)
35 1red 11197 . . . . . . . . . . . . . . 15 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → 1 ∈ ℝ)
3634, 35resubcld 11624 . . . . . . . . . . . . . 14 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → (𝑛 − 1) ∈ ℝ)
3723, 4syl 17 . . . . . . . . . . . . . 14 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → 𝐸 ∈ ℝ)
3836, 37remulcld 11226 . . . . . . . . . . . . 13 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → ((𝑛 − 1) · 𝐸) ∈ ℝ)
39 simpllr 774 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → ∀𝑡𝑇 (𝐹𝑡) < 𝑚)
4039r19.21bi 3247 . . . . . . . . . . . . 13 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → (𝐹𝑡) < 𝑚)
41 simplr 767 . . . . . . . . . . . . . 14 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → ((𝑚 / 𝐸) + 1) < 𝑛)
42 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → ((𝑚 / 𝐸) + 1) < 𝑛)
43 simpl1 1191 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → 𝜑)
44 simpl2 1192 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → 𝑚 ∈ ℕ)
4543, 44, 8syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → (𝑚 / 𝐸) ∈ ℝ)
46 1red 11197 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → 1 ∈ ℝ)
47 simpl3 1193 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → 𝑛 ∈ ℕ)
4847nnred 12209 . . . . . . . . . . . . . . . . 17 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → 𝑛 ∈ ℝ)
4945, 46, 48ltaddsubd 11796 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → (((𝑚 / 𝐸) + 1) < 𝑛 ↔ (𝑚 / 𝐸) < (𝑛 − 1)))
5042, 49mpbid 231 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → (𝑚 / 𝐸) < (𝑛 − 1))
5113ad2ant2 1134 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) → 𝑚 ∈ ℝ)
5251adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → 𝑚 ∈ ℝ)
5348, 46resubcld 11624 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → (𝑛 − 1) ∈ ℝ)
5443ad2ant1 1133 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) → 𝐸 ∈ ℝ)
5554adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → 𝐸 ∈ ℝ)
563rpgt0d 13001 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < 𝐸)
5743, 56syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → 0 < 𝐸)
58 ltdivmul2 12073 . . . . . . . . . . . . . . . 16 ((𝑚 ∈ ℝ ∧ (𝑛 − 1) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑚 / 𝐸) < (𝑛 − 1) ↔ 𝑚 < ((𝑛 − 1) · 𝐸)))
5952, 53, 55, 57, 58syl112anc 1374 . . . . . . . . . . . . . . 15 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → ((𝑚 / 𝐸) < (𝑛 − 1) ↔ 𝑚 < ((𝑛 − 1) · 𝐸)))
6050, 59mpbid 231 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → 𝑚 < ((𝑛 − 1) · 𝐸))
6123, 31, 33, 41, 60syl31anc 1373 . . . . . . . . . . . . 13 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → 𝑚 < ((𝑛 − 1) · 𝐸))
6230, 32, 38, 40, 61lttrd 11357 . . . . . . . . . . . 12 ((((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) ∧ 𝑡𝑇) → (𝐹𝑡) < ((𝑛 − 1) · 𝐸))
6362ex 413 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → (𝑡𝑇 → (𝐹𝑡) < ((𝑛 − 1) · 𝐸)))
6422, 63ralrimi 3253 . . . . . . . . . 10 (((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) ∧ ((𝑚 / 𝐸) + 1) < 𝑛) → ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸))
6564ex 413 . . . . . . . . 9 ((((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) ∧ 𝑛 ∈ ℕ) → (((𝑚 / 𝐸) + 1) < 𝑛 → ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)))
6665reximdva 3167 . . . . . . . 8 (((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) → (∃𝑛 ∈ ℕ ((𝑚 / 𝐸) + 1) < 𝑛 → ∃𝑛 ∈ ℕ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)))
6713, 66mpd 15 . . . . . . 7 (((𝜑𝑚 ∈ ℕ) ∧ ∀𝑡𝑇 (𝐹𝑡) < 𝑚) → ∃𝑛 ∈ ℕ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸))
68 stoweidlem60.1 . . . . . . . 8 𝑡𝐹
69 stoweidlem60.8 . . . . . . . 8 (𝜑𝐽 ∈ Comp)
70 stoweidlem60.9 . . . . . . . 8 (𝜑𝑇 ≠ ∅)
7168, 14, 24, 69, 25, 70, 26, 27rfcnnnub 43489 . . . . . . 7 (𝜑 → ∃𝑚 ∈ ℕ ∀𝑡𝑇 (𝐹𝑡) < 𝑚)
7267, 71r19.29a 3161 . . . . . 6 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸))
73 df-rex 3070 . . . . . 6 (∃𝑛 ∈ ℕ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸) ↔ ∃𝑛(𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)))
7472, 73sylib 217 . . . . 5 (𝜑 → ∃𝑛(𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)))
75 simpr 485 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸))) → (𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)))
7614, 19nfan 1902 . . . . . . . . . . 11 𝑡(𝜑𝑛 ∈ ℕ)
77 stoweidlem60.6 . . . . . . . . . . 11 𝐷 = (𝑗 ∈ (0...𝑛) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
78 stoweidlem60.7 . . . . . . . . . . 11 𝐵 = (𝑗 ∈ (0...𝑛) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
79 eqid 2731 . . . . . . . . . . 11 {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} = {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
80 eqid 2731 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑛) ↦ {𝑦 ∈ {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < (𝑦𝑡))}) = (𝑗 ∈ (0...𝑛) ↦ {𝑦 ∈ {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < (𝑦𝑡))})
8169adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐽 ∈ Comp)
82 stoweidlem60.10 . . . . . . . . . . . 12 (𝜑𝐴𝐶)
8382adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐴𝐶)
84 stoweidlem60.11 . . . . . . . . . . . 12 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
85843adant1r 1177 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
86 stoweidlem60.12 . . . . . . . . . . . 12 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
87863adant1r 1177 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
88 stoweidlem60.13 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
8988adantlr 713 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
90 stoweidlem60.14 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
9190adantlr 713 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
9227adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐹𝐶)
933adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐸 ∈ ℝ+)
94 stoweidlem60.18 . . . . . . . . . . . 12 (𝜑𝐸 < (1 / 3))
9594adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝐸 < (1 / 3))
96 simpr 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
9768, 76, 24, 25, 26, 77, 78, 79, 80, 81, 83, 85, 87, 89, 91, 92, 93, 95, 96stoweidlem59 44546 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ∃𝑥(𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))))
9897adantrr 715 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸))) → ∃𝑥(𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))))
99 19.42v 1957 . . . . . . . . 9 (∃𝑥((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ (𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ↔ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ ∃𝑥(𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))))
10075, 98, 99sylanbrc 583 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸))) → ∃𝑥((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ (𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))))
101 3anass 1095 . . . . . . . . 9 (((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))) ↔ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ (𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))))
102101exbii 1850 . . . . . . . 8 (∃𝑥((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))) ↔ ∃𝑥((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ (𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))))
103100, 102sylibr 233 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸))) → ∃𝑥((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))))
104103ex 413 . . . . . 6 (𝜑 → ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) → ∃𝑥((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))))
105104eximdv 1920 . . . . 5 (𝜑 → (∃𝑛(𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) → ∃𝑛𝑥((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))))
10674, 105mpd 15 . . . 4 (𝜑 → ∃𝑛𝑥((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))))
107 simpl 483 . . . . . . . 8 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → 𝜑)
108 simpr1l 1230 . . . . . . . 8 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → 𝑛 ∈ ℕ)
109 simpr2 1195 . . . . . . . 8 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → 𝑥:(0...𝑛)⟶𝐴)
110 nfv 1917 . . . . . . . . . 10 𝑡 𝑥:(0...𝑛)⟶𝐴
11114, 19, 110nf3an 1904 . . . . . . . . 9 𝑡(𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴)
112 simp2 1137 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴) → 𝑛 ∈ ℕ)
113 simp3 1138 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴) → 𝑥:(0...𝑛)⟶𝐴)
114 simp1 1136 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴) → 𝜑)
115114, 84syl3an1 1163 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
116114, 86syl3an1 1163 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
117883ad2antl1 1185 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴) ∧ 𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
11833ad2ant1 1133 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴) → 𝐸 ∈ ℝ+)
119118rpred 12998 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴) → 𝐸 ∈ ℝ)
12082sselda 3978 . . . . . . . . . . 11 ((𝜑𝑓𝐴) → 𝑓𝐶)
12124, 25, 26, 120fcnre 43478 . . . . . . . . . 10 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
1221213ad2antl1 1185 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴) ∧ 𝑓𝐴) → 𝑓:𝑇⟶ℝ)
123111, 112, 113, 115, 116, 117, 119, 122stoweidlem17 44504 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ ∧ 𝑥:(0...𝑛)⟶𝐴) → (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡))) ∈ 𝐴)
124107, 108, 109, 123syl3anc 1371 . . . . . . 7 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡))) ∈ 𝐴)
125 nfv 1917 . . . . . . . . 9 𝑗𝜑
126 nfv 1917 . . . . . . . . . 10 𝑗(𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸))
127 nfv 1917 . . . . . . . . . 10 𝑗 𝑥:(0...𝑛)⟶𝐴
128 nfra1 3280 . . . . . . . . . 10 𝑗𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))
129126, 127, 128nf3an 1904 . . . . . . . . 9 𝑗((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))
130125, 129nfan 1902 . . . . . . . 8 𝑗(𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))))
131 nfra1 3280 . . . . . . . . . . 11 𝑡𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)
13219, 131nfan 1902 . . . . . . . . . 10 𝑡(𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸))
133 nfcv 2902 . . . . . . . . . . 11 𝑡(0...𝑛)
134 nfra1 3280 . . . . . . . . . . . 12 𝑡𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1)
135 nfra1 3280 . . . . . . . . . . . 12 𝑡𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛)
136 nfra1 3280 . . . . . . . . . . . 12 𝑡𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)
137134, 135, 136nf3an 1904 . . . . . . . . . . 11 𝑡(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))
138133, 137nfralw 3307 . . . . . . . . . 10 𝑡𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))
139132, 110, 138nf3an 1904 . . . . . . . . 9 𝑡((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))
14014, 139nfan 1902 . . . . . . . 8 𝑡(𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))))
141 eqid 2731 . . . . . . . 8 (𝑡𝑇 ↦ {𝑗 ∈ (1...𝑛) ∣ 𝑡 ∈ (𝐷𝑗)}) = (𝑡𝑇 ↦ {𝑗 ∈ (1...𝑛) ∣ 𝑡 ∈ (𝐷𝑗)})
14269uniexd 7715 . . . . . . . . . 10 (𝜑 𝐽 ∈ V)
14325, 142eqeltrid 2836 . . . . . . . . 9 (𝜑𝑇 ∈ V)
144143adantr 481 . . . . . . . 8 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → 𝑇 ∈ V)
14528adantr 481 . . . . . . . 8 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → 𝐹:𝑇⟶ℝ)
146 stoweidlem60.16 . . . . . . . . . 10 (𝜑 → ∀𝑡𝑇 0 ≤ (𝐹𝑡))
147146r19.21bi 3247 . . . . . . . . 9 ((𝜑𝑡𝑇) → 0 ≤ (𝐹𝑡))
148147adantlr 713 . . . . . . . 8 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑡𝑇) → 0 ≤ (𝐹𝑡))
149 simpr1r 1231 . . . . . . . . 9 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸))
150149r19.21bi 3247 . . . . . . . 8 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑡𝑇) → (𝐹𝑡) < ((𝑛 − 1) · 𝐸))
1513adantr 481 . . . . . . . 8 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → 𝐸 ∈ ℝ+)
15294adantr 481 . . . . . . . 8 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → 𝐸 < (1 / 3))
153 simpll 765 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛)) → 𝜑)
154 simplr2 1216 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛)) → 𝑥:(0...𝑛)⟶𝐴)
155 simpr 485 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛)) → 𝑗 ∈ (0...𝑛))
156 simp1 1136 . . . . . . . . . 10 ((𝜑𝑥:(0...𝑛)⟶𝐴𝑗 ∈ (0...𝑛)) → 𝜑)
157 ffvelcdm 7068 . . . . . . . . . . 11 ((𝑥:(0...𝑛)⟶𝐴𝑗 ∈ (0...𝑛)) → (𝑥𝑗) ∈ 𝐴)
1581573adant1 1130 . . . . . . . . . 10 ((𝜑𝑥:(0...𝑛)⟶𝐴𝑗 ∈ (0...𝑛)) → (𝑥𝑗) ∈ 𝐴)
15982sselda 3978 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑗) ∈ 𝐴) → (𝑥𝑗) ∈ 𝐶)
16024, 25, 26, 159fcnre 43478 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑗) ∈ 𝐴) → (𝑥𝑗):𝑇⟶ℝ)
161156, 158, 160syl2anc 584 . . . . . . . . 9 ((𝜑𝑥:(0...𝑛)⟶𝐴𝑗 ∈ (0...𝑛)) → (𝑥𝑗):𝑇⟶ℝ)
162153, 154, 155, 161syl3anc 1371 . . . . . . . 8 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛)) → (𝑥𝑗):𝑇⟶ℝ)
163 simp1r3 1271 . . . . . . . . . 10 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡𝑇) → ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))
164 r19.26-3 3111 . . . . . . . . . . 11 (∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)) ↔ (∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑗 ∈ (0...𝑛)∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑗 ∈ (0...𝑛)∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))
165164simp1bi 1145 . . . . . . . . . 10 (∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)) → ∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1))
166 simpl 483 . . . . . . . . . . 11 ((0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) → 0 ≤ ((𝑥𝑗)‘𝑡))
1671662ralimi 3122 . . . . . . . . . 10 (∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) → ∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 0 ≤ ((𝑥𝑗)‘𝑡))
168163, 165, 1673syl 18 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡𝑇) → ∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 0 ≤ ((𝑥𝑗)‘𝑡))
169 simp2 1137 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡𝑇) → 𝑗 ∈ (0...𝑛))
170 simp3 1138 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡𝑇) → 𝑡𝑇)
171 rspa 3244 . . . . . . . . . 10 ((∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 0 ≤ ((𝑥𝑗)‘𝑡) ∧ 𝑗 ∈ (0...𝑛)) → ∀𝑡𝑇 0 ≤ ((𝑥𝑗)‘𝑡))
172171r19.21bi 3247 . . . . . . . . 9 (((∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 0 ≤ ((𝑥𝑗)‘𝑡) ∧ 𝑗 ∈ (0...𝑛)) ∧ 𝑡𝑇) → 0 ≤ ((𝑥𝑗)‘𝑡))
173168, 169, 170, 172syl21anc 836 . . . . . . . 8 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡𝑇) → 0 ≤ ((𝑥𝑗)‘𝑡))
174 simpr 485 . . . . . . . . . . 11 ((0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) → ((𝑥𝑗)‘𝑡) ≤ 1)
1751742ralimi 3122 . . . . . . . . . 10 (∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) → ∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 ((𝑥𝑗)‘𝑡) ≤ 1)
176163, 165, 1753syl 18 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡𝑇) → ∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 ((𝑥𝑗)‘𝑡) ≤ 1)
177 rspa 3244 . . . . . . . . . 10 ((∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 ((𝑥𝑗)‘𝑡) ≤ 1 ∧ 𝑗 ∈ (0...𝑛)) → ∀𝑡𝑇 ((𝑥𝑗)‘𝑡) ≤ 1)
178177r19.21bi 3247 . . . . . . . . 9 (((∀𝑗 ∈ (0...𝑛)∀𝑡𝑇 ((𝑥𝑗)‘𝑡) ≤ 1 ∧ 𝑗 ∈ (0...𝑛)) ∧ 𝑡𝑇) → ((𝑥𝑗)‘𝑡) ≤ 1)
179176, 169, 170, 178syl21anc 836 . . . . . . . 8 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡𝑇) → ((𝑥𝑗)‘𝑡) ≤ 1)
180 simp1r3 1271 . . . . . . . . . 10 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡 ∈ (𝐷𝑗)) → ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))
181164simp2bi 1146 . . . . . . . . . 10 (∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)) → ∀𝑗 ∈ (0...𝑛)∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛))
182180, 181syl 17 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡 ∈ (𝐷𝑗)) → ∀𝑗 ∈ (0...𝑛)∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛))
183 simp2 1137 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑗 ∈ (0...𝑛))
184 simp3 1138 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ (𝐷𝑗))
185 rspa 3244 . . . . . . . . . 10 ((∀𝑗 ∈ (0...𝑛)∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ 𝑗 ∈ (0...𝑛)) → ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛))
186185r19.21bi 3247 . . . . . . . . 9 (((∀𝑗 ∈ (0...𝑛)∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ 𝑗 ∈ (0...𝑛)) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛))
187182, 183, 184, 186syl21anc 836 . . . . . . . 8 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛))
188 simp1r3 1271 . . . . . . . . . 10 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡 ∈ (𝐵𝑗)) → ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))
189164simp3bi 1147 . . . . . . . . . 10 (∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)) → ∀𝑗 ∈ (0...𝑛)∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))
190188, 189syl 17 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡 ∈ (𝐵𝑗)) → ∀𝑗 ∈ (0...𝑛)∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))
191 simp2 1137 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑗 ∈ (0...𝑛))
192 simp3 1138 . . . . . . . . 9 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑡 ∈ (𝐵𝑗))
193 rspa 3244 . . . . . . . . . 10 ((∀𝑗 ∈ (0...𝑛)∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡) ∧ 𝑗 ∈ (0...𝑛)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))
194193r19.21bi 3247 . . . . . . . . 9 (((∀𝑗 ∈ (0...𝑛)∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡) ∧ 𝑗 ∈ (0...𝑛)) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))
195190, 191, 192, 194syl21anc 836 . . . . . . . 8 (((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))
19668, 130, 140, 77, 78, 141, 108, 144, 145, 148, 150, 151, 152, 162, 173, 179, 187, 195stoweidlem34 44521 . . . . . . 7 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → ∀𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡))))
197 nfmpt1 5249 . . . . . . . . . 10 𝑡(𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))
198197nfeq2 2919 . . . . . . . . 9 𝑡 𝑔 = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))
199 fveq1 6877 . . . . . . . . . . . . 13 (𝑔 = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡))) → (𝑔𝑡) = ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡))
200199breq1d 5151 . . . . . . . . . . . 12 (𝑔 = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡))) → ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ↔ ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸)))
201199breq2d 5153 . . . . . . . . . . . 12 (𝑔 = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡) ↔ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡)))
202200, 201anbi12d 631 . . . . . . . . . . 11 (𝑔 = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡))) → (((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡)) ↔ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡))))
203202anbi2d 629 . . . . . . . . . 10 (𝑔 = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡))) → (((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))) ↔ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡)))))
204203rexbidv 3177 . . . . . . . . 9 (𝑔 = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡))) → (∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))) ↔ ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡)))))
205198, 204ralbid 3269 . . . . . . . 8 (𝑔 = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡))) → (∀𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))) ↔ ∀𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡)))))
206205rspcev 3609 . . . . . . 7 (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡))) ∈ 𝐴 ∧ ∀𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑥𝑖)‘𝑡)))‘𝑡)))) → ∃𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))))
207124, 196, 206syl2anc 584 . . . . . 6 ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡)))) → ∃𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))))
208207ex 413 . . . . 5 (𝜑 → (((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))) → ∃𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡)))))
2092082eximdv 1922 . . . 4 (𝜑 → (∃𝑛𝑥((𝑛 ∈ ℕ ∧ ∀𝑡𝑇 (𝐹𝑡) < ((𝑛 − 1) · 𝐸)) ∧ 𝑥:(0...𝑛)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑛)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑛) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑛)) < ((𝑥𝑗)‘𝑡))) → ∃𝑛𝑥𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡)))))
210106, 209mpd 15 . . 3 (𝜑 → ∃𝑛𝑥𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))))
211 idd 24 . . . 4 (𝜑 → (∃𝑥𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))) → ∃𝑥𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡)))))
212211exlimdv 1936 . . 3 (𝜑 → (∃𝑛𝑥𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))) → ∃𝑥𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡)))))
213210, 212mpd 15 . 2 (𝜑 → ∃𝑥𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))))
214 idd 24 . . 3 (𝜑 → (∃𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))) → ∃𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡)))))
215214exlimdv 1936 . 2 (𝜑 → (∃𝑥𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))) → ∃𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡)))))
216213, 215mpd 15 1 (𝜑 → ∃𝑔𝐴𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ ((𝑔𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < (𝑔𝑡))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wnf 1785  wcel 2106  wnfc 2882  wne 2939  wral 3060  wrex 3069  {crab 3431  Vcvv 3473  wss 3944  c0 4318   cuni 4901   class class class wbr 5141  cmpt 5224  ran crn 5670  wf 6528  cfv 6532  (class class class)co 7393  cr 11091  0cc0 11092  1c1 11093   + caddc 11095   · cmul 11097   < clt 11230  cle 11231  cmin 11426   / cdiv 11853  cn 12194  3c3 12250  4c4 12251  +crp 12956  (,)cioo 13306  ...cfz 13466  Σcsu 15614  topGenctg 17365   Cn ccn 22657  Compccmp 22819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-inf2 9618  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169  ax-pre-sup 11170  ax-mulf 11172
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-tp 4627  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-isom 6541  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-of 7653  df-om 7839  df-1st 7957  df-2nd 7958  df-supp 8129  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-2o 8449  df-er 8686  df-map 8805  df-pm 8806  df-ixp 8875  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-fsupp 9345  df-fi 9388  df-sup 9419  df-inf 9420  df-oi 9487  df-card 9916  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-div 11854  df-nn 12195  df-2 12257  df-3 12258  df-4 12259  df-5 12260  df-6 12261  df-7 12262  df-8 12263  df-9 12264  df-n0 12455  df-z 12541  df-dec 12660  df-uz 12805  df-q 12915  df-rp 12957  df-xneg 13074  df-xadd 13075  df-xmul 13076  df-ioo 13310  df-ioc 13311  df-ico 13312  df-icc 13313  df-fz 13467  df-fzo 13610  df-fl 13739  df-seq 13949  df-exp 14010  df-hash 14273  df-cj 15028  df-re 15029  df-im 15030  df-sqrt 15164  df-abs 15165  df-clim 15414  df-rlim 15415  df-sum 15615  df-struct 17062  df-sets 17079  df-slot 17097  df-ndx 17109  df-base 17127  df-ress 17156  df-plusg 17192  df-mulr 17193  df-starv 17194  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ds 17201  df-unif 17202  df-hom 17203  df-cco 17204  df-rest 17350  df-topn 17351  df-0g 17369  df-gsum 17370  df-topgen 17371  df-pt 17372  df-prds 17375  df-xrs 17430  df-qtop 17435  df-imas 17436  df-xps 17438  df-mre 17512  df-mrc 17513  df-acs 17515  df-mgm 18543  df-sgrp 18592  df-mnd 18603  df-submnd 18648  df-mulg 18923  df-cntz 19147  df-cmn 19614  df-psmet 20870  df-xmet 20871  df-met 20872  df-bl 20873  df-mopn 20874  df-cnfld 20879  df-top 22325  df-topon 22342  df-topsp 22364  df-bases 22378  df-cld 22452  df-cn 22660  df-cnp 22661  df-cmp 22820  df-tx 22995  df-hmeo 23188  df-xms 23755  df-ms 23756  df-tms 23757
This theorem is referenced by:  stoweidlem61  44548
  Copyright terms: Public domain W3C validator