Proof of Theorem stoweidlem26
Step | Hyp | Ref
| Expression |
1 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
2 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈
ℝ)) |
3 | 1, 2 | mpbiri 247 |
. . . . . . 7
⊢ (𝐿 = 1 → 𝐿 ∈ ℝ) |
4 | 3 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℝ) |
5 | | 4re 10974 |
. . . . . . . 8
⊢ 4 ∈
ℝ |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 4 ∈
ℝ) |
7 | | 3re 10971 |
. . . . . . . 8
⊢ 3 ∈
ℝ |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ∈
ℝ) |
9 | | 3ne0 10992 |
. . . . . . . 8
⊢ 3 ≠
0 |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ≠ 0) |
11 | 6, 8, 10 | redivcld 10732 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈
ℝ) |
12 | 4, 11 | resubcld 10337 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈
ℝ) |
13 | | stoweidlem26.11 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
14 | 13 | rpred 11748 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℝ) |
15 | 14 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐸 ∈ ℝ) |
16 | 12, 15 | remulcld 9949 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ) |
17 | | 0red 9920 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ∈
ℝ) |
18 | | fzfid 12634 |
. . . . . 6
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
19 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ) |
20 | | stoweidlem26.13 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ) |
21 | | stoweidlem26.9 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1)))) |
22 | | eldif 3550 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))) |
23 | 21, 22 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))) |
24 | 23 | simpld 474 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ (𝐷‘𝐿)) |
25 | | 1e0p1 11428 |
. . . . . . . . . . . . . . . 16
⊢ 1 = (0 +
1) |
26 | 25 | oveq1i 6559 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑁) = ((0 +
1)...𝑁) |
27 | | 0z 11265 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
28 | | fzp1ss 12262 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
ℤ → ((0 + 1)...𝑁) ⊆ (0...𝑁)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((0 +
1)...𝑁) ⊆ (0...𝑁) |
30 | 26, 29 | eqsstri 3598 |
. . . . . . . . . . . . . 14
⊢
(1...𝑁) ⊆
(0...𝑁) |
31 | | stoweidlem26.8 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) |
32 | 30, 31 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ (0...𝑁)) |
33 | | stoweidlem26.7 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ V) |
34 | | rabexg 4739 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V) |
36 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3))) |
37 | 36 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸)) |
38 | 37 | breq2d 4595 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝐿 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸))) |
39 | 38 | rabbidv 3164 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝐿 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)}) |
40 | | stoweidlem26.4 |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
41 | 39, 40 | fvmptg 6189 |
. . . . . . . . . . . . 13
⊢ ((𝐿 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘𝐿) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)}) |
42 | 32, 35, 41 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘𝐿) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)}) |
43 | 24, 42 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)}) |
44 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝑆 |
45 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝑇 |
46 | | stoweidlem26.1 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡𝐹 |
47 | 46, 44 | nffv 6110 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡(𝐹‘𝑆) |
48 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡
≤ |
49 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝐿 − (1 / 3)) · 𝐸) |
50 | 47, 48, 49 | nfbr 4629 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡(𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸) |
51 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑆 → (𝐹‘𝑡) = (𝐹‘𝑆)) |
52 | 51 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸))) |
53 | 44, 45, 50, 52 | elrabf 3329 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸))) |
54 | 43, 53 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸))) |
55 | 54 | simpld 474 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ 𝑇) |
56 | 55 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑆 ∈ 𝑇) |
57 | 20, 56 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
58 | 19, 57 | remulcld 9949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
59 | 18, 58 | fsumrecl 14312 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
60 | 59 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
61 | 5, 7, 9 | redivcli 10671 |
. . . . . . 7
⊢ (4 / 3)
∈ ℝ |
62 | 61 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈
ℝ) |
63 | 4, 62 | resubcld 10337 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈
ℝ) |
64 | 4 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℂ) |
65 | 64 | subid1d 10260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) = 𝐿) |
66 | | 3cn 10972 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
67 | 66, 9 | dividi 10637 |
. . . . . . . . 9
⊢ (3 / 3) =
1 |
68 | | 3lt4 11074 |
. . . . . . . . . 10
⊢ 3 <
4 |
69 | | 3pos 10991 |
. . . . . . . . . . 11
⊢ 0 <
3 |
70 | 7, 5, 7, 69 | ltdiv1ii 10832 |
. . . . . . . . . 10
⊢ (3 < 4
↔ (3 / 3) < (4 / 3)) |
71 | 68, 70 | mpbi 219 |
. . . . . . . . 9
⊢ (3 / 3)
< (4 / 3) |
72 | 67, 71 | eqbrtrri 4606 |
. . . . . . . 8
⊢ 1 < (4
/ 3) |
73 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 /
3))) |
74 | 73 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 /
3))) |
75 | 72, 74 | mpbiri 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 < (4 / 3)) |
76 | 65, 75 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) < (4 / 3)) |
77 | 4, 17, 62, 76 | ltsub23d 10511 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) < 0) |
78 | 13 | rpgt0d 11751 |
. . . . . 6
⊢ (𝜑 → 0 < 𝐸) |
79 | 78 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → 0 < 𝐸) |
80 | | mulltgt0 38204 |
. . . . 5
⊢ ((((𝐿 − (4 / 3)) ∈ ℝ
∧ (𝐿 − (4 / 3))
< 0) ∧ (𝐸 ∈
ℝ ∧ 0 < 𝐸))
→ ((𝐿 − (4 / 3))
· 𝐸) <
0) |
81 | 63, 77, 15, 79, 80 | syl22anc 1319 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0) |
82 | | 0cn 9911 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
83 | | fsumconst 14364 |
. . . . . . . 8
⊢
(((0...𝑁) ∈ Fin
∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((#‘(0...𝑁)) · 0)) |
84 | 18, 82, 83 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((#‘(0...𝑁)) · 0)) |
85 | | hashcl 13009 |
. . . . . . . . 9
⊢
((0...𝑁) ∈ Fin
→ (#‘(0...𝑁))
∈ ℕ0) |
86 | | nn0cn 11179 |
. . . . . . . . 9
⊢
((#‘(0...𝑁))
∈ ℕ0 → (#‘(0...𝑁)) ∈ ℂ) |
87 | 18, 85, 86 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (#‘(0...𝑁)) ∈
ℂ) |
88 | 87 | mul01d 10114 |
. . . . . . 7
⊢ (𝜑 → ((#‘(0...𝑁)) · 0) =
0) |
89 | 84, 88 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0) |
90 | 89 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0) |
91 | | 0red 9920 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ) |
92 | 13 | rpge0d 11752 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐸) |
93 | 92 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸) |
94 | | stoweidlem26.3 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝜑 |
95 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡 𝑖 ∈ (0...𝑁) |
96 | 94, 95 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁)) |
97 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡0 ≤
((𝑋‘𝑖)‘𝑆) |
98 | 96, 97 | nfim 1813 |
. . . . . . . . . 10
⊢
Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)) |
99 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑆 → ((𝑋‘𝑖)‘𝑡) = ((𝑋‘𝑖)‘𝑆)) |
100 | 99 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑆 → (0 ≤ ((𝑋‘𝑖)‘𝑡) ↔ 0 ≤ ((𝑋‘𝑖)‘𝑆))) |
101 | 100 | imbi2d 329 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)))) |
102 | | stoweidlem26.14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) |
103 | 102 | 3expia 1259 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 → 0 ≤ ((𝑋‘𝑖)‘𝑡))) |
104 | 103 | com12 32 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡))) |
105 | 44, 98, 101, 104 | vtoclgaf 3244 |
. . . . . . . . 9
⊢ (𝑆 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))) |
106 | 56, 105 | mpcom 37 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)) |
107 | 19, 57, 93, 106 | mulge0d 10483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))) |
108 | 18, 91, 58, 107 | fsumle 14372 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
109 | 108 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
110 | 90, 109 | eqbrtrrd 4607 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
111 | 16, 17, 60, 81, 110 | ltletrd 10076 |
. . 3
⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
112 | | elfzelz 12213 |
. . . . . . . . 9
⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ) |
113 | | zre 11258 |
. . . . . . . . 9
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) |
114 | 31, 112, 113 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ ℝ) |
115 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 4 ∈
ℝ) |
116 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 3 ∈
ℝ) |
117 | 9 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 3 ≠ 0) |
118 | 115, 116,
117 | redivcld 10732 |
. . . . . . . 8
⊢ (𝜑 → (4 / 3) ∈
ℝ) |
119 | 114, 118 | resubcld 10337 |
. . . . . . 7
⊢ (𝜑 → (𝐿 − (4 / 3)) ∈
ℝ) |
120 | 119, 14 | remulcld 9949 |
. . . . . 6
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ) |
121 | 120 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ) |
122 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) |
123 | | stoweidlem26.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
124 | 14, 123 | nndivred 10946 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ) |
125 | 122, 124 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ) |
126 | 114, 122 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 − 1) ∈ ℝ) |
127 | 125, 126 | remulcld 9949 |
. . . . . . 7
⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈
ℝ) |
128 | 14, 127 | remulcld 9949 |
. . . . . 6
⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈
ℝ) |
129 | 128 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈
ℝ) |
130 | | fzfid 12634 |
. . . . . . . 8
⊢ (𝜑 → (0...(𝐿 − 2)) ∈ Fin) |
131 | 31, 112 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ ℤ) |
132 | | 2z 11286 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℤ) |
134 | 131, 133 | zsubcld 11363 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 − 2) ∈ ℤ) |
135 | 123 | nnzd 11357 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) |
136 | 131 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐿 ∈ ℝ) |
137 | | 2re 10967 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
138 | 137 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℝ) |
139 | 136, 138 | resubcld 10337 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 − 2) ∈ ℝ) |
140 | 123 | nnred 10912 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
141 | | 0le2 10988 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
2 |
142 | | 0red 9920 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ∈
ℝ) |
143 | 142, 138,
136 | lesub2d 10514 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0))) |
144 | 141, 143 | mpbii 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0)) |
145 | 131 | zcnd 11359 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐿 ∈ ℂ) |
146 | 145 | subid1d 10260 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐿 − 0) = 𝐿) |
147 | 144, 146 | breqtrd 4609 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 − 2) ≤ 𝐿) |
148 | | elfzle2 12216 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ≤ 𝑁) |
149 | 31, 148 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ≤ 𝑁) |
150 | 139, 136,
140, 147, 149 | letrd 10073 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 − 2) ≤ 𝑁) |
151 | 134, 135,
150 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁)) |
152 | | eluz2 11569 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁)) |
153 | 151, 152 | sylibr 223 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝐿 − 2))) |
154 | | fzss2 12252 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁)) |
155 | 153, 154 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁)) |
156 | 155 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁)) |
157 | 156, 57 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
158 | 130, 157 | fsumrecl 14312 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
159 | 14, 158 | remulcld 9949 |
. . . . . 6
⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
160 | 159 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
161 | 14, 126 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · (𝐿 − 1)) ∈
ℝ) |
162 | 14, 14 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℝ) |
163 | 161, 162 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ) |
164 | 126, 123 | nndivred 10946 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ) |
165 | 162, 164 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ) |
166 | 161, 165 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ) |
167 | 126, 14 | resubcld 10337 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ) |
168 | 122, 14 | readdcld 9948 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 + 𝐸) ∈ ℝ) |
169 | 1, 7, 9 | redivcli 10671 |
. . . . . . . . . . . . . . 15
⊢ (1 / 3)
∈ ℝ |
170 | 169 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / 3) ∈
ℝ) |
171 | | stoweidlem26.12 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 < (1 / 3)) |
172 | 14, 170, 122, 171 | ltadd2dd 10075 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 + 𝐸) < (1 + (1 / 3))) |
173 | | ax-1cn 9873 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
174 | 66, 173, 66, 9 | divdiri 10661 |
. . . . . . . . . . . . . 14
⊢ ((3 + 1)
/ 3) = ((3 / 3) + (1 / 3)) |
175 | | 3p1e4 11030 |
. . . . . . . . . . . . . . 15
⊢ (3 + 1) =
4 |
176 | 175 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ ((3 + 1)
/ 3) = (4 / 3) |
177 | 67 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ ((3 / 3)
+ (1 / 3)) = (1 + (1 / 3)) |
178 | 174, 176,
177 | 3eqtr3ri 2641 |
. . . . . . . . . . . . 13
⊢ (1 + (1 /
3)) = (4 / 3) |
179 | 172, 178 | syl6breq 4624 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 + 𝐸) < (4 / 3)) |
180 | 168, 118,
114, 179 | ltsub2dd 10519 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸))) |
181 | 173 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
182 | 13 | rpcnd 11750 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℂ) |
183 | 145, 181,
182 | subsub4d 10302 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸))) |
184 | 180, 183 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸)) |
185 | 119, 167,
13, 184 | ltmul1dd 11803 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸)) |
186 | 145, 181 | subcld 10271 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 − 1) ∈ ℂ) |
187 | 186, 182 | subcld 10271 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ) |
188 | 182, 187 | mulcomd 9940 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸)) |
189 | 182, 186,
182 | subdid 10365 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸))) |
190 | 188, 189 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸))) |
191 | 185, 190 | breqtrd 4609 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸))) |
192 | | 1zzd 11285 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℤ) |
193 | | elfz 12203 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℤ ∧ 1 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝐿 ∈
(1...𝑁) ↔ (1 ≤
𝐿 ∧ 𝐿 ≤ 𝑁))) |
194 | 131, 192,
135, 193 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁))) |
195 | 31, 194 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) |
196 | 195 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ≤ 𝑁) |
197 | | zlem1lt 11306 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁)) |
198 | 131, 135,
197 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁)) |
199 | 196, 198 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 − 1) < 𝑁) |
200 | 123 | nngt0d 10941 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) |
201 | | ltdiv1 10766 |
. . . . . . . . . . . . . 14
⊢ (((𝐿 − 1) ∈ ℝ ∧
𝑁 ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))) |
202 | 126, 140,
140, 200, 201 | syl112anc 1322 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))) |
203 | 199, 202 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)) |
204 | 123 | nncnd 10913 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
205 | 123 | nnne0d 10942 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ 0) |
206 | 204, 205 | dividd 10678 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 / 𝑁) = 1) |
207 | 203, 206 | breqtrd 4609 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < 1) |
208 | 14, 14, 78, 78 | mulgt0d 10071 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝐸 · 𝐸)) |
209 | | ltmul2 10753 |
. . . . . . . . . . . 12
⊢ ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ
∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 <
(𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))) |
210 | 164, 122,
162, 208, 209 | syl112anc 1322 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))) |
211 | 207, 210 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)) |
212 | 182, 182 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℂ) |
213 | 212 | mulid1d 9936 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸)) |
214 | 211, 213 | breqtrd 4609 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸)) |
215 | 165, 162,
161, 214 | ltsub2dd 10519 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) |
216 | 120, 163,
166, 191, 215 | lttrd 10077 |
. . . . . . 7
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) |
217 | 182, 204,
205 | divcld 10680 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℂ) |
218 | 181, 217,
186 | subdird 10366 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1)))) |
219 | 186 | mulid2d 9937 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1)) |
220 | 219 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) |
221 | 218, 220 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) |
222 | 221 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))) |
223 | 217, 186 | mulcld 9939 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈
ℂ) |
224 | 182, 186,
223 | subdid 10365 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))))) |
225 | 182, 204,
186, 205 | div32d 10703 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁))) |
226 | 225 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁)))) |
227 | 186, 204,
205 | divcld 10680 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ) |
228 | 182, 182,
227 | mulassd 9942 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁)))) |
229 | 226, 228 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) |
230 | 229 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) |
231 | 222, 224,
230 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) |
232 | 216, 231 | breqtrrd 4611 |
. . . . . 6
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))) |
233 | 232 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))) |
234 | 181, 217 | subcld 10271 |
. . . . . . . . . 10
⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ) |
235 | | fsumconst 14364 |
. . . . . . . . . 10
⊢
(((0...(𝐿 −
2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁)))) |
236 | 130, 234,
235 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁)))) |
237 | 236 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁)))) |
238 | | 0zd 11266 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈
ℤ) |
239 | 31 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁)) |
240 | 239, 112 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ) |
241 | 132 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈
ℤ) |
242 | 240, 241 | zsubcld 11363 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ) |
243 | | elnnuz 11600 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
244 | 123, 243 | sylib 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
245 | | elfzp12 12288 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))) |
246 | 244, 245 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))) |
247 | 31, 246 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))) |
248 | 247 | orcanai 950 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁)) |
249 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 + 1) =
2 |
250 | 249 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2) |
251 | 250 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁)) |
252 | 248, 251 | eleqtrd 2690 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁)) |
253 | | elfzle1 12215 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿) |
254 | 252, 253 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿) |
255 | 114 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ) |
256 | 137 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈
ℝ) |
257 | 255, 256 | subge0d 10496 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿)) |
258 | 254, 257 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2)) |
259 | 238, 242,
258 | 3jca 1235 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧
0 ≤ (𝐿 −
2))) |
260 | | eluz2 11569 |
. . . . . . . . . . . 12
⊢ ((𝐿 − 2) ∈
(ℤ≥‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧
0 ≤ (𝐿 −
2))) |
261 | 259, 260 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈
(ℤ≥‘0)) |
262 | | hashfz 13074 |
. . . . . . . . . . 11
⊢ ((𝐿 − 2) ∈
(ℤ≥‘0) → (#‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) +
1)) |
263 | 261, 262 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (#‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) +
1)) |
264 | | 2cn 10968 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
265 | 264 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) |
266 | 145, 265 | subcld 10271 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 − 2) ∈ ℂ) |
267 | 266 | subid1d 10260 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2)) |
268 | 267 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) +
1)) |
269 | 145, 265,
181 | subadd23d 10293 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2))) |
270 | 264, 173 | negsubdi2i 10246 |
. . . . . . . . . . . . . . . 16
⊢ -(2
− 1) = (1 − 2) |
271 | | 2m1e1 11012 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
272 | 271 | negeqi 10153 |
. . . . . . . . . . . . . . . 16
⊢ -(2
− 1) = -1 |
273 | 270, 272 | eqtr3i 2634 |
. . . . . . . . . . . . . . 15
⊢ (1
− 2) = -1 |
274 | 273 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 − 2) =
-1) |
275 | 274 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1)) |
276 | 145, 181 | negsubd 10277 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 + -1) = (𝐿 − 1)) |
277 | 275, 276 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1)) |
278 | 268, 269,
277 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1)) |
279 | 278 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1)) |
280 | 263, 279 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (#‘(0...(𝐿 − 2))) = (𝐿 − 1)) |
281 | 280 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((#‘(0...(𝐿 − 2))) · (1
− (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁)))) |
282 | 186, 234 | mulcomd 9940 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) |
283 | 282 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) |
284 | 237, 281,
283 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) |
285 | | fzfid 12634 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin) |
286 | | fzn0 12226 |
. . . . . . . . 9
⊢
((0...(𝐿 − 2))
≠ ∅ ↔ (𝐿
− 2) ∈ (ℤ≥‘0)) |
287 | 261, 286 | sylibr 223 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅) |
288 | 125 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ) |
289 | | simpll 786 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑) |
290 | 156 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁)) |
291 | 289, 290,
57 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
292 | 55 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ 𝑇) |
293 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ) |
294 | 293 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ) |
295 | 294 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ) |
296 | 169 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈
ℝ) |
297 | 295, 296 | readdcld 9948 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ) |
298 | 14 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ) |
299 | 297, 298 | remulcld 9949 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ) |
300 | 114 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ) |
301 | 137 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈
ℝ) |
302 | 300, 301 | resubcld 10337 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ) |
303 | 302, 296 | readdcld 9948 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈
ℝ) |
304 | 303, 298 | remulcld 9949 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈
ℝ) |
305 | | stoweidlem26.10 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) |
306 | 305, 55 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇)) |
307 | 306 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇)) |
308 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇) → (𝐹‘𝑆) ∈ ℝ) |
309 | 307, 308 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹‘𝑆) ∈ ℝ) |
310 | | elfzle2 12216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2)) |
311 | 310 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2)) |
312 | 295, 302,
296, 311 | leadd1dd 10520 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3))) |
313 | 14, 78 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
314 | 313 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
315 | | lemul1 10754 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 + (1 / 3)) ∈ ℝ ∧
((𝐿 − 2) + (1 / 3))
∈ ℝ ∧ (𝐸
∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))) |
316 | 297, 303,
314, 315 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))) |
317 | 312, 316 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)) |
318 | 114, 138 | resubcld 10337 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐿 − 2) ∈ ℝ) |
319 | 318, 170 | readdcld 9948 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈
ℝ) |
320 | 319, 14 | remulcld 9949 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈
ℝ) |
321 | 305, 55 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ) |
322 | 126, 170 | resubcld 10337 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈
ℝ) |
323 | 322, 14 | remulcld 9949 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈
ℝ) |
324 | | addid1 10095 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
ℂ → (1 + 0) = 1) |
325 | 324 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 ∈
ℂ → 1 = (1 + 0)) |
326 | 173, 325 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 = (1 +
0)) |
327 | 181 | subidd 10259 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (1 − 1) =
0) |
328 | 327 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 0 = (1 −
1)) |
329 | 328 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 + 0) = (1 + (1 −
1))) |
330 | | addsubass 10170 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1)
− 1) = (1 + (1 − 1))) |
331 | 330 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1
− 1)) = ((1 + 1) − 1)) |
332 | 181, 181,
181, 331 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 + (1 − 1)) = ((1
+ 1) − 1)) |
333 | 326, 329,
332 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 = ((1 + 1) −
1)) |
334 | 333 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) −
1))) |
335 | 249 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 + 1) =
2) |
336 | 335 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1 + 1) − 1) = (2
− 1)) |
337 | 336 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 −
1))) |
338 | 145, 265,
181 | subsubd 10299 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) +
1)) |
339 | 334, 337,
338 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1)) |
340 | 339 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 /
3))) |
341 | 264, 66, 9 | divcli 10646 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 / 3)
∈ ℂ |
342 | 341 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2 / 3) ∈
ℂ) |
343 | 266, 181,
342 | addsubassd 10291 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 /
3)))) |
344 | 173, 66, 9 | divcli 10646 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 / 3)
∈ ℂ |
345 | | df-3 10957 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 = (2 +
1) |
346 | 345 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (3 / 3) =
((2 + 1) / 3) |
347 | 264, 173,
66, 9 | divdiri 10661 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2 + 1)
/ 3) = ((2 / 3) + (1 / 3)) |
348 | 346, 67, 347 | 3eqtr3ri 2641 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2 / 3)
+ (1 / 3)) = 1 |
349 | 173, 341,
344, 348 | subaddrii 10249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1
− (2 / 3)) = (1 / 3) |
350 | 349 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 − (2 / 3)) = (1 /
3)) |
351 | 350 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 /
3))) |
352 | 340, 343,
351 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 /
3))) |
353 | 137, 7, 9 | redivcli 10671 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 / 3)
∈ ℝ |
354 | 353 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2 / 3) ∈
ℝ) |
355 | | 1lt2 11071 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
2 |
356 | 7, 69 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (3 ∈
ℝ ∧ 0 < 3) |
357 | 1, 137, 356 | 3pm3.2i 1232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 <
3)) |
358 | | ltdiv1 10766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
→ (1 < 2 ↔ (1 / 3) < (2 / 3))) |
359 | 357, 358 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 < 2 ↔ (1 / 3)
< (2 / 3))) |
360 | 355, 359 | mpbii 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 / 3) < (2 /
3)) |
361 | 170, 354,
126, 360 | ltsub2dd 10519 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 /
3))) |
362 | 352, 361 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 /
3))) |
363 | 319, 322,
13, 362 | ltmul1dd 11803 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸)) |
364 | 23 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))) |
365 | 195 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 1 ≤ 𝐿) |
366 | 140, 122 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) |
367 | 140 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1)) |
368 | 114, 140,
366, 196, 367 | letrd 10073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐿 ≤ (𝑁 + 1)) |
369 | 135 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
370 | | elfz 12203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐿 ∈ ℤ ∧ 1 ∈
ℤ ∧ (𝑁 + 1)
∈ ℤ) → (𝐿
∈ (1...(𝑁 + 1)) ↔
(1 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 + 1)))) |
371 | 131, 192,
369, 370 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐿 ∈ (1...(𝑁 + 1)) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 + 1)))) |
372 | 365, 368,
371 | mpbir2and 959 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐿 ∈ (1...(𝑁 + 1))) |
373 | 145, 181 | npcand 10275 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝐿 − 1) + 1) = 𝐿) |
374 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0 + 1) =
1 |
375 | 374 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (0 + 1) =
1) |
376 | 375 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))) |
377 | 372, 373,
376 | 3eltr4d 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))) |
378 | | 0zd 11266 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ∈
ℤ) |
379 | 131, 192 | zsubcld 11363 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐿 − 1) ∈ ℤ) |
380 | | fzaddel 12246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((0
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ ((𝐿
− 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))) |
381 | 378, 135,
379, 192, 380 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))) |
382 | 377, 381 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐿 − 1) ∈ (0...𝑁)) |
383 | | rabexg 4739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V) |
384 | 33, 383 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V) |
385 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 /
3))) |
386 | 385 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸)) |
387 | 386 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 = (𝐿 − 1) → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
388 | 387 | rabbidv 3164 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = (𝐿 − 1) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)}) |
389 | 388, 40 | fvmptg 6189 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐿 − 1) ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘(𝐿 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)}) |
390 | 382, 384,
389 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)}) |
391 | 364, 390 | neleqtrd 2709 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)}) |
392 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸) |
393 | 47, 48, 392 | nfbr 4629 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑡(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) |
394 | 51 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
395 | 44, 45, 393, 394 | elrabf 3329 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
396 | 391, 395 | sylnib 317 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
397 | | ianor 508 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
398 | 396, 397 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
399 | | olc 398 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ 𝑇 → (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇)) |
400 | 399 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ 𝑇 ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))) |
401 | 55, 398, 400 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))) |
402 | | orcom 401 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)) |
403 | 402 | anbi2i 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((¬
(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))) |
404 | 401, 403 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))) |
405 | | pm4.43 964 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))) |
406 | 404, 405 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) |
407 | 323, 321 | ltnled 10063 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆) ↔ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
408 | 406, 407 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆)) |
409 | 320, 323,
321, 363, 408 | lttrd 10077 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹‘𝑆)) |
410 | 320, 321,
409 | ltled 10064 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)) |
411 | 410 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)) |
412 | 299, 304,
309, 317, 411 | letrd 10073 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)) |
413 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) |
414 | 413, 48, 47 | nfbr 4629 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆) |
415 | 51 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))) |
416 | 44, 45, 414, 415 | elrabf 3329 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑆 ∈ 𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))) |
417 | 292, 412,
416 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
418 | | rabexg 4739 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) |
419 | 33, 418 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) |
420 | 419 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) |
421 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3))) |
422 | 421 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸)) |
423 | 422 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡))) |
424 | 423 | rabbidv 3164 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
425 | | stoweidlem26.5 |
. . . . . . . . . . . . 13
⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
426 | 424, 425 | fvmptg 6189 |
. . . . . . . . . . . 12
⊢ ((𝑖 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) → (𝐵‘𝑖) = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
427 | 156, 420,
426 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐵‘𝑖) = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
428 | 417, 427 | eleqtrrd 2691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵‘𝑖)) |
429 | 151 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁)) |
430 | 429, 152 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑁 ∈ (ℤ≥‘(𝐿 − 2))) |
431 | 430, 154 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁)) |
432 | | simp2 1055 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...(𝐿 − 2))) |
433 | 431, 432 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...𝑁)) |
434 | | elex 3185 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (𝐵‘𝑖) → 𝑆 ∈ V) |
435 | 434 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑆 ∈ V) |
436 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡(0...𝑁) |
437 | | nfrab1 3099 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} |
438 | 436, 437 | nfmpt 4674 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
439 | 425, 438 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝐵 |
440 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝑖 |
441 | 439, 440 | nffv 6110 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡(𝐵‘𝑖) |
442 | 441 | nfel2 2767 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡 𝑆 ∈ (𝐵‘𝑖) |
443 | 94, 95, 442 | nf3an 1819 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) |
444 | | nfv 1830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(1 −
(𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆) |
445 | 443, 444 | nfim 1813 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) |
446 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑆 → (𝑡 ∈ (𝐵‘𝑖) ↔ 𝑆 ∈ (𝐵‘𝑖))) |
447 | 446 | 3anbi3d 1397 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑆 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)))) |
448 | 99 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))) |
449 | 447, 448 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))) |
450 | | stoweidlem26.15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) |
451 | 445, 449,
450 | vtoclg1f 3238 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ V → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))) |
452 | 435, 451 | mpcom 37 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) |
453 | 433, 452 | syld3an2 1365 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) |
454 | 428, 453 | mpd3an3 1417 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) |
455 | 454 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) |
456 | 285, 287,
288, 291, 455 | fsumlt 14373 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) |
457 | 284, 456 | eqbrtrrd 4607 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) |
458 | 127 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈
ℝ) |
459 | 158 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
460 | 313 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
461 | | ltmul2 10753 |
. . . . . . 7
⊢ ((((1
− (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧
Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))) |
462 | 458, 459,
460, 461 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))) |
463 | 457, 462 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))) |
464 | 121, 129,
160, 233, 463 | lttrd 10077 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))) |
465 | 156, 58 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
466 | 465 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
467 | 466 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) |
468 | 285, 467 | fsumcl 14311 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) |
469 | 468 | addid1d 10115 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
470 | | 0red 9920 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈
ℝ) |
471 | | fzfid 12634 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin) |
472 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ) |
473 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ) |
474 | 126 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ) |
475 | | elfzelz 12213 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ) |
476 | 475 | zred 11358 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ) |
477 | 476 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ) |
478 | | 1m1e0 10966 |
. . . . . . . . . . . . . . 15
⊢ (1
− 1) = 0 |
479 | 122, 114,
122, 365 | lesub1dd 10522 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 − 1) ≤ (𝐿 − 1)) |
480 | 478, 479 | syl5eqbrr 4619 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ (𝐿 − 1)) |
481 | 480 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1)) |
482 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁)) |
483 | 475 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ) |
484 | 379 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ) |
485 | 135 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ) |
486 | | elfz 12203 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧
𝑁 ∈ ℤ) →
(𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
487 | 483, 484,
485, 486 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
488 | 482, 487 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)) |
489 | 488 | simpld 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖) |
490 | 473, 474,
477, 481, 489 | letrd 10073 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖) |
491 | | elfzle2 12216 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ≤ 𝑁) |
492 | 491 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ≤ 𝑁) |
493 | | 0zd 11266 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ) |
494 | | elfz 12203 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑖 ∈
(0...𝑁) ↔ (0 ≤
𝑖 ∧ 𝑖 ≤ 𝑁))) |
495 | 483, 493,
485, 494 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ (0...𝑁) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
496 | 490, 492,
495 | mpbir2and 959 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁)) |
497 | 496, 57 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
498 | 472, 497 | remulcld 9949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
499 | 498 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
500 | 471, 499 | fsumrecl 14312 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
501 | 285, 466 | fsumrecl 14312 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
502 | | fzfid 12634 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin) |
503 | 182 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ) |
504 | 503 | mul01d 10114 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0) |
505 | 496, 106 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)) |
506 | 313 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
507 | | lemul2 10755 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ ((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
508 | 473, 497,
506, 507 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
509 | 505, 508 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))) |
510 | 504, 509 | eqbrtrrd 4607 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))) |
511 | 502, 498,
510 | fsumge0 14368 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
512 | 511 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
513 | 470, 500,
501, 512 | leadd2dd 10521 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
514 | 469, 513 | eqbrtrrd 4607 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
515 | 157 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ) |
516 | 130, 182,
515 | fsummulc2 14358 |
. . . . . 6
⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
517 | 516 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
518 | | stoweidlem26.2 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝜑 |
519 | | elfzelz 12213 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ) |
520 | 519 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ) |
521 | 520 | zred 11358 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ) |
522 | 318 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ) |
523 | 126 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ) |
524 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2))) |
525 | | 0zd 11266 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈
ℤ) |
526 | 134 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ) |
527 | | elfz 12203 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℤ ∧ 0 ∈
ℤ ∧ (𝐿 − 2)
∈ ℤ) → (𝑗
∈ (0...(𝐿 − 2))
↔ (0 ≤ 𝑗 ∧
𝑗 ≤ (𝐿 − 2)))) |
528 | 520, 525,
526, 527 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2)))) |
529 | 524, 528 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))) |
530 | 529 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2)) |
531 | 122, 138,
114 | ltsub2d 10516 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1))) |
532 | 355, 531 | mpbii 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐿 − 2) < (𝐿 − 1)) |
533 | 532 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1)) |
534 | 521, 522,
523, 530, 533 | lelttrd 10074 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1)) |
535 | 521, 523 | ltnled 10063 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗)) |
536 | 534, 535 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗) |
537 | 536 | intnanrd 954 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)) |
538 | 379 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ) |
539 | 135 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ) |
540 | | elfz 12203 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧
𝑁 ∈ ℤ) →
(𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
541 | 520, 538,
539, 540 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
542 | 537, 541 | mtbird 314 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)) |
543 | 542 | ex 449 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))) |
544 | 518, 543 | ralrimi 2940 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)) |
545 | | disj 3969 |
. . . . . . . 8
⊢
(((0...(𝐿 −
2)) ∩ ((𝐿 −
1)...𝑁)) = ∅ ↔
∀𝑗 ∈
(0...(𝐿 − 2)) ¬
𝑗 ∈ ((𝐿 − 1)...𝑁)) |
546 | 544, 545 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅) |
547 | 546 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅) |
548 | 150 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁) |
549 | 134, 378,
135 | 3jca 1235 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ)) |
550 | 549 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ)) |
551 | | elfz 12203 |
. . . . . . . . . 10
⊢ (((𝐿 − 2) ∈ ℤ ∧
0 ∈ ℤ ∧ 𝑁
∈ ℤ) → ((𝐿
− 2) ∈ (0...𝑁)
↔ (0 ≤ (𝐿 −
2) ∧ (𝐿 − 2) ≤
𝑁))) |
552 | 550, 551 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁))) |
553 | 258, 548,
552 | mpbir2and 959 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁)) |
554 | | fzsplit 12238 |
. . . . . . . 8
⊢ ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁))) |
555 | 553, 554 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁))) |
556 | 269, 275,
276 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1)) |
557 | 556 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁)) |
558 | 557 | uneq2d 3729 |
. . . . . . . 8
⊢ (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁))) |
559 | 558 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁))) |
560 | 555, 559 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁))) |
561 | | fzfid 12634 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin) |
562 | 182 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ) |
563 | 57 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ) |
564 | 562, 563 | mulcld 9939 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) |
565 | 564 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) |
566 | 547, 560,
561, 565 | fsumsplit 14318 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
567 | 514, 517,
566 | 3brtr4d 4615 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
568 | 120, 159,
59 | 3jca 1235 |
. . . . . 6
⊢ (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)) |
569 | 568 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)) |
570 | | ltletr 10008 |
. . . . 5
⊢ ((((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
571 | 569, 570 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
572 | 464, 567,
571 | mp2and 711 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
573 | 111, 572 | pm2.61dan 828 |
. 2
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
574 | | sumex 14266 |
. . 3
⊢
Σ𝑖 ∈
(0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V |
575 | 99 | oveq2d 6565 |
. . . . 5
⊢ (𝑡 = 𝑆 → (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘𝑖)‘𝑆))) |
576 | 575 | sumeq2sdv 14282 |
. . . 4
⊢ (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
577 | | eqid 2610 |
. . . 4
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
578 | 576, 577 | fvmptg 6189 |
. . 3
⊢ ((𝑆 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
579 | 55, 574, 578 | sylancl 693 |
. 2
⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
580 | 573, 579 | breqtrrd 4611 |
1
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆)) |