stoweidlem26 - Mathbox for Glauco Siliprandi

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

Theorem stoweidlem26 43457

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**
Step	Hyp	Ref	Expression
1		1re 10906	. . . . . . . 8 ⊢ 1 ∈ ℝ
2		eleq1 2826	. . . . . . . 8 ⊢ (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
3	1, 2	mpbiri 257	. . . . . . 7 ⊢ (𝐿 = 1 → 𝐿 ∈ ℝ)
4	3	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℝ)
5		4re 11987	. . . . . . . 8 ⊢ 4 ∈ ℝ
6	5	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 4 ∈ ℝ)
7		3re 11983	. . . . . . . 8 ⊢ 3 ∈ ℝ
8	7	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ∈ ℝ)
9		3ne0 12009	. . . . . . . 8 ⊢ 3 ≠ 0
10	9	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ≠ 0)
11	6, 8, 10	redivcld 11733	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈ ℝ)
12	4, 11	resubcld 11333	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
13		stoweidlem26.11	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
14	13	rpred 12701	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ)
15	14	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐸 ∈ ℝ)
16	12, 15	remulcld 10936	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
17		0red 10909	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ∈ ℝ)
18		fzfid 13621	. . . . . 6 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
19	14	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
20		stoweidlem26.13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ)
21		stoweidlem26.9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))))
22		eldif 3893	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
23	21, 22	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
24	23	simpld 494	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝐷‘𝐿))
25		stoweidlem26.4	. . . . . . . . . . . . 13 ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
26		oveq1 7262	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3)))
27	26	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸))
28	27	breq2d 5082	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐿 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
29	28	rabbidv 3404	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐿 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
30		fz1ssfz0 13281	. . . . . . . . . . . . . 14 ⊢ (1...𝑁) ⊆ (0...𝑁)
31		stoweidlem26.8	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))
32	30, 31	sselid 3915	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ (0...𝑁))
33		stoweidlem26.7	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ V)
34		rabexg 5250	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
35	33, 34	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
36	25, 29, 32, 35	fvmptd3 6880	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘𝐿) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
37	24, 36	eleqtrd 2841	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
38		nfcv 2906	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝑆
39		nfcv 2906	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝑇
40		stoweidlem26.1	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡𝐹
41	40, 38	nffv 6766	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡(𝐹‘𝑆)
42		nfcv 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡 ≤
43		nfcv 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝐿 − (1 / 3)) · 𝐸)
44	41, 42, 43	nfbr 5117	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡(𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)
45		fveq2 6756	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (𝐹‘𝑡) = (𝐹‘𝑆))
46	45	breq1d 5080	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
47	38, 39, 44, 46	elrabf 3613	. . . . . . . . . . 11 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
48	37, 47	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
49	48	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ 𝑇)
50	49	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑆 ∈ 𝑇)
51	20, 50	ffvelrnd 6944	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
52	19, 51	remulcld 10936	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
53	18, 52	fsumrecl 15374	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
54	53	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
55	5, 7, 9	redivcli 11672	. . . . . . 7 ⊢ (4 / 3) ∈ ℝ
56	55	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈ ℝ)
57	4, 56	resubcld 11333	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
58	4	recnd 10934	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℂ)
59	58	subid1d 11251	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) = 𝐿)
60		3cn 11984	. . . . . . . . . 10 ⊢ 3 ∈ ℂ
61	60, 9	dividi 11638	. . . . . . . . 9 ⊢ (3 / 3) = 1
62		3lt4 12077	. . . . . . . . . 10 ⊢ 3 < 4
63		3pos 12008	. . . . . . . . . . 11 ⊢ 0 < 3
64	7, 5, 7, 63	ltdiv1ii 11834	. . . . . . . . . 10 ⊢ (3 < 4 ↔ (3 / 3) < (4 / 3))
65	62, 64	mpbi 229	. . . . . . . . 9 ⊢ (3 / 3) < (4 / 3)
66	61, 65	eqbrtrri 5093	. . . . . . . 8 ⊢ 1 < (4 / 3)
67		breq1 5073	. . . . . . . . 9 ⊢ (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
68	67	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
69	66, 68	mpbiri 257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 < (4 / 3))
70	59, 69	eqbrtrd 5092	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) < (4 / 3))
71	4, 17, 56, 70	ltsub23d 11510	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) < 0)
72	13	rpgt0d 12704	. . . . . 6 ⊢ (𝜑 → 0 < 𝐸)
73	72	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 < 𝐸)
74		mulltgt0 42454	. . . . 5 ⊢ ((((𝐿 − (4 / 3)) ∈ ℝ ∧ (𝐿 − (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
75	57, 71, 15, 73, 74	syl22anc 835	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
76		0cn 10898	. . . . . . . 8 ⊢ 0 ∈ ℂ
77		fsumconst 15430	. . . . . . . 8 ⊢ (((0...𝑁) ∈ Fin ∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
78	18, 76, 77	sylancl 585	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
79		hashcl 13999	. . . . . . . . 9 ⊢ ((0...𝑁) ∈ Fin → (♯‘(0...𝑁)) ∈ ℕ₀)
80		nn0cn 12173	. . . . . . . . 9 ⊢ ((♯‘(0...𝑁)) ∈ ℕ₀ → (♯‘(0...𝑁)) ∈ ℂ)
81	18, 79, 80	3syl 18	. . . . . . . 8 ⊢ (𝜑 → (♯‘(0...𝑁)) ∈ ℂ)
82	81	mul01d 11104	. . . . . . 7 ⊢ (𝜑 → ((♯‘(0...𝑁)) · 0) = 0)
83	78, 82	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0)
84	83	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0)
85		0red 10909	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ)
86	13	rpge0d 12705	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝐸)
87	86	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸)
88		stoweidlem26.3	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝜑
89		nfv 1918	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑖 ∈ (0...𝑁)
90	88, 89	nfan 1903	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁))
91		nfv 1918	. . . . . . . . . . 11 ⊢ Ⅎ𝑡0 ≤ ((𝑋‘𝑖)‘𝑆)
92	90, 91	nfim 1900	. . . . . . . . . 10 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
93		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑆 → ((𝑋‘𝑖)‘𝑡) = ((𝑋‘𝑖)‘𝑆))
94	93	breq2d 5082	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑆 → (0 ≤ ((𝑋‘𝑖)‘𝑡) ↔ 0 ≤ ((𝑋‘𝑖)‘𝑆)))
95	94	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))))
96		stoweidlem26.14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡))
97	96	3expia 1119	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 → 0 ≤ ((𝑋‘𝑖)‘𝑡)))
98	97	com12 32	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)))
99	38, 92, 95, 98	vtoclgaf 3502	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)))
100	50, 99	mpcom 38	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
101	19, 51, 87, 100	mulge0d 11482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
102	18, 85, 52, 101	fsumle 15439	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
103	102	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
104	84, 103	eqbrtrrd 5094	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
105	16, 17, 54, 75, 104	ltletrd 11065	. . 3 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
106		elfzelz 13185	. . . . . . . . 9 ⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ)
107		zre 12253	. . . . . . . . 9 ⊢ (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
108	31, 106, 107	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ℝ)
109	5	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 4 ∈ ℝ)
110	7	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 3 ∈ ℝ)
111	9	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 3 ≠ 0)
112	109, 110, 111	redivcld 11733	. . . . . . . 8 ⊢ (𝜑 → (4 / 3) ∈ ℝ)
113	108, 112	resubcld 11333	. . . . . . 7 ⊢ (𝜑 → (𝐿 − (4 / 3)) ∈ ℝ)
114	113, 14	remulcld 10936	. . . . . 6 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
115	114	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
116	1	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℝ)
117		stoweidlem26.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
118	14, 117	nndivred 11957	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
119	116, 118	resubcld 11333	. . . . . . . 8 ⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ)
120	108, 116	resubcld 11333	. . . . . . . 8 ⊢ (𝜑 → (𝐿 − 1) ∈ ℝ)
121	119, 120	remulcld 10936	. . . . . . 7 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
122	14, 121	remulcld 10936	. . . . . 6 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
123	122	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
124		fzfid 13621	. . . . . . . 8 ⊢ (𝜑 → (0...(𝐿 − 2)) ∈ Fin)
125	31	elfzelzd 13186	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℤ)
126		2z 12282	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
127	126	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℤ)
128	125, 127	zsubcld 12360	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 2) ∈ ℤ)
129	117	nnzd 12354	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
130	125	zred 12355	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿 ∈ ℝ)
131		2re 11977	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
132	131	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℝ)
133	130, 132	resubcld 11333	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ∈ ℝ)
134	117	nnred 11918	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ)
135		0le2 12005	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 2
136		0red 10909	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
137	136, 132, 130	lesub2d 11513	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0)))
138	135, 137	mpbii 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0))
139	125	zcnd 12356	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐿 ∈ ℂ)
140	139	subid1d 11251	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 0) = 𝐿)
141	138, 140	breqtrd 5096	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ≤ 𝐿)
142		elfzle2 13189	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ≤ 𝑁)
143	31, 142	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ≤ 𝑁)
144	133, 130, 134, 141, 143	letrd 11062	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 2) ≤ 𝑁)
145	128, 129, 144	3jca 1126	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
146		eluz2 12517	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
147	145, 146	sylibr 233	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝐿 − 2)))
148		fzss2 13225	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
149	147, 148	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁))
150	149	sselda 3917	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
151	150, 51	syldan 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
152	124, 151	fsumrecl 15374	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ)
153	14, 152	remulcld 10936	. . . . . 6 ⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
154	153	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
155	14, 120	remulcld 10936	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · (𝐿 − 1)) ∈ ℝ)
156	14, 14	remulcld 10936	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
157	155, 156	resubcld 11333	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ)
158	120, 117	nndivred 11957	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ)
159	156, 158	remulcld 10936	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ)
160	155, 159	resubcld 11333	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ)
161	120, 14	resubcld 11333	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ)
162	116, 14	readdcld 10935	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 + 𝐸) ∈ ℝ)
163	1, 7, 9	redivcli 11672	. . . . . . . . . . . . . . 15 ⊢ (1 / 3) ∈ ℝ
164	163	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 3) ∈ ℝ)
165		stoweidlem26.12	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 < (1 / 3))
166	14, 164, 116, 165	ltadd2dd 11064	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 + 𝐸) < (1 + (1 / 3)))
167		ax-1cn 10860	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
168	60, 167, 60, 9	divdiri 11662	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
169		3p1e4 12048	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
170	169	oveq1i 7265	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) / 3) = (4 / 3)
171	61	oveq1i 7265	. . . . . . . . . . . . . 14 ⊢ ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
172	168, 170, 171	3eqtr3ri 2775	. . . . . . . . . . . . 13 ⊢ (1 + (1 / 3)) = (4 / 3)
173	166, 172	breqtrdi 5111	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 + 𝐸) < (4 / 3))
174	162, 112, 108, 173	ltsub2dd 11518	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸)))
175	167	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
176	13	rpcnd 12703	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ ℂ)
177	139, 175, 176	subsub4d 11293	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸)))
178	174, 177	breqtrrd 5098	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸))
179	113, 161, 13, 178	ltmul1dd 12756	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸))
180	139, 175	subcld 11262	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 − 1) ∈ ℂ)
181	180, 176	subcld 11262	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ)
182	176, 181	mulcomd 10927	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸))
183	176, 180, 176	subdid 11361	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
184	182, 183	eqtr3d 2780	. . . . . . . . 9 ⊢ (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
185	179, 184	breqtrd 5096	. . . . . . . 8 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
186		1zzd 12281	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℤ)
187		elfz 13174	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)))
188	125, 186, 129, 187	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)))
189	31, 188	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁))
190	189	simprd 495	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ≤ 𝑁)
191		zlem1lt 12302	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁))
192	125, 129, 191	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁))
193	190, 192	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 1) < 𝑁)
194	117	nngt0d 11952	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝑁)
195		ltdiv1 11769	. . . . . . . . . . . . . 14 ⊢ (((𝐿 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
196	120, 134, 134, 194, 195	syl112anc 1372	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
197	193, 196	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))
198	117	nncnd 11919	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
199	117	nnne0d 11953	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
200	198, 199	dividd 11679	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / 𝑁) = 1)
201	197, 200	breqtrd 5096	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < 1)
202	14, 14, 72, 72	mulgt0d 11060	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (𝐸 · 𝐸))
203		ltmul2 11756	. . . . . . . . . . . 12 ⊢ ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 < (𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
204	158, 116, 156, 202, 203	syl112anc 1372	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
205	201, 204	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))
206	176, 176	mulcld 10926	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℂ)
207	206	mulid1d 10923	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸))
208	205, 207	breqtrd 5096	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸))
209	159, 156, 155, 208	ltsub2dd 11518	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
210	114, 157, 160, 185, 209	lttrd 11066	. . . . . . 7 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
211	176, 198, 199	divcld 11681	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
212	175, 211, 180	subdird 11362	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))))
213	180	mulid2d 10924	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1))
214	213	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
215	212, 214	eqtrd 2778	. . . . . . . . 9 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
216	215	oveq2d 7271	. . . . . . . 8 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))))
217	211, 180	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈ ℂ)
218	176, 180, 217	subdid 11361	. . . . . . . 8 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))))
219	176, 198, 180, 199	div32d 11704	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁)))
220	219	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
221	180, 198, 199	divcld 11681	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ)
222	176, 176, 221	mulassd 10929	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
223	220, 222	eqtr4d 2781	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))
224	223	oveq2d 7271	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
225	216, 218, 224	3eqtrd 2782	. . . . . . 7 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
226	210, 225	breqtrrd 5098	. . . . . 6 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
227	226	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
228	175, 211	subcld 11262	. . . . . . . . . 10 ⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ)
229		fsumconst 15430	. . . . . . . . . 10 ⊢ (((0...(𝐿 − 2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
230	124, 228, 229	syl2anc 583	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
231	230	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
232		0zd 12261	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℤ)
233	31	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁))
234	233	elfzelzd 13186	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ)
235	126	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℤ)
236	234, 235	zsubcld 12360	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ)
237		elnnuz 12551	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
238	117, 237	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
239		elfzp12 13264	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
240	238, 239	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
241	31, 240	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
242	241	orcanai 999	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁))
243		1p1e2 12028	. . . . . . . . . . . . . . . . . 18 ⊢ (1 + 1) = 2
244	243	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2)
245	244	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁))
246	242, 245	eleqtrd 2841	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁))
247		elfzle1 13188	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿)
248	246, 247	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿)
249	108	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ)
250	131	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℝ)
251	249, 250	subge0d 11495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿))
252	248, 251	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2))
253	232, 236, 252	3jca 1126	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
254		eluz2 12517	. . . . . . . . . . . 12 ⊢ ((𝐿 − 2) ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
255	253, 254	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (ℤ_≥‘0))
256		hashfz 14070	. . . . . . . . . . 11 ⊢ ((𝐿 − 2) ∈ (ℤ_≥‘0) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
257	255, 256	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
258		2cn 11978	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
259	258	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
260	139, 259	subcld 11262	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ∈ ℂ)
261	260	subid1d 11251	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2))
262	261	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) + 1))
263	139, 259, 175	subadd23d 11284	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2)))
264	258, 167	negsubdi2i 11237	. . . . . . . . . . . . . . . 16 ⊢ -(2 − 1) = (1 − 2)
265		2m1e1 12029	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) = 1
266	265	negeqi 11144	. . . . . . . . . . . . . . . 16 ⊢ -(2 − 1) = -1
267	264, 266	eqtr3i 2768	. . . . . . . . . . . . . . 15 ⊢ (1 − 2) = -1
268	267	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 − 2) = -1)
269	268	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1))
270	139, 175	negsubd 11268	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 + -1) = (𝐿 − 1))
271	269, 270	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1))
272	262, 263, 271	3eqtrd 2782	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
273	272	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
274	257, 273	eqtrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (𝐿 − 1))
275	274	oveq1d 7270	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁))))
276	180, 228	mulcomd 10927	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
277	276	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
278	231, 275, 277	3eqtrd 2782	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
279		fzfid 13621	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin)
280		fzn0 13199	. . . . . . . . 9 ⊢ ((0...(𝐿 − 2)) ≠ ∅ ↔ (𝐿 − 2) ∈ (ℤ_≥‘0))
281	255, 280	sylibr 233	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅)
282	119	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ)
283		simpll 763	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑)
284	150	adantlr 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
285	283, 284, 51	syl2anc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
286	49	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ 𝑇)
287		elfzelz 13185	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ)
288	287	zred 12355	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ)
289	288	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ)
290	163	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈ ℝ)
291	289, 290	readdcld 10935	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ)
292	14	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ)
293	291, 292	remulcld 10936	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ)
294	108	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ)
295	131	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈ ℝ)
296	294, 295	resubcld 11333	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
297	296, 290	readdcld 10935	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
298	297, 292	remulcld 10936	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
299		stoweidlem26.10	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
300	299, 49	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇))
301	300	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇))
302		ffvelrn 6941	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇) → (𝐹‘𝑆) ∈ ℝ)
303	301, 302	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹‘𝑆) ∈ ℝ)
304		elfzle2 13189	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2))
305	304	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2))
306	289, 296, 290, 305	leadd1dd 11519	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)))
307	14, 72	jca 511	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
308	307	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
309		lemul1 11757	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 − 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
310	291, 297, 308, 309	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
311	306, 310	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))
312	108, 132	resubcld 11333	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 − 2) ∈ ℝ)
313	312, 164	readdcld 10935	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
314	313, 14	remulcld 10936	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
315	299, 49	ffvelrnd 6944	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ)
316	120, 164	resubcld 11333	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈ ℝ)
317	316, 14	remulcld 10936	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈ ℝ)
318		addid1 11085	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1 ∈ ℂ → (1 + 0) = 1)
319	318	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 ∈ ℂ → 1 = (1 + 0))
320	167, 319	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 1 = (1 + 0))
321	175	subidd 11250	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 − 1) = 0)
322	321	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 = (1 − 1))
323	322	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + 0) = (1 + (1 − 1)))
324		addsubass 11161	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1) − 1) = (1 + (1 − 1)))
325	324	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1 − 1)) = ((1 + 1) − 1))
326	175, 175, 175, 325	syl3anc 1369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + (1 − 1)) = ((1 + 1) − 1))
327	320, 323, 326	3eqtrd 2782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 1 = ((1 + 1) − 1))
328	327	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) − 1)))
329	243	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + 1) = 2)
330	329	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 + 1) − 1) = (2 − 1))
331	330	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 − 1)))
332	139, 259, 175	subsubd 11290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) + 1))
333	328, 331, 332	3eqtrd 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1))
334	333	oveq1d 7270	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 / 3)))
335	258, 60, 9	divcli 11647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 / 3) ∈ ℂ
336	335	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2 / 3) ∈ ℂ)
337	260, 175, 336	addsubassd 11282	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 / 3))))
338	167, 60, 9	divcli 11647	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 / 3) ∈ ℂ
339		df-3 11967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 3 = (2 + 1)
340	339	oveq1i 7265	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (3 / 3) = ((2 + 1) / 3)
341	258, 167, 60, 9	divdiri 11662	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
342	340, 61, 341	3eqtr3ri 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 / 3) + (1 / 3)) = 1
343	167, 335, 338, 342	subaddrii 11240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − (2 / 3)) = (1 / 3)
344	343	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 − (2 / 3)) = (1 / 3))
345	344	oveq2d 7271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 / 3)))
346	334, 337, 345	3eqtrd 2782	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 / 3)))
347	131, 7, 9	redivcli 11672	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 / 3) ∈ ℝ
348	347	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2 / 3) ∈ ℝ)
349		1lt2 12074	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 < 2
350	7, 63	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (3 ∈ ℝ ∧ 0 < 3)
351	1, 131, 350	3pm3.2i 1337	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
352		ltdiv1 11769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (1 < 2 ↔ (1 / 3) < (2 / 3)))
353	351, 352	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 < 2 ↔ (1 / 3) < (2 / 3)))
354	349, 353	mpbii 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 / 3) < (2 / 3))
355	164, 348, 120, 354	ltsub2dd 11518	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 / 3)))
356	346, 355	eqbrtrrd 5094	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 / 3)))
357	313, 316, 13, 356	ltmul1dd 12756	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸))
358	23	simprd 495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))
359		oveq1 7262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 / 3)))
360	359	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸))
361	360	breq2d 5082	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = (𝐿 − 1) → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
362	361	rabbidv 3404	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝐿 − 1) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
363	129	peano2zd 12358	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
364	189	simpld 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 1 ≤ 𝐿)
365	134, 116	readdcld 10935	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
366	134	lep1d 11836	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
367	108, 134, 365, 190, 366	letrd 11062	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐿 ≤ (𝑁 + 1))
368	186, 363, 125, 364, 367	elfzd 13176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐿 ∈ (1...(𝑁 + 1)))
369	139, 175	npcand 11266	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐿 − 1) + 1) = 𝐿)
370		0p1e1 12025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 + 1) = 1
371	370	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (0 + 1) = 1)
372	371	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
373	368, 369, 372	3eltr4d 2854	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
374		0zd 12261	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℤ)
375	125, 186	zsubcld 12360	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐿 − 1) ∈ ℤ)
376		fzaddel 13219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐿 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
377	374, 129, 375, 186, 376	syl22anc 835	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
378	373, 377	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐿 − 1) ∈ (0...𝑁))
379		rabexg 5250	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
380	33, 379	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
381	25, 362, 378, 380	fvmptd3 6880	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
382	358, 381	neleqtrd 2860	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
383		nfcv 2906	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸)
384	41, 42, 383	nfbr 5117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)
385	45	breq1d 5080	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
386	38, 39, 384, 385	elrabf 3613	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
387	382, 386	sylnib 327	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
388		ianor 978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
389	387, 388	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
390		olc 864	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ 𝑇 → (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇))
391	390	anim1i 614	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑇 ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
392	49, 389, 391	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
393		orcom 866	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))
394	393	anbi2i 622	. . . . . . . . . . . . . . . . . . 19 ⊢ (((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
395	392, 394	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
396		pm4.43 1019	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
397	395, 396	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))
398	317, 315	ltnled 11052	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆) ↔ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
399	397, 398	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆))
400	314, 317, 315, 357, 399	lttrd 11066	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹‘𝑆))
401	314, 315, 400	ltled 11053	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
402	401	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
403	293, 298, 303, 311, 402	letrd 11062	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
404		nfcv 2906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸)
405	404, 42, 41	nfbr 5117	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)
406	45	breq2d 5082	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)))
407	38, 39, 405, 406	elrabf 3613	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑆 ∈ 𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)))
408	286, 403, 407	sylanbrc 582	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
409		stoweidlem26.5	. . . . . . . . . . . 12 ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
410		oveq1 7262	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
411	410	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸))
412	411	breq1d 5080	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
413	412	rabbidv 3404	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑖 → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
414		rabexg 5250	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
415	33, 414	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
416	415	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
417	409, 413, 150, 416	fvmptd3 6880	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐵‘𝑖) = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
418	408, 417	eleqtrrd 2842	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵‘𝑖))
419	145	3ad2ant1 1131	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
420	419, 146	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑁 ∈ (ℤ_≥‘(𝐿 − 2)))
421	420, 148	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
422		simp2 1135	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...(𝐿 − 2)))
423	421, 422	sseldd 3918	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...𝑁))
424		elex 3440	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (𝐵‘𝑖) → 𝑆 ∈ V)
425	424	3ad2ant3 1133	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑆 ∈ V)
426		nfcv 2906	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡(0...𝑁)
427		nfrab1 3310	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
428	426, 427	nfmpt 5177	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
429	409, 428	nfcxfr 2904	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝐵
430		nfcv 2906	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝑖
431	429, 430	nffv 6766	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝐵‘𝑖)
432	431	nfel2 2924	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡 𝑆 ∈ (𝐵‘𝑖)
433	88, 89, 432	nf3an 1905	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖))
434		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)
435	433, 434	nfim 1900	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
436		eleq1 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑆 → (𝑡 ∈ (𝐵‘𝑖) ↔ 𝑆 ∈ (𝐵‘𝑖)))
437	436	3anbi3d 1440	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑆 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖))))
438	93	breq2d 5082	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))
439	437, 438	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))))
440		stoweidlem26.15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡))
441	435, 439, 440	vtoclg1f 3494	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ V → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))
442	425, 441	mpcom 38	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
443	423, 442	syld3an2 1409	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
444	418, 443	mpd3an3 1460	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
445	444	adantlr 711	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
446	279, 281, 282, 285, 445	fsumlt 15440	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))
447	278, 446	eqbrtrrd 5094	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))
448	121	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
449	152	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ)
450	307	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
451		ltmul2 11756	. . . . . . 7 ⊢ ((((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))))
452	448, 449, 450, 451	syl3anc 1369	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))))
453	447, 452	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))
454	115, 123, 154, 227, 453	lttrd 11066	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))
455	150, 52	syldan 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
456	455	adantlr 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
457	456	recnd 10934	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
458	279, 457	fsumcl 15373	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
459	458	addid1d 11105	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
460		0red 10909	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℝ)
461		fzfid 13621	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin)
462	14	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ)
463		0zd 12261	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ)
464	129	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ)
465		elfzelz 13185	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ)
466	465	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ)
467		0red 10909	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ)
468	120	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ)
469	465	zred 12355	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ)
470	469	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ)
471		1m1e0 11975	. . . . . . . . . . . . . . 15 ⊢ (1 − 1) = 0
472	116, 108, 116, 364	lesub1dd 11521	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 − 1) ≤ (𝐿 − 1))
473	471, 472	eqbrtrrid 5106	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (𝐿 − 1))
474	473	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1))
475		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁))
476	375	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ)
477		elfz 13174	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
478	466, 476, 464, 477	syl3anc 1369	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
479	475, 478	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))
480	479	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖)
481	467, 468, 470, 474, 480	letrd 11062	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖)
482		elfzle2 13189	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ≤ 𝑁)
483	482	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ≤ 𝑁)
484	463, 464, 466, 481, 483	elfzd 13176	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁))
485	484, 51	syldan 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
486	462, 485	remulcld 10936	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
487	486	adantlr 711	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
488	461, 487	fsumrecl 15374	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
489	279, 456	fsumrecl 15374	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
490		fzfid 13621	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin)
491	176	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ)
492	491	mul01d 11104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0)
493	484, 100	syldan 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
494	307	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
495		lemul2 11758	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ ((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))))
496	467, 485, 494, 495	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))))
497	493, 496	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
498	492, 497	eqbrtrrd 5094	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
499	490, 486, 498	fsumge0 15435	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
500	499	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
501	460, 488, 489, 500	leadd2dd 11520	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
502	459, 501	eqbrtrrd 5094	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
503	151	recnd 10934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ)
504	124, 176, 503	fsummulc2 15424	. . . . . 6 ⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
505	504	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
506		stoweidlem26.2	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
507		elfzelz 13185	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ)
508	507	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ)
509	508	zred 12355	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ)
510	312	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
511	120	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ)
512		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2)))
513		0zd 12261	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈ ℤ)
514	128	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ)
515		elfz 13174	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))))
516	508, 513, 514, 515	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))))
517	512, 516	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2)))
518	517	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2))
519	116, 132, 108	ltsub2d 11515	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1)))
520	349, 519	mpbii 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 2) < (𝐿 − 1))
521	520	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1))
522	509, 510, 511, 518, 521	lelttrd 11063	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1))
523	509, 511	ltnled 11052	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗))
524	522, 523	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗)
525	524	intnanrd 489	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))
526	375	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ)
527	129	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ)
528		elfz 13174	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
529	508, 526, 527, 528	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
530	525, 529	mtbird 324	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
531	530	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)))
532	506, 531	ralrimi 3139	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
533		disj 4378	. . . . . . . 8 ⊢ (((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅ ↔ ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
534	532, 533	sylibr 233	. . . . . . 7 ⊢ (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
535	534	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
536	144	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁)
537	128, 374, 129	3jca 1126	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
538	537	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
539		elfz 13174	. . . . . . . . . 10 ⊢ (((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
540	538, 539	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
541	252, 536, 540	mpbir2and 709	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁))
542		fzsplit 13211	. . . . . . . 8 ⊢ ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
543	541, 542	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
544	263, 269, 270	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1))
545	544	oveq1d 7270	. . . . . . . . 9 ⊢ (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁))
546	545	uneq2d 4093	. . . . . . . 8 ⊢ (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
547	546	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
548	543, 547	eqtrd 2778	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
549		fzfid 13621	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin)
550	176	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
551	51	recnd 10934	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ)
552	550, 551	mulcld 10926	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
553	552	adantlr 711	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
554	535, 548, 549, 553	fsumsplit 15381	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
555	502, 505, 554	3brtr4d 5102	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
556	114, 153, 53	3jca 1126	. . . . . 6 ⊢ (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ))
557	556	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ))
558		ltletr 10997	. . . . 5 ⊢ ((((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
559	557, 558	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
560	454, 555, 559	mp2and 695	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
561	105, 560	pm2.61dan 809	. 2 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
562		sumex 15327	. . 3 ⊢ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V
563	93	oveq2d 7271	. . . . 5 ⊢ (𝑡 = 𝑆 → (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘𝑖)‘𝑆)))
564	563	sumeq2sdv 15344	. . . 4 ⊢ (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
565		eqid 2738	. . . 4 ⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))
566	564, 565	fvmptg 6855	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
567	49, 562, 566	sylancl 585	. 2 ⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
568	561, 567	breqtrrd 5098	1 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∧ w3a 1085 = wceq 1539 Ⅎwnf 1787 ∈ wcel 2108 Ⅎwnfc 2886 ≠ wne 2942 ∀wral 3063 {crab 3067 Vcvv 3422 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 class class class wbr 5070 ↦ cmpt 5153 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 Fincfn 8691 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 < clt 10940 ≤ cle 10941 − cmin 11135 -cneg 11136 / cdiv 11562 ℕcn 11903 2c2 11958 3c3 11959 4c4 11960 ℕ₀cn0 12163 ℤcz 12249 ℤ_≥cuz 12511 ℝ⁺crp 12659 ...cfz 13168 ♯chash 13972 Σcsu 15325

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-oi 9199 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-ico 13014 df-fz 13169 df-fzo 13312 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-clim 15125 df-sum 15326

This theorem is referenced by: stoweidlem34 43465

W3C validator