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 40561
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 10077 . . . . . . . 8 1 ∈ ℝ
2 eleq1 2718 . . . . . . . 8 (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
31, 2mpbiri 248 . . . . . . 7 (𝐿 = 1 → 𝐿 ∈ ℝ)
43adantl 481 . . . . . 6 ((𝜑𝐿 = 1) → 𝐿 ∈ ℝ)
5 4re 11135 . . . . . . . 8 4 ∈ ℝ
65a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 4 ∈ ℝ)
7 3re 11132 . . . . . . . 8 3 ∈ ℝ
87a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 3 ∈ ℝ)
9 3ne0 11153 . . . . . . . 8 3 ≠ 0
109a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 3 ≠ 0)
116, 8, 10redivcld 10891 . . . . . 6 ((𝜑𝐿 = 1) → (4 / 3) ∈ ℝ)
124, 11resubcld 10496 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
13 stoweidlem26.11 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
1413rpred 11910 . . . . . 6 (𝜑𝐸 ∈ ℝ)
1514adantr 480 . . . . 5 ((𝜑𝐿 = 1) → 𝐸 ∈ ℝ)
1612, 15remulcld 10108 . . . 4 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
17 0red 10079 . . . 4 ((𝜑𝐿 = 1) → 0 ∈ ℝ)
18 fzfid 12812 . . . . . 6 (𝜑 → (0...𝑁) ∈ Fin)
1914adantr 480 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
20 stoweidlem26.13 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
21 stoweidlem26.9 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))))
22 eldif 3617 . . . . . . . . . . . . . 14 (𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
2321, 22sylib 208 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∈ (𝐷𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
2423simpld 474 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (𝐷𝐿))
25 fz1ssfz0 12474 . . . . . . . . . . . . . 14 (1...𝑁) ⊆ (0...𝑁)
26 stoweidlem26.8 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ (1...𝑁))
2725, 26sseldi 3634 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (0...𝑁))
28 stoweidlem26.7 . . . . . . . . . . . . . 14 (𝜑𝑇 ∈ V)
29 rabexg 4844 . . . . . . . . . . . . . 14 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
3028, 29syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
31 oveq1 6697 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3)))
3231oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸))
3332breq2d 4697 . . . . . . . . . . . . . . 15 (𝑗 = 𝐿 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
3433rabbidv 3220 . . . . . . . . . . . . . 14 (𝑗 = 𝐿 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
35 stoweidlem26.4 . . . . . . . . . . . . . 14 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
3634, 35fvmptg 6319 . . . . . . . . . . . . 13 ((𝐿 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷𝐿) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
3727, 30, 36syl2anc 694 . . . . . . . . . . . 12 (𝜑 → (𝐷𝐿) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
3824, 37eleqtrd 2732 . . . . . . . . . . 11 (𝜑𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
39 nfcv 2793 . . . . . . . . . . . 12 𝑡𝑆
40 nfcv 2793 . . . . . . . . . . . 12 𝑡𝑇
41 stoweidlem26.1 . . . . . . . . . . . . . 14 𝑡𝐹
4241, 39nffv 6236 . . . . . . . . . . . . 13 𝑡(𝐹𝑆)
43 nfcv 2793 . . . . . . . . . . . . 13 𝑡
44 nfcv 2793 . . . . . . . . . . . . 13 𝑡((𝐿 − (1 / 3)) · 𝐸)
4542, 43, 44nfbr 4732 . . . . . . . . . . . 12 𝑡(𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)
46 fveq2 6229 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (𝐹𝑡) = (𝐹𝑆))
4746breq1d 4695 . . . . . . . . . . . 12 (𝑡 = 𝑆 → ((𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4839, 40, 45, 47elrabf 3392 . . . . . . . . . . 11 (𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆𝑇 ∧ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4938, 48sylib 208 . . . . . . . . . 10 (𝜑 → (𝑆𝑇 ∧ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
5049simpld 474 . . . . . . . . 9 (𝜑𝑆𝑇)
5150adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑆𝑇)
5220, 51ffvelrnd 6400 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
5319, 52remulcld 10108 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
5418, 53fsumrecl 14509 . . . . 5 (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
5554adantr 480 . . . 4 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
565, 7, 9redivcli 10830 . . . . . . 7 (4 / 3) ∈ ℝ
5756a1i 11 . . . . . 6 ((𝜑𝐿 = 1) → (4 / 3) ∈ ℝ)
584, 57resubcld 10496 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
594recnd 10106 . . . . . . . 8 ((𝜑𝐿 = 1) → 𝐿 ∈ ℂ)
6059subid1d 10419 . . . . . . 7 ((𝜑𝐿 = 1) → (𝐿 − 0) = 𝐿)
61 3cn 11133 . . . . . . . . . 10 3 ∈ ℂ
6261, 9dividi 10796 . . . . . . . . 9 (3 / 3) = 1
63 3lt4 11235 . . . . . . . . . 10 3 < 4
64 3pos 11152 . . . . . . . . . . 11 0 < 3
657, 5, 7, 64ltdiv1ii 10991 . . . . . . . . . 10 (3 < 4 ↔ (3 / 3) < (4 / 3))
6663, 65mpbi 220 . . . . . . . . 9 (3 / 3) < (4 / 3)
6762, 66eqbrtrri 4708 . . . . . . . 8 1 < (4 / 3)
68 breq1 4688 . . . . . . . . 9 (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
6968adantl 481 . . . . . . . 8 ((𝜑𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
7067, 69mpbiri 248 . . . . . . 7 ((𝜑𝐿 = 1) → 𝐿 < (4 / 3))
7160, 70eqbrtrd 4707 . . . . . 6 ((𝜑𝐿 = 1) → (𝐿 − 0) < (4 / 3))
724, 17, 57, 71ltsub23d 10670 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) < 0)
7313rpgt0d 11913 . . . . . 6 (𝜑 → 0 < 𝐸)
7473adantr 480 . . . . 5 ((𝜑𝐿 = 1) → 0 < 𝐸)
75 mulltgt0 39495 . . . . 5 ((((𝐿 − (4 / 3)) ∈ ℝ ∧ (𝐿 − (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
7658, 72, 15, 74, 75syl22anc 1367 . . . 4 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
77 0cn 10070 . . . . . . . 8 0 ∈ ℂ
78 fsumconst 14566 . . . . . . . 8 (((0...𝑁) ∈ Fin ∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((#‘(0...𝑁)) · 0))
7918, 77, 78sylancl 695 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((#‘(0...𝑁)) · 0))
80 hashcl 13185 . . . . . . . . 9 ((0...𝑁) ∈ Fin → (#‘(0...𝑁)) ∈ ℕ0)
81 nn0cn 11340 . . . . . . . . 9 ((#‘(0...𝑁)) ∈ ℕ0 → (#‘(0...𝑁)) ∈ ℂ)
8218, 80, 813syl 18 . . . . . . . 8 (𝜑 → (#‘(0...𝑁)) ∈ ℂ)
8382mul01d 10273 . . . . . . 7 (𝜑 → ((#‘(0...𝑁)) · 0) = 0)
8479, 83eqtrd 2685 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0)
8584adantr 480 . . . . 5 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0)
86 0red 10079 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ)
8713rpge0d 11914 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐸)
8887adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸)
89 stoweidlem26.3 . . . . . . . . . . . 12 𝑡𝜑
90 nfv 1883 . . . . . . . . . . . 12 𝑡 𝑖 ∈ (0...𝑁)
9189, 90nfan 1868 . . . . . . . . . . 11 𝑡(𝜑𝑖 ∈ (0...𝑁))
92 nfv 1883 . . . . . . . . . . 11 𝑡0 ≤ ((𝑋𝑖)‘𝑆)
9391, 92nfim 1865 . . . . . . . . . 10 𝑡((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
94 fveq2 6229 . . . . . . . . . . . 12 (𝑡 = 𝑆 → ((𝑋𝑖)‘𝑡) = ((𝑋𝑖)‘𝑆))
9594breq2d 4697 . . . . . . . . . . 11 (𝑡 = 𝑆 → (0 ≤ ((𝑋𝑖)‘𝑡) ↔ 0 ≤ ((𝑋𝑖)‘𝑆)))
9695imbi2d 329 . . . . . . . . . 10 (𝑡 = 𝑆 → (((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))))
97 stoweidlem26.14 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
98973expia 1286 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑡𝑇 → 0 ≤ ((𝑋𝑖)‘𝑡)))
9998com12 32 . . . . . . . . . 10 (𝑡𝑇 → ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑡)))
10039, 93, 96, 99vtoclgaf 3302 . . . . . . . . 9 (𝑆𝑇 → ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆)))
10151, 100mpcom 38 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
10219, 52, 88, 101mulge0d 10642 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
10318, 86, 53, 102fsumle 14575 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
104103adantr 480 . . . . 5 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
10585, 104eqbrtrrd 4709 . . . 4 ((𝜑𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
10616, 17, 55, 76, 105ltletrd 10235 . . 3 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
107 elfzelz 12380 . . . . . . . . 9 (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ)
108 zre 11419 . . . . . . . . 9 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
10926, 107, 1083syl 18 . . . . . . . 8 (𝜑𝐿 ∈ ℝ)
1105a1i 11 . . . . . . . . 9 (𝜑 → 4 ∈ ℝ)
1117a1i 11 . . . . . . . . 9 (𝜑 → 3 ∈ ℝ)
1129a1i 11 . . . . . . . . 9 (𝜑 → 3 ≠ 0)
113110, 111, 112redivcld 10891 . . . . . . . 8 (𝜑 → (4 / 3) ∈ ℝ)
114109, 113resubcld 10496 . . . . . . 7 (𝜑 → (𝐿 − (4 / 3)) ∈ ℝ)
115114, 14remulcld 10108 . . . . . 6 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
116115adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
1171a1i 11 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ)
118 stoweidlem26.6 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
11914, 118nndivred 11107 . . . . . . . . 9 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
120117, 119resubcld 10496 . . . . . . . 8 (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ)
121109, 117resubcld 10496 . . . . . . . 8 (𝜑 → (𝐿 − 1) ∈ ℝ)
122120, 121remulcld 10108 . . . . . . 7 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
12314, 122remulcld 10108 . . . . . 6 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
124123adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
125 fzfid 12812 . . . . . . . 8 (𝜑 → (0...(𝐿 − 2)) ∈ Fin)
12626, 107syl 17 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ ℤ)
127 2z 11447 . . . . . . . . . . . . . . 15 2 ∈ ℤ
128127a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℤ)
129126, 128zsubcld 11525 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 2) ∈ ℤ)
130118nnzd 11519 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℤ)
131126zred 11520 . . . . . . . . . . . . . . 15 (𝜑𝐿 ∈ ℝ)
132 2re 11128 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
133132a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℝ)
134131, 133resubcld 10496 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ∈ ℝ)
135118nnred 11073 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
136 0le2 11149 . . . . . . . . . . . . . . . 16 0 ≤ 2
137 0red 10079 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
138137, 133, 131lesub2d 10673 . . . . . . . . . . . . . . . 16 (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0)))
139136, 138mpbii 223 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0))
140126zcnd 11521 . . . . . . . . . . . . . . . 16 (𝜑𝐿 ∈ ℂ)
141140subid1d 10419 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 0) = 𝐿)
142139, 141breqtrd 4711 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ≤ 𝐿)
143 elfzle2 12383 . . . . . . . . . . . . . . 15 (𝐿 ∈ (1...𝑁) → 𝐿𝑁)
14426, 143syl 17 . . . . . . . . . . . . . 14 (𝜑𝐿𝑁)
145134, 131, 135, 142, 144letrd 10232 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 2) ≤ 𝑁)
146129, 130, 1453jca 1261 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
147 eluz2 11731 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
148146, 147sylibr 224 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝐿 − 2)))
149 fzss2 12419 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
150148, 149syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁))
151150sselda 3636 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
152151, 52syldan 486 . . . . . . . 8 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
153125, 152fsumrecl 14509 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ)
15414, 153remulcld 10108 . . . . . 6 (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ)
155154adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ)
15614, 121remulcld 10108 . . . . . . . . 9 (𝜑 → (𝐸 · (𝐿 − 1)) ∈ ℝ)
15714, 14remulcld 10108 . . . . . . . . 9 (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
158156, 157resubcld 10496 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ)
159121, 118nndivred 11107 . . . . . . . . . 10 (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ)
160157, 159remulcld 10108 . . . . . . . . 9 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ)
161156, 160resubcld 10496 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ)
162121, 14resubcld 10496 . . . . . . . . . 10 (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ)
163117, 14readdcld 10107 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) ∈ ℝ)
1641, 7, 9redivcli 10830 . . . . . . . . . . . . . . 15 (1 / 3) ∈ ℝ
165164a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 / 3) ∈ ℝ)
166 stoweidlem26.12 . . . . . . . . . . . . . 14 (𝜑𝐸 < (1 / 3))
16714, 165, 117, 166ltadd2dd 10234 . . . . . . . . . . . . 13 (𝜑 → (1 + 𝐸) < (1 + (1 / 3)))
168 ax-1cn 10032 . . . . . . . . . . . . . . 15 1 ∈ ℂ
16961, 168, 61, 9divdiri 10820 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
170 3p1e4 11191 . . . . . . . . . . . . . . 15 (3 + 1) = 4
171170oveq1i 6700 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = (4 / 3)
17262oveq1i 6700 . . . . . . . . . . . . . 14 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
173169, 171, 1723eqtr3ri 2682 . . . . . . . . . . . . 13 (1 + (1 / 3)) = (4 / 3)
174167, 173syl6breq 4726 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) < (4 / 3))
175163, 113, 109, 174ltsub2dd 10678 . . . . . . . . . . 11 (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸)))
176168a1i 11 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
17713rpcnd 11912 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℂ)
178140, 176, 177subsub4d 10461 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸)))
179175, 178breqtrrd 4713 . . . . . . . . . 10 (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸))
180114, 162, 13, 179ltmul1dd 11965 . . . . . . . . 9 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸))
181140, 176subcld 10430 . . . . . . . . . . . 12 (𝜑 → (𝐿 − 1) ∈ ℂ)
182181, 177subcld 10430 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ)
183177, 182mulcomd 10099 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸))
184177, 181, 177subdid 10524 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
185183, 184eqtr3d 2687 . . . . . . . . 9 (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
186180, 185breqtrd 4711 . . . . . . . 8 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
187 1zzd 11446 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
188 elfz 12370 . . . . . . . . . . . . . . . . 17 ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿𝐿𝑁)))
189126, 187, 130, 188syl3anc 1366 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿𝐿𝑁)))
19026, 189mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → (1 ≤ 𝐿𝐿𝑁))
191190simprd 478 . . . . . . . . . . . . . 14 (𝜑𝐿𝑁)
192 zlem1lt 11467 . . . . . . . . . . . . . . 15 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿𝑁 ↔ (𝐿 − 1) < 𝑁))
193126, 130, 192syl2anc 694 . . . . . . . . . . . . . 14 (𝜑 → (𝐿𝑁 ↔ (𝐿 − 1) < 𝑁))
194191, 193mpbid 222 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 1) < 𝑁)
195118nngt0d 11102 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑁)
196 ltdiv1 10925 . . . . . . . . . . . . . 14 (((𝐿 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
197121, 135, 135, 195, 196syl112anc 1370 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
198194, 197mpbid 222 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))
199118nncnd 11074 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
200118nnne0d 11103 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
201199, 200dividd 10837 . . . . . . . . . . . 12 (𝜑 → (𝑁 / 𝑁) = 1)
202198, 201breqtrd 4711 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) / 𝑁) < 1)
20314, 14, 73, 73mulgt0d 10230 . . . . . . . . . . . 12 (𝜑 → 0 < (𝐸 · 𝐸))
204 ltmul2 10912 . . . . . . . . . . . 12 ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 < (𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
205159, 117, 157, 203, 204syl112anc 1370 . . . . . . . . . . 11 (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
206202, 205mpbid 222 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))
207177, 177mulcld 10098 . . . . . . . . . . 11 (𝜑 → (𝐸 · 𝐸) ∈ ℂ)
208207mulid1d 10095 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸))
209206, 208breqtrd 4711 . . . . . . . . 9 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸))
210160, 157, 156, 209ltsub2dd 10678 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
211115, 158, 161, 186, 210lttrd 10236 . . . . . . 7 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
212177, 199, 200divcld 10839 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
213176, 212, 181subdird 10525 . . . . . . . . . 10 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))))
214181mulid2d 10096 . . . . . . . . . . 11 (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1))
215214oveq1d 6705 . . . . . . . . . 10 (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
216213, 215eqtrd 2685 . . . . . . . . 9 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
217216oveq2d 6706 . . . . . . . 8 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))))
218212, 181mulcld 10098 . . . . . . . . 9 (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈ ℂ)
219177, 181, 218subdid 10524 . . . . . . . 8 (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))))
220177, 199, 181, 200div32d 10862 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁)))
221220oveq2d 6706 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
222181, 199, 200divcld 10839 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ)
223177, 177, 222mulassd 10101 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
224221, 223eqtr4d 2688 . . . . . . . . 9 (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))
225224oveq2d 6706 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
226217, 219, 2253eqtrd 2689 . . . . . . 7 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
227211, 226breqtrrd 4713 . . . . . 6 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
228227adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
229176, 212subcld 10430 . . . . . . . . . 10 (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ)
230 fsumconst 14566 . . . . . . . . . 10 (((0...(𝐿 − 2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
231125, 229, 230syl2anc 694 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
232231adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
233 0zd 11427 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℤ)
23426adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁))
235234, 107syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ)
236127a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℤ)
237235, 236zsubcld 11525 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ)
238 elnnuz 11762 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
239118, 238sylib 208 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘1))
240 elfzp12 12457 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
241239, 240syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
24226, 241mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
243242orcanai 972 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁))
244 1p1e2 11172 . . . . . . . . . . . . . . . . . 18 (1 + 1) = 2
245244a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2)
246245oveq1d 6705 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁))
247243, 246eleqtrd 2732 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁))
248 elfzle1 12382 . . . . . . . . . . . . . . 15 (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿)
249247, 248syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿)
250109adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ)
251132a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℝ)
252250, 251subge0d 10655 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿))
253249, 252mpbird 247 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2))
254233, 237, 2533jca 1261 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
255 eluz2 11731 . . . . . . . . . . . 12 ((𝐿 − 2) ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
256254, 255sylibr 224 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (ℤ‘0))
257 hashfz 13252 . . . . . . . . . . 11 ((𝐿 − 2) ∈ (ℤ‘0) → (#‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
258256, 257syl 17 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → (#‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
259 2cn 11129 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
260259a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
261140, 260subcld 10430 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ∈ ℂ)
262261subid1d 10419 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2))
263262oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) + 1))
264140, 260, 176subadd23d 10452 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2)))
265259, 168negsubdi2i 10405 . . . . . . . . . . . . . . . 16 -(2 − 1) = (1 − 2)
266 2m1e1 11173 . . . . . . . . . . . . . . . . 17 (2 − 1) = 1
267266negeqi 10312 . . . . . . . . . . . . . . . 16 -(2 − 1) = -1
268265, 267eqtr3i 2675 . . . . . . . . . . . . . . 15 (1 − 2) = -1
269268a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 − 2) = -1)
270269oveq2d 6706 . . . . . . . . . . . . 13 (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1))
271140, 176negsubd 10436 . . . . . . . . . . . . 13 (𝜑 → (𝐿 + -1) = (𝐿 − 1))
272270, 271eqtrd 2685 . . . . . . . . . . . 12 (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1))
273263, 264, 2723eqtrd 2689 . . . . . . . . . . 11 (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
274273adantr 480 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
275258, 274eqtrd 2685 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → (#‘(0...(𝐿 − 2))) = (𝐿 − 1))
276275oveq1d 6705 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁))))
277181, 229mulcomd 10099 . . . . . . . . 9 (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
278277adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
279232, 276, 2783eqtrd 2689 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
280 fzfid 12812 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin)
281 fzn0 12393 . . . . . . . . 9 ((0...(𝐿 − 2)) ≠ ∅ ↔ (𝐿 − 2) ∈ (ℤ‘0))
282256, 281sylibr 224 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅)
283120ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ)
284 simpll 805 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑)
285151adantlr 751 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
286284, 285, 52syl2anc 694 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
28750adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆𝑇)
288 elfzelz 12380 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ)
289288zred 11520 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ)
290289adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ)
291164a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈ ℝ)
292290, 291readdcld 10107 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ)
29314adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ)
294292, 293remulcld 10108 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ)
295109adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ)
296132a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈ ℝ)
297295, 296resubcld 10496 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
298297, 291readdcld 10107 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
299298, 293remulcld 10108 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
300 stoweidlem26.10 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑇⟶ℝ)
301300, 50jca 553 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆𝑇))
302301adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆𝑇))
303 ffvelrn 6397 . . . . . . . . . . . . . 14 ((𝐹:𝑇⟶ℝ ∧ 𝑆𝑇) → (𝐹𝑆) ∈ ℝ)
304302, 303syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐹𝑆) ∈ ℝ)
305 elfzle2 12383 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2))
306305adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2))
307290, 297, 291, 306leadd1dd 10679 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)))
30814, 73jca 553 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
309308adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
310 lemul1 10913 . . . . . . . . . . . . . . 15 (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 − 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
311292, 298, 309, 310syl3anc 1366 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
312307, 311mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))
313109, 133resubcld 10496 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 − 2) ∈ ℝ)
314313, 165readdcld 10107 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
315314, 14remulcld 10108 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
316300, 50ffvelrnd 6400 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑆) ∈ ℝ)
317121, 165resubcld 10496 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈ ℝ)
318317, 14remulcld 10108 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈ ℝ)
319 addid1 10254 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℂ → (1 + 0) = 1)
320319eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ ℂ → 1 = (1 + 0))
321168, 320mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 = (1 + 0))
322176subidd 10418 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 − 1) = 0)
323322eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 0 = (1 − 1))
324323oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + 0) = (1 + (1 − 1)))
325 addsubass 10329 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1) − 1) = (1 + (1 − 1)))
326325eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1 − 1)) = ((1 + 1) − 1))
327176, 176, 176, 326syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + (1 − 1)) = ((1 + 1) − 1))
328321, 324, 3273eqtrd 2689 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 = ((1 + 1) − 1))
329328oveq2d 6706 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) − 1)))
330244a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + 1) = 2)
331330oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1 + 1) − 1) = (2 − 1))
332331oveq2d 6706 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 − 1)))
333140, 260, 176subsubd 10458 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) + 1))
334329, 332, 3333eqtrd 2689 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1))
335334oveq1d 6705 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 / 3)))
336259, 61, 9divcli 10805 . . . . . . . . . . . . . . . . . . . . 21 (2 / 3) ∈ ℂ
337336a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 / 3) ∈ ℂ)
338261, 176, 337addsubassd 10450 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 / 3))))
339168, 61, 9divcli 10805 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 3) ∈ ℂ
340 df-3 11118 . . . . . . . . . . . . . . . . . . . . . . . 24 3 = (2 + 1)
341340oveq1i 6700 . . . . . . . . . . . . . . . . . . . . . . 23 (3 / 3) = ((2 + 1) / 3)
342259, 168, 61, 9divdiri 10820 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
343341, 62, 3423eqtr3ri 2682 . . . . . . . . . . . . . . . . . . . . . 22 ((2 / 3) + (1 / 3)) = 1
344168, 336, 339, 343subaddrii 10408 . . . . . . . . . . . . . . . . . . . . 21 (1 − (2 / 3)) = (1 / 3)
345344a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 − (2 / 3)) = (1 / 3))
346345oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 / 3)))
347335, 338, 3463eqtrd 2689 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 / 3)))
348132, 7, 9redivcli 10830 . . . . . . . . . . . . . . . . . . . 20 (2 / 3) ∈ ℝ
349348a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2 / 3) ∈ ℝ)
350 1lt2 11232 . . . . . . . . . . . . . . . . . . . 20 1 < 2
3517, 64pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . 22 (3 ∈ ℝ ∧ 0 < 3)
3521, 132, 3513pm3.2i 1259 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
353 ltdiv1 10925 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (1 < 2 ↔ (1 / 3) < (2 / 3)))
354352, 353mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 < 2 ↔ (1 / 3) < (2 / 3)))
355350, 354mpbii 223 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1 / 3) < (2 / 3))
356165, 349, 121, 355ltsub2dd 10678 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 / 3)))
357347, 356eqbrtrrd 4709 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 / 3)))
358314, 317, 13, 357ltmul1dd 11965 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸))
35923simprd 478 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))
360190simpld 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 1 ≤ 𝐿)
361135, 117readdcld 10107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 + 1) ∈ ℝ)
362135lep1d 10993 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ≤ (𝑁 + 1))
363109, 135, 361, 191, 362letrd 10232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐿 ≤ (𝑁 + 1))
364130peano2zd 11523 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 + 1) ∈ ℤ)
365 elfz 12370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → (𝐿 ∈ (1...(𝑁 + 1)) ↔ (1 ≤ 𝐿𝐿 ≤ (𝑁 + 1))))
366126, 187, 364, 365syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐿 ∈ (1...(𝑁 + 1)) ↔ (1 ≤ 𝐿𝐿 ≤ (𝑁 + 1))))
367360, 363, 366mpbir2and 977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐿 ∈ (1...(𝑁 + 1)))
368140, 176npcand 10434 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐿 − 1) + 1) = 𝐿)
369 0p1e1 11170 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 + 1) = 1
370369a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (0 + 1) = 1)
371370oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
372367, 368, 3713eltr4d 2745 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
373 0zd 11427 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 0 ∈ ℤ)
374126, 187zsubcld 11525 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐿 − 1) ∈ ℤ)
375 fzaddel 12413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐿 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
376373, 130, 374, 187, 375syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
377372, 376mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐿 − 1) ∈ (0...𝑁))
378 rabexg 4844 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
37928, 378syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
380 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 / 3)))
381380oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸))
382381breq2d 4697 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = (𝐿 − 1) → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
383382rabbidv 3220 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝐿 − 1) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
384383, 35fvmptg 6319 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐿 − 1) ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘(𝐿 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
385377, 379, 384syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
386359, 385neleqtrd 2751 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
387 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸)
38842, 43, 387nfbr 4732 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)
38946breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑆 → ((𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
39039, 40, 388, 389elrabf 3392 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
391386, 390sylnib 317 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
392 ianor 508 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
393391, 392sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
394 olc 398 . . . . . . . . . . . . . . . . . . . . 21 (𝑆𝑇 → (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇))
395394anim1i 591 . . . . . . . . . . . . . . . . . . . 20 ((𝑆𝑇 ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
39650, 393, 395syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
397 orcom 401 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇))
398397anbi2i 730 . . . . . . . . . . . . . . . . . . 19 (((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
399396, 398sylib 208 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
400 pm4.43 988 . . . . . . . . . . . . . . . . . 18 (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
401399, 400sylibr 224 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))
402318, 316ltnled 10222 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹𝑆) ↔ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
403401, 402mpbird 247 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹𝑆))
404315, 318, 316, 358, 403lttrd 10236 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹𝑆))
405315, 316, 404ltled 10223 . . . . . . . . . . . . . 14 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
406405adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
407294, 299, 304, 312, 406letrd 10232 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
408 nfcv 2793 . . . . . . . . . . . . . 14 𝑡((𝑖 + (1 / 3)) · 𝐸)
409408, 43, 42nfbr 4732 . . . . . . . . . . . . 13 𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)
41046breq2d 4697 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)))
41139, 40, 409, 410elrabf 3392 . . . . . . . . . . . 12 (𝑆 ∈ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ↔ (𝑆𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)))
412287, 407, 411sylanbrc 699 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
413 rabexg 4844 . . . . . . . . . . . . . 14 (𝑇 ∈ V → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
41428, 413syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
415414adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
416 oveq1 6697 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
417416oveq1d 6705 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸))
418417breq1d 4695 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
419418rabbidv 3220 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
420 stoweidlem26.5 . . . . . . . . . . . . 13 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
421419, 420fvmptg 6319 . . . . . . . . . . . 12 ((𝑖 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V) → (𝐵𝑖) = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
422151, 415, 421syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐵𝑖) = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
423412, 422eleqtrrd 2733 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵𝑖))
4241463ad2ant1 1102 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
425424, 147sylibr 224 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑁 ∈ (ℤ‘(𝐿 − 2)))
426425, 149syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
427 simp2 1082 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑖 ∈ (0...(𝐿 − 2)))
428426, 427sseldd 3637 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑖 ∈ (0...𝑁))
429 elex 3243 . . . . . . . . . . . . 13 (𝑆 ∈ (𝐵𝑖) → 𝑆 ∈ V)
4304293ad2ant3 1104 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑆 ∈ V)
431 nfcv 2793 . . . . . . . . . . . . . . . . . . 19 𝑡(0...𝑁)
432 nfrab1 3152 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
433431, 432nfmpt 4779 . . . . . . . . . . . . . . . . . 18 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
434420, 433nfcxfr 2791 . . . . . . . . . . . . . . . . 17 𝑡𝐵
435 nfcv 2793 . . . . . . . . . . . . . . . . 17 𝑡𝑖
436434, 435nffv 6236 . . . . . . . . . . . . . . . 16 𝑡(𝐵𝑖)
437436nfel2 2810 . . . . . . . . . . . . . . 15 𝑡 𝑆 ∈ (𝐵𝑖)
43889, 90, 437nf3an 1871 . . . . . . . . . . . . . 14 𝑡(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖))
439 nfv 1883 . . . . . . . . . . . . . 14 𝑡(1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)
440438, 439nfim 1865 . . . . . . . . . . . . 13 𝑡((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
441 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑡 = 𝑆 → (𝑡 ∈ (𝐵𝑖) ↔ 𝑆 ∈ (𝐵𝑖)))
4424413anbi3d 1445 . . . . . . . . . . . . . 14 (𝑡 = 𝑆 → ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖))))
44394breq2d 4697 . . . . . . . . . . . . . 14 (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)))
444442, 443imbi12d 333 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))))
445 stoweidlem26.15 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
446440, 444, 445vtoclg1f 3296 . . . . . . . . . . . 12 (𝑆 ∈ V → ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)))
447430, 446mpcom 38 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
448428, 447syld3an2 1413 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
449423, 448mpd3an3 1465 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
450449adantlr 751 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
451280, 282, 283, 286, 450fsumlt 14576 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))
452279, 451eqbrtrrd 4709 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))
453122adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
454153adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ)
455308adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
456 ltmul2 10912 . . . . . . 7 ((((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))))
457453, 454, 455, 456syl3anc 1366 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))))
458452, 457mpbid 222 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)))
459116, 124, 155, 228, 458lttrd 10236 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)))
460151, 53syldan 486 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
461460adantlr 751 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
462461recnd 10106 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
463280, 462fsumcl 14508 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
464463addid1d 10274 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
465 0red 10079 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℝ)
466 fzfid 12812 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin)
46714adantr 480 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ)
468 0red 10079 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ)
469121adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ)
470 elfzelz 12380 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ)
471470zred 11520 . . . . . . . . . . . . . 14 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ)
472471adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ)
473 1m1e0 11127 . . . . . . . . . . . . . . 15 (1 − 1) = 0
474117, 109, 117, 360lesub1dd 10681 . . . . . . . . . . . . . . 15 (𝜑 → (1 − 1) ≤ (𝐿 − 1))
475473, 474syl5eqbrr 4721 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝐿 − 1))
476475adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1))
477 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁))
478470adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ)
479374adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ)
480130adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ)
481 elfz 12370 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖𝑖𝑁)))
482478, 479, 480, 481syl3anc 1366 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖𝑖𝑁)))
483477, 482mpbid 222 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖𝑖𝑁))
484483simpld 474 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖)
485468, 469, 472, 476, 484letrd 10232 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖)
486 elfzle2 12383 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖𝑁)
487486adantl 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖𝑁)
488 0zd 11427 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ)
489 elfz 12370 . . . . . . . . . . . . 13 ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0...𝑁) ↔ (0 ≤ 𝑖𝑖𝑁)))
490478, 488, 480, 489syl3anc 1366 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ (0...𝑁) ↔ (0 ≤ 𝑖𝑖𝑁)))
491485, 487, 490mpbir2and 977 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁))
492491, 52syldan 486 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
493467, 492remulcld 10108 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
494493adantlr 751 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
495466, 494fsumrecl 14509 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
496280, 461fsumrecl 14509 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
497 fzfid 12812 . . . . . . . . 9 (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin)
498177adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ)
499498mul01d 10273 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0)
500491, 101syldan 486 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
501308adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
502 lemul2 10914 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ ((𝑋𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆))))
503468, 492, 501, 502syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆))))
504500, 503mpbid 222 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
505499, 504eqbrtrrd 4709 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
506497, 493, 505fsumge0 14571 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
507506adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
508465, 495, 496, 507leadd2dd 10680 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
509464, 508eqbrtrrd 4709 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
510152recnd 10106 . . . . . . 7 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℂ)
511125, 177, 510fsummulc2 14560 . . . . . 6 (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
512511adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
513 stoweidlem26.2 . . . . . . . . 9 𝑗𝜑
514 elfzelz 12380 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ)
515514adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ)
516515zred 11520 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ)
517313adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
518121adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ)
519 simpr 476 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2)))
520 0zd 11427 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈ ℤ)
521129adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ)
522 elfz 12370 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2))))
523515, 520, 521, 522syl3anc 1366 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2))))
524519, 523mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2)))
525524simprd 478 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2))
526117, 133, 109ltsub2d 10675 . . . . . . . . . . . . . . . 16 (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1)))
527350, 526mpbii 223 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 2) < (𝐿 − 1))
528527adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1))
529516, 517, 518, 525, 528lelttrd 10233 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1))
530516, 518ltnled 10222 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗))
531529, 530mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗)
532531intnanrd 983 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗𝑗𝑁))
533374adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ)
534130adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ)
535 elfz 12370 . . . . . . . . . . . 12 ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗𝑗𝑁)))
536515, 533, 534, 535syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗𝑗𝑁)))
537532, 536mtbird 314 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
538537ex 449 . . . . . . . . 9 (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)))
539513, 538ralrimi 2986 . . . . . . . 8 (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
540 disj 4050 . . . . . . . 8 (((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅ ↔ ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
541539, 540sylibr 224 . . . . . . 7 (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
542541adantr 480 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
543145adantr 480 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁)
544129, 373, 1303jca 1261 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
545544adantr 480 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
546 elfz 12370 . . . . . . . . . 10 (((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
547545, 546syl 17 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
548253, 543, 547mpbir2and 977 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁))
549 fzsplit 12405 . . . . . . . 8 ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
550548, 549syl 17 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
551264, 270, 2713eqtrd 2689 . . . . . . . . . 10 (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1))
552551oveq1d 6705 . . . . . . . . 9 (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁))
553552uneq2d 3800 . . . . . . . 8 (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
554553adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
555550, 554eqtrd 2685 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
556 fzfid 12812 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin)
557177adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
55852recnd 10106 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℂ)
559557, 558mulcld 10098 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
560559adantlr 751 . . . . . 6 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
561542, 555, 556, 560fsumsplit 14515 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
562509, 512, 5613brtr4d 4717 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
563115, 154, 543jca 1261 . . . . . 6 (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ))
564563adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ))
565 ltletr 10167 . . . . 5 ((((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
566564, 565syl 17 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
567459, 562, 566mp2and 715 . . 3 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
568106, 567pm2.61dan 849 . 2 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
569 sumex 14462 . . 3 Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ V
57094oveq2d 6706 . . . . 5 (𝑡 = 𝑆 → (𝐸 · ((𝑋𝑖)‘𝑡)) = (𝐸 · ((𝑋𝑖)‘𝑆)))
571570sumeq2sdv 14479 . . . 4 (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
572 eqid 2651 . . . 4 (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡))) = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))
573571, 572fvmptg 6319 . . 3 ((𝑆𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ V) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
57450, 569, 573sylancl 695 . 2 (𝜑 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
575568, 574breqtrrd 4713 1 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wnf 1748  wcel 2030  wnfc 2780  wne 2823  wral 2941  {crab 2945  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948   class class class wbr 4685  cmpt 4762  wf 5922  cfv 5926  (class class class)co 6690  Fincfn 7997  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304  -cneg 10305   / cdiv 10722  cn 11058  2c2 11108  3c3 11109  4c4 11110  0cn0 11330  cz 11415  cuz 11725  +crp 11870  ...cfz 12364  #chash 13157  Σcsu 14460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-ico 12219  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461
This theorem is referenced by:  stoweidlem34  40569
  Copyright terms: Public domain W3C validator