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 40243

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 10039	. . . . . . . 8 ⊢ 1 ∈ ℝ
2		eleq1 2689	. . . . . . . 8 ⊢ (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
3	1, 2	mpbiri 248	. . . . . . 7 ⊢ (𝐿 = 1 → 𝐿 ∈ ℝ)
4	3	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℝ)
5		4re 11097	. . . . . . . 8 ⊢ 4 ∈ ℝ
6	5	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 4 ∈ ℝ)
7		3re 11094	. . . . . . . 8 ⊢ 3 ∈ ℝ
8	7	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ∈ ℝ)
9		3ne0 11115	. . . . . . . 8 ⊢ 3 ≠ 0
10	9	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ≠ 0)
11	6, 8, 10	redivcld 10853	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈ ℝ)
12	4, 11	resubcld 10458	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
13		stoweidlem26.11	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
14	13	rpred 11872	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ)
15	14	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐸 ∈ ℝ)
16	12, 15	remulcld 10070	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
17		0red 10041	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ∈ ℝ)
18		fzfid 12772	. . . . . 6 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
19	14	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
20		stoweidlem26.13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ)
21		stoweidlem26.9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))))
22		eldif 3584	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
23	21, 22	sylib 208	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
24	23	simpld 475	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝐷‘𝐿))
25		1e0p1 11552	. . . . . . . . . . . . . . . 16 ⊢ 1 = (0 + 1)
26	25	oveq1i 6660	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) = ((0 + 1)...𝑁)
27		0z 11388	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℤ
28		fzp1ss 12392	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ ℤ → ((0 + 1)...𝑁) ⊆ (0...𝑁))
29	27, 28	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((0 + 1)...𝑁) ⊆ (0...𝑁)
30	26, 29	eqsstri 3635	. . . . . . . . . . . . . 14 ⊢ (1...𝑁) ⊆ (0...𝑁)
31		stoweidlem26.8	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))
32	30, 31	sseldi 3601	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ (0...𝑁))
33		stoweidlem26.7	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ V)
34		rabexg 4812	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
35	33, 34	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
36		oveq1 6657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3)))
37	36	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸))
38	37	breq2d 4665	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐿 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
39	38	rabbidv 3189	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐿 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
40		stoweidlem26.4	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
41	39, 40	fvmptg 6280	. . . . . . . . . . . . 13 ⊢ ((𝐿 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘𝐿) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
42	32, 35, 41	syl2anc 693	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘𝐿) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
43	24, 42	eleqtrd 2703	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
44		nfcv 2764	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝑆
45		nfcv 2764	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝑇
46		stoweidlem26.1	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡𝐹
47	46, 44	nffv 6198	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡(𝐹‘𝑆)
48		nfcv 2764	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡 ≤
49		nfcv 2764	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝐿 − (1 / 3)) · 𝐸)
50	47, 48, 49	nfbr 4699	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡(𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)
51		fveq2 6191	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (𝐹‘𝑡) = (𝐹‘𝑆))
52	51	breq1d 4663	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
53	44, 45, 50, 52	elrabf 3360	. . . . . . . . . . 11 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
54	43, 53	sylib 208	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
55	54	simpld 475	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ 𝑇)
56	55	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑆 ∈ 𝑇)
57	20, 56	ffvelrnd 6360	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
58	19, 57	remulcld 10070	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
59	18, 58	fsumrecl 14465	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
60	59	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
61	5, 7, 9	redivcli 10792	. . . . . . 7 ⊢ (4 / 3) ∈ ℝ
62	61	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈ ℝ)
63	4, 62	resubcld 10458	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
64	4	recnd 10068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℂ)
65	64	subid1d 10381	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) = 𝐿)
66		3cn 11095	. . . . . . . . . 10 ⊢ 3 ∈ ℂ
67	66, 9	dividi 10758	. . . . . . . . 9 ⊢ (3 / 3) = 1
68		3lt4 11197	. . . . . . . . . 10 ⊢ 3 < 4
69		3pos 11114	. . . . . . . . . . 11 ⊢ 0 < 3
70	7, 5, 7, 69	ltdiv1ii 10953	. . . . . . . . . 10 ⊢ (3 < 4 ↔ (3 / 3) < (4 / 3))
71	68, 70	mpbi 220	. . . . . . . . 9 ⊢ (3 / 3) < (4 / 3)
72	67, 71	eqbrtrri 4676	. . . . . . . 8 ⊢ 1 < (4 / 3)
73		breq1 4656	. . . . . . . . 9 ⊢ (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
74	73	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
75	72, 74	mpbiri 248	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 < (4 / 3))
76	65, 75	eqbrtrd 4675	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) < (4 / 3))
77	4, 17, 62, 76	ltsub23d 10632	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) < 0)
78	13	rpgt0d 11875	. . . . . 6 ⊢ (𝜑 → 0 < 𝐸)
79	78	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 < 𝐸)
80		mulltgt0 39181	. . . . 5 ⊢ ((((𝐿 − (4 / 3)) ∈ ℝ ∧ (𝐿 − (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
81	63, 77, 15, 79, 80	syl22anc 1327	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
82		0cn 10032	. . . . . . . 8 ⊢ 0 ∈ ℂ
83		fsumconst 14522	. . . . . . . 8 ⊢ (((0...𝑁) ∈ Fin ∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((#‘(0...𝑁)) · 0))
84	18, 82, 83	sylancl 694	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((#‘(0...𝑁)) · 0))
85		hashcl 13147	. . . . . . . . 9 ⊢ ((0...𝑁) ∈ Fin → (#‘(0...𝑁)) ∈ ℕ₀)
86		nn0cn 11302	. . . . . . . . 9 ⊢ ((#‘(0...𝑁)) ∈ ℕ₀ → (#‘(0...𝑁)) ∈ ℂ)
87	18, 85, 86	3syl 18	. . . . . . . 8 ⊢ (𝜑 → (#‘(0...𝑁)) ∈ ℂ)
88	87	mul01d 10235	. . . . . . 7 ⊢ (𝜑 → ((#‘(0...𝑁)) · 0) = 0)
89	84, 88	eqtrd 2656	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0)
90	89	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0)
91		0red 10041	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ)
92	13	rpge0d 11876	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝐸)
93	92	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸)
94		stoweidlem26.3	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝜑
95		nfv 1843	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑖 ∈ (0...𝑁)
96	94, 95	nfan 1828	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁))
97		nfv 1843	. . . . . . . . . . 11 ⊢ Ⅎ𝑡0 ≤ ((𝑋‘𝑖)‘𝑆)
98	96, 97	nfim 1825	. . . . . . . . . 10 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
99		fveq2 6191	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑆 → ((𝑋‘𝑖)‘𝑡) = ((𝑋‘𝑖)‘𝑆))
100	99	breq2d 4665	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑆 → (0 ≤ ((𝑋‘𝑖)‘𝑡) ↔ 0 ≤ ((𝑋‘𝑖)‘𝑆)))
101	100	imbi2d 330	. . . . . . . . . 10 ⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))))
102		stoweidlem26.14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡))
103	102	3expia 1267	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 → 0 ≤ ((𝑋‘𝑖)‘𝑡)))
104	103	com12 32	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)))
105	44, 98, 101, 104	vtoclgaf 3271	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)))
106	56, 105	mpcom 38	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
107	19, 57, 93, 106	mulge0d 10604	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
108	18, 91, 58, 107	fsumle 14531	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
109	108	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
110	90, 109	eqbrtrrd 4677	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
111	16, 17, 60, 81, 110	ltletrd 10197	. . 3 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
112		elfzelz 12342	. . . . . . . . 9 ⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ)
113		zre 11381	. . . . . . . . 9 ⊢ (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
114	31, 112, 113	3syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ ℝ)
115	5	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 4 ∈ ℝ)
116	7	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 3 ∈ ℝ)
117	9	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 3 ≠ 0)
118	115, 116, 117	redivcld 10853	. . . . . . . 8 ⊢ (𝜑 → (4 / 3) ∈ ℝ)
119	114, 118	resubcld 10458	. . . . . . 7 ⊢ (𝜑 → (𝐿 − (4 / 3)) ∈ ℝ)
120	119, 14	remulcld 10070	. . . . . 6 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
121	120	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
122	1	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℝ)
123		stoweidlem26.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
124	14, 123	nndivred 11069	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
125	122, 124	resubcld 10458	. . . . . . . 8 ⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ)
126	114, 122	resubcld 10458	. . . . . . . 8 ⊢ (𝜑 → (𝐿 − 1) ∈ ℝ)
127	125, 126	remulcld 10070	. . . . . . 7 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
128	14, 127	remulcld 10070	. . . . . 6 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
129	128	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
130		fzfid 12772	. . . . . . . 8 ⊢ (𝜑 → (0...(𝐿 − 2)) ∈ Fin)
131	31, 112	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℤ)
132		2z 11409	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
133	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℤ)
134	131, 133	zsubcld 11487	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 2) ∈ ℤ)
135	123	nnzd 11481	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
136	131	zred 11482	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿 ∈ ℝ)
137		2re 11090	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
138	137	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℝ)
139	136, 138	resubcld 10458	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ∈ ℝ)
140	123	nnred 11035	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ)
141		0le2 11111	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 2
142		0red 10041	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
143	142, 138, 136	lesub2d 10635	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0)))
144	141, 143	mpbii 223	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0))
145	131	zcnd 11483	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐿 ∈ ℂ)
146	145	subid1d 10381	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 0) = 𝐿)
147	144, 146	breqtrd 4679	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ≤ 𝐿)
148		elfzle2 12345	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ≤ 𝑁)
149	31, 148	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ≤ 𝑁)
150	139, 136, 140, 147, 149	letrd 10194	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 2) ≤ 𝑁)
151	134, 135, 150	3jca 1242	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
152		eluz2 11693	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
153	151, 152	sylibr 224	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝐿 − 2)))
154		fzss2 12381	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
155	153, 154	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁))
156	155	sselda 3603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
157	156, 57	syldan 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
158	130, 157	fsumrecl 14465	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ)
159	14, 158	remulcld 10070	. . . . . 6 ⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
160	159	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
161	14, 126	remulcld 10070	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · (𝐿 − 1)) ∈ ℝ)
162	14, 14	remulcld 10070	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
163	161, 162	resubcld 10458	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ)
164	126, 123	nndivred 11069	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ)
165	162, 164	remulcld 10070	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ)
166	161, 165	resubcld 10458	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ)
167	126, 14	resubcld 10458	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ)
168	122, 14	readdcld 10069	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 + 𝐸) ∈ ℝ)
169	1, 7, 9	redivcli 10792	. . . . . . . . . . . . . . 15 ⊢ (1 / 3) ∈ ℝ
170	169	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 3) ∈ ℝ)
171		stoweidlem26.12	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 < (1 / 3))
172	14, 170, 122, 171	ltadd2dd 10196	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 + 𝐸) < (1 + (1 / 3)))
173		ax-1cn 9994	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
174	66, 173, 66, 9	divdiri 10782	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
175		3p1e4 11153	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
176	175	oveq1i 6660	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) / 3) = (4 / 3)
177	67	oveq1i 6660	. . . . . . . . . . . . . 14 ⊢ ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
178	174, 176, 177	3eqtr3ri 2653	. . . . . . . . . . . . 13 ⊢ (1 + (1 / 3)) = (4 / 3)
179	172, 178	syl6breq 4694	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 + 𝐸) < (4 / 3))
180	168, 118, 114, 179	ltsub2dd 10640	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸)))
181	173	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
182	13	rpcnd 11874	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ ℂ)
183	145, 181, 182	subsub4d 10423	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸)))
184	180, 183	breqtrrd 4681	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸))
185	119, 167, 13, 184	ltmul1dd 11927	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸))
186	145, 181	subcld 10392	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 − 1) ∈ ℂ)
187	186, 182	subcld 10392	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ)
188	182, 187	mulcomd 10061	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸))
189	182, 186, 182	subdid 10486	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
190	188, 189	eqtr3d 2658	. . . . . . . . 9 ⊢ (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
191	185, 190	breqtrd 4679	. . . . . . . 8 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
192		1zzd 11408	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℤ)
193		elfz 12332	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)))
194	131, 192, 135, 193	syl3anc 1326	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)))
195	31, 194	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁))
196	195	simprd 479	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ≤ 𝑁)
197		zlem1lt 11429	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁))
198	131, 135, 197	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁))
199	196, 198	mpbid 222	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 1) < 𝑁)
200	123	nngt0d 11064	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝑁)
201		ltdiv1 10887	. . . . . . . . . . . . . 14 ⊢ (((𝐿 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
202	126, 140, 140, 200, 201	syl112anc 1330	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
203	199, 202	mpbid 222	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))
204	123	nncnd 11036	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
205	123	nnne0d 11065	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
206	204, 205	dividd 10799	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / 𝑁) = 1)
207	203, 206	breqtrd 4679	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < 1)
208	14, 14, 78, 78	mulgt0d 10192	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (𝐸 · 𝐸))
209		ltmul2 10874	. . . . . . . . . . . 12 ⊢ ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 < (𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
210	164, 122, 162, 208, 209	syl112anc 1330	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
211	207, 210	mpbid 222	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))
212	182, 182	mulcld 10060	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℂ)
213	212	mulid1d 10057	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸))
214	211, 213	breqtrd 4679	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸))
215	165, 162, 161, 214	ltsub2dd 10640	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
216	120, 163, 166, 191, 215	lttrd 10198	. . . . . . 7 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
217	182, 204, 205	divcld 10801	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
218	181, 217, 186	subdird 10487	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))))
219	186	mulid2d 10058	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1))
220	219	oveq1d 6665	. . . . . . . . . 10 ⊢ (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
221	218, 220	eqtrd 2656	. . . . . . . . 9 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
222	221	oveq2d 6666	. . . . . . . 8 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))))
223	217, 186	mulcld 10060	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈ ℂ)
224	182, 186, 223	subdid 10486	. . . . . . . 8 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))))
225	182, 204, 186, 205	div32d 10824	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁)))
226	225	oveq2d 6666	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
227	186, 204, 205	divcld 10801	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ)
228	182, 182, 227	mulassd 10063	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
229	226, 228	eqtr4d 2659	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))
230	229	oveq2d 6666	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
231	222, 224, 230	3eqtrd 2660	. . . . . . 7 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
232	216, 231	breqtrrd 4681	. . . . . 6 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
233	232	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
234	181, 217	subcld 10392	. . . . . . . . . 10 ⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ)
235		fsumconst 14522	. . . . . . . . . 10 ⊢ (((0...(𝐿 − 2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
236	130, 234, 235	syl2anc 693	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
237	236	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
238		0zd 11389	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℤ)
239	31	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁))
240	239, 112	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ)
241	132	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℤ)
242	240, 241	zsubcld 11487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ)
243		elnnuz 11724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
244	123, 243	sylib 208	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
245		elfzp12 12419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
246	244, 245	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
247	31, 246	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
248	247	orcanai 952	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁))
249		1p1e2 11134	. . . . . . . . . . . . . . . . . 18 ⊢ (1 + 1) = 2
250	249	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2)
251	250	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁))
252	248, 251	eleqtrd 2703	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁))
253		elfzle1 12344	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿)
254	252, 253	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿)
255	114	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ)
256	137	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℝ)
257	255, 256	subge0d 10617	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿))
258	254, 257	mpbird 247	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2))
259	238, 242, 258	3jca 1242	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
260		eluz2 11693	. . . . . . . . . . . 12 ⊢ ((𝐿 − 2) ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
261	259, 260	sylibr 224	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (ℤ_≥‘0))
262		hashfz 13214	. . . . . . . . . . 11 ⊢ ((𝐿 − 2) ∈ (ℤ_≥‘0) → (#‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
263	261, 262	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (#‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
264		2cn 11091	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
265	264	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
266	145, 265	subcld 10392	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ∈ ℂ)
267	266	subid1d 10381	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2))
268	267	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) + 1))
269	145, 265, 181	subadd23d 10414	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2)))
270	264, 173	negsubdi2i 10367	. . . . . . . . . . . . . . . 16 ⊢ -(2 − 1) = (1 − 2)
271		2m1e1 11135	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) = 1
272	271	negeqi 10274	. . . . . . . . . . . . . . . 16 ⊢ -(2 − 1) = -1
273	270, 272	eqtr3i 2646	. . . . . . . . . . . . . . 15 ⊢ (1 − 2) = -1
274	273	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 − 2) = -1)
275	274	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1))
276	145, 181	negsubd 10398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 + -1) = (𝐿 − 1))
277	275, 276	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1))
278	268, 269, 277	3eqtrd 2660	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
279	278	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
280	263, 279	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (#‘(0...(𝐿 − 2))) = (𝐿 − 1))
281	280	oveq1d 6665	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁))))
282	186, 234	mulcomd 10061	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
283	282	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
284	237, 281, 283	3eqtrd 2660	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
285		fzfid 12772	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin)
286		fzn0 12355	. . . . . . . . 9 ⊢ ((0...(𝐿 − 2)) ≠ ∅ ↔ (𝐿 − 2) ∈ (ℤ_≥‘0))
287	261, 286	sylibr 224	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅)
288	125	ad2antrr 762	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ)
289		simpll 790	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑)
290	156	adantlr 751	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
291	289, 290, 57	syl2anc 693	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
292	55	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ 𝑇)
293		elfzelz 12342	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ)
294	293	zred 11482	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ)
295	294	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ)
296	169	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈ ℝ)
297	295, 296	readdcld 10069	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ)
298	14	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ)
299	297, 298	remulcld 10070	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ)
300	114	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ)
301	137	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈ ℝ)
302	300, 301	resubcld 10458	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
303	302, 296	readdcld 10069	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
304	303, 298	remulcld 10070	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
305		stoweidlem26.10	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
306	305, 55	jca 554	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇))
307	306	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇))
308		ffvelrn 6357	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇) → (𝐹‘𝑆) ∈ ℝ)
309	307, 308	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹‘𝑆) ∈ ℝ)
310		elfzle2 12345	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2))
311	310	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2))
312	295, 302, 296, 311	leadd1dd 10641	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)))
313	14, 78	jca 554	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
314	313	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
315		lemul1 10875	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 − 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
316	297, 303, 314, 315	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
317	312, 316	mpbid 222	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))
318	114, 138	resubcld 10458	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 − 2) ∈ ℝ)
319	318, 170	readdcld 10069	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
320	319, 14	remulcld 10070	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
321	305, 55	ffvelrnd 6360	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ)
322	126, 170	resubcld 10458	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈ ℝ)
323	322, 14	remulcld 10070	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈ ℝ)
324		addid1 10216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1 ∈ ℂ → (1 + 0) = 1)
325	324	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 ∈ ℂ → 1 = (1 + 0))
326	173, 325	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 1 = (1 + 0))
327	181	subidd 10380	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 − 1) = 0)
328	327	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 = (1 − 1))
329	328	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + 0) = (1 + (1 − 1)))
330		addsubass 10291	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1) − 1) = (1 + (1 − 1)))
331	330	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1 − 1)) = ((1 + 1) − 1))
332	181, 181, 181, 331	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + (1 − 1)) = ((1 + 1) − 1))
333	326, 329, 332	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 1 = ((1 + 1) − 1))
334	333	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) − 1)))
335	249	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + 1) = 2)
336	335	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 + 1) − 1) = (2 − 1))
337	336	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 − 1)))
338	145, 265, 181	subsubd 10420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) + 1))
339	334, 337, 338	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1))
340	339	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 / 3)))
341	264, 66, 9	divcli 10767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 / 3) ∈ ℂ
342	341	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2 / 3) ∈ ℂ)
343	266, 181, 342	addsubassd 10412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 / 3))))
344	173, 66, 9	divcli 10767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 / 3) ∈ ℂ
345		df-3 11080	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 3 = (2 + 1)
346	345	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (3 / 3) = ((2 + 1) / 3)
347	264, 173, 66, 9	divdiri 10782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
348	346, 67, 347	3eqtr3ri 2653	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 / 3) + (1 / 3)) = 1
349	173, 341, 344, 348	subaddrii 10370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − (2 / 3)) = (1 / 3)
350	349	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 − (2 / 3)) = (1 / 3))
351	350	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 / 3)))
352	340, 343, 351	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 / 3)))
353	137, 7, 9	redivcli 10792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 / 3) ∈ ℝ
354	353	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2 / 3) ∈ ℝ)
355		1lt2 11194	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 < 2
356	7, 69	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (3 ∈ ℝ ∧ 0 < 3)
357	1, 137, 356	3pm3.2i 1239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
358		ltdiv1 10887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (1 < 2 ↔ (1 / 3) < (2 / 3)))
359	357, 358	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 < 2 ↔ (1 / 3) < (2 / 3)))
360	355, 359	mpbii 223	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 / 3) < (2 / 3))
361	170, 354, 126, 360	ltsub2dd 10640	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 / 3)))
362	352, 361	eqbrtrrd 4677	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 / 3)))
363	319, 322, 13, 362	ltmul1dd 11927	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸))
364	23	simprd 479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))
365	195	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 1 ≤ 𝐿)
366	140, 122	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
367	140	lep1d 10955	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
368	114, 140, 366, 196, 367	letrd 10194	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐿 ≤ (𝑁 + 1))
369	135	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
370		elfz 12332	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → (𝐿 ∈ (1...(𝑁 + 1)) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 + 1))))
371	131, 192, 369, 370	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝐿 ∈ (1...(𝑁 + 1)) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 + 1))))
372	365, 368, 371	mpbir2and 957	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐿 ∈ (1...(𝑁 + 1)))
373	145, 181	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐿 − 1) + 1) = 𝐿)
374		0p1e1 11132	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 + 1) = 1
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (0 + 1) = 1)
376	375	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
377	372, 373, 376	3eltr4d 2716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
378		0zd 11389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℤ)
379	131, 192	zsubcld 11487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐿 − 1) ∈ ℤ)
380		fzaddel 12375	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐿 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
381	378, 135, 379, 192, 380	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
382	377, 381	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐿 − 1) ∈ (0...𝑁))
383		rabexg 4812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
384	33, 383	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
385		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 / 3)))
386	385	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸))
387	386	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (𝐿 − 1) → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
388	387	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = (𝐿 − 1) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
389	388, 40	fvmptg 6280	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐿 − 1) ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘(𝐿 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
390	382, 384, 389	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
391	364, 390	neleqtrd 2722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
392		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸)
393	47, 48, 392	nfbr 4699	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)
394	51	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
395	44, 45, 393, 394	elrabf 3360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
396	391, 395	sylnib 318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
397		ianor 509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
398	396, 397	sylib 208	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
399		olc 399	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ 𝑇 → (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇))
400	399	anim1i 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑇 ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
401	55, 398, 400	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
402		orcom 402	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))
403	402	anbi2i 730	. . . . . . . . . . . . . . . . . . 19 ⊢ (((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
404	401, 403	sylib 208	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
405		pm4.43 968	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
406	404, 405	sylibr 224	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))
407	323, 321	ltnled 10184	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆) ↔ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
408	406, 407	mpbird 247	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆))
409	320, 323, 321, 363, 408	lttrd 10198	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹‘𝑆))
410	320, 321, 409	ltled 10185	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
411	410	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
412	299, 304, 309, 317, 411	letrd 10194	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
413		nfcv 2764	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸)
414	413, 48, 47	nfbr 4699	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)
415	51	breq2d 4665	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)))
416	44, 45, 414, 415	elrabf 3360	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑆 ∈ 𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)))
417	292, 412, 416	sylanbrc 698	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
418		rabexg 4812	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
419	33, 418	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
420	419	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
421		oveq1 6657	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
422	421	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸))
423	422	breq1d 4663	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
424	423	rabbidv 3189	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
425		stoweidlem26.5	. . . . . . . . . . . . 13 ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
426	424, 425	fvmptg 6280	. . . . . . . . . . . 12 ⊢ ((𝑖 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) → (𝐵‘𝑖) = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
427	156, 420, 426	syl2anc 693	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐵‘𝑖) = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
428	417, 427	eleqtrrd 2704	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵‘𝑖))
429	151	3ad2ant1 1082	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
430	429, 152	sylibr 224	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑁 ∈ (ℤ_≥‘(𝐿 − 2)))
431	430, 154	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
432		simp2 1062	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...(𝐿 − 2)))
433	431, 432	sseldd 3604	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...𝑁))
434		elex 3212	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (𝐵‘𝑖) → 𝑆 ∈ V)
435	434	3ad2ant3 1084	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑆 ∈ V)
436		nfcv 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡(0...𝑁)
437		nfrab1 3122	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
438	436, 437	nfmpt 4746	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
439	425, 438	nfcxfr 2762	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝐵
440		nfcv 2764	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝑖
441	439, 440	nffv 6198	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝐵‘𝑖)
442	441	nfel2 2781	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡 𝑆 ∈ (𝐵‘𝑖)
443	94, 95, 442	nf3an 1831	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖))
444		nfv 1843	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)
445	443, 444	nfim 1825	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
446		eleq1 2689	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑆 → (𝑡 ∈ (𝐵‘𝑖) ↔ 𝑆 ∈ (𝐵‘𝑖)))
447	446	3anbi3d 1405	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑆 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖))))
448	99	breq2d 4665	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))
449	447, 448	imbi12d 334	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))))
450		stoweidlem26.15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡))
451	445, 449, 450	vtoclg1f 3265	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ V → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))
452	435, 451	mpcom 38	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
453	433, 452	syld3an2 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
454	428, 453	mpd3an3 1425	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
455	454	adantlr 751	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
456	285, 287, 288, 291, 455	fsumlt 14532	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))
457	284, 456	eqbrtrrd 4677	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))
458	127	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
459	158	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ)
460	313	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
461		ltmul2 10874	. . . . . . 7 ⊢ ((((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))))
462	458, 459, 460, 461	syl3anc 1326	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))))
463	457, 462	mpbid 222	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))
464	121, 129, 160, 233, 463	lttrd 10198	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))
465	156, 58	syldan 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
466	465	adantlr 751	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
467	466	recnd 10068	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
468	285, 467	fsumcl 14464	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
469	468	addid1d 10236	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
470		0red 10041	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℝ)
471		fzfid 12772	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin)
472	14	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ)
473		0red 10041	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ)
474	126	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ)
475		elfzelz 12342	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ)
476	475	zred 11482	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ)
477	476	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ)
478		1m1e0 11089	. . . . . . . . . . . . . . 15 ⊢ (1 − 1) = 0
479	122, 114, 122, 365	lesub1dd 10643	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 − 1) ≤ (𝐿 − 1))
480	478, 479	syl5eqbrr 4689	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (𝐿 − 1))
481	480	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1))
482		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁))
483	475	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ)
484	379	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ)
485	135	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ)
486		elfz 12332	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
487	483, 484, 485, 486	syl3anc 1326	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
488	482, 487	mpbid 222	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))
489	488	simpld 475	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖)
490	473, 474, 477, 481, 489	letrd 10194	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖)
491		elfzle2 12345	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ≤ 𝑁)
492	491	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ≤ 𝑁)
493		0zd 11389	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ)
494		elfz 12332	. . . . . . . . . . . . 13 ⊢ ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0...𝑁) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
495	483, 493, 485, 494	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ (0...𝑁) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
496	490, 492, 495	mpbir2and 957	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁))
497	496, 57	syldan 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
498	472, 497	remulcld 10070	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
499	498	adantlr 751	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
500	471, 499	fsumrecl 14465	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
501	285, 466	fsumrecl 14465	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
502		fzfid 12772	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin)
503	182	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ)
504	503	mul01d 10235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0)
505	496, 106	syldan 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
506	313	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
507		lemul2 10876	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ ((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))))
508	473, 497, 506, 507	syl3anc 1326	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))))
509	505, 508	mpbid 222	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
510	504, 509	eqbrtrrd 4677	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
511	502, 498, 510	fsumge0 14527	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
512	511	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
513	470, 500, 501, 512	leadd2dd 10642	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
514	469, 513	eqbrtrrd 4677	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
515	157	recnd 10068	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ)
516	130, 182, 515	fsummulc2 14516	. . . . . 6 ⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
517	516	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
518		stoweidlem26.2	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
519		elfzelz 12342	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ)
520	519	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ)
521	520	zred 11482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ)
522	318	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
523	126	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ)
524		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2)))
525		0zd 11389	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈ ℤ)
526	134	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ)
527		elfz 12332	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))))
528	520, 525, 526, 527	syl3anc 1326	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))))
529	524, 528	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2)))
530	529	simprd 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2))
531	122, 138, 114	ltsub2d 10637	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1)))
532	355, 531	mpbii 223	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 2) < (𝐿 − 1))
533	532	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1))
534	521, 522, 523, 530, 533	lelttrd 10195	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1))
535	521, 523	ltnled 10184	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗))
536	534, 535	mpbid 222	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗)
537	536	intnanrd 963	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))
538	379	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ)
539	135	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ)
540		elfz 12332	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
541	520, 538, 539, 540	syl3anc 1326	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
542	537, 541	mtbird 315	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
543	542	ex 450	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)))
544	518, 543	ralrimi 2957	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
545		disj 4017	. . . . . . . 8 ⊢ (((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅ ↔ ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
546	544, 545	sylibr 224	. . . . . . 7 ⊢ (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
547	546	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
548	150	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁)
549	134, 378, 135	3jca 1242	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
550	549	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
551		elfz 12332	. . . . . . . . . 10 ⊢ (((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
552	550, 551	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
553	258, 548, 552	mpbir2and 957	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁))
554		fzsplit 12367	. . . . . . . 8 ⊢ ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
555	553, 554	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
556	269, 275, 276	3eqtrd 2660	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1))
557	556	oveq1d 6665	. . . . . . . . 9 ⊢ (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁))
558	557	uneq2d 3767	. . . . . . . 8 ⊢ (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
559	558	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
560	555, 559	eqtrd 2656	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
561		fzfid 12772	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin)
562	182	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
563	57	recnd 10068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ)
564	562, 563	mulcld 10060	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
565	564	adantlr 751	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
566	547, 560, 561, 565	fsumsplit 14471	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
567	514, 517, 566	3brtr4d 4685	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
568	120, 159, 59	3jca 1242	. . . . . 6 ⊢ (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ))
569	568	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ))
570		ltletr 10129	. . . . 5 ⊢ ((((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
571	569, 570	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
572	464, 567, 571	mp2and 715	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
573	111, 572	pm2.61dan 832	. 2 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
574		sumex 14418	. . 3 ⊢ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V
575	99	oveq2d 6666	. . . . 5 ⊢ (𝑡 = 𝑆 → (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘𝑖)‘𝑆)))
576	575	sumeq2sdv 14435	. . . 4 ⊢ (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
577		eqid 2622	. . . 4 ⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))
578	576, 577	fvmptg 6280	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
579	55, 574, 578	sylancl 694	. 2 ⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
580	573, 579	breqtrrd 4681	1 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 ∧ w3a 1037 = wceq 1483 Ⅎwnf 1708 ∈ wcel 1990 Ⅎwnfc 2751 ≠ wne 2794 ∀wral 2912 {crab 2916 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 class class class wbr 4653 ↦ cmpt 4729 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 Fincfn 7955 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 ≤ cle 10075 − cmin 10266 -cneg 10267 / cdiv 10684 ℕcn 11020 2c2 11070 3c3 11071 4c4 11072 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 ...cfz 12326 #chash 13117 Σcsu 14416

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-n0 11293 df-z 11378 df-uz 11688 df-rp 11833 df-ico 12181 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417

This theorem is referenced by: stoweidlem34 40251

W3C validator