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

Proof of Theorem stoweidlem34
Dummy variables 𝑘 𝑙 𝑠 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem34.3 . 2 𝑡𝜑
2 simpr 485 . . . . . . . 8 ((𝜑𝑡𝑇) → 𝑡𝑇)
3 ovex 7390 . . . . . . . . 9 (1...𝑁) ∈ V
43rabex 5289 . . . . . . . 8 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ∈ V
5 stoweidlem34.6 . . . . . . . . 9 𝐽 = (𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
65fvmpt2 6959 . . . . . . . 8 ((𝑡𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ∈ V) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
72, 4, 6sylancl 586 . . . . . . 7 ((𝜑𝑡𝑇) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
8 ssrab2 4037 . . . . . . 7 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ⊆ (1...𝑁)
97, 8eqsstrdi 3998 . . . . . 6 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ (1...𝑁))
10 elfznn 13470 . . . . . . 7 (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
1110ssriv 3948 . . . . . 6 (1...𝑁) ⊆ ℕ
129, 11sstrdi 3956 . . . . 5 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ ℕ)
13 nnssre 12157 . . . . 5 ℕ ⊆ ℝ
1412, 13sstrdi 3956 . . . 4 ((𝜑𝑡𝑇) → (𝐽𝑡) ⊆ ℝ)
15 stoweidlem34.7 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℕ)
1615adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → 𝑁 ∈ ℕ)
17 nnuz 12806 . . . . . . . . . . . . . . 15 ℕ = (ℤ‘1)
1816, 17eleqtrdi 2848 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 𝑁 ∈ (ℤ‘1))
19 eluzfz2 13449 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ‘1) → 𝑁 ∈ (1...𝑁))
2018, 19syl 17 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑁 ∈ (1...𝑁))
21 stoweidlem34.11 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝐹𝑡) < ((𝑁 − 1) · 𝐸))
22 3re 12233 . . . . . . . . . . . . . . . . . . . . 21 3 ∈ ℝ
23 3ne0 12259 . . . . . . . . . . . . . . . . . . . . 21 3 ≠ 0
2422, 23rereccli 11920 . . . . . . . . . . . . . . . . . . . 20 (1 / 3) ∈ ℝ
2524a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (1 / 3) ∈ ℝ)
26 1red 11156 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 1 ∈ ℝ)
2716nnred 12168 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 𝑁 ∈ ℝ)
28 1lt3 12326 . . . . . . . . . . . . . . . . . . . . 21 1 < 3
2922, 28pm3.2i 471 . . . . . . . . . . . . . . . . . . . 20 (3 ∈ ℝ ∧ 1 < 3)
30 recgt1i 12052 . . . . . . . . . . . . . . . . . . . . 21 ((3 ∈ ℝ ∧ 1 < 3) → (0 < (1 / 3) ∧ (1 / 3) < 1))
3130simprd 496 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℝ ∧ 1 < 3) → (1 / 3) < 1)
3229, 31mp1i 13 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (1 / 3) < 1)
3325, 26, 27, 32ltsub2dd 11768 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝑇) → (𝑁 − 1) < (𝑁 − (1 / 3)))
3427, 26resubcld 11583 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (𝑁 − 1) ∈ ℝ)
3527, 25resubcld 11583 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → (𝑁 − (1 / 3)) ∈ ℝ)
36 stoweidlem34.12 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐸 ∈ ℝ+)
3736rpred 12957 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐸 ∈ ℝ)
3837adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 𝐸 ∈ ℝ)
3936rpgt0d 12960 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 < 𝐸)
4039adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝑇) → 0 < 𝐸)
41 ltmul1 12005 . . . . . . . . . . . . . . . . . . 19 (((𝑁 − 1) ∈ ℝ ∧ (𝑁 − (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
4234, 35, 38, 40, 41syl112anc 1374 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝑇) → ((𝑁 − 1) < (𝑁 − (1 / 3)) ↔ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
4333, 42mpbid 231 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸))
4421, 43jca 512 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → ((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)))
45 stoweidlem34.9 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝑇⟶ℝ)
4645ffvelcdmda 7035 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ)
4734, 38remulcld 11185 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − 1) · 𝐸) ∈ ℝ)
4835, 38remulcld 11185 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ)
49 lttr 11231 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸)))
50 ltle 11243 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
51503adant2 1131 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → ((𝐹𝑡) < ((𝑁 − (1 / 3)) · 𝐸) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5249, 51syld 47 . . . . . . . . . . . . . . . . 17 (((𝐹𝑡) ∈ ℝ ∧ ((𝑁 − 1) · 𝐸) ∈ ℝ ∧ ((𝑁 − (1 / 3)) · 𝐸) ∈ ℝ) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5346, 47, 48, 52syl3anc 1371 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (((𝐹𝑡) < ((𝑁 − 1) · 𝐸) ∧ ((𝑁 − 1) · 𝐸) < ((𝑁 − (1 / 3)) · 𝐸)) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
5444, 53mpd 15 . . . . . . . . . . . . . . 15 ((𝜑𝑡𝑇) → (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸))
55 rabid 3427 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
562, 54, 55sylanbrc 583 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
57 stoweidlem34.4 . . . . . . . . . . . . . . . 16 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
58 oveq1 7364 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑁 → (𝑗 − (1 / 3)) = (𝑁 − (1 / 3)))
5958oveq1d 7372 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑁 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑁 − (1 / 3)) · 𝐸))
6059breq2d 5117 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑁 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)))
6160rabbidv 3415 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑁 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
62 nnnn0 12420 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
63 nn0uz 12805 . . . . . . . . . . . . . . . . . 18 0 = (ℤ‘0)
6462, 63eleqtrdi 2848 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ‘0))
65 eluzfz2 13449 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ‘0) → 𝑁 ∈ (0...𝑁))
6615, 64, 653syl 18 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (0...𝑁))
67 stoweidlem34.8 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ V)
68 rabexg 5288 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V)
6967, 68syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)} ∈ V)
7057, 61, 66, 69fvmptd3 6971 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7170adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐷𝑁) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑁 − (1 / 3)) · 𝐸)})
7256, 71eleqtrrd 2841 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑡 ∈ (𝐷𝑁))
73 nfcv 2907 . . . . . . . . . . . . . 14 𝑗𝑁
74 nfcv 2907 . . . . . . . . . . . . . 14 𝑗(1...𝑁)
75 nfmpt1 5213 . . . . . . . . . . . . . . . . 17 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7657, 75nfcxfr 2905 . . . . . . . . . . . . . . . 16 𝑗𝐷
7776, 73nffv 6852 . . . . . . . . . . . . . . 15 𝑗(𝐷𝑁)
7877nfcri 2894 . . . . . . . . . . . . . 14 𝑗 𝑡 ∈ (𝐷𝑁)
79 fveq2 6842 . . . . . . . . . . . . . . 15 (𝑗 = 𝑁 → (𝐷𝑗) = (𝐷𝑁))
8079eleq2d 2823 . . . . . . . . . . . . . 14 (𝑗 = 𝑁 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑁)))
8173, 74, 78, 80elrabf 3641 . . . . . . . . . . . . 13 (𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ↔ (𝑁 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑁)))
8220, 72, 81sylanbrc 583 . . . . . . . . . . . 12 ((𝜑𝑡𝑇) → 𝑁 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
8382, 7eleqtrrd 2841 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → 𝑁 ∈ (𝐽𝑡))
84 ne0i 4294 . . . . . . . . . . 11 (𝑁 ∈ (𝐽𝑡) → (𝐽𝑡) ≠ ∅)
8583, 84syl 17 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝐽𝑡) ≠ ∅)
86 nnwo 12838 . . . . . . . . . . 11 (((𝐽𝑡) ⊆ ℕ ∧ (𝐽𝑡) ≠ ∅) → ∃𝑖 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑖𝑘)
87 nfcv 2907 . . . . . . . . . . . 12 𝑖(𝐽𝑡)
88 nfcv 2907 . . . . . . . . . . . . . . 15 𝑗𝑇
89 nfrab1 3426 . . . . . . . . . . . . . . 15 𝑗{𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)}
9088, 89nfmpt 5212 . . . . . . . . . . . . . 14 𝑗(𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
915, 90nfcxfr 2905 . . . . . . . . . . . . 13 𝑗𝐽
92 nfcv 2907 . . . . . . . . . . . . 13 𝑗𝑡
9391, 92nffv 6852 . . . . . . . . . . . 12 𝑗(𝐽𝑡)
94 nfv 1917 . . . . . . . . . . . . 13 𝑗 𝑖𝑘
9593, 94nfralw 3294 . . . . . . . . . . . 12 𝑗𝑘 ∈ (𝐽𝑡)𝑖𝑘
96 nfv 1917 . . . . . . . . . . . 12 𝑖𝑘 ∈ (𝐽𝑡)𝑗𝑘
97 breq1 5108 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → (𝑖𝑘𝑗𝑘))
9897ralbidv 3174 . . . . . . . . . . . 12 (𝑖 = 𝑗 → (∀𝑘 ∈ (𝐽𝑡)𝑖𝑘 ↔ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘))
9987, 93, 95, 96, 98cbvrexfw 3288 . . . . . . . . . . 11 (∃𝑖 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑖𝑘 ↔ ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
10086, 99sylib 217 . . . . . . . . . 10 (((𝐽𝑡) ⊆ ℕ ∧ (𝐽𝑡) ≠ ∅) → ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
10112, 85, 100syl2anc 584 . . . . . . . . 9 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
102 stoweidlem34.2 . . . . . . . . . . 11 𝑗𝜑
103 nfv 1917 . . . . . . . . . . 11 𝑗 𝑡𝑇
104102, 103nfan 1902 . . . . . . . . . 10 𝑗(𝜑𝑡𝑇)
1057eleq2d 2823 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) ↔ 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)}))
106105biimpa 477 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
107 rabid 3427 . . . . . . . . . . . . . . 15 (𝑗 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)))
108106, 107sylib 217 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)))
109108simprd 496 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑡 ∈ (𝐷𝑗))
110109adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → 𝑡 ∈ (𝐷𝑗))
111 simp3 1138 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑡 ∈ (𝐷‘(𝑗 − 1)))
112 simp1l 1197 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝜑)
113 noel 4290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ¬ 𝑡 ∈ ∅
114 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 = 1 → (𝑗 − 1) = (1 − 1))
115 1m1e0 12225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 − 1) = 0
116114, 115eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 = 1 → (𝑗 − 1) = 0)
117116fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 = 1 → (𝐷‘(𝑗 − 1)) = (𝐷‘0))
11822a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑡𝑇) → 3 ∈ ℝ)
11923a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝜑𝑡𝑇) → 3 ≠ 0)
12026, 118, 119redivcld 11983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑡𝑇) → (1 / 3) ∈ ℝ)
121120renegcld 11582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → -(1 / 3) ∈ ℝ)
122121, 38remulcld 11185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) ∈ ℝ)
123 0red 11158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → 0 ∈ ℝ)
124 3pos 12258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
12522, 124recgt0ii 12061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
126 lt0neg2 11662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((1 / 3) ∈ ℝ → (0 < (1 / 3) ↔ -(1 / 3) < 0))
12724, 126ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (0 < (1 / 3) ↔ -(1 / 3) < 0)
128125, 127mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 -(1 / 3) < 0
129 ltmul1 12005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((-(1 / 3) ∈ ℝ ∧ 0 ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (-(1 / 3) < 0 ↔ (-(1 / 3) · 𝐸) < (0 · 𝐸)))
130121, 123, 38, 40, 129syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝜑𝑡𝑇) → (-(1 / 3) < 0 ↔ (-(1 / 3) · 𝐸) < (0 · 𝐸)))
131128, 130mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < (0 · 𝐸))
132 mul02lem2 11332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐸 ∈ ℝ → (0 · 𝐸) = 0)
13338, 132syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝜑𝑡𝑇) → (0 · 𝐸) = 0)
134131, 133breqtrd 5131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < 0)
135 stoweidlem34.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝜑𝑡𝑇) → 0 ≤ (𝐹𝑡))
136122, 123, 46, 134, 135ltletrd 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑡𝑇) → (-(1 / 3) · 𝐸) < (𝐹𝑡))
137122, 46ltnled 11302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑡𝑇) → ((-(1 / 3) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
138136, 137mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑡𝑇) → ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸))
139 nan 828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸))) ↔ ((𝜑𝑡𝑇) → ¬ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
140138, 139mpbir 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
141 rabid 3427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
142140, 141sylnibr 328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
143 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 0 → (𝑗 − (1 / 3)) = (0 − (1 / 3)))
144 df-neg 11388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 -(1 / 3) = (0 − (1 / 3))
145143, 144eqtr4di 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 = 0 → (𝑗 − (1 / 3)) = -(1 / 3))
146145oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 = 0 → ((𝑗 − (1 / 3)) · 𝐸) = (-(1 / 3) · 𝐸))
147146breq2d 5117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑗 = 0 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)))
148147rabbidv 3415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑗 = 0 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
14915nnnn0d 12473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝜑𝑁 ∈ ℕ0)
150 elnn0uz 12808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ ℕ0𝑁 ∈ (ℤ‘0))
151149, 150sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝑁 ∈ (ℤ‘0))
152 eluzfz1 13448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑁 ∈ (ℤ‘0) → 0 ∈ (0...𝑁))
153151, 152syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → 0 ∈ (0...𝑁))
154 rabexg 5288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V)
15567, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)} ∈ V)
15657, 148, 153, 155fvmptd3 6971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑 → (𝐷‘0) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (-(1 / 3) · 𝐸)})
157142, 156neleqtrrd 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → ¬ 𝑡 ∈ (𝐷‘0))
1581, 157alrimi 2206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0))
159 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑡(0...𝑁)
160 nfrab1 3426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑡{𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
161159, 160nfmpt 5212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
16257, 161nfcxfr 2905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑡𝐷
163 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑡0
164162, 163nffv 6852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 𝑡(𝐷‘0)
165164eq0f 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐷‘0) = ∅ ↔ ∀𝑡 ¬ 𝑡 ∈ (𝐷‘0))
166158, 165sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐷‘0) = ∅)
167117, 166sylan9eqr 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 = 1) → (𝐷‘(𝑗 − 1)) = ∅)
168167eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 = 1) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ ∅))
169113, 168mtbiri 326 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 = 1) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
170169ex 413 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑗 = 1 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
171170con2d 134 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ 𝑗 = 1))
172112, 111, 171sylc 65 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 = 1)
173 simplll 773 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → 𝜑)
174105, 107bitrdi 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) ↔ (𝑗 ∈ (1...𝑁) ∧ 𝑡 ∈ (𝐷𝑗))))
175174simprbda 499 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ (1...𝑁))
17615, 17eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ (ℤ‘1))
177176adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ (𝐽𝑡)) → 𝑁 ∈ (ℤ‘1))
178 elfzp12 13520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ (ℤ‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
179177, 178syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
180179adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁))))
181175, 180mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑗 = 1 ∨ 𝑗 ∈ ((1 + 1)...𝑁)))
182181orcanai 1001 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → 𝑗 ∈ ((1 + 1)...𝑁))
183 fzssp1 13484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1...(𝑁 − 1)) ⊆ (1...((𝑁 − 1) + 1))
18415nncnd 12169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℂ)
185 1cnd 11150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → 1 ∈ ℂ)
186184, 185npcand 11516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
187186oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
188183, 187sseqtrid 3996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
189188adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
190 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ((1 + 1)...𝑁))
191 1z 12533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ∈ ℤ
192 zaddcl 12543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((1 ∈ ℤ ∧ 1 ∈ ℤ) → (1 + 1) ∈ ℤ)
193191, 191, 192mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 + 1) ∈ ℤ
194193a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (1 + 1) ∈ ℤ)
19515nnzd 12526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑𝑁 ∈ ℤ)
196195adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑁 ∈ ℤ)
197 elfzelz 13441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑗 ∈ ((1 + 1)...𝑁) → 𝑗 ∈ ℤ)
198197adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 𝑗 ∈ ℤ)
199 1zzd 12534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → 1 ∈ ℤ)
200 fzsubel 13477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((1 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
201194, 196, 198, 199, 200syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 ∈ ((1 + 1)...𝑁) ↔ (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1))))
202190, 201mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (((1 + 1) − 1)...(𝑁 − 1)))
203 ax-1cn 11109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ ℂ
204203, 203pncan3oi 11417 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((1 + 1) − 1) = 1
205204oveq1i 7367 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((1 + 1) − 1)...(𝑁 − 1)) = (1...(𝑁 − 1))
206202, 205eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...(𝑁 − 1)))
207189, 206sseldd 3945 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ ((1 + 1)...𝑁)) → (𝑗 − 1) ∈ (1...𝑁))
208173, 182, 207syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ¬ 𝑗 = 1) → (𝑗 − 1) ∈ (1...𝑁))
209208ex 413 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁)))
2102093adant3 1132 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (¬ 𝑗 = 1 → (𝑗 − 1) ∈ (1...𝑁)))
211172, 210mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (1...𝑁))
212 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 = (𝑗 − 1) → (𝐷𝑖) = (𝐷‘(𝑗 − 1)))
213212eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = (𝑗 − 1) → (𝑡 ∈ (𝐷𝑖) ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
214213elrab3 3646 . . . . . . . . . . . . . . . . . . . . 21 ((𝑗 − 1) ∈ (1...𝑁) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
215211, 214syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ((𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)} ↔ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
216111, 215mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)})
217 nfcv 2907 . . . . . . . . . . . . . . . . . . . 20 𝑖(1...𝑁)
218 nfv 1917 . . . . . . . . . . . . . . . . . . . 20 𝑖 𝑡 ∈ (𝐷𝑗)
219 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . 22 𝑗𝑖
22076, 219nffv 6852 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝐷𝑖)
221220nfcri 2894 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑡 ∈ (𝐷𝑖)
222 fveq2 6842 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (𝐷𝑗) = (𝐷𝑖))
223222eleq2d 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑖)))
22474, 217, 218, 221, 223cbvrabw 3439 . . . . . . . . . . . . . . . . . . 19 {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} = {𝑖 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑖)}
225216, 224eleqtrrdi 2849 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
22673ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝐽𝑡) = {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
227225, 226eleqtrrd 2841 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → (𝑗 − 1) ∈ (𝐽𝑡))
228 elfzelz 13441 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ ℤ)
229 zre 12503 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℤ → 𝑗 ∈ ℝ)
230175, 228, 2293syl 18 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 𝑗 ∈ ℝ)
2312303adant3 1132 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → 𝑗 ∈ ℝ)
232 peano2rem 11468 . . . . . . . . . . . . . . . . . 18 (𝑗 ∈ ℝ → (𝑗 − 1) ∈ ℝ)
233 ltm1 11997 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → (𝑗 − 1) < 𝑗)
234233adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → (𝑗 − 1) < 𝑗)
235 ltnle 11234 . . . . . . . . . . . . . . . . . . . 20 (((𝑗 − 1) ∈ ℝ ∧ 𝑗 ∈ ℝ) → ((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
236235ancoms 459 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → ((𝑗 − 1) < 𝑗 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
237234, 236mpbid 231 . . . . . . . . . . . . . . . . . 18 ((𝑗 ∈ ℝ ∧ (𝑗 − 1) ∈ ℝ) → ¬ 𝑗 ≤ (𝑗 − 1))
238231, 232, 237syl2anc2 585 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑗 ≤ (𝑗 − 1))
239 breq2 5109 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑗 − 1) → (𝑗𝑘𝑗 ≤ (𝑗 − 1)))
240239notbid 317 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑗 − 1) → (¬ 𝑗𝑘 ↔ ¬ 𝑗 ≤ (𝑗 − 1)))
241240rspcev 3581 . . . . . . . . . . . . . . . . 17 (((𝑗 − 1) ∈ (𝐽𝑡) ∧ ¬ 𝑗 ≤ (𝑗 − 1)) → ∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘)
242227, 238, 241syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘)
243 rexnal 3103 . . . . . . . . . . . . . . . 16 (∃𝑘 ∈ (𝐽𝑡) ¬ 𝑗𝑘 ↔ ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
244242, 243sylib 217 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘)
2452443expia 1121 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) → ¬ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘))
246245con2d 134 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → (∀𝑘 ∈ (𝐽𝑡)𝑗𝑘 → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))))
247246imp 407 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
248110, 247eldifd 3921 . . . . . . . . . . 11 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ ∀𝑘 ∈ (𝐽𝑡)𝑗𝑘) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
249248exp31 420 . . . . . . . . . 10 ((𝜑𝑡𝑇) → (𝑗 ∈ (𝐽𝑡) → (∀𝑘 ∈ (𝐽𝑡)𝑗𝑘𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))))
250104, 249reximdai 3244 . . . . . . . . 9 ((𝜑𝑡𝑇) → (∃𝑗 ∈ (𝐽𝑡)∀𝑘 ∈ (𝐽𝑡)𝑗𝑘 → ∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
251101, 250mpd 15 . . . . . . . 8 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
252 df-rex 3074 . . . . . . . 8 (∃𝑗 ∈ (𝐽𝑡)𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
253251, 252sylib 217 . . . . . . 7 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
254 simprl 769 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (𝐽𝑡))
255 eldifn 4087 . . . . . . . . . . . . 13 (𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
256 simplr 767 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑡𝑇)
257 simpll 765 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝜑)
258175adantrr 715 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ (1...𝑁))
259 simprr 771 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))
260 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = 𝑘 → (𝑗 − (1 / 3)) = (𝑘 − (1 / 3)))
261260oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = 𝑘 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑘 − (1 / 3)) · 𝐸))
262261breq2d 5117 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 𝑘 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)))
263262rabbidv 3415 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑘 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
264263cbvmptv 5218 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
26557, 264eqtri 2764 . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (𝑘 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)})
266 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = (𝑗 − 1) → (𝑘 − (1 / 3)) = ((𝑗 − 1) − (1 / 3)))
267266oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = (𝑗 − 1) → ((𝑘 − (1 / 3)) · 𝐸) = (((𝑗 − 1) − (1 / 3)) · 𝐸))
268267breq2d 5117 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = (𝑗 − 1) → ((𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)))
269268rabbidv 3415 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = (𝑗 − 1) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
270 fzssp1 13484 . . . . . . . . . . . . . . . . . . . . . . . 24 (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
271186oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
272270, 271sseqtrid 3996 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
273272adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
274 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
275 1zzd 12534 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 1 ∈ ℤ)
276195adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℤ)
277228adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℤ)
278 fzsubel 13477 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
279275, 276, 277, 275, 278syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
280274, 279mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1)))
281115a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (1...𝑁)) → (1 − 1) = 0)
282281oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (1...𝑁)) → ((1 − 1)...(𝑁 − 1)) = (0...(𝑁 − 1)))
283280, 282eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
284273, 283sseldd 3945 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 − 1) ∈ (0...𝑁))
28567adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑇 ∈ V)
286 rabexg 5288 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V)
287285, 286syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (1...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ∈ V)
288265, 269, 284, 287fvmptd3 6971 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐷‘(𝑗 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
289288eleq2d 2823 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}))
290289notbid 317 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → (¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)) ↔ ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)}))
291290biimpa 477 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (1...𝑁)) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1))) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
292257, 258, 259, 291syl21anc 836 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)})
293 rabid 3427 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)))
294230adantrr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → 𝑗 ∈ ℝ)
295 recn 11141 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → 𝑗 ∈ ℂ)
296 1cnd 11150 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → 1 ∈ ℂ)
297 1re 11155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℝ
298297, 22, 233pm3.2i 1339 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0)
299 redivcl 11874 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (1 / 3) ∈ ℝ)
300 recn 11141 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 / 3) ∈ ℝ → (1 / 3) ∈ ℂ)
301298, 299, 300mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 / 3) ∈ ℂ
302301a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → (1 / 3) ∈ ℂ)
303295, 296, 302subsub4d 11543 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) = (𝑗 − (1 + (1 / 3))))
304 3cn 12234 . . . . . . . . . . . . . . . . . . . . . . . . . 26 3 ∈ ℂ
305304, 203, 304, 23divdiri 11912 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
306 3p1e4 12298 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 + 1) = 4
307306oveq1i 7367 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 + 1) / 3) = (4 / 3)
308304, 23dividi 11888 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (3 / 3) = 1
309308oveq1i 7367 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
310305, 307, 3093eqtr3i 2772 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 / 3) = (1 + (1 / 3))
311310a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 ∈ ℝ → (4 / 3) = (1 + (1 / 3)))
312311oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 ∈ ℝ → (𝑗 − (4 / 3)) = (𝑗 − (1 + (1 / 3))))
313303, 312eqtr4d 2779 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ ℝ → ((𝑗 − 1) − (1 / 3)) = (𝑗 − (4 / 3)))
314313oveq1d 7372 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ ℝ → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
315294, 314syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (((𝑗 − 1) − (1 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
316315breq2d 5117 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
317316anbi2d 629 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ((𝑡𝑇 ∧ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)) ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))))
318293, 317bitrid 282 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝑗 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))))
319292, 318mtbid 323 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
320 imnan 400 . . . . . . . . . . . . . . 15 ((𝑡𝑇 → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)) ↔ ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
321319, 320sylibr 233 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → (𝑡𝑇 → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
322256, 321mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ ¬ 𝑡 ∈ (𝐷‘(𝑗 − 1)))) → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))
323255, 322sylanr2 681 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸))
324230adantrr 715 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ ℝ)
325 4re 12237 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ
326325a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 4 ∈ ℝ)
32722a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ∈ ℝ)
32823a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 3 ≠ 0)
329326, 327, 328redivcld 11983 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (4 / 3) ∈ ℝ)
330324, 329resubcld 11583 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 − (4 / 3)) ∈ ℝ)
33137ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ)
332 remulcl 11136 . . . . . . . . . . . . . . 15 (((𝑗 − (4 / 3)) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ)
333332rexrd 11205 . . . . . . . . . . . . . 14 (((𝑗 − (4 / 3)) ∈ ℝ ∧ 𝐸 ∈ ℝ) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*)
334330, 331, 333syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ*)
33546rexrd 11205 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → (𝐹𝑡) ∈ ℝ*)
336335adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹𝑡) ∈ ℝ*)
337 xrltnle 11222 . . . . . . . . . . . . 13 ((((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ* ∧ (𝐹𝑡) ∈ ℝ*) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
338334, 336, 337syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (4 / 3)) · 𝐸)))
339323, 338mpbird 256 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡))
340 simpl 483 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝜑𝑡𝑇))
341 simprr 771 . . . . . . . . . . . . 13 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
342341eldifad 3922 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡 ∈ (𝐷𝑗))
343 simplll 773 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝜑)
344175adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑗 ∈ (1...𝑁))
345 simpr 485 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ (𝐷𝑗))
346 oveq1 7364 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑗 → (𝑘 − (1 / 3)) = (𝑗 − (1 / 3)))
347346oveq1d 7372 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑗 → ((𝑘 − (1 / 3)) · 𝐸) = ((𝑗 − (1 / 3)) · 𝐸))
348347breq2d 5117 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑗 → ((𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
349348rabbidv 3415 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑗 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑘 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
350 fz1ssfz0 13537 . . . . . . . . . . . . . . . . . . . 20 (1...𝑁) ⊆ (0...𝑁)
351350sseli 3940 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ (0...𝑁))
352351adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (0...𝑁))
353 rabexg 5288 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
354285, 353syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (1...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
355265, 349, 352, 354fvmptd3 6971 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (1...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
356355eleq2d 2823 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑡 ∈ (𝐷𝑗) ↔ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}))
357356biimpa 477 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
358343, 344, 345, 357syl21anc 836 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
359 rabid 3427 . . . . . . . . . . . . . 14 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
360358, 359sylib 217 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
361360simprd 496 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑡 ∈ (𝐷𝑗)) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
362340, 254, 342, 361syl21anc 836 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
363339, 362jca 512 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
36415ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑁 ∈ ℕ)
365 simplr 767 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑡𝑇)
366175adantrr 715 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝑗 ∈ (1...𝑁))
367 nfv 1917 . . . . . . . . . . . . . . . 16 𝑗 𝑖 ∈ (0...𝑁)
368102, 367nfan 1902 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁))
369 nfv 1917 . . . . . . . . . . . . . . 15 𝑗(𝑋𝑖):𝑇⟶ℝ
370368, 369nfim 1899 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
371 eleq1w 2820 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑗 ∈ (0...𝑁) ↔ 𝑖 ∈ (0...𝑁)))
372371anbi2d 629 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑖 ∈ (0...𝑁))))
373 fveq2 6842 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑋𝑗) = (𝑋𝑖))
374373feq1d 6653 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑋𝑗):𝑇⟶ℝ ↔ (𝑋𝑖):𝑇⟶ℝ))
375372, 374imbi12d 344 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ) ↔ ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)))
376 stoweidlem34.14 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑋𝑗):𝑇⟶ℝ)
377370, 375, 376chvarfv 2233 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
378377ad4ant14 750 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
379 simplll 773 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝜑)
380 simpr 485 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁))
381 simpllr 774 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑡𝑇)
382102, 367, 103nf3an 1904 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇)
383 nfv 1917 . . . . . . . . . . . . . . 15 𝑗((𝑋𝑖)‘𝑡) ≤ 1
384382, 383nfim 1899 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)
3853713anbi2d 1441 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇)))
386373fveq1d 6844 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → ((𝑋𝑗)‘𝑡) = ((𝑋𝑖)‘𝑡))
387386breq1d 5115 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (((𝑋𝑗)‘𝑡) ≤ 1 ↔ ((𝑋𝑖)‘𝑡) ≤ 1))
388385, 387imbi12d 344 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)))
389 stoweidlem34.16 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑗)‘𝑡) ≤ 1)
390384, 388, 389chvarfv 2233 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → ((𝑋𝑖)‘𝑡) ≤ 1)
391379, 380, 381, 390syl3anc 1371 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑡) ≤ 1)
392 simplll 773 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑)
393 0zd 12511 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ)
394 elfzel2 13439 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑗...𝑁) → 𝑁 ∈ ℤ)
395394adantl 482 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ)
396 elfzelz 13441 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℤ)
397396adantl 482 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ)
398 0red 11158 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℝ)
399 elfzel1 13440 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℤ)
400399zred 12607 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑗 ∈ ℝ)
401400adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ)
402396zred 12607 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑖 ∈ ℝ)
403402adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
404 0red 11158 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ∈ ℝ)
405 1red 11156 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 1 ∈ ℝ)
406 0le1 11678 . . . . . . . . . . . . . . . . . . 19 0 ≤ 1
407406a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ≤ 1)
408 elfzle1 13444 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ (1...𝑁) → 1 ≤ 𝑗)
409175, 408syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 1 ≤ 𝑗)
410404, 405, 230, 407, 409letrd 11312 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) → 0 ≤ 𝑗)
411410adantr 481 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑗)
412 elfzle1 13444 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (𝑗...𝑁) → 𝑗𝑖)
413412adantl 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗𝑖)
414398, 401, 403, 411, 413letrd 11312 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ≤ 𝑖)
415 elfzle2 13445 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (𝑗...𝑁) → 𝑖𝑁)
416415adantl 482 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖𝑁)
417393, 395, 397, 414, 416elfzd 13432 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
418417adantlrr 719 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
419 simpll 765 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑𝑡𝑇))
420 simplrl 775 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽𝑡))
421 simplrr 776 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
422421eldifad 3922 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑗))
423 simpr 485 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁))
424 simpl1 1191 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝜑𝑡𝑇))
425424simprd 496 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡𝑇)
426424, 46syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ∈ ℝ)
427400adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ ℝ)
42824a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈ ℝ)
429427, 428resubcld 11583 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
430 simpl1l 1224 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝜑)
431430, 37syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
432429, 431remulcld 11185 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
433402adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
43424a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (1 / 3) ∈ ℝ)
435433, 434resubcld 11583 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈ ℝ)
43637adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
437435, 436remulcld 11185 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ)
438430, 437sylancom 588 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑖 − (1 / 3)) · 𝐸) ∈ ℝ)
439 simpl3 1193 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑗))
440 simpl2 1192 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (𝐽𝑡))
441424, 440, 175syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗 ∈ (1...𝑁))
442430, 441, 355syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
443439, 442eleqtrd 2840 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
444443, 359sylib 217 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
445444simprd 496 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
446402adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℝ)
447412adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑗𝑖)
448427, 446, 428, 447lesub1dd 11771 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)))
449430, 435sylancom 588 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑖 − (1 / 3)) ∈ ℝ)
45036rpregt0d 12963 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
451430, 450syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
452 lemul1 12007 . . . . . . . . . . . . . . . . . . 19 (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑖 − (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
453429, 449, 451, 452syl3anc 1371 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) ≤ (𝑖 − (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
454448, 453mpbid 231 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ≤ ((𝑖 − (1 / 3)) · 𝐸))
455426, 432, 438, 445, 454letrd 11312 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸))
456 rabid 3427 . . . . . . . . . . . . . . . 16 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
457425, 455, 456sylanbrc 583 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
458 simpr 485 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (𝑗...𝑁))
459 0zd 12511 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 ∈ ℤ)
4603943ad2ant3 1135 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℤ)
4613963ad2ant3 1135 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ ℤ)
462459, 460, 4613jca 1128 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ))
463414, 416jca 512 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖𝑖𝑁))
4644633impa 1110 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → (0 ≤ 𝑖𝑖𝑁))
465 elfz2 13431 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ) ∧ (0 ≤ 𝑖𝑖𝑁)))
466462, 464, 465sylanbrc 583 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
467424, 440, 458, 466syl3anc 1371 . . . . . . . . . . . . . . . 16 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
468 oveq1 7364 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (𝑗 − (1 / 3)) = (𝑖 − (1 / 3)))
469468oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝑖 − (1 / 3)) · 𝐸))
470469breq2d 5117 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)))
471470rabbidv 3415 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑖 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
472 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0...𝑁))
473 rabexg 5288 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
47467, 473syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
475474adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)} ∈ V)
47657, 471, 472, 475fvmptd3 6971 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
477430, 467, 476syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐷𝑖) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑖 − (1 / 3)) · 𝐸)})
478457, 477eleqtrrd 2841 . . . . . . . . . . . . . 14 ((((𝜑𝑡𝑇) ∧ 𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ (𝐷𝑗)) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑖))
479419, 420, 422, 423, 478syl31anc 1373 . . . . . . . . . . . . 13 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ (𝐷𝑖))
480102, 367, 221nf3an 1904 . . . . . . . . . . . . . . 15 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖))
481 nfv 1917 . . . . . . . . . . . . . . 15 𝑗((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁)
482480, 481nfim 1899 . . . . . . . . . . . . . 14 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
483371, 2233anbi23d 1439 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖))))
484386breq1d 5115 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁)))
485483, 484imbi12d 344 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))))
486 stoweidlem34.17 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑗)) → ((𝑋𝑗)‘𝑡) < (𝐸 / 𝑁))
487482, 485, 486chvarfv 2233 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐷𝑖)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
488392, 418, 479, 487syl3anc 1371 . . . . . . . . . . . 12 ((((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
48936ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 ∈ ℝ+)
490 stoweidlem34.13 . . . . . . . . . . . . 13 (𝜑𝐸 < (1 / 3))
491490ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → 𝐸 < (1 / 3))
492364, 365, 366, 378, 391, 488, 489, 491stoweidlem11 44242 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸))
493 eleq1w 2820 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑙 ∈ (𝐽𝑡) ↔ 𝑗 ∈ (𝐽𝑡)))
494 fveq2 6842 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑗 → (𝐷𝑙) = (𝐷𝑗))
495 oveq1 7364 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑗 → (𝑙 − 1) = (𝑗 − 1))
496495fveq2d 6846 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑗 → (𝐷‘(𝑙 − 1)) = (𝐷‘(𝑗 − 1)))
497494, 496difeq12d 4083 . . . . . . . . . . . . . . . . . 18 (𝑙 = 𝑗 → ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) = ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))
498497eleq2d 2823 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))
499493, 498anbi12d 631 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑗 → ((𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))))
500499anbi2d 629 . . . . . . . . . . . . . . 15 (𝑙 = 𝑗 → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))))))
501 oveq1 7364 . . . . . . . . . . . . . . . . 17 (𝑙 = 𝑗 → (𝑙 − (4 / 3)) = (𝑗 − (4 / 3)))
502501oveq1d 7372 . . . . . . . . . . . . . . . 16 (𝑙 = 𝑗 → ((𝑙 − (4 / 3)) · 𝐸) = ((𝑗 − (4 / 3)) · 𝐸))
503502breq1d 5115 . . . . . . . . . . . . . . 15 (𝑙 = 𝑗 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) ↔ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
504500, 503imbi12d 344 . . . . . . . . . . . . . 14 (𝑙 = 𝑗 → ((((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)) ↔ (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
505 eleq1w 2820 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑠𝑇𝑡𝑇))
506505anbi2d 629 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝜑𝑠𝑇) ↔ (𝜑𝑡𝑇)))
507 fveq2 6842 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑡 → (𝐽𝑠) = (𝐽𝑡))
508507eleq2d 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑙 ∈ (𝐽𝑠) ↔ 𝑙 ∈ (𝐽𝑡)))
509 eleq1w 2820 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = 𝑡 → (𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))) ↔ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
510508, 509anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))) ↔ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))))
511506, 510anbi12d 631 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ↔ ((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))))
512 fveq2 6842 . . . . . . . . . . . . . . . . . . 19 (𝑠 = 𝑡 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠) = ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
513512breq2d 5117 . . . . . . . . . . . . . . . . . 18 (𝑠 = 𝑡 → (((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠) ↔ ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
514511, 513imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑠 = 𝑡 → ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠)) ↔ (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
515 stoweidlem34.1 . . . . . . . . . . . . . . . . . 18 𝑡𝐹
516 nfv 1917 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑠𝑇
517102, 516nfan 1902 . . . . . . . . . . . . . . . . . . 19 𝑗(𝜑𝑠𝑇)
518 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . 22 𝑗𝑠
51991, 518nffv 6852 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝐽𝑠)
520519nfcri 2894 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑙 ∈ (𝐽𝑠)
521 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗𝑙
52276, 521nffv 6852 . . . . . . . . . . . . . . . . . . . . . 22 𝑗(𝐷𝑙)
523 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗(𝑙 − 1)
52476, 523nffv 6852 . . . . . . . . . . . . . . . . . . . . . 22 𝑗(𝐷‘(𝑙 − 1))
525522, 524nfdif 4085 . . . . . . . . . . . . . . . . . . . . 21 𝑗((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
526525nfcri 2894 . . . . . . . . . . . . . . . . . . . 20 𝑗 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
527520, 526nfan 1902 . . . . . . . . . . . . . . . . . . 19 𝑗(𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
528517, 527nfan 1902 . . . . . . . . . . . . . . . . . 18 𝑗((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
529 nfv 1917 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑠𝑇
5301, 529nfan 1902 . . . . . . . . . . . . . . . . . . 19 𝑡(𝜑𝑠𝑇)
531 nfmpt1 5213 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑡𝑇 ↦ {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)})
5325, 531nfcxfr 2905 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝐽
533 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . 22 𝑡𝑠
534532, 533nffv 6852 . . . . . . . . . . . . . . . . . . . . 21 𝑡(𝐽𝑠)
535534nfcri 2894 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑙 ∈ (𝐽𝑠)
536 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡𝑙
537162, 536nffv 6852 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝐷𝑙)
538 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑙 − 1)
539162, 538nffv 6852 . . . . . . . . . . . . . . . . . . . . . 22 𝑡(𝐷‘(𝑙 − 1))
540537, 539nfdif 4085 . . . . . . . . . . . . . . . . . . . . 21 𝑡((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
541540nfcri 2894 . . . . . . . . . . . . . . . . . . . 20 𝑡 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))
542535, 541nfan 1902 . . . . . . . . . . . . . . . . . . 19 𝑡(𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
543530, 542nfan 1902 . . . . . . . . . . . . . . . . . 18 𝑡((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1)))))
544 stoweidlem34.5 . . . . . . . . . . . . . . . . . 18 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
54515ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑁 ∈ ℕ)
54667ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑇 ∈ V)
5473rabex 5289 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ∈ V
548 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑡𝑗
549162, 548nffv 6852 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡(𝐷𝑗)
550549nfcri 2894 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 𝑠 ∈ (𝐷𝑗)
551 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(1...𝑁)
552550, 551nfrabw 3440 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡{𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)}
553 eleq1w 2820 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑠 → (𝑡 ∈ (𝐷𝑗) ↔ 𝑠 ∈ (𝐷𝑗)))
554553rabbidv 3415 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑠 → {𝑗 ∈ (1...𝑁) ∣ 𝑡 ∈ (𝐷𝑗)} = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
555533, 552, 554, 5fvmptf 6969 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑠𝑇 ∧ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ∈ V) → (𝐽𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
556547, 555mpan2 689 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑠𝑇 → (𝐽𝑠) = {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
557556eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠𝑇 → (𝑙 ∈ (𝐽𝑠) ↔ 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)}))
558557biimpa 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → 𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)})
559522nfcri 2894 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 𝑠 ∈ (𝐷𝑙)
560 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑙 → (𝐷𝑗) = (𝐷𝑙))
561560eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑙 → (𝑠 ∈ (𝐷𝑗) ↔ 𝑠 ∈ (𝐷𝑙)))
562521, 74, 559, 561elrabf 3641 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ {𝑗 ∈ (1...𝑁) ∣ 𝑠 ∈ (𝐷𝑗)} ↔ (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷𝑙)))
563558, 562sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → (𝑙 ∈ (1...𝑁) ∧ 𝑠 ∈ (𝐷𝑙)))
564563simpld 495 . . . . . . . . . . . . . . . . . . 19 ((𝑠𝑇𝑙 ∈ (𝐽𝑠)) → 𝑙 ∈ (1...𝑁))
565564ad2ant2lr 746 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑙 ∈ (1...𝑁))
566 simprr 771 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))
56745ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐹:𝑇⟶ℝ)
56836ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 ∈ ℝ+)
569490ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → 𝐸 < (1 / 3))
570377ad4ant14 750 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
571 simp1ll 1236 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 𝜑)
572 nfv 1917 . . . . . . . . . . . . . . . . . . . . 21 𝑗0 ≤ ((𝑋𝑖)‘𝑡)
573382, 572nfim 1899 . . . . . . . . . . . . . . . . . . . 20 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
574386breq2d 5117 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → (0 ≤ ((𝑋𝑗)‘𝑡) ↔ 0 ≤ ((𝑋𝑖)‘𝑡)))
575385, 574imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))))
576 stoweidlem34.15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑗)‘𝑡))
577573, 575, 576chvarfv 2233 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
578571, 577syld3an1 1410 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
579 simp1ll 1236 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → 𝜑)
580 nfmpt1 5213 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
581544, 580nfcxfr 2905 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑗𝐵
582581, 219nffv 6852 . . . . . . . . . . . . . . . . . . . . . . 23 𝑗(𝐵𝑖)
583582nfcri 2894 . . . . . . . . . . . . . . . . . . . . . 22 𝑗 𝑡 ∈ (𝐵𝑖)
584102, 367, 583nf3an 1904 . . . . . . . . . . . . . . . . . . . . 21 𝑗(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖))
585 nfv 1917 . . . . . . . . . . . . . . . . . . . . 21 𝑗(1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)
586584, 585nfim 1899 . . . . . . . . . . . . . . . . . . . 20 𝑗((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
587 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑖 → (𝐵𝑗) = (𝐵𝑖))
588587eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑖 → (𝑡 ∈ (𝐵𝑗) ↔ 𝑡 ∈ (𝐵𝑖)))
589371, 5883anbi23d 1439 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖))))
590386breq2d 5117 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑖 → ((1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)))
591589, 590imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑖 → (((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))))
592 stoweidlem34.18 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑗)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑗)‘𝑡))
593586, 591, 592chvarfv 2233 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
594579, 593syld3an1 1410 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
595515, 528, 543, 57, 544, 545, 546, 565, 566, 567, 568, 569, 570, 578, 594stoweidlem26 44257 . . . . . . . . . . . . . . . . 17 (((𝜑𝑠𝑇) ∧ (𝑙 ∈ (𝐽𝑠) ∧ 𝑠 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑠))
596514, 595vtoclg 3525 . . . . . . . . . . . . . . . 16 (𝑡𝑇 → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
597596ad2antlr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
598597pm2.43i 52 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ (𝑙 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑙) ∖ (𝐷‘(𝑙 − 1))))) → ((𝑙 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
599504, 598vtoclg 3525 . . . . . . . . . . . . 13 (𝑗 ∈ (𝐽𝑡) → (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
600599ad2antrl 726 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
601600pm2.43i 52 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))
602492, 601jca 512 . . . . . . . . . 10 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))
603254, 363, 6023jca 1128 . . . . . . . . 9 (((𝜑𝑡𝑇) ∧ (𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1))))) → (𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
604603ex 413 . . . . . . . 8 ((𝜑𝑡𝑇) → ((𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))) → (𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
605104, 604eximd 2209 . . . . . . 7 ((𝜑𝑡𝑇) → (∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ 𝑡 ∈ ((𝐷𝑗) ∖ (𝐷‘(𝑗 − 1)))) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
606253, 605mpd 15 . . . . . 6 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
607 3anass 1095 . . . . . . 7 ((𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ (𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
608607exbii 1850 . . . . . 6 (∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ (((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
609606, 608sylib 217 . . . . 5 ((𝜑𝑡𝑇) → ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
610 df-rex 3074 . . . . 5 (∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) ↔ ∃𝑗(𝑗 ∈ (𝐽𝑡) ∧ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
611609, 610sylibr 233 . . . 4 ((𝜑𝑡𝑇) → ∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
612 nfcv 2907 . . . . 5 𝑗
61393, 612ssrexf 4008 . . . 4 ((𝐽𝑡) ⊆ ℝ → (∃𝑗 ∈ (𝐽𝑡)((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))) → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
61414, 611, 613sylc 65 . . 3 ((𝜑𝑡𝑇) → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
615614ex 413 . 2 (𝜑 → (𝑡𝑇 → ∃𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡)))))
6161, 615ralrimi 3240 1 (𝜑 → ∀𝑡𝑇𝑗 ∈ ℝ ((((𝑗 − (4 / 3)) · 𝐸) < (𝐹𝑡) ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)) ∧ (((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸) ∧ ((𝑗 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087  wal 1539   = wceq 1541  wex 1781  wnf 1785  wcel 2106  wnfc 2887  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cdif 3907  wss 3910  c0 4282   class class class wbr 5105  cmpt 5188  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  *cxr 11188   < clt 11189  cle 11190  cmin 11385  -cneg 11386   / cdiv 11812  cn 12153  3c3 12209  4c4 12210  0cn0 12413  cz 12499  cuz 12763  +crp 12915  ...cfz 13424  Σcsu 15570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-ico 13270  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571
This theorem is referenced by:  stoweidlem60  44291
  Copyright terms: Public domain W3C validator