Proof of Theorem stoweidlem26
Step | Hyp | Ref
| Expression |
1 | | 1re 10376 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
2 | | eleq1 2847 |
. . . . . . . 8
⊢ (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈
ℝ)) |
3 | 1, 2 | mpbiri 250 |
. . . . . . 7
⊢ (𝐿 = 1 → 𝐿 ∈ ℝ) |
4 | 3 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℝ) |
5 | | 4re 11460 |
. . . . . . . 8
⊢ 4 ∈
ℝ |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 4 ∈
ℝ) |
7 | | 3re 11455 |
. . . . . . . 8
⊢ 3 ∈
ℝ |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ∈
ℝ) |
9 | | 3ne0 11488 |
. . . . . . . 8
⊢ 3 ≠
0 |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ≠ 0) |
11 | 6, 8, 10 | redivcld 11203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈
ℝ) |
12 | 4, 11 | resubcld 10803 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈
ℝ) |
13 | | stoweidlem26.11 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
14 | 13 | rpred 12181 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℝ) |
15 | 14 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐸 ∈ ℝ) |
16 | 12, 15 | remulcld 10407 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ) |
17 | | 0red 10380 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ∈
ℝ) |
18 | | fzfid 13091 |
. . . . . 6
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
19 | 14 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ) |
20 | | stoweidlem26.13 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ) |
21 | | stoweidlem26.9 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1)))) |
22 | | eldif 3802 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))) |
23 | 21, 22 | sylib 210 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))) |
24 | 23 | simpld 490 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ (𝐷‘𝐿)) |
25 | | stoweidlem26.4 |
. . . . . . . . . . . . 13
⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) |
26 | | oveq1 6929 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3))) |
27 | 26 | oveq1d 6937 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸)) |
28 | 27 | breq2d 4898 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝐿 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸))) |
29 | 28 | rabbidv 3386 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝐿 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)}) |
30 | | fz1ssfz0 12754 |
. . . . . . . . . . . . . 14
⊢
(1...𝑁) ⊆
(0...𝑁) |
31 | | stoweidlem26.8 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) |
32 | 30, 31 | sseldi 3819 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ (0...𝑁)) |
33 | | stoweidlem26.7 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ V) |
34 | | rabexg 5048 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V) |
36 | 25, 29, 32, 35 | fvmptd3 6564 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘𝐿) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)}) |
37 | 24, 36 | eleqtrd 2861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)}) |
38 | | nfcv 2934 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝑆 |
39 | | nfcv 2934 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝑇 |
40 | | stoweidlem26.1 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡𝐹 |
41 | 40, 38 | nffv 6456 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡(𝐹‘𝑆) |
42 | | nfcv 2934 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡
≤ |
43 | | nfcv 2934 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝐿 − (1 / 3)) · 𝐸) |
44 | 41, 42, 43 | nfbr 4933 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡(𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸) |
45 | | fveq2 6446 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑆 → (𝐹‘𝑡) = (𝐹‘𝑆)) |
46 | 45 | breq1d 4896 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸))) |
47 | 38, 39, 44, 46 | elrabf 3568 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸))) |
48 | 37, 47 | sylib 210 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸))) |
49 | 48 | simpld 490 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ 𝑇) |
50 | 49 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑆 ∈ 𝑇) |
51 | 20, 50 | ffvelrnd 6624 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
52 | 19, 51 | remulcld 10407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
53 | 18, 52 | fsumrecl 14872 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
54 | 53 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
55 | 5, 7, 9 | redivcli 11142 |
. . . . . . 7
⊢ (4 / 3)
∈ ℝ |
56 | 55 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈
ℝ) |
57 | 4, 56 | resubcld 10803 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈
ℝ) |
58 | 4 | recnd 10405 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℂ) |
59 | 58 | subid1d 10723 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) = 𝐿) |
60 | | 3cn 11456 |
. . . . . . . . . 10
⊢ 3 ∈
ℂ |
61 | 60, 9 | dividi 11108 |
. . . . . . . . 9
⊢ (3 / 3) =
1 |
62 | | 3lt4 11556 |
. . . . . . . . . 10
⊢ 3 <
4 |
63 | | 3pos 11487 |
. . . . . . . . . . 11
⊢ 0 <
3 |
64 | 7, 5, 7, 63 | ltdiv1ii 11307 |
. . . . . . . . . 10
⊢ (3 < 4
↔ (3 / 3) < (4 / 3)) |
65 | 62, 64 | mpbi 222 |
. . . . . . . . 9
⊢ (3 / 3)
< (4 / 3) |
66 | 61, 65 | eqbrtrri 4909 |
. . . . . . . 8
⊢ 1 < (4
/ 3) |
67 | | breq1 4889 |
. . . . . . . . 9
⊢ (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 /
3))) |
68 | 67 | adantl 475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 /
3))) |
69 | 66, 68 | mpbiri 250 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 < (4 / 3)) |
70 | 59, 69 | eqbrtrd 4908 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) < (4 / 3)) |
71 | 4, 17, 56, 70 | ltsub23d 10980 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) < 0) |
72 | 13 | rpgt0d 12184 |
. . . . . 6
⊢ (𝜑 → 0 < 𝐸) |
73 | 72 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → 0 < 𝐸) |
74 | | mulltgt0 40118 |
. . . . 5
⊢ ((((𝐿 − (4 / 3)) ∈ ℝ
∧ (𝐿 − (4 / 3))
< 0) ∧ (𝐸 ∈
ℝ ∧ 0 < 𝐸))
→ ((𝐿 − (4 / 3))
· 𝐸) <
0) |
75 | 57, 71, 15, 73, 74 | syl22anc 829 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0) |
76 | | 0cn 10368 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
77 | | fsumconst 14926 |
. . . . . . . 8
⊢
(((0...𝑁) ∈ Fin
∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0)) |
78 | 18, 76, 77 | sylancl 580 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0)) |
79 | | hashcl 13462 |
. . . . . . . . 9
⊢
((0...𝑁) ∈ Fin
→ (♯‘(0...𝑁)) ∈
ℕ0) |
80 | | nn0cn 11653 |
. . . . . . . . 9
⊢
((♯‘(0...𝑁)) ∈ ℕ0 →
(♯‘(0...𝑁))
∈ ℂ) |
81 | 18, 79, 80 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(0...𝑁)) ∈
ℂ) |
82 | 81 | mul01d 10575 |
. . . . . . 7
⊢ (𝜑 → ((♯‘(0...𝑁)) · 0) =
0) |
83 | 78, 82 | eqtrd 2814 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0) |
84 | 83 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0) |
85 | | 0red 10380 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ) |
86 | 13 | rpge0d 12185 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐸) |
87 | 86 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸) |
88 | | stoweidlem26.3 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡𝜑 |
89 | | nfv 1957 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑡 𝑖 ∈ (0...𝑁) |
90 | 88, 89 | nfan 1946 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁)) |
91 | | nfv 1957 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡0 ≤
((𝑋‘𝑖)‘𝑆) |
92 | 90, 91 | nfim 1943 |
. . . . . . . . . 10
⊢
Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)) |
93 | | fveq2 6446 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑆 → ((𝑋‘𝑖)‘𝑡) = ((𝑋‘𝑖)‘𝑆)) |
94 | 93 | breq2d 4898 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑆 → (0 ≤ ((𝑋‘𝑖)‘𝑡) ↔ 0 ≤ ((𝑋‘𝑖)‘𝑆))) |
95 | 94 | imbi2d 332 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)))) |
96 | | stoweidlem26.14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) |
97 | 96 | 3expia 1111 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 → 0 ≤ ((𝑋‘𝑖)‘𝑡))) |
98 | 97 | com12 32 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡))) |
99 | 38, 92, 95, 98 | vtoclgaf 3473 |
. . . . . . . . 9
⊢ (𝑆 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))) |
100 | 50, 99 | mpcom 38 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)) |
101 | 19, 51, 87, 100 | mulge0d 10952 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))) |
102 | 18, 85, 52, 101 | fsumle 14935 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
103 | 102 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
104 | 84, 103 | eqbrtrrd 4910 |
. . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
105 | 16, 17, 54, 75, 104 | ltletrd 10536 |
. . 3
⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
106 | | elfzelz 12659 |
. . . . . . . . 9
⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ) |
107 | | zre 11732 |
. . . . . . . . 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 11203 |
. . . . . . . 8
⊢ (𝜑 → (4 / 3) ∈
ℝ) |
113 | 108, 112 | resubcld 10803 |
. . . . . . 7
⊢ (𝜑 → (𝐿 − (4 / 3)) ∈
ℝ) |
114 | 113, 14 | remulcld 10407 |
. . . . . 6
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ) |
115 | 114 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ) |
116 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) |
117 | | stoweidlem26.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
118 | 14, 117 | nndivred 11429 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ) |
119 | 116, 118 | resubcld 10803 |
. . . . . . . 8
⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ) |
120 | 108, 116 | resubcld 10803 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 − 1) ∈ ℝ) |
121 | 119, 120 | remulcld 10407 |
. . . . . . 7
⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈
ℝ) |
122 | 14, 121 | remulcld 10407 |
. . . . . 6
⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈
ℝ) |
123 | 122 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈
ℝ) |
124 | | fzfid 13091 |
. . . . . . . 8
⊢ (𝜑 → (0...(𝐿 − 2)) ∈ Fin) |
125 | 31, 106 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ ℤ) |
126 | | 2z 11761 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
127 | 126 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℤ) |
128 | 125, 127 | zsubcld 11839 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 − 2) ∈ ℤ) |
129 | 117 | nnzd 11833 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) |
130 | 125 | zred 11834 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐿 ∈ ℝ) |
131 | | 2re 11449 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℝ) |
133 | 130, 132 | resubcld 10803 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 − 2) ∈ ℝ) |
134 | 117 | nnred 11391 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
135 | | 0le2 11484 |
. . . . . . . . . . . . . . . 16
⊢ 0 ≤
2 |
136 | | 0red 10380 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ∈
ℝ) |
137 | 136, 132,
130 | lesub2d 10983 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0))) |
138 | 135, 137 | mpbii 225 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0)) |
139 | 125 | zcnd 11835 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐿 ∈ ℂ) |
140 | 139 | subid1d 10723 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐿 − 0) = 𝐿) |
141 | 138, 140 | breqtrd 4912 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 − 2) ≤ 𝐿) |
142 | | elfzle2 12662 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ≤ 𝑁) |
143 | 31, 142 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ≤ 𝑁) |
144 | 133, 130,
134, 141, 143 | letrd 10533 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 − 2) ≤ 𝑁) |
145 | 128, 129,
144 | 3jca 1119 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁)) |
146 | | eluz2 11998 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁)) |
147 | 145, 146 | sylibr 226 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝐿 − 2))) |
148 | | fzss2 12698 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁)) |
149 | 147, 148 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁)) |
150 | 149 | sselda 3821 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁)) |
151 | 150, 51 | syldan 585 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
152 | 124, 151 | fsumrecl 14872 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
153 | 14, 152 | remulcld 10407 |
. . . . . 6
⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
154 | 153 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
155 | 14, 120 | remulcld 10407 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · (𝐿 − 1)) ∈
ℝ) |
156 | 14, 14 | remulcld 10407 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℝ) |
157 | 155, 156 | resubcld 10803 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ) |
158 | 120, 117 | nndivred 11429 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ) |
159 | 156, 158 | remulcld 10407 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ) |
160 | 155, 159 | resubcld 10803 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ) |
161 | 120, 14 | resubcld 10803 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ) |
162 | 116, 14 | readdcld 10406 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 + 𝐸) ∈ ℝ) |
163 | 1, 7, 9 | redivcli 11142 |
. . . . . . . . . . . . . . 15
⊢ (1 / 3)
∈ ℝ |
164 | 163 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / 3) ∈
ℝ) |
165 | | stoweidlem26.12 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 < (1 / 3)) |
166 | 14, 164, 116, 165 | ltadd2dd 10535 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 + 𝐸) < (1 + (1 / 3))) |
167 | | ax-1cn 10330 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
168 | 60, 167, 60, 9 | divdiri 11132 |
. . . . . . . . . . . . . 14
⊢ ((3 + 1)
/ 3) = ((3 / 3) + (1 / 3)) |
169 | | 3p1e4 11527 |
. . . . . . . . . . . . . . 15
⊢ (3 + 1) =
4 |
170 | 169 | oveq1i 6932 |
. . . . . . . . . . . . . 14
⊢ ((3 + 1)
/ 3) = (4 / 3) |
171 | 61 | oveq1i 6932 |
. . . . . . . . . . . . . 14
⊢ ((3 / 3)
+ (1 / 3)) = (1 + (1 / 3)) |
172 | 168, 170,
171 | 3eqtr3ri 2811 |
. . . . . . . . . . . . 13
⊢ (1 + (1 /
3)) = (4 / 3) |
173 | 166, 172 | syl6breq 4927 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 + 𝐸) < (4 / 3)) |
174 | 162, 112,
108, 173 | ltsub2dd 10988 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸))) |
175 | 167 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
176 | 13 | rpcnd 12183 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℂ) |
177 | 139, 175,
176 | subsub4d 10765 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸))) |
178 | 174, 177 | breqtrrd 4914 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸)) |
179 | 113, 161,
13, 178 | ltmul1dd 12236 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸)) |
180 | 139, 175 | subcld 10734 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 − 1) ∈ ℂ) |
181 | 180, 176 | subcld 10734 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ) |
182 | 176, 181 | mulcomd 10398 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸)) |
183 | 176, 180,
176 | subdid 10831 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸))) |
184 | 182, 183 | eqtr3d 2816 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸))) |
185 | 179, 184 | breqtrd 4912 |
. . . . . . . 8
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸))) |
186 | | 1zzd 11760 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℤ) |
187 | | elfz 12649 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℤ ∧ 1 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝐿 ∈
(1...𝑁) ↔ (1 ≤
𝐿 ∧ 𝐿 ≤ 𝑁))) |
188 | 125, 186,
129, 187 | syl3anc 1439 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁))) |
189 | 31, 188 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) |
190 | 189 | simprd 491 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ≤ 𝑁) |
191 | | zlem1lt 11781 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁)) |
192 | 125, 129,
191 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁)) |
193 | 190, 192 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 − 1) < 𝑁) |
194 | 117 | nngt0d 11424 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) |
195 | | ltdiv1 11241 |
. . . . . . . . . . . . . 14
⊢ (((𝐿 − 1) ∈ ℝ ∧
𝑁 ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))) |
196 | 120, 134,
134, 194, 195 | syl112anc 1442 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))) |
197 | 193, 196 | mpbid 224 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)) |
198 | 117 | nncnd 11392 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
199 | 117 | nnne0d 11425 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ 0) |
200 | 198, 199 | dividd 11149 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 / 𝑁) = 1) |
201 | 197, 200 | breqtrd 4912 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < 1) |
202 | 14, 14, 72, 72 | mulgt0d 10531 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝐸 · 𝐸)) |
203 | | ltmul2 11228 |
. . . . . . . . . . . 12
⊢ ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ
∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 <
(𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))) |
204 | 158, 116,
156, 202, 203 | syl112anc 1442 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))) |
205 | 201, 204 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)) |
206 | 176, 176 | mulcld 10397 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℂ) |
207 | 206 | mulid1d 10394 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸)) |
208 | 205, 207 | breqtrd 4912 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸)) |
209 | 159, 156,
155, 208 | ltsub2dd 10988 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) |
210 | 114, 157,
160, 185, 209 | lttrd 10537 |
. . . . . . 7
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) |
211 | 176, 198,
199 | divcld 11151 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℂ) |
212 | 175, 211,
180 | subdird 10832 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1)))) |
213 | 180 | mulid2d 10395 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1)) |
214 | 213 | oveq1d 6937 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) |
215 | 212, 214 | eqtrd 2814 |
. . . . . . . . 9
⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) |
216 | 215 | oveq2d 6938 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))) |
217 | 211, 180 | mulcld 10397 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈
ℂ) |
218 | 176, 180,
217 | subdid 10831 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))))) |
219 | 176, 198,
180, 199 | div32d 11174 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁))) |
220 | 219 | oveq2d 6938 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁)))) |
221 | 180, 198,
199 | divcld 11151 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ) |
222 | 176, 176,
221 | mulassd 10400 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁)))) |
223 | 220, 222 | eqtr4d 2817 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) |
224 | 223 | oveq2d 6938 |
. . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) |
225 | 216, 218,
224 | 3eqtrd 2818 |
. . . . . . 7
⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) |
226 | 210, 225 | breqtrrd 4914 |
. . . . . 6
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))) |
227 | 226 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))) |
228 | 175, 211 | subcld 10734 |
. . . . . . . . . 10
⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ) |
229 | | fsumconst 14926 |
. . . . . . . . . 10
⊢
(((0...(𝐿 −
2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁)))) |
230 | 124, 228,
229 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁)))) |
231 | 230 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁)))) |
232 | | 0zd 11740 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈
ℤ) |
233 | 31 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁)) |
234 | 233, 106 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ) |
235 | 126 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈
ℤ) |
236 | 234, 235 | zsubcld 11839 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ) |
237 | | elnnuz 12030 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
238 | 117, 237 | sylib 210 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) |
239 | | elfzp12 12737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))) |
240 | 238, 239 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))) |
241 | 31, 240 | mpbid 224 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))) |
242 | 241 | orcanai 988 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁)) |
243 | | 1p1e2 11507 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 + 1) =
2 |
244 | 243 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2) |
245 | 244 | oveq1d 6937 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁)) |
246 | 242, 245 | eleqtrd 2861 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁)) |
247 | | elfzle1 12661 |
. . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿) |
248 | 246, 247 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿) |
249 | 108 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ) |
250 | 131 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈
ℝ) |
251 | 249, 250 | subge0d 10965 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿)) |
252 | 248, 251 | mpbird 249 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2)) |
253 | 232, 236,
252 | 3jca 1119 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧
0 ≤ (𝐿 −
2))) |
254 | | eluz2 11998 |
. . . . . . . . . . . 12
⊢ ((𝐿 − 2) ∈
(ℤ≥‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧
0 ≤ (𝐿 −
2))) |
255 | 253, 254 | sylibr 226 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈
(ℤ≥‘0)) |
256 | | hashfz 13528 |
. . . . . . . . . . 11
⊢ ((𝐿 − 2) ∈
(ℤ≥‘0) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) +
1)) |
257 | 255, 256 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) +
1)) |
258 | | 2cn 11450 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
259 | 258 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) |
260 | 139, 259 | subcld 10734 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 − 2) ∈ ℂ) |
261 | 260 | subid1d 10723 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2)) |
262 | 261 | oveq1d 6937 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) +
1)) |
263 | 139, 259,
175 | subadd23d 10756 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2))) |
264 | 258, 167 | negsubdi2i 10709 |
. . . . . . . . . . . . . . . 16
⊢ -(2
− 1) = (1 − 2) |
265 | | 2m1e1 11508 |
. . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 |
266 | 265 | negeqi 10615 |
. . . . . . . . . . . . . . . 16
⊢ -(2
− 1) = -1 |
267 | 264, 266 | eqtr3i 2804 |
. . . . . . . . . . . . . . 15
⊢ (1
− 2) = -1 |
268 | 267 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 − 2) =
-1) |
269 | 268 | oveq2d 6938 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1)) |
270 | 139, 175 | negsubd 10740 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 + -1) = (𝐿 − 1)) |
271 | 269, 270 | eqtrd 2814 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1)) |
272 | 262, 263,
271 | 3eqtrd 2818 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1)) |
273 | 272 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1)) |
274 | 257, 273 | eqtrd 2814 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (𝐿 − 1)) |
275 | 274 | oveq1d 6937 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((♯‘(0...(𝐿 − 2))) · (1
− (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁)))) |
276 | 180, 228 | mulcomd 10398 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) |
277 | 276 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) |
278 | 231, 275,
277 | 3eqtrd 2818 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) |
279 | | fzfid 13091 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin) |
280 | | fzn0 12672 |
. . . . . . . . 9
⊢
((0...(𝐿 − 2))
≠ ∅ ↔ (𝐿
− 2) ∈ (ℤ≥‘0)) |
281 | 255, 280 | sylibr 226 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅) |
282 | 119 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ) |
283 | | simpll 757 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑) |
284 | 150 | adantlr 705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁)) |
285 | 283, 284,
51 | syl2anc 579 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
286 | 49 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ 𝑇) |
287 | | elfzelz 12659 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ) |
288 | 287 | zred 11834 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ) |
289 | 288 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ) |
290 | 163 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈
ℝ) |
291 | 289, 290 | readdcld 10406 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ) |
292 | 14 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ) |
293 | 291, 292 | remulcld 10407 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ) |
294 | 108 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ) |
295 | 131 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈
ℝ) |
296 | 294, 295 | resubcld 10803 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ) |
297 | 296, 290 | readdcld 10406 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈
ℝ) |
298 | 297, 292 | remulcld 10407 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈
ℝ) |
299 | | stoweidlem26.10 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) |
300 | 299, 49 | jca 507 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇)) |
301 | 300 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇)) |
302 | | ffvelrn 6621 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇) → (𝐹‘𝑆) ∈ ℝ) |
303 | 301, 302 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹‘𝑆) ∈ ℝ) |
304 | | elfzle2 12662 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2)) |
305 | 304 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2)) |
306 | 289, 296,
290, 305 | leadd1dd 10989 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3))) |
307 | 14, 72 | jca 507 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
308 | 307 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
309 | | lemul1 11229 |
. . . . . . . . . . . . . . 15
⊢ (((𝑖 + (1 / 3)) ∈ ℝ ∧
((𝐿 − 2) + (1 / 3))
∈ ℝ ∧ (𝐸
∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))) |
310 | 291, 297,
308, 309 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))) |
311 | 306, 310 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)) |
312 | 108, 132 | resubcld 10803 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐿 − 2) ∈ ℝ) |
313 | 312, 164 | readdcld 10406 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈
ℝ) |
314 | 313, 14 | remulcld 10407 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈
ℝ) |
315 | 299, 49 | ffvelrnd 6624 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ) |
316 | 120, 164 | resubcld 10803 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈
ℝ) |
317 | 316, 14 | remulcld 10407 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈
ℝ) |
318 | | addid1 10556 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
ℂ → (1 + 0) = 1) |
319 | 318 | eqcomd 2784 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 ∈
ℂ → 1 = (1 + 0)) |
320 | 167, 319 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 = (1 +
0)) |
321 | 175 | subidd 10722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (1 − 1) =
0) |
322 | 321 | eqcomd 2784 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 0 = (1 −
1)) |
323 | 322 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 + 0) = (1 + (1 −
1))) |
324 | | addsubass 10633 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1)
− 1) = (1 + (1 − 1))) |
325 | 324 | eqcomd 2784 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1
− 1)) = ((1 + 1) − 1)) |
326 | 175, 175,
175, 325 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 + (1 − 1)) = ((1
+ 1) − 1)) |
327 | 320, 323,
326 | 3eqtrd 2818 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 = ((1 + 1) −
1)) |
328 | 327 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) −
1))) |
329 | 243 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 + 1) =
2) |
330 | 329 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1 + 1) − 1) = (2
− 1)) |
331 | 330 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 −
1))) |
332 | 139, 259,
175 | subsubd 10762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) +
1)) |
333 | 328, 331,
332 | 3eqtrd 2818 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1)) |
334 | 333 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 /
3))) |
335 | 258, 60, 9 | divcli 11117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2 / 3)
∈ ℂ |
336 | 335 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2 / 3) ∈
ℂ) |
337 | 260, 175,
336 | addsubassd 10754 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 /
3)))) |
338 | 167, 60, 9 | divcli 11117 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 / 3)
∈ ℂ |
339 | | df-3 11439 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 = (2 +
1) |
340 | 339 | oveq1i 6932 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (3 / 3) =
((2 + 1) / 3) |
341 | 258, 167,
60, 9 | divdiri 11132 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2 + 1)
/ 3) = ((2 / 3) + (1 / 3)) |
342 | 340, 61, 341 | 3eqtr3ri 2811 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2 / 3)
+ (1 / 3)) = 1 |
343 | 167, 335,
338, 342 | subaddrii 10712 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1
− (2 / 3)) = (1 / 3) |
344 | 343 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 − (2 / 3)) = (1 /
3)) |
345 | 344 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 /
3))) |
346 | 334, 337,
345 | 3eqtrd 2818 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 /
3))) |
347 | 131, 7, 9 | redivcli 11142 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 / 3)
∈ ℝ |
348 | 347 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2 / 3) ∈
ℝ) |
349 | | 1lt2 11553 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
2 |
350 | 7, 63 | pm3.2i 464 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (3 ∈
ℝ ∧ 0 < 3) |
351 | 1, 131, 350 | 3pm3.2i 1395 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 <
3)) |
352 | | ltdiv1 11241 |
. . . . . . . . . . . . . . . . . . . . 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 225 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 / 3) < (2 /
3)) |
355 | 164, 348,
120, 354 | ltsub2dd 10988 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 /
3))) |
356 | 346, 355 | eqbrtrrd 4910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 /
3))) |
357 | 313, 316,
13, 356 | ltmul1dd 12236 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸)) |
358 | 23 | simprd 491 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))) |
359 | | oveq1 6929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 /
3))) |
360 | 359 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸)) |
361 | 360 | breq2d 4898 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = (𝐿 − 1) → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
362 | 361 | rabbidv 3386 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = (𝐿 − 1) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)}) |
363 | 189 | simpld 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 1 ≤ 𝐿) |
364 | 134, 116 | readdcld 10406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) |
365 | 134 | lep1d 11309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1)) |
366 | 108, 134,
364, 190, 365 | letrd 10533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐿 ≤ (𝑁 + 1)) |
367 | 129 | peano2zd 11837 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
368 | | elfz 12649 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐿 ∈ ℤ ∧ 1 ∈
ℤ ∧ (𝑁 + 1)
∈ ℤ) → (𝐿
∈ (1...(𝑁 + 1)) ↔
(1 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 + 1)))) |
369 | 125, 186,
367, 368 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐿 ∈ (1...(𝑁 + 1)) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 + 1)))) |
370 | 363, 366,
369 | mpbir2and 703 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐿 ∈ (1...(𝑁 + 1))) |
371 | 139, 175 | npcand 10738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝐿 − 1) + 1) = 𝐿) |
372 | | 0p1e1 11504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0 + 1) =
1 |
373 | 372 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (0 + 1) =
1) |
374 | 373 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))) |
375 | 370, 371,
374 | 3eltr4d 2874 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))) |
376 | | 0zd 11740 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ∈
ℤ) |
377 | 125, 186 | zsubcld 11839 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐿 − 1) ∈ ℤ) |
378 | | fzaddel 12692 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((0
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ ((𝐿
− 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))) |
379 | 376, 129,
377, 186, 378 | syl22anc 829 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))) |
380 | 375, 379 | mpbird 249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐿 − 1) ∈ (0...𝑁)) |
381 | | rabexg 5048 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V) |
382 | 33, 381 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V) |
383 | 25, 362, 380, 382 | fvmptd3 6564 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)}) |
384 | 358, 383 | neleqtrd 2880 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)}) |
385 | | nfcv 2934 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸) |
386 | 41, 42, 385 | nfbr 4933 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑡(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) |
387 | 45 | breq1d 4896 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
388 | 38, 39, 386, 387 | elrabf 3568 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
389 | 384, 388 | sylnib 320 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
390 | | ianor 967 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
391 | 389, 390 | sylib 210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
392 | | olc 857 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ 𝑇 → (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇)) |
393 | 392 | anim1i 608 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ 𝑇 ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))) |
394 | 49, 391, 393 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))) |
395 | | orcom 859 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)) |
396 | 395 | anbi2i 616 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((¬
(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))) |
397 | 394, 396 | sylib 210 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))) |
398 | | pm4.43 1008 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))) |
399 | 397, 398 | sylibr 226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) |
400 | 317, 315 | ltnled 10523 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆) ↔ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) |
401 | 399, 400 | mpbird 249 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆)) |
402 | 314, 317,
315, 357, 401 | lttrd 10537 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹‘𝑆)) |
403 | 314, 315,
402 | ltled 10524 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)) |
404 | 403 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)) |
405 | 293, 298,
303, 311, 404 | letrd 10533 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)) |
406 | | nfcv 2934 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) |
407 | 406, 42, 41 | nfbr 4933 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆) |
408 | 45 | breq2d 4898 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))) |
409 | 38, 39, 407, 408 | elrabf 3568 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑆 ∈ 𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))) |
410 | 286, 405,
409 | sylanbrc 578 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
411 | | stoweidlem26.5 |
. . . . . . . . . . . 12
⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
412 | | oveq1 6929 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3))) |
413 | 412 | oveq1d 6937 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸)) |
414 | 413 | breq1d 4896 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡))) |
415 | 414 | rabbidv 3386 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
416 | | rabexg 5048 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) |
417 | 33, 416 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) |
418 | 417 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) |
419 | 411, 415,
150, 418 | fvmptd3 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐵‘𝑖) = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
420 | 410, 419 | eleqtrrd 2862 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵‘𝑖)) |
421 | 145 | 3ad2ant1 1124 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁)) |
422 | 421, 146 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑁 ∈ (ℤ≥‘(𝐿 − 2))) |
423 | 422, 148 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁)) |
424 | | simp2 1128 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...(𝐿 − 2))) |
425 | 423, 424 | sseldd 3822 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...𝑁)) |
426 | | elex 3414 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (𝐵‘𝑖) → 𝑆 ∈ V) |
427 | 426 | 3ad2ant3 1126 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑆 ∈ V) |
428 | | nfcv 2934 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡(0...𝑁) |
429 | | nfrab1 3309 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} |
430 | 428, 429 | nfmpt 4981 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) |
431 | 411, 430 | nfcxfr 2932 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝐵 |
432 | | nfcv 2934 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝑖 |
433 | 431, 432 | nffv 6456 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡(𝐵‘𝑖) |
434 | 433 | nfel2 2950 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡 𝑆 ∈ (𝐵‘𝑖) |
435 | 88, 89, 434 | nf3an 1948 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) |
436 | | nfv 1957 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(1 −
(𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆) |
437 | 435, 436 | nfim 1943 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) |
438 | | eleq1 2847 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑆 → (𝑡 ∈ (𝐵‘𝑖) ↔ 𝑆 ∈ (𝐵‘𝑖))) |
439 | 438 | 3anbi3d 1515 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑆 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)))) |
440 | 93 | breq2d 4898 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))) |
441 | 439, 440 | imbi12d 336 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))) |
442 | | stoweidlem26.15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) |
443 | 437, 441,
442 | vtoclg1f 3466 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ V → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))) |
444 | 427, 443 | mpcom 38 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) |
445 | 425, 444 | syld3an2 1480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) |
446 | 420, 445 | mpd3an3 1535 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) |
447 | 446 | adantlr 705 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) |
448 | 279, 281,
282, 285, 447 | fsumlt 14936 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) |
449 | 278, 448 | eqbrtrrd 4910 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) |
450 | 121 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈
ℝ) |
451 | 152 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
452 | 307 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
453 | | ltmul2 11228 |
. . . . . . 7
⊢ ((((1
− (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧
Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))) |
454 | 450, 451,
452, 453 | syl3anc 1439 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))) |
455 | 449, 454 | mpbid 224 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))) |
456 | 115, 123,
154, 227, 455 | lttrd 10537 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))) |
457 | 150, 52 | syldan 585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
458 | 457 | adantlr 705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
459 | 458 | recnd 10405 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) |
460 | 279, 459 | fsumcl 14871 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) |
461 | 460 | addid1d 10576 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
462 | | 0red 10380 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈
ℝ) |
463 | | fzfid 13091 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin) |
464 | 14 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ) |
465 | | 0red 10380 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ) |
466 | 120 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ) |
467 | | elfzelz 12659 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ) |
468 | 467 | zred 11834 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ) |
469 | 468 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ) |
470 | | 1m1e0 11447 |
. . . . . . . . . . . . . . 15
⊢ (1
− 1) = 0 |
471 | 116, 108,
116, 363 | lesub1dd 10991 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 − 1) ≤ (𝐿 − 1)) |
472 | 470, 471 | syl5eqbrr 4922 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ (𝐿 − 1)) |
473 | 472 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1)) |
474 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁)) |
475 | 467 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ) |
476 | 377 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ) |
477 | 129 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ) |
478 | | elfz 12649 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧
𝑁 ∈ ℤ) →
(𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
479 | 475, 476,
477, 478 | syl3anc 1439 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
480 | 474, 479 | mpbid 224 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)) |
481 | 480 | simpld 490 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖) |
482 | 465, 466,
469, 473, 481 | letrd 10533 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖) |
483 | | elfzle2 12662 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ≤ 𝑁) |
484 | 483 | adantl 475 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ≤ 𝑁) |
485 | | 0zd 11740 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ) |
486 | | elfz 12649 |
. . . . . . . . . . . . 13
⊢ ((𝑖 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝑖 ∈
(0...𝑁) ↔ (0 ≤
𝑖 ∧ 𝑖 ≤ 𝑁))) |
487 | 475, 485,
477, 486 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ (0...𝑁) ↔ (0 ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) |
488 | 482, 484,
487 | mpbir2and 703 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁)) |
489 | 488, 51 | syldan 585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) |
490 | 464, 489 | remulcld 10407 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
491 | 490 | adantlr 705 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
492 | 463, 491 | fsumrecl 14872 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
493 | 279, 458 | fsumrecl 14872 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) |
494 | | fzfid 13091 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin) |
495 | 176 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ) |
496 | 495 | mul01d 10575 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0) |
497 | 488, 100 | syldan 585 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)) |
498 | 307 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) |
499 | | lemul2 11230 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ ((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
500 | 465, 489,
498, 499 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
501 | 497, 500 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))) |
502 | 496, 501 | eqbrtrrd 4910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))) |
503 | 494, 490,
502 | fsumge0 14931 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
504 | 503 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
505 | 462, 492,
493, 504 | leadd2dd 10990 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
506 | 461, 505 | eqbrtrrd 4910 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
507 | 151 | recnd 10405 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ) |
508 | 124, 176,
507 | fsummulc2 14920 |
. . . . . 6
⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
509 | 508 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
510 | | stoweidlem26.2 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝜑 |
511 | | elfzelz 12659 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ) |
512 | 511 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ) |
513 | 512 | zred 11834 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ) |
514 | 312 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ) |
515 | 120 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ) |
516 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2))) |
517 | | 0zd 11740 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈
ℤ) |
518 | 128 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ) |
519 | | elfz 12649 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℤ ∧ 0 ∈
ℤ ∧ (𝐿 − 2)
∈ ℤ) → (𝑗
∈ (0...(𝐿 − 2))
↔ (0 ≤ 𝑗 ∧
𝑗 ≤ (𝐿 − 2)))) |
520 | 512, 517,
518, 519 | syl3anc 1439 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2)))) |
521 | 516, 520 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))) |
522 | 521 | simprd 491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2)) |
523 | 116, 132,
108 | ltsub2d 10985 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1))) |
524 | 349, 523 | mpbii 225 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐿 − 2) < (𝐿 − 1)) |
525 | 524 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1)) |
526 | 513, 514,
515, 522, 525 | lelttrd 10534 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1)) |
527 | 513, 515 | ltnled 10523 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗)) |
528 | 526, 527 | mpbid 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗) |
529 | 528 | intnanrd 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)) |
530 | 377 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ) |
531 | 129 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ) |
532 | | elfz 12649 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧
𝑁 ∈ ℤ) →
(𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
533 | 512, 530,
531, 532 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) |
534 | 529, 533 | mtbird 317 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)) |
535 | 534 | ex 403 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))) |
536 | 510, 535 | ralrimi 3139 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)) |
537 | | disj 4242 |
. . . . . . . 8
⊢
(((0...(𝐿 −
2)) ∩ ((𝐿 −
1)...𝑁)) = ∅ ↔
∀𝑗 ∈
(0...(𝐿 − 2)) ¬
𝑗 ∈ ((𝐿 − 1)...𝑁)) |
538 | 536, 537 | sylibr 226 |
. . . . . . 7
⊢ (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅) |
539 | 538 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅) |
540 | 144 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁) |
541 | 128, 376,
129 | 3jca 1119 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ)) |
542 | 541 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ)) |
543 | | elfz 12649 |
. . . . . . . . . 10
⊢ (((𝐿 − 2) ∈ ℤ ∧
0 ∈ ℤ ∧ 𝑁
∈ ℤ) → ((𝐿
− 2) ∈ (0...𝑁)
↔ (0 ≤ (𝐿 −
2) ∧ (𝐿 − 2) ≤
𝑁))) |
544 | 542, 543 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁))) |
545 | 252, 540,
544 | mpbir2and 703 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁)) |
546 | | fzsplit 12684 |
. . . . . . . 8
⊢ ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁))) |
547 | 545, 546 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁))) |
548 | 263, 269,
270 | 3eqtrd 2818 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1)) |
549 | 548 | oveq1d 6937 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁)) |
550 | 549 | uneq2d 3990 |
. . . . . . . 8
⊢ (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁))) |
551 | 550 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁))) |
552 | 547, 551 | eqtrd 2814 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁))) |
553 | | fzfid 13091 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin) |
554 | 176 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ) |
555 | 51 | recnd 10405 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ) |
556 | 554, 555 | mulcld 10397 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) |
557 | 556 | adantlr 705 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) |
558 | 539, 552,
553, 557 | fsumsplit 14878 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
559 | 506, 509,
558 | 3brtr4d 4918 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
560 | 114, 153,
53 | 3jca 1119 |
. . . . . 6
⊢ (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)) |
561 | 560 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)) |
562 | | ltletr 10468 |
. . . . 5
⊢ ((((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
563 | 561, 562 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) |
564 | 456, 559,
563 | mp2and 689 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
565 | 105, 564 | pm2.61dan 803 |
. 2
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
566 | | sumex 14826 |
. . 3
⊢
Σ𝑖 ∈
(0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V |
567 | 93 | oveq2d 6938 |
. . . . 5
⊢ (𝑡 = 𝑆 → (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘𝑖)‘𝑆))) |
568 | 567 | sumeq2sdv 14842 |
. . . 4
⊢ (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
569 | | eqid 2778 |
. . . 4
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
570 | 568, 569 | fvmptg 6540 |
. . 3
⊢ ((𝑆 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
571 | 49, 566, 570 | sylancl 580 |
. 2
⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) |
572 | 565, 571 | breqtrrd 4914 |
1
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆)) |