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 44342
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 15581 . . 3 Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ V
3 eqid 2733 . . . 4 (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
43fvmpt2 6963 . . 3 ((𝑑 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ V) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) = Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
51, 2, 4sylancl 587 . 2 (πœ‘ β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) = Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
6 fzfid 13887 . . . 4 (πœ‘ β†’ (0...𝑁) ∈ Fin)
7 stoweidlem11.7 . . . . . . 7 (πœ‘ β†’ 𝐸 ∈ ℝ+)
87rpred 12965 . . . . . 6 (πœ‘ β†’ 𝐸 ∈ ℝ)
98adantr 482 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 𝐸 ∈ ℝ)
10 stoweidlem11.4 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„)
111adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 𝑑 ∈ 𝑇)
1210, 11ffvelcdmd 7040 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
139, 12remulcld 11193 . . . 4 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
146, 13fsumrecl 15627 . . 3 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
15 stoweidlem11.3 . . . . . . 7 (πœ‘ β†’ 𝑗 ∈ (1...𝑁))
1615elfzelzd 13451 . . . . . 6 (πœ‘ β†’ 𝑗 ∈ β„€)
1716zred 12615 . . . . 5 (πœ‘ β†’ 𝑗 ∈ ℝ)
188, 17remulcld 11193 . . . 4 (πœ‘ β†’ (𝐸 Β· 𝑗) ∈ ℝ)
19 stoweidlem11.1 . . . . . . . 8 (πœ‘ β†’ 𝑁 ∈ β„•)
2019nnred 12176 . . . . . . 7 (πœ‘ β†’ 𝑁 ∈ ℝ)
2120, 17resubcld 11591 . . . . . 6 (πœ‘ β†’ (𝑁 βˆ’ 𝑗) ∈ ℝ)
22 1red 11164 . . . . . 6 (πœ‘ β†’ 1 ∈ ℝ)
2321, 22readdcld 11192 . . . . 5 (πœ‘ β†’ ((𝑁 βˆ’ 𝑗) + 1) ∈ ℝ)
248, 19nndivred 12215 . . . . . 6 (πœ‘ β†’ (𝐸 / 𝑁) ∈ ℝ)
258, 24remulcld 11193 . . . . 5 (πœ‘ β†’ (𝐸 Β· (𝐸 / 𝑁)) ∈ ℝ)
2623, 25remulcld 11193 . . . 4 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁))) ∈ ℝ)
2718, 26readdcld 11192 . . 3 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))) ∈ ℝ)
28 3re 12241 . . . . . . 7 3 ∈ ℝ
2928a1i 11 . . . . . 6 (πœ‘ β†’ 3 ∈ ℝ)
30 3ne0 12267 . . . . . . 7 3 β‰  0
3130a1i 11 . . . . . 6 (πœ‘ β†’ 3 β‰  0)
3229, 31rereccld 11990 . . . . 5 (πœ‘ β†’ (1 / 3) ∈ ℝ)
3317, 32readdcld 11192 . . . 4 (πœ‘ β†’ (𝑗 + (1 / 3)) ∈ ℝ)
3433, 8remulcld 11193 . . 3 (πœ‘ β†’ ((𝑗 + (1 / 3)) Β· 𝐸) ∈ ℝ)
35 fzfid 13887 . . . . . 6 (πœ‘ β†’ (0...(𝑗 βˆ’ 1)) ∈ Fin)
368adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ 𝐸 ∈ ℝ)
37 elfzelz 13450 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑁) β†’ 𝑗 ∈ β„€)
38 peano2zm 12554 . . . . . . . . . . . 12 (𝑗 ∈ β„€ β†’ (𝑗 βˆ’ 1) ∈ β„€)
3915, 37, 383syl 18 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ β„€)
4019nnzd 12534 . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ β„€)
4117, 22resubcld 11591 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ ℝ)
4217lem1d 12096 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑗 βˆ’ 1) ≀ 𝑗)
43 elfzuz3 13447 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑁) β†’ 𝑁 ∈ (β„€β‰₯β€˜π‘—))
44 eluzle 12784 . . . . . . . . . . . . 13 (𝑁 ∈ (β„€β‰₯β€˜π‘—) β†’ 𝑗 ≀ 𝑁)
4515, 43, 443syl 18 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑗 ≀ 𝑁)
4641, 17, 20, 42, 45letrd 11320 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗 βˆ’ 1) ≀ 𝑁)
47 eluz2 12777 . . . . . . . . . . 11 (𝑁 ∈ (β„€β‰₯β€˜(𝑗 βˆ’ 1)) ↔ ((𝑗 βˆ’ 1) ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ (𝑗 βˆ’ 1) ≀ 𝑁))
4839, 40, 46, 47syl3anbrc 1344 . . . . . . . . . 10 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜(𝑗 βˆ’ 1)))
49 fzss2 13490 . . . . . . . . . 10 (𝑁 ∈ (β„€β‰₯β€˜(𝑗 βˆ’ 1)) β†’ (0...(𝑗 βˆ’ 1)) βŠ† (0...𝑁))
5048, 49syl 17 . . . . . . . . 9 (πœ‘ β†’ (0...(𝑗 βˆ’ 1)) βŠ† (0...𝑁))
5150sselda 3948 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ 𝑖 ∈ (0...𝑁))
5251, 12syldan 592 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
5336, 52remulcld 11193 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
5435, 53fsumrecl 15627 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
5554, 26readdcld 11192 . . . 4 (πœ‘ β†’ (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))) ∈ ℝ)
5617ltm1d 12095 . . . . . . 7 (πœ‘ β†’ (𝑗 βˆ’ 1) < 𝑗)
57 fzdisj 13477 . . . . . . 7 ((𝑗 βˆ’ 1) < 𝑗 β†’ ((0...(𝑗 βˆ’ 1)) ∩ (𝑗...𝑁)) = βˆ…)
5856, 57syl 17 . . . . . 6 (πœ‘ β†’ ((0...(𝑗 βˆ’ 1)) ∩ (𝑗...𝑁)) = βˆ…)
59 fzssp1 13493 . . . . . . . . . 10 (0...(𝑁 βˆ’ 1)) βŠ† (0...((𝑁 βˆ’ 1) + 1))
6019nncnd 12177 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„‚)
61 1cnd 11158 . . . . . . . . . . . 12 (πœ‘ β†’ 1 ∈ β„‚)
6260, 61npcand 11524 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑁 βˆ’ 1) + 1) = 𝑁)
6362oveq2d 7377 . . . . . . . . . 10 (πœ‘ β†’ (0...((𝑁 βˆ’ 1) + 1)) = (0...𝑁))
6459, 63sseqtrid 4000 . . . . . . . . 9 (πœ‘ β†’ (0...(𝑁 βˆ’ 1)) βŠ† (0...𝑁))
65 1zzd 12542 . . . . . . . . . . . 12 (πœ‘ β†’ 1 ∈ β„€)
66 fzsubel 13486 . . . . . . . . . . . 12 (((1 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ (𝑗 ∈ β„€ ∧ 1 ∈ β„€)) β†’ (𝑗 ∈ (1...𝑁) ↔ (𝑗 βˆ’ 1) ∈ ((1 βˆ’ 1)...(𝑁 βˆ’ 1))))
6765, 40, 16, 65, 66syl22anc 838 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗 ∈ (1...𝑁) ↔ (𝑗 βˆ’ 1) ∈ ((1 βˆ’ 1)...(𝑁 βˆ’ 1))))
6815, 67mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ ((1 βˆ’ 1)...(𝑁 βˆ’ 1)))
69 1m1e0 12233 . . . . . . . . . . 11 (1 βˆ’ 1) = 0
7069oveq1i 7371 . . . . . . . . . 10 ((1 βˆ’ 1)...(𝑁 βˆ’ 1)) = (0...(𝑁 βˆ’ 1))
7168, 70eleqtrdi 2844 . . . . . . . . 9 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1)))
7264, 71sseldd 3949 . . . . . . . 8 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ (0...𝑁))
73 fzsplit 13476 . . . . . . . 8 ((𝑗 βˆ’ 1) ∈ (0...𝑁) β†’ (0...𝑁) = ((0...(𝑗 βˆ’ 1)) βˆͺ (((𝑗 βˆ’ 1) + 1)...𝑁)))
7472, 73syl 17 . . . . . . 7 (πœ‘ β†’ (0...𝑁) = ((0...(𝑗 βˆ’ 1)) βˆͺ (((𝑗 βˆ’ 1) + 1)...𝑁)))
7516zcnd 12616 . . . . . . . . . 10 (πœ‘ β†’ 𝑗 ∈ β„‚)
7675, 61npcand 11524 . . . . . . . . 9 (πœ‘ β†’ ((𝑗 βˆ’ 1) + 1) = 𝑗)
7776oveq1d 7376 . . . . . . . 8 (πœ‘ β†’ (((𝑗 βˆ’ 1) + 1)...𝑁) = (𝑗...𝑁))
7877uneq2d 4127 . . . . . . 7 (πœ‘ β†’ ((0...(𝑗 βˆ’ 1)) βˆͺ (((𝑗 βˆ’ 1) + 1)...𝑁)) = ((0...(𝑗 βˆ’ 1)) βˆͺ (𝑗...𝑁)))
7974, 78eqtrd 2773 . . . . . 6 (πœ‘ β†’ (0...𝑁) = ((0...(𝑗 βˆ’ 1)) βˆͺ (𝑗...𝑁)))
807rpcnd 12967 . . . . . . . 8 (πœ‘ β†’ 𝐸 ∈ β„‚)
8180adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 𝐸 ∈ β„‚)
8212recnd 11191 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ β„‚)
8381, 82mulcld 11183 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ β„‚)
8458, 79, 6, 83fsumsplit 15634 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))))
85 fzfid 13887 . . . . . . 7 (πœ‘ β†’ (𝑗...𝑁) ∈ Fin)
868adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ 𝐸 ∈ ℝ)
87 0zd 12519 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ∈ β„€)
88 0red 11166 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 ∈ ℝ)
89 0le1 11686 . . . . . . . . . . . . . . 15 0 ≀ 1
9089a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 ≀ 1)
91 elfzuz 13446 . . . . . . . . . . . . . . . . 17 (𝑗 ∈ (1...𝑁) β†’ 𝑗 ∈ (β„€β‰₯β€˜1))
9215, 91syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑗 ∈ (β„€β‰₯β€˜1))
93 eluz2 12777 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (β„€β‰₯β€˜1) ↔ (1 ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 1 ≀ 𝑗))
9492, 93sylib 217 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1 ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 1 ≀ 𝑗))
9594simp3d 1145 . . . . . . . . . . . . . 14 (πœ‘ β†’ 1 ≀ 𝑗)
9688, 22, 17, 90, 95letrd 11320 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 ≀ 𝑗)
97 eluz2 12777 . . . . . . . . . . . . 13 (𝑗 ∈ (β„€β‰₯β€˜0) ↔ (0 ∈ β„€ ∧ 𝑗 ∈ β„€ ∧ 0 ≀ 𝑗))
9887, 16, 96, 97syl3anbrc 1344 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑗 ∈ (β„€β‰₯β€˜0))
99 fzss1 13489 . . . . . . . . . . . 12 (𝑗 ∈ (β„€β‰₯β€˜0) β†’ (𝑗...𝑁) βŠ† (0...𝑁))
10098, 99syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗...𝑁) βŠ† (0...𝑁))
101100sselda 3948 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ 𝑖 ∈ (0...𝑁))
102101, 10syldan 592 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„)
1031adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ 𝑑 ∈ 𝑇)
104102, 103ffvelcdmd 7040 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ)
10586, 104remulcld 11193 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
10685, 105fsumrecl 15627 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ∈ ℝ)
107 eluzfz2 13458 . . . . . . . . 9 (𝑁 ∈ (β„€β‰₯β€˜π‘—) β†’ 𝑁 ∈ (𝑗...𝑁))
108 ne0i 4298 . . . . . . . . 9 (𝑁 ∈ (𝑗...𝑁) β†’ (𝑗...𝑁) β‰  βˆ…)
10915, 43, 107, 1084syl 19 . . . . . . . 8 (πœ‘ β†’ (𝑗...𝑁) β‰  βˆ…)
11019adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ 𝑁 ∈ β„•)
11186, 110nndivred 12215 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (𝐸 / 𝑁) ∈ ℝ)
11286, 111remulcld 11193 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (𝐸 Β· (𝐸 / 𝑁)) ∈ ℝ)
113 stoweidlem11.6 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) < (𝐸 / 𝑁))
1147rpgt0d 12968 . . . . . . . . . . 11 (πœ‘ β†’ 0 < 𝐸)
115114adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ 0 < 𝐸)
116 ltmul2 12014 . . . . . . . . . 10 ((((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ ∧ (𝐸 / 𝑁) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ (((π‘‹β€˜π‘–)β€˜π‘‘) < (𝐸 / 𝑁) ↔ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < (𝐸 Β· (𝐸 / 𝑁))))
117104, 111, 86, 115, 116syl112anc 1375 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (((π‘‹β€˜π‘–)β€˜π‘‘) < (𝐸 / 𝑁) ↔ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < (𝐸 Β· (𝐸 / 𝑁))))
118113, 117mpbid 231 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (𝑗...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < (𝐸 Β· (𝐸 / 𝑁)))
11985, 109, 105, 112, 118fsumlt 15693 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· (𝐸 / 𝑁)))
12019nnne0d 12211 . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 β‰  0)
12180, 60, 120divcld 11939 . . . . . . . . . 10 (πœ‘ β†’ (𝐸 / 𝑁) ∈ β„‚)
12280, 121mulcld 11183 . . . . . . . . 9 (πœ‘ β†’ (𝐸 Β· (𝐸 / 𝑁)) ∈ β„‚)
123 fsumconst 15683 . . . . . . . . 9 (((𝑗...𝑁) ∈ Fin ∧ (𝐸 Β· (𝐸 / 𝑁)) ∈ β„‚) β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· (𝐸 / 𝑁)) = ((β™―β€˜(𝑗...𝑁)) Β· (𝐸 Β· (𝐸 / 𝑁))))
12485, 122, 123syl2anc 585 . . . . . . . 8 (πœ‘ β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· (𝐸 / 𝑁)) = ((β™―β€˜(𝑗...𝑁)) Β· (𝐸 Β· (𝐸 / 𝑁))))
125 hashfz 14336 . . . . . . . . . 10 (𝑁 ∈ (β„€β‰₯β€˜π‘—) β†’ (β™―β€˜(𝑗...𝑁)) = ((𝑁 βˆ’ 𝑗) + 1))
12615, 43, 1253syl 18 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(𝑗...𝑁)) = ((𝑁 βˆ’ 𝑗) + 1))
127126oveq1d 7376 . . . . . . . 8 (πœ‘ β†’ ((β™―β€˜(𝑗...𝑁)) Β· (𝐸 Β· (𝐸 / 𝑁))) = (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁))))
128124, 127eqtrd 2773 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· (𝐸 / 𝑁)) = (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁))))
129119, 128breqtrd 5135 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁))))
130106, 26, 54, 129ltadd2dd 11322 . . . . 5 (πœ‘ β†’ (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + Σ𝑖 ∈ (𝑗...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) < (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))))
13184, 130eqbrtrd 5131 . . . 4 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))))
132 stoweidlem11.5 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ≀ 1)
13351, 132syldan 592 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) ≀ 1)
134 1red 11164 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ 1 ∈ ℝ)
135114adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ 0 < 𝐸)
136 lemul2 12016 . . . . . . . . . 10 ((((π‘‹β€˜π‘–)β€˜π‘‘) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ (((π‘‹β€˜π‘–)β€˜π‘‘) ≀ 1 ↔ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ (𝐸 Β· 1)))
13752, 134, 36, 135, 136syl112anc 1375 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ (((π‘‹β€˜π‘–)β€˜π‘‘) ≀ 1 ↔ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ (𝐸 Β· 1)))
138133, 137mpbid 231 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ (𝐸 Β· 1))
13980mulid1d 11180 . . . . . . . . 9 (πœ‘ β†’ (𝐸 Β· 1) = 𝐸)
140139adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ (𝐸 Β· 1) = 𝐸)
141138, 140breqtrd 5135 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...(𝑗 βˆ’ 1))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ 𝐸)
14235, 53, 36, 141fsumle 15692 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))𝐸)
143 fsumconst 15683 . . . . . . . 8 (((0...(𝑗 βˆ’ 1)) ∈ Fin ∧ 𝐸 ∈ β„‚) β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))𝐸 = ((β™―β€˜(0...(𝑗 βˆ’ 1))) Β· 𝐸))
14435, 80, 143syl2anc 585 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))𝐸 = ((β™―β€˜(0...(𝑗 βˆ’ 1))) Β· 𝐸))
145 0z 12518 . . . . . . . . . . 11 0 ∈ β„€
146 1e0p1 12668 . . . . . . . . . . . . 13 1 = (0 + 1)
147146fveq2i 6849 . . . . . . . . . . . 12 (β„€β‰₯β€˜1) = (β„€β‰₯β€˜(0 + 1))
14892, 147eleqtrdi 2844 . . . . . . . . . . 11 (πœ‘ β†’ 𝑗 ∈ (β„€β‰₯β€˜(0 + 1)))
149 eluzp1m1 12797 . . . . . . . . . . 11 ((0 ∈ β„€ ∧ 𝑗 ∈ (β„€β‰₯β€˜(0 + 1))) β†’ (𝑗 βˆ’ 1) ∈ (β„€β‰₯β€˜0))
150145, 148, 149sylancr 588 . . . . . . . . . 10 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ (β„€β‰₯β€˜0))
151 hashfz 14336 . . . . . . . . . 10 ((𝑗 βˆ’ 1) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜(0...(𝑗 βˆ’ 1))) = (((𝑗 βˆ’ 1) βˆ’ 0) + 1))
152150, 151syl 17 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜(0...(𝑗 βˆ’ 1))) = (((𝑗 βˆ’ 1) βˆ’ 0) + 1))
15375, 61subcld 11520 . . . . . . . . . . 11 (πœ‘ β†’ (𝑗 βˆ’ 1) ∈ β„‚)
154153subid1d 11509 . . . . . . . . . 10 (πœ‘ β†’ ((𝑗 βˆ’ 1) βˆ’ 0) = (𝑗 βˆ’ 1))
155154oveq1d 7376 . . . . . . . . 9 (πœ‘ β†’ (((𝑗 βˆ’ 1) βˆ’ 0) + 1) = ((𝑗 βˆ’ 1) + 1))
156152, 155, 763eqtrd 2777 . . . . . . . 8 (πœ‘ β†’ (β™―β€˜(0...(𝑗 βˆ’ 1))) = 𝑗)
157156oveq1d 7376 . . . . . . 7 (πœ‘ β†’ ((β™―β€˜(0...(𝑗 βˆ’ 1))) Β· 𝐸) = (𝑗 Β· 𝐸))
15875, 80mulcomd 11184 . . . . . . 7 (πœ‘ β†’ (𝑗 Β· 𝐸) = (𝐸 Β· 𝑗))
159144, 157, 1583eqtrd 2777 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))𝐸 = (𝐸 Β· 𝑗))
160142, 159breqtrd 5135 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) ≀ (𝐸 Β· 𝑗))
16154, 18, 26, 160leadd1dd 11777 . . . 4 (πœ‘ β†’ (Σ𝑖 ∈ (0...(𝑗 βˆ’ 1))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))) ≀ ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))))
16214, 55, 27, 131, 161ltletrd 11323 . . 3 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))))
1638, 8remulcld 11193 . . . . 5 (πœ‘ β†’ (𝐸 Β· 𝐸) ∈ ℝ)
16418, 163readdcld 11192 . . . 4 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)) ∈ ℝ)
16560, 75subcld 11520 . . . . . . . 8 (πœ‘ β†’ (𝑁 βˆ’ 𝑗) ∈ β„‚)
166165, 61addcld 11182 . . . . . . 7 (πœ‘ β†’ ((𝑁 βˆ’ 𝑗) + 1) ∈ β„‚)
16780, 166, 121mul12d 11372 . . . . . 6 (πœ‘ β†’ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁))) = (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁))))
168167oveq2d 7377 . . . . 5 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)))) = ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))))
16923, 24remulcld 11193 . . . . . . 7 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)) ∈ ℝ)
1708, 169remulcld 11193 . . . . . 6 (πœ‘ β†’ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁))) ∈ ℝ)
171166, 80, 60, 120div12d 11975 . . . . . . . 8 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)) = (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) / 𝑁)))
17222, 17resubcld 11591 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 βˆ’ 𝑗) ∈ ℝ)
173 elfzle1 13453 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑁) β†’ 1 ≀ 𝑗)
17415, 173syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 1 ≀ 𝑗)
17522, 17suble0d 11754 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((1 βˆ’ 𝑗) ≀ 0 ↔ 1 ≀ 𝑗))
176174, 175mpbird 257 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 βˆ’ 𝑗) ≀ 0)
177172, 88, 20, 176leadd2dd 11778 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑁 + (1 βˆ’ 𝑗)) ≀ (𝑁 + 0))
17860, 61, 75addsub12d 11543 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑁 + (1 βˆ’ 𝑗)) = (1 + (𝑁 βˆ’ 𝑗)))
17961, 165addcomd 11365 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 + (𝑁 βˆ’ 𝑗)) = ((𝑁 βˆ’ 𝑗) + 1))
180178, 179eqtrd 2773 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑁 + (1 βˆ’ 𝑗)) = ((𝑁 βˆ’ 𝑗) + 1))
18160addid1d 11363 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑁 + 0) = 𝑁)
182177, 180, 1813brtr3d 5140 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑁 βˆ’ 𝑗) + 1) ≀ 𝑁)
18319nngt0d 12210 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < 𝑁)
184 lediv1 12028 . . . . . . . . . . . . 13 ((((𝑁 βˆ’ 𝑗) + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ (((𝑁 βˆ’ 𝑗) + 1) ≀ 𝑁 ↔ (((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ≀ (𝑁 / 𝑁)))
18523, 20, 20, 183, 184syl112anc 1375 . . . . . . . . . . . 12 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) ≀ 𝑁 ↔ (((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ≀ (𝑁 / 𝑁)))
186182, 185mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ≀ (𝑁 / 𝑁))
18760, 120dividd 11937 . . . . . . . . . . 11 (πœ‘ β†’ (𝑁 / 𝑁) = 1)
188186, 187breqtrd 5135 . . . . . . . . . 10 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ≀ 1)
18923, 19nndivred 12215 . . . . . . . . . . 11 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ∈ ℝ)
190189, 22, 7lemul2d 13009 . . . . . . . . . 10 (πœ‘ β†’ ((((𝑁 βˆ’ 𝑗) + 1) / 𝑁) ≀ 1 ↔ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) / 𝑁)) ≀ (𝐸 Β· 1)))
191188, 190mpbid 231 . . . . . . . . 9 (πœ‘ β†’ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) / 𝑁)) ≀ (𝐸 Β· 1))
192191, 139breqtrd 5135 . . . . . . . 8 (πœ‘ β†’ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) / 𝑁)) ≀ 𝐸)
193171, 192eqbrtrd 5131 . . . . . . 7 (πœ‘ β†’ (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)) ≀ 𝐸)
194169, 8, 7lemul2d 13009 . . . . . . 7 (πœ‘ β†’ ((((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)) ≀ 𝐸 ↔ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁))) ≀ (𝐸 Β· 𝐸)))
195193, 194mpbid 231 . . . . . 6 (πœ‘ β†’ (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁))) ≀ (𝐸 Β· 𝐸))
196170, 163, 18, 195leadd2dd 11778 . . . . 5 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 / 𝑁)))) ≀ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)))
197168, 196eqbrtrrd 5133 . . . 4 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))) ≀ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)))
19880, 75mulcomd 11184 . . . . . . 7 (πœ‘ β†’ (𝐸 Β· 𝑗) = (𝑗 Β· 𝐸))
199198oveq1d 7376 . . . . . 6 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)) = ((𝑗 Β· 𝐸) + (𝐸 Β· 𝐸)))
20075, 80, 80adddird 11188 . . . . . 6 (πœ‘ β†’ ((𝑗 + 𝐸) Β· 𝐸) = ((𝑗 Β· 𝐸) + (𝐸 Β· 𝐸)))
201199, 200eqtr4d 2776 . . . . 5 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)) = ((𝑗 + 𝐸) Β· 𝐸))
20217, 8readdcld 11192 . . . . . 6 (πœ‘ β†’ (𝑗 + 𝐸) ∈ ℝ)
203 stoweidlem11.8 . . . . . . 7 (πœ‘ β†’ 𝐸 < (1 / 3))
2048, 32, 17, 203ltadd2dd 11322 . . . . . 6 (πœ‘ β†’ (𝑗 + 𝐸) < (𝑗 + (1 / 3)))
205202, 33, 7, 204ltmul1dd 13020 . . . . 5 (πœ‘ β†’ ((𝑗 + 𝐸) Β· 𝐸) < ((𝑗 + (1 / 3)) Β· 𝐸))
206201, 205eqbrtrd 5131 . . . 4 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (𝐸 Β· 𝐸)) < ((𝑗 + (1 / 3)) Β· 𝐸))
20727, 164, 34, 197, 206lelttrd 11321 . . 3 (πœ‘ β†’ ((𝐸 Β· 𝑗) + (((𝑁 βˆ’ 𝑗) + 1) Β· (𝐸 Β· (𝐸 / 𝑁)))) < ((𝑗 + (1 / 3)) Β· 𝐸))
20814, 27, 34, 162, 207lttrd 11324 . 2 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) < ((𝑗 + (1 / 3)) Β· 𝐸))
2095, 208eqbrtrd 5131 1 (πœ‘ β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘‘) < ((𝑗 + (1 / 3)) Β· 𝐸))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2940  Vcvv 3447   βˆͺ cun 3912   ∩ cin 3913   βŠ† wss 3914  βˆ…c0 4286   class class class wbr 5109   ↦ cmpt 5192  βŸΆ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   βˆ’ cmin 11393   / cdiv 11820  β„•cn 12161  3c3 12217  β„€cz 12507  β„€β‰₯cuz 12771  β„+crp 12923  ...cfz 13433  β™―chash 14239  Ξ£csu 15579
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-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-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
This theorem is referenced by:  stoweidlem34  44365
  Copyright terms: Public domain W3C validator