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 46605

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 represent 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 11183	. . . . . . . 8 ⊢ 1 ∈ ℝ
2		eleq1 2852	. . . . . . . 8 ⊢ (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
3	1, 2	mpbiri 260	. . . . . . 7 ⊢ (𝐿 = 1 → 𝐿 ∈ ℝ)
4	3	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℝ)
5		4re 12304	. . . . . . . 8 ⊢ 4 ∈ ℝ
6	5	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 4 ∈ ℝ)
7		3re 12300	. . . . . . . 8 ⊢ 3 ∈ ℝ
8	7	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ∈ ℝ)
9		3ne0 12329	. . . . . . . 8 ⊢ 3 ≠ 0
10	9	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ≠ 0)
11	6, 8, 10	redivcld 12021	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈ ℝ)
12	4, 11	resubcld 11617	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
13		stoweidlem26.11	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
14	13	rpred 13039	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ)
15	14	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐸 ∈ ℝ)
16	12, 15	remulcld 11214	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
17		0red 11186	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ∈ ℝ)
18		fzfid 13988	. . . . . 6 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
19	14	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
20		stoweidlem26.13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ)
21		stoweidlem26.9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))))
22		eldif 3916	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
23	21, 22	sylib 220	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
24	23	simpld 498	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝐷‘𝐿))
25		stoweidlem26.4	. . . . . . . . . . . . 13 ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
26		oveq1 7405	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3)))
27	26	oveq1d 7413	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸))
28	27	breq2d 5114	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐿 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
29	28	rabbidv 3423	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐿 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
30		fz1ssfz0 13630	. . . . . . . . . . . . . 14 ⊢ (1...𝑁) ⊆ (0...𝑁)
31		stoweidlem26.8	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))
32	30, 31	sselid 3936	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ (0...𝑁))
33		stoweidlem26.7	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ V)
34		rabexg 5295	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
35	33, 34	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
36	25, 29, 32, 35	fvmptd3 7001	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘𝐿) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
37	24, 36	eleqtrd 2866	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
38		nfcv 2926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝑆
39		nfcv 2926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝑇
40		stoweidlem26.1	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡𝐹
41	40, 38	nffv 6879	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡(𝐹‘𝑆)
42		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡 ≤
43		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝐿 − (1 / 3)) · 𝐸)
44	41, 42, 43	nfbr 5149	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡(𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)
45		fveq2 6869	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (𝐹‘𝑡) = (𝐹‘𝑆))
46	45	breq1d 5112	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
47	38, 39, 44, 46	elrabf 3649	. . . . . . . . . . 11 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
48	37, 47	sylib 220	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
49	48	simpld 498	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ 𝑇)
50	49	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑆 ∈ 𝑇)
51	20, 50	ffvelcdmd 7068	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
52	19, 51	remulcld 11214	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
53	18, 52	fsumrecl 15763	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
54	53	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
55	5, 7, 9	redivcli 11960	. . . . . . 7 ⊢ (4 / 3) ∈ ℝ
56	55	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈ ℝ)
57	4, 56	resubcld 11617	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
58	4	recnd 11212	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℂ)
59	58	subid1d 11533	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) = 𝐿)
60		3cn 12301	. . . . . . . . . 10 ⊢ 3 ∈ ℂ
61	60, 9	dividi 11926	. . . . . . . . 9 ⊢ (3 / 3) = 1
62		3lt4 12396	. . . . . . . . . 10 ⊢ 3 < 4
63		3pos 12328	. . . . . . . . . . 11 ⊢ 0 < 3
64	7, 5, 7, 63	ltdiv1ii 12123	. . . . . . . . . 10 ⊢ (3 < 4 ↔ (3 / 3) < (4 / 3))
65	62, 64	mpbi 232	. . . . . . . . 9 ⊢ (3 / 3) < (4 / 3)
66	61, 65	eqbrtrri 5125	. . . . . . . 8 ⊢ 1 < (4 / 3)
67		breq1 5105	. . . . . . . . 9 ⊢ (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
68	67	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
69	66, 68	mpbiri 260	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 < (4 / 3))
70	59, 69	eqbrtrd 5124	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) < (4 / 3))
71	4, 17, 56, 70	ltsub23d 11794	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) < 0)
72	13	rpgt0d 13042	. . . . . 6 ⊢ (𝜑 → 0 < 𝐸)
73	72	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 < 𝐸)
74		mulltgt0 45607	. . . . 5 ⊢ ((((𝐿 − (4 / 3)) ∈ ℝ ∧ (𝐿 − (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
75	57, 71, 15, 73, 74	syl22anc 849	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
76		0cn 11173	. . . . . . . 8 ⊢ 0 ∈ ℂ
77		fsumconst 15819	. . . . . . . 8 ⊢ (((0...𝑁) ∈ Fin ∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
78	18, 76, 77	sylancl 595	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
79		hashcl 14371	. . . . . . . . 9 ⊢ ((0...𝑁) ∈ Fin → (♯‘(0...𝑁)) ∈ ℕ₀)
80		nn0cn 12493	. . . . . . . . 9 ⊢ ((♯‘(0...𝑁)) ∈ ℕ₀ → (♯‘(0...𝑁)) ∈ ℂ)
81	18, 79, 80	3syl 18	. . . . . . . 8 ⊢ (𝜑 → (♯‘(0...𝑁)) ∈ ℂ)
82	81	mul01d 11384	. . . . . . 7 ⊢ (𝜑 → ((♯‘(0...𝑁)) · 0) = 0)
83	78, 82	eqtrd 2799	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0)
84	83	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0)
85		0red 11186	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ)
86	13	rpge0d 13043	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝐸)
87	86	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸)
88		stoweidlem26.3	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝜑
89		nfv 1936	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑖 ∈ (0...𝑁)
90	88, 89	nfan 1921	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁))
91		nfv 1936	. . . . . . . . . . 11 ⊢ Ⅎ𝑡0 ≤ ((𝑋‘𝑖)‘𝑆)
92	90, 91	nfim 1918	. . . . . . . . . 10 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
93		fveq2 6869	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑆 → ((𝑋‘𝑖)‘𝑡) = ((𝑋‘𝑖)‘𝑆))
94	93	breq2d 5114	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑆 → (0 ≤ ((𝑋‘𝑖)‘𝑡) ↔ 0 ≤ ((𝑋‘𝑖)‘𝑆)))
95	94	imbi2d 342	. . . . . . . . . 10 ⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))))
96		stoweidlem26.14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡))
97	96	3expia 1135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 → 0 ≤ ((𝑋‘𝑖)‘𝑡)))
98	97	com12 32	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)))
99	38, 92, 95, 98	vtoclgaf 3542	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)))
100	50, 99	mpcom 38	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
101	19, 51, 87, 100	mulge0d 11766	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
102	18, 85, 52, 101	fsumle 15829	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
103	102	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
104	84, 103	eqbrtrrd 5126	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
105	16, 17, 54, 75, 104	ltletrd 11345	. . 3 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
106		elfzelz 13531	. . . . . . . . 9 ⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ)
107		zre 12574	. . . . . . . . 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 12021	. . . . . . . 8 ⊢ (𝜑 → (4 / 3) ∈ ℝ)
113	108, 112	resubcld 11617	. . . . . . 7 ⊢ (𝜑 → (𝐿 − (4 / 3)) ∈ ℝ)
114	113, 14	remulcld 11214	. . . . . 6 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
115	114	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
116	1	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℝ)
117		stoweidlem26.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
118	14, 117	nndivred 12269	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
119	116, 118	resubcld 11617	. . . . . . . 8 ⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ)
120	108, 116	resubcld 11617	. . . . . . . 8 ⊢ (𝜑 → (𝐿 − 1) ∈ ℝ)
121	119, 120	remulcld 11214	. . . . . . 7 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
122	14, 121	remulcld 11214	. . . . . 6 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
123	122	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
124		fzfid 13988	. . . . . . . 8 ⊢ (𝜑 → (0...(𝐿 − 2)) ∈ Fin)
125	31	elfzelzd 13532	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℤ)
126		2z 12605	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
127	126	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℤ)
128	125, 127	zsubcld 12684	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 2) ∈ ℤ)
129	117	nnzd 12596	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
130	125	zred 12679	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿 ∈ ℝ)
131		2re 12294	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
132	131	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℝ)
133	130, 132	resubcld 11617	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ∈ ℝ)
134	117	nnred 12227	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ)
135		0le2 12322	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 2
136		0red 11186	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
137	136, 132, 130	lesub2d 11797	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0)))
138	135, 137	mpbii 235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0))
139	125	zcnd 12680	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐿 ∈ ℂ)
140	139	subid1d 11533	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 0) = 𝐿)
141	138, 140	breqtrd 5128	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ≤ 𝐿)
142		elfzle2 13535	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ≤ 𝑁)
143	31, 142	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ≤ 𝑁)
144	133, 130, 134, 141, 143	letrd 11342	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 2) ≤ 𝑁)
145	128, 129, 144	3jca 1142	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
146		eluz2 12847	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
147	145, 146	sylibr 236	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝐿 − 2)))
148		fzss2 13571	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
149	147, 148	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁))
150	149	sselda 3938	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
151	150, 51	syldan 600	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
152	124, 151	fsumrecl 15763	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ)
153	14, 152	remulcld 11214	. . . . . 6 ⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
154	153	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
155	14, 120	remulcld 11214	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · (𝐿 − 1)) ∈ ℝ)
156	14, 14	remulcld 11214	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
157	155, 156	resubcld 11617	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ)
158	120, 117	nndivred 12269	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ)
159	156, 158	remulcld 11214	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ)
160	155, 159	resubcld 11617	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ)
161	120, 14	resubcld 11617	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ)
162	116, 14	readdcld 11213	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 + 𝐸) ∈ ℝ)
163	1, 7, 9	redivcli 11960	. . . . . . . . . . . . . . 15 ⊢ (1 / 3) ∈ ℝ
164	163	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 3) ∈ ℝ)
165		stoweidlem26.12	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 < (1 / 3))
166	14, 164, 116, 165	ltadd2dd 11344	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 + 𝐸) < (1 + (1 / 3)))
167		ax-1cn 11133	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
168	60, 167, 60, 9	divdiri 11950	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
169		3p1e4 12364	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
170	169	oveq1i 7408	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) / 3) = (4 / 3)
171	61	oveq1i 7408	. . . . . . . . . . . . . 14 ⊢ ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
172	168, 170, 171	3eqtr3ri 2796	. . . . . . . . . . . . 13 ⊢ (1 + (1 / 3)) = (4 / 3)
173	166, 172	breqtrdi 5143	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 + 𝐸) < (4 / 3))
174	162, 112, 108, 173	ltsub2dd 11802	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸)))
175	167	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
176	13	rpcnd 13041	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ ℂ)
177	139, 175, 176	subsub4d 11575	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸)))
178	174, 177	breqtrrd 5130	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸))
179	113, 161, 13, 178	ltmul1dd 13094	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸))
180	139, 175	subcld 11544	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 − 1) ∈ ℂ)
181	180, 176	subcld 11544	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ)
182	176, 181	mulcomd 11205	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸))
183	176, 180, 176	subdid 11645	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
184	182, 183	eqtr3d 2801	. . . . . . . . 9 ⊢ (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
185	179, 184	breqtrd 5128	. . . . . . . 8 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
186		1zzd 12604	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℤ)
187		elfz 13520	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)))
188	125, 186, 129, 187	syl3anc 1392	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)))
189	31, 188	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁))
190	189	simprd 499	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ≤ 𝑁)
191		zlem1lt 12625	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁))
192	125, 129, 191	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁))
193	190, 192	mpbid 234	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 1) < 𝑁)
194	117	nngt0d 12264	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝑁)
195		ltdiv1 12058	. . . . . . . . . . . . . 14 ⊢ (((𝐿 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
196	120, 134, 134, 194, 195	syl112anc 1395	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
197	193, 196	mpbid 234	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))
198	117	nncnd 12228	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
199	117	nnne0d 12265	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
200	198, 199	dividd 11967	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / 𝑁) = 1)
201	197, 200	breqtrd 5128	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < 1)
202	14, 14, 72, 72	mulgt0d 11340	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (𝐸 · 𝐸))
203		ltmul2 12044	. . . . . . . . . . . 12 ⊢ ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 < (𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
204	158, 116, 156, 202, 203	syl112anc 1395	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
205	201, 204	mpbid 234	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))
206	176, 176	mulcld 11204	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℂ)
207	206	mulridd 11201	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸))
208	205, 207	breqtrd 5128	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸))
209	159, 156, 155, 208	ltsub2dd 11802	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
210	114, 157, 160, 185, 209	lttrd 11346	. . . . . . 7 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
211	176, 198, 199	divcld 11969	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
212	175, 211, 180	subdird 11646	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))))
213	180	mullidd 11202	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1))
214	213	oveq1d 7413	. . . . . . . . . 10 ⊢ (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
215	212, 214	eqtrd 2799	. . . . . . . . 9 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
216	215	oveq2d 7414	. . . . . . . 8 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))))
217	211, 180	mulcld 11204	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈ ℂ)
218	176, 180, 217	subdid 11645	. . . . . . . 8 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))))
219	176, 198, 180, 199	div32d 11992	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁)))
220	219	oveq2d 7414	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
221	180, 198, 199	divcld 11969	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ)
222	176, 176, 221	mulassd 11207	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
223	220, 222	eqtr4d 2802	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))
224	223	oveq2d 7414	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
225	216, 218, 224	3eqtrd 2803	. . . . . . 7 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
226	210, 225	breqtrrd 5130	. . . . . 6 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
227	226	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
228	175, 211	subcld 11544	. . . . . . . . . 10 ⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ)
229		fsumconst 15819	. . . . . . . . . 10 ⊢ (((0...(𝐿 − 2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
230	124, 228, 229	syl2anc 593	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
231	230	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
232		0zd 12582	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℤ)
233	31	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁))
234	233	elfzelzd 13532	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ)
235	126	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℤ)
236	234, 235	zsubcld 12684	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ)
237		elnnuz 12881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
238	117, 237	sylib 220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
239		elfzp12 13610	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
240	238, 239	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
241	31, 240	mpbid 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
242	241	orcanai 1016	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁))
243		1p1e2 12343	. . . . . . . . . . . . . . . . . 18 ⊢ (1 + 1) = 2
244	243	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2)
245	244	oveq1d 7413	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁))
246	242, 245	eleqtrd 2866	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁))
247		elfzle1 13534	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿)
248	246, 247	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿)
249	108	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ)
250	131	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℝ)
251	249, 250	subge0d 11779	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿))
252	248, 251	mpbird 259	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2))
253	232, 236, 252	3jca 1142	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
254		eluz2 12847	. . . . . . . . . . . 12 ⊢ ((𝐿 − 2) ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
255	253, 254	sylibr 236	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (ℤ_≥‘0))
256		hashfz 14442	. . . . . . . . . . 11 ⊢ ((𝐿 − 2) ∈ (ℤ_≥‘0) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
257	255, 256	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
258		2cn 12295	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
259	258	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
260	139, 259	subcld 11544	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ∈ ℂ)
261	260	subid1d 11533	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2))
262	261	oveq1d 7413	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) + 1))
263	139, 259, 175	subadd23d 11566	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2)))
264	258, 167	negsubdi2i 11519	. . . . . . . . . . . . . . . 16 ⊢ -(2 − 1) = (1 − 2)
265		2m1e1 12344	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) = 1
266	265	negeqi 11425	. . . . . . . . . . . . . . . 16 ⊢ -(2 − 1) = -1
267	264, 266	eqtr3i 2789	. . . . . . . . . . . . . . 15 ⊢ (1 − 2) = -1
268	267	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 − 2) = -1)
269	268	oveq2d 7414	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1))
270	139, 175	negsubd 11550	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 + -1) = (𝐿 − 1))
271	269, 270	eqtrd 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1))
272	262, 263, 271	3eqtrd 2803	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
273	272	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
274	257, 273	eqtrd 2799	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (𝐿 − 1))
275	274	oveq1d 7413	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁))))
276	180, 228	mulcomd 11205	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
277	276	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
278	231, 275, 277	3eqtrd 2803	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
279		fzfid 13988	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin)
280		fzn0 13545	. . . . . . . . 9 ⊢ ((0...(𝐿 − 2)) ≠ ∅ ↔ (𝐿 − 2) ∈ (ℤ_≥‘0))
281	255, 280	sylibr 236	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅)
282	119	ad2antrr 736	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ)
283		simpll 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑)
284	150	adantlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
285	283, 284, 51	syl2anc 593	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
286	49	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ 𝑇)
287		elfzelz 13531	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ)
288	287	zred 12679	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ)
289	288	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ)
290	163	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈ ℝ)
291	289, 290	readdcld 11213	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ)
292	14	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ)
293	291, 292	remulcld 11214	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ)
294	108	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ)
295	131	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈ ℝ)
296	294, 295	resubcld 11617	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
297	296, 290	readdcld 11213	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
298	297, 292	remulcld 11214	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
299		stoweidlem26.10	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
300	299, 49	jca 519	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇))
301	300	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇))
302		ffvelcdm 7064	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇) → (𝐹‘𝑆) ∈ ℝ)
303	301, 302	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹‘𝑆) ∈ ℝ)
304		elfzle2 13535	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2))
305	304	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2))
306	289, 296, 290, 305	leadd1dd 11803	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)))
307	14, 72	jca 519	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
308	307	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
309		lemul1 12045	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 − 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
310	291, 297, 308, 309	syl3anc 1392	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
311	306, 310	mpbid 234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))
312	108, 132	resubcld 11617	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 − 2) ∈ ℝ)
313	312, 164	readdcld 11213	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
314	313, 14	remulcld 11214	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
315	299, 49	ffvelcdmd 7068	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ)
316	120, 164	resubcld 11617	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈ ℝ)
317	316, 14	remulcld 11214	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈ ℝ)
318		addrid 11365	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1 ∈ ℂ → (1 + 0) = 1)
319	318	eqcomd 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 ∈ ℂ → 1 = (1 + 0))
320	167, 319	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 1 = (1 + 0))
321	175	subidd 11532	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 − 1) = 0)
322	321	eqcomd 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 = (1 − 1))
323	322	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + 0) = (1 + (1 − 1)))
324		addsubass 11442	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1) − 1) = (1 + (1 − 1)))
325	324	eqcomd 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1 − 1)) = ((1 + 1) − 1))
326	175, 175, 175, 325	syl3anc 1392	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + (1 − 1)) = ((1 + 1) − 1))
327	320, 323, 326	3eqtrd 2803	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 1 = ((1 + 1) − 1))
328	327	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) − 1)))
329	243	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + 1) = 2)
330	329	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 + 1) − 1) = (2 − 1))
331	330	oveq2d 7414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 − 1)))
332	139, 259, 175	subsubd 11572	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) + 1))
333	328, 331, 332	3eqtrd 2803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1))
334	333	oveq1d 7413	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 / 3)))
335	258, 60, 9	divcli 11935	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 / 3) ∈ ℂ
336	335	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2 / 3) ∈ ℂ)
337	260, 175, 336	addsubassd 11564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 / 3))))
338	167, 60, 9	divcli 11935	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 / 3) ∈ ℂ
339		df-3 12283	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 3 = (2 + 1)
340	339	oveq1i 7408	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (3 / 3) = ((2 + 1) / 3)
341	258, 167, 60, 9	divdiri 11950	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
342	340, 61, 341	3eqtr3ri 2796	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 / 3) + (1 / 3)) = 1
343	167, 335, 338, 342	subaddrii 11522	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − (2 / 3)) = (1 / 3)
344	343	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 − (2 / 3)) = (1 / 3))
345	344	oveq2d 7414	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 / 3)))
346	334, 337, 345	3eqtrd 2803	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 / 3)))
347	131, 7, 9	redivcli 11960	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 / 3) ∈ ℝ
348	347	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2 / 3) ∈ ℝ)
349		1lt2 12392	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 < 2
350	7, 63	pm3.2i 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (3 ∈ ℝ ∧ 0 < 3)
351	1, 131, 350	3pm3.2i 1354	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
352		ltdiv1 12058	. . . . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 / 3) < (2 / 3))
355	164, 348, 120, 354	ltsub2dd 11802	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 / 3)))
356	346, 355	eqbrtrrd 5126	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 / 3)))
357	313, 316, 13, 356	ltmul1dd 13094	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸))
358	23	simprd 499	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))
359		oveq1 7405	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 / 3)))
360	359	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸))
361	360	breq2d 5114	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = (𝐿 − 1) → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
362	361	rabbidv 3423	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝐿 − 1) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
363	129	peano2zd 12682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
364	189	simpld 498	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 1 ≤ 𝐿)
365	134, 116	readdcld 11213	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
366	134	lep1d 12125	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
367	108, 134, 365, 190, 366	letrd 11342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐿 ≤ (𝑁 + 1))
368	186, 363, 125, 364, 367	elfzd 13522	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐿 ∈ (1...(𝑁 + 1)))
369	139, 175	npcand 11548	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐿 − 1) + 1) = 𝐿)
370		0p1e1 12340	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 + 1) = 1
371	370	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (0 + 1) = 1)
372	371	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
373	368, 369, 372	3eltr4d 2879	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
374		0zd 12582	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℤ)
375	125, 186	zsubcld 12684	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐿 − 1) ∈ ℤ)
376		fzaddel 13565	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐿 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
377	374, 129, 375, 186, 376	syl22anc 849	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
378	373, 377	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐿 − 1) ∈ (0...𝑁))
379		rabexg 5295	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
380	33, 379	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
381	25, 362, 378, 380	fvmptd3 7001	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
382	358, 381	neleqtrd 2886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
383		nfcv 2926	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸)
384	41, 42, 383	nfbr 5149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)
385	45	breq1d 5112	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
386	38, 39, 384, 385	elrabf 3649	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
387	382, 386	sylnib 330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
388		ianor 995	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
389	387, 388	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
390		olc 879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ 𝑇 → (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇))
391	390	anim1i 624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑇 ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
392	49, 389, 391	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
393		orcom 881	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))
394	393	anbi2i 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
395	392, 394	sylib 220	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
396		pm4.43 1036	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
397	395, 396	sylibr 236	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))
398	317, 315	ltnled 11332	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆) ↔ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
399	397, 398	mpbird 259	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆))
400	314, 317, 315, 357, 399	lttrd 11346	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹‘𝑆))
401	314, 315, 400	ltled 11333	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
402	401	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
403	293, 298, 303, 311, 402	letrd 11342	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
404		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸)
405	404, 42, 41	nfbr 5149	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)
406	45	breq2d 5114	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)))
407	38, 39, 405, 406	elrabf 3649	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑆 ∈ 𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)))
408	286, 403, 407	sylanbrc 592	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
409		stoweidlem26.5	. . . . . . . . . . . 12 ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
410		oveq1 7405	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
411	410	oveq1d 7413	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸))
412	411	breq1d 5112	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
413	412	rabbidv 3423	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑖 → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
414		rabexg 5295	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
415	33, 414	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
416	415	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
417	409, 413, 150, 416	fvmptd3 7001	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐵‘𝑖) = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
418	408, 417	eleqtrrd 2867	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵‘𝑖))
419	145	3ad2ant1 1147	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
420	419, 146	sylibr 236	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑁 ∈ (ℤ_≥‘(𝐿 − 2)))
421	420, 148	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
422		simp2 1151	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...(𝐿 − 2)))
423	421, 422	sseldd 3939	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...𝑁))
424		elex 3477	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (𝐵‘𝑖) → 𝑆 ∈ V)
425	424	3ad2ant3 1149	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑆 ∈ V)
426		nfcv 2926	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡(0...𝑁)
427		nfrab1 3436	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
428	426, 427	nfmpt 5200	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
429	409, 428	nfcxfr 2924	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝐵
430		nfcv 2926	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝑖
431	429, 430	nffv 6879	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝐵‘𝑖)
432	431	nfel2 2944	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡 𝑆 ∈ (𝐵‘𝑖)
433	88, 89, 432	nf3an 1923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖))
434		nfv 1936	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)
435	433, 434	nfim 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
436		eleq1 2852	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑆 → (𝑡 ∈ (𝐵‘𝑖) ↔ 𝑆 ∈ (𝐵‘𝑖)))
437	436	3anbi3d 1465	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑆 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖))))
438	93	breq2d 5114	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))
439	437, 438	imbi12d 346	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))))
440		stoweidlem26.15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡))
441	435, 439, 440	vtoclg1f 3537	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ V → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))
442	425, 441	mpcom 38	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
443	423, 442	syld3an2 1432	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
444	418, 443	mpd3an3 1485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
445	444	adantlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
446	279, 281, 282, 285, 445	fsumlt 15830	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))
447	278, 446	eqbrtrrd 5126	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))
448	121	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
449	152	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ)
450	307	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
451		ltmul2 12044	. . . . . . 7 ⊢ ((((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))))
452	448, 449, 450, 451	syl3anc 1392	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))))
453	447, 452	mpbid 234	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))
454	115, 123, 154, 227, 453	lttrd 11346	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))
455	150, 52	syldan 600	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
456	455	adantlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
457	456	recnd 11212	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
458	279, 457	fsumcl 15762	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
459	458	addridd 11385	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
460		0red 11186	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℝ)
461		fzfid 13988	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin)
462	14	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ)
463		0zd 12582	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ)
464	129	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ)
465		elfzelz 13531	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ)
466	465	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ)
467		0red 11186	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ)
468	120	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ)
469	465	zred 12679	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ)
470	469	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ)
471		1m1e0 12292	. . . . . . . . . . . . . . 15 ⊢ (1 − 1) = 0
472	116, 108, 116, 364	lesub1dd 11805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 − 1) ≤ (𝐿 − 1))
473	471, 472	eqbrtrrid 5138	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (𝐿 − 1))
474	473	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1))
475		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁))
476	375	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ)
477		elfz 13520	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
478	466, 476, 464, 477	syl3anc 1392	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
479	475, 478	mpbid 234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))
480	479	simpld 498	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖)
481	467, 468, 470, 474, 480	letrd 11342	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖)
482		elfzle2 13535	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ≤ 𝑁)
483	482	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ≤ 𝑁)
484	463, 464, 466, 481, 483	elfzd 13522	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁))
485	484, 51	syldan 600	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
486	462, 485	remulcld 11214	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
487	486	adantlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
488	461, 487	fsumrecl 15763	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
489	279, 456	fsumrecl 15763	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
490		fzfid 13988	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin)
491	176	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ)
492	491	mul01d 11384	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0)
493	484, 100	syldan 600	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
494	307	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
495		lemul2 12046	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ ((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))))
496	467, 485, 494, 495	syl3anc 1392	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))))
497	493, 496	mpbid 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
498	492, 497	eqbrtrrd 5126	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
499	490, 486, 498	fsumge0 15825	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
500	499	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
501	460, 488, 489, 500	leadd2dd 11804	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
502	459, 501	eqbrtrrd 5126	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
503	151	recnd 11212	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ)
504	124, 176, 503	fsummulc2 15813	. . . . . 6 ⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
505	504	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
506		stoweidlem26.2	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
507		elfzelz 13531	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ)
508	507	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ)
509	508	zred 12679	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ)
510	312	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
511	120	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ)
512		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2)))
513		0zd 12582	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈ ℤ)
514	128	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ)
515		elfz 13520	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))))
516	508, 513, 514, 515	syl3anc 1392	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))))
517	512, 516	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2)))
518	517	simprd 499	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2))
519	116, 132, 108	ltsub2d 11799	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1)))
520	349, 519	mpbii 235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 2) < (𝐿 − 1))
521	520	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1))
522	509, 510, 511, 518, 521	lelttrd 11343	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1))
523	509, 511	ltnled 11332	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗))
524	522, 523	mpbid 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗)
525	524	intnanrd 493	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))
526	375	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ)
527	129	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ)
528		elfz 13520	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
529	508, 526, 527, 528	syl3anc 1392	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
530	525, 529	mtbird 327	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
531	530	ex 416	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)))
532	506, 531	ralrimi 3262	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
533		disj 4406	. . . . . . . 8 ⊢ (((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅ ↔ ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
534	532, 533	sylibr 236	. . . . . . 7 ⊢ (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
535	534	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
536	144	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁)
537	128, 374, 129	3jca 1142	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
538	537	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
539		elfz 13520	. . . . . . . . . 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 723	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁))
542		fzsplit 13557	. . . . . . . 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 2803	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1))
545	544	oveq1d 7413	. . . . . . . . 9 ⊢ (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁))
546	545	uneq2d 4123	. . . . . . . 8 ⊢ (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
547	546	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
548	543, 547	eqtrd 2799	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
549		fzfid 13988	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin)
550	176	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
551	51	recnd 11212	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ)
552	550, 551	mulcld 11204	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
553	552	adantlr 725	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
554	535, 548, 549, 553	fsumsplit 15770	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
555	502, 505, 554	3brtr4d 5134	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
556	114, 153, 53	3jca 1142	. . . . . 6 ⊢ (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ))
557	556	adantr 484	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ))
558		ltletr 11277	. . . . 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 709	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
561	105, 560	pm2.61dan 822	. 2 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
562		sumex 15717	. . 3 ⊢ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V
563	93	oveq2d 7414	. . . . 5 ⊢ (𝑡 = 𝑆 → (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘𝑖)‘𝑆)))
564	563	sumeq2sdv 15732	. . . 4 ⊢ (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
565		eqid 2764	. . . 4 ⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))
566	564, 565	fvmptg 6975	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
567	49, 562, 566	sylancl 595	. 2 ⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
568	561, 567	breqtrrd 5130	1 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∧ w3a 1099 = wceq 1562 Ⅎwnf 1805 ∈ wcel 2144 Ⅎwnfc 2911 ≠ wne 2959 ∀wral 3078 {crab 3416 Vcvv 3456 ∖ cdif 3903 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4287 class class class wbr 5102 ↦ cmpt 5183 ⟶wf 6519 ‘cfv 6523 (class class class)co 7398 Fincfn 8929 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 + caddc 11078 · cmul 11080 < clt 11218 ≤ cle 11219 − cmin 11416 -cneg 11417 / cdiv 11846 ℕcn 12212 2c2 12274 3c3 12275 4c4 12276 ℕ₀cn0 12483 ℤcz 12570 ℤ_≥cuz 12841 ℝ⁺crp 12995 ...cfz 13514 ♯chash 14345 Σcsu 15715

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-rep 5229 ax-sep 5248 ax-nul 5258 ax-pow 5324 ax-pr 5392 ax-un 7720 ax-inf2 9598 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5544 df-eprel 5549 df-po 5557 df-so 5558 df-fr 5602 df-se 5603 df-we 5604 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-pred 6290 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-isom 6532 df-riota 7355 df-ov 7401 df-oprab 7402 df-mpo 7403 df-om 7849 df-1st 7972 df-2nd 7973 df-frecs 8264 df-wrecs 8295 df-recs 8344 df-rdg 8383 df-1o 8439 df-er 8680 df-en 8930 df-dom 8931 df-sdom 8932 df-fin 8933 df-sup 9390 df-oi 9460 df-card 9899 df-pnf 11220 df-mnf 11221 df-xr 11222 df-ltxr 11223 df-le 11224 df-sub 11418 df-neg 11419 df-div 11847 df-nn 12213 df-2 12282 df-3 12283 df-4 12284 df-n0 12484 df-z 12571 df-uz 12842 df-rp 12996 df-ico 13357 df-fz 13515 df-fzo 13662 df-seq 14017 df-exp 14077 df-hash 14346 df-cj 15128 df-re 15129 df-im 15130 df-sqrt 15264 df-abs 15265 df-clim 15517 df-sum 15716

This theorem is referenced by: stoweidlem34 46613

W3C validator