Proof of Theorem stoweidlem26
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1re 11261 | . . . . . . . 8
⊢ 1 ∈
ℝ | 
| 2 |  | eleq1 2829 | . . . . . . . 8
⊢ (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈
ℝ)) | 
| 3 | 1, 2 | mpbiri 258 | . . . . . . 7
⊢ (𝐿 = 1 → 𝐿 ∈ ℝ) | 
| 4 | 3 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℝ) | 
| 5 |  | 4re 12350 | . . . . . . . 8
⊢ 4 ∈
ℝ | 
| 6 | 5 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 4 ∈
ℝ) | 
| 7 |  | 3re 12346 | . . . . . . . 8
⊢ 3 ∈
ℝ | 
| 8 | 7 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ∈
ℝ) | 
| 9 |  | 3ne0 12372 | . . . . . . . 8
⊢ 3 ≠
0 | 
| 10 | 9 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 3 ≠ 0) | 
| 11 | 6, 8, 10 | redivcld 12095 | . . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈
ℝ) | 
| 12 | 4, 11 | resubcld 11691 | . . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈
ℝ) | 
| 13 |  | stoweidlem26.11 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 14 | 13 | rpred 13077 | . . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 15 | 14 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐸 ∈ ℝ) | 
| 16 | 12, 15 | remulcld 11291 | . . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ) | 
| 17 |  | 0red 11264 | . . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ∈
ℝ) | 
| 18 |  | fzfid 14014 | . . . . . 6
⊢ (𝜑 → (0...𝑁) ∈ Fin) | 
| 19 | 14 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ) | 
| 20 |  | stoweidlem26.13 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ) | 
| 21 |  | stoweidlem26.9 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1)))) | 
| 22 |  | eldif 3961 | . . . . . . . . . . . . . 14
⊢ (𝑆 ∈ ((𝐷‘𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))) | 
| 23 | 21, 22 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∈ (𝐷‘𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))) | 
| 24 | 23 | simpld 494 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ (𝐷‘𝐿)) | 
| 25 |  | stoweidlem26.4 | . . . . . . . . . . . . 13
⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) | 
| 26 |  | oveq1 7438 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3))) | 
| 27 | 26 | oveq1d 7446 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸)) | 
| 28 | 27 | breq2d 5155 | . . . . . . . . . . . . . 14
⊢ (𝑗 = 𝐿 → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸))) | 
| 29 | 28 | rabbidv 3444 | . . . . . . . . . . . . 13
⊢ (𝑗 = 𝐿 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)}) | 
| 30 |  | fz1ssfz0 13663 | . . . . . . . . . . . . . 14
⊢
(1...𝑁) ⊆
(0...𝑁) | 
| 31 |  | stoweidlem26.8 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) | 
| 32 | 30, 31 | sselid 3981 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐿 ∈ (0...𝑁)) | 
| 33 |  | stoweidlem26.7 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ V) | 
| 34 |  | rabexg 5337 | . . . . . . . . . . . . . 14
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V) | 
| 35 | 33, 34 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V) | 
| 36 | 25, 29, 32, 35 | fvmptd3 7039 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘𝐿) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)}) | 
| 37 | 24, 36 | eleqtrd 2843 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)}) | 
| 38 |  | nfcv 2905 | . . . . . . . . . . . 12
⊢
Ⅎ𝑡𝑆 | 
| 39 |  | nfcv 2905 | . . . . . . . . . . . 12
⊢
Ⅎ𝑡𝑇 | 
| 40 |  | stoweidlem26.1 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑡𝐹 | 
| 41 | 40, 38 | nffv 6916 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑡(𝐹‘𝑆) | 
| 42 |  | nfcv 2905 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑡
≤ | 
| 43 |  | nfcv 2905 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝐿 − (1 / 3)) · 𝐸) | 
| 44 | 41, 42, 43 | nfbr 5190 | . . . . . . . . . . . 12
⊢
Ⅎ𝑡(𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸) | 
| 45 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑆 → (𝐹‘𝑡) = (𝐹‘𝑆)) | 
| 46 | 45 | breq1d 5153 | . . . . . . . . . . . 12
⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸))) | 
| 47 | 38, 39, 44, 46 | elrabf 3688 | . . . . . . . . . . 11
⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸))) | 
| 48 | 37, 47 | sylib 218 | . . . . . . . . . 10
⊢ (𝜑 → (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸))) | 
| 49 | 48 | simpld 494 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ 𝑇) | 
| 50 | 49 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑆 ∈ 𝑇) | 
| 51 | 20, 50 | ffvelcdmd 7105 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) | 
| 52 | 19, 51 | remulcld 11291 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 53 | 18, 52 | fsumrecl 15770 | . . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 54 | 53 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 55 | 5, 7, 9 | redivcli 12034 | . . . . . . 7
⊢ (4 / 3)
∈ ℝ | 
| 56 | 55 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → (4 / 3) ∈
ℝ) | 
| 57 | 4, 56 | resubcld 11691 | . . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) ∈
ℝ) | 
| 58 | 4 | recnd 11289 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 ∈ ℂ) | 
| 59 | 58 | subid1d 11609 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) = 𝐿) | 
| 60 |  | 3cn 12347 | . . . . . . . . . 10
⊢ 3 ∈
ℂ | 
| 61 | 60, 9 | dividi 12000 | . . . . . . . . 9
⊢ (3 / 3) =
1 | 
| 62 |  | 3lt4 12440 | . . . . . . . . . 10
⊢ 3 <
4 | 
| 63 |  | 3pos 12371 | . . . . . . . . . . 11
⊢ 0 <
3 | 
| 64 | 7, 5, 7, 63 | ltdiv1ii 12197 | . . . . . . . . . 10
⊢ (3 < 4
↔ (3 / 3) < (4 / 3)) | 
| 65 | 62, 64 | mpbi 230 | . . . . . . . . 9
⊢ (3 / 3)
< (4 / 3) | 
| 66 | 61, 65 | eqbrtrri 5166 | . . . . . . . 8
⊢ 1 < (4
/ 3) | 
| 67 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 /
3))) | 
| 68 | 67 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 /
3))) | 
| 69 | 66, 68 | mpbiri 258 | . . . . . . 7
⊢ ((𝜑 ∧ 𝐿 = 1) → 𝐿 < (4 / 3)) | 
| 70 | 59, 69 | eqbrtrd 5165 | . . . . . 6
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − 0) < (4 / 3)) | 
| 71 | 4, 17, 56, 70 | ltsub23d 11868 | . . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → (𝐿 − (4 / 3)) < 0) | 
| 72 | 13 | rpgt0d 13080 | . . . . . 6
⊢ (𝜑 → 0 < 𝐸) | 
| 73 | 72 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → 0 < 𝐸) | 
| 74 |  | mulltgt0 45027 | . . . . 5
⊢ ((((𝐿 − (4 / 3)) ∈ ℝ
∧ (𝐿 − (4 / 3))
< 0) ∧ (𝐸 ∈
ℝ ∧ 0 < 𝐸))
→ ((𝐿 − (4 / 3))
· 𝐸) <
0) | 
| 75 | 57, 71, 15, 73, 74 | syl22anc 839 | . . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0) | 
| 76 |  | 0cn 11253 | . . . . . . . 8
⊢ 0 ∈
ℂ | 
| 77 |  | fsumconst 15826 | . . . . . . . 8
⊢
(((0...𝑁) ∈ Fin
∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0)) | 
| 78 | 18, 76, 77 | sylancl 586 | . . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0)) | 
| 79 |  | hashcl 14395 | . . . . . . . . 9
⊢
((0...𝑁) ∈ Fin
→ (♯‘(0...𝑁)) ∈
ℕ0) | 
| 80 |  | nn0cn 12536 | . . . . . . . . 9
⊢
((♯‘(0...𝑁)) ∈ ℕ0 →
(♯‘(0...𝑁))
∈ ℂ) | 
| 81 | 18, 79, 80 | 3syl 18 | . . . . . . . 8
⊢ (𝜑 → (♯‘(0...𝑁)) ∈
ℂ) | 
| 82 | 81 | mul01d 11460 | . . . . . . 7
⊢ (𝜑 → ((♯‘(0...𝑁)) · 0) =
0) | 
| 83 | 78, 82 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0) | 
| 84 | 83 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0) | 
| 85 |  | 0red 11264 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ) | 
| 86 | 13 | rpge0d 13081 | . . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝐸) | 
| 87 | 86 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸) | 
| 88 |  | stoweidlem26.3 | . . . . . . . . . . . 12
⊢
Ⅎ𝑡𝜑 | 
| 89 |  | nfv 1914 | . . . . . . . . . . . 12
⊢
Ⅎ𝑡 𝑖 ∈ (0...𝑁) | 
| 90 | 88, 89 | nfan 1899 | . . . . . . . . . . 11
⊢
Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁)) | 
| 91 |  | nfv 1914 | . . . . . . . . . . 11
⊢
Ⅎ𝑡0 ≤
((𝑋‘𝑖)‘𝑆) | 
| 92 | 90, 91 | nfim 1896 | . . . . . . . . . 10
⊢
Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)) | 
| 93 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑡 = 𝑆 → ((𝑋‘𝑖)‘𝑡) = ((𝑋‘𝑖)‘𝑆)) | 
| 94 | 93 | breq2d 5155 | . . . . . . . . . . 11
⊢ (𝑡 = 𝑆 → (0 ≤ ((𝑋‘𝑖)‘𝑡) ↔ 0 ≤ ((𝑋‘𝑖)‘𝑆))) | 
| 95 | 94 | imbi2d 340 | . . . . . . . . . 10
⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)))) | 
| 96 |  | stoweidlem26.14 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ 𝑇) → 0 ≤ ((𝑋‘𝑖)‘𝑡)) | 
| 97 | 96 | 3expia 1122 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 → 0 ≤ ((𝑋‘𝑖)‘𝑡))) | 
| 98 | 97 | com12 32 | . . . . . . . . . 10
⊢ (𝑡 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑡))) | 
| 99 | 38, 92, 95, 98 | vtoclgaf 3576 | . . . . . . . . 9
⊢ (𝑆 ∈ 𝑇 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆))) | 
| 100 | 50, 99 | mpcom 38 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)) | 
| 101 | 19, 51, 87, 100 | mulge0d 11840 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 102 | 18, 85, 52, 101 | fsumle 15835 | . . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 103 | 102 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 104 | 84, 103 | eqbrtrrd 5167 | . . . 4
⊢ ((𝜑 ∧ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 105 | 16, 17, 54, 75, 104 | ltletrd 11421 | . . 3
⊢ ((𝜑 ∧ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 106 |  | elfzelz 13564 | . . . . . . . . 9
⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ) | 
| 107 |  | zre 12617 | . . . . . . . . 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 12095 | . . . . . . . 8
⊢ (𝜑 → (4 / 3) ∈
ℝ) | 
| 113 | 108, 112 | resubcld 11691 | . . . . . . 7
⊢ (𝜑 → (𝐿 − (4 / 3)) ∈
ℝ) | 
| 114 | 113, 14 | remulcld 11291 | . . . . . 6
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ) | 
| 115 | 114 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ) | 
| 116 | 1 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℝ) | 
| 117 |  | stoweidlem26.6 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 118 | 14, 117 | nndivred 12320 | . . . . . . . . 9
⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ) | 
| 119 | 116, 118 | resubcld 11691 | . . . . . . . 8
⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ) | 
| 120 | 108, 116 | resubcld 11691 | . . . . . . . 8
⊢ (𝜑 → (𝐿 − 1) ∈ ℝ) | 
| 121 | 119, 120 | remulcld 11291 | . . . . . . 7
⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈
ℝ) | 
| 122 | 14, 121 | remulcld 11291 | . . . . . 6
⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈
ℝ) | 
| 123 | 122 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈
ℝ) | 
| 124 |  | fzfid 14014 | . . . . . . . 8
⊢ (𝜑 → (0...(𝐿 − 2)) ∈ Fin) | 
| 125 | 31 | elfzelzd 13565 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ∈ ℤ) | 
| 126 |  | 2z 12649 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ | 
| 127 | 126 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℤ) | 
| 128 | 125, 127 | zsubcld 12727 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 − 2) ∈ ℤ) | 
| 129 | 117 | nnzd 12640 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 130 | 125 | zred 12722 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐿 ∈ ℝ) | 
| 131 |  | 2re 12340 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ | 
| 132 | 131 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℝ) | 
| 133 | 130, 132 | resubcld 11691 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 − 2) ∈ ℝ) | 
| 134 | 117 | nnred 12281 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 135 |  | 0le2 12368 | . . . . . . . . . . . . . . . 16
⊢ 0 ≤
2 | 
| 136 |  | 0red 11264 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ∈
ℝ) | 
| 137 | 136, 132,
130 | lesub2d 11871 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0))) | 
| 138 | 135, 137 | mpbii 233 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0)) | 
| 139 | 125 | zcnd 12723 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐿 ∈ ℂ) | 
| 140 | 139 | subid1d 11609 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐿 − 0) = 𝐿) | 
| 141 | 138, 140 | breqtrd 5169 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 − 2) ≤ 𝐿) | 
| 142 |  | elfzle2 13568 | . . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ (1...𝑁) → 𝐿 ≤ 𝑁) | 
| 143 | 31, 142 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ≤ 𝑁) | 
| 144 | 133, 130,
134, 141, 143 | letrd 11418 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 − 2) ≤ 𝑁) | 
| 145 | 128, 129,
144 | 3jca 1129 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁)) | 
| 146 |  | eluz2 12884 | . . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁)) | 
| 147 | 145, 146 | sylibr 234 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝐿 − 2))) | 
| 148 |  | fzss2 13604 | . . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁)) | 
| 149 | 147, 148 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁)) | 
| 150 | 149 | sselda 3983 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁)) | 
| 151 | 150, 51 | syldan 591 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) | 
| 152 | 124, 151 | fsumrecl 15770 | . . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ) | 
| 153 | 14, 152 | remulcld 11291 | . . . . . 6
⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 154 | 153 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 155 | 14, 120 | remulcld 11291 | . . . . . . . . 9
⊢ (𝜑 → (𝐸 · (𝐿 − 1)) ∈
ℝ) | 
| 156 | 14, 14 | remulcld 11291 | . . . . . . . . 9
⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℝ) | 
| 157 | 155, 156 | resubcld 11691 | . . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ) | 
| 158 | 120, 117 | nndivred 12320 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ) | 
| 159 | 156, 158 | remulcld 11291 | . . . . . . . . 9
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ) | 
| 160 | 155, 159 | resubcld 11691 | . . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ) | 
| 161 | 120, 14 | resubcld 11691 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ) | 
| 162 | 116, 14 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → (1 + 𝐸) ∈ ℝ) | 
| 163 | 1, 7, 9 | redivcli 12034 | . . . . . . . . . . . . . . 15
⊢ (1 / 3)
∈ ℝ | 
| 164 | 163 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1 / 3) ∈
ℝ) | 
| 165 |  | stoweidlem26.12 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐸 < (1 / 3)) | 
| 166 | 14, 164, 116, 165 | ltadd2dd 11420 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1 + 𝐸) < (1 + (1 / 3))) | 
| 167 |  | ax-1cn 11213 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ | 
| 168 | 60, 167, 60, 9 | divdiri 12024 | . . . . . . . . . . . . . 14
⊢ ((3 + 1)
/ 3) = ((3 / 3) + (1 / 3)) | 
| 169 |  | 3p1e4 12411 | . . . . . . . . . . . . . . 15
⊢ (3 + 1) =
4 | 
| 170 | 169 | oveq1i 7441 | . . . . . . . . . . . . . 14
⊢ ((3 + 1)
/ 3) = (4 / 3) | 
| 171 | 61 | oveq1i 7441 | . . . . . . . . . . . . . 14
⊢ ((3 / 3)
+ (1 / 3)) = (1 + (1 / 3)) | 
| 172 | 168, 170,
171 | 3eqtr3ri 2774 | . . . . . . . . . . . . 13
⊢ (1 + (1 /
3)) = (4 / 3) | 
| 173 | 166, 172 | breqtrdi 5184 | . . . . . . . . . . . 12
⊢ (𝜑 → (1 + 𝐸) < (4 / 3)) | 
| 174 | 162, 112,
108, 173 | ltsub2dd 11876 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸))) | 
| 175 | 167 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) | 
| 176 | 13 | rpcnd 13079 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 177 | 139, 175,
176 | subsub4d 11651 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸))) | 
| 178 | 174, 177 | breqtrrd 5171 | . . . . . . . . . 10
⊢ (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸)) | 
| 179 | 113, 161,
13, 178 | ltmul1dd 13132 | . . . . . . . . 9
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸)) | 
| 180 | 139, 175 | subcld 11620 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 − 1) ∈ ℂ) | 
| 181 | 180, 176 | subcld 11620 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ) | 
| 182 | 176, 181 | mulcomd 11282 | . . . . . . . . . 10
⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸)) | 
| 183 | 176, 180,
176 | subdid 11719 | . . . . . . . . . 10
⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸))) | 
| 184 | 182, 183 | eqtr3d 2779 | . . . . . . . . 9
⊢ (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸))) | 
| 185 | 179, 184 | breqtrd 5169 | . . . . . . . 8
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸))) | 
| 186 |  | 1zzd 12648 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℤ) | 
| 187 |  | elfz 13553 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐿 ∈ ℤ ∧ 1 ∈
ℤ ∧ 𝑁 ∈
ℤ) → (𝐿 ∈
(1...𝑁) ↔ (1 ≤
𝐿 ∧ 𝐿 ≤ 𝑁))) | 
| 188 | 125, 186,
129, 187 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁))) | 
| 189 | 31, 188 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁)) | 
| 190 | 189 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿 ≤ 𝑁) | 
| 191 |  | zlem1lt 12669 | . . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁)) | 
| 192 | 125, 129,
191 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 ≤ 𝑁 ↔ (𝐿 − 1) < 𝑁)) | 
| 193 | 190, 192 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 − 1) < 𝑁) | 
| 194 | 117 | nngt0d 12315 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) | 
| 195 |  | ltdiv1 12132 | . . . . . . . . . . . . . 14
⊢ (((𝐿 − 1) ∈ ℝ ∧
𝑁 ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))) | 
| 196 | 120, 134,
134, 194, 195 | syl112anc 1376 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))) | 
| 197 | 193, 196 | mpbid 232 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)) | 
| 198 | 117 | nncnd 12282 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 199 | 117 | nnne0d 12316 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ 0) | 
| 200 | 198, 199 | dividd 12041 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 / 𝑁) = 1) | 
| 201 | 197, 200 | breqtrd 5169 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) < 1) | 
| 202 | 14, 14, 72, 72 | mulgt0d 11416 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝐸 · 𝐸)) | 
| 203 |  | ltmul2 12118 | . . . . . . . . . . . 12
⊢ ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ
∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 <
(𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))) | 
| 204 | 158, 116,
156, 202, 203 | syl112anc 1376 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))) | 
| 205 | 201, 204 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)) | 
| 206 | 176, 176 | mulcld 11281 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℂ) | 
| 207 | 206 | mulridd 11278 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸)) | 
| 208 | 205, 207 | breqtrd 5169 | . . . . . . . . 9
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸)) | 
| 209 | 159, 156,
155, 208 | ltsub2dd 11876 | . . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) | 
| 210 | 114, 157,
160, 185, 209 | lttrd 11422 | . . . . . . 7
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) | 
| 211 | 176, 198,
199 | divcld 12043 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℂ) | 
| 212 | 175, 211,
180 | subdird 11720 | . . . . . . . . . 10
⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1)))) | 
| 213 | 180 | mullidd 11279 | . . . . . . . . . . 11
⊢ (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1)) | 
| 214 | 213 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) | 
| 215 | 212, 214 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) | 
| 216 | 215 | oveq2d 7447 | . . . . . . . 8
⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))) | 
| 217 | 211, 180 | mulcld 11281 | . . . . . . . . 9
⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈
ℂ) | 
| 218 | 176, 180,
217 | subdid 11719 | . . . . . . . 8
⊢ (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))))) | 
| 219 | 176, 198,
180, 199 | div32d 12066 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁))) | 
| 220 | 219 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁)))) | 
| 221 | 180, 198,
199 | divcld 12043 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ) | 
| 222 | 176, 176,
221 | mulassd 11284 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁)))) | 
| 223 | 220, 222 | eqtr4d 2780 | . . . . . . . . 9
⊢ (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) | 
| 224 | 223 | oveq2d 7447 | . . . . . . . 8
⊢ (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) | 
| 225 | 216, 218,
224 | 3eqtrd 2781 | . . . . . . 7
⊢ (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))) | 
| 226 | 210, 225 | breqtrrd 5171 | . . . . . 6
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))) | 
| 227 | 226 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))) | 
| 228 | 175, 211 | subcld 11620 | . . . . . . . . . 10
⊢ (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ) | 
| 229 |  | fsumconst 15826 | . . . . . . . . . 10
⊢
(((0...(𝐿 −
2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁)))) | 
| 230 | 124, 228,
229 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁)))) | 
| 231 | 230 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁)))) | 
| 232 |  | 0zd 12625 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈
ℤ) | 
| 233 | 31 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁)) | 
| 234 | 233 | elfzelzd 13565 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ) | 
| 235 | 126 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈
ℤ) | 
| 236 | 234, 235 | zsubcld 12727 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ) | 
| 237 |  | elnnuz 12922 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) | 
| 238 | 117, 237 | sylib 218 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘1)) | 
| 239 |  | elfzp12 13643 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈
(ℤ≥‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))) | 
| 240 | 238, 239 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))) | 
| 241 | 31, 240 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))) | 
| 242 | 241 | orcanai 1005 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁)) | 
| 243 |  | 1p1e2 12391 | . . . . . . . . . . . . . . . . . 18
⊢ (1 + 1) =
2 | 
| 244 | 243 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2) | 
| 245 | 244 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁)) | 
| 246 | 242, 245 | eleqtrd 2843 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁)) | 
| 247 |  | elfzle1 13567 | . . . . . . . . . . . . . . 15
⊢ (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿) | 
| 248 | 246, 247 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿) | 
| 249 | 108 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ) | 
| 250 | 131 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈
ℝ) | 
| 251 | 249, 250 | subge0d 11853 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿)) | 
| 252 | 248, 251 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2)) | 
| 253 | 232, 236,
252 | 3jca 1129 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧
0 ≤ (𝐿 −
2))) | 
| 254 |  | eluz2 12884 | . . . . . . . . . . . 12
⊢ ((𝐿 − 2) ∈
(ℤ≥‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧
0 ≤ (𝐿 −
2))) | 
| 255 | 253, 254 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈
(ℤ≥‘0)) | 
| 256 |  | hashfz 14466 | . . . . . . . . . . 11
⊢ ((𝐿 − 2) ∈
(ℤ≥‘0) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) +
1)) | 
| 257 | 255, 256 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) +
1)) | 
| 258 |  | 2cn 12341 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ | 
| 259 | 258 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℂ) | 
| 260 | 139, 259 | subcld 11620 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐿 − 2) ∈ ℂ) | 
| 261 | 260 | subid1d 11609 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2)) | 
| 262 | 261 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) +
1)) | 
| 263 | 139, 259,
175 | subadd23d 11642 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2))) | 
| 264 | 258, 167 | negsubdi2i 11595 | . . . . . . . . . . . . . . . 16
⊢ -(2
− 1) = (1 − 2) | 
| 265 |  | 2m1e1 12392 | . . . . . . . . . . . . . . . . 17
⊢ (2
− 1) = 1 | 
| 266 | 265 | negeqi 11501 | . . . . . . . . . . . . . . . 16
⊢ -(2
− 1) = -1 | 
| 267 | 264, 266 | eqtr3i 2767 | . . . . . . . . . . . . . . 15
⊢ (1
− 2) = -1 | 
| 268 | 267 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1 − 2) =
-1) | 
| 269 | 268 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1)) | 
| 270 | 139, 175 | negsubd 11626 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐿 + -1) = (𝐿 − 1)) | 
| 271 | 269, 270 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1)) | 
| 272 | 262, 263,
271 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1)) | 
| 273 | 272 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1)) | 
| 274 | 257, 273 | eqtrd 2777 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (𝐿 − 1)) | 
| 275 | 274 | oveq1d 7446 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((♯‘(0...(𝐿 − 2))) · (1
− (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁)))) | 
| 276 | 180, 228 | mulcomd 11282 | . . . . . . . . 9
⊢ (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) | 
| 277 | 276 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) | 
| 278 | 231, 275,
277 | 3eqtrd 2781 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) | 
| 279 |  | fzfid 14014 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin) | 
| 280 |  | fzn0 13578 | . . . . . . . . 9
⊢
((0...(𝐿 − 2))
≠ ∅ ↔ (𝐿
− 2) ∈ (ℤ≥‘0)) | 
| 281 | 255, 280 | sylibr 234 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅) | 
| 282 | 119 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ) | 
| 283 |  | simpll 767 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑) | 
| 284 | 150 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁)) | 
| 285 | 283, 284,
51 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) | 
| 286 | 49 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ 𝑇) | 
| 287 |  | elfzelz 13564 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ) | 
| 288 | 287 | zred 12722 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ) | 
| 289 | 288 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ) | 
| 290 | 163 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈
ℝ) | 
| 291 | 289, 290 | readdcld 11290 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ) | 
| 292 | 14 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ) | 
| 293 | 291, 292 | remulcld 11291 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ) | 
| 294 | 108 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ) | 
| 295 | 131 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈
ℝ) | 
| 296 | 294, 295 | resubcld 11691 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ) | 
| 297 | 296, 290 | readdcld 11290 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈
ℝ) | 
| 298 | 297, 292 | remulcld 11291 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈
ℝ) | 
| 299 |  | stoweidlem26.10 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) | 
| 300 | 299, 49 | jca 511 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇)) | 
| 301 | 300 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇)) | 
| 302 |  | ffvelcdm 7101 | . . . . . . . . . . . . . 14
⊢ ((𝐹:𝑇⟶ℝ ∧ 𝑆 ∈ 𝑇) → (𝐹‘𝑆) ∈ ℝ) | 
| 303 | 301, 302 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐹‘𝑆) ∈ ℝ) | 
| 304 |  | elfzle2 13568 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2)) | 
| 305 | 304 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2)) | 
| 306 | 289, 296,
290, 305 | leadd1dd 11877 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3))) | 
| 307 | 14, 72 | jca 511 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) | 
| 308 | 307 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) | 
| 309 |  | lemul1 12119 | . . . . . . . . . . . . . . 15
⊢ (((𝑖 + (1 / 3)) ∈ ℝ ∧
((𝐿 − 2) + (1 / 3))
∈ ℝ ∧ (𝐸
∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))) | 
| 310 | 291, 297,
308, 309 | syl3anc 1373 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))) | 
| 311 | 306, 310 | mpbid 232 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)) | 
| 312 | 108, 132 | resubcld 11691 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐿 − 2) ∈ ℝ) | 
| 313 | 312, 164 | readdcld 11290 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈
ℝ) | 
| 314 | 313, 14 | remulcld 11291 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈
ℝ) | 
| 315 | 299, 49 | ffvelcdmd 7105 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹‘𝑆) ∈ ℝ) | 
| 316 | 120, 164 | resubcld 11691 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈
ℝ) | 
| 317 | 316, 14 | remulcld 11291 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈
ℝ) | 
| 318 |  | addrid 11441 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (1 ∈
ℂ → (1 + 0) = 1) | 
| 319 | 318 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 ∈
ℂ → 1 = (1 + 0)) | 
| 320 | 167, 319 | mp1i 13 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 = (1 +
0)) | 
| 321 | 175 | subidd 11608 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (1 − 1) =
0) | 
| 322 | 321 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 0 = (1 −
1)) | 
| 323 | 322 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 + 0) = (1 + (1 −
1))) | 
| 324 |  | addsubass 11518 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1)
− 1) = (1 + (1 − 1))) | 
| 325 | 324 | eqcomd 2743 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1
− 1)) = ((1 + 1) − 1)) | 
| 326 | 175, 175,
175, 325 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 + (1 − 1)) = ((1
+ 1) − 1)) | 
| 327 | 320, 323,
326 | 3eqtrd 2781 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 = ((1 + 1) −
1)) | 
| 328 | 327 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) −
1))) | 
| 329 | 243 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 + 1) =
2) | 
| 330 | 329 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((1 + 1) − 1) = (2
− 1)) | 
| 331 | 330 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 −
1))) | 
| 332 | 139, 259,
175 | subsubd 11648 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) +
1)) | 
| 333 | 328, 331,
332 | 3eqtrd 2781 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1)) | 
| 334 | 333 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 /
3))) | 
| 335 | 258, 60, 9 | divcli 12009 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (2 / 3)
∈ ℂ | 
| 336 | 335 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2 / 3) ∈
ℂ) | 
| 337 | 260, 175,
336 | addsubassd 11640 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 /
3)))) | 
| 338 | 167, 60, 9 | divcli 12009 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 / 3)
∈ ℂ | 
| 339 |  | df-3 12330 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 = (2 +
1) | 
| 340 | 339 | oveq1i 7441 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (3 / 3) =
((2 + 1) / 3) | 
| 341 | 258, 167,
60, 9 | divdiri 12024 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2 + 1)
/ 3) = ((2 / 3) + (1 / 3)) | 
| 342 | 340, 61, 341 | 3eqtr3ri 2774 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2 / 3)
+ (1 / 3)) = 1 | 
| 343 | 167, 335,
338, 342 | subaddrii 11598 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (1
− (2 / 3)) = (1 / 3) | 
| 344 | 343 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (1 − (2 / 3)) = (1 /
3)) | 
| 345 | 344 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 /
3))) | 
| 346 | 334, 337,
345 | 3eqtrd 2781 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 /
3))) | 
| 347 | 131, 7, 9 | redivcli 12034 | . . . . . . . . . . . . . . . . . . . 20
⊢ (2 / 3)
∈ ℝ | 
| 348 | 347 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2 / 3) ∈
ℝ) | 
| 349 |  | 1lt2 12437 | . . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
2 | 
| 350 | 7, 63 | pm3.2i 470 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (3 ∈
ℝ ∧ 0 < 3) | 
| 351 | 1, 131, 350 | 3pm3.2i 1340 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 <
3)) | 
| 352 |  | ltdiv1 12132 | . . . . . . . . . . . . . . . . . . . . 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 233 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1 / 3) < (2 /
3)) | 
| 355 | 164, 348,
120, 354 | ltsub2dd 11876 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 /
3))) | 
| 356 | 346, 355 | eqbrtrrd 5167 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 /
3))) | 
| 357 | 313, 316,
13, 356 | ltmul1dd 13132 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸)) | 
| 358 | 23 | simprd 495 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))) | 
| 359 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 /
3))) | 
| 360 | 359 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸)) | 
| 361 | 360 | breq2d 5155 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = (𝐿 − 1) → ((𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) | 
| 362 | 361 | rabbidv 3444 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 = (𝐿 − 1) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)}) | 
| 363 | 129 | peano2zd 12725 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) | 
| 364 | 189 | simpld 494 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 1 ≤ 𝐿) | 
| 365 | 134, 116 | readdcld 11290 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) | 
| 366 | 134 | lep1d 12199 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1)) | 
| 367 | 108, 134,
365, 190, 366 | letrd 11418 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐿 ≤ (𝑁 + 1)) | 
| 368 | 186, 363,
125, 364, 367 | elfzd 13555 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐿 ∈ (1...(𝑁 + 1))) | 
| 369 | 139, 175 | npcand 11624 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝐿 − 1) + 1) = 𝐿) | 
| 370 |  | 0p1e1 12388 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (0 + 1) =
1 | 
| 371 | 370 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (0 + 1) =
1) | 
| 372 | 371 | oveq1d 7446 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))) | 
| 373 | 368, 369,
372 | 3eltr4d 2856 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))) | 
| 374 |  | 0zd 12625 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 0 ∈
ℤ) | 
| 375 | 125, 186 | zsubcld 12727 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐿 − 1) ∈ ℤ) | 
| 376 |  | fzaddel 13598 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((0
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ ((𝐿
− 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))) | 
| 377 | 374, 129,
375, 186, 376 | syl22anc 839 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))) | 
| 378 | 373, 377 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐿 − 1) ∈ (0...𝑁)) | 
| 379 |  | rabexg 5337 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V) | 
| 380 | 33, 379 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V) | 
| 381 | 25, 362, 378, 380 | fvmptd3 7039 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)}) | 
| 382 | 358, 381 | neleqtrd 2863 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ¬ 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)}) | 
| 383 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸) | 
| 384 | 41, 42, 383 | nfbr 5190 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑡(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) | 
| 385 | 45 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 𝑆 → ((𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) | 
| 386 | 38, 39, 384, 385 | elrabf 3688 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) | 
| 387 | 382, 386 | sylnib 328 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ¬ (𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) | 
| 388 |  | ianor 984 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝑆 ∈ 𝑇 ∧ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) | 
| 389 | 387, 388 | sylib 218 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) | 
| 390 |  | olc 869 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ 𝑇 → (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇)) | 
| 391 | 390 | anim1i 615 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ 𝑇 ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))) | 
| 392 | 49, 389, 391 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))) | 
| 393 |  | orcom 871 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇)) | 
| 394 | 393 | anbi2i 623 | . . . . . . . . . . . . . . . . . . 19
⊢ (((¬
(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ 𝑆 ∈ 𝑇 ∨ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))) | 
| 395 | 392, 394 | sylib 218 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))) | 
| 396 |  | pm4.43 1025 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆 ∈ 𝑇))) | 
| 397 | 395, 396 | sylibr 234 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) | 
| 398 | 317, 315 | ltnled 11408 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆) ↔ ¬ (𝐹‘𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) | 
| 399 | 397, 398 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹‘𝑆)) | 
| 400 | 314, 317,
315, 357, 399 | lttrd 11422 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹‘𝑆)) | 
| 401 | 314, 315,
400 | ltled 11409 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)) | 
| 402 | 401 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)) | 
| 403 | 293, 298,
303, 311, 402 | letrd 11418 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆)) | 
| 404 |  | nfcv 2905 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) | 
| 405 | 404, 42, 41 | nfbr 5190 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆) | 
| 406 | 45 | breq2d 5155 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))) | 
| 407 | 38, 39, 405, 406 | elrabf 3688 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑆 ∈ 𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑆))) | 
| 408 | 286, 403,
407 | sylanbrc 583 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) | 
| 409 |  | stoweidlem26.5 | . . . . . . . . . . . 12
⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) | 
| 410 |  | oveq1 7438 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3))) | 
| 411 | 410 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸)) | 
| 412 | 411 | breq1d 5153 | . . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡))) | 
| 413 | 412 | rabbidv 3444 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝑖 → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) | 
| 414 |  | rabexg 5337 | . . . . . . . . . . . . . 14
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) | 
| 415 | 33, 414 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) | 
| 416 | 415 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) | 
| 417 | 409, 413,
150, 416 | fvmptd3 7039 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐵‘𝑖) = {𝑡 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) | 
| 418 | 408, 417 | eleqtrrd 2844 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵‘𝑖)) | 
| 419 | 145 | 3ad2ant1 1134 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁)) | 
| 420 | 419, 146 | sylibr 234 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑁 ∈ (ℤ≥‘(𝐿 − 2))) | 
| 421 | 420, 148 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁)) | 
| 422 |  | simp2 1138 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...(𝐿 − 2))) | 
| 423 | 421, 422 | sseldd 3984 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑖 ∈ (0...𝑁)) | 
| 424 |  | elex 3501 | . . . . . . . . . . . . 13
⊢ (𝑆 ∈ (𝐵‘𝑖) → 𝑆 ∈ V) | 
| 425 | 424 | 3ad2ant3 1136 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → 𝑆 ∈ V) | 
| 426 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡(0...𝑁) | 
| 427 |  | nfrab1 3457 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} | 
| 428 | 426, 427 | nfmpt 5249 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) | 
| 429 | 409, 428 | nfcxfr 2903 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝐵 | 
| 430 |  | nfcv 2905 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡𝑖 | 
| 431 | 429, 430 | nffv 6916 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡(𝐵‘𝑖) | 
| 432 | 431 | nfel2 2924 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡 𝑆 ∈ (𝐵‘𝑖) | 
| 433 | 88, 89, 432 | nf3an 1901 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) | 
| 434 |  | nfv 1914 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(1 −
(𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆) | 
| 435 | 433, 434 | nfim 1896 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) | 
| 436 |  | eleq1 2829 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑆 → (𝑡 ∈ (𝐵‘𝑖) ↔ 𝑆 ∈ (𝐵‘𝑖))) | 
| 437 | 436 | 3anbi3d 1444 | . . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑆 → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) ↔ (𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)))) | 
| 438 | 93 | breq2d 5155 | . . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))) | 
| 439 | 437, 438 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑡 = 𝑆 → (((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) ↔ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)))) | 
| 440 |  | stoweidlem26.15 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑡)) | 
| 441 | 435, 439,
440 | vtoclg1f 3570 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ V → ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆))) | 
| 442 | 425, 441 | mpcom 38 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) | 
| 443 | 423, 442 | syld3an2 1413 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵‘𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) | 
| 444 | 418, 443 | mpd3an3 1464 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) | 
| 445 | 444 | adantlr 715 | . . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋‘𝑖)‘𝑆)) | 
| 446 | 279, 281,
282, 285, 445 | fsumlt 15836 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) | 
| 447 | 278, 446 | eqbrtrrd 5167 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) | 
| 448 | 121 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈
ℝ) | 
| 449 | 152 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ) | 
| 450 | 307 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) | 
| 451 |  | ltmul2 12118 | . . . . . . 7
⊢ ((((1
− (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧
Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))) | 
| 452 | 448, 449,
450, 451 | syl3anc 1373 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)))) | 
| 453 | 447, 452 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))) | 
| 454 | 115, 123,
154, 227, 453 | lttrd 11422 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆))) | 
| 455 | 150, 52 | syldan 591 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 456 | 455 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 457 | 456 | recnd 11289 | . . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) | 
| 458 | 279, 457 | fsumcl 15769 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) | 
| 459 | 458 | addridd 11461 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 460 |  | 0red 11264 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈
ℝ) | 
| 461 |  | fzfid 14014 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin) | 
| 462 | 14 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ) | 
| 463 |  | 0zd 12625 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ) | 
| 464 | 129 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ) | 
| 465 |  | elfzelz 13564 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ) | 
| 466 | 465 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ) | 
| 467 |  | 0red 11264 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ) | 
| 468 | 120 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ) | 
| 469 | 465 | zred 12722 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ) | 
| 470 | 469 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ) | 
| 471 |  | 1m1e0 12338 | . . . . . . . . . . . . . . 15
⊢ (1
− 1) = 0 | 
| 472 | 116, 108,
116, 364 | lesub1dd 11879 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 − 1) ≤ (𝐿 − 1)) | 
| 473 | 471, 472 | eqbrtrrid 5179 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ (𝐿 − 1)) | 
| 474 | 473 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1)) | 
| 475 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁)) | 
| 476 | 375 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ) | 
| 477 |  | elfz 13553 | . . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧
𝑁 ∈ ℤ) →
(𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) | 
| 478 | 466, 476,
464, 477 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁))) | 
| 479 | 475, 478 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁)) | 
| 480 | 479 | simpld 494 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖) | 
| 481 | 467, 468,
470, 474, 480 | letrd 11418 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖) | 
| 482 |  | elfzle2 13568 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ≤ 𝑁) | 
| 483 | 482 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ≤ 𝑁) | 
| 484 | 463, 464,
466, 481, 483 | elfzd 13555 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁)) | 
| 485 | 484, 51 | syldan 591 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℝ) | 
| 486 | 462, 485 | remulcld 11291 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 487 | 486 | adantlr 715 | . . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 488 | 461, 487 | fsumrecl 15770 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 489 | 279, 456 | fsumrecl 15770 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) | 
| 490 |  | fzfid 14014 | . . . . . . . . 9
⊢ (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin) | 
| 491 | 176 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ) | 
| 492 | 491 | mul01d 11460 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0) | 
| 493 | 484, 100 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋‘𝑖)‘𝑆)) | 
| 494 | 307 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) | 
| 495 |  | lemul2 12120 | . . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ ((𝑋‘𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))) | 
| 496 | 467, 485,
494, 495 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋‘𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆)))) | 
| 497 | 493, 496 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 498 | 492, 497 | eqbrtrrd 5167 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 499 | 490, 486,
498 | fsumge0 15831 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 500 | 499 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 501 | 460, 488,
489, 500 | leadd2dd 11878 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) | 
| 502 | 459, 501 | eqbrtrrd 5167 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) | 
| 503 | 151 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ) | 
| 504 | 124, 176,
503 | fsummulc2 15820 | . . . . . 6
⊢ (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 505 | 504 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 506 |  | stoweidlem26.2 | . . . . . . . . 9
⊢
Ⅎ𝑗𝜑 | 
| 507 |  | elfzelz 13564 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ) | 
| 508 | 507 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ) | 
| 509 | 508 | zred 12722 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ) | 
| 510 | 312 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ) | 
| 511 | 120 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ) | 
| 512 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2))) | 
| 513 |  | 0zd 12625 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈
ℤ) | 
| 514 | 128 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ) | 
| 515 |  | elfz 13553 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℤ ∧ 0 ∈
ℤ ∧ (𝐿 − 2)
∈ ℤ) → (𝑗
∈ (0...(𝐿 − 2))
↔ (0 ≤ 𝑗 ∧
𝑗 ≤ (𝐿 − 2)))) | 
| 516 | 508, 513,
514, 515 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2)))) | 
| 517 | 512, 516 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗 ∧ 𝑗 ≤ (𝐿 − 2))) | 
| 518 | 517 | simprd 495 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2)) | 
| 519 | 116, 132,
108 | ltsub2d 11873 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1))) | 
| 520 | 349, 519 | mpbii 233 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐿 − 2) < (𝐿 − 1)) | 
| 521 | 520 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1)) | 
| 522 | 509, 510,
511, 518, 521 | lelttrd 11419 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1)) | 
| 523 | 509, 511 | ltnled 11408 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗)) | 
| 524 | 522, 523 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗) | 
| 525 | 524 | intnanrd 489 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁)) | 
| 526 | 375 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ) | 
| 527 | 129 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ) | 
| 528 |  | elfz 13553 | . . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧
𝑁 ∈ ℤ) →
(𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) | 
| 529 | 508, 526,
527, 528 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁))) | 
| 530 | 525, 529 | mtbird 325 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)) | 
| 531 | 530 | ex 412 | . . . . . . . . 9
⊢ (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))) | 
| 532 | 506, 531 | ralrimi 3257 | . . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)) | 
| 533 |  | disj 4450 | . . . . . . . 8
⊢
(((0...(𝐿 −
2)) ∩ ((𝐿 −
1)...𝑁)) = ∅ ↔
∀𝑗 ∈
(0...(𝐿 − 2)) ¬
𝑗 ∈ ((𝐿 − 1)...𝑁)) | 
| 534 | 532, 533 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅) | 
| 535 | 534 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅) | 
| 536 | 144 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁) | 
| 537 | 128, 374,
129 | 3jca 1129 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ)) | 
| 538 | 537 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑁 ∈
ℤ)) | 
| 539 |  | elfz 13553 | . . . . . . . . . 10
⊢ (((𝐿 − 2) ∈ ℤ ∧
0 ∈ ℤ ∧ 𝑁
∈ ℤ) → ((𝐿
− 2) ∈ (0...𝑁)
↔ (0 ≤ (𝐿 −
2) ∧ (𝐿 − 2) ≤
𝑁))) | 
| 540 | 538, 539 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁))) | 
| 541 | 252, 536,
540 | mpbir2and 713 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁)) | 
| 542 |  | fzsplit 13590 | . . . . . . . 8
⊢ ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁))) | 
| 543 | 541, 542 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁))) | 
| 544 | 263, 269,
270 | 3eqtrd 2781 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1)) | 
| 545 | 544 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁)) | 
| 546 | 545 | uneq2d 4168 | . . . . . . . 8
⊢ (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁))) | 
| 547 | 546 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁))) | 
| 548 | 543, 547 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁))) | 
| 549 |  | fzfid 14014 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin) | 
| 550 | 176 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ) | 
| 551 | 51 | recnd 11289 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑆) ∈ ℂ) | 
| 552 | 550, 551 | mulcld 11281 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) | 
| 553 | 552 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℂ) | 
| 554 | 535, 548,
549, 553 | fsumsplit 15777 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋‘𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) | 
| 555 | 502, 505,
554 | 3brtr4d 5175 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 556 | 114, 153,
53 | 3jca 1129 | . . . . . 6
⊢ (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)) | 
| 557 | 556 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ)) | 
| 558 |  | ltletr 11353 | . . . . 5
⊢ ((((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ ℝ) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) | 
| 559 | 557, 558 | syl 17 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋‘𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)))) | 
| 560 | 454, 555,
559 | mp2and 699 | . . 3
⊢ ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 561 | 105, 560 | pm2.61dan 813 | . 2
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 562 |  | sumex 15724 | . . 3
⊢
Σ𝑖 ∈
(0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V | 
| 563 | 93 | oveq2d 7447 | . . . . 5
⊢ (𝑡 = 𝑆 → (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 564 | 563 | sumeq2sdv 15739 | . . . 4
⊢ (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 565 |  | eqid 2737 | . . . 4
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) | 
| 566 | 564, 565 | fvmptg 7014 | . . 3
⊢ ((𝑆 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆)) ∈ V) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 567 | 49, 562, 566 | sylancl 586 | . 2
⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑆))) | 
| 568 | 561, 567 | breqtrrd 5171 | 1
⊢ (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑆)) |