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

Theorem stoweidlem11 44717
Description: This lemma is used to prove that there is a function 𝑔 as in the proof of [BrosowskiDeutsh] p. 92 (at the top of page 92): this lemma proves that g(t) < ( j + 1 / 3 ) * Ξ΅. Here 𝐸 is used to represent Ξ΅ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem11.1 (πœ‘ β†’ 𝑁 ∈ β„•)
stoweidlem11.2 (πœ‘ β†’ 𝑑 ∈ 𝑇)
stoweidlem11.3 (πœ‘ β†’ 𝑗 ∈ (1...𝑁))
stoweidlem11.4 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„)
stoweidlem11.5 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ≀ 1)
stoweidlem11.6 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) < (𝐸 / 𝑁))
stoweidlem11.7 (πœ‘ β†’ 𝐸 ∈ ℝ+)
stoweidlem11.8 (πœ‘ β†’ 𝐸 < (1 / 3))
Assertion
Ref Expression
stoweidlem11 (πœ‘ β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸))
Distinct variable groups:   𝑖,𝑗   𝑑,𝑖,𝐸   𝑖,𝑁,𝑑   πœ‘,𝑖   𝑑,𝑇   𝑑,𝑋
Allowed substitution hints:   πœ‘(𝑑,𝑗)   𝑇(𝑖,𝑗)   𝐸(𝑗)   𝑁(𝑗)   𝑋(𝑖,𝑗)

Proof of Theorem stoweidlem11
StepHypRef Expression
1 stoweidlem11.2 . . 3 (πœ‘ β†’ 𝑑 ∈ 𝑇)
2 sumex 15633 . . 3 Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ V
3 eqid 2732 . . . 4 (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
43fvmpt2 7009 . . 3 ((𝑑 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ V) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) = Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
51, 2, 4sylancl 586 . 2 (πœ‘ β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) = Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
6 fzfid 13937 . . . 4 (πœ‘ β†’ (0...𝑁) ∈ Fin)
7 stoweidlem11.7 . . . . . . 7 (πœ‘ β†’ 𝐸 ∈ ℝ+)
87rpred 13015 . . . . . 6 (πœ‘ β†’ 𝐸 ∈ ℝ)
98adantr 481 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 𝐸 ∈ ℝ)
10 stoweidlem11.4 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„)
111adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 𝑑 ∈ 𝑇)
1210, 11ffvelcdmd 7087 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
139, 12remulcld 11243 . . . 4 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
146, 13fsumrecl 15679 . . 3 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
15 stoweidlem11.3 . . . . . . 7 (πœ‘ β†’ 𝑗 ∈ (1...𝑁))
1615elfzelzd 13501 . . . . . 6 (πœ‘ β†’ 𝑗 ∈ β„€)
1716zred 12665 . . . . 5 (πœ‘ β†’ 𝑗 ∈ ℝ)
188, 17remulcld 11243 . . . 4 (πœ‘ β†’ (𝐸 Β· 𝑗) ∈ ℝ)
19 stoweidlem11.1 . . . . . . . 8 (πœ‘ β†’ 𝑁 ∈ β„•)
2019nnred 12226 . . . . . . 7 (πœ‘ β†’ 𝑁 ∈ ℝ)
2120, 17resubcld 11641 . . . . . 6 (πœ‘ β†’ (𝑁 βˆ’ 𝑗) ∈ ℝ)
22 1red 11214 . . . . . 6 (πœ‘ β†’ 1 ∈ ℝ)
2321, 22readdcld 11242 . . . . 5 (πœ‘ β†’ ((𝑁 βˆ’ 𝑗) + 1) ∈ ℝ)
248, 19nndivred 12265 . . . . . 6 (πœ‘ β†’ (𝐸 / 𝑁) ∈ ℝ)
258, 24remulcld 11243 . . . . 5 (πœ‘ β†’ (𝐸 Β· (𝐸 / 𝑁)) ∈ ℝ)
2623, 25remulcld 11243 . . . 4 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁))) ∈ ℝ)
2718, 26readdcld 11242 . . 3 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))) ∈ ℝ)
28 3re 12291 . . . . . . 7 3 ∈ ℝ
2928a1i 11 . . . . . 6 (πœ‘ β†’ 3 ∈ ℝ)
30 3ne0 12317 . . . . . . 7 3 β‰  0
3130a1i 11 . . . . . 6 (πœ‘ β†’ 3 β‰  0)
3229, 31rereccld 12040 . . . . 5 (πœ‘ β†’ (1 / 3) ∈ ℝ)
3317, 32readdcld 11242 . . . 4 (πœ‘ β†’ (𝑗 + (1 / 3)) ∈ ℝ)
3433, 8remulcld 11243 . . 3 (πœ‘ β†’ ((𝑗 + (1 / 3)) Β· 𝐸) ∈ ℝ)
35 fzfid 13937 . . . . . 6 (πœ‘ β†’ (0...(𝑗 βˆ’ 1)) ∈ Fin)
368adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ 𝐸 ∈ ℝ)
37 elfzelz 13500 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑁) β†’ 𝑗 ∈ β„€)
38 peano2zm 12604 . . . . . . . . . . . 12 (𝑗 ∈ β„€ β†’ (𝑗 βˆ’ 1) ∈ β„€)
3915, 37, 383syl 18 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ β„€)
4019nnzd 12584 . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ β„€)
4117, 22resubcld 11641 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ ℝ)
4217lem1d 12146 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑗 βˆ’ 1) ≀ 𝑗)
43 elfzuz3 13497 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑁) β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘—))
44 eluzle 12834 . . . . . . . . . . . . 13 (𝑁 ∈ (β„€β‰₯β€˜π‘—) β†’ 𝑗 ≀ 𝑁)
4515, 43, 443syl 18 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑗 ≀ 𝑁)
4641, 17, 20, 42, 45letrd 11370 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗 βˆ’ 1) ≀ 𝑁)
47 eluz2 12827 . . . . . . . . . . 11 (𝑁 ∈ (β„€β‰₯β€˜(𝑗 βˆ’ 1)) ↔ ((𝑗 βˆ’ 1) ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ (𝑗 βˆ’ 1) ≀ 𝑁))
4839, 40, 46, 47syl3anbrc 1343 . . . . . . . . . 10 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜(𝑗 βˆ’ 1)))
49 fzss2 13540 . . . . . . . . . 10 (𝑁 ∈ (β„€β‰₯β€˜(𝑗 βˆ’ 1)) β†’ (0...(𝑗 βˆ’ 1)) βŠ† (0...𝑁))
5048, 49syl 17 . . . . . . . . 9 (πœ‘ β†’ (0...(𝑗 βˆ’ 1)) βŠ† (0...𝑁))
5150sselda 3982 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ 𝑖 ∈ (0...𝑁))
5251, 12syldan 591 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
5336, 52remulcld 11243 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
5435, 53fsumrecl 15679 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
5554, 26readdcld 11242 . . . 4 (πœ‘ β†’ (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))) ∈ ℝ)
5617ltm1d 12145 . . . . . . 7 (πœ‘ β†’ (𝑗 βˆ’ 1) < 𝑗)
57 fzdisj 13527 . . . . . . 7 ((𝑗 βˆ’ 1) < 𝑗 β†’ ((0...(𝑗 βˆ’ 1)) ∩ (𝑗...𝑁)) = βˆ…)
5856, 57syl 17 . . . . . 6 (πœ‘ β†’ ((0...(𝑗 βˆ’ 1)) ∩ (𝑗...𝑁)) = βˆ…)
59 fzssp1 13543 . . . . . . . . . 10 (0...(𝑁 βˆ’ 1)) βŠ† (0...((𝑁 βˆ’ 1) + 1))
6019nncnd 12227 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„‚)
61 1cnd 11208 . . . . . . . . . . . 12 (πœ‘ β†’ 1 ∈ β„‚)
6260, 61npcand 11574 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑁 βˆ’ 1) + 1) = 𝑁)
6362oveq2d 7424 . . . . . . . . . 10 (πœ‘ β†’ (0...((𝑁 βˆ’ 1) + 1)) = (0...𝑁))
6459, 63sseqtrid 4034 . . . . . . . . 9 (πœ‘ β†’ (0...(𝑁 βˆ’ 1)) βŠ† (0...𝑁))
65 1zzd 12592 . . . . . . . . . . . 12 (πœ‘ β†’ 1 ∈ β„€)
66 fzsubel 13536 . . . . . . . . . . . 12 (((1 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ (𝑗 ∈ β„€ ∧ 1 ∈ β„€)) β†’ (𝑗 ∈ (1...𝑁) ↔ (𝑗 βˆ’ 1) ∈ ((1 βˆ’ 1)...(𝑁 βˆ’ 1))))
6765, 40, 16, 65, 66syl22anc 837 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗 ∈ (1...𝑁) ↔ (𝑗 βˆ’ 1) ∈ ((1 βˆ’ 1)...(𝑁 βˆ’ 1))))
6815, 67mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ ((1 βˆ’ 1)...(𝑁 βˆ’ 1)))
69 1m1e0 12283 . . . . . . . . . . 11 (1 βˆ’ 1) = 0
7069oveq1i 7418 . . . . . . . . . 10 ((1 βˆ’ 1)...(𝑁 βˆ’ 1)) = (0...(𝑁 βˆ’ 1))
7168, 70eleqtrdi 2843 . . . . . . . . 9 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1)))
7264, 71sseldd 3983 . . . . . . . 8 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ (0...𝑁))
73 fzsplit 13526 . . . . . . . 8 ((𝑗 βˆ’ 1) ∈ (0...𝑁) β†’ (0...𝑁) = ((0...(𝑗 βˆ’ 1)) βˆͺ (((𝑗 βˆ’ 1) + 1)...𝑁)))
7472, 73syl 17 . . . . . . 7 (πœ‘ β†’ (0...𝑁) = ((0...(𝑗 βˆ’ 1)) βˆͺ (((𝑗 βˆ’ 1) + 1)...𝑁)))
7516zcnd 12666 . . . . . . . . . 10 (πœ‘ β†’ 𝑗 ∈ β„‚)
7675, 61npcand 11574 . . . . . . . . 9 (πœ‘ β†’ ((𝑗 βˆ’ 1) + 1) = 𝑗)
7776oveq1d 7423 . . . . . . . 8 (πœ‘ β†’ (((𝑗 βˆ’ 1) + 1)...𝑁) = (𝑗...𝑁))
7877uneq2d 4163 . . . . . . 7 (πœ‘ β†’ ((0...(𝑗 βˆ’ 1)) βˆͺ (((𝑗 βˆ’ 1) + 1)...𝑁)) = ((0...(𝑗 βˆ’ 1)) βˆͺ (𝑗...𝑁)))
7974, 78eqtrd 2772 . . . . . 6 (πœ‘ β†’ (0...𝑁) = ((0...(𝑗 βˆ’ 1)) βˆͺ (𝑗...𝑁)))
807rpcnd 13017 . . . . . . . 8 (πœ‘ β†’ 𝐸 ∈ β„‚)
8180adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 𝐸 ∈ β„‚)
8212recnd 11241 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ β„‚)
8381, 82mulcld 11233 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ β„‚)
8458, 79, 6, 83fsumsplit 15686 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))))
85 fzfid 13937 . . . . . . 7 (πœ‘ β†’ (𝑗...𝑁) ∈ Fin)
868adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ 𝐸 ∈ ℝ)
87 0zd 12569 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ∈ β„€)
88 0red 11216 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 ∈ ℝ)
89 0le1 11736 . . . . . . . . . . . . . . 15 0 ≀ 1
9089a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 ≀ 1)
91 elfzuz 13496 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑁) β†’ 𝑗 ∈ (β„€β‰₯β€˜1))
9215, 91syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑗 ∈ (β„€β‰₯β€˜1))
93 eluz2 12827 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (β„€β‰₯β€˜1) ↔ (1 ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 1 ≀ 𝑗))
9492, 93sylib 217 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1 ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 1 ≀ 𝑗))
9594simp3d 1144 . . . . . . . . . . . . . 14 (πœ‘ β†’ 1 ≀ 𝑗)
9688, 22, 17, 90, 95letrd 11370 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ≀ 𝑗)
97 eluz2 12827 . . . . . . . . . . . . 13 (𝑗 ∈ (β„€β‰₯β€˜0) ↔ (0 ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 0 ≀ 𝑗))
9887, 16, 96, 97syl3anbrc 1343 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑗 ∈ (β„€β‰₯β€˜0))
99 fzss1 13539 . . . . . . . . . . . 12 (𝑗 ∈ (β„€β‰₯β€˜0) β†’ (𝑗...𝑁) βŠ† (0...𝑁))
10098, 99syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗...𝑁) βŠ† (0...𝑁))
101100sselda 3982 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ 𝑖 ∈ (0...𝑁))
102101, 10syldan 591 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„)
1031adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ 𝑑 ∈ 𝑇)
104102, 103ffvelcdmd 7087 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
10586, 104remulcld 11243 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
10685, 105fsumrecl 15679 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
107 eluzfz2 13508 . . . . . . . . 9 (𝑁 ∈ (β„€β‰₯β€˜π‘—) β†’ 𝑁 ∈ (𝑗...𝑁))
108 ne0i 4334 . . . . . . . . 9 (𝑁 ∈ (𝑗...𝑁) β†’ (𝑗...𝑁) β‰  βˆ…)
10915, 43, 107, 1084syl 19 . . . . . . . 8 (πœ‘ β†’ (𝑗...𝑁) β‰  βˆ…)
11019adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ 𝑁 ∈ β„•)
11186, 110nndivred 12265 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (𝐸 / 𝑁) ∈ ℝ)
11286, 111remulcld 11243 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (𝐸 Β· (𝐸 / 𝑁)) ∈ ℝ)
113 stoweidlem11.6 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) < (𝐸 / 𝑁))
1147rpgt0d 13018 . . . . . . . . . . 11 (πœ‘ β†’ 0 < 𝐸)
115114adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ 0 < 𝐸)
116 ltmul2 12064 . . . . . . . . . 10 ((((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ ∧ (𝐸 / 𝑁) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ (((π‘‹β€˜π‘–)β€˜π‘‘) < (𝐸 / 𝑁) ↔ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < (𝐸 Β· (𝐸 / 𝑁))))
117104, 111, 86, 115, 116syl112anc 1374 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (((π‘‹β€˜π‘–)β€˜π‘‘) < (𝐸 / 𝑁) ↔ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < (𝐸 Β· (𝐸 / 𝑁))))
118113, 117mpbid 231 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < (𝐸 Β· (𝐸 / 𝑁)))
11985, 109, 105, 112, 118fsumlt 15745 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· (𝐸 / 𝑁)))
12019nnne0d 12261 . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 β‰  0)
12180, 60, 120divcld 11989 . . . . . . . . . 10 (πœ‘ β†’ (𝐸 / 𝑁) ∈ β„‚)
12280, 121mulcld 11233 . . . . . . . . 9 (πœ‘ β†’ (𝐸 Β· (𝐸 / 𝑁)) ∈ β„‚)
123 fsumconst 15735 . . . . . . . . 9 (((𝑗...𝑁) ∈ Fin ∧ (𝐸 Β· (𝐸 / 𝑁)) ∈ β„‚) β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· (𝐸 / 𝑁)) = ((β™―β€˜(𝑗...𝑁)) Β· (𝐸 Β· (𝐸 / 𝑁))))
12485, 122, 123syl2anc 584 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· (𝐸 / 𝑁)) = ((β™―β€˜(𝑗...𝑁)) Β· (𝐸 Β· (𝐸 / 𝑁))))
125 hashfz 14386 . . . . . . . . . 10 (𝑁 ∈ (β„€β‰₯β€˜π‘—) β†’ (β™―β€˜(𝑗...𝑁)) = ((𝑁 βˆ’ 𝑗) + 1))
12615, 43, 1253syl 18 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(𝑗...𝑁)) = ((𝑁 βˆ’ 𝑗) + 1))
127126oveq1d 7423 . . . . . . . 8 (πœ‘ β†’ ((β™―β€˜(𝑗...𝑁)) Β· (𝐸 Β· (𝐸 / 𝑁))) = (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁))))
128124, 127eqtrd 2772 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· (𝐸 / 𝑁)) = (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁))))
129119, 128breqtrd 5174 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁))))
130106, 26, 54, 129ltadd2dd 11372 . . . . 5 (πœ‘ β†’ (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) < (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))))
13184, 130eqbrtrd 5170 . . . 4 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))))
132 stoweidlem11.5 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ≀ 1)
13351, 132syldan 591 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ≀ 1)
134 1red 11214 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ 1 ∈ ℝ)
135114adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ 0 < 𝐸)
136 lemul2 12066 . . . . . . . . . 10 ((((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ (((π‘‹β€˜π‘–)β€˜π‘‘) ≀ 1 ↔ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ (𝐸 Β· 1)))
13752, 134, 36, 135, 136syl112anc 1374 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ (((π‘‹β€˜π‘–)β€˜π‘‘) ≀ 1 ↔ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ (𝐸 Β· 1)))
138133, 137mpbid 231 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ (𝐸 Β· 1))
13980mulridd 11230 . . . . . . . . 9 (πœ‘ β†’ (𝐸 Β· 1) = 𝐸)
140139adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ (𝐸 Β· 1) = 𝐸)
141138, 140breqtrd 5174 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ 𝐸)
14235, 53, 36, 141fsumle 15744 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))𝐸)
143 fsumconst 15735 . . . . . . . 8 (((0...(𝑗 βˆ’ 1)) ∈ Fin ∧ 𝐸 ∈ β„‚) β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))𝐸 = ((β™―β€˜(0...(𝑗 βˆ’ 1))) Β· 𝐸))
14435, 80, 143syl2anc 584 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))𝐸 = ((β™―β€˜(0...(𝑗 βˆ’ 1))) Β· 𝐸))
145 0z 12568 . . . . . . . . . . 11 0 ∈ β„€
146 1e0p1 12718 . . . . . . . . . . . . 13 1 = (0 + 1)
147146fveq2i 6894 . . . . . . . . . . . 12 (β„€β‰₯β€˜1) = (β„€β‰₯β€˜(0 + 1))
14892, 147eleqtrdi 2843 . . . . . . . . . . 11 (πœ‘ β†’ 𝑗 ∈ (β„€β‰₯β€˜(0 + 1)))
149 eluzp1m1 12847 . . . . . . . . . . 11 ((0 ∈ β„€ ∧ 𝑗 ∈ (β„€β‰₯β€˜(0 + 1))) β†’ (𝑗 βˆ’ 1) ∈ (β„€β‰₯β€˜0))
150145, 148, 149sylancr 587 . . . . . . . . . 10 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ (β„€β‰₯β€˜0))
151 hashfz 14386 . . . . . . . . . 10 ((𝑗 βˆ’ 1) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜(0...(𝑗 βˆ’ 1))) = (((𝑗 βˆ’ 1) βˆ’ 0) + 1))
152150, 151syl 17 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(0...(𝑗 βˆ’ 1))) = (((𝑗 βˆ’ 1) βˆ’ 0) + 1))
15375, 61subcld 11570 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ β„‚)
154153subid1d 11559 . . . . . . . . . 10 (πœ‘ β†’ ((𝑗 βˆ’ 1) βˆ’ 0) = (𝑗 βˆ’ 1))
155154oveq1d 7423 . . . . . . . . 9 (πœ‘ β†’ (((𝑗 βˆ’ 1) βˆ’ 0) + 1) = ((𝑗 βˆ’ 1) + 1))
156152, 155, 763eqtrd 2776 . . . . . . . 8 (πœ‘ β†’ (β™―β€˜(0...(𝑗 βˆ’ 1))) = 𝑗)
157156oveq1d 7423 . . . . . . 7 (πœ‘ β†’ ((β™―β€˜(0...(𝑗 βˆ’ 1))) Β· 𝐸) = (𝑗 Β· 𝐸))
15875, 80mulcomd 11234 . . . . . . 7 (πœ‘ β†’ (𝑗 Β· 𝐸) = (𝐸 Β· 𝑗))
159144, 157, 1583eqtrd 2776 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))𝐸 = (𝐸 Β· 𝑗))
160142, 159breqtrd 5174 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ (𝐸 Β· 𝑗))
16154, 18, 26, 160leadd1dd 11827 . . . 4 (πœ‘ β†’ (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))) ≀ ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))))
16214, 55, 27, 131, 161ltletrd 11373 . . 3 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))))
1638, 8remulcld 11243 . . . . 5 (πœ‘ β†’ (𝐸 Β· 𝐸) ∈ ℝ)
16418, 163readdcld 11242 . . . 4 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)) ∈ ℝ)
16560, 75subcld 11570 . . . . . . . 8 (πœ‘ β†’ (𝑁 βˆ’ 𝑗) ∈ β„‚)
166165, 61addcld 11232 . . . . . . 7 (πœ‘ β†’ ((𝑁 βˆ’ 𝑗) + 1) ∈ β„‚)
16780, 166, 121mul12d 11422 . . . . . 6 (πœ‘ β†’ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁))) = (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁))))
168167oveq2d 7424 . . . . 5 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)))) = ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))))
16923, 24remulcld 11243 . . . . . . 7 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)) ∈ ℝ)
1708, 169remulcld 11243 . . . . . 6 (πœ‘ β†’ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁))) ∈ ℝ)
171166, 80, 60, 120div12d 12025 . . . . . . . 8 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)) = (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) / 𝑁)))
17222, 17resubcld 11641 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 βˆ’ 𝑗) ∈ ℝ)
173 elfzle1 13503 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑁) β†’ 1 ≀ 𝑗)
17415, 173syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 1 ≀ 𝑗)
17522, 17suble0d 11804 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((1 βˆ’ 𝑗) ≀ 0 ↔ 1 ≀ 𝑗))
176174, 175mpbird 256 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 βˆ’ 𝑗) ≀ 0)
177172, 88, 20, 176leadd2dd 11828 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑁 + (1 βˆ’ 𝑗)) ≀ (𝑁 + 0))
17860, 61, 75addsub12d 11593 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑁 + (1 βˆ’ 𝑗)) = (1 + (𝑁 βˆ’ 𝑗)))
17961, 165addcomd 11415 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 + (𝑁 βˆ’ 𝑗)) = ((𝑁 βˆ’ 𝑗) + 1))
180178, 179eqtrd 2772 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑁 + (1 βˆ’ 𝑗)) = ((𝑁 βˆ’ 𝑗) + 1))
18160addridd 11413 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑁 + 0) = 𝑁)
182177, 180, 1813brtr3d 5179 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑁 βˆ’ 𝑗) + 1) ≀ 𝑁)
18319nngt0d 12260 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < 𝑁)
184 lediv1 12078 . . . . . . . . . . . . 13 ((((𝑁 βˆ’ 𝑗) + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ (((𝑁 βˆ’ 𝑗) + 1) ≀ 𝑁 ↔ (((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ≀ (𝑁 / 𝑁)))
18523, 20, 20, 183, 184syl112anc 1374 . . . . . . . . . . . 12 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) ≀ 𝑁 ↔ (((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ≀ (𝑁 / 𝑁)))
186182, 185mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ≀ (𝑁 / 𝑁))
18760, 120dividd 11987 . . . . . . . . . . 11 (πœ‘ β†’ (𝑁 / 𝑁) = 1)
188186, 187breqtrd 5174 . . . . . . . . . 10 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ≀ 1)
18923, 19nndivred 12265 . . . . . . . . . . 11 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ∈ ℝ)
190189, 22, 7lemul2d 13059 . . . . . . . . . 10 (πœ‘ β†’ ((((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ≀ 1 ↔ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) / 𝑁)) ≀ (𝐸 Β· 1)))
191188, 190mpbid 231 . . . . . . . . 9 (πœ‘ β†’ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) / 𝑁)) ≀ (𝐸 Β· 1))
192191, 139breqtrd 5174 . . . . . . . 8 (πœ‘ β†’ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) / 𝑁)) ≀ 𝐸)
193171, 192eqbrtrd 5170 . . . . . . 7 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)) ≀ 𝐸)
194169, 8, 7lemul2d 13059 . . . . . . 7 (πœ‘ β†’ ((((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)) ≀ 𝐸 ↔ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁))) ≀ (𝐸 Β· 𝐸)))
195193, 194mpbid 231 . . . . . 6 (πœ‘ β†’ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁))) ≀ (𝐸 Β· 𝐸))
196170, 163, 18, 195leadd2dd 11828 . . . . 5 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)))) ≀ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)))
197168, 196eqbrtrrd 5172 . . . 4 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))) ≀ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)))
19880, 75mulcomd 11234 . . . . . . 7 (πœ‘ β†’ (𝐸 Β· 𝑗) = (𝑗 Β· 𝐸))
199198oveq1d 7423 . . . . . 6 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)) = ((𝑗 Β· 𝐸) + (𝐸 Β· 𝐸)))
20075, 80, 80adddird 11238 . . . . . 6 (πœ‘ β†’ ((𝑗 + 𝐸) Β· 𝐸) = ((𝑗 Β· 𝐸) + (𝐸 Β· 𝐸)))
201199, 200eqtr4d 2775 . . . . 5 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)) = ((𝑗 + 𝐸) Β· 𝐸))
20217, 8readdcld 11242 . . . . . 6 (πœ‘ β†’ (𝑗 + 𝐸) ∈ ℝ)
203 stoweidlem11.8 . . . . . . 7 (πœ‘ β†’ 𝐸 < (1 / 3))
2048, 32, 17, 203ltadd2dd 11372 . . . . . 6 (πœ‘ β†’ (𝑗 + 𝐸) < (𝑗 + (1 / 3)))
205202, 33, 7, 204ltmul1dd 13070 . . . . 5 (πœ‘ β†’ ((𝑗 + 𝐸) Β· 𝐸) < ((𝑗 + (1 / 3)) Β· 𝐸))
206201, 205eqbrtrd 5170 . . . 4 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)) < ((𝑗 + (1 / 3)) Β· 𝐸))
20727, 164, 34, 197, 206lelttrd 11371 . . 3 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))) < ((𝑗 + (1 / 3)) Β· 𝐸))
20814, 27, 34, 162, 207lttrd 11374 . 2 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < ((𝑗 + (1 / 3)) Β· 𝐸))
2095, 208eqbrtrd 5170 1 (πœ‘ β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  Vcvv 3474   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322   class class class wbr 5148   ↦ cmpt 5231  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7408  Fincfn 8938  β„‚cc 11107  β„cr 11108  0cc0 11109  1c1 11110   + caddc 11112   Β· cmul 11114   < clt 11247   ≀ cle 11248   βˆ’ cmin 11443   / cdiv 11870  β„•cn 12211  3c3 12267  β„€cz 12557  β„€β‰₯cuz 12821  β„+crp 12973  ...cfz 13483  β™―chash 14289  Ξ£csu 15631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-inf2 9635  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-sup 9436  df-oi 9504  df-card 9933  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-3 12275  df-n0 12472  df-z 12558  df-uz 12822  df-rp 12974  df-ico 13329  df-fz 13484  df-fzo 13627  df-seq 13966  df-exp 14027  df-hash 14290  df-cj 15045  df-re 15046  df-im 15047  df-sqrt 15181  df-abs 15182  df-clim 15431  df-sum 15632
This theorem is referenced by:  stoweidlem34  44740
  Copyright terms: Public domain W3C validator