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

Theorem stoweidlem34 38710
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 475 . . . . . . . 8 ((𝜑𝑡𝑇) → 𝑡𝑇)
3 ovex 6554 . . . . . . . . 9 (1...𝑁) ∈ V
43rabex 4734 . . . . . . . 8 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ∈ V
5 stoweidlem34.6 . . . . . . . . 9 𝐽 = (𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
65fvmpt2 6184 . . . . . . . 8 ((𝑡𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ∈ V) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
72, 4, 6sylancl 692 . . . . . . 7 ((𝜑𝑡𝑇) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
8 ssrab2 3649 . . . . . . 7 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ⊆ (1...𝑁)
97, 8syl6eqss 3617 . . . . . 6 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ (1...𝑁))
10 elfznn 12198 . . . . . . 7 (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
1110ssriv 3571 . . . . . 6 (1...𝑁) ⊆ ℕ
129, 11syl6ss 3579 . . . . 5 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ ℕ)
13 nnssre 10873 . . . . 5 ℕ ⊆ ℝ
1412, 13syl6ss 3579 . . . 4 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ ℝ)
15 stoweidlem34.7 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
1615adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → 𝑁 ∈ ℕ)
17 nnuz 11557 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
1816, 17syl6eleq 2697 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 𝑁 ∈ (ℤ‘1))
19 eluzfz2 12177 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
2018, 19syl 17 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑁 ∈ (1...𝑁))
21 stoweidlem34.11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝐹𝑡) < ((𝑁 − 1) · 𝐸))
22 3re 10943 . . . . . . . . . . . . . . . . . . . . 21 3 ∈ ℝ
23 3ne0 10964 . . . . . . . . . . . . . . . . . . . . 21 3 ≠ 0
2422, 23rereccli 10641 . . . . . . . . . . . . . . . . . . . 20 (1 / 3) ∈ ℝ
2524a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (1 / 3) ∈ ℝ)
26 1red 9911 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 1 ∈ ℝ)
2716nnred 10884 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 𝑁 ∈ ℝ)
28 1lt3 11045 . . . . . . . . . . . . . . . . . . . . 21 1 < 3
2922, 28pm3.2i 469 . . . . . . . . . . . . . . . . . . . 20 (3 ∈ ℝ ∧ 1 < 3)
30 recgt1i 10771 . . . . . . . . . . . . . . . . . . . . 21 ((3 ∈ ℝ ∧ 1 < 3) → (0 < (1 / 3) ∧ (1 / 3) < 1))
3130simprd 477 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℝ ∧ 1 < 3) → (1 / 3) < 1)
3229, 31mp1i 13 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (1 / 3) < 1)
3325, 26, 27, 32ltsub2dd 10491 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝑇) → (𝑁 − 1) < (𝑁 − (1 / 3)))
3427, 26resubcld 10309 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (𝑁 − 1) ∈ ℝ)
3527, 25resubcld 10309 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (𝑁 − (1 / 3)) ∈ ℝ)
36 stoweidlem34.12 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸 ∈ ℝ+)
3736rpred 11706 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐸 ∈ ℝ)
3837adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 𝐸 ∈ ℝ)
3936rpgt0d 11709 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝐸)
4039adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 0 < 𝐸)
41 ltmul1 10724 . . . . . . . . . . . . . . . . . . 19 (((𝑁 − 1) ∈ ℝ ∧ (𝑁 − (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
4234, 35, 38, 40, 41syl112anc 1321 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝑇) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
4333, 42mpbid 220 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸))
4421, 43jca 552 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → ((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
45 stoweidlem34.9 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑇⟶ℝ)
4645fnvinran 37979 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
4734, 38remulcld 9926 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − 1) · 𝐸) ∈ ℝ)
4835, 38remulcld 9926 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ)
49 lttr 9965 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸)))
50 ltle 9977 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
51503adant2 1072 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5249, 51syld 45 . . . . . . . . . . . . . . . . 17 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5346, 47, 48, 52syl3anc 1317 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5444, 53mpd 15 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))
55 rabid 3094 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
562, 54, 55sylanbrc 694 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
57 nnnn0 11148 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
58 nn0uz 11556 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
5957, 58syl6eleq 2697 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘0))
60 eluzfz2 12177 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
6115, 59, 603syl 18 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (0...𝑁))
62 stoweidlem34.8 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ V)
63 rabexg 4733 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V)
6462, 63syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V)
65 oveq1 6533 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑁 → (𝑗 − (1 / 3)) = (𝑁 − (1 / 3)))
6665oveq1d 6541 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑁 − (1 / 3)) · 𝐸))
6766breq2d 4589 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑁 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
6867rabbidv 3163 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑁 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
69 stoweidlem34.4 . . . . . . . . . . . . . . . . 17 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7068, 69fvmptg 6173 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7161, 64, 70syl2anc 690 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7271adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7356, 72eleqtrrd 2690 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑡 ∈ (𝐷𝑁))
74 nfcv 2750 . . . . . . . . . . . . . 14 𝑗𝑁
75 nfcv 2750 . . . . . . . . . . . . . 14 𝑗(1...𝑁)
76 nfmpt1 4669 . . . . . . . . . . . . . . . . 17 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7769, 76nfcxfr 2748 . . . . . . . . . . . . . . . 16 𝑗𝐷
7877, 74nffv 6094 . . . . . . . . . . . . . . 15 𝑗(𝐷𝑁)
7978nfcri 2744 . . . . . . . . . . . . . 14 𝑗 𝑡 ∈ (𝐷𝑁)
80 fveq2 6087 . . . . . . . . . . . . . . 15 (𝑗 = 𝑁 → (𝐷𝑗) = (𝐷𝑁))
8180eleq2d 2672 . . . . . . . . . . . . . 14 (𝑗 = 𝑁 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑁)))
8274, 75, 79, 81elrabf 3328 . . . . . . . . . . . . 13 (𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ↔ (𝑁 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑁)))
8320, 73, 82sylanbrc 694 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → 𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
8483, 7eleqtrrd 2690 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝑁 ∈ (𝐽𝑡))
85 ne0i 3879 . . . . . . . . . . 11 (𝑁 ∈ (𝐽𝑡) → (𝐽𝑡) ≠ ∅)
8684, 85syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐽𝑡) ≠ ∅)
87 nnwo 11587 . . . . . . . . . . 11 (((𝐽𝑡) ⊆ ℕ ∧ (𝐽𝑡) ≠ ∅) → ∃𝑖 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑖𝑘)
88 nfcv 2750 . . . . . . . . . . . 12 𝑖(𝐽𝑡)
89 nfcv 2750 . . . . . . . . . . . . . . 15 𝑗𝑇
90 nfrab1 3098 . . . . . . . . . . . . . . 15 𝑗{𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)}
9189, 90nfmpt 4668 . . . . . . . . . . . . . 14 𝑗(𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
925, 91nfcxfr 2748 . . . . . . . . . . . . 13 𝑗𝐽
93 nfcv 2750 . . . . . . . . . . . . 13 𝑗𝑡
9492, 93nffv 6094 . . . . . . . . . . . 12 𝑗(𝐽𝑡)
95 nfv 1829 . . . . . . . . . . . . 13 𝑗 𝑖𝑘
9694, 95nfral 2928 . . . . . . . . . . . 12 𝑗𝑘 ∈ (𝐽𝑡)𝑖𝑘
97 nfv 1829 . . . . . . . . . . . 12 𝑖𝑘 ∈ (𝐽𝑡)𝑗𝑘
98 breq1 4580 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (𝑖𝑘𝑗𝑘))
9998ralbidv 2968 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (∀𝑘 ∈ (𝐽𝑡)𝑖𝑘 ↔ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘))
10088, 94, 96, 97, 99cbvrexf 3141 . . . . . . . . . . 11 (∃𝑖 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑖𝑘 ↔ ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
10187, 100sylib 206 . . . . . . . . . 10 (((𝐽𝑡) ⊆ ℕ ∧ (𝐽𝑡) ≠ ∅) → ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
10212, 86, 101syl2anc 690 . . . . . . . . 9 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
103 stoweidlem34.2 . . . . . . . . . . 11 𝑗𝜑
104 nfv 1829 . . . . . . . . . . 11 𝑗 𝑡𝑇
105103, 104nfan 1815 . . . . . . . . . 10 𝑗(𝜑𝑡𝑇)
1067eleq2d 2672 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) ↔ 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)}))
107106biimpa 499 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
108 rabid 3094 . . . . . . . . . . . . . . 15 (𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)))
109107, 108sylib 206 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)))
110109simprd 477 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑡 ∈ (𝐷𝑗))
111110adantr 479 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → 𝑡 ∈ (𝐷𝑗))
112 simp3 1055 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑡 ∈ (𝐷‘(𝑗 − 1)))
113 simp1l 1077 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝜑)
114 noel 3877 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ 𝑡 ∈ ∅
115 oveq1 6533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 = 1 → (𝑗 − 1) = (1 − 1))
116 1m1e0 10938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 − 1) = 0
117115, 116syl6eq 2659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 = 1 → (𝑗 − 1) = 0)
118117fveq2d 6091 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 = 1 → (𝐷‘(𝑗 − 1)) = (𝐷‘0))
11922a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑡𝑇) → 3 ∈ ℝ)
12023a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑡𝑇) → 3 ≠ 0)
12126, 119, 120redivcld 10704 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑡𝑇) → (1 / 3) ∈ ℝ)
122121renegcld 10308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → -(1 / 3) ∈ ℝ)
123122, 38remulcld 9926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) ∈ ℝ)
124 0red 9897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → 0 ∈ ℝ)
125 3pos 10963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
12622, 125recgt0ii 10780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
127 lt0neg2 10386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((1 / 3) ∈ ℝ → (0 < (1 / 3) ↔ -(1 / 3) < 0))
12824, 127ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (0 < (1 / 3) ↔ -(1 / 3) < 0)
129126, 128mpbi 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 -(1 / 3) < 0
130 ltmul1 10724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((-(1 / 3) ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (-(1 / 3) < 0 ↔ (-(1 / 3) · 𝐸) < (0 · 𝐸)))
131122, 124, 38, 40, 130syl112anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑡𝑇) → (-(1 / 3) < 0 ↔ (-(1 / 3) · 𝐸) < (0 · 𝐸)))
132129, 131mpbii 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < (0 · 𝐸))
133 mul02lem2 10064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐸 ∈ ℝ → (0 · 𝐸) = 0)
13438, 133syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → (0 · 𝐸) = 0)
135132, 134breqtrd 4603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < 0)
136 stoweidlem34.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → 0 ≤ (𝐹𝑡))
137123, 124, 46, 135, 136ltletrd 10048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < (𝐹𝑡))
138123, 46ltnled 10035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑡𝑇) → ((-(1 / 3) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
139137, 138mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑡𝑇) → ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸))
140 nan 601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸))) ↔ ((𝜑𝑡𝑇) → ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
141139, 140mpbir 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
142 rabid 3094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
143141, 142sylnibr 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
14415nnnn0d 11200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑁 ∈ ℕ0)
145 elnn0uz 11559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
146144, 145sylib 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝑁 ∈ (ℤ‘0))
147 eluzfz1 12176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ (ℤ‘0) → 0 ∈ (0...𝑁))
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → 0 ∈ (0...𝑁))
149 rabexg 4733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V)
15062, 149syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V)
151 oveq1 6533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 = 0 → (𝑗 − (1 / 3)) = (0 − (1 / 3)))
152 df-neg 10120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 -(1 / 3) = (0 − (1 / 3))
153151, 152syl6eqr 2661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 0 → (𝑗 − (1 / 3)) = -(1 / 3))
154153oveq1d 6541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 = 0 → ((𝑗 − (1 / 3)) · 𝐸) = (-(1 / 3) · 𝐸))
155154breq2d 4589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 = 0 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
156155rabbidv 3163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 = 0 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
157156, 69fvmptg 6173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((0 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V) → (𝐷‘0) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
158148, 150, 157syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝐷‘0) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
159143, 158neleqtrrd 2709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ¬ 𝑡 ∈ (𝐷‘0))
1601, 159alrimi 2068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0))
161 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑡(0...𝑁)
162 nfrab1 3098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑡{𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
163161, 162nfmpt 4668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
16469, 163nfcxfr 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑡𝐷
165 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑡0
166164, 165nffv 6094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑡(𝐷‘0)
167166eq0f 3883 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐷‘0) = ∅ ↔ ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0))
168160, 167sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐷‘0) = ∅)
169118, 168sylan9eqr 2665 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 = 1) → (𝐷‘(𝑗 − 1)) = ∅)
170169eleq2d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 = 1) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ ∅))
171114, 170mtbiri 315 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 = 1) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
172171ex 448 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑗 = 1 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
173172con2d 127 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ 𝑗 = 1))
174113, 112, 173sylc 62 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 = 1)
175 simplll 793 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → 𝜑)
176106, 108syl6bb 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗))))
177176simprbda 650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ (1...𝑁))
17815, 17syl6eleq 2697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ (ℤ‘1))
179178adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (𝐽𝑡)) → 𝑁 ∈ (ℤ‘1))
180 elfzp12 12245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
181179, 180syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
182181adantlr 746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
183177, 182mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁)))
184183orcanai 949 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → 𝑗 ∈ ((1 + 1)...𝑁))
185 fzssp1 12212 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1...(𝑁 − 1)) ⊆ (1...((𝑁 − 1) + 1))
18615nncnd 10885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℂ)
187 1cnd 9912 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → 1 ∈ ℂ)
188186, 187npcand 10247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
189188oveq2d 6542 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
190185, 189syl5sseq 3615 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
191190adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
192 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ((1 + 1)...𝑁))
193 1z 11242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ∈ ℤ
194 zaddcl 11252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1 ∈ ℤ ∧ 1 ∈ ℤ) → (1 + 1) ∈ ℤ)
195193, 193, 194mp2an 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 + 1) ∈ ℤ
196195a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (1 + 1) ∈ ℤ)
19715nnzd 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℤ)
198197adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑁 ∈ ℤ)
199 elfzelz 12170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ((1 + 1)...𝑁) → 𝑗 ∈ ℤ)
200199adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ℤ)
201 1zzd 11243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 1 ∈ ℤ)
202 fzsubel 12205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
203196, 198, 200, 201, 202syl22anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
204192, 203mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
205 ax-1cn 9850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
206205, 205pncan3oi 10148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 + 1) − 1) = 1
207206oveq1i 6536 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
208204, 207syl6eleq 2697 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...(𝑁 − 1)))
209191, 208sseldd 3568 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...𝑁))
210175, 184, 209syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → (𝑗 − 1) ∈ (1...𝑁))
211210ex 448 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁)))
2122113adant3 1073 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁)))
213174, 212mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (1...𝑁))
214 fveq2 6087 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑗 − 1) → (𝐷𝑖) = (𝐷‘(𝑗 − 1)))
215214eleq2d 2672 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑗 − 1) → (𝑡 ∈ (𝐷𝑖) ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
216215elrab3 3331 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 − 1) ∈ (1...𝑁) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
217213, 216syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
218112, 217mpbird 245 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)})
219 nfcv 2750 . . . . . . . . . . . . . . . . . . . 20 𝑖(1...𝑁)
220 nfv 1829 . . . . . . . . . . . . . . . . . . . 20 𝑖 𝑡 ∈ (𝐷𝑗)
221 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . 22 𝑗𝑖
22277, 221nffv 6094 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝐷𝑖)
223222nfcri 2744 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑡 ∈ (𝐷𝑖)
224 fveq2 6087 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
225224eleq2d 2672 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑖)))
22675, 219, 220, 223, 225cbvrab 3170 . . . . . . . . . . . . . . . . . . 19 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} = {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)}
227218, 226syl6eleqr 2698 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
22873ad2ant1 1074 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
229227, 228eleqtrrd 2690 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (𝐽𝑡))
230 elfzelz 12170 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ ℤ)
231 zre 11216 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
232177, 230, 2313syl 18 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ ℝ)
2332323adant3 1073 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑗 ∈ ℝ)
234 peano2rem 10199 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
235233, 234jccir 559 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ))
236 ltm1 10714 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → (𝑗 − 1) < 𝑗)
237236adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → (𝑗 − 1) < 𝑗)
238 ltnle 9968 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 − 1) ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
239238ancoms 467 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → ((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
240237, 239mpbid 220 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → ¬ 𝑗 ≤ (𝑗 − 1))
241235, 240syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 ≤ (𝑗 − 1))
242 breq2 4581 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑗 − 1) → (𝑗𝑘𝑗 ≤ (𝑗 − 1)))
243242notbid 306 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑗 − 1) → (¬ 𝑗𝑘 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
244243rspcev 3281 . . . . . . . . . . . . . . . . 17 (((𝑗 − 1) ∈ (𝐽𝑡) ∧ ¬ 𝑗 ≤ (𝑗 − 1)) → ∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘)
245229, 241, 244syl2anc 690 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘)
246 rexnal 2977 . . . . . . . . . . . . . . . 16 (∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘 ↔ ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
247245, 246sylib 206 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
2482473expia 1258 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘))
249248con2d 127 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (∀𝑘 ∈ (𝐽𝑡)𝑗𝑘 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
250249imp 443 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
251111, 250eldifd 3550 . . . . . . . . . . 11 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
252251exp31 627 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) → (∀𝑘 ∈ (𝐽𝑡)𝑗𝑘𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))))
253105, 252reximdai 2994 . . . . . . . . 9 ((𝜑𝑡𝑇) → (∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘 → ∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
254102, 253mpd 15 . . . . . . . 8 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
255 df-rex 2901 . . . . . . . 8 (∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
256254, 255sylib 206 . . . . . . 7 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
257 simprl 789 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (𝐽𝑡))
258 eldifn 3694 . . . . . . . . . . . . 13 (𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
259 simplr 787 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑡𝑇)
260 simpll 785 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝜑)
261177adantrr 748 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ (1...𝑁))
262 simprr 791 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
263 oveq1 6533 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 = 𝑘 → (𝑗 − (1 / 3)) = (𝑘 − (1 / 3)))
264263oveq1d 6541 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑘 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑘 − (1 / 3)) · 𝐸))
265264breq2d 4589 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑘 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)))
266265rabbidv 3163 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 𝑘 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
267266cbvmptv 4672 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
26869, 267eqtri 2631 . . . . . . . . . . . . . . . . . . . . . 22 𝐷 = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
269268a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → 𝐷 = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)}))
270 oveq1 6533 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = (𝑗 − 1) → (𝑘 − (1 / 3)) = ((𝑗 − 1) − (1 / 3)))
271270oveq1d 6541 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑗 − 1) → ((𝑘 − (1 / 3)) · 𝐸) = (((𝑗 − 1) − (1 / 3)) · 𝐸))
272271breq2d 4589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑗 − 1) → ((𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)))
273272rabbidv 3163 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 − 1) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
274273adantl 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 = (𝑗 − 1)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
275 fzssp1 12212 . . . . . . . . . . . . . . . . . . . . . . . 24 (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
276188oveq2d 6542 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
277275, 276syl5sseq 3615 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
278277adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
279 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
280 1zzd 11243 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 1 ∈ ℤ)
281197adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℤ)
282230adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℤ)
283 fzsubel 12205 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
284280, 281, 282, 280, 283syl22anc 1318 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
285279, 284mpbid 220 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1)))
286116a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → (1 − 1) = 0)
287286oveq1d 6541 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝑁)) → ((1 − 1)...(𝑁 − 1)) = (0...(𝑁 − 1)))
288285, 287eleqtrd 2689 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
289278, 288sseldd 3568 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...𝑁))
29062adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑇 ∈ V)
291 rabexg 4733 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V)
292290, 291syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V)
293269, 274, 289, 292fvmptd 6181 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐷‘(𝑗 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
294293eleq2d 2672 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}))
295294notbid 306 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → (¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}))
296295biimpa 499 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
297260, 261, 262, 296syl21anc 1316 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
298 rabid 3094 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)))
299232adantrr 748 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ ℝ)
300 recn 9882 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → 𝑗 ∈ ℂ)
301 1cnd 9912 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → 1 ∈ ℂ)
302 1re 9895 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
303302, 22, 233pm3.2i 1231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0)
304 redivcl 10595 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (1 / 3) ∈ ℝ)
305 recn 9882 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 / 3) ∈ ℝ → (1 / 3) ∈ ℂ)
306303, 304, 305mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 / 3) ∈ ℂ
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → (1 / 3) ∈ ℂ)
308300, 301, 307subsub4d 10274 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) = (𝑗 − (1 + (1 / 3))))
309 3cn 10944 . . . . . . . . . . . . . . . . . . . . . . . . . 26 3 ∈ ℂ
310309, 205, 309, 23divdiri 10633 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
311 3p1e4 11002 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 + 1) = 4
312311oveq1i 6536 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 + 1) / 3) = (4 / 3)
313309, 23dividi 10609 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 / 3) = 1
314313oveq1i 6536 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
315310, 312, 3143eqtr3i 2639 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 / 3) = (1 + (1 / 3))
316315a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → (4 / 3) = (1 + (1 / 3)))
317316oveq2d 6542 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℝ → (𝑗 − (4 / 3)) = (𝑗 − (1 + (1 / 3))))
318308, 317eqtr4d 2646 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) = (𝑗 − (4 / 3)))
319318oveq1d 6541 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
320299, 319syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
321320breq2d 4589 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
322321anbi2d 735 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝑡𝑇 ∧ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)) ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))))
323298, 322syl5bb 270 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))))
324297, 323mtbid 312 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
325 imnan 436 . . . . . . . . . . . . . . 15 ((𝑡𝑇 → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)) ↔ ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
326324, 325sylibr 222 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡𝑇 → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
327259, 326mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))
328258, 327sylanr2 682 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))
329232adantrr 748 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ ℝ)
330 4re 10946 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ
331330a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 4 ∈ ℝ)
33222a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ∈ ℝ)
33323a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ≠ 0)
334331, 332, 333redivcld 10704 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (4 / 3) ∈ ℝ)
335329, 334resubcld 10309 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 − (4 / 3)) ∈ ℝ)
33637ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ)
337 remulcl 9877 . . . . . . . . . . . . . . 15 (((𝑗 − (4 / 3)) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ)
338337rexrd 9945 . . . . . . . . . . . . . 14 (((𝑗 − (4 / 3)) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*)
339335, 336, 338syl2anc 690 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*)
34046rexrd 9945 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ*)
341340adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹𝑡) ∈ ℝ*)
342 xrltnle 9956 . . . . . . . . . . . . 13 ((((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ* ∧ (𝐹𝑡) ∈ ℝ*) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
343339, 341, 342syl2anc 690 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
344328, 343mpbird 245 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡))
345 simpl 471 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝜑𝑡𝑇))
346 simprr 791 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
347346eldifad 3551 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ (𝐷𝑗))
348 simplll 793 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝜑)
349177adantr 479 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑗 ∈ (1...𝑁))
350 simpr 475 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ (𝐷𝑗))
351 oveq1 6533 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑗 → (𝑘 − (1 / 3)) = (𝑗 − (1 / 3)))
352351oveq1d 6541 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑗 → ((𝑘 − (1 / 3)) · 𝐸) = ((𝑗 − (1 / 3)) · 𝐸))
353352breq2d 4589 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → ((𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
354353rabbidv 3163 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
355354adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 = 𝑗) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
356 0p1e1 10981 . . . . . . . . . . . . . . . . . . . . . 22 (0 + 1) = 1
357356oveq1i 6536 . . . . . . . . . . . . . . . . . . . . 21 ((0 + 1)...𝑁) = (1...𝑁)
358 0z 11223 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℤ
359 fzp1ss 12219 . . . . . . . . . . . . . . . . . . . . . 22 (0 ∈ ℤ → ((0 + 1)...𝑁) ⊆ (0...𝑁))
360358, 359ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ((0 + 1)...𝑁) ⊆ (0...𝑁)
361357, 360eqsstr3i 3598 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ⊆ (0...𝑁)
362361sseli 3563 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ (0...𝑁))
363362adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (0...𝑁))
364 rabexg 4733 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
365290, 364syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
366269, 355, 363, 365fvmptd 6181 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
367366eleq2d 2672 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}))
368367biimpa 499 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
369348, 349, 350, 368syl21anc 1316 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
370 rabid 3094 . . . . . . . . . . . . . 14 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
371369, 370sylib 206 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
372371simprd 477 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
373345, 257, 347, 372syl21anc 1316 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
374344, 373jca 552 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
37515ad2antrr 757 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑁 ∈ ℕ)
376 simplr 787 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡𝑇)
377177adantrr 748 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (1...𝑁))
378 nfv 1829 . . . . . . . . . . . . . . . 16 𝑗 𝑖 ∈ (0...𝑁)
379103, 378nfan 1815 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁))
380 nfv 1829 . . . . . . . . . . . . . . 15 𝑗(𝑋𝑖):𝑇⟶ℝ
381379, 380nfim 1812 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
382 eleq1 2675 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑗 ∈ (0...𝑁) ↔ 𝑖 ∈ (0...𝑁)))
383382anbi2d 735 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑖 ∈ (0...𝑁))))
384 fveq2 6087 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑋𝑗) = (𝑋𝑖))
385384feq1d 5928 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑋𝑗):𝑇⟶ℝ ↔ (𝑋𝑖):𝑇⟶ℝ))
386383, 385imbi12d 332 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ) ↔ ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)))
387 stoweidlem34.14 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ)
388381, 386, 387chvar 2249 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
389388ad4ant14 1284 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
390 simplll 793 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝜑)
391 simpr 475 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁))
392 simpllr 794 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑡𝑇)
393103, 378, 104nf3an 1818 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇)
394 nfv 1829 . . . . . . . . . . . . . . 15 𝑗((𝑋𝑖)‘𝑡) ≤ 1
395393, 394nfim 1812 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)
3963823anbi2d 1395 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇)))
397384fveq1d 6089 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → ((𝑋𝑗)‘𝑡) = ((𝑋𝑖)‘𝑡))
398397breq1d 4587 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (((𝑋𝑗)‘𝑡) ≤ 1 ↔ ((𝑋𝑖)‘𝑡) ≤ 1))
399396, 398imbi12d 332 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)))
400 stoweidlem34.16 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1)
401395, 399, 400chvar 2249 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)
402390, 391, 392, 401syl3anc 1317 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑡) ≤ 1)
403 simplll 793 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑)
404 0zd 11224 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ)
405 elfzel2 12168 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑁 ∈ ℤ)
406405adantl 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ)
407 elfzelz 12170 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℤ)
408407adantl 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ)
409404, 406, 4083jca 1234 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
410 0red 9897 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℝ)
411 elfzel1 12169 . . . . . . . . . . . . . . . . . . 19 (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℤ)
412411zred 11316 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℝ)
413412adantl 480 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ)
414407zred 11316 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℝ)
415414adantl 480 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
416 0red 9897 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ∈ ℝ)
417 1red 9911 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 1 ∈ ℝ)
418 0le1 10402 . . . . . . . . . . . . . . . . . . . 20 0 ≤ 1
419418a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ≤ 1)
420 elfzle1 12172 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...𝑁) → 1 ≤ 𝑗)
421177, 420syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 1 ≤ 𝑗)
422416, 417, 232, 419, 421letrd 10045 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ≤ 𝑗)
423422adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑗)
424 elfzle1 12172 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑗𝑖)
425424adantl 480 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗𝑖)
426410, 413, 415, 423, 425letrd 10045 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑖)
427 elfzle2 12173 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑖𝑁)
428427adantl 480 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖𝑁)
429426, 428jca 552 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖𝑖𝑁))
430 elfz2 12161 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑁)))
431409, 429, 430sylanbrc 694 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
432431adantlrr 752 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
433 simpll 785 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑𝑡𝑇))
434 simplrl 795 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽𝑡))
435 simplrr 796 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
436435eldifad 3551 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑗))
437 simpr 475 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁))
438 simpl1 1056 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑𝑡𝑇))
439438simprd 477 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡𝑇)
440438, 46syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ∈ ℝ)
441412adantl 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ)
44224a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈ ℝ)
443441, 442resubcld 10309 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
444 simpl1l 1104 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑)
445444, 37syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
446443, 445remulcld 9926 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
447414adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
44824a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈ ℝ)
449447, 448resubcld 10309 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈ ℝ)
45037adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
451449, 450remulcld 9926 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ)
452444, 451sylancom 697 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ)
453 simpl3 1058 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑗))
454 simpl2 1057 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽𝑡))
455438, 454, 177syl2anc 690 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (1...𝑁))
456444, 455, 366syl2anc 690 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
457453, 456eleqtrd 2689 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
458457, 370sylib 206 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
459458simprd 477 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
460414adantl 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
461424adantl 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗𝑖)
462441, 460, 442, 461lesub1dd 10494 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)))
463444, 449sylancom 697 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈ ℝ)
46436rpregt0d 11712 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
465444, 464syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
466 lemul1 10726 . . . . . . . . . . . . . . . . . . 19 (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑖 − (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
467443, 463, 465, 466syl3anc 1317 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
468462, 467mpbid 220 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸))
469440, 446, 452, 459, 468letrd 10045 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸))
470 rabid 3094 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
471439, 469, 470sylanbrc 694 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
472 simpr 475 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁))
473 0zd 11224 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ)
4744053ad2ant3 1076 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ)
4754073ad2ant3 1076 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ)
476473, 474, 4753jca 1234 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
4774293impa 1250 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖𝑖𝑁))
478476, 477, 430sylanbrc 694 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
479438, 454, 472, 478syl3anc 1317 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
480 simpr 475 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁))
481 rabexg 4733 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
48262, 481syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
483482adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
484 oveq1 6533 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝑗 − (1 / 3)) = (𝑖 − (1 / 3)))
485484oveq1d 6541 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑖 − (1 / 3)) · 𝐸))
486485breq2d 4589 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
487486rabbidv 3163 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
488487, 69fvmptg 6173 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
489480, 483, 488syl2anc 690 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
490444, 479, 489syl2anc 690 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
491471, 490eleqtrrd 2690 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑖))
492433, 434, 436, 437, 491syl31anc 1320 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑖))
493103, 378, 223nf3an 1818 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖))
494 nfv 1829 . . . . . . . . . . . . . . 15 𝑗((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁)
495493, 494nfim 1812 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
496382, 2253anbi23d 1393 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖))))
497397breq1d 4587 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁)))
498496, 497imbi12d 332 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))))
499 stoweidlem34.17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁))
500495, 498, 499chvar 2249 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
501403, 432, 492, 500syl3anc 1317 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
50236ad2antrr 757 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ+)
503 stoweidlem34.13 . . . . . . . . . . . . 13 (𝜑𝐸 < (1 / 3))
504503ad2antrr 757 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 < (1 / 3))
505375, 376, 377, 389, 402, 501, 502, 504stoweidlem11 38687 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸))
506 eleq1 2675 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑙 ∈ (𝐽𝑡) ↔ 𝑗 ∈ (𝐽𝑡)))
507 fveq2 6087 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑗 → (𝐷𝑙) = (𝐷𝑗))
508 oveq1 6533 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 → (𝑙 − 1) = (𝑗 − 1))
509508fveq2d 6091 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑗 → (𝐷‘(𝑙 − 1)) = (𝐷‘(𝑗 − 1)))
510507, 509difeq12d 3690 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑗 → ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) = ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
511510eleq2d 2672 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
512506, 511anbi12d 742 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑗 → ((𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))))
513512anbi2d 735 . . . . . . . . . . . . . . 15 (𝑙 = 𝑗 → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))))
514 oveq1 6533 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑙 − (4 / 3)) = (𝑗 − (4 / 3)))
515514oveq1d 6541 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑗 → ((𝑙 − (4 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
516515breq1d 4587 . . . . . . . . . . . . . . 15 (𝑙 = 𝑗 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) ↔ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
517513, 516imbi12d 332 . . . . . . . . . . . . . 14 (𝑙 = 𝑗 → ((((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)) ↔ (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
518 eleq1 2675 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑠𝑇𝑡𝑇))
519518anbi2d 735 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝜑𝑠𝑇) ↔ (𝜑𝑡𝑇)))
520 fveq2 6087 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑡 → (𝐽𝑠) = (𝐽𝑡))
521520eleq2d 2672 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑙 ∈ (𝐽𝑠) ↔ 𝑙 ∈ (𝐽𝑡)))
522 eleq1 2675 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
523521, 522anbi12d 742 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))))
524519, 523anbi12d 742 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))))
525 fveq2 6087 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠) = ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
526525breq2d 4589 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠) ↔ ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
527524, 526imbi12d 332 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠)) ↔ (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
528 stoweidlem34.1 . . . . . . . . . . . . . . . . . 18 𝑡𝐹
529 nfv 1829 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑠𝑇
530103, 529nfan 1815 . . . . . . . . . . . . . . . . . . 19 𝑗(𝜑𝑠𝑇)
531 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . 22 𝑗𝑠
53292, 531nffv 6094 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝐽𝑠)
533532nfcri 2744 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑙 ∈ (𝐽𝑠)
534 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗𝑙
53577, 534nffv 6094 . . . . . . . . . . . . . . . . . . . . . 22 𝑗(𝐷𝑙)
536 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗(𝑙 − 1)
53777, 536nffv 6094 . . . . . . . . . . . . . . . . . . . . . 22 𝑗(𝐷‘(𝑙 − 1))
538535, 537nfdif 3692 . . . . . . . . . . . . . . . . . . . . 21 𝑗((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
539538nfcri 2744 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
540533, 539nfan 1815 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
541530, 540nfan 1815 . . . . . . . . . . . . . . . . . 18 𝑗((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
542 nfv 1829 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑠𝑇
5431, 542nfan 1815 . . . . . . . . . . . . . . . . . . 19 𝑡(𝜑𝑠𝑇)
544 nfmpt1 4669 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
5455, 544nfcxfr 2748 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝐽
546 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝑠
547545, 546nffv 6094 . . . . . . . . . . . . . . . . . . . . 21 𝑡(𝐽𝑠)
548547nfcri 2744 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑙 ∈ (𝐽𝑠)
549 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝑙
550164, 549nffv 6094 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝐷𝑙)
551 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑙 − 1)
552164, 551nffv 6094 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝐷‘(𝑙 − 1))
553550, 552nfdif 3692 . . . . . . . . . . . . . . . . . . . . 21 𝑡((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
554553nfcri 2744 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
555548, 554nfan 1815 . . . . . . . . . . . . . . . . . . 19 𝑡(𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
556543, 555nfan 1815 . . . . . . . . . . . . . . . . . 18 𝑡((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
557 stoweidlem34.5 . . . . . . . . . . . . . . . . . 18 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
55815ad2antrr 757 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑁 ∈ ℕ)
55962ad2antrr 757 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑇 ∈ V)
5603rabex 4734 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ∈ V
561 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑡𝑗
562164, 561nffv 6094 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡(𝐷𝑗)
563562nfcri 2744 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 𝑠 ∈ (𝐷𝑗)
564 nfcv 2750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(1...𝑁)
565563, 564nfrab 3099 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡{𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)}
566 eleq1 2675 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑠 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑠 ∈ (𝐷𝑗)))
567566rabbidv 3163 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑠 → {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
568546, 565, 567, 5fvmptf 6193 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ∈ V) → (𝐽𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
569560, 568mpan2 702 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠𝑇 → (𝐽𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
570569eleq2d 2672 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠𝑇 → (𝑙 ∈ (𝐽𝑠) ↔ 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)}))
571570biimpa 499 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
572535nfcri 2744 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 𝑠 ∈ (𝐷𝑙)
573 fveq2 6087 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑙 → (𝐷𝑗) = (𝐷𝑙))
574573eleq2d 2672 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑙 → (𝑠 ∈ (𝐷𝑗) ↔ 𝑠 ∈ (𝐷𝑙)))
575534, 75, 572, 574elrabf 3328 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ↔ (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷𝑙)))
576571, 575sylib 206 . . . . . . . . . . . . . . . . . . . 20 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷𝑙)))
577576simpld 473 . . . . . . . . . . . . . . . . . . 19 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → 𝑙 ∈ (1...𝑁))
578577ad2ant2lr 779 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑙 ∈ (1...𝑁))
579 simprr 791 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
58045ad2antrr 757 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐹:𝑇⟶ℝ)
58136ad2antrr 757 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 ∈ ℝ+)
582503ad2antrr 757 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 < (1 / 3))
583388ad4ant14 1284 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
584 simp1ll 1116 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 𝜑)
585 nfv 1829 . . . . . . . . . . . . . . . . . . . . 21 𝑗0 ≤ ((𝑋𝑖)‘𝑡)
586393, 585nfim 1812 . . . . . . . . . . . . . . . . . . . 20 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
587397breq2d 4589 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (0 ≤ ((𝑋𝑗)‘𝑡) ↔ 0 ≤ ((𝑋𝑖)‘𝑡)))
588396, 587imbi12d 332 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))))
589 stoweidlem34.15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡))
590586, 588, 589chvar 2249 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
591584, 590syld3an1 1363 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
592 simp1ll 1116 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → 𝜑)
593 nfmpt1 4669 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
594557, 593nfcxfr 2748 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑗𝐵
595594, 221nffv 6094 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗(𝐵𝑖)
596595nfcri 2744 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 𝑡 ∈ (𝐵𝑖)
597103, 378, 596nf3an 1818 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖))
598 nfv 1829 . . . . . . . . . . . . . . . . . . . . 21 𝑗(1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)
599597, 598nfim 1812 . . . . . . . . . . . . . . . . . . . 20 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
600 fveq2 6087 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → (𝐵𝑗) = (𝐵𝑖))
601600eleq2d 2672 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑖 → (𝑡 ∈ (𝐵𝑗) ↔ 𝑡 ∈ (𝐵𝑖)))
602382, 6013anbi23d 1393 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖))))
603397breq2d 4589 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → ((1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)))
604602, 603imbi12d 332 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))))
605 stoweidlem34.18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡))
606599, 604, 605chvar 2249 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
607592, 606syld3an1 1363 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
608528, 541, 556, 69, 557, 558, 559, 578, 579, 580, 581, 582, 583, 591, 607stoweidlem26 38702 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠))
609527, 608vtoclg 3238 . . . . . . . . . . . . . . . 16 (𝑡𝑇 → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
610609ad2antlr 758 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
611610pm2.43i 49 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
612517, 611vtoclg 3238 . . . . . . . . . . . . 13 (𝑗 ∈ (𝐽𝑡) → (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
613612ad2antrl 759 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
614613pm2.43i 49 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
615505, 614jca 552 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
616257, 374, 6153jca 1234 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
617616ex 448 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))) → (𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
618105, 617eximd 2071 . . . . . . 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 1034 . . . . . . 7 ((𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ (𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
621620exbii 1763 . . . . . 6 (∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
622619, 621sylib 206 . . . . 5 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
623 df-rex 2901 . . . . 5 (∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
624622, 623sylibr 222 . . . 4 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
625 nfcv 2750 . . . . 5 𝑗
62694, 625ssrexf 3627 . . . 4 ((𝐽𝑡) ⊆ ℝ → (∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
62714, 624, 626sylc 62 . . 3 ((𝜑𝑡𝑇) → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
628627ex 448 . 2 (𝜑 → (𝑡𝑇 → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
6291, 628ralrimi 2939 1 (𝜑 → ∀𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030  wal 1472   = wceq 1474  wex 1694  wnf 1698  wcel 1976  wnfc 2737  wne 2779  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  cdif 3536  wss 3539  c0 3873   class class class wbr 4577  cmpt 4637  wf 5785  cfv 5789  (class class class)co 6526  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797  *cxr 9929   < clt 9930  cle 9931  cmin 10117  -cneg 10118   / cdiv 10535  cn 10869  3c3 10920  4c4 10921  0cn0 11141  cz 11212  cuz 11521  +crp 11666  ...cfz 12154  Σcsu 14212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4938  df-id 4942  df-po 4948  df-so 4949  df-fr 4986  df-se 4987  df-we 4988  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-pred 5582  df-ord 5628  df-on 5629  df-lim 5630  df-suc 5631  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-isom 5798  df-riota 6488  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-sup 8208  df-oi 8275  df-card 8625  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10536  df-nn 10870  df-2 10928  df-3 10929  df-4 10930  df-n0 11142  df-z 11213  df-uz 11522  df-rp 11667  df-ico 12010  df-fz 12155  df-fzo 12292  df-seq 12621  df-exp 12680  df-hash 12937  df-cj 13635  df-re 13636  df-im 13637  df-sqrt 13771  df-abs 13772  df-clim 14015  df-sum 14213
This theorem is referenced by:  stoweidlem60  38736
  Copyright terms: Public domain W3C validator