Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑗 = (𝐽‘𝑚) → (1st ‘𝑗) = (1st
‘(𝐽‘𝑚))) |
2 | 1 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑗 = (𝐽‘𝑚) → (𝐹‘(1st ‘𝑗)) = (𝐹‘(1st ‘(𝐽‘𝑚)))) |
3 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑗 = (𝐽‘𝑚) → (2nd ‘𝑗) = (2nd
‘(𝐽‘𝑚))) |
4 | 2, 3 | fveq12d 6109 |
. . . . . . 7
⊢ (𝑗 = (𝐽‘𝑚) → ((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)) = ((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))) |
5 | 4 | fveq2d 6107 |
. . . . . 6
⊢ (𝑗 = (𝐽‘𝑚) → (2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) = (2nd
‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚))))) |
6 | 4 | fveq2d 6107 |
. . . . . 6
⊢ (𝑗 = (𝐽‘𝑚) → (1st ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) = (1st
‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚))))) |
7 | 5, 6 | oveq12d 6567 |
. . . . 5
⊢ (𝑗 = (𝐽‘𝑚) → ((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) =
((2nd ‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) − (1st ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))))) |
8 | | fzfid 12634 |
. . . . 5
⊢ (𝜑 → (1...𝐾) ∈ Fin) |
9 | | ovoliun.j |
. . . . . . 7
⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) |
10 | | f1of1 6049 |
. . . . . . 7
⊢ (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → 𝐽:ℕ–1-1→(ℕ × ℕ)) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽:ℕ–1-1→(ℕ × ℕ)) |
12 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑚 ∈ (1...𝐾) → 𝑚 ∈ ℕ) |
13 | 12 | ssriv 3572 |
. . . . . 6
⊢
(1...𝐾) ⊆
ℕ |
14 | | f1ores 6064 |
. . . . . 6
⊢ ((𝐽:ℕ–1-1→(ℕ × ℕ) ∧ (1...𝐾) ⊆ ℕ) → (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾))) |
15 | 11, 13, 14 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾))) |
16 | | fvres 6117 |
. . . . . 6
⊢ (𝑚 ∈ (1...𝐾) → ((𝐽 ↾ (1...𝐾))‘𝑚) = (𝐽‘𝑚)) |
17 | 16 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → ((𝐽 ↾ (1...𝐾))‘𝑚) = (𝐽‘𝑚)) |
18 | | inss2 3796 |
. . . . . . . . 9
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
19 | | ovoliun.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)) |
20 | 19 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)) |
21 | | imassrn 5396 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 “ (1...𝐾)) ⊆ ran 𝐽 |
22 | | f1of 6050 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → 𝐽:ℕ⟶(ℕ ×
ℕ)) |
23 | 9, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽:ℕ⟶(ℕ ×
ℕ)) |
24 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽:ℕ⟶(ℕ ×
ℕ) → ran 𝐽
⊆ (ℕ × ℕ)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐽 ⊆ (ℕ ×
ℕ)) |
26 | 21, 25 | syl5ss 3579 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐽 “ (1...𝐾)) ⊆ (ℕ ×
ℕ)) |
27 | 26 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝑗 ∈ (ℕ ×
ℕ)) |
28 | | xp1st 7089 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (ℕ ×
ℕ) → (1st ‘𝑗) ∈ ℕ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘𝑗) ∈
ℕ) |
30 | 20, 29 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (𝐹‘(1st ‘𝑗)) ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)) |
31 | | reex 9906 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
32 | 31, 31 | xpex 6860 |
. . . . . . . . . . . . 13
⊢ (ℝ
× ℝ) ∈ V |
33 | 32 | inex2 4728 |
. . . . . . . . . . . 12
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
34 | | nnex 10903 |
. . . . . . . . . . . 12
⊢ ℕ
∈ V |
35 | 33, 34 | elmap 7772 |
. . . . . . . . . . 11
⊢ ((𝐹‘(1st
‘𝑗)) ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ) ↔
(𝐹‘(1st
‘𝑗)):ℕ⟶(
≤ ∩ (ℝ × ℝ))) |
36 | 30, 35 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (𝐹‘(1st ‘𝑗)):ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
37 | | xp2nd 7090 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (ℕ ×
ℕ) → (2nd ‘𝑗) ∈ ℕ) |
38 | 27, 37 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (2nd ‘𝑗) ∈
ℕ) |
39 | 36, 38 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → ((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)) ∈ ( ≤
∩ (ℝ × ℝ))) |
40 | 18, 39 | sseldi 3566 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → ((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)) ∈ (ℝ
× ℝ)) |
41 | | xp2nd 7090 |
. . . . . . . 8
⊢ (((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗)) ∈ (ℝ ×
ℝ) → (2nd ‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗))) ∈
ℝ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) ∈
ℝ) |
43 | | xp1st 7089 |
. . . . . . . 8
⊢ (((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗)) ∈ (ℝ ×
ℝ) → (1st ‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗))) ∈
ℝ) |
44 | 40, 43 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) ∈
ℝ) |
45 | 42, 44 | resubcld 10337 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → ((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) ∈
ℝ) |
46 | 45 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → ((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) ∈
ℂ) |
47 | 7, 8, 15, 17, 46 | fsumf1o 14301 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) = Σ𝑚 ∈ (1...𝐾)((2nd ‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) − (1st ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))))) |
48 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ)) |
49 | 23 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐽‘𝑘) ∈ (ℕ ×
ℕ)) |
50 | | xp1st 7089 |
. . . . . . . . . . . 12
⊢ ((𝐽‘𝑘) ∈ (ℕ × ℕ) →
(1st ‘(𝐽‘𝑘)) ∈ ℕ) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐽‘𝑘)) ∈
ℕ) |
52 | 48, 51 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽‘𝑘))) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
53 | 33, 34 | elmap 7772 |
. . . . . . . . . 10
⊢ ((𝐹‘(1st
‘(𝐽‘𝑘))) ∈ (( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ↔ (𝐹‘(1st
‘(𝐽‘𝑘))):ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
54 | 52, 53 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽‘𝑘))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
55 | | xp2nd 7090 |
. . . . . . . . . 10
⊢ ((𝐽‘𝑘) ∈ (ℕ × ℕ) →
(2nd ‘(𝐽‘𝑘)) ∈ ℕ) |
56 | 49, 55 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐽‘𝑘)) ∈
ℕ) |
57 | 54, 56 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
58 | | ovoliun.h |
. . . . . . . 8
⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘)))) |
59 | 57, 58 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
60 | | eqid 2610 |
. . . . . . . 8
⊢ ((abs
∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻) |
61 | 60 | ovolfsval 23046 |
. . . . . . 7
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘𝑚) = ((2nd ‘(𝐻‘𝑚)) − (1st ‘(𝐻‘𝑚)))) |
62 | 59, 12, 61 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (((abs ∘ − ) ∘
𝐻)‘𝑚) = ((2nd ‘(𝐻‘𝑚)) − (1st ‘(𝐻‘𝑚)))) |
63 | 12 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → 𝑚 ∈ ℕ) |
64 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (𝐽‘𝑘) = (𝐽‘𝑚)) |
65 | 64 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (1st ‘(𝐽‘𝑘)) = (1st ‘(𝐽‘𝑚))) |
66 | 65 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝐹‘(1st ‘(𝐽‘𝑘))) = (𝐹‘(1st ‘(𝐽‘𝑚)))) |
67 | 64 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (2nd ‘(𝐽‘𝑘)) = (2nd ‘(𝐽‘𝑚))) |
68 | 66, 67 | fveq12d 6109 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))) = ((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) |
69 | | fvex 6113 |
. . . . . . . . . 10
⊢ ((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚))) ∈ V |
70 | 68, 58, 69 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → (𝐻‘𝑚) = ((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) |
71 | 63, 70 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (𝐻‘𝑚) = ((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) |
72 | 71 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (2nd ‘(𝐻‘𝑚)) = (2nd ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚))))) |
73 | 71 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (1st ‘(𝐻‘𝑚)) = (1st ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚))))) |
74 | 72, 73 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻‘𝑚)) − (1st ‘(𝐻‘𝑚))) = ((2nd ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))) − (1st
‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))))) |
75 | 62, 74 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (((abs ∘ − ) ∘
𝐻)‘𝑚) = ((2nd ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))) − (1st
‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))))) |
76 | | ovoliun.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℕ) |
77 | | nnuz 11599 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
78 | 76, 77 | syl6eleq 2698 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘1)) |
79 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
80 | 59, 12, 79 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (𝐻‘𝑚) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
81 | 18, 80 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (𝐻‘𝑚) ∈ (ℝ ×
ℝ)) |
82 | | xp2nd 7090 |
. . . . . . . . 9
⊢ ((𝐻‘𝑚) ∈ (ℝ × ℝ) →
(2nd ‘(𝐻‘𝑚)) ∈ ℝ) |
83 | 81, 82 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (2nd ‘(𝐻‘𝑚)) ∈ ℝ) |
84 | | xp1st 7089 |
. . . . . . . . 9
⊢ ((𝐻‘𝑚) ∈ (ℝ × ℝ) →
(1st ‘(𝐻‘𝑚)) ∈ ℝ) |
85 | 81, 84 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (1st ‘(𝐻‘𝑚)) ∈ ℝ) |
86 | 83, 85 | resubcld 10337 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻‘𝑚)) − (1st ‘(𝐻‘𝑚))) ∈ ℝ) |
87 | 86 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻‘𝑚)) − (1st ‘(𝐻‘𝑚))) ∈ ℂ) |
88 | 74, 87 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → ((2nd ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))) − (1st
‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚))))) ∈ ℂ) |
89 | 75, 78, 88 | fsumser 14308 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (1...𝐾)((2nd ‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) − (1st ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚))))) = (seq1( + , ((abs ∘
− ) ∘ 𝐻))‘𝐾)) |
90 | 47, 89 | eqtrd 2644 |
. . 3
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) = (seq1( + ,
((abs ∘ − ) ∘ 𝐻))‘𝐾)) |
91 | | ovoliun.u |
. . . 4
⊢ 𝑈 = seq1( + , ((abs ∘
− ) ∘ 𝐻)) |
92 | 91 | fveq1i 6104 |
. . 3
⊢ (𝑈‘𝐾) = (seq1( + , ((abs ∘ − )
∘ 𝐻))‘𝐾) |
93 | 90, 92 | syl6eqr 2662 |
. 2
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) = (𝑈‘𝐾)) |
94 | | f1oeng 7860 |
. . . . . . 7
⊢
(((1...𝐾) ∈ Fin
∧ (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾))) → (1...𝐾) ≈ (𝐽 “ (1...𝐾))) |
95 | 8, 15, 94 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (1...𝐾) ≈ (𝐽 “ (1...𝐾))) |
96 | 95 | ensymd 7893 |
. . . . 5
⊢ (𝜑 → (𝐽 “ (1...𝐾)) ≈ (1...𝐾)) |
97 | | enfii 8062 |
. . . . 5
⊢
(((1...𝐾) ∈ Fin
∧ (𝐽 “ (1...𝐾)) ≈ (1...𝐾)) → (𝐽 “ (1...𝐾)) ∈ Fin) |
98 | 8, 96, 97 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐽 “ (1...𝐾)) ∈ Fin) |
99 | 98, 45 | fsumrecl 14312 |
. . 3
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) ∈
ℝ) |
100 | | fzfid 12634 |
. . . . 5
⊢ (𝜑 → (1...𝐿) ∈ Fin) |
101 | | elfznn 12241 |
. . . . . 6
⊢ (𝑛 ∈ (1...𝐿) → 𝑛 ∈ ℕ) |
102 | | ovoliun.v |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
103 | 101, 102 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈ ℝ) |
104 | 100, 103 | fsumrecl 14312 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ℝ) |
105 | | ovoliun.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
106 | 105 | rpred 11748 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
107 | | 2nn 11062 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
108 | | nnnn0 11176 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
109 | | nnexpcl 12735 |
. . . . . . . 8
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
110 | 107, 108,
109 | sylancr 694 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℕ) |
111 | 101, 110 | syl 17 |
. . . . . 6
⊢ (𝑛 ∈ (1...𝐿) → (2↑𝑛) ∈ ℕ) |
112 | | nndivre 10933 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧
(2↑𝑛) ∈ ℕ)
→ (𝐵 / (2↑𝑛)) ∈
ℝ) |
113 | 106, 111,
112 | syl2an 493 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐵 / (2↑𝑛)) ∈ ℝ) |
114 | 100, 113 | fsumrecl 14312 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) ∈ ℝ) |
115 | 104, 114 | readdcld 9948 |
. . 3
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))) ∈ ℝ) |
116 | | ovoliun.r |
. . . 4
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
117 | 116, 106 | readdcld 9948 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) + 𝐵) ∈
ℝ) |
118 | | relxp 5150 |
. . . . . . . . . . . . . . 15
⊢ Rel
({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) |
119 | | relres 5346 |
. . . . . . . . . . . . . . 15
⊢ Rel
((𝐽 “ (1...𝐾)) ↾ {𝑛}) |
120 | | opelxp 5070 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ↔ (𝑥 ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) |
121 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
122 | 121 | opelres 5322 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ∈ ((𝐽 “ (1...𝐾)) ↾ {𝑛}) ↔ (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) ∧ 𝑥 ∈ {𝑛})) |
123 | | ancom 465 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ {𝑛} ∧ 〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾))) ↔ (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) ∧ 𝑥 ∈ {𝑛})) |
124 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ {𝑛} → 𝑥 = 𝑛) |
125 | 124 | opeq1d 4346 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ {𝑛} → 〈𝑥, 𝑦〉 = 〈𝑛, 𝑦〉) |
126 | 125 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑛} → (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) ↔ 〈𝑛, 𝑦〉 ∈ (𝐽 “ (1...𝐾)))) |
127 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑛 ∈ V |
128 | 127, 121 | elimasn 5409 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}) ↔ 〈𝑛, 𝑦〉 ∈ (𝐽 “ (1...𝐾))) |
129 | 126, 128 | syl6bbr 277 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑛} → (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) ↔ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) |
130 | 129 | pm5.32i 667 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ {𝑛} ∧ 〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾))) ↔ (𝑥 ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) |
131 | 122, 123,
130 | 3bitr2ri 288 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})) ↔ 〈𝑥, 𝑦〉 ∈ ((𝐽 “ (1...𝐾)) ↾ {𝑛})) |
132 | 120, 131 | bitri 263 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ↔ 〈𝑥, 𝑦〉 ∈ ((𝐽 “ (1...𝐾)) ↾ {𝑛})) |
133 | 118, 119,
132 | eqrelriiv 5137 |
. . . . . . . . . . . . . 14
⊢ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ↾ {𝑛}) |
134 | | df-res 5050 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 “ (1...𝐾)) ↾ {𝑛}) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)) |
135 | 133, 134 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)) |
136 | 135 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V))) |
137 | 136 | iuneq2dv 4478 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ∪
𝑛 ∈ (1...𝐿)((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V))) |
138 | | iunin2 4520 |
. . . . . . . . . . 11
⊢ ∪ 𝑛 ∈ (1...𝐿)((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)) = ((𝐽 “ (1...𝐾)) ∩ ∪
𝑛 ∈ (1...𝐿)({𝑛} × V)) |
139 | 137, 138 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ ∪
𝑛 ∈ (1...𝐿)({𝑛} × V))) |
140 | | relxp 5150 |
. . . . . . . . . . . . . 14
⊢ Rel
(ℕ × ℕ) |
141 | | relss 5129 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ) →
(Rel (ℕ × ℕ) → Rel (𝐽 “ (1...𝐾)))) |
142 | 26, 140, 141 | mpisyl 21 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Rel (𝐽 “ (1...𝐾))) |
143 | | ovoliun.l2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿) |
144 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐽:ℕ⟶(ℕ ×
ℕ) → 𝐽 Fn
ℕ) |
145 | 23, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐽 Fn ℕ) |
146 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = (𝐽‘𝑤) → (1st ‘𝑗) = (1st
‘(𝐽‘𝑤))) |
147 | 146 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (𝐽‘𝑤) → ((1st ‘𝑗) ≤ 𝐿 ↔ (1st ‘(𝐽‘𝑤)) ≤ 𝐿)) |
148 | 147 | ralima 6402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 Fn ℕ ∧ (1...𝐾) ⊆ ℕ) →
(∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st ‘𝑗) ≤ 𝐿 ↔ ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿)) |
149 | 145, 13, 148 | sylancl 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st ‘𝑗) ≤ 𝐿 ↔ ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿)) |
150 | 143, 149 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st ‘𝑗) ≤ 𝐿) |
151 | 150 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘𝑗) ≤ 𝐿) |
152 | 29, 77 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘𝑗) ∈
(ℤ≥‘1)) |
153 | | ovoliun.l1 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐿 ∈ ℤ) |
154 | 153 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝐿 ∈ ℤ) |
155 | | elfz5 12205 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1st ‘𝑗) ∈ (ℤ≥‘1)
∧ 𝐿 ∈ ℤ)
→ ((1st ‘𝑗) ∈ (1...𝐿) ↔ (1st ‘𝑗) ≤ 𝐿)) |
156 | 152, 154,
155 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → ((1st ‘𝑗) ∈ (1...𝐿) ↔ (1st ‘𝑗) ≤ 𝐿)) |
157 | 151, 156 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘𝑗) ∈ (1...𝐿)) |
158 | 157 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st ‘𝑗) ∈ (1...𝐿)) |
159 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
160 | 159, 121 | op1std 7069 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 〈𝑥, 𝑦〉 → (1st ‘𝑗) = 𝑥) |
161 | 160 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 〈𝑥, 𝑦〉 → ((1st ‘𝑗) ∈ (1...𝐿) ↔ 𝑥 ∈ (1...𝐿))) |
162 | 161 | rspccv 3279 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑗 ∈
(𝐽 “ (1...𝐾))(1st ‘𝑗) ∈ (1...𝐿) → (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) → 𝑥 ∈ (1...𝐿))) |
163 | 158, 162 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) → 𝑥 ∈ (1...𝐿))) |
164 | | opelxp 5070 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ (∪ 𝑛 ∈ (1...𝐿){𝑛} × V) ↔ (𝑥 ∈ ∪
𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V)) |
165 | 121 | biantru 525 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (1...𝐿){𝑛} ↔ (𝑥 ∈ ∪
𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V)) |
166 | | iunid 4511 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ (1...𝐿){𝑛} = (1...𝐿) |
167 | 166 | eleq2i 2680 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (1...𝐿){𝑛} ↔ 𝑥 ∈ (1...𝐿)) |
168 | 164, 165,
167 | 3bitr2i 287 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ (∪ 𝑛 ∈ (1...𝐿){𝑛} × V) ↔ 𝑥 ∈ (1...𝐿)) |
169 | 163, 168 | syl6ibr 241 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) → 〈𝑥, 𝑦〉 ∈ (∪ 𝑛 ∈ (1...𝐿){𝑛} × V))) |
170 | 142, 169 | relssdv 5135 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐽 “ (1...𝐾)) ⊆ (∪ 𝑛 ∈ (1...𝐿){𝑛} × V)) |
171 | | xpiundir 5097 |
. . . . . . . . . . . 12
⊢ (∪ 𝑛 ∈ (1...𝐿){𝑛} × V) = ∪ 𝑛 ∈ (1...𝐿)({𝑛} × V) |
172 | 170, 171 | syl6sseq 3614 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐽 “ (1...𝐾)) ⊆ ∪ 𝑛 ∈ (1...𝐿)({𝑛} × V)) |
173 | | df-ss 3554 |
. . . . . . . . . . 11
⊢ ((𝐽 “ (1...𝐾)) ⊆ ∪ 𝑛 ∈ (1...𝐿)({𝑛} × V) ↔ ((𝐽 “ (1...𝐾)) ∩ ∪
𝑛 ∈ (1...𝐿)({𝑛} × V)) = (𝐽 “ (1...𝐾))) |
174 | 172, 173 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐽 “ (1...𝐾)) ∩ ∪
𝑛 ∈ (1...𝐿)({𝑛} × V)) = (𝐽 “ (1...𝐾))) |
175 | 139, 174 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = (𝐽 “ (1...𝐾))) |
176 | 175, 98 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin) |
177 | | ssiun2 4499 |
. . . . . . . 8
⊢ (𝑛 ∈ (1...𝐿) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ⊆ ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) |
178 | | ssfi 8065 |
. . . . . . . 8
⊢
((∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ⊆ ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin) |
179 | 176, 177,
178 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin) |
180 | | 2ndconst 7153 |
. . . . . . . . . 10
⊢ (𝑛 ∈ V → (2nd
↾ ({𝑛} ×
((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛})) |
181 | 127, 180 | ax-mp 5 |
. . . . . . . . 9
⊢
(2nd ↾ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛}) |
182 | | f1oeng 7860 |
. . . . . . . . 9
⊢ ((({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ (2nd ↾
({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛})) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ≈ ((𝐽 “ (1...𝐾)) “ {𝑛})) |
183 | 179, 181,
182 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ≈ ((𝐽 “ (1...𝐾)) “ {𝑛})) |
184 | 183 | ensymd 7893 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ≈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) |
185 | | enfii 8062 |
. . . . . . 7
⊢ ((({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ ((𝐽 “ (1...𝐾)) “ {𝑛}) ≈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ∈ Fin) |
186 | 179, 184,
185 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ∈ Fin) |
187 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑𝑚 ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
188 | 19, 101, 187 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐹‘𝑛) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)) |
189 | 33, 34 | elmap 7772 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ) ↔ (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
190 | 188, 189 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
191 | 190 | adantrr 749 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
192 | | imassrn 5396 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 “ (1...𝐾)) “ {𝑛}) ⊆ ran (𝐽 “ (1...𝐾)) |
193 | 26 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐽 “ (1...𝐾)) ⊆ (ℕ ×
ℕ)) |
194 | | rnss 5275 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ) →
ran (𝐽 “ (1...𝐾)) ⊆ ran (ℕ ×
ℕ)) |
195 | 193, 194 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran (𝐽 “ (1...𝐾)) ⊆ ran (ℕ ×
ℕ)) |
196 | | rnxpid 5486 |
. . . . . . . . . . . . . . 15
⊢ ran
(ℕ × ℕ) = ℕ |
197 | 195, 196 | syl6sseq 3614 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran (𝐽 “ (1...𝐾)) ⊆ ℕ) |
198 | 192, 197 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ⊆ ℕ) |
199 | 198 | sseld 3567 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}) → 𝑖 ∈ ℕ)) |
200 | 199 | impr 647 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → 𝑖 ∈ ℕ) |
201 | 191, 200 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐹‘𝑛)‘𝑖) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
202 | 18, 201 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐹‘𝑛)‘𝑖) ∈ (ℝ ×
ℝ)) |
203 | | xp2nd 7090 |
. . . . . . . . 9
⊢ (((𝐹‘𝑛)‘𝑖) ∈ (ℝ × ℝ) →
(2nd ‘((𝐹‘𝑛)‘𝑖)) ∈ ℝ) |
204 | 202, 203 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (2nd ‘((𝐹‘𝑛)‘𝑖)) ∈ ℝ) |
205 | | xp1st 7089 |
. . . . . . . . 9
⊢ (((𝐹‘𝑛)‘𝑖) ∈ (ℝ × ℝ) →
(1st ‘((𝐹‘𝑛)‘𝑖)) ∈ ℝ) |
206 | 202, 205 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (1st ‘((𝐹‘𝑛)‘𝑖)) ∈ ℝ) |
207 | 204, 206 | resubcld 10337 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ) |
208 | 207 | anassrs 678 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})) → ((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ) |
209 | 186, 208 | fsumrecl 14312 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ) |
210 | 106, 110,
112 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 / (2↑𝑛)) ∈ ℝ) |
211 | 102, 210 | readdcld 9948 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ) |
212 | 101, 211 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ) |
213 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ∘ (𝐹‘𝑛)) = ((abs ∘ − ) ∘ (𝐹‘𝑛)) |
214 | | ovoliun.s |
. . . . . . . . . . . 12
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ (𝐹‘𝑛))) |
215 | 213, 214 | ovolsf 23048 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
216 | 190, 215 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 𝑆:ℕ⟶(0[,)+∞)) |
217 | | frn 5966 |
. . . . . . . . . 10
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ ran 𝑆 ⊆
(0[,)+∞)) |
218 | 216, 217 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆ (0[,)+∞)) |
219 | | icossxr 12129 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ* |
220 | 218, 219 | syl6ss 3580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆
ℝ*) |
221 | | supxrcl 12017 |
. . . . . . . 8
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
222 | 220, 221 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
223 | | mnfxr 9975 |
. . . . . . . . 9
⊢ -∞
∈ ℝ* |
224 | 223 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → -∞ ∈
ℝ*) |
225 | 103 | rexrd 9968 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈
ℝ*) |
226 | | mnflt 11833 |
. . . . . . . . 9
⊢
((vol*‘𝐴)
∈ ℝ → -∞ < (vol*‘𝐴)) |
227 | 103, 226 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → -∞ < (vol*‘𝐴)) |
228 | | ovoliun.x1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛))) |
229 | 101, 228 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛))) |
230 | 214 | ovollb 23054 |
. . . . . . . . 9
⊢ (((𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ 𝐴
⊆ ∪ ran ((,) ∘ (𝐹‘𝑛))) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |
231 | 190, 229,
230 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |
232 | 224, 225,
222, 227, 231 | xrltletrd 11868 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → -∞ < sup(ran 𝑆, ℝ*, <
)) |
233 | | ovoliun.x2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
≤ ((vol*‘𝐴) +
(𝐵 / (2↑𝑛)))) |
234 | 101, 233 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) |
235 | | xrre 11874 |
. . . . . . 7
⊢
(((sup(ran 𝑆,
ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ) ∧ (-∞ <
sup(ran 𝑆,
ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ) |
236 | 222, 212,
232, 234, 235 | syl22anc 1319 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ) |
237 | | 1zzd 11285 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 1 ∈ ℤ) |
238 | 213 | ovolfsval 23046 |
. . . . . . . . 9
⊢ (((𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ 𝑖
∈ ℕ) → (((abs ∘ − ) ∘ (𝐹‘𝑛))‘𝑖) = ((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖)))) |
239 | 190, 238 | sylan 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((abs ∘
− ) ∘ (𝐹‘𝑛))‘𝑖) = ((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖)))) |
240 | 213 | ovolfsf 23047 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → ((abs ∘ − ) ∘ (𝐹‘𝑛)):ℕ⟶(0[,)+∞)) |
241 | 190, 240 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ((abs ∘ − ) ∘
(𝐹‘𝑛)):ℕ⟶(0[,)+∞)) |
242 | 241 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((abs ∘
− ) ∘ (𝐹‘𝑛))‘𝑖) ∈ (0[,)+∞)) |
243 | 239, 242 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → ((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ (0[,)+∞)) |
244 | | elrege0 12149 |
. . . . . . . . . 10
⊢
(((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ (0[,)+∞) ↔
(((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ ∧ 0 ≤
((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))))) |
245 | 243, 244 | sylib 207 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ ∧ 0 ≤
((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))))) |
246 | 245 | simpld 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → ((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ) |
247 | 245 | simprd 478 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → 0 ≤
((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖)))) |
248 | | supxrub 12026 |
. . . . . . . . . . . . . . 15
⊢ ((ran
𝑆 ⊆
ℝ* ∧ 𝑧
∈ ran 𝑆) → 𝑧 ≤ sup(ran 𝑆, ℝ*, <
)) |
249 | 220, 248 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑧 ∈ ran 𝑆) → 𝑧 ≤ sup(ran 𝑆, ℝ*, <
)) |
250 | 249 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ sup(ran 𝑆, ℝ*, <
)) |
251 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = sup(ran 𝑆, ℝ*, < ) → (𝑧 ≤ 𝑥 ↔ 𝑧 ≤ sup(ran 𝑆, ℝ*, <
))) |
252 | 251 | ralbidv 2969 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = sup(ran 𝑆, ℝ*, < ) →
(∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ sup(ran 𝑆, ℝ*, <
))) |
253 | 252 | rspcev 3282 |
. . . . . . . . . . . . 13
⊢ ((sup(ran
𝑆, ℝ*,
< ) ∈ ℝ ∧ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ sup(ran 𝑆, ℝ*, < )) →
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) |
254 | 236, 250,
253 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) |
255 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ 𝑆 Fn
ℕ) |
256 | 216, 255 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 𝑆 Fn ℕ) |
257 | | breq1 4586 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ 𝑥 ↔ (𝑆‘𝑘) ≤ 𝑥)) |
258 | 257 | ralrn 6270 |
. . . . . . . . . . . . . 14
⊢ (𝑆 Fn ℕ →
(∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)) |
259 | 256, 258 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)) |
260 | 259 | rexbidv 3034 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)) |
261 | 254, 260 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥) |
262 | 77, 214, 237, 239, 246, 247, 261 | isumsup2 14417 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 𝑆 ⇝ sup(ran 𝑆, ℝ, < )) |
263 | 214, 262 | syl5eqbrr 4619 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → seq1( + , ((abs ∘ − )
∘ (𝐹‘𝑛))) ⇝ sup(ran 𝑆, ℝ, <
)) |
264 | | climrel 14071 |
. . . . . . . . . 10
⊢ Rel
⇝ |
265 | 264 | releldmi 5283 |
. . . . . . . . 9
⊢ (seq1( +
, ((abs ∘ − ) ∘ (𝐹‘𝑛))) ⇝ sup(ran 𝑆, ℝ, < ) → seq1( + , ((abs
∘ − ) ∘ (𝐹‘𝑛))) ∈ dom ⇝ ) |
266 | 263, 265 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → seq1( + , ((abs ∘ − )
∘ (𝐹‘𝑛))) ∈ dom ⇝
) |
267 | 77, 237, 186, 198, 239, 246, 247, 266 | isumless 14416 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ≤ Σ𝑖 ∈ ℕ ((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖)))) |
268 | 77, 214, 237, 239, 246, 247, 261 | isumsup 14418 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ℕ ((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) = sup(ran 𝑆, ℝ, < )) |
269 | | rge0ssre 12151 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
270 | 218, 269 | syl6ss 3580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆ ℝ) |
271 | | 1nn 10908 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
272 | | fdm 5964 |
. . . . . . . . . . . . 13
⊢ (𝑆:ℕ⟶(0[,)+∞)
→ dom 𝑆 =
ℕ) |
273 | 216, 272 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → dom 𝑆 = ℕ) |
274 | 271, 273 | syl5eleqr 2695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 1 ∈ dom 𝑆) |
275 | | ne0i 3880 |
. . . . . . . . . . 11
⊢ (1 ∈
dom 𝑆 → dom 𝑆 ≠ ∅) |
276 | 274, 275 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → dom 𝑆 ≠ ∅) |
277 | | dm0rn0 5263 |
. . . . . . . . . . 11
⊢ (dom
𝑆 = ∅ ↔ ran
𝑆 =
∅) |
278 | 277 | necon3bii 2834 |
. . . . . . . . . 10
⊢ (dom
𝑆 ≠ ∅ ↔ ran
𝑆 ≠
∅) |
279 | 276, 278 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran 𝑆 ≠ ∅) |
280 | | supxrre 12029 |
. . . . . . . . 9
⊢ ((ran
𝑆 ⊆ ℝ ∧ ran
𝑆 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran
𝑆, ℝ, <
)) |
281 | 270, 279,
254, 280 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) = sup(ran
𝑆, ℝ, <
)) |
282 | 268, 281 | eqtr4d 2647 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ℕ ((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) = sup(ran 𝑆, ℝ*, <
)) |
283 | 267, 282 | breqtrd 4609 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ≤ sup(ran 𝑆, ℝ*, <
)) |
284 | 209, 236,
212, 283, 234 | letrd 10073 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) |
285 | 100, 209,
212, 284 | fsumle 14372 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ≤ Σ𝑛 ∈ (1...𝐿)((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) |
286 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑖 ∈ V |
287 | 127, 286 | op1std 7069 |
. . . . . . . . . 10
⊢ (𝑗 = 〈𝑛, 𝑖〉 → (1st ‘𝑗) = 𝑛) |
288 | 287 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑗 = 〈𝑛, 𝑖〉 → (𝐹‘(1st ‘𝑗)) = (𝐹‘𝑛)) |
289 | 127, 286 | op2ndd 7070 |
. . . . . . . . 9
⊢ (𝑗 = 〈𝑛, 𝑖〉 → (2nd ‘𝑗) = 𝑖) |
290 | 288, 289 | fveq12d 6109 |
. . . . . . . 8
⊢ (𝑗 = 〈𝑛, 𝑖〉 → ((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)) = ((𝐹‘𝑛)‘𝑖)) |
291 | 290 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑗 = 〈𝑛, 𝑖〉 → (2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) = (2nd
‘((𝐹‘𝑛)‘𝑖))) |
292 | 290 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑗 = 〈𝑛, 𝑖〉 → (1st ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) = (1st
‘((𝐹‘𝑛)‘𝑖))) |
293 | 291, 292 | oveq12d 6567 |
. . . . . 6
⊢ (𝑗 = 〈𝑛, 𝑖〉 → ((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) =
((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖)))) |
294 | 207 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℂ) |
295 | 293, 100,
186, 294 | fsum2d 14344 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) = Σ𝑗 ∈ ∪
𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗))))) |
296 | 175 | sumeq1d 14279 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ ∪
𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) = Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗))))) |
297 | 295, 296 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) = Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗))))) |
298 | 103 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈ ℂ) |
299 | 113 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐵 / (2↑𝑛)) ∈ ℂ) |
300 | 100, 298,
299 | fsumadd 14317 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)((vol*‘𝐴) + (𝐵 / (2↑𝑛))) = (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)))) |
301 | 285, 297,
300 | 3brtr3d 4614 |
. . 3
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) ≤
(Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)))) |
302 | | 1zzd 11285 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
303 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
304 | | ovoliun.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) |
305 | 304 | fvmpt2 6200 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧
(vol*‘𝐴) ∈
ℝ) → (𝐺‘𝑛) = (vol*‘𝐴)) |
306 | 303, 102,
305 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = (vol*‘𝐴)) |
307 | 306, 102 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℝ) |
308 | 77, 302, 307 | serfre 12692 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
309 | | ovoliun.t |
. . . . . . . . 9
⊢ 𝑇 = seq1( + , 𝐺) |
310 | 309 | feq1i 5949 |
. . . . . . . 8
⊢ (𝑇:ℕ⟶ℝ ↔
seq1( + , 𝐺):ℕ⟶ℝ) |
311 | 308, 310 | sylibr 223 |
. . . . . . 7
⊢ (𝜑 → 𝑇:ℕ⟶ℝ) |
312 | | frn 5966 |
. . . . . . 7
⊢ (𝑇:ℕ⟶ℝ →
ran 𝑇 ⊆
ℝ) |
313 | 311, 312 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝑇 ⊆ ℝ) |
314 | | ressxr 9962 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
315 | 313, 314 | syl6ss 3580 |
. . . . 5
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
316 | 101, 306 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐺‘𝑛) = (vol*‘𝐴)) |
317 | | 1red 9934 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
318 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝐽:ℕ⟶(ℕ ×
ℕ) ∧ 1 ∈ ℕ) → (𝐽‘1) ∈ (ℕ ×
ℕ)) |
319 | 23, 271, 318 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐽‘1) ∈ (ℕ ×
ℕ)) |
320 | | xp1st 7089 |
. . . . . . . . . . . 12
⊢ ((𝐽‘1) ∈ (ℕ
× ℕ) → (1st ‘(𝐽‘1)) ∈ ℕ) |
321 | 319, 320 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (1st
‘(𝐽‘1)) ∈
ℕ) |
322 | 321 | nnred 10912 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘(𝐽‘1)) ∈
ℝ) |
323 | 153 | zred 11358 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ ℝ) |
324 | 321 | nnge1d 10940 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≤ (1st
‘(𝐽‘1))) |
325 | | eluzfz1 12219 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈
(ℤ≥‘1) → 1 ∈ (1...𝐾)) |
326 | 78, 325 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈ (1...𝐾)) |
327 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 1 → (𝐽‘𝑤) = (𝐽‘1)) |
328 | 327 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 1 → (1st
‘(𝐽‘𝑤)) = (1st
‘(𝐽‘1))) |
329 | 328 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑤 = 1 → ((1st
‘(𝐽‘𝑤)) ≤ 𝐿 ↔ (1st ‘(𝐽‘1)) ≤ 𝐿)) |
330 | 329 | rspcv 3278 |
. . . . . . . . . . 11
⊢ (1 ∈
(1...𝐾) →
(∀𝑤 ∈
(1...𝐾)(1st
‘(𝐽‘𝑤)) ≤ 𝐿 → (1st ‘(𝐽‘1)) ≤ 𝐿)) |
331 | 326, 143,
330 | sylc 63 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘(𝐽‘1)) ≤
𝐿) |
332 | 317, 322,
323, 324, 331 | letrd 10073 |
. . . . . . . . 9
⊢ (𝜑 → 1 ≤ 𝐿) |
333 | | elnnz1 11280 |
. . . . . . . . 9
⊢ (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 1 ≤
𝐿)) |
334 | 153, 332,
333 | sylanbrc 695 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ ℕ) |
335 | 334, 77 | syl6eleq 2698 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈
(ℤ≥‘1)) |
336 | 316, 335,
298 | fsumser 14308 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) = (seq1( + , 𝐺)‘𝐿)) |
337 | | seqfn 12675 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → seq1( + , 𝐺)
Fn (ℤ≥‘1)) |
338 | 302, 337 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐺) Fn
(ℤ≥‘1)) |
339 | | fnfvelrn 6264 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐺) Fn
(ℤ≥‘1) ∧ 𝐿 ∈ (ℤ≥‘1))
→ (seq1( + , 𝐺)‘𝐿) ∈ ran seq1( + , 𝐺)) |
340 | 338, 335,
339 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (seq1( + , 𝐺)‘𝐿) ∈ ran seq1( + , 𝐺)) |
341 | 309 | rneqi 5273 |
. . . . . . 7
⊢ ran 𝑇 = ran seq1( + , 𝐺) |
342 | 340, 341 | syl6eleqr 2699 |
. . . . . 6
⊢ (𝜑 → (seq1( + , 𝐺)‘𝐿) ∈ ran 𝑇) |
343 | 336, 342 | eqeltrd 2688 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ran 𝑇) |
344 | | supxrub 12026 |
. . . . 5
⊢ ((ran
𝑇 ⊆
ℝ* ∧ Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ran 𝑇) → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) |
345 | 315, 343,
344 | syl2anc 691 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) |
346 | 106 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
347 | | geo2sum 14443 |
. . . . . 6
⊢ ((𝐿 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) = (𝐵 − (𝐵 / (2↑𝐿)))) |
348 | 334, 346,
347 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) = (𝐵 − (𝐵 / (2↑𝐿)))) |
349 | 334 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈
ℕ0) |
350 | | nnexpcl 12735 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝐿
∈ ℕ0) → (2↑𝐿) ∈ ℕ) |
351 | 107, 349,
350 | sylancr 694 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝐿) ∈ ℕ) |
352 | 351 | nnrpd 11746 |
. . . . . . . 8
⊢ (𝜑 → (2↑𝐿) ∈
ℝ+) |
353 | 105, 352 | rpdivcld 11765 |
. . . . . . 7
⊢ (𝜑 → (𝐵 / (2↑𝐿)) ∈
ℝ+) |
354 | 353 | rpge0d 11752 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐵 / (2↑𝐿))) |
355 | 106, 351 | nndivred 10946 |
. . . . . . 7
⊢ (𝜑 → (𝐵 / (2↑𝐿)) ∈ ℝ) |
356 | 106, 355 | subge02d 10498 |
. . . . . 6
⊢ (𝜑 → (0 ≤ (𝐵 / (2↑𝐿)) ↔ (𝐵 − (𝐵 / (2↑𝐿))) ≤ 𝐵)) |
357 | 354, 356 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝐵 − (𝐵 / (2↑𝐿))) ≤ 𝐵) |
358 | 348, 357 | eqbrtrd 4605 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) ≤ 𝐵) |
359 | 104, 114,
116, 106, 345, 358 | le2addd 10525 |
. . 3
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
360 | 99, 115, 117, 301, 359 | letrd 10073 |
. 2
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) ≤ (sup(ran
𝑇, ℝ*,
< ) + 𝐵)) |
361 | 93, 360 | eqbrtrrd 4607 |
1
⊢ (𝜑 → (𝑈‘𝐾) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |