Proof of Theorem stoweidlem38
| Step | Hyp | Ref
| Expression |
| 1 | | stoweidlem38.3 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 2 | 1 | nnrecred 12317 |
. . . . 5
⊢ (𝜑 → (1 / 𝑀) ∈ ℝ) |
| 3 | 2 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (1 / 𝑀) ∈ ℝ) |
| 4 | | fzfid 14014 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (1...𝑀) ∈ Fin) |
| 5 | | stoweidlem38.1 |
. . . . . . . 8
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
| 6 | | stoweidlem38.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄) |
| 7 | | stoweidlem38.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
| 8 | 5, 6, 7 | stoweidlem15 46030 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑆 ∈ 𝑇) → (((𝐺‘𝑖)‘𝑆) ∈ ℝ ∧ 0 ≤ ((𝐺‘𝑖)‘𝑆) ∧ ((𝐺‘𝑖)‘𝑆) ≤ 1)) |
| 9 | 8 | simp1d 1143 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑆 ∈ 𝑇) → ((𝐺‘𝑖)‘𝑆) ∈ ℝ) |
| 10 | 9 | an32s 652 |
. . . . 5
⊢ (((𝜑 ∧ 𝑆 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑆) ∈ ℝ) |
| 11 | 4, 10 | fsumrecl 15770 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆) ∈ ℝ) |
| 12 | | 1red 11262 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
| 13 | | 0le1 11786 |
. . . . . . 7
⊢ 0 ≤
1 |
| 14 | 13 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 1) |
| 15 | 1 | nnred 12281 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 16 | 1 | nngt0d 12315 |
. . . . . 6
⊢ (𝜑 → 0 < 𝑀) |
| 17 | | divge0 12137 |
. . . . . 6
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 ≤ (1 / 𝑀)) |
| 18 | 12, 14, 15, 16, 17 | syl22anc 839 |
. . . . 5
⊢ (𝜑 → 0 ≤ (1 / 𝑀)) |
| 19 | 18 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → 0 ≤ (1 / 𝑀)) |
| 20 | 8 | simp2d 1144 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑆 ∈ 𝑇) → 0 ≤ ((𝐺‘𝑖)‘𝑆)) |
| 21 | 20 | an32s 652 |
. . . . 5
⊢ (((𝜑 ∧ 𝑆 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 0 ≤ ((𝐺‘𝑖)‘𝑆)) |
| 22 | 4, 10, 21 | fsumge0 15831 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → 0 ≤ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆)) |
| 23 | 3, 11, 19, 22 | mulge0d 11840 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → 0 ≤ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆))) |
| 24 | | stoweidlem38.2 |
. . . 4
⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
| 25 | 5, 24, 1, 6, 7 | stoweidlem30 46045 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (𝑃‘𝑆) = ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆))) |
| 26 | 23, 25 | breqtrrd 5171 |
. 2
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → 0 ≤ (𝑃‘𝑆)) |
| 27 | | 1red 11262 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → 1 ∈ ℝ) |
| 28 | 8 | simp3d 1145 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑆 ∈ 𝑇) → ((𝐺‘𝑖)‘𝑆) ≤ 1) |
| 29 | 28 | an32s 652 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑆) ≤ 1) |
| 30 | 4, 10, 27, 29 | fsumle 15835 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆) ≤ Σ𝑖 ∈ (1...𝑀)1) |
| 31 | | fzfid 14014 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
| 32 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 33 | | fsumconst 15826 |
. . . . . . . . 9
⊢
(((1...𝑀) ∈ Fin
∧ 1 ∈ ℂ) → Σ𝑖 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1)) |
| 34 | 31, 32, 33 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)1 = ((♯‘(1...𝑀)) · 1)) |
| 35 | 1 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 36 | | hashfz1 14385 |
. . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) |
| 38 | 37 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘(1...𝑀)) · 1) = (𝑀 · 1)) |
| 39 | 1 | nncnd 12282 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℂ) |
| 40 | 39 | mulridd 11278 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 · 1) = 𝑀) |
| 41 | 34, 38, 40 | 3eqtrd 2781 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑀)1 = 𝑀) |
| 42 | 41 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)1 = 𝑀) |
| 43 | 30, 42 | breqtrd 5169 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆) ≤ 𝑀) |
| 44 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → 𝑀 ∈ ℝ) |
| 45 | | 1red 11262 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → 1 ∈ ℝ) |
| 46 | | 0lt1 11785 |
. . . . . . . 8
⊢ 0 <
1 |
| 47 | 46 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → 0 < 1) |
| 48 | 15, 16 | jca 511 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ∈ ℝ ∧ 0 < 𝑀)) |
| 49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (𝑀 ∈ ℝ ∧ 0 < 𝑀)) |
| 50 | | divgt0 12136 |
. . . . . . 7
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → 0 < (1 / 𝑀)) |
| 51 | 45, 47, 49, 50 | syl21anc 838 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → 0 < (1 / 𝑀)) |
| 52 | | lemul2 12120 |
. . . . . 6
⊢
((Σ𝑖 ∈
(1...𝑀)((𝐺‘𝑖)‘𝑆) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((1 / 𝑀) ∈ ℝ ∧ 0 < (1
/ 𝑀))) → (Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆) ≤ 𝑀 ↔ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆)) ≤ ((1 / 𝑀) · 𝑀))) |
| 53 | 11, 44, 3, 51, 52 | syl112anc 1376 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆) ≤ 𝑀 ↔ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆)) ≤ ((1 / 𝑀) · 𝑀))) |
| 54 | 43, 53 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑆)) ≤ ((1 / 𝑀) · 𝑀)) |
| 55 | 25, 54 | eqbrtrd 5165 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (𝑃‘𝑆) ≤ ((1 / 𝑀) · 𝑀)) |
| 56 | 32 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) |
| 57 | 1 | nnne0d 12316 |
. . . . . 6
⊢ (𝜑 → 𝑀 ≠ 0) |
| 58 | 56, 39, 57 | 3jca 1129 |
. . . . 5
⊢ (𝜑 → (1 ∈ ℂ ∧
𝑀 ∈ ℂ ∧
𝑀 ≠ 0)) |
| 59 | 58 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (1 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0)) |
| 60 | | divcan1 11931 |
. . . 4
⊢ ((1
∈ ℂ ∧ 𝑀
∈ ℂ ∧ 𝑀 ≠
0) → ((1 / 𝑀) ·
𝑀) = 1) |
| 61 | 59, 60 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → ((1 / 𝑀) · 𝑀) = 1) |
| 62 | 55, 61 | breqtrd 5169 |
. 2
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (𝑃‘𝑆) ≤ 1) |
| 63 | 26, 62 | jca 511 |
1
⊢ ((𝜑 ∧ 𝑆 ∈ 𝑇) → (0 ≤ (𝑃‘𝑆) ∧ (𝑃‘𝑆) ≤ 1)) |