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 44375
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 2733 . . . 4 (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘))
4 eqid 2733 . . . 4 (𝑑 ∈ 𝑇 ↦ (1 / 𝑀)) = (𝑑 ∈ 𝑇 ↦ (1 / 𝑀))
5 stoweidlem44.6 . . . 4 (πœ‘ β†’ 𝑀 ∈ β„•)
65nnrecred 12212 . . . 4 (πœ‘ β†’ (1 / 𝑀) ∈ ℝ)
7 stoweidlem44.7 . . . . 5 (πœ‘ β†’ 𝐺:(1...𝑀)βŸΆπ‘„)
8 stoweidlem44.4 . . . . . 6 𝑄 = {β„Ž ∈ 𝐴 ∣ ((β„Žβ€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1))}
9 ssrab2 4041 . . . . . 6 {β„Ž ∈ 𝐴 ∣ ((β„Žβ€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (β„Žβ€˜π‘‘) ∧ (β„Žβ€˜π‘‘) ≀ 1))} βŠ† 𝐴
108, 9eqsstri 3982 . . . . 5 𝑄 βŠ† 𝐴
11 fss 6689 . . . . 5 ((𝐺:(1...𝑀)βŸΆπ‘„ ∧ 𝑄 βŠ† 𝐴) β†’ 𝐺:(1...𝑀)⟢𝐴)
127, 10, 11sylancl 587 . . . 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 2733 . . . . 5 (𝐽 Cn 𝐾) = (𝐽 Cn 𝐾)
19 stoweidlem44.10 . . . . . 6 (πœ‘ β†’ 𝐴 βŠ† (𝐽 Cn 𝐾))
2019sselda 3948 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓 ∈ (𝐽 Cn 𝐾))
2116, 17, 18, 20fcnre 43322 . . . 4 ((πœ‘ ∧ 𝑓 ∈ 𝐴) β†’ 𝑓:π‘‡βŸΆβ„)
221, 2, 3, 4, 5, 6, 12, 13, 14, 15, 21stoweidlem32 44363 . . 3 (πœ‘ β†’ 𝑃 ∈ 𝐴)
238, 2, 5, 7, 21stoweidlem38 44369 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (0 ≀ (π‘ƒβ€˜π‘‘) ∧ (π‘ƒβ€˜π‘‘) ≀ 1))
2423ex 414 . . . . 5 (πœ‘ β†’ (𝑑 ∈ 𝑇 β†’ (0 ≀ (π‘ƒβ€˜π‘‘) ∧ (π‘ƒβ€˜π‘‘) ≀ 1)))
251, 24ralrimi 3239 . . . 4 (πœ‘ β†’ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘ƒβ€˜π‘‘) ∧ (π‘ƒβ€˜π‘‘) ≀ 1))
26 stoweidlem44.14 . . . . 5 (πœ‘ β†’ 𝑍 ∈ 𝑇)
278, 2, 5, 7, 21, 26stoweidlem37 44368 . . . 4 (πœ‘ β†’ (π‘ƒβ€˜π‘) = 0)
28 stoweidlem44.1 . . . . . . . . 9 β„²π‘—πœ‘
29 nfv 1918 . . . . . . . . 9 Ⅎ𝑗 𝑑 ∈ (𝑇 βˆ– π‘ˆ)
3028, 29nfan 1903 . . . . . . . 8 Ⅎ𝑗(πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ))
31 nfv 1918 . . . . . . . 8 Ⅎ𝑗0 < ((1 / 𝑀) Β· Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘))
32 stoweidlem44.8 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)βˆƒπ‘— ∈ (1...𝑀)0 < ((πΊβ€˜π‘—)β€˜π‘‘))
3332r19.21bi 3233 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) β†’ βˆƒπ‘— ∈ (1...𝑀)0 < ((πΊβ€˜π‘—)β€˜π‘‘))
34 df-rex 3071 . . . . . . . . 9 (βˆƒπ‘— ∈ (1...𝑀)0 < ((πΊβ€˜π‘—)β€˜π‘‘) ↔ βˆƒπ‘—(𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘)))
3533, 34sylib 217 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) β†’ βˆƒπ‘—(𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘)))
366ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ (1 / 𝑀) ∈ ℝ)
37 simpll 766 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ πœ‘)
38 eldifi 4090 . . . . . . . . . . 11 (𝑑 ∈ (𝑇 βˆ– π‘ˆ) β†’ 𝑑 ∈ 𝑇)
3938ad2antlr 726 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ 𝑑 ∈ 𝑇)
40 fzfid 13887 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (1...𝑀) ∈ Fin)
418, 7, 21stoweidlem15 44346 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ (1...𝑀)) ∧ 𝑑 ∈ 𝑇) β†’ (((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ ∧ 0 ≀ ((πΊβ€˜π‘–)β€˜π‘‘) ∧ ((πΊβ€˜π‘–)β€˜π‘‘) ≀ 1))
4241an32s 651 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) β†’ (((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ ∧ 0 ≀ ((πΊβ€˜π‘–)β€˜π‘‘) ∧ ((πΊβ€˜π‘–)β€˜π‘‘) ≀ 1))
4342simp1d 1143 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) β†’ ((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
4440, 43fsumrecl 15627 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
4537, 39, 44syl2anc 585 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
465nnred 12176 . . . . . . . . . . 11 (πœ‘ β†’ 𝑀 ∈ ℝ)
475nngt0d 12210 . . . . . . . . . . 11 (πœ‘ β†’ 0 < 𝑀)
4846, 47recgt0d 12097 . . . . . . . . . 10 (πœ‘ β†’ 0 < (1 / 𝑀))
4948ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ 0 < (1 / 𝑀))
50 0red 11166 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ 0 ∈ ℝ)
51 simprl 770 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ 𝑗 ∈ (1...𝑀))
5237, 51, 393jca 1129 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ (πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇))
53 snfi 8994 . . . . . . . . . . . . . . 15 {𝑗} ∈ Fin
5453a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ {𝑗} ∈ Fin)
55 simpl1 1192 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) β†’ πœ‘)
56 simpl3 1194 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) β†’ 𝑑 ∈ 𝑇)
57 elsni 4607 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ {𝑗} β†’ 𝑖 = 𝑗)
5857adantl 483 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) β†’ 𝑖 = 𝑗)
59 simpl2 1193 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) β†’ 𝑗 ∈ (1...𝑀))
6058, 59eqeltrd 2834 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) β†’ 𝑖 ∈ (1...𝑀))
6155, 56, 60, 43syl21anc 837 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ {𝑗}) β†’ ((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
6254, 61fsumrecl 15627 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
6352, 62syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
6450, 63readdcld 11192 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ (0 + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)) ∈ ℝ)
65 fzfi 13886 . . . . . . . . . . . . . . 15 (1...𝑀) ∈ Fin
66 diffi 9129 . . . . . . . . . . . . . . 15 ((1...𝑀) ∈ Fin β†’ ((1...𝑀) βˆ– {𝑗}) ∈ Fin)
6765, 66mp1i 13 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((1...𝑀) βˆ– {𝑗}) ∈ Fin)
68 eldifi 4090 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((1...𝑀) βˆ– {𝑗}) β†’ 𝑖 ∈ (1...𝑀))
6968, 43sylan2 594 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) βˆ– {𝑗})) β†’ ((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
7067, 69fsumrecl 15627 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
7137, 39, 70syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
7271, 63readdcld 11192 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ (Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘) + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)) ∈ ℝ)
73 00id 11338 . . . . . . . . . . . 12 (0 + 0) = 0
74 simprr 772 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))
758, 7, 21stoweidlem15 44346 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑑 ∈ 𝑇) β†’ (((πΊβ€˜π‘—)β€˜π‘‘) ∈ ℝ ∧ 0 ≀ ((πΊβ€˜π‘—)β€˜π‘‘) ∧ ((πΊβ€˜π‘—)β€˜π‘‘) ≀ 1))
7675simp1d 1143 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑗 ∈ (1...𝑀)) ∧ 𝑑 ∈ 𝑇) β†’ ((πΊβ€˜π‘—)β€˜π‘‘) ∈ ℝ)
7737, 51, 39, 76syl21anc 837 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ ((πΊβ€˜π‘—)β€˜π‘‘) ∈ ℝ)
7877recnd 11191 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ ((πΊβ€˜π‘—)β€˜π‘‘) ∈ β„‚)
79 fveq2 6846 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 β†’ (πΊβ€˜π‘–) = (πΊβ€˜π‘—))
8079fveq1d 6848 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑗 β†’ ((πΊβ€˜π‘–)β€˜π‘‘) = ((πΊβ€˜π‘—)β€˜π‘‘))
8180sumsn 15639 . . . . . . . . . . . . . . 15 ((𝑗 ∈ (1...𝑀) ∧ ((πΊβ€˜π‘—)β€˜π‘‘) ∈ β„‚) β†’ Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘) = ((πΊβ€˜π‘—)β€˜π‘‘))
8251, 78, 81syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘) = ((πΊβ€˜π‘—)β€˜π‘‘))
8374, 82breqtrrd 5137 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ 0 < Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘))
8450, 63, 50, 83ltadd2dd 11322 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ (0 + 0) < (0 + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)))
8573, 84eqbrtrrid 5145 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ 0 < (0 + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)))
86 0red 11166 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ 0 ∈ ℝ)
87703adant2 1132 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
88 simpll 766 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) βˆ– {𝑗})) β†’ πœ‘)
8968adantl 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) βˆ– {𝑗})) β†’ 𝑖 ∈ (1...𝑀))
90 simplr 768 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) βˆ– {𝑗})) β†’ 𝑑 ∈ 𝑇)
9188, 89, 90, 41syl21anc 837 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) βˆ– {𝑗})) β†’ (((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ ∧ 0 ≀ ((πΊβ€˜π‘–)β€˜π‘‘) ∧ ((πΊβ€˜π‘–)β€˜π‘‘) ≀ 1))
9291simp2d 1144 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ ((1...𝑀) βˆ– {𝑗})) β†’ 0 ≀ ((πΊβ€˜π‘–)β€˜π‘‘))
9367, 69, 92fsumge0 15688 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 0 ≀ Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘))
94933adant2 1132 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ 0 ≀ Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘))
9586, 87, 62, 94leadd1dd 11777 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ (0 + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)) ≀ (Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘) + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)))
9652, 95syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ (0 + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)) ≀ (Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘) + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)))
9750, 64, 72, 85, 96ltletrd 11323 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ 0 < (Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘) + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)))
98 eldifn 4091 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ((1...𝑀) βˆ– {𝑗}) β†’ Β¬ π‘₯ ∈ {𝑗})
99 imnan 401 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ ((1...𝑀) βˆ– {𝑗}) β†’ Β¬ π‘₯ ∈ {𝑗}) ↔ Β¬ (π‘₯ ∈ ((1...𝑀) βˆ– {𝑗}) ∧ π‘₯ ∈ {𝑗}))
10098, 99mpbi 229 . . . . . . . . . . . . . . 15 Β¬ (π‘₯ ∈ ((1...𝑀) βˆ– {𝑗}) ∧ π‘₯ ∈ {𝑗})
101 elin 3930 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (((1...𝑀) βˆ– {𝑗}) ∩ {𝑗}) ↔ (π‘₯ ∈ ((1...𝑀) βˆ– {𝑗}) ∧ π‘₯ ∈ {𝑗}))
102100, 101mtbir 323 . . . . . . . . . . . . . 14 Β¬ π‘₯ ∈ (((1...𝑀) βˆ– {𝑗}) ∩ {𝑗})
103102nel0 4314 . . . . . . . . . . . . 13 (((1...𝑀) βˆ– {𝑗}) ∩ {𝑗}) = βˆ…
104103a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ (((1...𝑀) βˆ– {𝑗}) ∩ {𝑗}) = βˆ…)
105 undif1 4439 . . . . . . . . . . . . 13 (((1...𝑀) βˆ– {𝑗}) βˆͺ {𝑗}) = ((1...𝑀) βˆͺ {𝑗})
106 snssi 4772 . . . . . . . . . . . . . . 15 (𝑗 ∈ (1...𝑀) β†’ {𝑗} βŠ† (1...𝑀))
1071063ad2ant2 1135 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ {𝑗} βŠ† (1...𝑀))
108 ssequn2 4147 . . . . . . . . . . . . . 14 ({𝑗} βŠ† (1...𝑀) ↔ ((1...𝑀) βˆͺ {𝑗}) = (1...𝑀))
109107, 108sylib 217 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ ((1...𝑀) βˆͺ {𝑗}) = (1...𝑀))
110105, 109eqtr2id 2786 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ (1...𝑀) = (((1...𝑀) βˆ– {𝑗}) βˆͺ {𝑗}))
111 fzfid 13887 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ (1...𝑀) ∈ Fin)
112433adantl2 1168 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) β†’ ((πΊβ€˜π‘–)β€˜π‘‘) ∈ ℝ)
113112recnd 11191 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑀)) β†’ ((πΊβ€˜π‘–)β€˜π‘‘) ∈ β„‚)
114104, 110, 111, 113fsumsplit 15634 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (1...𝑀) ∧ 𝑑 ∈ 𝑇) β†’ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘) = (Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘) + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)))
11552, 114syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘) = (Σ𝑖 ∈ ((1...𝑀) βˆ– {𝑗})((πΊβ€˜π‘–)β€˜π‘‘) + Σ𝑖 ∈ {𝑗} ((πΊβ€˜π‘–)β€˜π‘‘)))
11697, 115breqtrrd 5137 . . . . . . . . 9 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ 0 < Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘))
11736, 45, 49, 116mulgt0d 11318 . . . . . . . 8 (((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) ∧ (𝑗 ∈ (1...𝑀) ∧ 0 < ((πΊβ€˜π‘—)β€˜π‘‘))) β†’ 0 < ((1 / 𝑀) Β· Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)))
11830, 31, 35, 117exlimdd 2214 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) β†’ 0 < ((1 / 𝑀) Β· Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)))
1198, 2, 5, 7, 21stoweidlem30 44361 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (π‘ƒβ€˜π‘‘) = ((1 / 𝑀) Β· Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)))
12038, 119sylan2 594 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) β†’ (π‘ƒβ€˜π‘‘) = ((1 / 𝑀) Β· Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)))
121118, 120breqtrrd 5137 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ (𝑇 βˆ– π‘ˆ)) β†’ 0 < (π‘ƒβ€˜π‘‘))
122121ex 414 . . . . 5 (πœ‘ β†’ (𝑑 ∈ (𝑇 βˆ– π‘ˆ) β†’ 0 < (π‘ƒβ€˜π‘‘)))
1231, 122ralrimi 3239 . . . 4 (πœ‘ β†’ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘ƒβ€˜π‘‘))
12425, 27, 1233jca 1129 . . 3 (πœ‘ β†’ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘ƒβ€˜π‘‘) ∧ (π‘ƒβ€˜π‘‘) ≀ 1) ∧ (π‘ƒβ€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘ƒβ€˜π‘‘)))
125 eleq1 2822 . . . . . 6 (𝑝 = 𝑃 β†’ (𝑝 ∈ 𝐴 ↔ 𝑃 ∈ 𝐴))
126 nfmpt1 5217 . . . . . . . . . 10 Ⅎ𝑑(𝑑 ∈ 𝑇 ↦ ((1 / 𝑀) Β· Σ𝑖 ∈ (1...𝑀)((πΊβ€˜π‘–)β€˜π‘‘)))
1272, 126nfcxfr 2902 . . . . . . . . 9 Ⅎ𝑑𝑃
128127nfeq2 2921 . . . . . . . 8 Ⅎ𝑑 𝑝 = 𝑃
129 fveq1 6845 . . . . . . . . . 10 (𝑝 = 𝑃 β†’ (π‘β€˜π‘‘) = (π‘ƒβ€˜π‘‘))
130129breq2d 5121 . . . . . . . . 9 (𝑝 = 𝑃 β†’ (0 ≀ (π‘β€˜π‘‘) ↔ 0 ≀ (π‘ƒβ€˜π‘‘)))
131129breq1d 5119 . . . . . . . . 9 (𝑝 = 𝑃 β†’ ((π‘β€˜π‘‘) ≀ 1 ↔ (π‘ƒβ€˜π‘‘) ≀ 1))
132130, 131anbi12d 632 . . . . . . . 8 (𝑝 = 𝑃 β†’ ((0 ≀ (π‘β€˜π‘‘) ∧ (π‘β€˜π‘‘) ≀ 1) ↔ (0 ≀ (π‘ƒβ€˜π‘‘) ∧ (π‘ƒβ€˜π‘‘) ≀ 1)))
133128, 132ralbid 3255 . . . . . . 7 (𝑝 = 𝑃 β†’ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘β€˜π‘‘) ∧ (π‘β€˜π‘‘) ≀ 1) ↔ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘ƒβ€˜π‘‘) ∧ (π‘ƒβ€˜π‘‘) ≀ 1)))
134 fveq1 6845 . . . . . . . 8 (𝑝 = 𝑃 β†’ (π‘β€˜π‘) = (π‘ƒβ€˜π‘))
135134eqeq1d 2735 . . . . . . 7 (𝑝 = 𝑃 β†’ ((π‘β€˜π‘) = 0 ↔ (π‘ƒβ€˜π‘) = 0))
136129breq2d 5121 . . . . . . . 8 (𝑝 = 𝑃 β†’ (0 < (π‘β€˜π‘‘) ↔ 0 < (π‘ƒβ€˜π‘‘)))
137128, 136ralbid 3255 . . . . . . 7 (𝑝 = 𝑃 β†’ (βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘β€˜π‘‘) ↔ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘ƒβ€˜π‘‘)))
138133, 135, 1373anbi123d 1437 . . . . . 6 (𝑝 = 𝑃 β†’ ((βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘β€˜π‘‘) ∧ (π‘β€˜π‘‘) ≀ 1) ∧ (π‘β€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘β€˜π‘‘)) ↔ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘ƒβ€˜π‘‘) ∧ (π‘ƒβ€˜π‘‘) ≀ 1) ∧ (π‘ƒβ€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘ƒβ€˜π‘‘))))
139125, 138anbi12d 632 . . . . 5 (𝑝 = 𝑃 β†’ ((𝑝 ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘β€˜π‘‘) ∧ (π‘β€˜π‘‘) ≀ 1) ∧ (π‘β€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘β€˜π‘‘))) ↔ (𝑃 ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘ƒβ€˜π‘‘) ∧ (π‘ƒβ€˜π‘‘) ≀ 1) ∧ (π‘ƒβ€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘ƒβ€˜π‘‘)))))
140139spcegv 3558 . . . 4 (𝑃 ∈ 𝐴 β†’ ((𝑃 ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘ƒβ€˜π‘‘) ∧ (π‘ƒβ€˜π‘‘) ≀ 1) ∧ (π‘ƒβ€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘ƒβ€˜π‘‘))) β†’ βˆƒπ‘(𝑝 ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘β€˜π‘‘) ∧ (π‘β€˜π‘‘) ≀ 1) ∧ (π‘β€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘β€˜π‘‘)))))
14122, 140syl 17 . . 3 (πœ‘ β†’ ((𝑃 ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘ƒβ€˜π‘‘) ∧ (π‘ƒβ€˜π‘‘) ≀ 1) ∧ (π‘ƒβ€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘ƒβ€˜π‘‘))) β†’ βˆƒπ‘(𝑝 ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘β€˜π‘‘) ∧ (π‘β€˜π‘‘) ≀ 1) ∧ (π‘β€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘β€˜π‘‘)))))
14222, 124, 141mp2and 698 . 2 (πœ‘ β†’ βˆƒπ‘(𝑝 ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘β€˜π‘‘) ∧ (π‘β€˜π‘‘) ≀ 1) ∧ (π‘β€˜π‘) = 0 ∧ βˆ€π‘‘ ∈ (𝑇 βˆ– π‘ˆ)0 < (π‘β€˜π‘‘))))
143 df-rex 3071 . 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 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782  β„²wnf 1786   ∈ wcel 2107  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406   βˆ– cdif 3911   βˆͺ cun 3912   ∩ cin 3913   βŠ† wss 3914  βˆ…c0 4286  {csn 4590  βˆͺ cuni 4869   class class class wbr 5109   ↦ cmpt 5192  ran crn 5638  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361  Fincfn 8889  β„‚cc 11057  β„cr 11058  0cc0 11059  1c1 11060   + caddc 11062   Β· cmul 11064   < clt 11197   ≀ cle 11198   / cdiv 11820  β„•cn 12161  (,)cioo 13273  ...cfz 13433  Ξ£csu 15579  topGenctg 17327   Cn ccn 22598
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-sup 9386  df-oi 9454  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-n0 12422  df-z 12508  df-uz 12772  df-rp 12924  df-ioo 13277  df-ico 13279  df-fz 13434  df-fzo 13577  df-seq 13916  df-exp 13977  df-hash 14240  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-clim 15379  df-sum 15580  df-topgen 17333  df-top 22266  df-topon 22283  df-bases 22319  df-cn 22601
This theorem is referenced by:  stoweidlem53  44384
  Copyright terms: Public domain W3C validator