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 44257

Description: This lemma is used to prove that there is a function 𝑔 as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here 𝐿 is used to represnt j in the paper, 𝐷 is used to represent A in the paper, 𝑆 is used to represent t, and 𝐸 is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)

**Hypotheses**
Ref	Expression
stoweidlem26.1	⊢ Ⅎ𝑡𝐹
stoweidlem26.2	⊢ Ⅎ𝑗𝜑
stoweidlem26.3	⊢ Ⅎ𝑡𝜑
stoweidlem26.4	⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
stoweidlem26.5	⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
stoweidlem26.6	⊢ (𝜑 → 𝑁 ∈ ℕ)
stoweidlem26.7	⊢ (𝜑 → 𝑇 ∈ V)
stoweidlem26.8	⊢ (𝜑 → 𝐿 ∈ (1...𝑁))
stoweidlem26.9	⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))))
stoweidlem26.10	⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
stoweidlem26.11	⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
stoweidlem26.12	⊢ (𝜑 → 𝐸 < (1 / 3))
stoweidlem26.13	⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ)
stoweidlem26.14	⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡))
stoweidlem26.15	⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡))

**Assertion**
Ref	Expression
stoweidlem26	⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆))

Distinct variable groups: 𝑖,𝑗,𝑡,𝐸 𝑖,𝐿,𝑗,𝑡 𝑖,𝑁,𝑗,𝑡 𝑆,𝑖,𝑡 𝜑,𝑖 𝑗,𝐹 𝑇,𝑗,𝑡 𝑡,𝑋 Allowed substitution hints: 𝜑(𝑡,𝑗) 𝐵(𝑡,𝑖,𝑗) 𝐷(𝑡,𝑖,𝑗) 𝑆(𝑗) 𝑇(𝑖) 𝐹(𝑡,𝑖) 𝑋(𝑖,𝑗)

**Proof of Theorem stoweidlem26**
Step	Hyp	Ref	Expression
1		1re 11155	. . . . . . . 8 ⊢ 1 ∈ ℝ
2		eleq1 2825	. . . . . . . 8 ⊢ (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
3	1, 2	mpbiri 257	. . . . . . 7 ⊢ (𝐿 = 1 → 𝐿 ∈ ℝ)
4	3	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℝ)
5		4re 12237	. . . . . . . 8 ⊢ 4 ∈ ℝ
6	5	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 4 ∈ ℝ)
7		3re 12233	. . . . . . . 8 ⊢ 3 ∈ ℝ
8	7	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ∈ ℝ)
9		3ne0 12259	. . . . . . . 8 ⊢ 3 ≠ 0
10	9	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ≠ 0)
11	6, 8, 10	redivcld 11983	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈ ℝ)
12	4, 11	resubcld 11583	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
13		stoweidlem26.11	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
14	13	rpred 12957	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ ℝ)
15	14	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐸 ∈ ℝ)
16	12, 15	remulcld 11185	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
17		0red 11158	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ∈ ℝ)
18		fzfid 13878	. . . . . 6 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
19	14	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
20		stoweidlem26.13	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ)
21		stoweidlem26.9	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))))
22		eldif 3920	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
23	21, 22	sylib 217	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
24	23	simpld 495	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ (𝐷‘𝐿))
25		stoweidlem26.4	. . . . . . . . . . . . 13 ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
26		oveq1 7364	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3)))
27	26	oveq1d 7372	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸))
28	27	breq2d 5117	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐿 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
29	28	rabbidv 3415	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐿 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
30		fz1ssfz0 13537	. . . . . . . . . . . . . 14 ⊢ (1...𝑁) ⊆ (0...𝑁)
31		stoweidlem26.8	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ (1...𝑁))
32	30, 31	sselid 3942	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐿 ∈ (0...𝑁))
33		stoweidlem26.7	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ V)
34		rabexg 5288	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
35	33, 34	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
36	25, 29, 32, 35	fvmptd3 6971	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷‘𝐿) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
37	24, 36	eleqtrd 2840	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
38		nfcv 2907	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝑆
39		nfcv 2907	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝑇
40		stoweidlem26.1	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡𝐹
41	40, 38	nffv 6852	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡(𝐹‘𝑆)
42		nfcv 2907	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡 ≤
43		nfcv 2907	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝐿 − (1 / 3)) · 𝐸)
44	41, 42, 43	nfbr 5152	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡(𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)
45		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (𝐹‘𝑡) = (𝐹‘𝑆))
46	45	breq1d 5115	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
47	38, 39, 44, 46	elrabf 3641	. . . . . . . . . . 11 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
48	37, 47	sylib 217	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
49	48	simpld 495	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ 𝑇)
50	49	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑆 ∈ 𝑇)
51	20, 50	ffvelcdmd 7036	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
52	19, 51	remulcld 11185	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
53	18, 52	fsumrecl 15619	. . . . 5 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
54	53	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
55	5, 7, 9	redivcli 11922	. . . . . . 7 ⊢ (4 / 3) ∈ ℝ
56	55	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈ ℝ)
57	4, 56	resubcld 11583	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
58	4	recnd 11183	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℂ)
59	58	subid1d 11501	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) = 𝐿)
60		3cn 12234	. . . . . . . . . 10 ⊢ 3 ∈ ℂ
61	60, 9	dividi 11888	. . . . . . . . 9 ⊢ (3 / 3) = 1
62		3lt4 12327	. . . . . . . . . 10 ⊢ 3 < 4
63		3pos 12258	. . . . . . . . . . 11 ⊢ 0 < 3
64	7, 5, 7, 63	ltdiv1ii 12084	. . . . . . . . . 10 ⊢ (3 < 4 ↔ (3 / 3) < (4 / 3))
65	62, 64	mpbi 229	. . . . . . . . 9 ⊢ (3 / 3) < (4 / 3)
66	61, 65	eqbrtrri 5128	. . . . . . . 8 ⊢ 1 < (4 / 3)
67		breq1 5108	. . . . . . . . 9 ⊢ (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
68	67	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
69	66, 68	mpbiri 257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 < (4 / 3))
70	59, 69	eqbrtrd 5127	. . . . . 6 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) < (4 / 3))
71	4, 17, 56, 70	ltsub23d 11760	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) < 0)
72	13	rpgt0d 12960	. . . . . 6 ⊢ (𝜑 → 0 < 𝐸)
73	72	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 < 𝐸)
74		mulltgt0 43217	. . . . 5 ⊢ ((((𝐿 − (4 / 3)) ∈ ℝ ∧ (𝐿 − (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
75	57, 71, 15, 73, 74	syl22anc 837	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
76		0cn 11147	. . . . . . . 8 ⊢ 0 ∈ ℂ
77		fsumconst 15675	. . . . . . . 8 ⊢ (((0...𝑁) ∈ Fin ∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
78	18, 76, 77	sylancl 586	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
79		hashcl 14256	. . . . . . . . 9 ⊢ ((0...𝑁) ∈ Fin → (♯‘(0...𝑁)) ∈ ℕ₀)
80		nn0cn 12423	. . . . . . . . 9 ⊢ ((♯‘(0...𝑁)) ∈ ℕ₀ → (♯‘(0...𝑁)) ∈ ℂ)
81	18, 79, 80	3syl 18	. . . . . . . 8 ⊢ (𝜑 → (♯‘(0...𝑁)) ∈ ℂ)
82	81	mul01d 11354	. . . . . . 7 ⊢ (𝜑 → ((♯‘(0...𝑁)) · 0) = 0)
83	78, 82	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0)
84	83	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0)
85		0red 11158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ)
86	13	rpge0d 12961	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ 𝐸)
87	86	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸)
88		stoweidlem26.3	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡𝜑
89		nfv 1917	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑖 ∈ (0...𝑁)
90	88, 89	nfan 1902	. . . . . . . . . . 11 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁))
91		nfv 1917	. . . . . . . . . . 11 ⊢ Ⅎ𝑡0 ≤ ((𝑋‘𝑖)‘𝑆)
92	90, 91	nfim 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
93		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑆 → ((𝑋‘𝑖)‘𝑡) = ((𝑋‘𝑖)‘𝑆))
94	93	breq2d 5117	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑆 → (0 ≤ ((𝑋‘𝑖)‘𝑡) ↔ 0 ≤ ((𝑋‘𝑖)‘𝑆)))
95	94	imbi2d 340	. . . . . . . . . 10 ⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))))
96		stoweidlem26.14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡))
97	96	3expia 1121	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 → 0 ≤ ((𝑋‘𝑖)‘𝑡)))
98	97	com12 32	. . . . . . . . . 10 ⊢ (𝑡 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)))
99	38, 92, 95, 98	vtoclgaf 3533	. . . . . . . . 9 ⊢ (𝑆 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)))
100	50, 99	mpcom 38	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
101	19, 51, 87, 100	mulge0d 11732	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
102	18, 85, 52, 101	fsumle 15684	. . . . . 6 ⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
103	102	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
104	84, 103	eqbrtrrd 5129	. . . 4 ⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
105	16, 17, 54, 75, 104	ltletrd 11315	. . 3 ⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
106		elfzelz 13441	. . . . . . . . 9 ⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ)
107		zre 12503	. . . . . . . . 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 11983	. . . . . . . 8 ⊢ (𝜑 → (4 / 3) ∈ ℝ)
113	108, 112	resubcld 11583	. . . . . . 7 ⊢ (𝜑 → (𝐿 − (4 / 3)) ∈ ℝ)
114	113, 14	remulcld 11185	. . . . . 6 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
115	114	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
116	1	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℝ)
117		stoweidlem26.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℕ)
118	14, 117	nndivred 12207	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
119	116, 118	resubcld 11583	. . . . . . . 8 ⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ)
120	108, 116	resubcld 11583	. . . . . . . 8 ⊢ (𝜑 → (𝐿 − 1) ∈ ℝ)
121	119, 120	remulcld 11185	. . . . . . 7 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
122	14, 121	remulcld 11185	. . . . . 6 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
123	122	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
124		fzfid 13878	. . . . . . . 8 ⊢ (𝜑 → (0...(𝐿 − 2)) ∈ Fin)
125	31	elfzelzd 13442	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ∈ ℤ)
126		2z 12535	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
127	126	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 2 ∈ ℤ)
128	125, 127	zsubcld 12612	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 2) ∈ ℤ)
129	117	nnzd 12526	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
130	125	zred 12607	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐿 ∈ ℝ)
131		2re 12227	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
132	131	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℝ)
133	130, 132	resubcld 11583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ∈ ℝ)
134	117	nnred 12168	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ)
135		0le2 12255	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 2
136		0red 11158	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ∈ ℝ)
137	136, 132, 130	lesub2d 11763	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0)))
138	135, 137	mpbii 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0))
139	125	zcnd 12608	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐿 ∈ ℂ)
140	139	subid1d 11501	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 0) = 𝐿)
141	138, 140	breqtrd 5131	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ≤ 𝐿)
142		elfzle2 13445	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ≤ 𝑁)
143	31, 142	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ≤ 𝑁)
144	133, 130, 134, 141, 143	letrd 11312	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 2) ≤ 𝑁)
145	128, 129, 144	3jca 1128	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
146		eluz2 12769	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
147	145, 146	sylibr 233	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝐿 − 2)))
148		fzss2 13481	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
149	147, 148	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁))
150	149	sselda 3944	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
151	150, 51	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
152	124, 151	fsumrecl 15619	. . . . . . 7 ⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ)
153	14, 152	remulcld 11185	. . . . . 6 ⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
154	153	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
155	14, 120	remulcld 11185	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · (𝐿 − 1)) ∈ ℝ)
156	14, 14	remulcld 11185	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
157	155, 156	resubcld 11583	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ)
158	120, 117	nndivred 12207	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ)
159	156, 158	remulcld 11185	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ)
160	155, 159	resubcld 11583	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ)
161	120, 14	resubcld 11583	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ)
162	116, 14	readdcld 11184	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 + 𝐸) ∈ ℝ)
163	1, 7, 9	redivcli 11922	. . . . . . . . . . . . . . 15 ⊢ (1 / 3) ∈ ℝ
164	163	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 / 3) ∈ ℝ)
165		stoweidlem26.12	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐸 < (1 / 3))
166	14, 164, 116, 165	ltadd2dd 11314	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1 + 𝐸) < (1 + (1 / 3)))
167		ax-1cn 11109	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
168	60, 167, 60, 9	divdiri 11912	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
169		3p1e4 12298	. . . . . . . . . . . . . . 15 ⊢ (3 + 1) = 4
170	169	oveq1i 7367	. . . . . . . . . . . . . 14 ⊢ ((3 + 1) / 3) = (4 / 3)
171	61	oveq1i 7367	. . . . . . . . . . . . . 14 ⊢ ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
172	168, 170, 171	3eqtr3ri 2773	. . . . . . . . . . . . 13 ⊢ (1 + (1 / 3)) = (4 / 3)
173	166, 172	breqtrdi 5146	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 + 𝐸) < (4 / 3))
174	162, 112, 108, 173	ltsub2dd 11768	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸)))
175	167	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℂ)
176	13	rpcnd 12959	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ ℂ)
177	139, 175, 176	subsub4d 11543	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸)))
178	174, 177	breqtrrd 5133	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸))
179	113, 161, 13, 178	ltmul1dd 13012	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸))
180	139, 175	subcld 11512	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 − 1) ∈ ℂ)
181	180, 176	subcld 11512	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ)
182	176, 181	mulcomd 11176	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸))
183	176, 180, 176	subdid 11611	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
184	182, 183	eqtr3d 2778	. . . . . . . . 9 ⊢ (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
185	179, 184	breqtrd 5131	. . . . . . . 8 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
186		1zzd 12534	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℤ)
187		elfz 13430	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)))
188	125, 186, 129, 187	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)))
189	31, 188	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁))
190	189	simprd 496	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐿 ≤ 𝑁)
191		zlem1lt 12555	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁))
192	125, 129, 191	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁))
193	190, 192	mpbid 231	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 − 1) < 𝑁)
194	117	nngt0d 12202	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < 𝑁)
195		ltdiv1 12019	. . . . . . . . . . . . . 14 ⊢ (((𝐿 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
196	120, 134, 134, 194, 195	syl112anc 1374	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
197	193, 196	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))
198	117	nncnd 12169	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
199	117	nnne0d 12203	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
200	198, 199	dividd 11929	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / 𝑁) = 1)
201	197, 200	breqtrd 5131	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < 1)
202	14, 14, 72, 72	mulgt0d 11310	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < (𝐸 · 𝐸))
203		ltmul2 12006	. . . . . . . . . . . 12 ⊢ ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 < (𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
204	158, 116, 156, 202, 203	syl112anc 1374	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
205	201, 204	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))
206	176, 176	mulcld 11175	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℂ)
207	206	mulid1d 11172	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸))
208	205, 207	breqtrd 5131	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸))
209	159, 156, 155, 208	ltsub2dd 11768	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
210	114, 157, 160, 185, 209	lttrd 11316	. . . . . . 7 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
211	176, 198, 199	divcld 11931	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
212	175, 211, 180	subdird 11612	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))))
213	180	mulid2d 11173	. . . . . . . . . . 11 ⊢ (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1))
214	213	oveq1d 7372	. . . . . . . . . 10 ⊢ (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
215	212, 214	eqtrd 2776	. . . . . . . . 9 ⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
216	215	oveq2d 7373	. . . . . . . 8 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))))
217	211, 180	mulcld 11175	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈ ℂ)
218	176, 180, 217	subdid 11611	. . . . . . . 8 ⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))))
219	176, 198, 180, 199	div32d 11954	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁)))
220	219	oveq2d 7373	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
221	180, 198, 199	divcld 11931	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ)
222	176, 176, 221	mulassd 11178	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
223	220, 222	eqtr4d 2779	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))
224	223	oveq2d 7373	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
225	216, 218, 224	3eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
226	210, 225	breqtrrd 5133	. . . . . 6 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
227	226	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
228	175, 211	subcld 11512	. . . . . . . . . 10 ⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ)
229		fsumconst 15675	. . . . . . . . . 10 ⊢ (((0...(𝐿 − 2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
230	124, 228, 229	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
231	230	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
232		0zd 12511	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℤ)
233	31	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁))
234	233	elfzelzd 13442	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ)
235	126	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℤ)
236	234, 235	zsubcld 12612	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ)
237		elnnuz 12807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
238	117, 237	sylib 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
239		elfzp12 13520	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
240	238, 239	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
241	31, 240	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
242	241	orcanai 1001	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁))
243		1p1e2 12278	. . . . . . . . . . . . . . . . . 18 ⊢ (1 + 1) = 2
244	243	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2)
245	244	oveq1d 7372	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁))
246	242, 245	eleqtrd 2840	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁))
247		elfzle1 13444	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿)
248	246, 247	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿)
249	108	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ)
250	131	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℝ)
251	249, 250	subge0d 11745	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿))
252	248, 251	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2))
253	232, 236, 252	3jca 1128	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
254		eluz2 12769	. . . . . . . . . . . 12 ⊢ ((𝐿 − 2) ∈ (ℤ_≥‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
255	253, 254	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (ℤ_≥‘0))
256		hashfz 14327	. . . . . . . . . . 11 ⊢ ((𝐿 − 2) ∈ (ℤ_≥‘0) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
257	255, 256	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
258		2cn 12228	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
259	258	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 2 ∈ ℂ)
260	139, 259	subcld 11512	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐿 − 2) ∈ ℂ)
261	260	subid1d 11501	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2))
262	261	oveq1d 7372	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) + 1))
263	139, 259, 175	subadd23d 11534	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2)))
264	258, 167	negsubdi2i 11487	. . . . . . . . . . . . . . . 16 ⊢ -(2 − 1) = (1 − 2)
265		2m1e1 12279	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) = 1
266	265	negeqi 11394	. . . . . . . . . . . . . . . 16 ⊢ -(2 − 1) = -1
267	264, 266	eqtr3i 2766	. . . . . . . . . . . . . . 15 ⊢ (1 − 2) = -1
268	267	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1 − 2) = -1)
269	268	oveq2d 7373	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1))
270	139, 175	negsubd 11518	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐿 + -1) = (𝐿 − 1))
271	269, 270	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1))
272	262, 263, 271	3eqtrd 2780	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
273	272	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
274	257, 273	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (𝐿 − 1))
275	274	oveq1d 7372	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁))))
276	180, 228	mulcomd 11176	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
277	276	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
278	231, 275, 277	3eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
279		fzfid 13878	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin)
280		fzn0 13455	. . . . . . . . 9 ⊢ ((0...(𝐿 − 2)) ≠ ∅ ↔ (𝐿 − 2) ∈ (ℤ_≥‘0))
281	255, 280	sylibr 233	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅)
282	119	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ)
283		simpll 765	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑)
284	150	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
285	283, 284, 51	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
286	49	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ 𝑇)
287		elfzelz 13441	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ)
288	287	zred 12607	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ)
289	288	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ)
290	163	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈ ℝ)
291	289, 290	readdcld 11184	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ)
292	14	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ)
293	291, 292	remulcld 11185	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ)
294	108	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ)
295	131	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈ ℝ)
296	294, 295	resubcld 11583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
297	296, 290	readdcld 11184	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
298	297, 292	remulcld 11185	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
299		stoweidlem26.10	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
300	299, 49	jca 512	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇))
301	300	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇))
302		ffvelcdm 7032	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇) → (𝐹‘𝑆) ∈ ℝ)
303	301, 302	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹‘𝑆) ∈ ℝ)
304		elfzle2 13445	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2))
305	304	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2))
306	289, 296, 290, 305	leadd1dd 11769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)))
307	14, 72	jca 512	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
308	307	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
309		lemul1 12007	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 − 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
310	291, 297, 308, 309	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
311	306, 310	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))
312	108, 132	resubcld 11583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐿 − 2) ∈ ℝ)
313	312, 164	readdcld 11184	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
314	313, 14	remulcld 11185	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
315	299, 49	ffvelcdmd 7036	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ)
316	120, 164	resubcld 11583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈ ℝ)
317	316, 14	remulcld 11185	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈ ℝ)
318		addid1 11335	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1 ∈ ℂ → (1 + 0) = 1)
319	318	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 ∈ ℂ → 1 = (1 + 0))
320	167, 319	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 1 = (1 + 0))
321	175	subidd 11500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 − 1) = 0)
322	321	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 0 = (1 − 1))
323	322	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + 0) = (1 + (1 − 1)))
324		addsubass 11411	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1) − 1) = (1 + (1 − 1)))
325	324	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1 − 1)) = ((1 + 1) − 1))
326	175, 175, 175, 325	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + (1 − 1)) = ((1 + 1) − 1))
327	320, 323, 326	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 1 = ((1 + 1) − 1))
328	327	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) − 1)))
329	243	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1 + 1) = 2)
330	329	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1 + 1) − 1) = (2 − 1))
331	330	oveq2d 7373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 − 1)))
332	139, 259, 175	subsubd 11540	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) + 1))
333	328, 331, 332	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1))
334	333	oveq1d 7372	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 / 3)))
335	258, 60, 9	divcli 11897	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 / 3) ∈ ℂ
336	335	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (2 / 3) ∈ ℂ)
337	260, 175, 336	addsubassd 11532	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 / 3))))
338	167, 60, 9	divcli 11897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 / 3) ∈ ℂ
339		df-3 12217	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 3 = (2 + 1)
340	339	oveq1i 7367	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (3 / 3) = ((2 + 1) / 3)
341	258, 167, 60, 9	divdiri 11912	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
342	340, 61, 341	3eqtr3ri 2773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 / 3) + (1 / 3)) = 1
343	167, 335, 338, 342	subaddrii 11490	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 − (2 / 3)) = (1 / 3)
344	343	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 − (2 / 3)) = (1 / 3))
345	344	oveq2d 7373	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 / 3)))
346	334, 337, 345	3eqtrd 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 / 3)))
347	131, 7, 9	redivcli 11922	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 / 3) ∈ ℝ
348	347	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2 / 3) ∈ ℝ)
349		1lt2 12324	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 < 2
350	7, 63	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (3 ∈ ℝ ∧ 0 < 3)
351	1, 131, 350	3pm3.2i 1339	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
352		ltdiv1 12019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (1 < 2 ↔ (1 / 3) < (2 / 3)))
353	351, 352	mp1i 13	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1 < 2 ↔ (1 / 3) < (2 / 3)))
354	349, 353	mpbii 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1 / 3) < (2 / 3))
355	164, 348, 120, 354	ltsub2dd 11768	. . . . . . . . . . . . . . . . . 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 13012	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸))
358	23	simprd 496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))
359		oveq1 7364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 / 3)))
360	359	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸))
361	360	breq2d 5117	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑗 = (𝐿 − 1) → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
362	361	rabbidv 3415	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑗 = (𝐿 − 1) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
363	129	peano2zd 12610	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
364	189	simpld 495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 1 ≤ 𝐿)
365	134, 116	readdcld 11184	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
366	134	lep1d 12086	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1))
367	108, 134, 365, 190, 366	letrd 11312	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐿 ≤ (𝑁 + 1))
368	186, 363, 125, 364, 367	elfzd 13432	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐿 ∈ (1...(𝑁 + 1)))
369	139, 175	npcand 11516	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝐿 − 1) + 1) = 𝐿)
370		0p1e1 12275	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (0 + 1) = 1
371	370	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (0 + 1) = 1)
372	371	oveq1d 7372	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
373	368, 369, 372	3eltr4d 2853	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
374		0zd 12511	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 0 ∈ ℤ)
375	125, 186	zsubcld 12612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐿 − 1) ∈ ℤ)
376		fzaddel 13475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐿 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
377	374, 129, 375, 186, 376	syl22anc 837	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
378	373, 377	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐿 − 1) ∈ (0...𝑁))
379		rabexg 5288	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
380	33, 379	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
381	25, 362, 378, 380	fvmptd3 6971	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
382	358, 381	neleqtrd 2859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
383		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸)
384	41, 42, 383	nfbr 5152	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)
385	45	breq1d 5115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
386	38, 39, 384, 385	elrabf 3641	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
387	382, 386	sylnib 327	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
388		ianor 980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
389	387, 388	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
390		olc 866	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑆 ∈ 𝑇 → (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇))
391	390	anim1i 615	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑇 ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
392	49, 389, 391	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
393		orcom 868	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))
394	393	anbi2i 623	. . . . . . . . . . . . . . . . . . 19 ⊢ (((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
395	392, 394	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
396		pm4.43 1021	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)))
397	395, 396	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))
398	317, 315	ltnled 11302	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆) ↔ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
399	397, 398	mpbird 256	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆))
400	314, 317, 315, 357, 399	lttrd 11316	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹‘𝑆))
401	314, 315, 400	ltled 11303	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
402	401	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
403	293, 298, 303, 311, 402	letrd 11312	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))
404		nfcv 2907	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸)
405	404, 42, 41	nfbr 5152	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)
406	45	breq2d 5117	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)))
407	38, 39, 405, 406	elrabf 3641	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑆 ∈ 𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)))
408	286, 403, 407	sylanbrc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
409		stoweidlem26.5	. . . . . . . . . . . 12 ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
410		oveq1 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
411	410	oveq1d 7372	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸))
412	411	breq1d 5115	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
413	412	rabbidv 3415	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑖 → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
414		rabexg 5288	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
415	33, 414	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
416	415	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
417	409, 413, 150, 416	fvmptd3 6971	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐵‘𝑖) = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
418	408, 417	eleqtrrd 2841	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵‘𝑖))
419	145	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
420	419, 146	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑁 ∈ (ℤ_≥‘(𝐿 − 2)))
421	420, 148	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
422		simp2 1137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...(𝐿 − 2)))
423	421, 422	sseldd 3945	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...𝑁))
424		elex 3463	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (𝐵‘𝑖) → 𝑆 ∈ V)
425	424	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑆 ∈ V)
426		nfcv 2907	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡(0...𝑁)
427		nfrab1 3426	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
428	426, 427	nfmpt 5212	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
429	409, 428	nfcxfr 2905	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝐵
430		nfcv 2907	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡𝑖
431	429, 430	nffv 6852	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝐵‘𝑖)
432	431	nfel2 2925	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡 𝑆 ∈ (𝐵‘𝑖)
433	88, 89, 432	nf3an 1904	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖))
434		nfv 1917	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)
435	433, 434	nfim 1899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
436		eleq1 2825	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑆 → (𝑡 ∈ (𝐵‘𝑖) ↔ 𝑆 ∈ (𝐵‘𝑖)))
437	436	3anbi3d 1442	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑆 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖))))
438	93	breq2d 5117	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))
439	437, 438	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))))
440		stoweidlem26.15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡))
441	435, 439, 440	vtoclg1f 3524	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ V → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))
442	425, 441	mpcom 38	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
443	423, 442	syld3an2 1411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
444	418, 443	mpd3an3 1462	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
445	444	adantlr 713	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))
446	279, 281, 282, 285, 445	fsumlt 15685	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))
447	278, 446	eqbrtrrd 5129	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))
448	121	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
449	152	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ)
450	307	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
451		ltmul2 12006	. . . . . . 7 ⊢ ((((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))))
452	448, 449, 450, 451	syl3anc 1371	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))))
453	447, 452	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))
454	115, 123, 154, 227, 453	lttrd 11316	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))
455	150, 52	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
456	455	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
457	456	recnd 11183	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
458	279, 457	fsumcl 15618	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
459	458	addid1d 11355	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
460		0red 11158	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℝ)
461		fzfid 13878	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin)
462	14	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ)
463		0zd 12511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ)
464	129	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ)
465		elfzelz 13441	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ)
466	465	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ)
467		0red 11158	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ)
468	120	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ)
469	465	zred 12607	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ)
470	469	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ)
471		1m1e0 12225	. . . . . . . . . . . . . . 15 ⊢ (1 − 1) = 0
472	116, 108, 116, 364	lesub1dd 11771	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 − 1) ≤ (𝐿 − 1))
473	471, 472	eqbrtrrid 5141	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ≤ (𝐿 − 1))
474	473	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1))
475		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁))
476	375	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ)
477		elfz 13430	. . . . . . . . . . . . . . . 16 ⊢ ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
478	466, 476, 464, 477	syl3anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)))
479	475, 478	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))
480	479	simpld 495	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖)
481	467, 468, 470, 474, 480	letrd 11312	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖)
482		elfzle2 13445	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ≤ 𝑁)
483	482	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ≤ 𝑁)
484	463, 464, 466, 481, 483	elfzd 13432	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁))
485	484, 51	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ)
486	462, 485	remulcld 11185	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
487	486	adantlr 713	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
488	461, 487	fsumrecl 15619	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
489	279, 456	fsumrecl 15619	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)
490		fzfid 13878	. . . . . . . . 9 ⊢ (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin)
491	176	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ)
492	491	mul01d 11354	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0)
493	484, 100	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))
494	307	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
495		lemul2 12008	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ ((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))))
496	467, 485, 494, 495	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))))
497	493, 496	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
498	492, 497	eqbrtrrd 5129	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))
499	490, 486, 498	fsumge0 15680	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
500	499	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
501	460, 488, 489, 500	leadd2dd 11770	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
502	459, 501	eqbrtrrd 5129	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
503	151	recnd 11183	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ)
504	124, 176, 503	fsummulc2 15669	. . . . . 6 ⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
505	504	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)))
506		stoweidlem26.2	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
507		elfzelz 13441	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ)
508	507	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ)
509	508	zred 12607	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ)
510	312	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
511	120	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ)
512		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2)))
513		0zd 12511	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈ ℤ)
514	128	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ)
515		elfz 13430	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))))
516	508, 513, 514, 515	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))))
517	512, 516	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2)))
518	517	simprd 496	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2))
519	116, 132, 108	ltsub2d 11765	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1)))
520	349, 519	mpbii 232	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐿 − 2) < (𝐿 − 1))
521	520	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1))
522	509, 510, 511, 518, 521	lelttrd 11313	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1))
523	509, 511	ltnled 11302	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗))
524	522, 523	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗)
525	524	intnanrd 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))
526	375	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ)
527	129	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ)
528		elfz 13430	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
529	508, 526, 527, 528	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)))
530	525, 529	mtbird 324	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
531	530	ex 413	. . . . . . . . 9 ⊢ (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)))
532	506, 531	ralrimi 3240	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
533		disj 4407	. . . . . . . 8 ⊢ (((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅ ↔ ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
534	532, 533	sylibr 233	. . . . . . 7 ⊢ (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
535	534	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
536	144	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁)
537	128, 374, 129	3jca 1128	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
538	537	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
539		elfz 13430	. . . . . . . . . 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 711	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁))
542		fzsplit 13467	. . . . . . . 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 2780	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1))
545	544	oveq1d 7372	. . . . . . . . 9 ⊢ (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁))
546	545	uneq2d 4123	. . . . . . . 8 ⊢ (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
547	546	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
548	543, 547	eqtrd 2776	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
549		fzfid 13878	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin)
550	176	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
551	51	recnd 11183	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ)
552	550, 551	mulcld 11175	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
553	552	adantlr 713	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ)
554	535, 548, 549, 553	fsumsplit 15626	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))))
555	502, 505, 554	3brtr4d 5137	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
556	114, 153, 53	3jca 1128	. . . . . 6 ⊢ (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ))
557	556	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ))
558		ltletr 11247	. . . . 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 697	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
561	105, 560	pm2.61dan 811	. 2 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
562		sumex 15572	. . 3 ⊢ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V
563	93	oveq2d 7373	. . . . 5 ⊢ (𝑡 = 𝑆 → (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘𝑖)‘𝑆)))
564	563	sumeq2sdv 15589	. . . 4 ⊢ (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
565		eqid 2736	. . . 4 ⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))
566	564, 565	fvmptg 6946	. . 3 ⊢ ((𝑆 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
567	49, 562, 566	sylancl 586	. 2 ⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))
568	561, 567	breqtrrd 5133	1 ⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 Ⅎwnf 1785 ∈ wcel 2106 Ⅎwnfc 2887 ≠ wne 2943 ∀wral 3064 {crab 3407 Vcvv 3445 ∖ cdif 3907 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 class class class wbr 5105 ↦ cmpt 5188 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 Fincfn 8883 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 · cmul 11056 < clt 11189 ≤ cle 11190 − cmin 11385 -cneg 11386 / cdiv 11812 ℕcn 12153 2c2 12208 3c3 12209 4c4 12210 ℕ₀cn0 12413 ℤcz 12499 ℤ_≥cuz 12763 ℝ⁺crp 12915 ...cfz 13424 ♯chash 14230 Σcsu 15570

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-er 8648 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9378 df-oi 9446 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-4 12218 df-n0 12414 df-z 12500 df-uz 12764 df-rp 12916 df-ico 13270 df-fz 13425 df-fzo 13568 df-seq 13907 df-exp 13968 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-clim 15370 df-sum 15571

This theorem is referenced by: stoweidlem34 44265

W3C validator