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 45261
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 12216 . . . . . . . . . . . . 13 (π‘š ∈ β„• β†’ π‘š ∈ ℝ)
21adantl 481 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•) β†’ π‘š ∈ ℝ)
3 stoweidlem60.17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐸 ∈ ℝ+)
43rpred 13013 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐸 ∈ ℝ)
54adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 𝐸 ∈ ℝ)
63rpne0d 13018 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐸 β‰  0)
76adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 𝐸 β‰  0)
82, 5, 7redivcld 12039 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•) β†’ (π‘š / 𝐸) ∈ ℝ)
9 1red 11212 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ β„•) β†’ 1 ∈ ℝ)
108, 9readdcld 11240 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ β„•) β†’ ((π‘š / 𝐸) + 1) ∈ ℝ)
1110adantr 480 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) β†’ ((π‘š / 𝐸) + 1) ∈ ℝ)
12 arch 12466 . . . . . . . . 9 (((π‘š / 𝐸) + 1) ∈ ℝ β†’ βˆƒπ‘› ∈ β„• ((π‘š / 𝐸) + 1) < 𝑛)
1311, 12syl 17 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) β†’ βˆƒπ‘› ∈ β„• ((π‘š / 𝐸) + 1) < 𝑛)
14 stoweidlem60.2 . . . . . . . . . . . . . . 15 β„²π‘‘πœ‘
15 nfv 1909 . . . . . . . . . . . . . . 15 Ⅎ𝑑 π‘š ∈ β„•
1614, 15nfan 1894 . . . . . . . . . . . . . 14 Ⅎ𝑑(πœ‘ ∧ π‘š ∈ β„•)
17 nfra1 3273 . . . . . . . . . . . . . 14 β„²π‘‘βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š
1816, 17nfan 1894 . . . . . . . . . . . . 13 Ⅎ𝑑((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š)
19 nfv 1909 . . . . . . . . . . . . 13 Ⅎ𝑑 𝑛 ∈ β„•
2018, 19nfan 1894 . . . . . . . . . . . 12 Ⅎ𝑑(((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•)
21 nfv 1909 . . . . . . . . . . . 12 Ⅎ𝑑((π‘š / 𝐸) + 1) < 𝑛
2220, 21nfan 1894 . . . . . . . . . . 11 Ⅎ𝑑((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛)
23 simp-5l 782 . . . . . . . . . . . . . 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 44198 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹:π‘‡βŸΆβ„)
2928ffvelcdmda 7076 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (πΉβ€˜π‘‘) ∈ ℝ)
3023, 29sylancom 587 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ (πΉβ€˜π‘‘) ∈ ℝ)
31 simp-5r 783 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ π‘š ∈ β„•)
3231nnred 12224 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ π‘š ∈ ℝ)
33 simpllr 773 . . . . . . . . . . . . . . . 16 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ 𝑛 ∈ β„•)
3433nnred 12224 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ 𝑛 ∈ ℝ)
35 1red 11212 . . . . . . . . . . . . . . 15 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ 1 ∈ ℝ)
3634, 35resubcld 11639 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ (𝑛 βˆ’ 1) ∈ ℝ)
3723, 4syl 17 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ 𝐸 ∈ ℝ)
3836, 37remulcld 11241 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ ((𝑛 βˆ’ 1) Β· 𝐸) ∈ ℝ)
39 simpllr 773 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š)
4039r19.21bi 3240 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ (πΉβ€˜π‘‘) < π‘š)
41 simplr 766 . . . . . . . . . . . . . 14 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘š / 𝐸) + 1) < 𝑛)
42 simpr 484 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ ((π‘š / 𝐸) + 1) < 𝑛)
43 simpl1 1188 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ πœ‘)
44 simpl2 1189 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ π‘š ∈ β„•)
4543, 44, 8syl2anc 583 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ (π‘š / 𝐸) ∈ ℝ)
46 1red 11212 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ 1 ∈ ℝ)
47 simpl3 1190 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ 𝑛 ∈ β„•)
4847nnred 12224 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ 𝑛 ∈ ℝ)
4945, 46, 48ltaddsubd 11811 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ (((π‘š / 𝐸) + 1) < 𝑛 ↔ (π‘š / 𝐸) < (𝑛 βˆ’ 1)))
5042, 49mpbid 231 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ (π‘š / 𝐸) < (𝑛 βˆ’ 1))
5113ad2ant2 1131 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) β†’ π‘š ∈ ℝ)
5251adantr 480 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ π‘š ∈ ℝ)
5348, 46resubcld 11639 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ (𝑛 βˆ’ 1) ∈ ℝ)
5443ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) β†’ 𝐸 ∈ ℝ)
5554adantr 480 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ 𝐸 ∈ ℝ)
563rpgt0d 13016 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 0 < 𝐸)
5743, 56syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ 0 < 𝐸)
58 ltdivmul2 12088 . . . . . . . . . . . . . . . 16 ((π‘š ∈ ℝ ∧ (𝑛 βˆ’ 1) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ ((π‘š / 𝐸) < (𝑛 βˆ’ 1) ↔ π‘š < ((𝑛 βˆ’ 1) Β· 𝐸)))
5952, 53, 55, 57, 58syl112anc 1371 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ ((π‘š / 𝐸) < (𝑛 βˆ’ 1) ↔ π‘š < ((𝑛 βˆ’ 1) Β· 𝐸)))
6050, 59mpbid 231 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘š ∈ β„• ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ π‘š < ((𝑛 βˆ’ 1) Β· 𝐸))
6123, 31, 33, 41, 60syl31anc 1370 . . . . . . . . . . . . 13 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ π‘š < ((𝑛 βˆ’ 1) Β· 𝐸))
6230, 32, 38, 40, 61lttrd 11372 . . . . . . . . . . . 12 ((((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) ∧ 𝑑 ∈ 𝑇) β†’ (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸))
6362ex 412 . . . . . . . . . . 11 (((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ (𝑑 ∈ 𝑇 β†’ (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)))
6422, 63ralrimi 3246 . . . . . . . . . 10 (((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) ∧ ((π‘š / 𝐸) + 1) < 𝑛) β†’ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸))
6564ex 412 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ β„•) ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š) ∧ 𝑛 ∈ β„•) β†’ (((π‘š / 𝐸) + 1) < 𝑛 β†’ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)))
6665reximdva 3160 . . . . . . . 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 44209 . . . . . . 7 (πœ‘ β†’ βˆƒπ‘š ∈ β„• βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < π‘š)
7267, 71r19.29a 3154 . . . . . 6 (πœ‘ β†’ βˆƒπ‘› ∈ β„• βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸))
73 df-rex 3063 . . . . . 6 (βˆƒπ‘› ∈ β„• βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸) ↔ βˆƒπ‘›(𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)))
7472, 73sylib 217 . . . . 5 (πœ‘ β†’ βˆƒπ‘›(𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)))
75 simpr 484 . . . . . . . . 9 ((πœ‘ ∧ (𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸))) β†’ (𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)))
7614, 19nfan 1894 . . . . . . . . . . 11 Ⅎ𝑑(πœ‘ ∧ 𝑛 ∈ β„•)
77 stoweidlem60.6 . . . . . . . . . . 11 𝐷 = (𝑗 ∈ (0...𝑛) ↦ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)})
78 stoweidlem60.7 . . . . . . . . . . 11 𝐡 = (𝑗 ∈ (0...𝑛) ↦ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
79 eqid 2724 . . . . . . . . . . 11 {𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)} = {𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)}
80 eqid 2724 . . . . . . . . . . 11 (𝑗 ∈ (0...𝑛) ↦ {𝑦 ∈ {𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)} ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < (π‘¦β€˜π‘‘))}) = (𝑗 ∈ (0...𝑛) ↦ {𝑦 ∈ {𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)} ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < (π‘¦β€˜π‘‘))})
8169adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐽 ∈ Comp)
82 stoweidlem60.10 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐴 βŠ† 𝐢)
8382adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† 𝐢)
84 stoweidlem60.11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
85843adant1r 1174 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
86 stoweidlem60.12 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
87863adant1r 1174 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
88 stoweidlem60.13 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
8988adantlr 712 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ 𝑦 ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
90 stoweidlem60.14 . . . . . . . . . . . 12 ((πœ‘ ∧ (π‘Ÿ ∈ 𝑇 ∧ 𝑑 ∈ 𝑇 ∧ π‘Ÿ β‰  𝑑)) β†’ βˆƒπ‘ž ∈ 𝐴 (π‘žβ€˜π‘Ÿ) β‰  (π‘žβ€˜π‘‘))
9190adantlr 712 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ β„•) ∧ (π‘Ÿ ∈ 𝑇 ∧ 𝑑 ∈ 𝑇 ∧ π‘Ÿ β‰  𝑑)) β†’ βˆƒπ‘ž ∈ 𝐴 (π‘žβ€˜π‘Ÿ) β‰  (π‘žβ€˜π‘‘))
9227adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐹 ∈ 𝐢)
933adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐸 ∈ ℝ+)
94 stoweidlem60.18 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐸 < (1 / 3))
9594adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐸 < (1 / 3))
96 simpr 484 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
9768, 76, 24, 25, 26, 77, 78, 79, 80, 81, 83, 85, 87, 89, 91, 92, 93, 95, 96stoweidlem59 45260 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ βˆƒπ‘₯(π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))))
9897adantrr 714 . . . . . . . . 9 ((πœ‘ ∧ (𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸))) β†’ βˆƒπ‘₯(π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))))
99 19.42v 1949 . . . . . . . . 9 (βˆƒπ‘₯((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ (π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ↔ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ βˆƒπ‘₯(π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))))
10075, 98, 99sylanbrc 582 . . . . . . . 8 ((πœ‘ ∧ (𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸))) β†’ βˆƒπ‘₯((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ (π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))))
101 3anass 1092 . . . . . . . . 9 (((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))) ↔ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ (π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))))
102101exbii 1842 . . . . . . . 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 412 . . . . . 6 (πœ‘ β†’ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) β†’ βˆƒπ‘₯((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))))
105104eximdv 1912 . . . . 5 (πœ‘ β†’ (βˆƒπ‘›(𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) β†’ βˆƒπ‘›βˆƒπ‘₯((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))))
10674, 105mpd 15 . . . 4 (πœ‘ β†’ βˆƒπ‘›βˆƒπ‘₯((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))))
107 simpl 482 . . . . . . . 8 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ πœ‘)
108 simpr1l 1227 . . . . . . . 8 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ 𝑛 ∈ β„•)
109 simpr2 1192 . . . . . . . 8 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ π‘₯:(0...𝑛)⟢𝐴)
110 nfv 1909 . . . . . . . . . 10 Ⅎ𝑑 π‘₯:(0...𝑛)⟢𝐴
11114, 19, 110nf3an 1896 . . . . . . . . 9 Ⅎ𝑑(πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴)
112 simp2 1134 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴) β†’ 𝑛 ∈ β„•)
113 simp3 1135 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴) β†’ π‘₯:(0...𝑛)⟢𝐴)
114 simp1 1133 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴) β†’ πœ‘)
115114, 84syl3an1 1160 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
116114, 86syl3an1 1160 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
117883ad2antl1 1182 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴) ∧ 𝑦 ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
11833ad2ant1 1130 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴) β†’ 𝐸 ∈ ℝ+)
119118rpred 13013 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴) β†’ 𝐸 ∈ ℝ)
12082sselda 3974 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓 ∈ 𝐢)
12124, 25, 26, 120fcnre 44198 . . . . . . . . . 10 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
1221213ad2antl1 1182 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴) ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
123111, 112, 113, 115, 116, 117, 119, 122stoweidlem17 45218 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„• ∧ π‘₯:(0...𝑛)⟢𝐴) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
124107, 108, 109, 123syl3anc 1368 . . . . . . 7 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘))) ∈ 𝐴)
125 nfv 1909 . . . . . . . . 9 β„²π‘—πœ‘
126 nfv 1909 . . . . . . . . . 10 Ⅎ𝑗(𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸))
127 nfv 1909 . . . . . . . . . 10 Ⅎ𝑗 π‘₯:(0...𝑛)⟢𝐴
128 nfra1 3273 . . . . . . . . . 10 β„²π‘—βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))
129126, 127, 128nf3an 1896 . . . . . . . . 9 Ⅎ𝑗((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))
130125, 129nfan 1894 . . . . . . . 8 Ⅎ𝑗(πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))))
131 nfra1 3273 . . . . . . . . . . 11 β„²π‘‘βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)
13219, 131nfan 1894 . . . . . . . . . 10 Ⅎ𝑑(𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸))
133 nfcv 2895 . . . . . . . . . . 11 Ⅎ𝑑(0...𝑛)
134 nfra1 3273 . . . . . . . . . . . 12 β„²π‘‘βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1)
135 nfra1 3273 . . . . . . . . . . . 12 β„²π‘‘βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛)
136 nfra1 3273 . . . . . . . . . . . 12 β„²π‘‘βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)
137134, 135, 136nf3an 1896 . . . . . . . . . . 11 Ⅎ𝑑(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))
138133, 137nfralw 3300 . . . . . . . . . 10 β„²π‘‘βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))
139132, 110, 138nf3an 1896 . . . . . . . . 9 Ⅎ𝑑((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))
14014, 139nfan 1894 . . . . . . . 8 Ⅎ𝑑(πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))))
141 eqid 2724 . . . . . . . 8 (𝑑 ∈ 𝑇 ↦ {𝑗 ∈ (1...𝑛) ∣ 𝑑 ∈ (π·β€˜π‘—)}) = (𝑑 ∈ 𝑇 ↦ {𝑗 ∈ (1...𝑛) ∣ 𝑑 ∈ (π·β€˜π‘—)})
14269uniexd 7725 . . . . . . . . . 10 (πœ‘ β†’ βˆͺ 𝐽 ∈ V)
14325, 142eqeltrid 2829 . . . . . . . . 9 (πœ‘ β†’ 𝑇 ∈ V)
144143adantr 480 . . . . . . . 8 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ 𝑇 ∈ V)
14528adantr 480 . . . . . . . 8 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ 𝐹:π‘‡βŸΆβ„)
146 stoweidlem60.16 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘‘ ∈ 𝑇 0 ≀ (πΉβ€˜π‘‘))
147146r19.21bi 3240 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 0 ≀ (πΉβ€˜π‘‘))
148147adantlr 712 . . . . . . . 8 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑑 ∈ 𝑇) β†’ 0 ≀ (πΉβ€˜π‘‘))
149 simpr1r 1228 . . . . . . . . 9 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸))
150149r19.21bi 3240 . . . . . . . 8 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑑 ∈ 𝑇) β†’ (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸))
1513adantr 480 . . . . . . . 8 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ 𝐸 ∈ ℝ+)
15294adantr 480 . . . . . . . 8 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ 𝐸 < (1 / 3))
153 simpll 764 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛)) β†’ πœ‘)
154 simplr2 1213 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛)) β†’ π‘₯:(0...𝑛)⟢𝐴)
155 simpr 484 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛)) β†’ 𝑗 ∈ (0...𝑛))
156 simp1 1133 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ 𝑗 ∈ (0...𝑛)) β†’ πœ‘)
157 ffvelcdm 7073 . . . . . . . . . . 11 ((π‘₯:(0...𝑛)⟢𝐴 ∧ 𝑗 ∈ (0...𝑛)) β†’ (π‘₯β€˜π‘—) ∈ 𝐴)
1581573adant1 1127 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ 𝑗 ∈ (0...𝑛)) β†’ (π‘₯β€˜π‘—) ∈ 𝐴)
15982sselda 3974 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯β€˜π‘—) ∈ 𝐴) β†’ (π‘₯β€˜π‘—) ∈ 𝐢)
16024, 25, 26, 159fcnre 44198 . . . . . . . . . 10 ((πœ‘ ∧ (π‘₯β€˜π‘—) ∈ 𝐴) β†’ (π‘₯β€˜π‘—):π‘‡βŸΆβ„)
161156, 158, 160syl2anc 583 . . . . . . . . 9 ((πœ‘ ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ 𝑗 ∈ (0...𝑛)) β†’ (π‘₯β€˜π‘—):π‘‡βŸΆβ„)
162153, 154, 155, 161syl3anc 1368 . . . . . . . 8 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛)) β†’ (π‘₯β€˜π‘—):π‘‡βŸΆβ„)
163 simp1r3 1268 . . . . . . . . . 10 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ 𝑇) β†’ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))
164 r19.26-3 3104 . . . . . . . . . . 11 (βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)) ↔ (βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))
165164simp1bi 1142 . . . . . . . . . 10 (βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)) β†’ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1))
166 simpl 482 . . . . . . . . . . 11 ((0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) β†’ 0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘))
1671662ralimi 3115 . . . . . . . . . 10 (βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) β†’ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘))
168163, 165, 1673syl 18 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ 𝑇) β†’ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘))
169 simp2 1134 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ 𝑇) β†’ 𝑗 ∈ (0...𝑛))
170 simp3 1135 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ 𝑇) β†’ 𝑑 ∈ 𝑇)
171 rspa 3237 . . . . . . . . . 10 ((βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ 𝑗 ∈ (0...𝑛)) β†’ βˆ€π‘‘ ∈ 𝑇 0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘))
172171r19.21bi 3240 . . . . . . . . 9 (((βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ 𝑗 ∈ (0...𝑛)) ∧ 𝑑 ∈ 𝑇) β†’ 0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘))
173168, 169, 170, 172syl21anc 835 . . . . . . . 8 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ 𝑇) β†’ 0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘))
174 simpr 484 . . . . . . . . . . 11 ((0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) β†’ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1)
1751742ralimi 3115 . . . . . . . . . 10 (βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) β†’ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1)
176163, 165, 1753syl 18 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ 𝑇) β†’ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1)
177 rspa 3237 . . . . . . . . . 10 ((βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1 ∧ 𝑗 ∈ (0...𝑛)) β†’ βˆ€π‘‘ ∈ 𝑇 ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1)
178177r19.21bi 3240 . . . . . . . . 9 (((βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ 𝑇 ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1 ∧ 𝑗 ∈ (0...𝑛)) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1)
179176, 169, 170, 178syl21anc 835 . . . . . . . 8 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ 𝑇) β†’ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1)
180 simp1r3 1268 . . . . . . . . . 10 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ (π·β€˜π‘—)) β†’ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))
181164simp2bi 1143 . . . . . . . . . 10 (βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)) β†’ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛))
182180, 181syl 17 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ (π·β€˜π‘—)) β†’ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛))
183 simp2 1134 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ (π·β€˜π‘—)) β†’ 𝑗 ∈ (0...𝑛))
184 simp3 1135 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ (π·β€˜π‘—)) β†’ 𝑑 ∈ (π·β€˜π‘—))
185 rspa 3237 . . . . . . . . . 10 ((βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ 𝑗 ∈ (0...𝑛)) β†’ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛))
186185r19.21bi 3240 . . . . . . . . 9 (((βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ 𝑗 ∈ (0...𝑛)) ∧ 𝑑 ∈ (π·β€˜π‘—)) β†’ ((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛))
187182, 183, 184, 186syl21anc 835 . . . . . . . 8 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ (π·β€˜π‘—)) β†’ ((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛))
188 simp1r3 1268 . . . . . . . . . 10 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))
189164simp3bi 1144 . . . . . . . . . 10 (βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)) β†’ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))
190188, 189syl 17 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))
191 simp2 1134 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ 𝑗 ∈ (0...𝑛))
192 simp3 1135 . . . . . . . . 9 (((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) ∧ 𝑗 ∈ (0...𝑛) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ 𝑑 ∈ (π΅β€˜π‘—))
193 rspa 3237 . . . . . . . . . 10 ((βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ 𝑗 ∈ (0...𝑛)) β†’ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))
194193r19.21bi 3240 . . . . . . . . 9 (((βˆ€π‘— ∈ (0...𝑛)βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ 𝑗 ∈ (0...𝑛)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ (1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))
195190, 191, 192, 194syl21anc 835 . . . . . . . 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 45235 . . . . . . 7 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ βˆ€π‘‘ ∈ 𝑇 βˆƒπ‘— ∈ ℝ ((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘))))
197 nfmpt1 5246 . . . . . . . . . 10 Ⅎ𝑑(𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))
198197nfeq2 2912 . . . . . . . . 9 Ⅎ𝑑 𝑔 = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))
199 fveq1 6880 . . . . . . . . . . . . 13 (𝑔 = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘))) β†’ (π‘”β€˜π‘‘) = ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘))
200199breq1d 5148 . . . . . . . . . . . 12 (𝑔 = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘))) β†’ ((π‘”β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ↔ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸)))
201199breq2d 5150 . . . . . . . . . . . 12 (𝑔 = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘))) β†’ (((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (π‘”β€˜π‘‘) ↔ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘)))
202200, 201anbi12d 630 . . . . . . . . . . 11 (𝑔 = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘))) β†’ (((π‘”β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (π‘”β€˜π‘‘)) ↔ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘))))
203202anbi2d 628 . . . . . . . . . 10 (𝑔 = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘))) β†’ (((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ ((π‘”β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (π‘”β€˜π‘‘))) ↔ ((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘)))))
204203rexbidv 3170 . . . . . . . . 9 (𝑔 = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘))) β†’ (βˆƒπ‘— ∈ ℝ ((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ ((π‘”β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (π‘”β€˜π‘‘))) ↔ βˆƒπ‘— ∈ ℝ ((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘)))))
205198, 204ralbid 3262 . . . . . . . 8 (𝑔 = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘))) β†’ (βˆ€π‘‘ ∈ 𝑇 βˆƒπ‘— ∈ ℝ ((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ ((π‘”β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (π‘”β€˜π‘‘))) ↔ βˆ€π‘‘ ∈ 𝑇 βˆƒπ‘— ∈ ℝ ((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘)))))
206205rspcev 3604 . . . . . . 7 (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘))) ∈ 𝐴 ∧ βˆ€π‘‘ ∈ 𝑇 βˆƒπ‘— ∈ ℝ ((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ (((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 Β· ((π‘₯β€˜π‘–)β€˜π‘‘)))β€˜π‘‘)))) β†’ βˆƒπ‘” ∈ 𝐴 βˆ€π‘‘ ∈ 𝑇 βˆƒπ‘— ∈ ℝ ((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ ((π‘”β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (π‘”β€˜π‘‘))))
207124, 196, 206syl2anc 583 . . . . . 6 ((πœ‘ ∧ ((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))) β†’ βˆƒπ‘” ∈ 𝐴 βˆ€π‘‘ ∈ 𝑇 βˆƒπ‘— ∈ ℝ ((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ ((π‘”β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (π‘”β€˜π‘‘))))
208207ex 412 . . . . 5 (πœ‘ β†’ (((𝑛 ∈ β„• ∧ βˆ€π‘‘ ∈ 𝑇 (πΉβ€˜π‘‘) < ((𝑛 βˆ’ 1) Β· 𝐸)) ∧ π‘₯:(0...𝑛)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑛)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑛) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑛)) < ((π‘₯β€˜π‘—)β€˜π‘‘))) β†’ βˆƒπ‘” ∈ 𝐴 βˆ€π‘‘ ∈ 𝑇 βˆƒπ‘— ∈ ℝ ((((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)) ∧ ((π‘”β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸) ∧ ((𝑗 βˆ’ (4 / 3)) Β· 𝐸) < (π‘”β€˜π‘‘)))))
2092082eximdv 1914 . . . 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 1928 . . 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 1928 . 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 395   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773  β„²wnf 1777   ∈ wcel 2098  β„²wnfc 2875   β‰  wne 2932  βˆ€wral 3053  βˆƒwrex 3062  {crab 3424  Vcvv 3466   βŠ† wss 3940  βˆ…c0 4314  βˆͺ cuni 4899   class class class wbr 5138   ↦ cmpt 5221  ran crn 5667  βŸΆwf 6529  β€˜cfv 6533  (class class class)co 7401  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   Β· cmul 11111   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441   / cdiv 11868  β„•cn 12209  3c3 12265  4c4 12266  β„+crp 12971  (,)cioo 13321  ...cfz 13481  Ξ£csu 15629  topGenctg 17382   Cn ccn 23050  Compccmp 23212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-rlim 15430  df-sum 15630  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-mulg 18986  df-cntz 19223  df-cmn 19692  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-cnfld 21229  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-cn 23053  df-cnp 23054  df-cmp 23213  df-tx 23388  df-hmeo 23581  df-xms 24148  df-ms 24149  df-tms 24150
This theorem is referenced by:  stoweidlem61  45262
  Copyright terms: Public domain W3C validator