Metamath Proof Explorer

Theorem stoweidlem44

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__(t_0) = 0, and p > 0 on T - U. Z is used to represent t_0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses 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 stoweidlem44 ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem44.1 ⊢ Ⅎ 𝑗 𝜑
2 stoweidlem44.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem44.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
4 stoweidlem44.4 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
5 stoweidlem44.5 ⊢ 𝑃 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
6 stoweidlem44.6 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7 stoweidlem44.7 ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝑄 )
8 stoweidlem44.8 ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) )
9 stoweidlem44.9 ⊢ 𝑇 = ∪ 𝐽
10 stoweidlem44.10 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
11 stoweidlem44.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
12 stoweidlem44.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
13 stoweidlem44.13 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
14 stoweidlem44.14 ⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
15 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
16 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑀 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 1 / 𝑀 ) )
17 6 nnrecred ⊢ ( 𝜑 → ( 1 / 𝑀 ) ∈ ℝ )
18 ssrab2 ⊢ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } ⊆ 𝐴
19 4 18 eqsstri ⊢ 𝑄 ⊆ 𝐴
20 fss ⊢ ( ( 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝑄 ∧ 𝑄 ⊆ 𝐴 ) → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
21 7 19 20 sylancl ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝐴 )
22 eqid ⊢ ( 𝐽 Cn 𝐾 ) = ( 𝐽 Cn 𝐾 )
23 10 sselda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ ( 𝐽 Cn 𝐾 ) )
24 3 9 22 23 fcnre ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
25 2 5 15 16 6 17 21 11 12 13 24 stoweidlem32 ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
26 4 5 6 7 24 stoweidlem38 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
27 26 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 → ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ) )
28 2 27 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
29 4 5 6 7 24 14 stoweidlem37 ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑍 ) = 0 )
30 nfv ⊢ Ⅎ 𝑗 𝑡 ∈ ( 𝑇 ∖ 𝑈 )
31 1 30 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) )
32 nfv ⊢ Ⅎ 𝑗 0 < ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
33 8 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) )
34 df-rex ⊢ ( ∃ 𝑗 ∈ ( 1 ... 𝑀 ) 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ↔ ∃ 𝑗 ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) )
35 33 34 sylib ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ∃ 𝑗 ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) )
36 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ( 1 / 𝑀 ) ∈ ℝ )
37 simpll ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 𝜑 )
38 eldifi ⊢ ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) → 𝑡 ∈ 𝑇 )
39 38 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 𝑡 ∈ 𝑇 )
40 fzfid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 ... 𝑀 ) ∈ Fin )
41 4 7 24 stoweidlem15 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) )
42 41 an32s ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) )
43 42 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
44 40 43 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
45 37 39 44 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
46 6 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
47 6 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
48 46 47 recgt0d ⊢ ( 𝜑 → 0 < ( 1 / 𝑀 ) )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 0 < ( 1 / 𝑀 ) )
50 0red ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 0 ∈ ℝ )
51 simprl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
52 37 51 39 3jca ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) )
53 snfi ⊢ { 𝑗 } ∈ Fin
54 53 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → { 𝑗 } ∈ Fin )
55 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ { 𝑗 } ) → 𝜑 )
56 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ { 𝑗 } ) → 𝑡 ∈ 𝑇 )
57 elsni ⊢ ( 𝑖 ∈ { 𝑗 } → 𝑖 = 𝑗 )
58 57 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ { 𝑗 } ) → 𝑖 = 𝑗 )
59 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ { 𝑗 } ) → 𝑗 ∈ ( 1 ... 𝑀 ) )
60 58 59 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ { 𝑗 } ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
61 55 56 60 43 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ { 𝑗 } ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
62 54 61 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
63 52 62 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
64 50 63 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ( 0 + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
65 fzfi ⊢ ( 1 ... 𝑀 ) ∈ Fin
66 diffi ⊢ ( ( 1 ... 𝑀 ) ∈ Fin → ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∈ Fin )
67 65 66 mp1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∈ Fin )
68 eldifi ⊢ ( 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
69 68 43 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
70 67 69 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
71 37 39 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
72 71 63 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ( Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
73 00id ⊢ ( 0 + 0 ) = 0
74 simprr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) )
75 4 7 24 stoweidlem15 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) )
76 75 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ∈ ℝ )
77 37 51 39 76 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ∈ ℝ )
78 77 recnd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ∈ ℂ )
79 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) )
80 79 fveq1d ⊢ ( 𝑖 = 𝑗 → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) )
81 80 sumsn ⊢ ( ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ∈ ℂ ) → Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) )
82 51 78 81 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) )
83 74 82 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 0 < Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
84 50 63 50 83 ltadd2dd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ( 0 + 0 ) < ( 0 + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
85 73 84 eqbrtrrid ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 0 < ( 0 + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
86 0red ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ∈ ℝ )
87 70 3adant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
88 simpll ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ) → 𝜑 )
89 68 adantl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
90 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ) → 𝑡 ∈ 𝑇 )
91 88 89 90 41 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ) → ( ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) )
92 91 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ) → 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
93 67 69 92 fsumge0 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
94 93 3adant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
95 86 87 62 94 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( 0 + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ≤ ( Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
96 52 95 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ( 0 + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) ≤ ( Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
97 50 64 72 85 96 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 0 < ( Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
98 eldifn ⊢ ( 𝑥 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) → ¬ 𝑥 ∈ { 𝑗 } )
99 imnan ⊢ ( ( 𝑥 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) → ¬ 𝑥 ∈ { 𝑗 } ) ↔ ¬ ( 𝑥 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∧ 𝑥 ∈ { 𝑗 } ) )
100 98 99 mpbi ⊢ ¬ ( 𝑥 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∧ 𝑥 ∈ { 𝑗 } )
101 elin ⊢ ( 𝑥 ∈ ( ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∩ { 𝑗 } ) ↔ ( 𝑥 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∧ 𝑥 ∈ { 𝑗 } ) )
102 100 101 mtbir ⊢ ¬ 𝑥 ∈ ( ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∩ { 𝑗 } )
103 102 nel0 ⊢ ( ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∩ { 𝑗 } ) = ∅
104 103 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∩ { 𝑗 } ) = ∅ )
105 undif1 ⊢ ( ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∪ { 𝑗 } ) = ( ( 1 ... 𝑀 ) ∪ { 𝑗 } )
106 snssi ⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → { 𝑗 } ⊆ ( 1 ... 𝑀 ) )
107 106 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → { 𝑗 } ⊆ ( 1 ... 𝑀 ) )
108 ssequn2 ⊢ ( { 𝑗 } ⊆ ( 1 ... 𝑀 ) ↔ ( ( 1 ... 𝑀 ) ∪ { 𝑗 } ) = ( 1 ... 𝑀 ) )
109 107 108 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 1 ... 𝑀 ) ∪ { 𝑗 } ) = ( 1 ... 𝑀 ) )
110 105 109 eqtr2id ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( 1 ... 𝑀 ) = ( ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ∪ { 𝑗 } ) )
111 fzfid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → ( 1 ... 𝑀 ) ∈ Fin )
112 43 3adantl2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
113 112 recnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℂ )
114 104 110 111 113 fsumsplit ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 𝑡 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
115 52 114 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) = ( Σ 𝑖 ∈ ( ( 1 ... 𝑀 ) ∖ { 𝑗 } ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) + Σ 𝑖 ∈ { 𝑗 } ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
116 97 115 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 0 < Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) )
117 36 45 49 116 mulgt0d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑗 ∈ ( 1 ... 𝑀 ) ∧ 0 < ( ( 𝐺 ‘ 𝑗 ) ‘ 𝑡 ) ) ) → 0 < ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
118 31 32 35 117 exlimdd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 0 < ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
119 4 5 6 7 24 stoweidlem30 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑡 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
120 38 119 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑃 ‘ 𝑡 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
121 118 120 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 0 < ( 𝑃 ‘ 𝑡 ) )
122 121 ex ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) → 0 < ( 𝑃 ‘ 𝑡 ) ) )
123 2 122 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑃 ‘ 𝑡 ) )
124 28 29 123 3jca ⊢ ( 𝜑 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑃 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑃 ‘ 𝑡 ) ) )
125 eleq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∈ 𝐴 ↔ 𝑃 ∈ 𝐴 ) )
126 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
127 5 126 nfcxfr ⊢ Ⅎ 𝑡 𝑃
128 127 nfeq2 ⊢ Ⅎ 𝑡 𝑝 = 𝑃
129 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 𝑡 ) = ( 𝑃 ‘ 𝑡 ) )
130 129 breq2d ⊢ ( 𝑝 = 𝑃 → ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ↔ 0 ≤ ( 𝑃 ‘ 𝑡 ) ) )
131 129 breq1d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ 𝑡 ) ≤ 1 ↔ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
132 130 131 anbi12d ⊢ ( 𝑝 = 𝑃 → ( ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ) )
133 128 132 ralbid ⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ) )
134 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 𝑍 ) = ( 𝑃 ‘ 𝑍 ) )
135 134 eqeq1d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ 𝑍 ) = 0 ↔ ( 𝑃 ‘ 𝑍 ) = 0 ) )
136 129 breq2d ⊢ ( 𝑝 = 𝑃 → ( 0 < ( 𝑝 ‘ 𝑡 ) ↔ 0 < ( 𝑃 ‘ 𝑡 ) ) )
137 128 136 ralbid ⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑃 ‘ 𝑡 ) ) )
138 133 135 137 3anbi123d ⊢ ( 𝑝 = 𝑃 → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑃 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑃 ‘ 𝑡 ) ) ) )
139 125 138 anbi12d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ↔ ( 𝑃 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑃 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑃 ‘ 𝑡 ) ) ) ) )
140 139 spcegv ⊢ ( 𝑃 ∈ 𝐴 → ( ( 𝑃 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑃 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑃 ‘ 𝑡 ) ) ) → ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) )
141 25 140 syl ⊢ ( 𝜑 → ( ( 𝑃 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑃 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑃 ‘ 𝑡 ) ) ) → ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) ) )
142 25 124 141 mp2and ⊢ ( 𝜑 → ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) )
143 df-rex ⊢ ( ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ↔ ∃ 𝑝 ( 𝑝 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) )
144 142 143 sylibr ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )