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

Theorem stoweidlem34 41883
Description: This lemma proves that for all 𝑡 in 𝑇 there is a 𝑗 as in the proof of [BrosowskiDeutsh] p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here 𝐸 is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem34.1 𝑡𝐹
stoweidlem34.2 𝑗𝜑
stoweidlem34.3 𝑡𝜑
stoweidlem34.4 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
stoweidlem34.5 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
stoweidlem34.6 𝐽 = (𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
stoweidlem34.7 (𝜑𝑁 ∈ ℕ)
stoweidlem34.8 (𝜑𝑇 ∈ V)
stoweidlem34.9 (𝜑𝐹:𝑇⟶ℝ)
stoweidlem34.10 ((𝜑𝑡𝑇) → 0 ≤ (𝐹𝑡))
stoweidlem34.11 ((𝜑𝑡𝑇) → (𝐹𝑡) < ((𝑁 − 1) · 𝐸))
stoweidlem34.12 (𝜑𝐸 ∈ ℝ+)
stoweidlem34.13 (𝜑𝐸 < (1 / 3))
stoweidlem34.14 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ)
stoweidlem34.15 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡))
stoweidlem34.16 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1)
stoweidlem34.17 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁))
stoweidlem34.18 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡))
Assertion
Ref Expression
stoweidlem34 (𝜑 → ∀𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
Distinct variable groups:   𝑖,𝑗,𝑡,𝐸   𝐷,𝑖   𝑖,𝐽   𝑖,𝑁,𝑗,𝑡   𝑇,𝑖,𝑗,𝑡   𝜑,𝑖   𝑗,𝐹   𝑗,𝑋,𝑡
Allowed substitution hints:   𝜑(𝑡,𝑗)   𝐵(𝑡,𝑖,𝑗)   𝐷(𝑡,𝑗)   𝐹(𝑡,𝑖)   𝐽(𝑡,𝑗)   𝑋(𝑖)

Proof of Theorem stoweidlem34
Dummy variables 𝑘 𝑙 𝑠 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem34.3 . 2 𝑡𝜑
2 simpr 485 . . . . . . . 8 ((𝜑𝑡𝑇) → 𝑡𝑇)
3 ovex 7055 . . . . . . . . 9 (1...𝑁) ∈ V
43rabex 5133 . . . . . . . 8 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ∈ V
5 stoweidlem34.6 . . . . . . . . 9 𝐽 = (𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
65fvmpt2 6652 . . . . . . . 8 ((𝑡𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ∈ V) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
72, 4, 6sylancl 586 . . . . . . 7 ((𝜑𝑡𝑇) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
8 ssrab2 3983 . . . . . . 7 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ⊆ (1...𝑁)
97, 8syl6eqss 3948 . . . . . 6 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ (1...𝑁))
10 elfznn 12790 . . . . . . 7 (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
1110ssriv 3899 . . . . . 6 (1...𝑁) ⊆ ℕ
129, 11syl6ss 3907 . . . . 5 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ ℕ)
13 nnssre 11496 . . . . 5 ℕ ⊆ ℝ
1412, 13syl6ss 3907 . . . 4 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ ℝ)
15 stoweidlem34.7 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
1615adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → 𝑁 ∈ ℕ)
17 nnuz 12134 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
1816, 17syl6eleq 2895 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 𝑁 ∈ (ℤ‘1))
19 eluzfz2 12769 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
2018, 19syl 17 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑁 ∈ (1...𝑁))
21 stoweidlem34.11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝐹𝑡) < ((𝑁 − 1) · 𝐸))
22 3re 11571 . . . . . . . . . . . . . . . . . . . . 21 3 ∈ ℝ
23 3ne0 11597 . . . . . . . . . . . . . . . . . . . . 21 3 ≠ 0
2422, 23rereccli 11259 . . . . . . . . . . . . . . . . . . . 20 (1 / 3) ∈ ℝ
2524a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (1 / 3) ∈ ℝ)
26 1red 10495 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 1 ∈ ℝ)
2716nnred 11507 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 𝑁 ∈ ℝ)
28 1lt3 11664 . . . . . . . . . . . . . . . . . . . . 21 1 < 3
2922, 28pm3.2i 471 . . . . . . . . . . . . . . . . . . . 20 (3 ∈ ℝ ∧ 1 < 3)
30 recgt1i 11391 . . . . . . . . . . . . . . . . . . . . 21 ((3 ∈ ℝ ∧ 1 < 3) → (0 < (1 / 3) ∧ (1 / 3) < 1))
3130simprd 496 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℝ ∧ 1 < 3) → (1 / 3) < 1)
3229, 31mp1i 13 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (1 / 3) < 1)
3325, 26, 27, 32ltsub2dd 11107 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝑇) → (𝑁 − 1) < (𝑁 − (1 / 3)))
3427, 26resubcld 10922 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (𝑁 − 1) ∈ ℝ)
3527, 25resubcld 10922 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (𝑁 − (1 / 3)) ∈ ℝ)
36 stoweidlem34.12 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸 ∈ ℝ+)
3736rpred 12285 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐸 ∈ ℝ)
3837adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 𝐸 ∈ ℝ)
3936rpgt0d 12288 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝐸)
4039adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 0 < 𝐸)
41 ltmul1 11344 . . . . . . . . . . . . . . . . . . 19 (((𝑁 − 1) ∈ ℝ ∧ (𝑁 − (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
4234, 35, 38, 40, 41syl112anc 1367 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝑇) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
4333, 42mpbid 233 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸))
4421, 43jca 512 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → ((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
45 stoweidlem34.9 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑇⟶ℝ)
4645ffvelrnda 6723 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
4734, 38remulcld 10524 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − 1) · 𝐸) ∈ ℝ)
4835, 38remulcld 10524 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ)
49 lttr 10570 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸)))
50 ltle 10582 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
51503adant2 1124 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5249, 51syld 47 . . . . . . . . . . . . . . . . 17 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5346, 47, 48, 52syl3anc 1364 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5444, 53mpd 15 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))
55 rabid 3339 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
562, 54, 55sylanbrc 583 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
57 stoweidlem34.4 . . . . . . . . . . . . . . . 16 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
58 oveq1 7030 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → (𝑗 − (1 / 3)) = (𝑁 − (1 / 3)))
5958oveq1d 7038 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑁 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑁 − (1 / 3)) · 𝐸))
6059breq2d 4980 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑁 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
6160rabbidv 3428 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑁 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
62 nnnn0 11758 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
63 nn0uz 12133 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
6462, 63syl6eleq 2895 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘0))
65 eluzfz2 12769 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
6615, 64, 653syl 18 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (0...𝑁))
67 stoweidlem34.8 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ V)
68 rabexg 5132 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V)
6967, 68syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V)
7057, 61, 66, 69fvmptd3 6664 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7170adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7256, 71eleqtrrd 2888 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑡 ∈ (𝐷𝑁))
73 nfcv 2951 . . . . . . . . . . . . . 14 𝑗𝑁
74 nfcv 2951 . . . . . . . . . . . . . 14 𝑗(1...𝑁)
75 nfmpt1 5065 . . . . . . . . . . . . . . . . 17 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7657, 75nfcxfr 2949 . . . . . . . . . . . . . . . 16 𝑗𝐷
7776, 73nffv 6555 . . . . . . . . . . . . . . 15 𝑗(𝐷𝑁)
7877nfcri 2945 . . . . . . . . . . . . . 14 𝑗 𝑡 ∈ (𝐷𝑁)
79 fveq2 6545 . . . . . . . . . . . . . . 15 (𝑗 = 𝑁 → (𝐷𝑗) = (𝐷𝑁))
8079eleq2d 2870 . . . . . . . . . . . . . 14 (𝑗 = 𝑁 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑁)))
8173, 74, 78, 80elrabf 3617 . . . . . . . . . . . . 13 (𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ↔ (𝑁 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑁)))
8220, 72, 81sylanbrc 583 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → 𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
8382, 7eleqtrrd 2888 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝑁 ∈ (𝐽𝑡))
84 ne0i 4226 . . . . . . . . . . 11 (𝑁 ∈ (𝐽𝑡) → (𝐽𝑡) ≠ ∅)
8583, 84syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐽𝑡) ≠ ∅)
86 nnwo 12166 . . . . . . . . . . 11 (((𝐽𝑡) ⊆ ℕ ∧ (𝐽𝑡) ≠ ∅) → ∃𝑖 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑖𝑘)
87 nfcv 2951 . . . . . . . . . . . 12 𝑖(𝐽𝑡)
88 nfcv 2951 . . . . . . . . . . . . . . 15 𝑗𝑇
89 nfrab1 3346 . . . . . . . . . . . . . . 15 𝑗{𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)}
9088, 89nfmpt 5064 . . . . . . . . . . . . . 14 𝑗(𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
915, 90nfcxfr 2949 . . . . . . . . . . . . 13 𝑗𝐽
92 nfcv 2951 . . . . . . . . . . . . 13 𝑗𝑡
9391, 92nffv 6555 . . . . . . . . . . . 12 𝑗(𝐽𝑡)
94 nfv 1896 . . . . . . . . . . . . 13 𝑗 𝑖𝑘
9593, 94nfral 3193 . . . . . . . . . . . 12 𝑗𝑘 ∈ (𝐽𝑡)𝑖𝑘
96 nfv 1896 . . . . . . . . . . . 12 𝑖𝑘 ∈ (𝐽𝑡)𝑗𝑘
97 breq1 4971 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (𝑖𝑘𝑗𝑘))
9897ralbidv 3166 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (∀𝑘 ∈ (𝐽𝑡)𝑖𝑘 ↔ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘))
9987, 93, 95, 96, 98cbvrexf 3400 . . . . . . . . . . 11 (∃𝑖 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑖𝑘 ↔ ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
10086, 99sylib 219 . . . . . . . . . 10 (((𝐽𝑡) ⊆ ℕ ∧ (𝐽𝑡) ≠ ∅) → ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
10112, 85, 100syl2anc 584 . . . . . . . . 9 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
102 stoweidlem34.2 . . . . . . . . . . 11 𝑗𝜑
103 nfv 1896 . . . . . . . . . . 11 𝑗 𝑡𝑇
104102, 103nfan 1885 . . . . . . . . . 10 𝑗(𝜑𝑡𝑇)
1057eleq2d 2870 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) ↔ 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)}))
106105biimpa 477 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
107 rabid 3339 . . . . . . . . . . . . . . 15 (𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)))
108106, 107sylib 219 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)))
109108simprd 496 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑡 ∈ (𝐷𝑗))
110109adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → 𝑡 ∈ (𝐷𝑗))
111 simp3 1131 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑡 ∈ (𝐷‘(𝑗 − 1)))
112 simp1l 1190 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝜑)
113 noel 4222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ 𝑡 ∈ ∅
114 oveq1 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 = 1 → (𝑗 − 1) = (1 − 1))
115 1m1e0 11563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 − 1) = 0
116114, 115syl6eq 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 = 1 → (𝑗 − 1) = 0)
117116fveq2d 6549 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 = 1 → (𝐷‘(𝑗 − 1)) = (𝐷‘0))
11822a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑡𝑇) → 3 ∈ ℝ)
11923a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑡𝑇) → 3 ≠ 0)
12026, 118, 119redivcld 11322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑡𝑇) → (1 / 3) ∈ ℝ)
121120renegcld 10921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → -(1 / 3) ∈ ℝ)
122121, 38remulcld 10524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) ∈ ℝ)
123 0red 10497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → 0 ∈ ℝ)
124 3pos 11596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
12522, 124recgt0ii 11400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
126 lt0neg2 11001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((1 / 3) ∈ ℝ → (0 < (1 / 3) ↔ -(1 / 3) < 0))
12724, 126ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (0 < (1 / 3) ↔ -(1 / 3) < 0)
128125, 127mpbi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 -(1 / 3) < 0
129 ltmul1 11344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((-(1 / 3) ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (-(1 / 3) < 0 ↔ (-(1 / 3) · 𝐸) < (0 · 𝐸)))
130121, 123, 38, 40, 129syl112anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑡𝑇) → (-(1 / 3) < 0 ↔ (-(1 / 3) · 𝐸) < (0 · 𝐸)))
131128, 130mpbii 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < (0 · 𝐸))
132 mul02lem2 10670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐸 ∈ ℝ → (0 · 𝐸) = 0)
13338, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → (0 · 𝐸) = 0)
134131, 133breqtrd 4994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < 0)
135 stoweidlem34.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → 0 ≤ (𝐹𝑡))
136122, 123, 46, 134, 135ltletrd 10653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < (𝐹𝑡))
137122, 46ltnled 10640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑡𝑇) → ((-(1 / 3) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
138136, 137mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑡𝑇) → ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸))
139 nan 826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸))) ↔ ((𝜑𝑡𝑇) → ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
140138, 139mpbir 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
141 rabid 3339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
142140, 141sylnibr 330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
143 oveq1 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 0 → (𝑗 − (1 / 3)) = (0 − (1 / 3)))
144 df-neg 10726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 -(1 / 3) = (0 − (1 / 3))
145143, 144syl6eqr 2851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 = 0 → (𝑗 − (1 / 3)) = -(1 / 3))
146145oveq1d 7038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 = 0 → ((𝑗 − (1 / 3)) · 𝐸) = (-(1 / 3) · 𝐸))
147146breq2d 4980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 = 0 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
148147rabbidv 3428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 0 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
14915nnnn0d 11809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑁 ∈ ℕ0)
150 elnn0uz 12136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
151149, 150sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝑁 ∈ (ℤ‘0))
152 eluzfz1 12768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ (ℤ‘0) → 0 ∈ (0...𝑁))
153151, 152syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → 0 ∈ (0...𝑁))
154 rabexg 5132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V)
15567, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V)
15657, 148, 153, 155fvmptd3 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝐷‘0) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
157142, 156neleqtrrd 2907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ¬ 𝑡 ∈ (𝐷‘0))
1581, 157alrimi 2180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0))
159 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑡(0...𝑁)
160 nfrab1 3346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑡{𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
161159, 160nfmpt 5064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
16257, 161nfcxfr 2949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑡𝐷
163 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑡0
164162, 163nffv 6555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑡(𝐷‘0)
165164eq0f 4231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐷‘0) = ∅ ↔ ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0))
166158, 165sylibr 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐷‘0) = ∅)
167117, 166sylan9eqr 2855 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 = 1) → (𝐷‘(𝑗 − 1)) = ∅)
168167eleq2d 2870 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 = 1) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ ∅))
169113, 168mtbiri 328 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 = 1) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
170169ex 413 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑗 = 1 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
171170con2d 136 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ 𝑗 = 1))
172112, 111, 171sylc 65 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 = 1)
173 simplll 771 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → 𝜑)
174105, 107syl6bb 288 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗))))
175174simprbda 499 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ (1...𝑁))
17615, 17syl6eleq 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ (ℤ‘1))
177176adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (𝐽𝑡)) → 𝑁 ∈ (ℤ‘1))
178 elfzp12 12840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
180179adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
181175, 180mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁)))
182181orcanai 997 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → 𝑗 ∈ ((1 + 1)...𝑁))
183 fzssp1 12804 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1...(𝑁 − 1)) ⊆ (1...((𝑁 − 1) + 1))
18415nncnd 11508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℂ)
185 1cnd 10489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → 1 ∈ ℂ)
186184, 185npcand 10855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
187186oveq2d 7039 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
188183, 187sseqtrid 3946 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
189188adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
190 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ((1 + 1)...𝑁))
191 1z 11866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ∈ ℤ
192 zaddcl 11876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1 ∈ ℤ ∧ 1 ∈ ℤ) → (1 + 1) ∈ ℤ)
193191, 191, 192mp2an 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 + 1) ∈ ℤ
194193a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (1 + 1) ∈ ℤ)
19515nnzd 11940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℤ)
196195adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑁 ∈ ℤ)
197 elfzelz 12762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ((1 + 1)...𝑁) → 𝑗 ∈ ℤ)
198197adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ℤ)
199 1zzd 11867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 1 ∈ ℤ)
200 fzsubel 12797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
201194, 196, 198, 199, 200syl22anc 835 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
202190, 201mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
203 ax-1cn 10448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
204203, 203pncan3oi 10756 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 + 1) − 1) = 1
205204oveq1i 7033 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
206202, 205syl6eleq 2895 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...(𝑁 − 1)))
207189, 206sseldd 3896 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...𝑁))
208173, 182, 207syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → (𝑗 − 1) ∈ (1...𝑁))
209208ex 413 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁)))
2102093adant3 1125 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁)))
211172, 210mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (1...𝑁))
212 fveq2 6545 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑗 − 1) → (𝐷𝑖) = (𝐷‘(𝑗 − 1)))
213212eleq2d 2870 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑗 − 1) → (𝑡 ∈ (𝐷𝑖) ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
214213elrab3 3622 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 − 1) ∈ (1...𝑁) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
215211, 214syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
216111, 215mpbird 258 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)})
217 nfcv 2951 . . . . . . . . . . . . . . . . . . . 20 𝑖(1...𝑁)
218 nfv 1896 . . . . . . . . . . . . . . . . . . . 20 𝑖 𝑡 ∈ (𝐷𝑗)
219 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . 22 𝑗𝑖
22076, 219nffv 6555 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝐷𝑖)
221220nfcri 2945 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑡 ∈ (𝐷𝑖)
222 fveq2 6545 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
223222eleq2d 2870 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑖)))
22474, 217, 218, 221, 223cbvrab 3436 . . . . . . . . . . . . . . . . . . 19 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} = {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)}
225216, 224syl6eleqr 2896 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
22673ad2ant1 1126 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
227225, 226eleqtrrd 2888 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (𝐽𝑡))
228 elfzelz 12762 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ ℤ)
229 zre 11839 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
230175, 228, 2293syl 18 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ ℝ)
2312303adant3 1125 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑗 ∈ ℝ)
232 peano2rem 10807 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
233 ltm1 11336 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → (𝑗 − 1) < 𝑗)
234233adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → (𝑗 − 1) < 𝑗)
235 ltnle 10573 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 − 1) ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
236235ancoms 459 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → ((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
237234, 236mpbid 233 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → ¬ 𝑗 ≤ (𝑗 − 1))
238231, 232, 237syl2anc2 585 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 ≤ (𝑗 − 1))
239 breq2 4972 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑗 − 1) → (𝑗𝑘𝑗 ≤ (𝑗 − 1)))
240239notbid 319 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑗 − 1) → (¬ 𝑗𝑘 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
241240rspcev 3561 . . . . . . . . . . . . . . . . 17 (((𝑗 − 1) ∈ (𝐽𝑡) ∧ ¬ 𝑗 ≤ (𝑗 − 1)) → ∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘)
242227, 238, 241syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘)
243 rexnal 3204 . . . . . . . . . . . . . . . 16 (∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘 ↔ ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
244242, 243sylib 219 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
2452443expia 1114 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘))
246245con2d 136 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (∀𝑘 ∈ (𝐽𝑡)𝑗𝑘 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
247246imp 407 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
248110, 247eldifd 3876 . . . . . . . . . . 11 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
249248exp31 420 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) → (∀𝑘 ∈ (𝐽𝑡)𝑗𝑘𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))))
250104, 249reximdai 3274 . . . . . . . . 9 ((𝜑𝑡𝑇) → (∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘 → ∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
251101, 250mpd 15 . . . . . . . 8 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
252 df-rex 3113 . . . . . . . 8 (∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
253251, 252sylib 219 . . . . . . 7 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
254 simprl 767 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (𝐽𝑡))
255 eldifn 4031 . . . . . . . . . . . . 13 (𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
256 simplr 765 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑡𝑇)
257 simpll 763 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝜑)
258175adantrr 713 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ (1...𝑁))
259 simprr 769 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
260 oveq1 7030 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑘 → (𝑗 − (1 / 3)) = (𝑘 − (1 / 3)))
261260oveq1d 7038 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑘 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑘 − (1 / 3)) · 𝐸))
262261breq2d 4980 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 𝑘 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)))
263262rabbidv 3428 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑘 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
264263cbvmptv 5068 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
26557, 264eqtri 2821 . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
266 oveq1 7030 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑗 − 1) → (𝑘 − (1 / 3)) = ((𝑗 − 1) − (1 / 3)))
267266oveq1d 7038 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑗 − 1) → ((𝑘 − (1 / 3)) · 𝐸) = (((𝑗 − 1) − (1 / 3)) · 𝐸))
268267breq2d 4980 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 − 1) → ((𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)))
269268rabbidv 3428 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑗 − 1) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
270 fzssp1 12804 . . . . . . . . . . . . . . . . . . . . . . . 24 (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
271186oveq2d 7039 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
272270, 271sseqtrid 3946 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
273272adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
274 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
275 1zzd 11867 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 1 ∈ ℤ)
276195adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℤ)
277228adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℤ)
278 fzsubel 12797 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
279275, 276, 277, 275, 278syl22anc 835 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
280274, 279mpbid 233 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1)))
281115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → (1 − 1) = 0)
282281oveq1d 7038 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝑁)) → ((1 − 1)...(𝑁 − 1)) = (0...(𝑁 − 1)))
283280, 282eleqtrd 2887 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
284273, 283sseldd 3896 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...𝑁))
28567adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑇 ∈ V)
286 rabexg 5132 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V)
287285, 286syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V)
288265, 269, 284, 287fvmptd3 6664 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐷‘(𝑗 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
289288eleq2d 2870 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}))
290289notbid 319 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → (¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}))
291290biimpa 477 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
292257, 258, 259, 291syl21anc 834 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
293 rabid 3339 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)))
294230adantrr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ ℝ)
295 recn 10480 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → 𝑗 ∈ ℂ)
296 1cnd 10489 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → 1 ∈ ℂ)
297 1re 10494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
298297, 22, 233pm3.2i 1332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0)
299 redivcl 11213 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (1 / 3) ∈ ℝ)
300 recn 10480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 / 3) ∈ ℝ → (1 / 3) ∈ ℂ)
301298, 299, 300mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 / 3) ∈ ℂ
302301a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → (1 / 3) ∈ ℂ)
303295, 296, 302subsub4d 10882 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) = (𝑗 − (1 + (1 / 3))))
304 3cn 11572 . . . . . . . . . . . . . . . . . . . . . . . . . 26 3 ∈ ℂ
305304, 203, 304, 23divdiri 11251 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
306 3p1e4 11636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 + 1) = 4
307306oveq1i 7033 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 + 1) / 3) = (4 / 3)
308304, 23dividi 11227 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 / 3) = 1
309308oveq1i 7033 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
310305, 307, 3093eqtr3i 2829 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 / 3) = (1 + (1 / 3))
311310a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → (4 / 3) = (1 + (1 / 3)))
312311oveq2d 7039 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℝ → (𝑗 − (4 / 3)) = (𝑗 − (1 + (1 / 3))))
313303, 312eqtr4d 2836 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) = (𝑗 − (4 / 3)))
314313oveq1d 7038 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
315294, 314syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
316315breq2d 4980 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
317316anbi2d 628 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝑡𝑇 ∧ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)) ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))))
318293, 317syl5bb 284 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))))
319292, 318mtbid 325 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
320 imnan 400 . . . . . . . . . . . . . . 15 ((𝑡𝑇 → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)) ↔ ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
321319, 320sylibr 235 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡𝑇 → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
322256, 321mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))
323255, 322sylanr2 679 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))
324230adantrr 713 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ ℝ)
325 4re 11575 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ
326325a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 4 ∈ ℝ)
32722a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ∈ ℝ)
32823a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ≠ 0)
329326, 327, 328redivcld 11322 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (4 / 3) ∈ ℝ)
330324, 329resubcld 10922 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 − (4 / 3)) ∈ ℝ)
33137ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ)
332 remulcl 10475 . . . . . . . . . . . . . . 15 (((𝑗 − (4 / 3)) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ)
333332rexrd 10544 . . . . . . . . . . . . . 14 (((𝑗 − (4 / 3)) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*)
334330, 331, 333syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*)
33546rexrd 10544 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ*)
336335adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹𝑡) ∈ ℝ*)
337 xrltnle 10561 . . . . . . . . . . . . 13 ((((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ* ∧ (𝐹𝑡) ∈ ℝ*) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
338334, 336, 337syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
339323, 338mpbird 258 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡))
340 simpl 483 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝜑𝑡𝑇))
341 simprr 769 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
342341eldifad 3877 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ (𝐷𝑗))
343 simplll 771 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝜑)
344175adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑗 ∈ (1...𝑁))
345 simpr 485 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ (𝐷𝑗))
346 oveq1 7030 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑗 → (𝑘 − (1 / 3)) = (𝑗 − (1 / 3)))
347346oveq1d 7038 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → ((𝑘 − (1 / 3)) · 𝐸) = ((𝑗 − (1 / 3)) · 𝐸))
348347breq2d 4980 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → ((𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
349348rabbidv 3428 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
350 fz1ssfz0 12857 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ⊆ (0...𝑁)
351350sseli 3891 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ (0...𝑁))
352351adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (0...𝑁))
353 rabexg 5132 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
354285, 353syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
355265, 349, 352, 354fvmptd3 6664 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
356355eleq2d 2870 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}))
357356biimpa 477 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
358343, 344, 345, 357syl21anc 834 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
359 rabid 3339 . . . . . . . . . . . . . 14 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
360358, 359sylib 219 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
361360simprd 496 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
362340, 254, 342, 361syl21anc 834 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
363339, 362jca 512 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
36415ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑁 ∈ ℕ)
365 simplr 765 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡𝑇)
366175adantrr 713 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (1...𝑁))
367 nfv 1896 . . . . . . . . . . . . . . . 16 𝑗 𝑖 ∈ (0...𝑁)
368102, 367nfan 1885 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁))
369 nfv 1896 . . . . . . . . . . . . . . 15 𝑗(𝑋𝑖):𝑇⟶ℝ
370368, 369nfim 1882 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
371 eleq1w 2867 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑗 ∈ (0...𝑁) ↔ 𝑖 ∈ (0...𝑁)))
372371anbi2d 628 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑖 ∈ (0...𝑁))))
373 fveq2 6545 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑋𝑗) = (𝑋𝑖))
374373feq1d 6374 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑋𝑗):𝑇⟶ℝ ↔ (𝑋𝑖):𝑇⟶ℝ))
375372, 374imbi12d 346 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ) ↔ ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)))
376 stoweidlem34.14 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ)
377370, 375, 376chvar 2371 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
378377ad4ant14 748 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
379 simplll 771 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝜑)
380 simpr 485 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁))
381 simpllr 772 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑡𝑇)
382102, 367, 103nf3an 1887 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇)
383 nfv 1896 . . . . . . . . . . . . . . 15 𝑗((𝑋𝑖)‘𝑡) ≤ 1
384382, 383nfim 1882 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)
3853713anbi2d 1433 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇)))
386373fveq1d 6547 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → ((𝑋𝑗)‘𝑡) = ((𝑋𝑖)‘𝑡))
387386breq1d 4978 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (((𝑋𝑗)‘𝑡) ≤ 1 ↔ ((𝑋𝑖)‘𝑡) ≤ 1))
388385, 387imbi12d 346 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)))
389 stoweidlem34.16 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1)
390384, 388, 389chvar 2371 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)
391379, 380, 381, 390syl3anc 1364 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑡) ≤ 1)
392 simplll 771 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑)
393 0zd 11847 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ)
394 elfzel2 12760 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑁 ∈ ℤ)
395394adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ)
396 elfzelz 12762 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℤ)
397396adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ)
398393, 395, 3973jca 1121 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
399 0red 10497 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℝ)
400 elfzel1 12761 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℤ)
401400zred 11941 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℝ)
402401adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ)
403396zred 11941 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℝ)
404403adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
405 0red 10497 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ∈ ℝ)
406 1red 10495 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 1 ∈ ℝ)
407 0le1 11017 . . . . . . . . . . . . . . . . . . . 20 0 ≤ 1
408407a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ≤ 1)
409 elfzle1 12764 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...𝑁) → 1 ≤ 𝑗)
410175, 409syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 1 ≤ 𝑗)
411405, 406, 230, 408, 410letrd 10650 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ≤ 𝑗)
412411adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑗)
413 elfzle1 12764 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑗𝑖)
414413adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗𝑖)
415399, 402, 404, 412, 414letrd 10650 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑖)
416 elfzle2 12765 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑖𝑁)
417416adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖𝑁)
418415, 417jca 512 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖𝑖𝑁))
419 elfz2 12753 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑁)))
420398, 418, 419sylanbrc 583 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
421420adantlrr 717 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
422 simpll 763 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑𝑡𝑇))
423 simplrl 773 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽𝑡))
424 simplrr 774 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
425424eldifad 3877 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑗))
426 simpr 485 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁))
427 simpl1 1184 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑𝑡𝑇))
428427simprd 496 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡𝑇)
429427, 46syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ∈ ℝ)
430401adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ)
43124a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈ ℝ)
432430, 431resubcld 10922 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
433 simpl1l 1217 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑)
434433, 37syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
435432, 434remulcld 10524 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
436403adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
43724a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈ ℝ)
438436, 437resubcld 10922 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈ ℝ)
43937adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
440438, 439remulcld 10524 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ)
441433, 440sylancom 588 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ)
442 simpl3 1186 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑗))
443 simpl2 1185 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽𝑡))
444427, 443, 175syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (1...𝑁))
445433, 444, 355syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
446442, 445eleqtrd 2887 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
447446, 359sylib 219 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
448447simprd 496 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
449403adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
450413adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗𝑖)
451430, 449, 431, 450lesub1dd 11110 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)))
452433, 438sylancom 588 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈ ℝ)
45336rpregt0d 12291 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
454433, 453syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
455 lemul1 11346 . . . . . . . . . . . . . . . . . . 19 (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑖 − (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
456432, 452, 454, 455syl3anc 1364 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
457451, 456mpbid 233 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸))
458429, 435, 441, 448, 457letrd 10650 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸))
459 rabid 3339 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
460428, 458, 459sylanbrc 583 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
461 simpr 485 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁))
462 0zd 11847 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ)
4633943ad2ant3 1128 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ)
4643963ad2ant3 1128 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ)
465462, 463, 4643jca 1121 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
4664183impa 1103 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖𝑖𝑁))
467465, 466, 419sylanbrc 583 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
468427, 443, 461, 467syl3anc 1364 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
469 oveq1 7030 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 − (1 / 3)) = (𝑖 − (1 / 3)))
470469oveq1d 7038 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑖 − (1 / 3)) · 𝐸))
471470breq2d 4980 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
472471rabbidv 3428 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
473 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁))
474 rabexg 5132 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
47567, 474syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
476475adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
47757, 472, 473, 476fvmptd3 6664 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
478433, 468, 477syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
479460, 478eleqtrrd 2888 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑖))
480422, 423, 425, 426, 479syl31anc 1366 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑖))
481102, 367, 221nf3an 1887 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖))
482 nfv 1896 . . . . . . . . . . . . . . 15 𝑗((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁)
483481, 482nfim 1882 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
484371, 2233anbi23d 1431 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖))))
485386breq1d 4978 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁)))
486484, 485imbi12d 346 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))))
487 stoweidlem34.17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁))
488483, 486, 487chvar 2371 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
489392, 421, 480, 488syl3anc 1364 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
49036ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ+)
491 stoweidlem34.13 . . . . . . . . . . . . 13 (𝜑𝐸 < (1 / 3))
492491ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 < (1 / 3))
493364, 365, 366, 378, 391, 489, 490, 492stoweidlem11 41860 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸))
494 eleq1w 2867 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑙 ∈ (𝐽𝑡) ↔ 𝑗 ∈ (𝐽𝑡)))
495 fveq2 6545 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑗 → (𝐷𝑙) = (𝐷𝑗))
496 oveq1 7030 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 → (𝑙 − 1) = (𝑗 − 1))
497496fveq2d 6549 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑗 → (𝐷‘(𝑙 − 1)) = (𝐷‘(𝑗 − 1)))
498495, 497difeq12d 4027 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑗 → ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) = ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
499498eleq2d 2870 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
500494, 499anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑗 → ((𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))))
501500anbi2d 628 . . . . . . . . . . . . . . 15 (𝑙 = 𝑗 → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))))
502 oveq1 7030 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑙 − (4 / 3)) = (𝑗 − (4 / 3)))
503502oveq1d 7038 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑗 → ((𝑙 − (4 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
504503breq1d 4978 . . . . . . . . . . . . . . 15 (𝑙 = 𝑗 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) ↔ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
505501, 504imbi12d 346 . . . . . . . . . . . . . 14 (𝑙 = 𝑗 → ((((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)) ↔ (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
506 eleq1w 2867 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑠𝑇𝑡𝑇))
507506anbi2d 628 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝜑𝑠𝑇) ↔ (𝜑𝑡𝑇)))
508 fveq2 6545 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑡 → (𝐽𝑠) = (𝐽𝑡))
509508eleq2d 2870 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑙 ∈ (𝐽𝑠) ↔ 𝑙 ∈ (𝐽𝑡)))
510 eleq1w 2867 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
511509, 510anbi12d 630 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))))
512507, 511anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))))
513 fveq2 6545 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠) = ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
514513breq2d 4980 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠) ↔ ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
515512, 514imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠)) ↔ (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
516 stoweidlem34.1 . . . . . . . . . . . . . . . . . 18 𝑡𝐹
517 nfv 1896 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑠𝑇
518102, 517nfan 1885 . . . . . . . . . . . . . . . . . . 19 𝑗(𝜑𝑠𝑇)
519 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . 22 𝑗𝑠
52091, 519nffv 6555 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝐽𝑠)
521520nfcri 2945 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑙 ∈ (𝐽𝑠)
522 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗𝑙
52376, 522nffv 6555 . . . . . . . . . . . . . . . . . . . . . 22 𝑗(𝐷𝑙)
524 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗(𝑙 − 1)
52576, 524nffv 6555 . . . . . . . . . . . . . . . . . . . . . 22 𝑗(𝐷‘(𝑙 − 1))
526523, 525nfdif 4029 . . . . . . . . . . . . . . . . . . . . 21 𝑗((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
527526nfcri 2945 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
528521, 527nfan 1885 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
529518, 528nfan 1885 . . . . . . . . . . . . . . . . . 18 𝑗((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
530 nfv 1896 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑠𝑇
5311, 530nfan 1885 . . . . . . . . . . . . . . . . . . 19 𝑡(𝜑𝑠𝑇)
532 nfmpt1 5065 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
5335, 532nfcxfr 2949 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝐽
534 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝑠
535533, 534nffv 6555 . . . . . . . . . . . . . . . . . . . . 21 𝑡(𝐽𝑠)
536535nfcri 2945 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑙 ∈ (𝐽𝑠)
537 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝑙
538162, 537nffv 6555 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝐷𝑙)
539 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑙 − 1)
540162, 539nffv 6555 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝐷‘(𝑙 − 1))
541538, 540nfdif 4029 . . . . . . . . . . . . . . . . . . . . 21 𝑡((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
542541nfcri 2945 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
543536, 542nfan 1885 . . . . . . . . . . . . . . . . . . 19 𝑡(𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
544531, 543nfan 1885 . . . . . . . . . . . . . . . . . 18 𝑡((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
545 stoweidlem34.5 . . . . . . . . . . . . . . . . . 18 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
54615ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑁 ∈ ℕ)
54767ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑇 ∈ V)
5483rabex 5133 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ∈ V
549 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑡𝑗
550162, 549nffv 6555 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡(𝐷𝑗)
551550nfcri 2945 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 𝑠 ∈ (𝐷𝑗)
552 nfcv 2951 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(1...𝑁)
553551, 552nfrab 3347 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡{𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)}
554 eleq1w 2867 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑠 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑠 ∈ (𝐷𝑗)))
555554rabbidv 3428 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑠 → {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
556534, 553, 555, 5fvmptf 6662 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ∈ V) → (𝐽𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
557548, 556mpan2 687 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠𝑇 → (𝐽𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
558557eleq2d 2870 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠𝑇 → (𝑙 ∈ (𝐽𝑠) ↔ 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)}))
559558biimpa 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
560523nfcri 2945 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 𝑠 ∈ (𝐷𝑙)
561 fveq2 6545 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑙 → (𝐷𝑗) = (𝐷𝑙))
562561eleq2d 2870 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑙 → (𝑠 ∈ (𝐷𝑗) ↔ 𝑠 ∈ (𝐷𝑙)))
563522, 74, 560, 562elrabf 3617 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ↔ (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷𝑙)))
564559, 563sylib 219 . . . . . . . . . . . . . . . . . . . 20 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷𝑙)))
565564simpld 495 . . . . . . . . . . . . . . . . . . 19 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → 𝑙 ∈ (1...𝑁))
566565ad2ant2lr 744 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑙 ∈ (1...𝑁))
567 simprr 769 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
56845ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐹:𝑇⟶ℝ)
56936ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 ∈ ℝ+)
570491ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 < (1 / 3))
571377ad4ant14 748 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
572 simp1ll 1229 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 𝜑)
573 nfv 1896 . . . . . . . . . . . . . . . . . . . . 21 𝑗0 ≤ ((𝑋𝑖)‘𝑡)
574382, 573nfim 1882 . . . . . . . . . . . . . . . . . . . 20 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
575386breq2d 4980 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (0 ≤ ((𝑋𝑗)‘𝑡) ↔ 0 ≤ ((𝑋𝑖)‘𝑡)))
576385, 575imbi12d 346 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))))
577 stoweidlem34.15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡))
578574, 576, 577chvar 2371 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
579572, 578syld3an1 1403 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
580 simp1ll 1229 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → 𝜑)
581 nfmpt1 5065 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
582545, 581nfcxfr 2949 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑗𝐵
583582, 219nffv 6555 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗(𝐵𝑖)
584583nfcri 2945 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 𝑡 ∈ (𝐵𝑖)
585102, 367, 584nf3an 1887 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖))
586 nfv 1896 . . . . . . . . . . . . . . . . . . . . 21 𝑗(1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)
587585, 586nfim 1882 . . . . . . . . . . . . . . . . . . . 20 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
588 fveq2 6545 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → (𝐵𝑗) = (𝐵𝑖))
589588eleq2d 2870 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑖 → (𝑡 ∈ (𝐵𝑗) ↔ 𝑡 ∈ (𝐵𝑖)))
590371, 5893anbi23d 1431 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖))))
591386breq2d 4980 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → ((1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)))
592590, 591imbi12d 346 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))))
593 stoweidlem34.18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡))
594587, 592, 593chvar 2371 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
595580, 594syld3an1 1403 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
596516, 529, 544, 57, 545, 546, 547, 566, 567, 568, 569, 570, 571, 579, 595stoweidlem26 41875 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠))
597515, 596vtoclg 3513 . . . . . . . . . . . . . . . 16 (𝑡𝑇 → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
598597ad2antlr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
599598pm2.43i 52 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
600505, 599vtoclg 3513 . . . . . . . . . . . . 13 (𝑗 ∈ (𝐽𝑡) → (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
601600ad2antrl 724 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
602601pm2.43i 52 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
603493, 602jca 512 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
604254, 363, 6033jca 1121 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
605604ex 413 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))) → (𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
606104, 605eximd 2183 . . . . . . 7 ((𝜑𝑡𝑇) → (∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
607253, 606mpd 15 . . . . . 6 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
608 3anass 1088 . . . . . . 7 ((𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ (𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
609608exbii 1833 . . . . . 6 (∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
610607, 609sylib 219 . . . . 5 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
611 df-rex 3113 . . . . 5 (∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
612610, 611sylibr 235 . . . 4 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
613 nfcv 2951 . . . . 5 𝑗
61493, 613ssrexf 3958 . . . 4 ((𝐽𝑡) ⊆ ℝ → (∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
61514, 612, 614sylc 65 . . 3 ((𝜑𝑡𝑇) → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
616615ex 413 . 2 (𝜑 → (𝑡𝑇 → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
6171, 616ralrimi 3185 1 (𝜑 → ∀𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 842  w3a 1080  wal 1523   = wceq 1525  wex 1765  wnf 1769  wcel 2083  wnfc 2935  wne 2986  wral 3107  wrex 3108  {crab 3111  Vcvv 3440  cdif 3862  wss 3865  c0 4217   class class class wbr 4968  cmpt 5047  wf 6228  cfv 6232  (class class class)co 7023  cc 10388  cr 10389  0cc0 10390  1c1 10391   + caddc 10393   · cmul 10395  *cxr 10527   < clt 10528  cle 10529  cmin 10723  -cneg 10724   / cdiv 11151  cn 11492  3c3 11547  4c4 11548  0cn0 11751  cz 11835  cuz 12097  +crp 12243  ...cfz 12746  Σcsu 14880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-inf2 8957  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-pre-sup 10468
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-fal 1538  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-oadd 7964  df-er 8146  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-sup 8759  df-oi 8827  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-4 11556  df-n0 11752  df-z 11836  df-uz 12098  df-rp 12244  df-ico 12598  df-fz 12747  df-fzo 12888  df-seq 13224  df-exp 13284  df-hash 13545  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-clim 14683  df-sum 14881
This theorem is referenced by:  stoweidlem60  41909
  Copyright terms: Public domain W3C validator