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

Theorem stoweidlem26 42461
Description: This lemma is used to prove that there is a function 𝑔 as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here 𝐿 is used to represnt j in the paper, 𝐷 is used to represent A in the paper, 𝑆 is used to represent t, and 𝐸 is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem26.1 𝑡𝐹
stoweidlem26.2 𝑗𝜑
stoweidlem26.3 𝑡𝜑
stoweidlem26.4 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
stoweidlem26.5 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
stoweidlem26.6 (𝜑𝑁 ∈ ℕ)
stoweidlem26.7 (𝜑𝑇 ∈ V)
stoweidlem26.8 (𝜑𝐿 ∈ (1...𝑁))
stoweidlem26.9 (𝜑𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))))
stoweidlem26.10 (𝜑𝐹:𝑇⟶ℝ)
stoweidlem26.11 (𝜑𝐸 ∈ ℝ+)
stoweidlem26.12 (𝜑𝐸 < (1 / 3))
stoweidlem26.13 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
stoweidlem26.14 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
stoweidlem26.15 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
Assertion
Ref Expression
stoweidlem26 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆))
Distinct variable groups:   𝑖,𝑗,𝑡,𝐸   𝑖,𝐿,𝑗,𝑡   𝑖,𝑁,𝑗,𝑡   𝑆,𝑖,𝑡   𝜑,𝑖   𝑗,𝐹   𝑇,𝑗,𝑡   𝑡,𝑋
Allowed substitution hints:   𝜑(𝑡,𝑗)   𝐵(𝑡,𝑖,𝑗)   𝐷(𝑡,𝑖,𝑗)   𝑆(𝑗)   𝑇(𝑖)   𝐹(𝑡,𝑖)   𝑋(𝑖,𝑗)

Proof of Theorem stoweidlem26
StepHypRef Expression
1 1re 10618 . . . . . . . 8 1 ∈ ℝ
2 eleq1 2899 . . . . . . . 8 (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
31, 2mpbiri 261 . . . . . . 7 (𝐿 = 1 → 𝐿 ∈ ℝ)
43adantl 485 . . . . . 6 ((𝜑𝐿 = 1) → 𝐿 ∈ ℝ)
5 4re 11699 . . . . . . . 8 4 ∈ ℝ
65a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 4 ∈ ℝ)
7 3re 11695 . . . . . . . 8 3 ∈ ℝ
87a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 3 ∈ ℝ)
9 3ne0 11721 . . . . . . . 8 3 ≠ 0
109a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 3 ≠ 0)
116, 8, 10redivcld 11445 . . . . . 6 ((𝜑𝐿 = 1) → (4 / 3) ∈ ℝ)
124, 11resubcld 11045 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
13 stoweidlem26.11 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
1413rpred 12409 . . . . . 6 (𝜑𝐸 ∈ ℝ)
1514adantr 484 . . . . 5 ((𝜑𝐿 = 1) → 𝐸 ∈ ℝ)
1612, 15remulcld 10648 . . . 4 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
17 0red 10621 . . . 4 ((𝜑𝐿 = 1) → 0 ∈ ℝ)
18 fzfid 13324 . . . . . 6 (𝜑 → (0...𝑁) ∈ Fin)
1914adantr 484 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
20 stoweidlem26.13 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
21 stoweidlem26.9 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))))
22 eldif 3920 . . . . . . . . . . . . . 14 (𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
2321, 22sylib 221 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∈ (𝐷𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
2423simpld 498 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (𝐷𝐿))
25 stoweidlem26.4 . . . . . . . . . . . . 13 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
26 oveq1 7137 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3)))
2726oveq1d 7145 . . . . . . . . . . . . . . 15 (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸))
2827breq2d 5051 . . . . . . . . . . . . . 14 (𝑗 = 𝐿 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
2928rabbidv 3457 . . . . . . . . . . . . 13 (𝑗 = 𝐿 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
30 fz1ssfz0 12986 . . . . . . . . . . . . . 14 (1...𝑁) ⊆ (0...𝑁)
31 stoweidlem26.8 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ (1...𝑁))
3230, 31sseldi 3941 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (0...𝑁))
33 stoweidlem26.7 . . . . . . . . . . . . . 14 (𝜑𝑇 ∈ V)
34 rabexg 5207 . . . . . . . . . . . . . 14 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
3533, 34syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
3625, 29, 32, 35fvmptd3 6764 . . . . . . . . . . . 12 (𝜑 → (𝐷𝐿) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
3724, 36eleqtrd 2914 . . . . . . . . . . 11 (𝜑𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
38 nfcv 2974 . . . . . . . . . . . 12 𝑡𝑆
39 nfcv 2974 . . . . . . . . . . . 12 𝑡𝑇
40 stoweidlem26.1 . . . . . . . . . . . . . 14 𝑡𝐹
4140, 38nffv 6653 . . . . . . . . . . . . 13 𝑡(𝐹𝑆)
42 nfcv 2974 . . . . . . . . . . . . 13 𝑡
43 nfcv 2974 . . . . . . . . . . . . 13 𝑡((𝐿 − (1 / 3)) · 𝐸)
4441, 42, 43nfbr 5086 . . . . . . . . . . . 12 𝑡(𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)
45 fveq2 6643 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (𝐹𝑡) = (𝐹𝑆))
4645breq1d 5049 . . . . . . . . . . . 12 (𝑡 = 𝑆 → ((𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4738, 39, 44, 46elrabf 3653 . . . . . . . . . . 11 (𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆𝑇 ∧ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4837, 47sylib 221 . . . . . . . . . 10 (𝜑 → (𝑆𝑇 ∧ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4948simpld 498 . . . . . . . . 9 (𝜑𝑆𝑇)
5049adantr 484 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑆𝑇)
5120, 50ffvelrnd 6825 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
5219, 51remulcld 10648 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
5318, 52fsumrecl 15070 . . . . 5 (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
5453adantr 484 . . . 4 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
555, 7, 9redivcli 11384 . . . . . . 7 (4 / 3) ∈ ℝ
5655a1i 11 . . . . . 6 ((𝜑𝐿 = 1) → (4 / 3) ∈ ℝ)
574, 56resubcld 11045 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
584recnd 10646 . . . . . . . 8 ((𝜑𝐿 = 1) → 𝐿 ∈ ℂ)
5958subid1d 10963 . . . . . . 7 ((𝜑𝐿 = 1) → (𝐿 − 0) = 𝐿)
60 3cn 11696 . . . . . . . . . 10 3 ∈ ℂ
6160, 9dividi 11350 . . . . . . . . 9 (3 / 3) = 1
62 3lt4 11789 . . . . . . . . . 10 3 < 4
63 3pos 11720 . . . . . . . . . . 11 0 < 3
647, 5, 7, 63ltdiv1ii 11546 . . . . . . . . . 10 (3 < 4 ↔ (3 / 3) < (4 / 3))
6562, 64mpbi 233 . . . . . . . . 9 (3 / 3) < (4 / 3)
6661, 65eqbrtrri 5062 . . . . . . . 8 1 < (4 / 3)
67 breq1 5042 . . . . . . . . 9 (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
6867adantl 485 . . . . . . . 8 ((𝜑𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
6966, 68mpbiri 261 . . . . . . 7 ((𝜑𝐿 = 1) → 𝐿 < (4 / 3))
7059, 69eqbrtrd 5061 . . . . . 6 ((𝜑𝐿 = 1) → (𝐿 − 0) < (4 / 3))
714, 17, 56, 70ltsub23d 11222 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) < 0)
7213rpgt0d 12412 . . . . . 6 (𝜑 → 0 < 𝐸)
7372adantr 484 . . . . 5 ((𝜑𝐿 = 1) → 0 < 𝐸)
74 mulltgt0 41436 . . . . 5 ((((𝐿 − (4 / 3)) ∈ ℝ ∧ (𝐿 − (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
7557, 71, 15, 73, 74syl22anc 837 . . . 4 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
76 0cn 10610 . . . . . . . 8 0 ∈ ℂ
77 fsumconst 15124 . . . . . . . 8 (((0...𝑁) ∈ Fin ∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
7818, 76, 77sylancl 589 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
79 hashcl 13701 . . . . . . . . 9 ((0...𝑁) ∈ Fin → (♯‘(0...𝑁)) ∈ ℕ0)
80 nn0cn 11885 . . . . . . . . 9 ((♯‘(0...𝑁)) ∈ ℕ0 → (♯‘(0...𝑁)) ∈ ℂ)
8118, 79, 803syl 18 . . . . . . . 8 (𝜑 → (♯‘(0...𝑁)) ∈ ℂ)
8281mul01d 10816 . . . . . . 7 (𝜑 → ((♯‘(0...𝑁)) · 0) = 0)
8378, 82eqtrd 2856 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0)
8483adantr 484 . . . . 5 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0)
85 0red 10621 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ)
8613rpge0d 12413 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐸)
8786adantr 484 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸)
88 stoweidlem26.3 . . . . . . . . . . . 12 𝑡𝜑
89 nfv 1916 . . . . . . . . . . . 12 𝑡 𝑖 ∈ (0...𝑁)
9088, 89nfan 1901 . . . . . . . . . . 11 𝑡(𝜑𝑖 ∈ (0...𝑁))
91 nfv 1916 . . . . . . . . . . 11 𝑡0 ≤ ((𝑋𝑖)‘𝑆)
9290, 91nfim 1898 . . . . . . . . . 10 𝑡((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
93 fveq2 6643 . . . . . . . . . . . 12 (𝑡 = 𝑆 → ((𝑋𝑖)‘𝑡) = ((𝑋𝑖)‘𝑆))
9493breq2d 5051 . . . . . . . . . . 11 (𝑡 = 𝑆 → (0 ≤ ((𝑋𝑖)‘𝑡) ↔ 0 ≤ ((𝑋𝑖)‘𝑆)))
9594imbi2d 344 . . . . . . . . . 10 (𝑡 = 𝑆 → (((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))))
96 stoweidlem26.14 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
97963expia 1118 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑡𝑇 → 0 ≤ ((𝑋𝑖)‘𝑡)))
9897com12 32 . . . . . . . . . 10 (𝑡𝑇 → ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑡)))
9938, 92, 95, 98vtoclgaf 3550 . . . . . . . . 9 (𝑆𝑇 → ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆)))
10050, 99mpcom 38 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
10119, 51, 87, 100mulge0d 11194 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
10218, 85, 52, 101fsumle 15133 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
103102adantr 484 . . . . 5 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
10484, 103eqbrtrrd 5063 . . . 4 ((𝜑𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
10516, 17, 54, 75, 104ltletrd 10777 . . 3 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
106 elfzelz 12891 . . . . . . . . 9 (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ)
107 zre 11963 . . . . . . . . 9 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
10831, 106, 1073syl 18 . . . . . . . 8 (𝜑𝐿 ∈ ℝ)
1095a1i 11 . . . . . . . . 9 (𝜑 → 4 ∈ ℝ)
1107a1i 11 . . . . . . . . 9 (𝜑 → 3 ∈ ℝ)
1119a1i 11 . . . . . . . . 9 (𝜑 → 3 ≠ 0)
112109, 110, 111redivcld 11445 . . . . . . . 8 (𝜑 → (4 / 3) ∈ ℝ)
113108, 112resubcld 11045 . . . . . . 7 (𝜑 → (𝐿 − (4 / 3)) ∈ ℝ)
114113, 14remulcld 10648 . . . . . 6 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
115114adantr 484 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
1161a1i 11 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ)
117 stoweidlem26.6 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
11814, 117nndivred 11669 . . . . . . . . 9 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
119116, 118resubcld 11045 . . . . . . . 8 (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ)
120108, 116resubcld 11045 . . . . . . . 8 (𝜑 → (𝐿 − 1) ∈ ℝ)
121119, 120remulcld 10648 . . . . . . 7 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
12214, 121remulcld 10648 . . . . . 6 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
123122adantr 484 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
124 fzfid 13324 . . . . . . . 8 (𝜑 → (0...(𝐿 − 2)) ∈ Fin)
12531, 106syl 17 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ ℤ)
126 2z 11992 . . . . . . . . . . . . . . 15 2 ∈ ℤ
127126a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℤ)
128125, 127zsubcld 12070 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 2) ∈ ℤ)
129117nnzd 12064 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℤ)
130125zred 12065 . . . . . . . . . . . . . . 15 (𝜑𝐿 ∈ ℝ)
131 2re 11689 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
132131a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℝ)
133130, 132resubcld 11045 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ∈ ℝ)
134117nnred 11630 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
135 0le2 11717 . . . . . . . . . . . . . . . 16 0 ≤ 2
136 0red 10621 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
137136, 132, 130lesub2d 11225 . . . . . . . . . . . . . . . 16 (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0)))
138135, 137mpbii 236 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0))
139125zcnd 12066 . . . . . . . . . . . . . . . 16 (𝜑𝐿 ∈ ℂ)
140139subid1d 10963 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 0) = 𝐿)
141138, 140breqtrd 5065 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ≤ 𝐿)
142 elfzle2 12894 . . . . . . . . . . . . . . 15 (𝐿 ∈ (1...𝑁) → 𝐿𝑁)
14331, 142syl 17 . . . . . . . . . . . . . 14 (𝜑𝐿𝑁)
144133, 130, 134, 141, 143letrd 10774 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 2) ≤ 𝑁)
145128, 129, 1443jca 1125 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
146 eluz2 12227 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
147145, 146sylibr 237 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝐿 − 2)))
148 fzss2 12930 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
149147, 148syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁))
150149sselda 3943 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
151150, 51syldan 594 . . . . . . . 8 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
152124, 151fsumrecl 15070 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ)
15314, 152remulcld 10648 . . . . . 6 (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ)
154153adantr 484 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ)
15514, 120remulcld 10648 . . . . . . . . 9 (𝜑 → (𝐸 · (𝐿 − 1)) ∈ ℝ)
15614, 14remulcld 10648 . . . . . . . . 9 (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
157155, 156resubcld 11045 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ)
158120, 117nndivred 11669 . . . . . . . . . 10 (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ)
159156, 158remulcld 10648 . . . . . . . . 9 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ)
160155, 159resubcld 11045 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ)
161120, 14resubcld 11045 . . . . . . . . . 10 (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ)
162116, 14readdcld 10647 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) ∈ ℝ)
1631, 7, 9redivcli 11384 . . . . . . . . . . . . . . 15 (1 / 3) ∈ ℝ
164163a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 / 3) ∈ ℝ)
165 stoweidlem26.12 . . . . . . . . . . . . . 14 (𝜑𝐸 < (1 / 3))
16614, 164, 116, 165ltadd2dd 10776 . . . . . . . . . . . . 13 (𝜑 → (1 + 𝐸) < (1 + (1 / 3)))
167 ax-1cn 10572 . . . . . . . . . . . . . . 15 1 ∈ ℂ
16860, 167, 60, 9divdiri 11374 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
169 3p1e4 11760 . . . . . . . . . . . . . . 15 (3 + 1) = 4
170169oveq1i 7140 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = (4 / 3)
17161oveq1i 7140 . . . . . . . . . . . . . 14 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
172168, 170, 1713eqtr3ri 2853 . . . . . . . . . . . . 13 (1 + (1 / 3)) = (4 / 3)
173166, 172breqtrdi 5080 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) < (4 / 3))
174162, 112, 108, 173ltsub2dd 11230 . . . . . . . . . . 11 (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸)))
175167a1i 11 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
17613rpcnd 12411 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℂ)
177139, 175, 176subsub4d 11005 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸)))
178174, 177breqtrrd 5067 . . . . . . . . . 10 (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸))
179113, 161, 13, 178ltmul1dd 12464 . . . . . . . . 9 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸))
180139, 175subcld 10974 . . . . . . . . . . . 12 (𝜑 → (𝐿 − 1) ∈ ℂ)
181180, 176subcld 10974 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ)
182176, 181mulcomd 10639 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸))
183176, 180, 176subdid 11073 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
184182, 183eqtr3d 2858 . . . . . . . . 9 (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
185179, 184breqtrd 5065 . . . . . . . 8 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
186 1zzd 11991 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
187 elfz 12881 . . . . . . . . . . . . . . . . 17 ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿𝐿𝑁)))
188125, 186, 129, 187syl3anc 1368 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿𝐿𝑁)))
18931, 188mpbid 235 . . . . . . . . . . . . . . 15 (𝜑 → (1 ≤ 𝐿𝐿𝑁))
190189simprd 499 . . . . . . . . . . . . . 14 (𝜑𝐿𝑁)
191 zlem1lt 12012 . . . . . . . . . . . . . . 15 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿𝑁 ↔ (𝐿 − 1) < 𝑁))
192125, 129, 191syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → (𝐿𝑁 ↔ (𝐿 − 1) < 𝑁))
193190, 192mpbid 235 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 1) < 𝑁)
194117nngt0d 11664 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑁)
195 ltdiv1 11481 . . . . . . . . . . . . . 14 (((𝐿 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
196120, 134, 134, 194, 195syl112anc 1371 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
197193, 196mpbid 235 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))
198117nncnd 11631 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
199117nnne0d 11665 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
200198, 199dividd 11391 . . . . . . . . . . . 12 (𝜑 → (𝑁 / 𝑁) = 1)
201197, 200breqtrd 5065 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) / 𝑁) < 1)
20214, 14, 72, 72mulgt0d 10772 . . . . . . . . . . . 12 (𝜑 → 0 < (𝐸 · 𝐸))
203 ltmul2 11468 . . . . . . . . . . . 12 ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 < (𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
204158, 116, 156, 202, 203syl112anc 1371 . . . . . . . . . . 11 (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
205201, 204mpbid 235 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))
206176, 176mulcld 10638 . . . . . . . . . . 11 (𝜑 → (𝐸 · 𝐸) ∈ ℂ)
207206mulid1d 10635 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸))
208205, 207breqtrd 5065 . . . . . . . . 9 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸))
209159, 156, 155, 208ltsub2dd 11230 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
210114, 157, 160, 185, 209lttrd 10778 . . . . . . 7 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
211176, 198, 199divcld 11393 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
212175, 211, 180subdird 11074 . . . . . . . . . 10 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))))
213180mulid2d 10636 . . . . . . . . . . 11 (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1))
214213oveq1d 7145 . . . . . . . . . 10 (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
215212, 214eqtrd 2856 . . . . . . . . 9 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
216215oveq2d 7146 . . . . . . . 8 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))))
217211, 180mulcld 10638 . . . . . . . . 9 (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈ ℂ)
218176, 180, 217subdid 11073 . . . . . . . 8 (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))))
219176, 198, 180, 199div32d 11416 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁)))
220219oveq2d 7146 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
221180, 198, 199divcld 11393 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ)
222176, 176, 221mulassd 10641 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
223220, 222eqtr4d 2859 . . . . . . . . 9 (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))
224223oveq2d 7146 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
225216, 218, 2243eqtrd 2860 . . . . . . 7 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
226210, 225breqtrrd 5067 . . . . . 6 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
227226adantr 484 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
228175, 211subcld 10974 . . . . . . . . . 10 (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ)
229 fsumconst 15124 . . . . . . . . . 10 (((0...(𝐿 − 2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
230124, 228, 229syl2anc 587 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
231230adantr 484 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
232 0zd 11971 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℤ)
23331adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁))
234233, 106syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ)
235126a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℤ)
236234, 235zsubcld 12070 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ)
237 elnnuz 12260 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
238117, 237sylib 221 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘1))
239 elfzp12 12969 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
240238, 239syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
24131, 240mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
242241orcanai 1000 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁))
243 1p1e2 11740 . . . . . . . . . . . . . . . . . 18 (1 + 1) = 2
244243a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2)
245244oveq1d 7145 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁))
246242, 245eleqtrd 2914 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁))
247 elfzle1 12893 . . . . . . . . . . . . . . 15 (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿)
248246, 247syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿)
249108adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ)
250131a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℝ)
251249, 250subge0d 11207 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿))
252248, 251mpbird 260 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2))
253232, 236, 2523jca 1125 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
254 eluz2 12227 . . . . . . . . . . . 12 ((𝐿 − 2) ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
255253, 254sylibr 237 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (ℤ‘0))
256 hashfz 13772 . . . . . . . . . . 11 ((𝐿 − 2) ∈ (ℤ‘0) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
257255, 256syl 17 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
258 2cn 11690 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
259258a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
260139, 259subcld 10974 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ∈ ℂ)
261260subid1d 10963 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2))
262261oveq1d 7145 . . . . . . . . . . . 12 (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) + 1))
263139, 259, 175subadd23d 10996 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2)))
264258, 167negsubdi2i 10949 . . . . . . . . . . . . . . . 16 -(2 − 1) = (1 − 2)
265 2m1e1 11741 . . . . . . . . . . . . . . . . 17 (2 − 1) = 1
266265negeqi 10856 . . . . . . . . . . . . . . . 16 -(2 − 1) = -1
267264, 266eqtr3i 2846 . . . . . . . . . . . . . . 15 (1 − 2) = -1
268267a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 − 2) = -1)
269268oveq2d 7146 . . . . . . . . . . . . 13 (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1))
270139, 175negsubd 10980 . . . . . . . . . . . . 13 (𝜑 → (𝐿 + -1) = (𝐿 − 1))
271269, 270eqtrd 2856 . . . . . . . . . . . 12 (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1))
272262, 263, 2713eqtrd 2860 . . . . . . . . . . 11 (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
273272adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
274257, 273eqtrd 2856 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (𝐿 − 1))
275274oveq1d 7145 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁))))
276180, 228mulcomd 10639 . . . . . . . . 9 (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
277276adantr 484 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
278231, 275, 2773eqtrd 2860 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
279 fzfid 13324 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin)
280 fzn0 12904 . . . . . . . . 9 ((0...(𝐿 − 2)) ≠ ∅ ↔ (𝐿 − 2) ∈ (ℤ‘0))
281255, 280sylibr 237 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅)
282119ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ)
283 simpll 766 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑)
284150adantlr 714 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
285283, 284, 51syl2anc 587 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
28649adantr 484 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆𝑇)
287 elfzelz 12891 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ)
288287zred 12065 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ)
289288adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ)
290163a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈ ℝ)
291289, 290readdcld 10647 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ)
29214adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ)
293291, 292remulcld 10648 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ)
294108adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ)
295131a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈ ℝ)
296294, 295resubcld 11045 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
297296, 290readdcld 10647 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
298297, 292remulcld 10648 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
299 stoweidlem26.10 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑇⟶ℝ)
300299, 49jca 515 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆𝑇))
301300adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆𝑇))
302 ffvelrn 6822 . . . . . . . . . . . . . 14 ((𝐹:𝑇⟶ℝ ∧ 𝑆𝑇) → (𝐹𝑆) ∈ ℝ)
303301, 302syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐹𝑆) ∈ ℝ)
304 elfzle2 12894 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2))
305304adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2))
306289, 296, 290, 305leadd1dd 11231 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)))
30714, 72jca 515 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
308307adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
309 lemul1 11469 . . . . . . . . . . . . . . 15 (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 − 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
310291, 297, 308, 309syl3anc 1368 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
311306, 310mpbid 235 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))
312108, 132resubcld 11045 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 − 2) ∈ ℝ)
313312, 164readdcld 10647 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
314313, 14remulcld 10648 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
315299, 49ffvelrnd 6825 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑆) ∈ ℝ)
316120, 164resubcld 11045 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈ ℝ)
317316, 14remulcld 10648 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈ ℝ)
318 addid1 10797 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℂ → (1 + 0) = 1)
319318eqcomd 2827 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ ℂ → 1 = (1 + 0))
320167, 319mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 = (1 + 0))
321175subidd 10962 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 − 1) = 0)
322321eqcomd 2827 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 0 = (1 − 1))
323322oveq2d 7146 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + 0) = (1 + (1 − 1)))
324 addsubass 10873 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1) − 1) = (1 + (1 − 1)))
325324eqcomd 2827 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1 − 1)) = ((1 + 1) − 1))
326175, 175, 175, 325syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + (1 − 1)) = ((1 + 1) − 1))
327320, 323, 3263eqtrd 2860 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 = ((1 + 1) − 1))
328327oveq2d 7146 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) − 1)))
329243a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + 1) = 2)
330329oveq1d 7145 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1 + 1) − 1) = (2 − 1))
331330oveq2d 7146 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 − 1)))
332139, 259, 175subsubd 11002 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) + 1))
333328, 331, 3323eqtrd 2860 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1))
334333oveq1d 7145 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 / 3)))
335258, 60, 9divcli 11359 . . . . . . . . . . . . . . . . . . . . 21 (2 / 3) ∈ ℂ
336335a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 / 3) ∈ ℂ)
337260, 175, 336addsubassd 10994 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 / 3))))
338167, 60, 9divcli 11359 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 3) ∈ ℂ
339 df-3 11679 . . . . . . . . . . . . . . . . . . . . . . . 24 3 = (2 + 1)
340339oveq1i 7140 . . . . . . . . . . . . . . . . . . . . . . 23 (3 / 3) = ((2 + 1) / 3)
341258, 167, 60, 9divdiri 11374 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
342340, 61, 3413eqtr3ri 2853 . . . . . . . . . . . . . . . . . . . . . 22 ((2 / 3) + (1 / 3)) = 1
343167, 335, 338, 342subaddrii 10952 . . . . . . . . . . . . . . . . . . . . 21 (1 − (2 / 3)) = (1 / 3)
344343a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 − (2 / 3)) = (1 / 3))
345344oveq2d 7146 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 / 3)))
346334, 337, 3453eqtrd 2860 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 / 3)))
347131, 7, 9redivcli 11384 . . . . . . . . . . . . . . . . . . . 20 (2 / 3) ∈ ℝ
348347a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2 / 3) ∈ ℝ)
349 1lt2 11786 . . . . . . . . . . . . . . . . . . . 20 1 < 2
3507, 63pm3.2i 474 . . . . . . . . . . . . . . . . . . . . . 22 (3 ∈ ℝ ∧ 0 < 3)
3511, 131, 3503pm3.2i 1336 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
352 ltdiv1 11481 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (1 < 2 ↔ (1 / 3) < (2 / 3)))
353351, 352mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 < 2 ↔ (1 / 3) < (2 / 3)))
354349, 353mpbii 236 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1 / 3) < (2 / 3))
355164, 348, 120, 354ltsub2dd 11230 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 / 3)))
356346, 355eqbrtrrd 5063 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 / 3)))
357313, 316, 13, 356ltmul1dd 12464 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸))
35823simprd 499 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))
359 oveq1 7137 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 / 3)))
360359oveq1d 7145 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸))
361360breq2d 5051 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝐿 − 1) → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
362361rabbidv 3457 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝐿 − 1) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
363189simpld 498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 1 ≤ 𝐿)
364134, 116readdcld 10647 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 + 1) ∈ ℝ)
365134lep1d 11548 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ≤ (𝑁 + 1))
366108, 134, 364, 190, 365letrd 10774 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐿 ≤ (𝑁 + 1))
367129peano2zd 12068 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 + 1) ∈ ℤ)
368 elfz 12881 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → (𝐿 ∈ (1...(𝑁 + 1)) ↔ (1 ≤ 𝐿𝐿 ≤ (𝑁 + 1))))
369125, 186, 367, 368syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐿 ∈ (1...(𝑁 + 1)) ↔ (1 ≤ 𝐿𝐿 ≤ (𝑁 + 1))))
370363, 366, 369mpbir2and 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐿 ∈ (1...(𝑁 + 1)))
371139, 175npcand 10978 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐿 − 1) + 1) = 𝐿)
372 0p1e1 11737 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 + 1) = 1
373372a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (0 + 1) = 1)
374373oveq1d 7145 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
375370, 371, 3743eltr4d 2927 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
376 0zd 11971 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 0 ∈ ℤ)
377125, 186zsubcld 12070 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐿 − 1) ∈ ℤ)
378 fzaddel 12924 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐿 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
379376, 129, 377, 186, 378syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
380375, 379mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐿 − 1) ∈ (0...𝑁))
381 rabexg 5207 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
38233, 381syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
38325, 362, 380, 382fvmptd3 6764 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
384358, 383neleqtrd 2933 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
385 nfcv 2974 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸)
38641, 42, 385nfbr 5086 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)
38745breq1d 5049 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑆 → ((𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
38838, 39, 386, 387elrabf 3653 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
389384, 388sylnib 331 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
390 ianor 979 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
391389, 390sylib 221 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
392 olc 865 . . . . . . . . . . . . . . . . . . . . 21 (𝑆𝑇 → (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇))
393392anim1i 617 . . . . . . . . . . . . . . . . . . . 20 ((𝑆𝑇 ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
39449, 391, 393syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
395 orcom 867 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇))
396395anbi2i 625 . . . . . . . . . . . . . . . . . . 19 (((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
397394, 396sylib 221 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
398 pm4.43 1020 . . . . . . . . . . . . . . . . . 18 (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
399397, 398sylibr 237 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))
400317, 315ltnled 10764 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹𝑆) ↔ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
401399, 400mpbird 260 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹𝑆))
402314, 317, 315, 357, 401lttrd 10778 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹𝑆))
403314, 315, 402ltled 10765 . . . . . . . . . . . . . 14 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
404403adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
405293, 298, 303, 311, 404letrd 10774 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
406 nfcv 2974 . . . . . . . . . . . . . 14 𝑡((𝑖 + (1 / 3)) · 𝐸)
407406, 42, 41nfbr 5086 . . . . . . . . . . . . 13 𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)
40845breq2d 5051 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)))
40938, 39, 407, 408elrabf 3653 . . . . . . . . . . . 12 (𝑆 ∈ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ↔ (𝑆𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)))
410286, 405, 409sylanbrc 586 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
411 stoweidlem26.5 . . . . . . . . . . . 12 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
412 oveq1 7137 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
413412oveq1d 7145 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸))
414413breq1d 5049 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
415414rabbidv 3457 . . . . . . . . . . . 12 (𝑗 = 𝑖 → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
416 rabexg 5207 . . . . . . . . . . . . . 14 (𝑇 ∈ V → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
41733, 416syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
418417adantr 484 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
419411, 415, 150, 418fvmptd3 6764 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐵𝑖) = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
420410, 419eleqtrrd 2915 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵𝑖))
4211453ad2ant1 1130 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
422421, 146sylibr 237 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑁 ∈ (ℤ‘(𝐿 − 2)))
423422, 148syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
424 simp2 1134 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑖 ∈ (0...(𝐿 − 2)))
425423, 424sseldd 3944 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑖 ∈ (0...𝑁))
426 elex 3489 . . . . . . . . . . . . 13 (𝑆 ∈ (𝐵𝑖) → 𝑆 ∈ V)
4274263ad2ant3 1132 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑆 ∈ V)
428 nfcv 2974 . . . . . . . . . . . . . . . . . . 19 𝑡(0...𝑁)
429 nfrab1 3369 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
430428, 429nfmpt 5136 . . . . . . . . . . . . . . . . . 18 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
431411, 430nfcxfr 2972 . . . . . . . . . . . . . . . . 17 𝑡𝐵
432 nfcv 2974 . . . . . . . . . . . . . . . . 17 𝑡𝑖
433431, 432nffv 6653 . . . . . . . . . . . . . . . 16 𝑡(𝐵𝑖)
434433nfel2 2992 . . . . . . . . . . . . . . 15 𝑡 𝑆 ∈ (𝐵𝑖)
43588, 89, 434nf3an 1903 . . . . . . . . . . . . . 14 𝑡(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖))
436 nfv 1916 . . . . . . . . . . . . . 14 𝑡(1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)
437435, 436nfim 1898 . . . . . . . . . . . . 13 𝑡((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
438 eleq1 2899 . . . . . . . . . . . . . . 15 (𝑡 = 𝑆 → (𝑡 ∈ (𝐵𝑖) ↔ 𝑆 ∈ (𝐵𝑖)))
4394383anbi3d 1439 . . . . . . . . . . . . . 14 (𝑡 = 𝑆 → ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖))))
44093breq2d 5051 . . . . . . . . . . . . . 14 (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)))
441439, 440imbi12d 348 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))))
442 stoweidlem26.15 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
443437, 441, 442vtoclg1f 3543 . . . . . . . . . . . 12 (𝑆 ∈ V → ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)))
444427, 443mpcom 38 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
445425, 444syld3an2 1408 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
446420, 445mpd3an3 1459 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
447446adantlr 714 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
448279, 281, 282, 285, 447fsumlt 15134 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))
449278, 448eqbrtrrd 5063 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))
450121adantr 484 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
451152adantr 484 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ)
452307adantr 484 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
453 ltmul2 11468 . . . . . . 7 ((((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))))
454450, 451, 452, 453syl3anc 1368 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))))
455449, 454mpbid 235 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)))
456115, 123, 154, 227, 455lttrd 10778 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)))
457150, 52syldan 594 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
458457adantlr 714 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
459458recnd 10646 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
460279, 459fsumcl 15069 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
461460addid1d 10817 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
462 0red 10621 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℝ)
463 fzfid 13324 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin)
46414adantr 484 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ)
465 0red 10621 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ)
466120adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ)
467 elfzelz 12891 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ)
468467zred 12065 . . . . . . . . . . . . . 14 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ)
469468adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ)
470 1m1e0 11687 . . . . . . . . . . . . . . 15 (1 − 1) = 0
471116, 108, 116, 363lesub1dd 11233 . . . . . . . . . . . . . . 15 (𝜑 → (1 − 1) ≤ (𝐿 − 1))
472470, 471eqbrtrrid 5075 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝐿 − 1))
473472adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1))
474 simpr 488 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁))
475467adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ)
476377adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ)
477129adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ)
478 elfz 12881 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖𝑖𝑁)))
479475, 476, 477, 478syl3anc 1368 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖𝑖𝑁)))
480474, 479mpbid 235 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖𝑖𝑁))
481480simpld 498 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖)
482465, 466, 469, 473, 481letrd 10774 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖)
483 elfzle2 12894 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖𝑁)
484483adantl 485 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖𝑁)
485 0zd 11971 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ)
486 elfz 12881 . . . . . . . . . . . . 13 ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0...𝑁) ↔ (0 ≤ 𝑖𝑖𝑁)))
487475, 485, 477, 486syl3anc 1368 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ (0...𝑁) ↔ (0 ≤ 𝑖𝑖𝑁)))
488482, 484, 487mpbir2and 712 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁))
489488, 51syldan 594 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
490464, 489remulcld 10648 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
491490adantlr 714 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
492463, 491fsumrecl 15070 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
493279, 458fsumrecl 15070 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
494 fzfid 13324 . . . . . . . . 9 (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin)
495176adantr 484 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ)
496495mul01d 10816 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0)
497488, 100syldan 594 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
498307adantr 484 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
499 lemul2 11470 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ ((𝑋𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆))))
500465, 489, 498, 499syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆))))
501497, 500mpbid 235 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
502496, 501eqbrtrrd 5063 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
503494, 490, 502fsumge0 15129 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
504503adantr 484 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
505462, 492, 493, 504leadd2dd 11232 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
506461, 505eqbrtrrd 5063 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
507151recnd 10646 . . . . . . 7 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℂ)
508124, 176, 507fsummulc2 15118 . . . . . 6 (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
509508adantr 484 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
510 stoweidlem26.2 . . . . . . . . 9 𝑗𝜑
511 elfzelz 12891 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ)
512511adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ)
513512zred 12065 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ)
514312adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
515120adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ)
516 simpr 488 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2)))
517 0zd 11971 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈ ℤ)
518128adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ)
519 elfz 12881 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2))))
520512, 517, 518, 519syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2))))
521516, 520mpbid 235 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2)))
522521simprd 499 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2))
523116, 132, 108ltsub2d 11227 . . . . . . . . . . . . . . . 16 (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1)))
524349, 523mpbii 236 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 2) < (𝐿 − 1))
525524adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1))
526513, 514, 515, 522, 525lelttrd 10775 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1))
527513, 515ltnled 10764 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗))
528526, 527mpbid 235 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗)
529528intnanrd 493 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗𝑗𝑁))
530377adantr 484 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ)
531129adantr 484 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ)
532 elfz 12881 . . . . . . . . . . . 12 ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗𝑗𝑁)))
533512, 530, 531, 532syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗𝑗𝑁)))
534529, 533mtbird 328 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
535534ex 416 . . . . . . . . 9 (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)))
536510, 535ralrimi 3204 . . . . . . . 8 (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
537 disj 4372 . . . . . . . 8 (((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅ ↔ ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
538536, 537sylibr 237 . . . . . . 7 (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
539538adantr 484 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
540144adantr 484 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁)
541128, 376, 1293jca 1125 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
542541adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
543 elfz 12881 . . . . . . . . . 10 (((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
544542, 543syl 17 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
545252, 540, 544mpbir2and 712 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁))
546 fzsplit 12916 . . . . . . . 8 ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
547545, 546syl 17 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
548263, 269, 2703eqtrd 2860 . . . . . . . . . 10 (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1))
549548oveq1d 7145 . . . . . . . . 9 (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁))
550549uneq2d 4115 . . . . . . . 8 (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
551550adantr 484 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
552547, 551eqtrd 2856 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
553 fzfid 13324 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin)
554176adantr 484 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
55551recnd 10646 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℂ)
556554, 555mulcld 10638 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
557556adantlr 714 . . . . . 6 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
558539, 552, 553, 557fsumsplit 15076 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
559506, 509, 5583brtr4d 5071 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
560114, 153, 533jca 1125 . . . . . 6 (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ))
561560adantr 484 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ))
562 ltletr 10709 . . . . 5 ((((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
563561, 562syl 17 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
564456, 559, 563mp2and 698 . . 3 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
565105, 564pm2.61dan 812 . 2 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
566 sumex 15023 . . 3 Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ V
56793oveq2d 7146 . . . . 5 (𝑡 = 𝑆 → (𝐸 · ((𝑋𝑖)‘𝑡)) = (𝐸 · ((𝑋𝑖)‘𝑆)))
568567sumeq2sdv 15040 . . . 4 (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
569 eqid 2821 . . . 4 (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡))) = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))
570568, 569fvmptg 6739 . . 3 ((𝑆𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ V) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
57149, 566, 570sylancl 589 . 2 (𝜑 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
572565, 571breqtrrd 5067 1 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wnf 1785  wcel 2115  wnfc 2958  wne 3007  wral 3126  {crab 3130  Vcvv 3471  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4266   class class class wbr 5039  cmpt 5119  wf 6324  cfv 6328  (class class class)co 7130  Fincfn 8484  cc 10512  cr 10513  0cc0 10514  1c1 10515   + caddc 10517   · cmul 10519   < clt 10652  cle 10653  cmin 10847  -cneg 10848   / cdiv 11274  cn 11615  2c2 11670  3c3 11671  4c4 11672  0cn0 11875  cz 11959  cuz 12221  +crp 12367  ...cfz 12875  chash 13674  Σcsu 15021
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-inf2 9080  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591  ax-pre-sup 10592
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-int 4850  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-om 7556  df-1st 7664  df-2nd 7665  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-1o 8077  df-oadd 8081  df-er 8264  df-en 8485  df-dom 8486  df-sdom 8487  df-fin 8488  df-sup 8882  df-oi 8950  df-card 9344  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-div 11275  df-nn 11616  df-2 11678  df-3 11679  df-4 11680  df-n0 11876  df-z 11960  df-uz 12222  df-rp 12368  df-ico 12722  df-fz 12876  df-fzo 13017  df-seq 13353  df-exp 13414  df-hash 13675  df-cj 14437  df-re 14438  df-im 14439  df-sqrt 14573  df-abs 14574  df-clim 14824  df-sum 15022
This theorem is referenced by:  stoweidlem34  42469
  Copyright terms: Public domain W3C validator