Proof of Theorem stoweidlem44
Step | Hyp | Ref
| Expression |
1 | | stoweidlem44.2 |
. . . 4
⊢
Ⅎ𝑡𝜑 |
2 | | stoweidlem44.5 |
. . . 4
⊢ 𝑃 = (𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
3 | | eqid 2739 |
. . . 4
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
4 | | eqid 2739 |
. . . 4
⊢ (𝑡 ∈ 𝑇 ↦ (1 / 𝑀)) = (𝑡 ∈ 𝑇 ↦ (1 / 𝑀)) |
5 | | stoweidlem44.6 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
6 | 5 | nnrecred 11779 |
. . . 4
⊢ (𝜑 → (1 / 𝑀) ∈ ℝ) |
7 | | stoweidlem44.7 |
. . . . 5
⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝑄) |
8 | | stoweidlem44.4 |
. . . . . 6
⊢ 𝑄 = {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} |
9 | | ssrab2 3979 |
. . . . . 6
⊢ {ℎ ∈ 𝐴 ∣ ((ℎ‘𝑍) = 0 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (ℎ‘𝑡) ∧ (ℎ‘𝑡) ≤ 1))} ⊆ 𝐴 |
10 | 8, 9 | eqsstri 3921 |
. . . . 5
⊢ 𝑄 ⊆ 𝐴 |
11 | | fss 6531 |
. . . . 5
⊢ ((𝐺:(1...𝑀)⟶𝑄 ∧ 𝑄 ⊆ 𝐴) → 𝐺:(1...𝑀)⟶𝐴) |
12 | 7, 10, 11 | sylancl 589 |
. . . 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 2739 |
. . . . 5
⊢ (𝐽 Cn 𝐾) = (𝐽 Cn 𝐾) |
19 | | stoweidlem44.10 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
20 | 19 | sselda 3887 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓 ∈ (𝐽 Cn 𝐾)) |
21 | 16, 17, 18, 20 | fcnre 42146 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
22 | 1, 2, 3, 4, 5, 6, 12, 13, 14, 15, 21 | stoweidlem32 43155 |
. . 3
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
23 | 8, 2, 5, 7, 21 | stoweidlem38 43161 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) |
24 | 23 | ex 416 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝑇 → (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))) |
25 | 1, 24 | ralrimi 3129 |
. . . 4
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) |
26 | | stoweidlem44.14 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑇) |
27 | 8, 2, 5, 7, 21, 26 | stoweidlem37 43160 |
. . . 4
⊢ (𝜑 → (𝑃‘𝑍) = 0) |
28 | | stoweidlem44.1 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝜑 |
29 | | nfv 1921 |
. . . . . . . . 9
⊢
Ⅎ𝑗 𝑡 ∈ (𝑇 ∖ 𝑈) |
30 | 28, 29 | nfan 1906 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) |
31 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑗0 < ((1 /
𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
32 | | stoweidlem44.8 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)∃𝑗 ∈ (1...𝑀)0 < ((𝐺‘𝑗)‘𝑡)) |
33 | 32 | r19.21bi 3122 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑗 ∈ (1...𝑀)0 < ((𝐺‘𝑗)‘𝑡)) |
34 | | df-rex 3060 |
. . . . . . . . 9
⊢
(∃𝑗 ∈
(1...𝑀)0 < ((𝐺‘𝑗)‘𝑡) ↔ ∃𝑗(𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) |
35 | 33, 34 | sylib 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → ∃𝑗(𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) |
36 | 6 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (1 / 𝑀) ∈ ℝ) |
37 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 𝜑) |
38 | | eldifi 4027 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (𝑇 ∖ 𝑈) → 𝑡 ∈ 𝑇) |
39 | 38 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 𝑡 ∈ 𝑇) |
40 | | fzfid 13444 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1...𝑀) ∈ Fin) |
41 | 8, 7, 21 | stoweidlem15 43138 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝑇) → (((𝐺‘𝑖)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺‘𝑖)‘𝑡) ∧ ((𝐺‘𝑖)‘𝑡) ≤ 1)) |
42 | 41 | an32s 652 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺‘𝑖)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺‘𝑖)‘𝑡) ∧ ((𝐺‘𝑖)‘𝑡) ≤ 1)) |
43 | 42 | simp1d 1143 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
44 | 40, 43 | fsumrecl 15196 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
45 | 37, 39, 44 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
46 | 5 | nnred 11743 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℝ) |
47 | 5 | nngt0d 11777 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝑀) |
48 | 46, 47 | recgt0d 11664 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (1 / 𝑀)) |
49 | 48 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < (1 / 𝑀)) |
50 | | 0red 10734 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 ∈ ℝ) |
51 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 𝑗 ∈ (1...𝑀)) |
52 | 37, 51, 39 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇)) |
53 | | snfi 8654 |
. . . . . . . . . . . . . . 15
⊢ {𝑗} ∈ Fin |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → {𝑗} ∈ Fin) |
55 | | simpl1 1192 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝜑) |
56 | | simpl3 1194 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑡 ∈ 𝑇) |
57 | | elsni 4543 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ {𝑗} → 𝑖 = 𝑗) |
58 | 57 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑖 = 𝑗) |
59 | | simpl2 1193 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑗 ∈ (1...𝑀)) |
60 | 58, 59 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑖 ∈ (1...𝑀)) |
61 | 55, 56, 60, 43 | syl21anc 837 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
62 | 54, 61 | fsumrecl 15196 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
63 | 52, 62 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
64 | 50, 63 | readdcld 10760 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (0 + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡)) ∈ ℝ) |
65 | | fzfi 13443 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑀) ∈
Fin |
66 | | diffi 8839 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑀) ∈ Fin
→ ((1...𝑀) ∖
{𝑗}) ∈
Fin) |
67 | 65, 66 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((1...𝑀) ∖ {𝑗}) ∈ Fin) |
68 | | eldifi 4027 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ((1...𝑀) ∖ {𝑗}) → 𝑖 ∈ (1...𝑀)) |
69 | 68, 43 | sylan2 596 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
70 | 67, 69 | fsumrecl 15196 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
71 | 37, 39, 70 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
72 | 71, 63 | readdcld 10760 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡)) ∈ ℝ) |
73 | | 00id 10905 |
. . . . . . . . . . . 12
⊢ (0 + 0) =
0 |
74 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < ((𝐺‘𝑗)‘𝑡)) |
75 | 8, 7, 21 | stoweidlem15 43138 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝑇) → (((𝐺‘𝑗)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺‘𝑗)‘𝑡) ∧ ((𝐺‘𝑗)‘𝑡) ≤ 1)) |
76 | 75 | simp1d 1143 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑡 ∈ 𝑇) → ((𝐺‘𝑗)‘𝑡) ∈ ℝ) |
77 | 37, 51, 39, 76 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → ((𝐺‘𝑗)‘𝑡) ∈ ℝ) |
78 | 77 | recnd 10759 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → ((𝐺‘𝑗)‘𝑡) ∈ ℂ) |
79 | | fveq2 6686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑗 → (𝐺‘𝑖) = (𝐺‘𝑗)) |
80 | 79 | fveq1d 6688 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑗 → ((𝐺‘𝑖)‘𝑡) = ((𝐺‘𝑗)‘𝑡)) |
81 | 80 | sumsn 15206 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ (1...𝑀) ∧ ((𝐺‘𝑗)‘𝑡) ∈ ℂ) → Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡) = ((𝐺‘𝑗)‘𝑡)) |
82 | 51, 78, 81 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡) = ((𝐺‘𝑗)‘𝑡)) |
83 | 74, 82 | breqtrrd 5068 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡)) |
84 | 50, 63, 50, 83 | ltadd2dd 10889 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (0 + 0) < (0 + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) |
85 | 73, 84 | eqbrtrrid 5076 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < (0 + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) |
86 | | 0red 10734 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → 0 ∈ ℝ) |
87 | 70 | 3adant2 1132 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
88 | | simpll 767 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 𝜑) |
89 | 68 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑖 ∈ (1...𝑀)) |
90 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑡 ∈ 𝑇) |
91 | 88, 89, 90, 41 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → (((𝐺‘𝑖)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺‘𝑖)‘𝑡) ∧ ((𝐺‘𝑖)‘𝑡) ≤ 1)) |
92 | 91 | simp2d 1144 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 0 ≤ ((𝐺‘𝑖)‘𝑡)) |
93 | 67, 69, 92 | fsumge0 15255 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ≤ Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡)) |
94 | 93 | 3adant2 1132 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → 0 ≤ Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡)) |
95 | 86, 87, 62, 94 | leadd1dd 11344 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (0 + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡)) ≤ (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) |
96 | 52, 95 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → (0 + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡)) ≤ (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) |
97 | 50, 64, 72, 85, 96 | ltletrd 10890 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) |
98 | | eldifn 4028 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((1...𝑀) ∖ {𝑗}) → ¬ 𝑥 ∈ {𝑗}) |
99 | | imnan 403 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ((1...𝑀) ∖ {𝑗}) → ¬ 𝑥 ∈ {𝑗}) ↔ ¬ (𝑥 ∈ ((1...𝑀) ∖ {𝑗}) ∧ 𝑥 ∈ {𝑗})) |
100 | 98, 99 | mpbi 233 |
. . . . . . . . . . . . . . 15
⊢ ¬
(𝑥 ∈ ((1...𝑀) ∖ {𝑗}) ∧ 𝑥 ∈ {𝑗}) |
101 | | elin 3869 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (((1...𝑀) ∖ {𝑗}) ∩ {𝑗}) ↔ (𝑥 ∈ ((1...𝑀) ∖ {𝑗}) ∧ 𝑥 ∈ {𝑗})) |
102 | 100, 101 | mtbir 326 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑥 ∈ (((1...𝑀) ∖ {𝑗}) ∩ {𝑗}) |
103 | 102 | nel0 4249 |
. . . . . . . . . . . . 13
⊢
(((1...𝑀) ∖
{𝑗}) ∩ {𝑗}) = ∅ |
104 | 103 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (((1...𝑀) ∖ {𝑗}) ∩ {𝑗}) = ∅) |
105 | | undif1 4375 |
. . . . . . . . . . . . 13
⊢
(((1...𝑀) ∖
{𝑗}) ∪ {𝑗}) = ((1...𝑀) ∪ {𝑗}) |
106 | | snssi 4706 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (1...𝑀) → {𝑗} ⊆ (1...𝑀)) |
107 | 106 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → {𝑗} ⊆ (1...𝑀)) |
108 | | ssequn2 4083 |
. . . . . . . . . . . . . 14
⊢ ({𝑗} ⊆ (1...𝑀) ↔ ((1...𝑀) ∪ {𝑗}) = (1...𝑀)) |
109 | 107, 108 | sylib 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → ((1...𝑀) ∪ {𝑗}) = (1...𝑀)) |
110 | 105, 109 | eqtr2id 2787 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (1...𝑀) = (((1...𝑀) ∖ {𝑗}) ∪ {𝑗})) |
111 | | fzfid 13444 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (1...𝑀) ∈ Fin) |
112 | 43 | 3adantl2 1168 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
113 | 112 | recnd 10759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺‘𝑖)‘𝑡) ∈ ℂ) |
114 | 104, 110,
111, 113 | fsumsplit 15202 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) = (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) |
115 | 52, 114 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡) = (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺‘𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺‘𝑖)‘𝑡))) |
116 | 97, 115 | breqtrrd 5068 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
117 | 36, 45, 49, 116 | mulgt0d 10885 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺‘𝑗)‘𝑡))) → 0 < ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
118 | 30, 31, 35, 117 | exlimdd 2222 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 0 < ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
119 | 8, 2, 5, 7, 21 | stoweidlem30 43153 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑃‘𝑡) = ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
120 | 38, 119 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (𝑃‘𝑡) = ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
121 | 118, 120 | breqtrrd 5068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 0 < (𝑃‘𝑡)) |
122 | 121 | ex 416 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ (𝑇 ∖ 𝑈) → 0 < (𝑃‘𝑡))) |
123 | 1, 122 | ralrimi 3129 |
. . . 4
⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡)) |
124 | 25, 27, 123 | 3jca 1129 |
. . 3
⊢ (𝜑 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1) ∧ (𝑃‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡))) |
125 | | eleq1 2821 |
. . . . . 6
⊢ (𝑝 = 𝑃 → (𝑝 ∈ 𝐴 ↔ 𝑃 ∈ 𝐴)) |
126 | | nfmpt1 5138 |
. . . . . . . . . 10
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
127 | 2, 126 | nfcxfr 2898 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝑃 |
128 | 127 | nfeq2 2917 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑝 = 𝑃 |
129 | | fveq1 6685 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → (𝑝‘𝑡) = (𝑃‘𝑡)) |
130 | 129 | breq2d 5052 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → (0 ≤ (𝑝‘𝑡) ↔ 0 ≤ (𝑃‘𝑡))) |
131 | 129 | breq1d 5050 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → ((𝑝‘𝑡) ≤ 1 ↔ (𝑃‘𝑡) ≤ 1)) |
132 | 130, 131 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → ((0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ↔ (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))) |
133 | 128, 132 | ralbid 3146 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1))) |
134 | | fveq1 6685 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (𝑝‘𝑍) = (𝑃‘𝑍)) |
135 | 134 | eqeq1d 2741 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → ((𝑝‘𝑍) = 0 ↔ (𝑃‘𝑍) = 0)) |
136 | 129 | breq2d 5052 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → (0 < (𝑝‘𝑡) ↔ 0 < (𝑃‘𝑡))) |
137 | 128, 136 | ralbid 3146 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → (∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡))) |
138 | 133, 135,
137 | 3anbi123d 1437 |
. . . . . 6
⊢ (𝑝 = 𝑃 → ((∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1) ∧ (𝑃‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡)))) |
139 | 125, 138 | anbi12d 634 |
. . . . 5
⊢ (𝑝 = 𝑃 → ((𝑝 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡))) ↔ (𝑃 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1) ∧ (𝑃‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑃‘𝑡))))) |
140 | 139 | spcegv 3504 |
. . . 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 3060 |
. 2
⊢
(∃𝑝 ∈
𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)) ↔ ∃𝑝(𝑝 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡)))) |
144 | 142, 143 | sylibr 237 |
1
⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑝‘𝑡) ∧ (𝑝‘𝑡) ≤ 1) ∧ (𝑝‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)0 < (𝑝‘𝑡))) |