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

Theorem stoweidlem34 38927
 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 476 . . . . . . . 8 ((𝜑𝑡𝑇) → 𝑡𝑇)
3 ovex 6577 . . . . . . . . 9 (1...𝑁) ∈ V
43rabex 4740 . . . . . . . 8 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ∈ V
5 stoweidlem34.6 . . . . . . . . 9 𝐽 = (𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
65fvmpt2 6200 . . . . . . . 8 ((𝑡𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ∈ V) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
72, 4, 6sylancl 693 . . . . . . 7 ((𝜑𝑡𝑇) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
8 ssrab2 3650 . . . . . . 7 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ⊆ (1...𝑁)
97, 8syl6eqss 3618 . . . . . 6 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ (1...𝑁))
10 elfznn 12241 . . . . . . 7 (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
1110ssriv 3572 . . . . . 6 (1...𝑁) ⊆ ℕ
129, 11syl6ss 3580 . . . . 5 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ ℕ)
13 nnssre 10901 . . . . 5 ℕ ⊆ ℝ
1412, 13syl6ss 3580 . . . 4 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ ℝ)
15 stoweidlem34.7 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
1615adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → 𝑁 ∈ ℕ)
17 nnuz 11599 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
1816, 17syl6eleq 2698 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 𝑁 ∈ (ℤ‘1))
19 eluzfz2 12220 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
2018, 19syl 17 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑁 ∈ (1...𝑁))
21 stoweidlem34.11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝐹𝑡) < ((𝑁 − 1) · 𝐸))
22 3re 10971 . . . . . . . . . . . . . . . . . . . . 21 3 ∈ ℝ
23 3ne0 10992 . . . . . . . . . . . . . . . . . . . . 21 3 ≠ 0
2422, 23rereccli 10669 . . . . . . . . . . . . . . . . . . . 20 (1 / 3) ∈ ℝ
2524a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (1 / 3) ∈ ℝ)
26 1red 9934 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 1 ∈ ℝ)
2716nnred 10912 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 𝑁 ∈ ℝ)
28 1lt3 11073 . . . . . . . . . . . . . . . . . . . . 21 1 < 3
2922, 28pm3.2i 470 . . . . . . . . . . . . . . . . . . . 20 (3 ∈ ℝ ∧ 1 < 3)
30 recgt1i 10799 . . . . . . . . . . . . . . . . . . . . 21 ((3 ∈ ℝ ∧ 1 < 3) → (0 < (1 / 3) ∧ (1 / 3) < 1))
3130simprd 478 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℝ ∧ 1 < 3) → (1 / 3) < 1)
3229, 31mp1i 13 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (1 / 3) < 1)
3325, 26, 27, 32ltsub2dd 10519 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝑇) → (𝑁 − 1) < (𝑁 − (1 / 3)))
3427, 26resubcld 10337 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (𝑁 − 1) ∈ ℝ)
3527, 25resubcld 10337 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (𝑁 − (1 / 3)) ∈ ℝ)
36 stoweidlem34.12 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸 ∈ ℝ+)
3736rpred 11748 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐸 ∈ ℝ)
3837adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 𝐸 ∈ ℝ)
3936rpgt0d 11751 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝐸)
4039adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 0 < 𝐸)
41 ltmul1 10752 . . . . . . . . . . . . . . . . . . 19 (((𝑁 − 1) ∈ ℝ ∧ (𝑁 − (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
4234, 35, 38, 40, 41syl112anc 1322 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝑇) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
4333, 42mpbid 221 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸))
4421, 43jca 553 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → ((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
45 stoweidlem34.9 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑇⟶ℝ)
4645fnvinran 38196 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
4734, 38remulcld 9949 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − 1) · 𝐸) ∈ ℝ)
4835, 38remulcld 9949 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ)
49 lttr 9993 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸)))
50 ltle 10005 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
51503adant2 1073 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5249, 51syld 46 . . . . . . . . . . . . . . . . 17 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5346, 47, 48, 52syl3anc 1318 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5444, 53mpd 15 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))
55 rabid 3095 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
562, 54, 55sylanbrc 695 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
57 nnnn0 11176 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
58 nn0uz 11598 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
5957, 58syl6eleq 2698 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘0))
60 eluzfz2 12220 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
6115, 59, 603syl 18 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (0...𝑁))
62 stoweidlem34.8 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ V)
63 rabexg 4739 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V)
6462, 63syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V)
65 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑁 → (𝑗 − (1 / 3)) = (𝑁 − (1 / 3)))
6665oveq1d 6564 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑁 − (1 / 3)) · 𝐸))
6766breq2d 4595 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑁 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
6867rabbidv 3164 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑁 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
69 stoweidlem34.4 . . . . . . . . . . . . . . . . 17 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7068, 69fvmptg 6189 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7161, 64, 70syl2anc 691 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7271adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7356, 72eleqtrrd 2691 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑡 ∈ (𝐷𝑁))
74 nfcv 2751 . . . . . . . . . . . . . 14 𝑗𝑁
75 nfcv 2751 . . . . . . . . . . . . . 14 𝑗(1...𝑁)
76 nfmpt1 4675 . . . . . . . . . . . . . . . . 17 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7769, 76nfcxfr 2749 . . . . . . . . . . . . . . . 16 𝑗𝐷
7877, 74nffv 6110 . . . . . . . . . . . . . . 15 𝑗(𝐷𝑁)
7978nfcri 2745 . . . . . . . . . . . . . 14 𝑗 𝑡 ∈ (𝐷𝑁)
80 fveq2 6103 . . . . . . . . . . . . . . 15 (𝑗 = 𝑁 → (𝐷𝑗) = (𝐷𝑁))
8180eleq2d 2673 . . . . . . . . . . . . . 14 (𝑗 = 𝑁 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑁)))
8274, 75, 79, 81elrabf 3329 . . . . . . . . . . . . 13 (𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ↔ (𝑁 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑁)))
8320, 73, 82sylanbrc 695 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → 𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
8483, 7eleqtrrd 2691 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝑁 ∈ (𝐽𝑡))
85 ne0i 3880 . . . . . . . . . . 11 (𝑁 ∈ (𝐽𝑡) → (𝐽𝑡) ≠ ∅)
8684, 85syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐽𝑡) ≠ ∅)
87 nnwo 11629 . . . . . . . . . . 11 (((𝐽𝑡) ⊆ ℕ ∧ (𝐽𝑡) ≠ ∅) → ∃𝑖 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑖𝑘)
88 nfcv 2751 . . . . . . . . . . . 12 𝑖(𝐽𝑡)
89 nfcv 2751 . . . . . . . . . . . . . . 15 𝑗𝑇
90 nfrab1 3099 . . . . . . . . . . . . . . 15 𝑗{𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)}
9189, 90nfmpt 4674 . . . . . . . . . . . . . 14 𝑗(𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
925, 91nfcxfr 2749 . . . . . . . . . . . . 13 𝑗𝐽
93 nfcv 2751 . . . . . . . . . . . . 13 𝑗𝑡
9492, 93nffv 6110 . . . . . . . . . . . 12 𝑗(𝐽𝑡)
95 nfv 1830 . . . . . . . . . . . . 13 𝑗 𝑖𝑘
9694, 95nfral 2929 . . . . . . . . . . . 12 𝑗𝑘 ∈ (𝐽𝑡)𝑖𝑘
97 nfv 1830 . . . . . . . . . . . 12 𝑖𝑘 ∈ (𝐽𝑡)𝑗𝑘
98 breq1 4586 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (𝑖𝑘𝑗𝑘))
9998ralbidv 2969 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (∀𝑘 ∈ (𝐽𝑡)𝑖𝑘 ↔ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘))
10088, 94, 96, 97, 99cbvrexf 3142 . . . . . . . . . . 11 (∃𝑖 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑖𝑘 ↔ ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
10187, 100sylib 207 . . . . . . . . . 10 (((𝐽𝑡) ⊆ ℕ ∧ (𝐽𝑡) ≠ ∅) → ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
10212, 86, 101syl2anc 691 . . . . . . . . 9 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
103 stoweidlem34.2 . . . . . . . . . . 11 𝑗𝜑
104 nfv 1830 . . . . . . . . . . 11 𝑗 𝑡𝑇
105103, 104nfan 1816 . . . . . . . . . 10 𝑗(𝜑𝑡𝑇)
1067eleq2d 2673 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) ↔ 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)}))
107106biimpa 500 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
108 rabid 3095 . . . . . . . . . . . . . . 15 (𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)))
109107, 108sylib 207 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)))
110109simprd 478 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑡 ∈ (𝐷𝑗))
111110adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → 𝑡 ∈ (𝐷𝑗))
112 simp3 1056 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑡 ∈ (𝐷‘(𝑗 − 1)))
113 simp1l 1078 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝜑)
114 noel 3878 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ 𝑡 ∈ ∅
115 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 = 1 → (𝑗 − 1) = (1 − 1))
116 1m1e0 10966 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 − 1) = 0
117115, 116syl6eq 2660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 = 1 → (𝑗 − 1) = 0)
118117fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 = 1 → (𝐷‘(𝑗 − 1)) = (𝐷‘0))
11922a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑡𝑇) → 3 ∈ ℝ)
12023a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑡𝑇) → 3 ≠ 0)
12126, 119, 120redivcld 10732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑡𝑇) → (1 / 3) ∈ ℝ)
122121renegcld 10336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → -(1 / 3) ∈ ℝ)
123122, 38remulcld 9949 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) ∈ ℝ)
124 0red 9920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → 0 ∈ ℝ)
125 3pos 10991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
12622, 125recgt0ii 10808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
127 lt0neg2 10414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((1 / 3) ∈ ℝ → (0 < (1 / 3) ↔ -(1 / 3) < 0))
12824, 127ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (0 < (1 / 3) ↔ -(1 / 3) < 0)
129126, 128mpbi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 -(1 / 3) < 0
130 ltmul1 10752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((-(1 / 3) ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (-(1 / 3) < 0 ↔ (-(1 / 3) · 𝐸) < (0 · 𝐸)))
131122, 124, 38, 40, 130syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑡𝑇) → (-(1 / 3) < 0 ↔ (-(1 / 3) · 𝐸) < (0 · 𝐸)))
132129, 131mpbii 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < (0 · 𝐸))
133 mul02lem2 10092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐸 ∈ ℝ → (0 · 𝐸) = 0)
13438, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → (0 · 𝐸) = 0)
135132, 134breqtrd 4609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < 0)
136 stoweidlem34.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → 0 ≤ (𝐹𝑡))
137123, 124, 46, 135, 136ltletrd 10076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < (𝐹𝑡))
138123, 46ltnled 10063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑡𝑇) → ((-(1 / 3) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
139137, 138mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑡𝑇) → ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸))
140 nan 602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸))) ↔ ((𝜑𝑡𝑇) → ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
141139, 140mpbir 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
142 rabid 3095 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
143141, 142sylnibr 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
14415nnnn0d 11228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑁 ∈ ℕ0)
145 elnn0uz 11601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
146144, 145sylib 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝑁 ∈ (ℤ‘0))
147 eluzfz1 12219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ (ℤ‘0) → 0 ∈ (0...𝑁))
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → 0 ∈ (0...𝑁))
149 rabexg 4739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V)
15062, 149syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V)
151 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 = 0 → (𝑗 − (1 / 3)) = (0 − (1 / 3)))
152 df-neg 10148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 -(1 / 3) = (0 − (1 / 3))
153151, 152syl6eqr 2662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 0 → (𝑗 − (1 / 3)) = -(1 / 3))
154153oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 = 0 → ((𝑗 − (1 / 3)) · 𝐸) = (-(1 / 3) · 𝐸))
155154breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 = 0 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
156155rabbidv 3164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 = 0 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
157156, 69fvmptg 6189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V) → (𝐷‘0) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
158148, 150, 157syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝐷‘0) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
159143, 158neleqtrrd 2710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ¬ 𝑡 ∈ (𝐷‘0))
1601, 159alrimi 2069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0))
161 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑡(0...𝑁)
162 nfrab1 3099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑡{𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
163161, 162nfmpt 4674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
16469, 163nfcxfr 2749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑡𝐷
165 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑡0
166164, 165nffv 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑡(𝐷‘0)
167166eq0f 3884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐷‘0) = ∅ ↔ ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0))
168160, 167sylibr 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐷‘0) = ∅)
169118, 168sylan9eqr 2666 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 = 1) → (𝐷‘(𝑗 − 1)) = ∅)
170169eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 = 1) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ ∅))
171114, 170mtbiri 316 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 = 1) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
172171ex 449 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑗 = 1 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
173172con2d 128 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ 𝑗 = 1))
174113, 112, 173sylc 63 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 = 1)
175 simplll 794 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → 𝜑)
176106, 108syl6bb 275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗))))
177176simprbda 651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ (1...𝑁))
17815, 17syl6eleq 2698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ (ℤ‘1))
179178adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (𝐽𝑡)) → 𝑁 ∈ (ℤ‘1))
180 elfzp12 12288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
181179, 180syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
182181adantlr 747 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
183177, 182mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁)))
184183orcanai 950 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → 𝑗 ∈ ((1 + 1)...𝑁))
185 fzssp1 12255 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1...(𝑁 − 1)) ⊆ (1...((𝑁 − 1) + 1))
18615nncnd 10913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℂ)
187 1cnd 9935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → 1 ∈ ℂ)
188186, 187npcand 10275 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
189188oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
190185, 189syl5sseq 3616 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
191190adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
192 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ((1 + 1)...𝑁))
193 1z 11284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ∈ ℤ
194 zaddcl 11294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1 ∈ ℤ ∧ 1 ∈ ℤ) → (1 + 1) ∈ ℤ)
195193, 193, 194mp2an 704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 + 1) ∈ ℤ
196195a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (1 + 1) ∈ ℤ)
19715nnzd 11357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℤ)
198197adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑁 ∈ ℤ)
199 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ((1 + 1)...𝑁) → 𝑗 ∈ ℤ)
200199adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ℤ)
201 1zzd 11285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 1 ∈ ℤ)
202 fzsubel 12248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
203196, 198, 200, 201, 202syl22anc 1319 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
204192, 203mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
205 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
206205, 205pncan3oi 10176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 + 1) − 1) = 1
207206oveq1i 6559 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
208204, 207syl6eleq 2698 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...(𝑁 − 1)))
209191, 208sseldd 3569 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...𝑁))
210175, 184, 209syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → (𝑗 − 1) ∈ (1...𝑁))
211210ex 449 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁)))
2122113adant3 1074 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁)))
213174, 212mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (1...𝑁))
214 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑗 − 1) → (𝐷𝑖) = (𝐷‘(𝑗 − 1)))
215214eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑗 − 1) → (𝑡 ∈ (𝐷𝑖) ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
216215elrab3 3332 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 − 1) ∈ (1...𝑁) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
217213, 216syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
218112, 217mpbird 246 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)})
219 nfcv 2751 . . . . . . . . . . . . . . . . . . . 20 𝑖(1...𝑁)
220 nfv 1830 . . . . . . . . . . . . . . . . . . . 20 𝑖 𝑡 ∈ (𝐷𝑗)
221 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . 22 𝑗𝑖
22277, 221nffv 6110 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝐷𝑖)
223222nfcri 2745 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑡 ∈ (𝐷𝑖)
224 fveq2 6103 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
225224eleq2d 2673 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑖)))
22675, 219, 220, 223, 225cbvrab 3171 . . . . . . . . . . . . . . . . . . 19 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} = {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)}
227218, 226syl6eleqr 2699 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
22873ad2ant1 1075 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
229227, 228eleqtrrd 2691 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (𝐽𝑡))
230 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ ℤ)
231 zre 11258 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
232177, 230, 2313syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ ℝ)
2332323adant3 1074 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑗 ∈ ℝ)
234 peano2rem 10227 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
235233, 234jccir 560 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ))
236 ltm1 10742 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → (𝑗 − 1) < 𝑗)
237236adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → (𝑗 − 1) < 𝑗)
238 ltnle 9996 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 − 1) ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
239238ancoms 468 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → ((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
240237, 239mpbid 221 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → ¬ 𝑗 ≤ (𝑗 − 1))
241235, 240syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 ≤ (𝑗 − 1))
242 breq2 4587 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑗 − 1) → (𝑗𝑘𝑗 ≤ (𝑗 − 1)))
243242notbid 307 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑗 − 1) → (¬ 𝑗𝑘 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
244243rspcev 3282 . . . . . . . . . . . . . . . . 17 (((𝑗 − 1) ∈ (𝐽𝑡) ∧ ¬ 𝑗 ≤ (𝑗 − 1)) → ∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘)
245229, 241, 244syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘)
246 rexnal 2978 . . . . . . . . . . . . . . . 16 (∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘 ↔ ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
247245, 246sylib 207 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
2482473expia 1259 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘))
249248con2d 128 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (∀𝑘 ∈ (𝐽𝑡)𝑗𝑘 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
250249imp 444 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
251111, 250eldifd 3551 . . . . . . . . . . 11 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
252251exp31 628 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) → (∀𝑘 ∈ (𝐽𝑡)𝑗𝑘𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))))
253105, 252reximdai 2995 . . . . . . . . 9 ((𝜑𝑡𝑇) → (∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘 → ∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
254102, 253mpd 15 . . . . . . . 8 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
255 df-rex 2902 . . . . . . . 8 (∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
256254, 255sylib 207 . . . . . . 7 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
257 simprl 790 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (𝐽𝑡))
258 eldifn 3695 . . . . . . . . . . . . 13 (𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
259 simplr 788 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑡𝑇)
260 simpll 786 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝜑)
261177adantrr 749 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ (1...𝑁))
262 simprr 792 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
263 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 = 𝑘 → (𝑗 − (1 / 3)) = (𝑘 − (1 / 3)))
264263oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑘 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑘 − (1 / 3)) · 𝐸))
265264breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑘 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)))
266265rabbidv 3164 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 𝑘 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
267266cbvmptv 4678 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
26869, 267eqtri 2632 . . . . . . . . . . . . . . . . . . . . . 22 𝐷 = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
269268a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → 𝐷 = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)}))
270 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = (𝑗 − 1) → (𝑘 − (1 / 3)) = ((𝑗 − 1) − (1 / 3)))
271270oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑗 − 1) → ((𝑘 − (1 / 3)) · 𝐸) = (((𝑗 − 1) − (1 / 3)) · 𝐸))
272271breq2d 4595 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑗 − 1) → ((𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)))
273272rabbidv 3164 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 − 1) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
274273adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 = (𝑗 − 1)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
275 fzssp1 12255 . . . . . . . . . . . . . . . . . . . . . . . 24 (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
276188oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
277275, 276syl5sseq 3616 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
278277adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
279 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
280 1zzd 11285 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 1 ∈ ℤ)
281197adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℤ)
282230adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℤ)
283 fzsubel 12248 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
284280, 281, 282, 280, 283syl22anc 1319 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
285279, 284mpbid 221 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1)))
286116a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → (1 − 1) = 0)
287286oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝑁)) → ((1 − 1)...(𝑁 − 1)) = (0...(𝑁 − 1)))
288285, 287eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
289278, 288sseldd 3569 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...𝑁))
29062adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑇 ∈ V)
291 rabexg 4739 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V)
292290, 291syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V)
293269, 274, 289, 292fvmptd 6197 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐷‘(𝑗 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
294293eleq2d 2673 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}))
295294notbid 307 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → (¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}))
296295biimpa 500 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
297260, 261, 262, 296syl21anc 1317 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
298 rabid 3095 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)))
299232adantrr 749 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ ℝ)
300 recn 9905 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → 𝑗 ∈ ℂ)
301 1cnd 9935 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → 1 ∈ ℂ)
302 1re 9918 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
303302, 22, 233pm3.2i 1232 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0)
304 redivcl 10623 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (1 / 3) ∈ ℝ)
305 recn 9905 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 / 3) ∈ ℝ → (1 / 3) ∈ ℂ)
306303, 304, 305mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 / 3) ∈ ℂ
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → (1 / 3) ∈ ℂ)
308300, 301, 307subsub4d 10302 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) = (𝑗 − (1 + (1 / 3))))
309 3cn 10972 . . . . . . . . . . . . . . . . . . . . . . . . . 26 3 ∈ ℂ
310309, 205, 309, 23divdiri 10661 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
311 3p1e4 11030 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 + 1) = 4
312311oveq1i 6559 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 + 1) / 3) = (4 / 3)
313309, 23dividi 10637 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 / 3) = 1
314313oveq1i 6559 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
315310, 312, 3143eqtr3i 2640 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 / 3) = (1 + (1 / 3))
316315a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → (4 / 3) = (1 + (1 / 3)))
317316oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℝ → (𝑗 − (4 / 3)) = (𝑗 − (1 + (1 / 3))))
318308, 317eqtr4d 2647 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) = (𝑗 − (4 / 3)))
319318oveq1d 6564 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
320299, 319syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
321320breq2d 4595 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
322321anbi2d 736 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝑡𝑇 ∧ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)) ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))))
323298, 322syl5bb 271 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))))
324297, 323mtbid 313 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
325 imnan 437 . . . . . . . . . . . . . . 15 ((𝑡𝑇 → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)) ↔ ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
326324, 325sylibr 223 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡𝑇 → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
327259, 326mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))
328258, 327sylanr2 683 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))
329232adantrr 749 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ ℝ)
330 4re 10974 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ
331330a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 4 ∈ ℝ)
33222a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ∈ ℝ)
33323a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ≠ 0)
334331, 332, 333redivcld 10732 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (4 / 3) ∈ ℝ)
335329, 334resubcld 10337 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 − (4 / 3)) ∈ ℝ)
33637ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ)
337 remulcl 9900 . . . . . . . . . . . . . . 15 (((𝑗 − (4 / 3)) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ)
338337rexrd 9968 . . . . . . . . . . . . . 14 (((𝑗 − (4 / 3)) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*)
339335, 336, 338syl2anc 691 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*)
34046rexrd 9968 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ*)
341340adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹𝑡) ∈ ℝ*)
342 xrltnle 9984 . . . . . . . . . . . . 13 ((((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ* ∧ (𝐹𝑡) ∈ ℝ*) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
343339, 341, 342syl2anc 691 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
344328, 343mpbird 246 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡))
345 simpl 472 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝜑𝑡𝑇))
346 simprr 792 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
347346eldifad 3552 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ (𝐷𝑗))
348 simplll 794 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝜑)
349177adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑗 ∈ (1...𝑁))
350 simpr 476 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ (𝐷𝑗))
351 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑗 → (𝑘 − (1 / 3)) = (𝑗 − (1 / 3)))
352351oveq1d 6564 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑗 → ((𝑘 − (1 / 3)) · 𝐸) = ((𝑗 − (1 / 3)) · 𝐸))
353352breq2d 4595 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → ((𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
354353rabbidv 3164 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
355354adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 = 𝑗) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
356 0p1e1 11009 . . . . . . . . . . . . . . . . . . . . . 22 (0 + 1) = 1
357356oveq1i 6559 . . . . . . . . . . . . . . . . . . . . 21 ((0 + 1)...𝑁) = (1...𝑁)
358 0z 11265 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℤ
359 fzp1ss 12262 . . . . . . . . . . . . . . . . . . . . . 22 (0 ∈ ℤ → ((0 + 1)...𝑁) ⊆ (0...𝑁))
360358, 359ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((0 + 1)...𝑁) ⊆ (0...𝑁)
361357, 360eqsstr3i 3599 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ⊆ (0...𝑁)
362361sseli 3564 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ (0...𝑁))
363362adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (0...𝑁))
364 rabexg 4739 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
365290, 364syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
366269, 355, 363, 365fvmptd 6197 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
367366eleq2d 2673 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}))
368367biimpa 500 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
369348, 349, 350, 368syl21anc 1317 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
370 rabid 3095 . . . . . . . . . . . . . 14 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
371369, 370sylib 207 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
372371simprd 478 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
373345, 257, 347, 372syl21anc 1317 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
374344, 373jca 553 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
37515ad2antrr 758 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑁 ∈ ℕ)
376 simplr 788 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡𝑇)
377177adantrr 749 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (1...𝑁))
378 nfv 1830 . . . . . . . . . . . . . . . 16 𝑗 𝑖 ∈ (0...𝑁)
379103, 378nfan 1816 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁))
380 nfv 1830 . . . . . . . . . . . . . . 15 𝑗(𝑋𝑖):𝑇⟶ℝ
381379, 380nfim 1813 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
382 eleq1 2676 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑗 ∈ (0...𝑁) ↔ 𝑖 ∈ (0...𝑁)))
383382anbi2d 736 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑖 ∈ (0...𝑁))))
384 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑋𝑗) = (𝑋𝑖))
385384feq1d 5943 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑋𝑗):𝑇⟶ℝ ↔ (𝑋𝑖):𝑇⟶ℝ))
386383, 385imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ) ↔ ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)))
387 stoweidlem34.14 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ)
388381, 386, 387chvar 2250 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
389388ad4ant14 1285 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
390 simplll 794 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝜑)
391 simpr 476 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁))
392 simpllr 795 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑡𝑇)
393103, 378, 104nf3an 1819 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇)
394 nfv 1830 . . . . . . . . . . . . . . 15 𝑗((𝑋𝑖)‘𝑡) ≤ 1
395393, 394nfim 1813 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)
3963823anbi2d 1396 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇)))
397384fveq1d 6105 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → ((𝑋𝑗)‘𝑡) = ((𝑋𝑖)‘𝑡))
398397breq1d 4593 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (((𝑋𝑗)‘𝑡) ≤ 1 ↔ ((𝑋𝑖)‘𝑡) ≤ 1))
399396, 398imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)))
400 stoweidlem34.16 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1)
401395, 399, 400chvar 2250 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)
402390, 391, 392, 401syl3anc 1318 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑡) ≤ 1)
403 simplll 794 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑)
404 0zd 11266 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ)
405 elfzel2 12211 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑁 ∈ ℤ)
406405adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ)
407 elfzelz 12213 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℤ)
408407adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ)
409404, 406, 4083jca 1235 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
410 0red 9920 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℝ)
411 elfzel1 12212 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℤ)
412411zred 11358 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℝ)
413412adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ)
414407zred 11358 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℝ)
415414adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
416 0red 9920 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ∈ ℝ)
417 1red 9934 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 1 ∈ ℝ)
418 0le1 10430 . . . . . . . . . . . . . . . . . . . 20 0 ≤ 1
419418a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ≤ 1)
420 elfzle1 12215 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...𝑁) → 1 ≤ 𝑗)
421177, 420syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 1 ≤ 𝑗)
422416, 417, 232, 419, 421letrd 10073 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ≤ 𝑗)
423422adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑗)
424 elfzle1 12215 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑗𝑖)
425424adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗𝑖)
426410, 413, 415, 423, 425letrd 10073 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑖)
427 elfzle2 12216 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑖𝑁)
428427adantl 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖𝑁)
429426, 428jca 553 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖𝑖𝑁))
430 elfz2 12204 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑁)))
431409, 429, 430sylanbrc 695 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
432431adantlrr 753 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
433 simpll 786 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑𝑡𝑇))
434 simplrl 796 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽𝑡))
435 simplrr 797 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
436435eldifad 3552 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑗))
437 simpr 476 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁))
438 simpl1 1057 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑𝑡𝑇))
439438simprd 478 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡𝑇)
440438, 46syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ∈ ℝ)
441412adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ)
44224a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈ ℝ)
443441, 442resubcld 10337 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
444 simpl1l 1105 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑)
445444, 37syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
446443, 445remulcld 9949 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
447414adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
44824a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈ ℝ)
449447, 448resubcld 10337 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈ ℝ)
45037adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
451449, 450remulcld 9949 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ)
452444, 451sylancom 698 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ)
453 simpl3 1059 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑗))
454 simpl2 1058 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽𝑡))
455438, 454, 177syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (1...𝑁))
456444, 455, 366syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
457453, 456eleqtrd 2690 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
458457, 370sylib 207 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
459458simprd 478 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
460414adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
461424adantl 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗𝑖)
462441, 460, 442, 461lesub1dd 10522 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)))
463444, 449sylancom 698 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈ ℝ)
46436rpregt0d 11754 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
465444, 464syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
466 lemul1 10754 . . . . . . . . . . . . . . . . . . 19 (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑖 − (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
467443, 463, 465, 466syl3anc 1318 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
468462, 467mpbid 221 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸))
469440, 446, 452, 459, 468letrd 10073 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸))
470 rabid 3095 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
471439, 469, 470sylanbrc 695 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
472 simpr 476 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁))
473 0zd 11266 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ)
4744053ad2ant3 1077 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ)
4754073ad2ant3 1077 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ)
476473, 474, 4753jca 1235 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
4774293impa 1251 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖𝑖𝑁))
478476, 477, 430sylanbrc 695 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
479438, 454, 472, 478syl3anc 1318 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
480 simpr 476 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁))
481 rabexg 4739 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
48262, 481syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
483482adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
484 oveq1 6556 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝑗 − (1 / 3)) = (𝑖 − (1 / 3)))
485484oveq1d 6564 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑖 − (1 / 3)) · 𝐸))
486485breq2d 4595 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
487486rabbidv 3164 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
488487, 69fvmptg 6189 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
489480, 483, 488syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
490444, 479, 489syl2anc 691 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
491471, 490eleqtrrd 2691 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑖))
492433, 434, 436, 437, 491syl31anc 1321 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑖))
493103, 378, 223nf3an 1819 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖))
494 nfv 1830 . . . . . . . . . . . . . . 15 𝑗((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁)
495493, 494nfim 1813 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
496382, 2253anbi23d 1394 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖))))
497397breq1d 4593 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁)))
498496, 497imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))))
499 stoweidlem34.17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁))
500495, 498, 499chvar 2250 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
501403, 432, 492, 500syl3anc 1318 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
50236ad2antrr 758 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ+)
503 stoweidlem34.13 . . . . . . . . . . . . 13 (𝜑𝐸 < (1 / 3))
504503ad2antrr 758 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 < (1 / 3))
505375, 376, 377, 389, 402, 501, 502, 504stoweidlem11 38904 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸))
506 eleq1 2676 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑙 ∈ (𝐽𝑡) ↔ 𝑗 ∈ (𝐽𝑡)))
507 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑗 → (𝐷𝑙) = (𝐷𝑗))
508 oveq1 6556 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 → (𝑙 − 1) = (𝑗 − 1))
509508fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑗 → (𝐷‘(𝑙 − 1)) = (𝐷‘(𝑗 − 1)))
510507, 509difeq12d 3691 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑗 → ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) = ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
511510eleq2d 2673 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
512506, 511anbi12d 743 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑗 → ((𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))))
513512anbi2d 736 . . . . . . . . . . . . . . 15 (𝑙 = 𝑗 → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))))
514 oveq1 6556 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑙 − (4 / 3)) = (𝑗 − (4 / 3)))
515514oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑗 → ((𝑙 − (4 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
516515breq1d 4593 . . . . . . . . . . . . . . 15 (𝑙 = 𝑗 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) ↔ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
517513, 516imbi12d 333 . . . . . . . . . . . . . 14 (𝑙 = 𝑗 → ((((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)) ↔ (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
518 eleq1 2676 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑠𝑇𝑡𝑇))
519518anbi2d 736 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝜑𝑠𝑇) ↔ (𝜑𝑡𝑇)))
520 fveq2 6103 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑡 → (𝐽𝑠) = (𝐽𝑡))
521520eleq2d 2673 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑙 ∈ (𝐽𝑠) ↔ 𝑙 ∈ (𝐽𝑡)))
522 eleq1 2676 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
523521, 522anbi12d 743 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))))
524519, 523anbi12d 743 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))))
525 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠) = ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
526525breq2d 4595 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠) ↔ ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
527524, 526imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠)) ↔ (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
528 stoweidlem34.1 . . . . . . . . . . . . . . . . . 18 𝑡𝐹
529 nfv 1830 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑠𝑇
530103, 529nfan 1816 . . . . . . . . . . . . . . . . . . 19 𝑗(𝜑𝑠𝑇)
531 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . 22 𝑗𝑠
53292, 531nffv 6110 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝐽𝑠)
533532nfcri 2745 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑙 ∈ (𝐽𝑠)
534 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗𝑙
53577, 534nffv 6110 . . . . . . . . . . . . . . . . . . . . . 22 𝑗(𝐷𝑙)
536 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗(𝑙 − 1)
53777, 536nffv 6110 . . . . . . . . . . . . . . . . . . . . . 22 𝑗(𝐷‘(𝑙 − 1))
538535, 537nfdif 3693 . . . . . . . . . . . . . . . . . . . . 21 𝑗((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
539538nfcri 2745 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
540533, 539nfan 1816 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
541530, 540nfan 1816 . . . . . . . . . . . . . . . . . 18 𝑗((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
542 nfv 1830 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑠𝑇
5431, 542nfan 1816 . . . . . . . . . . . . . . . . . . 19 𝑡(𝜑𝑠𝑇)
544 nfmpt1 4675 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
5455, 544nfcxfr 2749 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝐽
546 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝑠
547545, 546nffv 6110 . . . . . . . . . . . . . . . . . . . . 21 𝑡(𝐽𝑠)
548547nfcri 2745 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑙 ∈ (𝐽𝑠)
549 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝑙
550164, 549nffv 6110 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝐷𝑙)
551 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑙 − 1)
552164, 551nffv 6110 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝐷‘(𝑙 − 1))
553550, 552nfdif 3693 . . . . . . . . . . . . . . . . . . . . 21 𝑡((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
554553nfcri 2745 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
555548, 554nfan 1816 . . . . . . . . . . . . . . . . . . 19 𝑡(𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
556543, 555nfan 1816 . . . . . . . . . . . . . . . . . 18 𝑡((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
557 stoweidlem34.5 . . . . . . . . . . . . . . . . . 18 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
55815ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑁 ∈ ℕ)
55962ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑇 ∈ V)
5603rabex 4740 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ∈ V
561 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑡𝑗
562164, 561nffv 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡(𝐷𝑗)
563562nfcri 2745 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 𝑠 ∈ (𝐷𝑗)
564 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(1...𝑁)
565563, 564nfrab 3100 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡{𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)}
566 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑠 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑠 ∈ (𝐷𝑗)))
567566rabbidv 3164 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑠 → {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
568546, 565, 567, 5fvmptf 6209 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ∈ V) → (𝐽𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
569560, 568mpan2 703 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠𝑇 → (𝐽𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
570569eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠𝑇 → (𝑙 ∈ (𝐽𝑠) ↔ 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)}))
571570biimpa 500 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
572535nfcri 2745 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 𝑠 ∈ (𝐷𝑙)
573 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑙 → (𝐷𝑗) = (𝐷𝑙))
574573eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑙 → (𝑠 ∈ (𝐷𝑗) ↔ 𝑠 ∈ (𝐷𝑙)))
575534, 75, 572, 574elrabf 3329 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ↔ (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷𝑙)))
576571, 575sylib 207 . . . . . . . . . . . . . . . . . . . 20 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷𝑙)))
577576simpld 474 . . . . . . . . . . . . . . . . . . 19 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → 𝑙 ∈ (1...𝑁))
578577ad2ant2lr 780 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑙 ∈ (1...𝑁))
579 simprr 792 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
58045ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐹:𝑇⟶ℝ)
58136ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 ∈ ℝ+)
582503ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 < (1 / 3))
583388ad4ant14 1285 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
584 simp1ll 1117 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 𝜑)
585 nfv 1830 . . . . . . . . . . . . . . . . . . . . 21 𝑗0 ≤ ((𝑋𝑖)‘𝑡)
586393, 585nfim 1813 . . . . . . . . . . . . . . . . . . . 20 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
587397breq2d 4595 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (0 ≤ ((𝑋𝑗)‘𝑡) ↔ 0 ≤ ((𝑋𝑖)‘𝑡)))
588396, 587imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))))
589 stoweidlem34.15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡))
590586, 588, 589chvar 2250 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
591584, 590syld3an1 1364 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
592 simp1ll 1117 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → 𝜑)
593 nfmpt1 4675 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
594557, 593nfcxfr 2749 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑗𝐵
595594, 221nffv 6110 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗(𝐵𝑖)
596595nfcri 2745 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 𝑡 ∈ (𝐵𝑖)
597103, 378, 596nf3an 1819 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖))
598 nfv 1830 . . . . . . . . . . . . . . . . . . . . 21 𝑗(1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)
599597, 598nfim 1813 . . . . . . . . . . . . . . . . . . . 20 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
600 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → (𝐵𝑗) = (𝐵𝑖))
601600eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑖 → (𝑡 ∈ (𝐵𝑗) ↔ 𝑡 ∈ (𝐵𝑖)))
602382, 6013anbi23d 1394 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖))))
603397breq2d 4595 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → ((1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)))
604602, 603imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))))
605 stoweidlem34.18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡))
606599, 604, 605chvar 2250 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
607592, 606syld3an1 1364 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
608528, 541, 556, 69, 557, 558, 559, 578, 579, 580, 581, 582, 583, 591, 607stoweidlem26 38919 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠))
609527, 608vtoclg 3239 . . . . . . . . . . . . . . . 16 (𝑡𝑇 → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
610609ad2antlr 759 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
611610pm2.43i 50 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
612517, 611vtoclg 3239 . . . . . . . . . . . . 13 (𝑗 ∈ (𝐽𝑡) → (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
613612ad2antrl 760 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
614613pm2.43i 50 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
615505, 614jca 553 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
616257, 374, 6153jca 1235 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
617616ex 449 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))) → (𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
618105, 617eximd 2072 . . . . . . 7 ((𝜑𝑡𝑇) → (∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
619256, 618mpd 15 . . . . . 6 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
620 3anass 1035 . . . . . . 7 ((𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ (𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
621620exbii 1764 . . . . . 6 (∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
622619, 621sylib 207 . . . . 5 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
623 df-rex 2902 . . . . 5 (∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
624622, 623sylibr 223 . . . 4 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
625 nfcv 2751 . . . . 5 𝑗
62694, 625ssrexf 3628 . . . 4 ((𝐽𝑡) ⊆ ℝ → (∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
62714, 624, 626sylc 63 . . 3 ((𝜑𝑡𝑇) → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
628627ex 449 . 2 (𝜑 → (𝑡𝑇 → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
6291, 628ralrimi 2940 1 (𝜑 → ∀𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   ↦ cmpt 4643  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145  -cneg 10146   / cdiv 10563  ℕcn 10897  3c3 10948  4c4 10949  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ℝ+crp 11708  ...cfz 12197  Σcsu 14264 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-ico 12052  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265 This theorem is referenced by:  stoweidlem60  38953
 Copyright terms: Public domain W3C validator