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

Theorem stoweidlem34 42663
 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 488 . . . . . . . 8 ((𝜑𝑡𝑇) → 𝑡𝑇)
3 ovex 7172 . . . . . . . . 9 (1...𝑁) ∈ V
43rabex 5202 . . . . . . . 8 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ∈ V
5 stoweidlem34.6 . . . . . . . . 9 𝐽 = (𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
65fvmpt2 6760 . . . . . . . 8 ((𝑡𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ∈ V) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
72, 4, 6sylancl 589 . . . . . . 7 ((𝜑𝑡𝑇) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
8 ssrab2 4010 . . . . . . 7 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ⊆ (1...𝑁)
97, 8eqsstrdi 3972 . . . . . 6 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ (1...𝑁))
10 elfznn 12935 . . . . . . 7 (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
1110ssriv 3922 . . . . . 6 (1...𝑁) ⊆ ℕ
129, 11sstrdi 3930 . . . . 5 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ ℕ)
13 nnssre 11633 . . . . 5 ℕ ⊆ ℝ
1412, 13sstrdi 3930 . . . 4 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ ℝ)
15 stoweidlem34.7 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
1615adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → 𝑁 ∈ ℕ)
17 nnuz 12273 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
1816, 17eleqtrdi 2903 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 𝑁 ∈ (ℤ‘1))
19 eluzfz2 12914 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
2018, 19syl 17 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑁 ∈ (1...𝑁))
21 stoweidlem34.11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝐹𝑡) < ((𝑁 − 1) · 𝐸))
22 3re 11709 . . . . . . . . . . . . . . . . . . . . 21 3 ∈ ℝ
23 3ne0 11735 . . . . . . . . . . . . . . . . . . . . 21 3 ≠ 0
2422, 23rereccli 11398 . . . . . . . . . . . . . . . . . . . 20 (1 / 3) ∈ ℝ
2524a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (1 / 3) ∈ ℝ)
26 1red 10635 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 1 ∈ ℝ)
2716nnred 11644 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 𝑁 ∈ ℝ)
28 1lt3 11802 . . . . . . . . . . . . . . . . . . . . 21 1 < 3
2922, 28pm3.2i 474 . . . . . . . . . . . . . . . . . . . 20 (3 ∈ ℝ ∧ 1 < 3)
30 recgt1i 11530 . . . . . . . . . . . . . . . . . . . . 21 ((3 ∈ ℝ ∧ 1 < 3) → (0 < (1 / 3) ∧ (1 / 3) < 1))
3130simprd 499 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℝ ∧ 1 < 3) → (1 / 3) < 1)
3229, 31mp1i 13 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (1 / 3) < 1)
3325, 26, 27, 32ltsub2dd 11246 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝑇) → (𝑁 − 1) < (𝑁 − (1 / 3)))
3427, 26resubcld 11061 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (𝑁 − 1) ∈ ℝ)
3527, 25resubcld 11061 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (𝑁 − (1 / 3)) ∈ ℝ)
36 stoweidlem34.12 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸 ∈ ℝ+)
3736rpred 12423 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐸 ∈ ℝ)
3837adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 𝐸 ∈ ℝ)
3936rpgt0d 12426 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝐸)
4039adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 0 < 𝐸)
41 ltmul1 11483 . . . . . . . . . . . . . . . . . . 19 (((𝑁 − 1) ∈ ℝ ∧ (𝑁 − (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
4234, 35, 38, 40, 41syl112anc 1371 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝑇) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
4333, 42mpbid 235 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸))
4421, 43jca 515 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → ((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
45 stoweidlem34.9 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑇⟶ℝ)
4645ffvelrnda 6832 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
4734, 38remulcld 10664 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − 1) · 𝐸) ∈ ℝ)
4835, 38remulcld 10664 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ)
49 lttr 10710 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸)))
50 ltle 10722 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
51503adant2 1128 . . . . . . . . . . . . . . . . . 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 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5444, 53mpd 15 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))
55 rabid 3334 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
562, 54, 55sylanbrc 586 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
57 stoweidlem34.4 . . . . . . . . . . . . . . . 16 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
58 oveq1 7146 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → (𝑗 − (1 / 3)) = (𝑁 − (1 / 3)))
5958oveq1d 7154 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑁 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑁 − (1 / 3)) · 𝐸))
6059breq2d 5045 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑁 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
6160rabbidv 3430 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑁 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
62 nnnn0 11896 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
63 nn0uz 12272 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
6462, 63eleqtrdi 2903 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘0))
65 eluzfz2 12914 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
6615, 64, 653syl 18 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (0...𝑁))
67 stoweidlem34.8 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ V)
68 rabexg 5201 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V)
6967, 68syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V)
7057, 61, 66, 69fvmptd3 6772 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7170adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7256, 71eleqtrrd 2896 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑡 ∈ (𝐷𝑁))
73 nfcv 2958 . . . . . . . . . . . . . 14 𝑗𝑁
74 nfcv 2958 . . . . . . . . . . . . . 14 𝑗(1...𝑁)
75 nfmpt1 5131 . . . . . . . . . . . . . . . . 17 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7657, 75nfcxfr 2956 . . . . . . . . . . . . . . . 16 𝑗𝐷
7776, 73nffv 6659 . . . . . . . . . . . . . . 15 𝑗(𝐷𝑁)
7877nfcri 2946 . . . . . . . . . . . . . 14 𝑗 𝑡 ∈ (𝐷𝑁)
79 fveq2 6649 . . . . . . . . . . . . . . 15 (𝑗 = 𝑁 → (𝐷𝑗) = (𝐷𝑁))
8079eleq2d 2878 . . . . . . . . . . . . . 14 (𝑗 = 𝑁 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑁)))
8173, 74, 78, 80elrabf 3627 . . . . . . . . . . . . 13 (𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ↔ (𝑁 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑁)))
8220, 72, 81sylanbrc 586 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → 𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
8382, 7eleqtrrd 2896 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝑁 ∈ (𝐽𝑡))
84 ne0i 4253 . . . . . . . . . . 11 (𝑁 ∈ (𝐽𝑡) → (𝐽𝑡) ≠ ∅)
8583, 84syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐽𝑡) ≠ ∅)
86 nnwo 12305 . . . . . . . . . . 11 (((𝐽𝑡) ⊆ ℕ ∧ (𝐽𝑡) ≠ ∅) → ∃𝑖 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑖𝑘)
87 nfcv 2958 . . . . . . . . . . . 12 𝑖(𝐽𝑡)
88 nfcv 2958 . . . . . . . . . . . . . . 15 𝑗𝑇
89 nfrab1 3340 . . . . . . . . . . . . . . 15 𝑗{𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)}
9088, 89nfmpt 5130 . . . . . . . . . . . . . 14 𝑗(𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
915, 90nfcxfr 2956 . . . . . . . . . . . . 13 𝑗𝐽
92 nfcv 2958 . . . . . . . . . . . . 13 𝑗𝑡
9391, 92nffv 6659 . . . . . . . . . . . 12 𝑗(𝐽𝑡)
94 nfv 1915 . . . . . . . . . . . . 13 𝑗 𝑖𝑘
9593, 94nfralw 3192 . . . . . . . . . . . 12 𝑗𝑘 ∈ (𝐽𝑡)𝑖𝑘
96 nfv 1915 . . . . . . . . . . . 12 𝑖𝑘 ∈ (𝐽𝑡)𝑗𝑘
97 breq1 5036 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (𝑖𝑘𝑗𝑘))
9897ralbidv 3165 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (∀𝑘 ∈ (𝐽𝑡)𝑖𝑘 ↔ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘))
9987, 93, 95, 96, 98cbvrexfw 3387 . . . . . . . . . . 11 (∃𝑖 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑖𝑘 ↔ ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
10086, 99sylib 221 . . . . . . . . . 10 (((𝐽𝑡) ⊆ ℕ ∧ (𝐽𝑡) ≠ ∅) → ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
10112, 85, 100syl2anc 587 . . . . . . . . 9 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
102 stoweidlem34.2 . . . . . . . . . . 11 𝑗𝜑
103 nfv 1915 . . . . . . . . . . 11 𝑗 𝑡𝑇
104102, 103nfan 1900 . . . . . . . . . 10 𝑗(𝜑𝑡𝑇)
1057eleq2d 2878 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) ↔ 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)}))
106105biimpa 480 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
107 rabid 3334 . . . . . . . . . . . . . . 15 (𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)))
108106, 107sylib 221 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)))
109108simprd 499 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑡 ∈ (𝐷𝑗))
110109adantr 484 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → 𝑡 ∈ (𝐷𝑗))
111 simp3 1135 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑡 ∈ (𝐷‘(𝑗 − 1)))
112 simp1l 1194 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝜑)
113 noel 4250 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ 𝑡 ∈ ∅
114 oveq1 7146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 = 1 → (𝑗 − 1) = (1 − 1))
115 1m1e0 11701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 − 1) = 0
116114, 115eqtrdi 2852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 = 1 → (𝑗 − 1) = 0)
117116fveq2d 6653 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 = 1 → (𝐷‘(𝑗 − 1)) = (𝐷‘0))
11822a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑡𝑇) → 3 ∈ ℝ)
11923a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑡𝑇) → 3 ≠ 0)
12026, 118, 119redivcld 11461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑡𝑇) → (1 / 3) ∈ ℝ)
121120renegcld 11060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → -(1 / 3) ∈ ℝ)
122121, 38remulcld 10664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) ∈ ℝ)
123 0red 10637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → 0 ∈ ℝ)
124 3pos 11734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
12522, 124recgt0ii 11539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
126 lt0neg2 11140 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((1 / 3) ∈ ℝ → (0 < (1 / 3) ↔ -(1 / 3) < 0))
12724, 126ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (0 < (1 / 3) ↔ -(1 / 3) < 0)
128125, 127mpbi 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 -(1 / 3) < 0
129 ltmul1 11483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((-(1 / 3) ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (-(1 / 3) < 0 ↔ (-(1 / 3) · 𝐸) < (0 · 𝐸)))
130121, 123, 38, 40, 129syl112anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑡𝑇) → (-(1 / 3) < 0 ↔ (-(1 / 3) · 𝐸) < (0 · 𝐸)))
131128, 130mpbii 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < (0 · 𝐸))
132 mul02lem2 10810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐸 ∈ ℝ → (0 · 𝐸) = 0)
13338, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → (0 · 𝐸) = 0)
134131, 133breqtrd 5059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < 0)
135 stoweidlem34.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → 0 ≤ (𝐹𝑡))
136122, 123, 46, 134, 135ltletrd 10793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < (𝐹𝑡))
137122, 46ltnled 10780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑡𝑇) → ((-(1 / 3) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
138136, 137mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑡𝑇) → ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸))
139 nan 828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸))) ↔ ((𝜑𝑡𝑇) → ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
140138, 139mpbir 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
141 rabid 3334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
142140, 141sylnibr 332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
143 oveq1 7146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 0 → (𝑗 − (1 / 3)) = (0 − (1 / 3)))
144 df-neg 10866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 -(1 / 3) = (0 − (1 / 3))
145143, 144eqtr4di 2854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 = 0 → (𝑗 − (1 / 3)) = -(1 / 3))
146145oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 = 0 → ((𝑗 − (1 / 3)) · 𝐸) = (-(1 / 3) · 𝐸))
147146breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 = 0 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
148147rabbidv 3430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 0 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
14915nnnn0d 11947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑁 ∈ ℕ0)
150 elnn0uz 12275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
151149, 150sylib 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝑁 ∈ (ℤ‘0))
152 eluzfz1 12913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ (ℤ‘0) → 0 ∈ (0...𝑁))
153151, 152syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → 0 ∈ (0...𝑁))
154 rabexg 5201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V)
15567, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V)
15657, 148, 153, 155fvmptd3 6772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝐷‘0) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
157142, 156neleqtrrd 2915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ¬ 𝑡 ∈ (𝐷‘0))
1581, 157alrimi 2212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0))
159 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑡(0...𝑁)
160 nfrab1 3340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑡{𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
161159, 160nfmpt 5130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
16257, 161nfcxfr 2956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑡𝐷
163 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑡0
164162, 163nffv 6659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑡(𝐷‘0)
165164eq0f 4258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐷‘0) = ∅ ↔ ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0))
166158, 165sylibr 237 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐷‘0) = ∅)
167117, 166sylan9eqr 2858 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 = 1) → (𝐷‘(𝑗 − 1)) = ∅)
168167eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 = 1) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ ∅))
169113, 168mtbiri 330 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 = 1) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
170169ex 416 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑗 = 1 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
171170con2d 136 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ 𝑗 = 1))
172112, 111, 171sylc 65 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 = 1)
173 simplll 774 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → 𝜑)
174105, 107syl6bb 290 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗))))
175174simprbda 502 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ (1...𝑁))
17615, 17eleqtrdi 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ (ℤ‘1))
177176adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (𝐽𝑡)) → 𝑁 ∈ (ℤ‘1))
178 elfzp12 12985 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
180179adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
181175, 180mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁)))
182181orcanai 1000 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → 𝑗 ∈ ((1 + 1)...𝑁))
183 fzssp1 12949 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1...(𝑁 − 1)) ⊆ (1...((𝑁 − 1) + 1))
18415nncnd 11645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℂ)
185 1cnd 10629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → 1 ∈ ℂ)
186184, 185npcand 10994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
187186oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
188183, 187sseqtrid 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
189188adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
190 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ((1 + 1)...𝑁))
191 1z 12004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ∈ ℤ
192 zaddcl 12014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1 ∈ ℤ ∧ 1 ∈ ℤ) → (1 + 1) ∈ ℤ)
193191, 191, 192mp2an 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 + 1) ∈ ℤ
194193a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (1 + 1) ∈ ℤ)
19515nnzd 12078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℤ)
196195adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑁 ∈ ℤ)
197 elfzelz 12906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ((1 + 1)...𝑁) → 𝑗 ∈ ℤ)
198197adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ℤ)
199 1zzd 12005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 1 ∈ ℤ)
200 fzsubel 12942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
201194, 196, 198, 199, 200syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
202190, 201mpbid 235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
203 ax-1cn 10588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
204203, 203pncan3oi 10895 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 + 1) − 1) = 1
205204oveq1i 7149 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
206202, 205eleqtrdi 2903 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...(𝑁 − 1)))
207189, 206sseldd 3919 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...𝑁))
208173, 182, 207syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → (𝑗 − 1) ∈ (1...𝑁))
209208ex 416 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁)))
2102093adant3 1129 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁)))
211172, 210mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (1...𝑁))
212 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑗 − 1) → (𝐷𝑖) = (𝐷‘(𝑗 − 1)))
213212eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑗 − 1) → (𝑡 ∈ (𝐷𝑖) ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
214213elrab3 3632 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 − 1) ∈ (1...𝑁) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
215211, 214syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
216111, 215mpbird 260 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)})
217 nfcv 2958 . . . . . . . . . . . . . . . . . . . 20 𝑖(1...𝑁)
218 nfv 1915 . . . . . . . . . . . . . . . . . . . 20 𝑖 𝑡 ∈ (𝐷𝑗)
219 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . 22 𝑗𝑖
22076, 219nffv 6659 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝐷𝑖)
221220nfcri 2946 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑡 ∈ (𝐷𝑖)
222 fveq2 6649 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
223222eleq2d 2878 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑖)))
22474, 217, 218, 221, 223cbvrabw 3440 . . . . . . . . . . . . . . . . . . 19 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} = {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)}
225216, 224eleqtrrdi 2904 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
22673ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
227225, 226eleqtrrd 2896 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (𝐽𝑡))
228 elfzelz 12906 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ ℤ)
229 zre 11977 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
230175, 228, 2293syl 18 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ ℝ)
2312303adant3 1129 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑗 ∈ ℝ)
232 peano2rem 10946 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
233 ltm1 11475 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → (𝑗 − 1) < 𝑗)
234233adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → (𝑗 − 1) < 𝑗)
235 ltnle 10713 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 − 1) ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
236235ancoms 462 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → ((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
237234, 236mpbid 235 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → ¬ 𝑗 ≤ (𝑗 − 1))
238231, 232, 237syl2anc2 588 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 ≤ (𝑗 − 1))
239 breq2 5037 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑗 − 1) → (𝑗𝑘𝑗 ≤ (𝑗 − 1)))
240239notbid 321 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑗 − 1) → (¬ 𝑗𝑘 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
241240rspcev 3574 . . . . . . . . . . . . . . . . 17 (((𝑗 − 1) ∈ (𝐽𝑡) ∧ ¬ 𝑗 ≤ (𝑗 − 1)) → ∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘)
242227, 238, 241syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘)
243 rexnal 3204 . . . . . . . . . . . . . . . 16 (∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘 ↔ ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
244242, 243sylib 221 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
2452443expia 1118 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘))
246245con2d 136 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (∀𝑘 ∈ (𝐽𝑡)𝑗𝑘 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
247246imp 410 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
248110, 247eldifd 3895 . . . . . . . . . . 11 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
249248exp31 423 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) → (∀𝑘 ∈ (𝐽𝑡)𝑗𝑘𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))))
250104, 249reximdai 3273 . . . . . . . . 9 ((𝜑𝑡𝑇) → (∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘 → ∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
251101, 250mpd 15 . . . . . . . 8 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
252 df-rex 3115 . . . . . . . 8 (∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
253251, 252sylib 221 . . . . . . 7 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
254 simprl 770 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (𝐽𝑡))
255 eldifn 4058 . . . . . . . . . . . . 13 (𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
256 simplr 768 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑡𝑇)
257 simpll 766 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝜑)
258175adantrr 716 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ (1...𝑁))
259 simprr 772 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
260 oveq1 7146 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑘 → (𝑗 − (1 / 3)) = (𝑘 − (1 / 3)))
261260oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑘 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑘 − (1 / 3)) · 𝐸))
262261breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 𝑘 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)))
263262rabbidv 3430 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑘 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
264263cbvmptv 5136 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
26557, 264eqtri 2824 . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
266 oveq1 7146 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑗 − 1) → (𝑘 − (1 / 3)) = ((𝑗 − 1) − (1 / 3)))
267266oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑗 − 1) → ((𝑘 − (1 / 3)) · 𝐸) = (((𝑗 − 1) − (1 / 3)) · 𝐸))
268267breq2d 5045 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 − 1) → ((𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)))
269268rabbidv 3430 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑗 − 1) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
270 fzssp1 12949 . . . . . . . . . . . . . . . . . . . . . . . 24 (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
271186oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
272270, 271sseqtrid 3970 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
273272adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
274 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
275 1zzd 12005 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 1 ∈ ℤ)
276195adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℤ)
277228adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℤ)
278 fzsubel 12942 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
279275, 276, 277, 275, 278syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
280274, 279mpbid 235 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1)))
281115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → (1 − 1) = 0)
282281oveq1d 7154 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝑁)) → ((1 − 1)...(𝑁 − 1)) = (0...(𝑁 − 1)))
283280, 282eleqtrd 2895 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
284273, 283sseldd 3919 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...𝑁))
28567adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑇 ∈ V)
286 rabexg 5201 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V)
287285, 286syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V)
288265, 269, 284, 287fvmptd3 6772 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐷‘(𝑗 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
289288eleq2d 2878 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}))
290289notbid 321 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → (¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}))
291290biimpa 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
292257, 258, 259, 291syl21anc 836 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
293 rabid 3334 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)))
294230adantrr 716 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ ℝ)
295 recn 10620 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → 𝑗 ∈ ℂ)
296 1cnd 10629 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → 1 ∈ ℂ)
297 1re 10634 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
298297, 22, 233pm3.2i 1336 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0)
299 redivcl 11352 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (1 / 3) ∈ ℝ)
300 recn 10620 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 / 3) ∈ ℝ → (1 / 3) ∈ ℂ)
301298, 299, 300mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 / 3) ∈ ℂ
302301a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → (1 / 3) ∈ ℂ)
303295, 296, 302subsub4d 11021 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) = (𝑗 − (1 + (1 / 3))))
304 3cn 11710 . . . . . . . . . . . . . . . . . . . . . . . . . 26 3 ∈ ℂ
305304, 203, 304, 23divdiri 11390 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
306 3p1e4 11774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 + 1) = 4
307306oveq1i 7149 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 + 1) / 3) = (4 / 3)
308304, 23dividi 11366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 / 3) = 1
309308oveq1i 7149 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
310305, 307, 3093eqtr3i 2832 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 / 3) = (1 + (1 / 3))
311310a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → (4 / 3) = (1 + (1 / 3)))
312311oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℝ → (𝑗 − (4 / 3)) = (𝑗 − (1 + (1 / 3))))
313303, 312eqtr4d 2839 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) = (𝑗 − (4 / 3)))
314313oveq1d 7154 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
315294, 314syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
316315breq2d 5045 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
317316anbi2d 631 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝑡𝑇 ∧ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)) ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))))
318293, 317syl5bb 286 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))))
319292, 318mtbid 327 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
320 imnan 403 . . . . . . . . . . . . . . 15 ((𝑡𝑇 → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)) ↔ ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
321319, 320sylibr 237 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡𝑇 → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
322256, 321mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))
323255, 322sylanr2 682 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))
324230adantrr 716 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ ℝ)
325 4re 11713 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ
326325a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 4 ∈ ℝ)
32722a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ∈ ℝ)
32823a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ≠ 0)
329326, 327, 328redivcld 11461 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (4 / 3) ∈ ℝ)
330324, 329resubcld 11061 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 − (4 / 3)) ∈ ℝ)
33137ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ)
332 remulcl 10615 . . . . . . . . . . . . . . 15 (((𝑗 − (4 / 3)) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ)
333332rexrd 10684 . . . . . . . . . . . . . 14 (((𝑗 − (4 / 3)) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*)
334330, 331, 333syl2anc 587 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*)
33546rexrd 10684 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ*)
336335adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹𝑡) ∈ ℝ*)
337 xrltnle 10701 . . . . . . . . . . . . 13 ((((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ* ∧ (𝐹𝑡) ∈ ℝ*) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
338334, 336, 337syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
339323, 338mpbird 260 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡))
340 simpl 486 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝜑𝑡𝑇))
341 simprr 772 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
342341eldifad 3896 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ (𝐷𝑗))
343 simplll 774 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝜑)
344175adantr 484 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑗 ∈ (1...𝑁))
345 simpr 488 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ (𝐷𝑗))
346 oveq1 7146 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑗 → (𝑘 − (1 / 3)) = (𝑗 − (1 / 3)))
347346oveq1d 7154 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → ((𝑘 − (1 / 3)) · 𝐸) = ((𝑗 − (1 / 3)) · 𝐸))
348347breq2d 5045 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → ((𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
349348rabbidv 3430 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
350 fz1ssfz0 13002 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ⊆ (0...𝑁)
351350sseli 3914 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ (0...𝑁))
352351adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (0...𝑁))
353 rabexg 5201 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
354285, 353syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
355265, 349, 352, 354fvmptd3 6772 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
356355eleq2d 2878 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}))
357356biimpa 480 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
358343, 344, 345, 357syl21anc 836 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
359 rabid 3334 . . . . . . . . . . . . . 14 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
360358, 359sylib 221 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
361360simprd 499 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
362340, 254, 342, 361syl21anc 836 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
363339, 362jca 515 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
36415ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑁 ∈ ℕ)
365 simplr 768 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡𝑇)
366175adantrr 716 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (1...𝑁))
367 nfv 1915 . . . . . . . . . . . . . . . 16 𝑗 𝑖 ∈ (0...𝑁)
368102, 367nfan 1900 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁))
369 nfv 1915 . . . . . . . . . . . . . . 15 𝑗(𝑋𝑖):𝑇⟶ℝ
370368, 369nfim 1897 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
371 eleq1w 2875 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑗 ∈ (0...𝑁) ↔ 𝑖 ∈ (0...𝑁)))
372371anbi2d 631 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑖 ∈ (0...𝑁))))
373 fveq2 6649 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑋𝑗) = (𝑋𝑖))
374373feq1d 6476 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑋𝑗):𝑇⟶ℝ ↔ (𝑋𝑖):𝑇⟶ℝ))
375372, 374imbi12d 348 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ) ↔ ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)))
376 stoweidlem34.14 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ)
377370, 375, 376chvarfv 2241 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
378377ad4ant14 751 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
379 simplll 774 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝜑)
380 simpr 488 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁))
381 simpllr 775 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑡𝑇)
382102, 367, 103nf3an 1902 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇)
383 nfv 1915 . . . . . . . . . . . . . . 15 𝑗((𝑋𝑖)‘𝑡) ≤ 1
384382, 383nfim 1897 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)
3853713anbi2d 1438 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇)))
386373fveq1d 6651 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → ((𝑋𝑗)‘𝑡) = ((𝑋𝑖)‘𝑡))
387386breq1d 5043 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (((𝑋𝑗)‘𝑡) ≤ 1 ↔ ((𝑋𝑖)‘𝑡) ≤ 1))
388385, 387imbi12d 348 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)))
389 stoweidlem34.16 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1)
390384, 388, 389chvarfv 2241 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)
391379, 380, 381, 390syl3anc 1368 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑡) ≤ 1)
392 simplll 774 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑)
393 0zd 11985 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ)
394 elfzel2 12904 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑁 ∈ ℤ)
395394adantl 485 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ)
396 elfzelz 12906 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℤ)
397396adantl 485 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ)
398393, 395, 3973jca 1125 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
399 0red 10637 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℝ)
400 elfzel1 12905 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℤ)
401400zred 12079 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℝ)
402401adantl 485 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ)
403396zred 12079 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℝ)
404403adantl 485 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
405 0red 10637 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ∈ ℝ)
406 1red 10635 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 1 ∈ ℝ)
407 0le1 11156 . . . . . . . . . . . . . . . . . . . 20 0 ≤ 1
408407a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ≤ 1)
409 elfzle1 12909 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...𝑁) → 1 ≤ 𝑗)
410175, 409syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 1 ≤ 𝑗)
411405, 406, 230, 408, 410letrd 10790 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ≤ 𝑗)
412411adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑗)
413 elfzle1 12909 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑗𝑖)
414413adantl 485 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗𝑖)
415399, 402, 404, 412, 414letrd 10790 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑖)
416 elfzle2 12910 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑖𝑁)
417416adantl 485 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖𝑁)
418415, 417jca 515 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖𝑖𝑁))
419 elfz2 12896 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑁)))
420398, 418, 419sylanbrc 586 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
421420adantlrr 720 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
422 simpll 766 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑𝑡𝑇))
423 simplrl 776 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽𝑡))
424 simplrr 777 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
425424eldifad 3896 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑗))
426 simpr 488 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁))
427 simpl1 1188 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑𝑡𝑇))
428427simprd 499 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡𝑇)
429427, 46syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ∈ ℝ)
430401adantl 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ)
43124a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈ ℝ)
432430, 431resubcld 11061 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
433 simpl1l 1221 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑)
434433, 37syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
435432, 434remulcld 10664 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
436403adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
43724a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈ ℝ)
438436, 437resubcld 11061 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈ ℝ)
43937adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
440438, 439remulcld 10664 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ)
441433, 440sylancom 591 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ)
442 simpl3 1190 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑗))
443 simpl2 1189 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽𝑡))
444427, 443, 175syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (1...𝑁))
445433, 444, 355syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
446442, 445eleqtrd 2895 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
447446, 359sylib 221 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
448447simprd 499 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
449403adantl 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
450413adantl 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗𝑖)
451430, 449, 431, 450lesub1dd 11249 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)))
452433, 438sylancom 591 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈ ℝ)
45336rpregt0d 12429 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
454433, 453syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
455 lemul1 11485 . . . . . . . . . . . . . . . . . . 19 (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑖 − (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
456432, 452, 454, 455syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
457451, 456mpbid 235 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸))
458429, 435, 441, 448, 457letrd 10790 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸))
459 rabid 3334 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
460428, 458, 459sylanbrc 586 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
461 simpr 488 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁))
462 0zd 11985 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ)
4633943ad2ant3 1132 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ)
4643963ad2ant3 1132 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ)
465462, 463, 4643jca 1125 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
4664183impa 1107 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖𝑖𝑁))
467465, 466, 419sylanbrc 586 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
468427, 443, 461, 467syl3anc 1368 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
469 oveq1 7146 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 − (1 / 3)) = (𝑖 − (1 / 3)))
470469oveq1d 7154 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑖 − (1 / 3)) · 𝐸))
471470breq2d 5045 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
472471rabbidv 3430 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
473 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁))
474 rabexg 5201 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
47567, 474syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
476475adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
47757, 472, 473, 476fvmptd3 6772 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
478433, 468, 477syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
479460, 478eleqtrrd 2896 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑖))
480422, 423, 425, 426, 479syl31anc 1370 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑖))
481102, 367, 221nf3an 1902 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖))
482 nfv 1915 . . . . . . . . . . . . . . 15 𝑗((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁)
483481, 482nfim 1897 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
484371, 2233anbi23d 1436 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖))))
485386breq1d 5043 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁)))
486484, 485imbi12d 348 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))))
487 stoweidlem34.17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁))
488483, 486, 487chvarfv 2241 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
489392, 421, 480, 488syl3anc 1368 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
49036ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ+)
491 stoweidlem34.13 . . . . . . . . . . . . 13 (𝜑𝐸 < (1 / 3))
492491ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 < (1 / 3))
493364, 365, 366, 378, 391, 489, 490, 492stoweidlem11 42640 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸))
494 eleq1w 2875 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑙 ∈ (𝐽𝑡) ↔ 𝑗 ∈ (𝐽𝑡)))
495 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑗 → (𝐷𝑙) = (𝐷𝑗))
496 oveq1 7146 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 → (𝑙 − 1) = (𝑗 − 1))
497496fveq2d 6653 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑗 → (𝐷‘(𝑙 − 1)) = (𝐷‘(𝑗 − 1)))
498495, 497difeq12d 4054 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑗 → ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) = ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
499498eleq2d 2878 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
500494, 499anbi12d 633 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑗 → ((𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))))
501500anbi2d 631 . . . . . . . . . . . . . . 15 (𝑙 = 𝑗 → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))))
502 oveq1 7146 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑙 − (4 / 3)) = (𝑗 − (4 / 3)))
503502oveq1d 7154 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑗 → ((𝑙 − (4 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
504503breq1d 5043 . . . . . . . . . . . . . . 15 (𝑙 = 𝑗 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) ↔ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
505501, 504imbi12d 348 . . . . . . . . . . . . . 14 (𝑙 = 𝑗 → ((((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)) ↔ (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
506 eleq1w 2875 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑠𝑇𝑡𝑇))
507506anbi2d 631 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝜑𝑠𝑇) ↔ (𝜑𝑡𝑇)))
508 fveq2 6649 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑡 → (𝐽𝑠) = (𝐽𝑡))
509508eleq2d 2878 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑙 ∈ (𝐽𝑠) ↔ 𝑙 ∈ (𝐽𝑡)))
510 eleq1w 2875 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
511509, 510anbi12d 633 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))))
512507, 511anbi12d 633 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))))
513 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠) = ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
514513breq2d 5045 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠) ↔ ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
515512, 514imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠)) ↔ (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
516 stoweidlem34.1 . . . . . . . . . . . . . . . . . 18 𝑡𝐹
517 nfv 1915 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑠𝑇
518102, 517nfan 1900 . . . . . . . . . . . . . . . . . . 19 𝑗(𝜑𝑠𝑇)
519 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . 22 𝑗𝑠
52091, 519nffv 6659 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝐽𝑠)
521520nfcri 2946 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑙 ∈ (𝐽𝑠)
522 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗𝑙
52376, 522nffv 6659 . . . . . . . . . . . . . . . . . . . . . 22 𝑗(𝐷𝑙)
524 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗(𝑙 − 1)
52576, 524nffv 6659 . . . . . . . . . . . . . . . . . . . . . 22 𝑗(𝐷‘(𝑙 − 1))
526523, 525nfdif 4056 . . . . . . . . . . . . . . . . . . . . 21 𝑗((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
527526nfcri 2946 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
528521, 527nfan 1900 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
529518, 528nfan 1900 . . . . . . . . . . . . . . . . . 18 𝑗((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
530 nfv 1915 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑠𝑇
5311, 530nfan 1900 . . . . . . . . . . . . . . . . . . 19 𝑡(𝜑𝑠𝑇)
532 nfmpt1 5131 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
5335, 532nfcxfr 2956 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝐽
534 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝑠
535533, 534nffv 6659 . . . . . . . . . . . . . . . . . . . . 21 𝑡(𝐽𝑠)
536535nfcri 2946 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑙 ∈ (𝐽𝑠)
537 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝑙
538162, 537nffv 6659 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝐷𝑙)
539 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑙 − 1)
540162, 539nffv 6659 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝐷‘(𝑙 − 1))
541538, 540nfdif 4056 . . . . . . . . . . . . . . . . . . . . 21 𝑡((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
542541nfcri 2946 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
543536, 542nfan 1900 . . . . . . . . . . . . . . . . . . 19 𝑡(𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
544531, 543nfan 1900 . . . . . . . . . . . . . . . . . 18 𝑡((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
545 stoweidlem34.5 . . . . . . . . . . . . . . . . . 18 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
54615ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑁 ∈ ℕ)
54767ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑇 ∈ V)
5483rabex 5202 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ∈ V
549 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑡𝑗
550162, 549nffv 6659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡(𝐷𝑗)
551550nfcri 2946 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 𝑠 ∈ (𝐷𝑗)
552 nfcv 2958 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(1...𝑁)
553551, 552nfrabw 3341 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡{𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)}
554 eleq1w 2875 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑠 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑠 ∈ (𝐷𝑗)))
555554rabbidv 3430 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑠 → {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
556534, 553, 555, 5fvmptf 6770 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ∈ V) → (𝐽𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
557548, 556mpan2 690 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠𝑇 → (𝐽𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
558557eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠𝑇 → (𝑙 ∈ (𝐽𝑠) ↔ 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)}))
559558biimpa 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
560523nfcri 2946 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 𝑠 ∈ (𝐷𝑙)
561 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑙 → (𝐷𝑗) = (𝐷𝑙))
562561eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑙 → (𝑠 ∈ (𝐷𝑗) ↔ 𝑠 ∈ (𝐷𝑙)))
563522, 74, 560, 562elrabf 3627 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ↔ (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷𝑙)))
564559, 563sylib 221 . . . . . . . . . . . . . . . . . . . 20 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷𝑙)))
565564simpld 498 . . . . . . . . . . . . . . . . . . 19 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → 𝑙 ∈ (1...𝑁))
566565ad2ant2lr 747 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑙 ∈ (1...𝑁))
567 simprr 772 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
56845ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐹:𝑇⟶ℝ)
56936ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 ∈ ℝ+)
570491ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 < (1 / 3))
571377ad4ant14 751 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
572 simp1ll 1233 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 𝜑)
573 nfv 1915 . . . . . . . . . . . . . . . . . . . . 21 𝑗0 ≤ ((𝑋𝑖)‘𝑡)
574382, 573nfim 1897 . . . . . . . . . . . . . . . . . . . 20 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
575386breq2d 5045 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (0 ≤ ((𝑋𝑗)‘𝑡) ↔ 0 ≤ ((𝑋𝑖)‘𝑡)))
576385, 575imbi12d 348 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))))
577 stoweidlem34.15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡))
578574, 576, 577chvarfv 2241 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
579572, 578syld3an1 1407 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
580 simp1ll 1233 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → 𝜑)
581 nfmpt1 5131 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
582545, 581nfcxfr 2956 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑗𝐵
583582, 219nffv 6659 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗(𝐵𝑖)
584583nfcri 2946 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 𝑡 ∈ (𝐵𝑖)
585102, 367, 584nf3an 1902 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖))
586 nfv 1915 . . . . . . . . . . . . . . . . . . . . 21 𝑗(1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)
587585, 586nfim 1897 . . . . . . . . . . . . . . . . . . . 20 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
588 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → (𝐵𝑗) = (𝐵𝑖))
589588eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑖 → (𝑡 ∈ (𝐵𝑗) ↔ 𝑡 ∈ (𝐵𝑖)))
590371, 5893anbi23d 1436 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖))))
591386breq2d 5045 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → ((1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)))
592590, 591imbi12d 348 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))))
593 stoweidlem34.18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡))
594587, 592, 593chvarfv 2241 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
595580, 594syld3an1 1407 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
596516, 529, 544, 57, 545, 546, 547, 566, 567, 568, 569, 570, 571, 579, 595stoweidlem26 42655 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠))
597515, 596vtoclg 3518 . . . . . . . . . . . . . . . 16 (𝑡𝑇 → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
598597ad2antlr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
599598pm2.43i 52 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
600505, 599vtoclg 3518 . . . . . . . . . . . . 13 (𝑗 ∈ (𝐽𝑡) → (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
601600ad2antrl 727 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
602601pm2.43i 52 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
603493, 602jca 515 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
604254, 363, 6033jca 1125 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
605604ex 416 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))) → (𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
606104, 605eximd 2215 . . . . . . 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 1092 . . . . . . 7 ((𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ (𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
609608exbii 1849 . . . . . 6 (∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
610607, 609sylib 221 . . . . 5 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
611 df-rex 3115 . . . . 5 (∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
612610, 611sylibr 237 . . . 4 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
613 nfcv 2958 . . . . 5 𝑗
61493, 613ssrexf 3982 . . . 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 416 . 2 (𝜑 → (𝑡𝑇 → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
6171, 616ralrimi 3183 1 (𝜑 → ∀𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084  ∀wal 1536   = wceq 1538  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2112  Ⅎwnfc 2939   ≠ wne 2990  ∀wral 3109  ∃wrex 3110  {crab 3113  Vcvv 3444   ∖ cdif 3881   ⊆ wss 3884  ∅c0 4246   class class class wbr 5033   ↦ cmpt 5113  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139  ℂcc 10528  ℝcr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535  ℝ*cxr 10667   < clt 10668   ≤ cle 10669   − cmin 10863  -cneg 10864   / cdiv 11290  ℕcn 11629  3c3 11685  4c4 11686  ℕ0cn0 11889  ℤcz 11973  ℤ≥cuz 12235  ℝ+crp 12381  ...cfz 12889  Σcsu 15037 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-sup 8894  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-n0 11890  df-z 11974  df-uz 12236  df-rp 12382  df-ico 12736  df-fz 12890  df-fzo 13033  df-seq 13369  df-exp 13430  df-hash 13691  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-sum 15038 This theorem is referenced by:  stoweidlem60  42689
 Copyright terms: Public domain W3C validator