Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem44 Structured version   Visualization version   GIF version

Theorem stoweidlem44 43585
Description: This lemma is used to prove the existence of a function p as in Lemma 1 of [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem44.1 𝑗𝜑
stoweidlem44.2 𝑡𝜑
stoweidlem44.3 𝐾 = (topGen‘ran (,))
stoweidlem44.4 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
stoweidlem44.5 𝑃 = (𝑡𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡)))
stoweidlem44.6 (𝜑𝑀 ∈ ℕ)
stoweidlem44.7 (𝜑𝐺:(1...𝑀)⟶𝑄)
stoweidlem44.8 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)∃𝑗 ∈ (1...𝑀)0 < ((𝐺𝑗)‘𝑡))
stoweidlem44.9 𝑇 = 𝐽
stoweidlem44.10 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
stoweidlem44.11 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
stoweidlem44.12 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
stoweidlem44.13 ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
stoweidlem44.14 (𝜑𝑍𝑇)
Assertion
Ref Expression
stoweidlem44 (𝜑 → ∃𝑝𝐴 (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)))
Distinct variable groups:   𝑓,𝑔,𝑖,𝑡,𝐺   𝑓,𝑗,𝑖,𝑡,𝐺   𝐴,𝑓,𝑔   𝑓,𝑀,𝑔,𝑖,𝑡   𝑇,𝑓,𝑔,𝑖,𝑡   𝜑,𝑓,𝑔,𝑖   ,𝑖,𝑗,𝑡,𝐺   𝐴,   𝑇,,𝑗   ,𝑍,𝑖,𝑡   𝑥,𝑗,𝑀,𝑡   𝑈,𝑗   𝑡,𝑝,𝑇   𝐴,𝑝   𝑃,𝑝   𝑈,𝑝   𝑍,𝑝   𝑥,𝐴   𝑥,𝑇   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑡,,𝑗,𝑝)   𝐴(𝑡,𝑖,𝑗)   𝑃(𝑥,𝑡,𝑓,𝑔,,𝑖,𝑗)   𝑄(𝑥,𝑡,𝑓,𝑔,,𝑖,𝑗,𝑝)   𝑈(𝑥,𝑡,𝑓,𝑔,,𝑖)   𝐺(𝑥,𝑝)   𝐽(𝑥,𝑡,𝑓,𝑔,,𝑖,𝑗,𝑝)   𝐾(𝑥,𝑡,𝑓,𝑔,,𝑖,𝑗,𝑝)   𝑀(,𝑝)   𝑍(𝑥,𝑓,𝑔,𝑗)

Proof of Theorem stoweidlem44
StepHypRef Expression
1 stoweidlem44.2 . . . 4 𝑡𝜑
2 stoweidlem44.5 . . . 4 𝑃 = (𝑡𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡)))
3 eqid 2738 . . . 4 (𝑡𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡)) = (𝑡𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡))
4 eqid 2738 . . . 4 (𝑡𝑇 ↦ (1 / 𝑀)) = (𝑡𝑇 ↦ (1 / 𝑀))
5 stoweidlem44.6 . . . 4 (𝜑𝑀 ∈ ℕ)
65nnrecred 12024 . . . 4 (𝜑 → (1 / 𝑀) ∈ ℝ)
7 stoweidlem44.7 . . . . 5 (𝜑𝐺:(1...𝑀)⟶𝑄)
8 stoweidlem44.4 . . . . . 6 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
9 ssrab2 4013 . . . . . 6 {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))} ⊆ 𝐴
108, 9eqsstri 3955 . . . . 5 𝑄𝐴
11 fss 6617 . . . . 5 ((𝐺:(1...𝑀)⟶𝑄𝑄𝐴) → 𝐺:(1...𝑀)⟶𝐴)
127, 10, 11sylancl 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 2738 . . . . 5 (𝐽 Cn 𝐾) = (𝐽 Cn 𝐾)
19 stoweidlem44.10 . . . . . 6 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
2019sselda 3921 . . . . 5 ((𝜑𝑓𝐴) → 𝑓 ∈ (𝐽 Cn 𝐾))
2116, 17, 18, 20fcnre 42568 . . . 4 ((𝜑𝑓𝐴) → 𝑓:𝑇⟶ℝ)
221, 2, 3, 4, 5, 6, 12, 13, 14, 15, 21stoweidlem32 43573 . . 3 (𝜑𝑃𝐴)
238, 2, 5, 7, 21stoweidlem38 43579 . . . . . 6 ((𝜑𝑡𝑇) → (0 ≤ (𝑃𝑡) ∧ (𝑃𝑡) ≤ 1))
2423ex 413 . . . . 5 (𝜑 → (𝑡𝑇 → (0 ≤ (𝑃𝑡) ∧ (𝑃𝑡) ≤ 1)))
251, 24ralrimi 3141 . . . 4 (𝜑 → ∀𝑡𝑇 (0 ≤ (𝑃𝑡) ∧ (𝑃𝑡) ≤ 1))
26 stoweidlem44.14 . . . . 5 (𝜑𝑍𝑇)
278, 2, 5, 7, 21, 26stoweidlem37 43578 . . . 4 (𝜑 → (𝑃𝑍) = 0)
28 stoweidlem44.1 . . . . . . . . 9 𝑗𝜑
29 nfv 1917 . . . . . . . . 9 𝑗 𝑡 ∈ (𝑇𝑈)
3028, 29nfan 1902 . . . . . . . 8 𝑗(𝜑𝑡 ∈ (𝑇𝑈))
31 nfv 1917 . . . . . . . 8 𝑗0 < ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡))
32 stoweidlem44.8 . . . . . . . . . 10 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)∃𝑗 ∈ (1...𝑀)0 < ((𝐺𝑗)‘𝑡))
3332r19.21bi 3134 . . . . . . . . 9 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑗 ∈ (1...𝑀)0 < ((𝐺𝑗)‘𝑡))
34 df-rex 3070 . . . . . . . . 9 (∃𝑗 ∈ (1...𝑀)0 < ((𝐺𝑗)‘𝑡) ↔ ∃𝑗(𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡)))
3533, 34sylib 217 . . . . . . . 8 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑗(𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡)))
366ad2antrr 723 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → (1 / 𝑀) ∈ ℝ)
37 simpll 764 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 𝜑)
38 eldifi 4061 . . . . . . . . . . 11 (𝑡 ∈ (𝑇𝑈) → 𝑡𝑇)
3938ad2antlr 724 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 𝑡𝑇)
40 fzfid 13693 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → (1...𝑀) ∈ Fin)
418, 7, 21stoweidlem15 43556 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (1...𝑀)) ∧ 𝑡𝑇) → (((𝐺𝑖)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺𝑖)‘𝑡) ∧ ((𝐺𝑖)‘𝑡) ≤ 1))
4241an32s 649 . . . . . . . . . . . 12 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → (((𝐺𝑖)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺𝑖)‘𝑡) ∧ ((𝐺𝑖)‘𝑡) ≤ 1))
4342simp1d 1141 . . . . . . . . . . 11 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺𝑖)‘𝑡) ∈ ℝ)
4440, 43fsumrecl 15446 . . . . . . . . . 10 ((𝜑𝑡𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡) ∈ ℝ)
4537, 39, 44syl2anc 584 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡) ∈ ℝ)
465nnred 11988 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
475nngt0d 12022 . . . . . . . . . . 11 (𝜑 → 0 < 𝑀)
4846, 47recgt0d 11909 . . . . . . . . . 10 (𝜑 → 0 < (1 / 𝑀))
4948ad2antrr 723 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 0 < (1 / 𝑀))
50 0red 10978 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 0 ∈ ℝ)
51 simprl 768 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 𝑗 ∈ (1...𝑀))
5237, 51, 393jca 1127 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → (𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇))
53 snfi 8834 . . . . . . . . . . . . . . 15 {𝑗} ∈ Fin
5453a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → {𝑗} ∈ Fin)
55 simpl1 1190 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝜑)
56 simpl3 1192 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑡𝑇)
57 elsni 4578 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ {𝑗} → 𝑖 = 𝑗)
5857adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑖 = 𝑗)
59 simpl2 1191 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑗 ∈ (1...𝑀))
6058, 59eqeltrd 2839 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) ∧ 𝑖 ∈ {𝑗}) → 𝑖 ∈ (1...𝑀))
6155, 56, 60, 43syl21anc 835 . . . . . . . . . . . . . 14 (((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) ∧ 𝑖 ∈ {𝑗}) → ((𝐺𝑖)‘𝑡) ∈ ℝ)
6254, 61fsumrecl 15446 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡) ∈ ℝ)
6352, 62syl 17 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡) ∈ ℝ)
6450, 63readdcld 11004 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → (0 + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)) ∈ ℝ)
65 fzfi 13692 . . . . . . . . . . . . . . 15 (1...𝑀) ∈ Fin
66 diffi 8962 . . . . . . . . . . . . . . 15 ((1...𝑀) ∈ Fin → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
6765, 66mp1i 13 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → ((1...𝑀) ∖ {𝑗}) ∈ Fin)
68 eldifi 4061 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((1...𝑀) ∖ {𝑗}) → 𝑖 ∈ (1...𝑀))
6968, 43sylan2 593 . . . . . . . . . . . . . 14 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → ((𝐺𝑖)‘𝑡) ∈ ℝ)
7067, 69fsumrecl 15446 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡) ∈ ℝ)
7137, 39, 70syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡) ∈ ℝ)
7271, 63readdcld 11004 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)) ∈ ℝ)
73 00id 11150 . . . . . . . . . . . 12 (0 + 0) = 0
74 simprr 770 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 0 < ((𝐺𝑗)‘𝑡))
758, 7, 21stoweidlem15 43556 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑡𝑇) → (((𝐺𝑗)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺𝑗)‘𝑡) ∧ ((𝐺𝑗)‘𝑡) ≤ 1))
7675simp1d 1141 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (1...𝑀)) ∧ 𝑡𝑇) → ((𝐺𝑗)‘𝑡) ∈ ℝ)
7737, 51, 39, 76syl21anc 835 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → ((𝐺𝑗)‘𝑡) ∈ ℝ)
7877recnd 11003 . . . . . . . . . . . . . . 15 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → ((𝐺𝑗)‘𝑡) ∈ ℂ)
79 fveq2 6774 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → (𝐺𝑖) = (𝐺𝑗))
8079fveq1d 6776 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 → ((𝐺𝑖)‘𝑡) = ((𝐺𝑗)‘𝑡))
8180sumsn 15458 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (1...𝑀) ∧ ((𝐺𝑗)‘𝑡) ∈ ℂ) → Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡) = ((𝐺𝑗)‘𝑡))
8251, 78, 81syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡) = ((𝐺𝑗)‘𝑡))
8374, 82breqtrrd 5102 . . . . . . . . . . . . 13 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 0 < Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡))
8450, 63, 50, 83ltadd2dd 11134 . . . . . . . . . . . 12 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → (0 + 0) < (0 + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)))
8573, 84eqbrtrrid 5110 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 0 < (0 + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)))
86 0red 10978 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → 0 ∈ ℝ)
87703adant2 1130 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡) ∈ ℝ)
88 simpll 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 𝜑)
8968adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑖 ∈ (1...𝑀))
90 simplr 766 . . . . . . . . . . . . . . . . 17 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 𝑡𝑇)
9188, 89, 90, 41syl21anc 835 . . . . . . . . . . . . . . . 16 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → (((𝐺𝑖)‘𝑡) ∈ ℝ ∧ 0 ≤ ((𝐺𝑖)‘𝑡) ∧ ((𝐺𝑖)‘𝑡) ≤ 1))
9291simp2d 1142 . . . . . . . . . . . . . . 15 (((𝜑𝑡𝑇) ∧ 𝑖 ∈ ((1...𝑀) ∖ {𝑗})) → 0 ≤ ((𝐺𝑖)‘𝑡))
9367, 69, 92fsumge0 15507 . . . . . . . . . . . . . 14 ((𝜑𝑡𝑇) → 0 ≤ Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡))
94933adant2 1130 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → 0 ≤ Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡))
9586, 87, 62, 94leadd1dd 11589 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → (0 + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)) ≤ (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)))
9652, 95syl 17 . . . . . . . . . . 11 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → (0 + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)) ≤ (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)))
9750, 64, 72, 85, 96ltletrd 11135 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 0 < (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)))
98 eldifn 4062 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ((1...𝑀) ∖ {𝑗}) → ¬ 𝑥 ∈ {𝑗})
99 imnan 400 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ((1...𝑀) ∖ {𝑗}) → ¬ 𝑥 ∈ {𝑗}) ↔ ¬ (𝑥 ∈ ((1...𝑀) ∖ {𝑗}) ∧ 𝑥 ∈ {𝑗}))
10098, 99mpbi 229 . . . . . . . . . . . . . . 15 ¬ (𝑥 ∈ ((1...𝑀) ∖ {𝑗}) ∧ 𝑥 ∈ {𝑗})
101 elin 3903 . . . . . . . . . . . . . . 15 (𝑥 ∈ (((1...𝑀) ∖ {𝑗}) ∩ {𝑗}) ↔ (𝑥 ∈ ((1...𝑀) ∖ {𝑗}) ∧ 𝑥 ∈ {𝑗}))
102100, 101mtbir 323 . . . . . . . . . . . . . 14 ¬ 𝑥 ∈ (((1...𝑀) ∖ {𝑗}) ∩ {𝑗})
103102nel0 4284 . . . . . . . . . . . . 13 (((1...𝑀) ∖ {𝑗}) ∩ {𝑗}) = ∅
104103a1i 11 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → (((1...𝑀) ∖ {𝑗}) ∩ {𝑗}) = ∅)
105 undif1 4409 . . . . . . . . . . . . 13 (((1...𝑀) ∖ {𝑗}) ∪ {𝑗}) = ((1...𝑀) ∪ {𝑗})
106 snssi 4741 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) → {𝑗} ⊆ (1...𝑀))
1071063ad2ant2 1133 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → {𝑗} ⊆ (1...𝑀))
108 ssequn2 4117 . . . . . . . . . . . . . 14 ({𝑗} ⊆ (1...𝑀) ↔ ((1...𝑀) ∪ {𝑗}) = (1...𝑀))
109107, 108sylib 217 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → ((1...𝑀) ∪ {𝑗}) = (1...𝑀))
110105, 109eqtr2id 2791 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → (1...𝑀) = (((1...𝑀) ∖ {𝑗}) ∪ {𝑗}))
111 fzfid 13693 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → (1...𝑀) ∈ Fin)
112433adantl2 1166 . . . . . . . . . . . . 13 (((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺𝑖)‘𝑡) ∈ ℝ)
113112recnd 11003 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) ∧ 𝑖 ∈ (1...𝑀)) → ((𝐺𝑖)‘𝑡) ∈ ℂ)
114104, 110, 111, 113fsumsplit 15453 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑀) ∧ 𝑡𝑇) → Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡) = (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)))
11552, 114syl 17 . . . . . . . . . 10 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡) = (Σ𝑖 ∈ ((1...𝑀) ∖ {𝑗})((𝐺𝑖)‘𝑡) + Σ𝑖 ∈ {𝑗} ((𝐺𝑖)‘𝑡)))
11697, 115breqtrrd 5102 . . . . . . . . 9 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 0 < Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡))
11736, 45, 49, 116mulgt0d 11130 . . . . . . . 8 (((𝜑𝑡 ∈ (𝑇𝑈)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((𝐺𝑗)‘𝑡))) → 0 < ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡)))
11830, 31, 35, 117exlimdd 2213 . . . . . . 7 ((𝜑𝑡 ∈ (𝑇𝑈)) → 0 < ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡)))
1198, 2, 5, 7, 21stoweidlem30 43571 . . . . . . . 8 ((𝜑𝑡𝑇) → (𝑃𝑡) = ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡)))
12038, 119sylan2 593 . . . . . . 7 ((𝜑𝑡 ∈ (𝑇𝑈)) → (𝑃𝑡) = ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡)))
121118, 120breqtrrd 5102 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → 0 < (𝑃𝑡))
122121ex 413 . . . . 5 (𝜑 → (𝑡 ∈ (𝑇𝑈) → 0 < (𝑃𝑡)))
1231, 122ralrimi 3141 . . . 4 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)0 < (𝑃𝑡))
12425, 27, 1233jca 1127 . . 3 (𝜑 → (∀𝑡𝑇 (0 ≤ (𝑃𝑡) ∧ (𝑃𝑡) ≤ 1) ∧ (𝑃𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑃𝑡)))
125 eleq1 2826 . . . . . 6 (𝑝 = 𝑃 → (𝑝𝐴𝑃𝐴))
126 nfmpt1 5182 . . . . . . . . . 10 𝑡(𝑡𝑇 ↦ ((1 / 𝑀) · Σ𝑖 ∈ (1...𝑀)((𝐺𝑖)‘𝑡)))
1272, 126nfcxfr 2905 . . . . . . . . 9 𝑡𝑃
128127nfeq2 2924 . . . . . . . 8 𝑡 𝑝 = 𝑃
129 fveq1 6773 . . . . . . . . . 10 (𝑝 = 𝑃 → (𝑝𝑡) = (𝑃𝑡))
130129breq2d 5086 . . . . . . . . 9 (𝑝 = 𝑃 → (0 ≤ (𝑝𝑡) ↔ 0 ≤ (𝑃𝑡)))
131129breq1d 5084 . . . . . . . . 9 (𝑝 = 𝑃 → ((𝑝𝑡) ≤ 1 ↔ (𝑃𝑡) ≤ 1))
132130, 131anbi12d 631 . . . . . . . 8 (𝑝 = 𝑃 → ((0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ↔ (0 ≤ (𝑃𝑡) ∧ (𝑃𝑡) ≤ 1)))
133128, 132ralbid 3161 . . . . . . 7 (𝑝 = 𝑃 → (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑃𝑡) ∧ (𝑃𝑡) ≤ 1)))
134 fveq1 6773 . . . . . . . 8 (𝑝 = 𝑃 → (𝑝𝑍) = (𝑃𝑍))
135134eqeq1d 2740 . . . . . . 7 (𝑝 = 𝑃 → ((𝑝𝑍) = 0 ↔ (𝑃𝑍) = 0))
136129breq2d 5086 . . . . . . . 8 (𝑝 = 𝑃 → (0 < (𝑝𝑡) ↔ 0 < (𝑃𝑡)))
137128, 136ralbid 3161 . . . . . . 7 (𝑝 = 𝑃 → (∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡) ↔ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑃𝑡)))
138133, 135, 1373anbi123d 1435 . . . . . 6 (𝑝 = 𝑃 → ((∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)) ↔ (∀𝑡𝑇 (0 ≤ (𝑃𝑡) ∧ (𝑃𝑡) ≤ 1) ∧ (𝑃𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑃𝑡))))
139125, 138anbi12d 631 . . . . 5 (𝑝 = 𝑃 → ((𝑝𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡))) ↔ (𝑃𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑃𝑡) ∧ (𝑃𝑡) ≤ 1) ∧ (𝑃𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑃𝑡)))))
140139spcegv 3536 . . . 4 (𝑃𝐴 → ((𝑃𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑃𝑡) ∧ (𝑃𝑡) ≤ 1) ∧ (𝑃𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑃𝑡))) → ∃𝑝(𝑝𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)))))
14122, 140syl 17 . . 3 (𝜑 → ((𝑃𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑃𝑡) ∧ (𝑃𝑡) ≤ 1) ∧ (𝑃𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑃𝑡))) → ∃𝑝(𝑝𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)))))
14222, 124, 141mp2and 696 . 2 (𝜑 → ∃𝑝(𝑝𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡))))
143 df-rex 3070 . 2 (∃𝑝𝐴 (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)) ↔ ∃𝑝(𝑝𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡))))
144142, 143sylibr 233 1 (𝜑 → ∃𝑝𝐴 (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1086   = wceq 1539  wex 1782  wnf 1786  wcel 2106  wral 3064  wrex 3065  {crab 3068  cdif 3884  cun 3885  cin 3886  wss 3887  c0 4256  {csn 4561   cuni 4839   class class class wbr 5074  cmpt 5157  ran crn 5590  wf 6429  cfv 6433  (class class class)co 7275  Fincfn 8733  cc 10869  cr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876   < clt 11009  cle 11010   / cdiv 11632  cn 11973  (,)cioo 13079  ...cfz 13239  Σcsu 15397  topGenctg 17148   Cn ccn 22375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-sup 9201  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-n0 12234  df-z 12320  df-uz 12583  df-rp 12731  df-ioo 13083  df-ico 13085  df-fz 13240  df-fzo 13383  df-seq 13722  df-exp 13783  df-hash 14045  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-clim 15197  df-sum 15398  df-topgen 17154  df-top 22043  df-topon 22060  df-bases 22096  df-cn 22378
This theorem is referenced by:  stoweidlem53  43594
  Copyright terms: Public domain W3C validator