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 47035

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 11308	. . . . . . . 8 ⊢ 1 ∈ ℝ
2		eleq1 2849	. . . . . . . 8 ⊢ (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
3	1, 2	mpbiri 261	. . . . . . 7 ⊢ (𝐿 = 1 → 𝐿 ∈ ℝ)
4	3	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℝ)
5		4re 12427	. . . . . . . 8 ⊢ 4 ∈ ℝ
6	5	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 4 ∈ ℝ)
7		3re 12423	. . . . . . . 8 ⊢ 3 ∈ ℝ
8	7	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ∈ ℝ)
9		3ne0 12452	. . . . . . . 8 ⊢ 3 ≠ 0
10	9	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ≠ 0)
11	6, 8, 10	redivcld 12145	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈ ℝ)
12	4, 11	resubcld 11744	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
13		stoweidlem26.11	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
14	13	rpred 13164	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ)
15	14	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐸 ∈ ℝ)
16	12, 15	remulcld 11339	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
17		0red 11311	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ∈ ℝ)
18		fzfid 14116	. . . . . 6 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
19	14	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
20		stoweidlem26.13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ)
21		stoweidlem26.9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))))
22		eldif 3909	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
23	21, 22	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
24	23	simpld 500	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝐷‘𝐿))
25		stoweidlem26.4	. . . . . . . . . . . . 13 ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
26		oveq1 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3)))
27	26	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸))
28	27	breq2d 5115	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐿 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
29	28	rabbidv 3420	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐿 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
30		fz1ssfz0 13757	. . . . . . . . . . . . . 14 ⊢ (1...𝑁) ⊆ (0...𝑁)
31		stoweidlem26.8	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))
32	30, 31	sselid 3929	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ (0...𝑁))
33		stoweidlem26.7	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ V)
34		rabexg 5299	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
35	33, 34	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
36	25, 29, 32, 35	fvmptd3 7017	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘𝐿) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
37	24, 36	eleqtrd 2863	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
38		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝑆
39		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝑇
40		stoweidlem26.1	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡𝐹
41	40, 38	nffv 6895	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡(𝐹‘𝑆)
42		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡 ≤
43		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝐿 − (1 / 3)) · 𝐸)
44	41, 42, 43	nfbr 5152	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡(𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)
45		fveq2 6885	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (𝐹‘𝑡) = (𝐹‘𝑆))
46	45	breq1d 5113	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
47	38, 39, 44, 46	elrabf 3642	. . . . . . . . . . 11 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
48	37, 47	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
49	48	simpld 500	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ 𝑇)
50	49	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑆 ∈ 𝑇)
51	20, 50	ffvelcdmd 7085	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
52	19, 51	remulcld 11339	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
53	18, 52	fsumrecl 15900	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
54	53	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
55	5, 7, 9	redivcli 12084	. . . . . . 7 ⊢ (4 / 3) ∈ ℝ
56	55	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈ ℝ)
57	4, 56	resubcld 11744	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
58	4	recnd 11337	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℂ)
59	58	subid1d 11658	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) = 𝐿)
60		3cn 12424	. . . . . . . . . 10 ⊢ 3 ∈ ℂ
61	60, 9	dividi 12050	. . . . . . . . 9 ⊢ (3 / 3) = 1
62		3lt4 12519	. . . . . . . . . 10 ⊢ 3 < 4
63		3pos 12451	. . . . . . . . . . 11 ⊢ 0 < 3
64	7, 5, 7, 63	ltdiv1ii 12246	. . . . . . . . . 10 ⊢ (3 < 4 ↔ (3 / 3) < (4 / 3))
65	62, 64	mpbi 233	. . . . . . . . 9 ⊢ (3 / 3) < (4 / 3)
66	61, 65	eqbrtrri 5128	. . . . . . . 8 ⊢ 1 < (4 / 3)
67		breq1 5106	. . . . . . . . 9 ⊢ (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
68	67	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
69	66, 68	mpbiri 261	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 < (4 / 3))
70	59, 69	eqbrtrd 5127	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) < (4 / 3))
71	4, 17, 56, 70	ltsub23d 11921	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) < 0)
72	13	rpgt0d 13167	. . . . . 6 ⊢ (𝜑 → 0 < 𝐸)
73	72	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 < 𝐸)
74		mulltgt0 46038	. . . . 5 ⊢ ((((𝐿 − (4 / 3)) ∈ ℝ ∧ (𝐿 − (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
75	57, 71, 15, 73, 74	syl22anc 852	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
76		0cn 11298	. . . . . . . 8 ⊢ 0 ∈ ℂ
77		fsumconst 15956	. . . . . . . 8 ⊢ (((0...𝑁) ∈ Fin ∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
78	18, 76, 77	sylancl 598	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
79		hashcl 14500	. . . . . . . . 9 ⊢ ((0...𝑁) ∈ Fin → (♯‘(0...𝑁)) ∈ ℕ₀)
80		nn0cn 12616	. . . . . . . . 9 ⊢ ((♯‘(0...𝑁)) ∈ ℕ₀ → (♯‘(0...𝑁)) ∈ ℂ)
81	18, 79, 80	3syl 19	. . . . . . . 8 ⊢ (𝜑 → (♯‘(0...𝑁)) ∈ ℂ)
82	81	mul01d 11509	. . . . . . 7 ⊢ (𝜑 → ((♯‘(0...𝑁)) · 0) = 0)
83	78, 82	eqtrd 2796	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0)
84	83	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0)
85		0red 11311	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ)
86	13	rpge0d 13168	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝐸)
87	86	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸)
88		stoweidlem26.3	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝜑
89		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑖 ∈ (0...𝑁)
90	88, 89	nfan 1932	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁))
91		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑡0 ≤ ((𝑋‘𝑖)‘𝑆)
92	90, 91	nfim 1929	. . . . . . . . . 10 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
93		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑆 → ((𝑋‘𝑖)‘𝑡) = ((𝑋‘𝑖)‘𝑆))
94	93	breq2d 5115	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑆 → (0 ≤ ((𝑋‘𝑖)‘𝑡) ↔ 0 ≤ ((𝑋‘𝑖)‘𝑆)))
95	94	imbi2d 343	. . . . . . . . . 10 ⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))))
96		stoweidlem26.14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡))
97	96	3expia 1139	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 → 0 ≤ ((𝑋‘𝑖)‘𝑡)))
98	97	com12 33	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)))
99	38, 92, 95, 98	vtoclgaf 3536	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)))
100	50, 99	mpcom 39	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
101	19, 51, 87, 100	mulge0d 11893	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
102	18, 85, 52, 101	fsumle 15966	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
103	102	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
104	84, 103	eqbrtrrd 5129	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
105	16, 17, 54, 75, 104	ltletrd 11470	. . 3 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
106		elfzelz 13656	. . . . . . . . 9 ⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ)
107		zre 12697	. . . . . . . . 9 ⊢ (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
108	31, 106, 107	3syl 19	. . . . . . . 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 12145	. . . . . . . 8 ⊢ (𝜑 → (4 / 3) ∈ ℝ)
113	108, 112	resubcld 11744	. . . . . . 7 ⊢ (𝜑 → (𝐿 − (4 / 3)) ∈ ℝ)
114	113, 14	remulcld 11339	. . . . . 6 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
115	114	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
116	1	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℝ)
117		stoweidlem26.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
118	14, 117	nndivred 12392	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
119	116, 118	resubcld 11744	. . . . . . . 8 ⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ)
120	108, 116	resubcld 11744	. . . . . . . 8 ⊢ (𝜑 → (𝐿 − 1) ∈ ℝ)
121	119, 120	remulcld 11339	. . . . . . 7 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
122	14, 121	remulcld 11339	. . . . . 6 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
123	122	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
124		fzfid 14116	. . . . . . . 8 ⊢ (𝜑 → (0...(𝐿 − 2)) ∈ Fin)
125	31	elfzelzd 13657	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℤ)
126		2z 12728	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
127	126	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℤ)
128	125, 127	zsubcld 12808	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 2) ∈ ℤ)
129	117	nnzd 12719	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
130	125	zred 12803	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿 ∈ ℝ)
131		2re 12417	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
132	131	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℝ)
133	130, 132	resubcld 11744	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ∈ ℝ)
134	117	nnred 12350	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ)
135		0le2 12445	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 2
136		0red 11311	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
137	136, 132, 130	lesub2d 11924	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0)))
138	135, 137	mpbii 236	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0))
139	125	zcnd 12804	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐿 ∈ ℂ)
140	139	subid1d 11658	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 0) = 𝐿)
141	138, 140	breqtrd 5131	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ≤ 𝐿)
142		elfzle2 13661	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ≤ 𝑁)
143	31, 142	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ≤ 𝑁)
144	133, 130, 134, 141, 143	letrd 11467	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 2) ≤ 𝑁)
145	128, 129, 144	3jca 1146	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
146		eluz2 12971	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
147	145, 146	sylibr 237	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝐿 − 2)))
148		fzss2 13698	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
149	147, 148	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁))
150	149	sselda 3931	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
151	150, 51	syldan 603	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
152	124, 151	fsumrecl 15900	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ)
153	14, 152	remulcld 11339	. . . . . 6 ⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
154	153	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
155	14, 120	remulcld 11339	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · (𝐿 − 1)) ∈ ℝ)
156	14, 14	remulcld 11339	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
157	155, 156	resubcld 11744	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ)
158	120, 117	nndivred 12392	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ)
159	156, 158	remulcld 11339	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ)
160	155, 159	resubcld 11744	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ)
161	120, 14	resubcld 11744	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ)
162	116, 14	readdcld 11338	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 + 𝐸) ∈ ℝ)
163	1, 7, 9	redivcli 12084	. . . . . . . . . . . . . . 15 ⊢ (1 / 3) ∈ ℝ
164	163	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 3) ∈ ℝ)
165		stoweidlem26.12	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 < (1 / 3))
166	14, 164, 116, 165	ltadd2dd 11469	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 + 𝐸) < (1 + (1 / 3)))
167		ax-1cn 11258	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
168	60, 167, 60, 9	divdiri 12074	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
169		3p1e4 12487	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
170	169	oveq1i 7430	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) / 3) = (4 / 3)
171	61	oveq1i 7430	. . . . . . . . . . . . . 14 ⊢ ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
172	168, 170, 171	3eqtr3ri 2793	. . . . . . . . . . . . 13 ⊢ (1 + (1 / 3)) = (4 / 3)
173	166, 172	breqtrdi 5146	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 + 𝐸) < (4 / 3))
174	162, 112, 108, 173	ltsub2dd 11929	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸)))
175	167	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
176	13	rpcnd 13166	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ ℂ)
177	139, 175, 176	subsub4d 11700	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸)))
178	174, 177	breqtrrd 5133	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸))
179	113, 161, 13, 178	ltmul1dd 13219	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸))
180	139, 175	subcld 11669	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 − 1) ∈ ℂ)
181	180, 176	subcld 11669	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ)
182	176, 181	mulcomd 11330	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸))
183	176, 180, 176	subdid 11772	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
184	182, 183	eqtr3d 2798	. . . . . . . . 9 ⊢ (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
185	179, 184	breqtrd 5131	. . . . . . . 8 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
186		1zzd 12727	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℤ)
187		elfz 13645	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)))
188	125, 186, 129, 187	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)))
189	31, 188	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁))
190	189	simprd 501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ≤ 𝑁)
191		zlem1lt 12748	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁))
192	125, 129, 191	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁))
193	190, 192	mpbid 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 1) < 𝑁)
194	117	nngt0d 12387	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝑁)
195		ltdiv1 12181	. . . . . . . . . . . . . 14 ⊢ (((𝐿 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
196	120, 134, 134, 194, 195	syl112anc 1401	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
197	193, 196	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))
198	117	nncnd 12351	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
199	117	nnne0d 12388	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
200	198, 199	dividd 12091	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / 𝑁) = 1)
201	197, 200	breqtrd 5131	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < 1)
202	14, 14, 72, 72	mulgt0d 11465	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (𝐸 · 𝐸))
203		ltmul2 12168	. . . . . . . . . . . 12 ⊢ ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 < (𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
204	158, 116, 156, 202, 203	syl112anc 1401	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
205	201, 204	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))
206	176, 176	mulcld 11329	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℂ)
207	206	mulridd 11326	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸))
208	205, 207	breqtrd 5131	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸))
209	159, 156, 155, 208	ltsub2dd 11929	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
210	114, 157, 160, 185, 209	lttrd 11471	. . . . . . 7 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
211	176, 198, 199	divcld 12093	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
212	175, 211, 180	subdird 11773	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))))
213	180	mullidd 11327	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1))
214	213	oveq1d 7435	. . . . . . . . . 10 ⊢ (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
215	212, 214	eqtrd 2796	. . . . . . . . 9 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
216	215	oveq2d 7436	. . . . . . . 8 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))))
217	211, 180	mulcld 11329	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈ ℂ)
218	176, 180, 217	subdid 11772	. . . . . . . 8 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))))
219	176, 198, 180, 199	div32d 12116	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁)))
220	219	oveq2d 7436	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
221	180, 198, 199	divcld 12093	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ)
222	176, 176, 221	mulassd 11332	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
223	220, 222	eqtr4d 2799	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))
224	223	oveq2d 7436	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
225	216, 218, 224	3eqtrd 2800	. . . . . . 7 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
226	210, 225	breqtrrd 5133	. . . . . 6 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
227	226	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
228	175, 211	subcld 11669	. . . . . . . . . 10 ⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ)
229		fsumconst 15956	. . . . . . . . . 10 ⊢ (((0...(𝐿 − 2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
230	124, 228, 229	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
231	230	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
232		0zd 12705	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℤ)
233	31	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁))
234	233	elfzelzd 13657	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ)
235	126	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℤ)
236	234, 235	zsubcld 12808	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ)
237		elnnuz 13005	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
238	117, 237	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
239		elfzp12 13737	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
240	238, 239	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
241	31, 240	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
242	241	orcanai 1018	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁))
243		1p1e2 12466	. . . . . . . . . . . . . . . . . 18 ⊢ (1 + 1) = 2
244	243	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2)
245	244	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁))
246	242, 245	eleqtrd 2863	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁))
247		elfzle1 13660	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿)
248	246, 247	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿)
249	108	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ)
250	131	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℝ)
251	249, 250	subge0d 11906	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿))
252	248, 251	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2))
253	232, 236, 252	3jca 1146	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
254		eluz2 12971	. . . . . . . . . . . 12 ⊢ ((𝐿 − 2) ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
255	253, 254	sylibr 237	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (ℤ_≥‘0))
256		hashfz 14572	. . . . . . . . . . 11 ⊢ ((𝐿 − 2) ∈ (ℤ_≥‘0) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
257	255, 256	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
258		2cn 12418	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
259	258	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
260	139, 259	subcld 11669	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ∈ ℂ)
261	260	subid1d 11658	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2))
262	261	oveq1d 7435	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) + 1))
263	139, 259, 175	subadd23d 11691	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2)))
264	258, 167	negsubdi2i 11644	. . . . . . . . . . . . . . . 16 ⊢ -(2 − 1) = (1 − 2)
265		2m1e1 12467	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) = 1
266	265	negeqi 11550	. . . . . . . . . . . . . . . 16 ⊢ -(2 − 1) = -1
267	264, 266	eqtr3i 2786	. . . . . . . . . . . . . . 15 ⊢ (1 − 2) = -1
268	267	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 − 2) = -1)
269	268	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1))
270	139, 175	negsubd 11675	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 + -1) = (𝐿 − 1))
271	269, 270	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1))
272	262, 263, 271	3eqtrd 2800	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
273	272	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
274	257, 273	eqtrd 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (𝐿 − 1))
275	274	oveq1d 7435	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁))))
276	180, 228	mulcomd 11330	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
277	276	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
278	231, 275, 277	3eqtrd 2800	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
279		fzfid 14116	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin)
280		fzn0 13671	. . . . . . . . 9 ⊢ ((0...(𝐿 − 2)) ≠ ∅ ↔ (𝐿 − 2) ∈ (ℤ_≥‘0))
281	255, 280	sylibr 237	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅)
282	119	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ)
283		simpll 779	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑)
284	150	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
285	283, 284, 51	syl2anc 596	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
286	49	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ 𝑇)
287		elfzelz 13656	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ)
288	287	zred 12803	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ)
289	288	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ)
290	163	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈ ℝ)
291	289, 290	readdcld 11338	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ)
292	14	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ)
293	291, 292	remulcld 11339	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ)
294	108	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ)
295	131	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈ ℝ)
296	294, 295	resubcld 11744	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
297	296, 290	readdcld 11338	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
298	297, 292	remulcld 11339	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
299		stoweidlem26.10	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
300	299, 49	jca 521	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇))
301	300	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇))
302		ffvelcdm 7081	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇) → (𝐹‘𝑆) ∈ ℝ)
303	301, 302	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹‘𝑆) ∈ ℝ)
304		elfzle2 13661	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2))
305	304	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2))
306	289, 296, 290, 305	leadd1dd 11930	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)))
307	14, 72	jca 521	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
308	307	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
309		lemul1 12169	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 − 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
310	291, 297, 308, 309	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
311	306, 310	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))
312	108, 132	resubcld 11744	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 − 2) ∈ ℝ)
313	312, 164	readdcld 11338	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
314	313, 14	remulcld 11339	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
315	299, 49	ffvelcdmd 7085	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ)
316	120, 164	resubcld 11744	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈ ℝ)
317	316, 14	remulcld 11339	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈ ℝ)
318		addrid 11490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1 ∈ ℂ → (1 + 0) = 1)
319	318	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 ∈ ℂ → 1 = (1 + 0))
320	167, 319	mp1i 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 1 = (1 + 0))
321	175	subidd 11657	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 − 1) = 0)
322	321	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 = (1 − 1))
323	322	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + 0) = (1 + (1 − 1)))
324		addsubass 11567	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1) − 1) = (1 + (1 − 1)))
325	324	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1 − 1)) = ((1 + 1) − 1))
326	175, 175, 175, 325	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + (1 − 1)) = ((1 + 1) − 1))
327	320, 323, 326	3eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 1 = ((1 + 1) − 1))
328	327	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) − 1)))
329	243	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + 1) = 2)
330	329	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 + 1) − 1) = (2 − 1))
331	330	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 − 1)))
332	139, 259, 175	subsubd 11697	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) + 1))
333	328, 331, 332	3eqtrd 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1))
334	333	oveq1d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 / 3)))
335	258, 60, 9	divcli 12059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 / 3) ∈ ℂ
336	335	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2 / 3) ∈ ℂ)
337	260, 175, 336	addsubassd 11689	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 / 3))))
338	167, 60, 9	divcli 12059	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 / 3) ∈ ℂ
339		df-3 12406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 3 = (2 + 1)
340	339	oveq1i 7430	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (3 / 3) = ((2 + 1) / 3)
341	258, 167, 60, 9	divdiri 12074	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
342	340, 61, 341	3eqtr3ri 2793	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 / 3) + (1 / 3)) = 1
343	167, 335, 338, 342	subaddrii 11647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − (2 / 3)) = (1 / 3)
344	343	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 − (2 / 3)) = (1 / 3))
345	344	oveq2d 7436	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 / 3)))
346	334, 337, 345	3eqtrd 2800	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 / 3)))
347	131, 7, 9	redivcli 12084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 / 3) ∈ ℝ
348	347	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2 / 3) ∈ ℝ)
349		1lt2 12515	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 < 2
350	7, 63	pm3.2i 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (3 ∈ ℝ ∧ 0 < 3)
351	1, 131, 350	3pm3.2i 1358	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
352		ltdiv1 12181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (1 < 2 ↔ (1 / 3) < (2 / 3)))
353	351, 352	mp1i 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 < 2 ↔ (1 / 3) < (2 / 3)))
354	349, 353	mpbii 236	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 / 3) < (2 / 3))
355	164, 348, 120, 354	ltsub2dd 11929	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 / 3)))
356	346, 355	eqbrtrrd 5129	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 / 3)))
357	313, 316, 13, 356	ltmul1dd 13219	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸))
358	23	simprd 501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))
359		oveq1 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 / 3)))
360	359	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸))
361	360	breq2d 5115	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = (𝐿 − 1) → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
362	361	rabbidv 3420	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝐿 − 1) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
363	129	peano2zd 12806	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
364	189	simpld 500	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 1 ≤ 𝐿)
365	134, 116	readdcld 11338	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
366	134	lep1d 12248	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
367	108, 134, 365, 190, 366	letrd 11467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐿 ≤ (𝑁 + 1))
368	186, 363, 125, 364, 367	elfzd 13647	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐿 ∈ (1...(𝑁 + 1)))
369	139, 175	npcand 11673	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐿 − 1) + 1) = 𝐿)
370		0p1e1 12463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 + 1) = 1
371	370	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (0 + 1) = 1)
372	371	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
373	368, 369, 372	3eltr4d 2876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
374		0zd 12705	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℤ)
375	125, 186	zsubcld 12808	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐿 − 1) ∈ ℤ)
376		fzaddel 13692	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐿 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
377	374, 129, 375, 186, 376	syl22anc 852	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
378	373, 377	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐿 − 1) ∈ (0...𝑁))
379		rabexg 5299	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
380	33, 379	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
381	25, 362, 378, 380	fvmptd3 7017	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
382	358, 381	neleqtrd 2883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
383		nfcv 2923	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸)
384	41, 42, 383	nfbr 5152	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)
385	45	breq1d 5113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
386	38, 39, 384, 385	elrabf 3642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
387	382, 386	sylnib 331	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
388		ianor 997	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
389	387, 388	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
390		olc 882	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ 𝑇 → (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇))
391	390	anim1i 627	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑇 ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
392	49, 389, 391	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
393		orcom 884	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))
394	393	anbi2i 635	. . . . . . . . . . . . . . . . . . 19 ⊢ (((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
395	392, 394	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
396		pm4.43 1040	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
397	395, 396	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))
398	317, 315	ltnled 11457	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆) ↔ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
399	397, 398	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆))
400	314, 317, 315, 357, 399	lttrd 11471	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹‘𝑆))
401	314, 315, 400	ltled 11458	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
402	401	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
403	293, 298, 303, 311, 402	letrd 11467	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
404		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸)
405	404, 42, 41	nfbr 5152	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)
406	45	breq2d 5115	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)))
407	38, 39, 405, 406	elrabf 3642	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑆 ∈ 𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)))
408	286, 403, 407	sylanbrc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
409		stoweidlem26.5	. . . . . . . . . . . 12 ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
410		oveq1 7427	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
411	410	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸))
412	411	breq1d 5113	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
413	412	rabbidv 3420	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑖 → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
414		rabexg 5299	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
415	33, 414	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
416	415	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
417	409, 413, 150, 416	fvmptd3 7017	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐵‘𝑖) = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
418	408, 417	eleqtrrd 2864	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵‘𝑖))
419	145	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
420	419, 146	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑁 ∈ (ℤ_≥‘(𝐿 − 2)))
421	420, 148	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
422		simp2 1155	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...(𝐿 − 2)))
423	421, 422	sseldd 3932	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...𝑁))
424		elex 3472	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (𝐵‘𝑖) → 𝑆 ∈ V)
425	424	3ad2ant3 1153	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑆 ∈ V)
426		nfcv 2923	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡(0...𝑁)
427		nfrab1 3432	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
428	426, 427	nfmpt 5203	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
429	409, 428	nfcxfr 2921	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝐵
430		nfcv 2923	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝑖
431	429, 430	nffv 6895	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝐵‘𝑖)
432	431	nfel2 2941	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡 𝑆 ∈ (𝐵‘𝑖)
433	88, 89, 432	nf3an 1934	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖))
434		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)
435	433, 434	nfim 1929	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
436		eleq1 2849	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑆 → (𝑡 ∈ (𝐵‘𝑖) ↔ 𝑆 ∈ (𝐵‘𝑖)))
437	436	3anbi3d 1470	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑆 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖))))
438	93	breq2d 5115	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))
439	437, 438	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))))
440		stoweidlem26.15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡))
441	435, 439, 440	vtoclg1f 3531	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ V → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))
442	425, 441	mpcom 39	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
443	423, 442	syld3an2 1438	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
444	418, 443	mpd3an3 1491	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
445	444	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
446	279, 281, 282, 285, 445	fsumlt 15967	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))
447	278, 446	eqbrtrrd 5129	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))
448	121	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
449	152	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ)
450	307	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
451		ltmul2 12168	. . . . . . 7 ⊢ ((((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))))
452	448, 449, 450, 451	syl3anc 1398	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))))
453	447, 452	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))
454	115, 123, 154, 227, 453	lttrd 11471	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))
455	150, 52	syldan 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
456	455	adantlr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
457	456	recnd 11337	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
458	279, 457	fsumcl 15899	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
459	458	addridd 11510	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
460		0red 11311	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℝ)
461		fzfid 14116	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin)
462	14	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ)
463		0zd 12705	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ)
464	129	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ)
465		elfzelz 13656	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ)
466	465	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ)
467		0red 11311	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ)
468	120	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ)
469	465	zred 12803	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ)
470	469	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ)
471		1m1e0 12415	. . . . . . . . . . . . . . 15 ⊢ (1 − 1) = 0
472	116, 108, 116, 364	lesub1dd 11932	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 − 1) ≤ (𝐿 − 1))
473	471, 472	eqbrtrrid 5141	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (𝐿 − 1))
474	473	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1))
475		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁))
476	375	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ)
477		elfz 13645	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
478	466, 476, 464, 477	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
479	475, 478	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))
480	479	simpld 500	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖)
481	467, 468, 470, 474, 480	letrd 11467	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖)
482		elfzle2 13661	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ≤ 𝑁)
483	482	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ≤ 𝑁)
484	463, 464, 466, 481, 483	elfzd 13647	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁))
485	484, 51	syldan 603	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
486	462, 485	remulcld 11339	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
487	486	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
488	461, 487	fsumrecl 15900	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
489	279, 456	fsumrecl 15900	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
490		fzfid 14116	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin)
491	176	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ)
492	491	mul01d 11509	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0)
493	484, 100	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
494	307	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
495		lemul2 12170	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ ((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))))
496	467, 485, 494, 495	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))))
497	493, 496	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
498	492, 497	eqbrtrrd 5129	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
499	490, 486, 498	fsumge0 15962	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
500	499	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
501	460, 488, 489, 500	leadd2dd 11931	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
502	459, 501	eqbrtrrd 5129	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
503	151	recnd 11337	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ)
504	124, 176, 503	fsummulc2 15950	. . . . . 6 ⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
505	504	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
506		stoweidlem26.2	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
507		elfzelz 13656	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ)
508	507	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ)
509	508	zred 12803	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ)
510	312	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
511	120	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ)
512		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2)))
513		0zd 12705	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈ ℤ)
514	128	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ)
515		elfz 13645	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))))
516	508, 513, 514, 515	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))))
517	512, 516	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2)))
518	517	simprd 501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2))
519	116, 132, 108	ltsub2d 11926	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1)))
520	349, 519	mpbii 236	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 2) < (𝐿 − 1))
521	520	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1))
522	509, 510, 511, 518, 521	lelttrd 11468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1))
523	509, 511	ltnled 11457	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗))
524	522, 523	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗)
525	524	intnanrd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))
526	375	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ)
527	129	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ)
528		elfz 13645	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
529	508, 526, 527, 528	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
530	525, 529	mtbird 328	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
531	530	ex 418	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)))
532	506, 531	ralrimi 3261	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
533		disj 4403	. . . . . . . 8 ⊢ (((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅ ↔ ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
534	532, 533	sylibr 237	. . . . . . 7 ⊢ (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
535	534	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
536	144	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁)
537	128, 374, 129	3jca 1146	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
538	537	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
539		elfz 13645	. . . . . . . . . 10 ⊢ (((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
540	538, 539	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
541	252, 536, 540	mpbir2and 726	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁))
542		fzsplit 13684	. . . . . . . 8 ⊢ ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
543	541, 542	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
544	263, 269, 270	3eqtrd 2800	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1))
545	544	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁))
546	545	uneq2d 4115	. . . . . . . 8 ⊢ (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
547	546	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
548	543, 547	eqtrd 2796	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
549		fzfid 14116	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin)
550	176	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
551	51	recnd 11337	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ)
552	550, 551	mulcld 11329	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
553	552	adantlr 728	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
554	535, 548, 549, 553	fsumsplit 15907	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
555	502, 505, 554	3brtr4d 5137	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
556	114, 153, 53	3jca 1146	. . . . . 6 ⊢ (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ))
557	556	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ))
558		ltletr 11402	. . . . 5 ⊢ ((((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
559	557, 558	syl 18	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
560	454, 555, 559	mp2and 712	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
561	105, 560	pm2.61dan 825	. 2 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
562		sumex 15855	. . 3 ⊢ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V
563	93	oveq2d 7436	. . . . 5 ⊢ (𝑡 = 𝑆 → (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘𝑖)‘𝑆)))
564	563	sumeq2sdv 15870	. . . 4 ⊢ (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
565		eqid 2761	. . . 4 ⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))
566	564, 565	fvmptg 6991	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
567	49, 562, 566	sylancl 598	. 2 ⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
568	561, 567	breqtrrd 5133	1 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 Ⅎwnf 1816 ∈ wcel 2145 Ⅎwnfc 2908 ≠ wne 2956 ∀wral 3077 {crab 3413 Vcvv 3451 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 class class class wbr 5103 ↦ cmpt 5186 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 Fincfn 8973 ℂcc 11198 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 < clt 11343 ≤ cle 11344 − cmin 11541 -cneg 11542 / cdiv 11973 ℕcn 12335 2c2 12397 3c3 12398 4c4 12399 ℕ₀cn0 12606 ℤcz 12693 ℤ_≥cuz 12965 ℝ⁺crp 13120 ...cfz 13639 ♯chash 14474 Σcsu 15853

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-inf2 9642 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 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 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-er 8717 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-sup 9434 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-n0 12607 df-z 12694 df-uz 12966 df-rp 13121 df-ico 13482 df-fz 13640 df-fzo 13789 df-seq 14145 df-exp 14205 df-hash 14475 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-clim 15655 df-sum 15854

This theorem is used by: stoweidlem34 47043

W3C validator