Proof of Theorem stoweidlem44
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | stoweidlem44.2 | . . . 4
⊢
Ⅎ𝑡𝜑 | 
| 2 |  | stoweidlem44.5 | . . . 4
⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) | 
| 3 |  | eqid 2736 | . . . 4
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) | 
| 4 |  | eqid 2736 | . . . 4
⊢ (𝑡 ∈ 𝑇 ↦ (1 / 𝑀)) = (𝑡 ∈ 𝑇 ↦ (1 / 𝑀)) | 
| 5 |  | stoweidlem44.6 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 6 | 5 | nnrecred 12318 | . . . 4
⊢ (𝜑 → (1 / 𝑀) ∈ ℝ) | 
| 7 |  | stoweidlem44.7 | . . . . 5
⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄) | 
| 8 |  | stoweidlem44.4 | . . . . . 6
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} | 
| 9 |  | ssrab2 4079 | . . . . . 6
⊢ {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} ⊆ 𝐴 | 
| 10 | 8, 9 | eqsstri 4029 | . . . . 5
⊢ 𝑄 ⊆ 𝐴 | 
| 11 |  | fss 6751 | . . . . 5
⊢ ((𝐺:(1...𝑀)⟶𝑄 ∧ 𝑄 ⊆ 𝐴) → 𝐺:(1...𝑀)⟶𝐴) | 
| 12 | 7, 10, 11 | sylancl 586 | . . . 4
⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝐴) | 
| 13 |  | stoweidlem44.11 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) | 
| 14 |  | stoweidlem44.12 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) | 
| 15 |  | stoweidlem44.13 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) | 
| 16 |  | stoweidlem44.3 | . . . . 5
⊢ 𝐾 = (topGen‘ran
(,)) | 
| 17 |  | stoweidlem44.9 | . . . . 5
⊢ 𝑇 = ∪
𝐽 | 
| 18 |  | eqid 2736 | . . . . 5
⊢ (𝐽 Cn 𝐾) = (𝐽 Cn 𝐾) | 
| 19 |  | stoweidlem44.10 | . . . . . 6
⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾)) | 
| 20 | 19 | sselda 3982 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓 ∈ (𝐽 Cn 𝐾)) | 
| 21 | 16, 17, 18, 20 | fcnre 45035 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) | 
| 22 | 1, 2, 3, 4, 5, 6, 12, 13, 14, 15, 21 | stoweidlem32 46052 | . . 3
⊢ (𝜑 → 𝑃 ∈ 𝐴) | 
| 23 | 8, 2, 5, 7, 21 | stoweidlem38 46058 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) | 
| 24 | 23 | ex 412 | . . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝑇 → (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))) | 
| 25 | 1, 24 | ralrimi 3256 | . . . 4
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) | 
| 26 |  | stoweidlem44.14 | . . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑇) | 
| 27 | 8, 2, 5, 7, 21, 26 | stoweidlem37 46057 | . . . 4
⊢ (𝜑 → (𝑃‘𝑍) = 0) | 
| 28 |  | stoweidlem44.1 | . . . . . . . . 9
⊢
Ⅎ𝑗𝜑 | 
| 29 |  | nfv 1913 | . . . . . . . . 9
⊢
Ⅎ𝑗 𝑡 ∈ (𝑇 ∖ 𝑈) | 
| 30 | 28, 29 | nfan 1898 | . . . . . . . 8
⊢
Ⅎ𝑗(𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) | 
| 31 |  | nfv 1913 | . . . . . . . 8
⊢
Ⅎ𝑗0 < ((1 /
𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) | 
| 32 |  | stoweidlem44.8 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑗 ∈ (1...𝑀)0 < ((𝐺‘𝑗)‘𝑡)) | 
| 33 | 32 | r19.21bi 3250 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑗 ∈ (1...𝑀)0 < ((𝐺‘𝑗)‘𝑡)) | 
| 34 |  | df-rex 3070 | . . . . . . . . 9
⊢
(∃𝑗 ∈
(1...𝑀)0 < ((𝐺‘𝑗)‘𝑡) ↔ ∃𝑗(𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) | 
| 35 | 33, 34 | sylib 218 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑗(𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) | 
| 36 | 6 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (1 / 𝑀) ∈ ℝ) | 
| 37 |  | simpll 766 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 𝜑) | 
| 38 |  | eldifi 4130 | . . . . . . . . . . 11
⊢ (𝑡 ∈ (𝑇 ∖ 𝑈) → 𝑡 ∈ 𝑇) | 
| 39 | 38 | ad2antlr 727 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 𝑡 ∈ 𝑇) | 
| 40 |  | fzfid 14015 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1...𝑀) ∈ Fin) | 
| 41 | 8, 7, 21 | stoweidlem15 46035 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝑇) → (((𝐺‘𝑖)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺‘𝑖)‘𝑡) ∧ ((𝐺‘𝑖)‘𝑡) ≤ 1)) | 
| 42 | 41 | an32s 652 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺‘𝑖)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺‘𝑖)‘𝑡) ∧ ((𝐺‘𝑖)‘𝑡) ≤ 1)) | 
| 43 | 42 | simp1d 1142 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 44 | 40, 43 | fsumrecl 15771 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 45 | 37, 39, 44 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 46 | 5 | nnred 12282 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 47 | 5 | nngt0d 12316 | . . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝑀) | 
| 48 | 46, 47 | recgt0d 12203 | . . . . . . . . . 10
⊢ (𝜑 → 0 < (1 / 𝑀)) | 
| 49 | 48 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < (1 / 𝑀)) | 
| 50 |  | 0red 11265 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 ∈ ℝ) | 
| 51 |  | simprl 770 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 𝑗 ∈ (1...𝑀)) | 
| 52 | 37, 51, 39 | 3jca 1128 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇)) | 
| 53 |  | snfi 9084 | . . . . . . . . . . . . . . 15
⊢ {𝑗} ∈ Fin | 
| 54 | 53 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → {𝑗} ∈ Fin) | 
| 55 |  | simpl1 1191 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝜑) | 
| 56 |  | simpl3 1193 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑡 ∈ 𝑇) | 
| 57 |  | elsni 4642 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ {𝑗} → 𝑖 = 𝑗) | 
| 58 | 57 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑖 = 𝑗) | 
| 59 |  | simpl2 1192 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑗 ∈ (1...𝑀)) | 
| 60 | 58, 59 | eqeltrd 2840 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑖 ∈ (1...𝑀)) | 
| 61 | 55, 56, 60, 43 | syl21anc 837 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 62 | 54, 61 | fsumrecl 15771 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 63 | 52, 62 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 64 | 50, 63 | readdcld 11291 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (0 + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡)) ∈ ℝ) | 
| 65 |  | fzfi 14014 | . . . . . . . . . . . . . . 15
⊢
(1...𝑀) ∈
Fin | 
| 66 |  | diffi 9216 | . . . . . . . . . . . . . . 15
⊢
((1...𝑀) ∈ Fin
→ ((1...𝑀) ∖
{𝑗}) ∈
Fin) | 
| 67 | 65, 66 | mp1i 13 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((1...𝑀) ∖ {𝑗}) ∈ Fin) | 
| 68 |  | eldifi 4130 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ((1...𝑀) ∖ {𝑗}) → 𝑖 ∈ (1...𝑀)) | 
| 69 | 68, 43 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 70 | 67, 69 | fsumrecl 15771 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 71 | 37, 39, 70 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 72 | 71, 63 | readdcld 11291 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡)) ∈ ℝ) | 
| 73 |  | 00id 11437 | . . . . . . . . . . . 12
⊢ (0 + 0) =
0 | 
| 74 |  | simprr 772 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < ((𝐺‘𝑗)‘𝑡)) | 
| 75 | 8, 7, 21 | stoweidlem15 46035 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝑇) → (((𝐺‘𝑗)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺‘𝑗)‘𝑡) ∧ ((𝐺‘𝑗)‘𝑡) ≤ 1)) | 
| 76 | 75 | simp1d 1142 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝑇) → ((𝐺‘𝑗)‘𝑡) ∈ ℝ) | 
| 77 | 37, 51, 39, 76 | syl21anc 837 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → ((𝐺‘𝑗)‘𝑡) ∈ ℝ) | 
| 78 | 77 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → ((𝐺‘𝑗)‘𝑡) ∈ ℂ) | 
| 79 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑗 → (𝐺‘𝑖) = (𝐺‘𝑗)) | 
| 80 | 79 | fveq1d 6907 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑗 → ((𝐺‘𝑖)‘𝑡) = ((𝐺‘𝑗)‘𝑡)) | 
| 81 | 80 | sumsn 15783 | . . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (1...𝑀) ∧ ((𝐺‘𝑗)‘𝑡) ∈ ℂ) → Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡) = ((𝐺‘𝑗)‘𝑡)) | 
| 82 | 51, 78, 81 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡) = ((𝐺‘𝑗)‘𝑡)) | 
| 83 | 74, 82 | breqtrrd 5170 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡)) | 
| 84 | 50, 63, 50, 83 | ltadd2dd 11421 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (0 + 0) < (0 + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) | 
| 85 | 73, 84 | eqbrtrrid 5178 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < (0 + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) | 
| 86 |  | 0red 11265 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → 0 ∈ ℝ) | 
| 87 | 70 | 3adant2 1131 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 88 |  | simpll 766 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 𝜑) | 
| 89 | 68 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑖 ∈ (1...𝑀)) | 
| 90 |  | simplr 768 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑡 ∈ 𝑇) | 
| 91 | 88, 89, 90, 41 | syl21anc 837 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → (((𝐺‘𝑖)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺‘𝑖)‘𝑡) ∧ ((𝐺‘𝑖)‘𝑡) ≤ 1)) | 
| 92 | 91 | simp2d 1143 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 0 ≤ ((𝐺‘𝑖)‘𝑡)) | 
| 93 | 67, 69, 92 | fsumge0 15832 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ≤ Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡)) | 
| 94 | 93 | 3adant2 1131 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → 0 ≤ Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡)) | 
| 95 | 86, 87, 62, 94 | leadd1dd 11878 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (0 + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡)) ≤ (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) | 
| 96 | 52, 95 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (0 + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡)) ≤ (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) | 
| 97 | 50, 64, 72, 85, 96 | ltletrd 11422 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) | 
| 98 |  | eldifn 4131 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((1...𝑀) ∖ {𝑗}) → ¬ 𝑥 ∈ {𝑗}) | 
| 99 |  | imnan 399 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ((1...𝑀) ∖ {𝑗}) → ¬ 𝑥 ∈ {𝑗}) ↔ ¬ (𝑥 ∈ ((1...𝑀) ∖ {𝑗}) ∧ 𝑥 ∈ {𝑗})) | 
| 100 | 98, 99 | mpbi 230 | . . . . . . . . . . . . . . 15
⊢  ¬
(𝑥 ∈ ((1...𝑀) ∖ {𝑗}) ∧ 𝑥 ∈ {𝑗}) | 
| 101 |  | elin 3966 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (((1...𝑀) ∖ {𝑗}) ∩ {𝑗}) ↔ (𝑥 ∈ ((1...𝑀) ∖ {𝑗}) ∧ 𝑥 ∈ {𝑗})) | 
| 102 | 100, 101 | mtbir 323 | . . . . . . . . . . . . . 14
⊢  ¬
𝑥 ∈ (((1...𝑀) ∖ {𝑗}) ∩ {𝑗}) | 
| 103 | 102 | nel0 4353 | . . . . . . . . . . . . 13
⊢
(((1...𝑀) ∖
{𝑗}) ∩ {𝑗}) = ∅ | 
| 104 | 103 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (((1...𝑀) ∖ {𝑗}) ∩ {𝑗}) = ∅) | 
| 105 |  | undif1 4475 | . . . . . . . . . . . . 13
⊢
(((1...𝑀) ∖
{𝑗}) ∪ {𝑗}) = ((1...𝑀) ∪ {𝑗}) | 
| 106 |  | snssi 4807 | . . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...𝑀) → {𝑗} ⊆ (1...𝑀)) | 
| 107 | 106 | 3ad2ant2 1134 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → {𝑗} ⊆ (1...𝑀)) | 
| 108 |  | ssequn2 4188 | . . . . . . . . . . . . . 14
⊢ ({𝑗} ⊆ (1...𝑀) ↔ ((1...𝑀) ∪ {𝑗}) = (1...𝑀)) | 
| 109 | 107, 108 | sylib 218 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → ((1...𝑀) ∪ {𝑗}) = (1...𝑀)) | 
| 110 | 105, 109 | eqtr2id 2789 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (1...𝑀) = (((1...𝑀) ∖ {𝑗}) ∪ {𝑗})) | 
| 111 |  | fzfid 14015 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (1...𝑀) ∈ Fin) | 
| 112 | 43 | 3adantl2 1167 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) | 
| 113 | 112 | recnd 11290 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑡) ∈ ℂ) | 
| 114 | 104, 110,
111, 113 | fsumsplit 15778 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) = (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) | 
| 115 | 52, 114 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) = (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) | 
| 116 | 97, 115 | breqtrrd 5170 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) | 
| 117 | 36, 45, 49, 116 | mulgt0d 11417 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) | 
| 118 | 30, 31, 35, 117 | exlimdd 2219 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 0 < ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) | 
| 119 | 8, 2, 5, 7, 21 | stoweidlem30 46050 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑃‘𝑡) = ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) | 
| 120 | 38, 119 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (𝑃‘𝑡) = ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) | 
| 121 | 118, 120 | breqtrrd 5170 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 0 < (𝑃‘𝑡)) | 
| 122 | 121 | ex 412 | . . . . 5
⊢ (𝜑 → (𝑡 ∈ (𝑇 ∖ 𝑈) → 0 < (𝑃‘𝑡))) | 
| 123 | 1, 122 | ralrimi 3256 | . . . 4
⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡)) | 
| 124 | 25, 27, 123 | 3jca 1128 | . . 3
⊢ (𝜑 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1) ∧ (𝑃‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡))) | 
| 125 |  | eleq1 2828 | . . . . . 6
⊢ (𝑝 = 𝑃 → (𝑝 ∈ 𝐴 ↔ 𝑃 ∈ 𝐴)) | 
| 126 |  | nfmpt1 5249 | . . . . . . . . . 10
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) | 
| 127 | 2, 126 | nfcxfr 2902 | . . . . . . . . 9
⊢
Ⅎ𝑡𝑃 | 
| 128 | 127 | nfeq2 2922 | . . . . . . . 8
⊢
Ⅎ𝑡 𝑝 = 𝑃 | 
| 129 |  | fveq1 6904 | . . . . . . . . . 10
⊢ (𝑝 = 𝑃 → (𝑝‘𝑡) = (𝑃‘𝑡)) | 
| 130 | 129 | breq2d 5154 | . . . . . . . . 9
⊢ (𝑝 = 𝑃 → (0 ≤ (𝑝‘𝑡) ↔ 0 ≤ (𝑃‘𝑡))) | 
| 131 | 129 | breq1d 5152 | . . . . . . . . 9
⊢ (𝑝 = 𝑃 → ((𝑝‘𝑡) ≤ 1 ↔ (𝑃‘𝑡) ≤ 1)) | 
| 132 | 130, 131 | anbi12d 632 | . . . . . . . 8
⊢ (𝑝 = 𝑃 → ((0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ↔ (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))) | 
| 133 | 128, 132 | ralbid 3272 | . . . . . . 7
⊢ (𝑝 = 𝑃 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))) | 
| 134 |  | fveq1 6904 | . . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑝‘𝑍) = (𝑃‘𝑍)) | 
| 135 | 134 | eqeq1d 2738 | . . . . . . 7
⊢ (𝑝 = 𝑃 → ((𝑝‘𝑍) = 0 ↔ (𝑃‘𝑍) = 0)) | 
| 136 | 129 | breq2d 5154 | . . . . . . . 8
⊢ (𝑝 = 𝑃 → (0 < (𝑝‘𝑡) ↔ 0 < (𝑃‘𝑡))) | 
| 137 | 128, 136 | ralbid 3272 | . . . . . . 7
⊢ (𝑝 = 𝑃 → (∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡))) | 
| 138 | 133, 135,
137 | 3anbi123d 1437 | . . . . . 6
⊢ (𝑝 = 𝑃 → ((∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1) ∧ (𝑃‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡)))) | 
| 139 | 125, 138 | anbi12d 632 | . . . . 5
⊢ (𝑝 = 𝑃 → ((𝑝 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡))) ↔ (𝑃 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1) ∧ (𝑃‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡))))) | 
| 140 | 139 | spcegv 3596 | . . . 4
⊢ (𝑃 ∈ 𝐴 → ((𝑃 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1) ∧ (𝑃‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡))) → ∃𝑝(𝑝 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡))))) | 
| 141 | 22, 140 | syl 17 | . . 3
⊢ (𝜑 → ((𝑃 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1) ∧ (𝑃‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡))) → ∃𝑝(𝑝 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡))))) | 
| 142 | 22, 124, 141 | mp2and 699 | . 2
⊢ (𝜑 → ∃𝑝(𝑝 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)))) | 
| 143 |  | df-rex 3070 | . 2
⊢
(∃𝑝 ∈
𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)) ↔ ∃𝑝(𝑝 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)))) | 
| 144 | 142, 143 | sylibr 234 | 1
⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡))) |