| Step | Hyp | Ref
| Expression |
| 1 | | 2fveq3 6911 |
. . . . . . . 8
⊢ (𝑗 = (𝐽‘𝑚) → (𝐹‘(1st ‘𝑗)) = (𝐹‘(1st ‘(𝐽‘𝑚)))) |
| 2 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑗 = (𝐽‘𝑚) → (2nd ‘𝑗) = (2nd
‘(𝐽‘𝑚))) |
| 3 | 1, 2 | fveq12d 6913 |
. . . . . . 7
⊢ (𝑗 = (𝐽‘𝑚) → ((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)) = ((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))) |
| 4 | 3 | fveq2d 6910 |
. . . . . 6
⊢ (𝑗 = (𝐽‘𝑚) → (2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) = (2nd
‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚))))) |
| 5 | 3 | fveq2d 6910 |
. . . . . 6
⊢ (𝑗 = (𝐽‘𝑚) → (1st ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) = (1st
‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚))))) |
| 6 | 4, 5 | oveq12d 7449 |
. . . . 5
⊢ (𝑗 = (𝐽‘𝑚) → ((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) =
((2nd ‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) − (1st ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))))) |
| 7 | | fzfid 14014 |
. . . . 5
⊢ (𝜑 → (1...𝐾) ∈ Fin) |
| 8 | | ovoliun.j |
. . . . . . 7
⊢ (𝜑 → 𝐽:ℕ–1-1-onto→(ℕ × ℕ)) |
| 9 | | f1of1 6847 |
. . . . . . 7
⊢ (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → 𝐽:ℕ–1-1→(ℕ × ℕ)) |
| 10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽:ℕ–1-1→(ℕ × ℕ)) |
| 11 | | fz1ssnn 13595 |
. . . . . 6
⊢
(1...𝐾) ⊆
ℕ |
| 12 | | f1ores 6862 |
. . . . . 6
⊢ ((𝐽:ℕ–1-1→(ℕ × ℕ) ∧ (1...𝐾) ⊆ ℕ) → (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾))) |
| 13 | 10, 11, 12 | sylancl 586 |
. . . . 5
⊢ (𝜑 → (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾))) |
| 14 | | fvres 6925 |
. . . . . 6
⊢ (𝑚 ∈ (1...𝐾) → ((𝐽 ↾ (1...𝐾))‘𝑚) = (𝐽‘𝑚)) |
| 15 | 14 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → ((𝐽 ↾ (1...𝐾))‘𝑚) = (𝐽‘𝑚)) |
| 16 | | ovoliun.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)) |
| 18 | | imassrn 6089 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 “ (1...𝐾)) ⊆ ran 𝐽 |
| 19 | | f1of 6848 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → 𝐽:ℕ⟶(ℕ ×
ℕ)) |
| 20 | 8, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽:ℕ⟶(ℕ ×
ℕ)) |
| 21 | 20 | frnd 6744 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ran 𝐽 ⊆ (ℕ ×
ℕ)) |
| 22 | 18, 21 | sstrid 3995 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐽 “ (1...𝐾)) ⊆ (ℕ ×
ℕ)) |
| 23 | 22 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝑗 ∈ (ℕ ×
ℕ)) |
| 24 | | xp1st 8046 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (ℕ ×
ℕ) → (1st ‘𝑗) ∈ ℕ) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘𝑗) ∈
ℕ) |
| 26 | 17, 25 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (𝐹‘(1st ‘𝑗)) ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)) |
| 27 | | elovolmlem 25509 |
. . . . . . . . . . 11
⊢ ((𝐹‘(1st
‘𝑗)) ∈ (( ≤
∩ (ℝ × ℝ)) ↑m ℕ) ↔ (𝐹‘(1st
‘𝑗)):ℕ⟶(
≤ ∩ (ℝ × ℝ))) |
| 28 | 26, 27 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (𝐹‘(1st ‘𝑗)):ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
| 29 | | xp2nd 8047 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (ℕ ×
ℕ) → (2nd ‘𝑗) ∈ ℕ) |
| 30 | 23, 29 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (2nd ‘𝑗) ∈
ℕ) |
| 31 | 28, 30 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → ((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)) ∈ ( ≤
∩ (ℝ × ℝ))) |
| 32 | 31 | elin2d 4205 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → ((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)) ∈ (ℝ
× ℝ)) |
| 33 | | xp2nd 8047 |
. . . . . . . 8
⊢ (((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗)) ∈ (ℝ ×
ℝ) → (2nd ‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗))) ∈
ℝ) |
| 34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) ∈
ℝ) |
| 35 | | xp1st 8046 |
. . . . . . . 8
⊢ (((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗)) ∈ (ℝ ×
ℝ) → (1st ‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗))) ∈
ℝ) |
| 36 | 32, 35 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) ∈
ℝ) |
| 37 | 34, 36 | resubcld 11691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → ((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) ∈
ℝ) |
| 38 | 37 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → ((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) ∈
ℂ) |
| 39 | 6, 7, 13, 15, 38 | fsumf1o 15759 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) = Σ𝑚 ∈ (1...𝐾)((2nd ‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) − (1st ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))))) |
| 40 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ
× ℝ)) ↑m ℕ)) |
| 41 | 20 | ffvelcdmda 7104 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐽‘𝑘) ∈ (ℕ ×
ℕ)) |
| 42 | | xp1st 8046 |
. . . . . . . . . . . 12
⊢ ((𝐽‘𝑘) ∈ (ℕ × ℕ) →
(1st ‘(𝐽‘𝑘)) ∈ ℕ) |
| 43 | 41, 42 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (1st
‘(𝐽‘𝑘)) ∈
ℕ) |
| 44 | 40, 43 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽‘𝑘))) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) |
| 45 | | elovolmlem 25509 |
. . . . . . . . . 10
⊢ ((𝐹‘(1st
‘(𝐽‘𝑘))) ∈ (( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ↔ (𝐹‘(1st
‘(𝐽‘𝑘))):ℕ⟶( ≤ ∩
(ℝ × ℝ))) |
| 46 | 44, 45 | sylib 218 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽‘𝑘))):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 47 | | xp2nd 8047 |
. . . . . . . . . 10
⊢ ((𝐽‘𝑘) ∈ (ℕ × ℕ) →
(2nd ‘(𝐽‘𝑘)) ∈ ℕ) |
| 48 | 41, 47 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2nd
‘(𝐽‘𝑘)) ∈
ℕ) |
| 49 | 46, 48 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 50 | | ovoliun.h |
. . . . . . . 8
⊢ 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘)))) |
| 51 | 49, 50 | fmptd 7134 |
. . . . . . 7
⊢ (𝜑 → 𝐻:ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 52 | | elfznn 13593 |
. . . . . . 7
⊢ (𝑚 ∈ (1...𝐾) → 𝑚 ∈ ℕ) |
| 53 | | eqid 2737 |
. . . . . . . 8
⊢ ((abs
∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻) |
| 54 | 53 | ovolfsval 25505 |
. . . . . . 7
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (((abs ∘
− ) ∘ 𝐻)‘𝑚) = ((2nd ‘(𝐻‘𝑚)) − (1st ‘(𝐻‘𝑚)))) |
| 55 | 51, 52, 54 | syl2an 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (((abs ∘ − ) ∘
𝐻)‘𝑚) = ((2nd ‘(𝐻‘𝑚)) − (1st ‘(𝐻‘𝑚)))) |
| 56 | 52 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → 𝑚 ∈ ℕ) |
| 57 | | 2fveq3 6911 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (1st ‘(𝐽‘𝑘)) = (1st ‘(𝐽‘𝑚))) |
| 58 | 57 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝐹‘(1st ‘(𝐽‘𝑘))) = (𝐹‘(1st ‘(𝐽‘𝑚)))) |
| 59 | | 2fveq3 6911 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (2nd ‘(𝐽‘𝑘)) = (2nd ‘(𝐽‘𝑚))) |
| 60 | 58, 59 | fveq12d 6913 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → ((𝐹‘(1st ‘(𝐽‘𝑘)))‘(2nd ‘(𝐽‘𝑘))) = ((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) |
| 61 | | fvex 6919 |
. . . . . . . . . 10
⊢ ((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚))) ∈ V |
| 62 | 60, 50, 61 | fvmpt 7016 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → (𝐻‘𝑚) = ((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) |
| 63 | 56, 62 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (𝐻‘𝑚) = ((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) |
| 64 | 63 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (2nd ‘(𝐻‘𝑚)) = (2nd ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚))))) |
| 65 | 63 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (1st ‘(𝐻‘𝑚)) = (1st ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚))))) |
| 66 | 64, 65 | oveq12d 7449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻‘𝑚)) − (1st ‘(𝐻‘𝑚))) = ((2nd ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))) − (1st
‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))))) |
| 67 | 55, 66 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (((abs ∘ − ) ∘
𝐻)‘𝑚) = ((2nd ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))) − (1st
‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))))) |
| 68 | | ovoliun.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℕ) |
| 69 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 70 | 68, 69 | eleqtrdi 2851 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘1)) |
| 71 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((𝐻:ℕ⟶( ≤ ∩
(ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 72 | 51, 52, 71 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (𝐻‘𝑚) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 73 | 72 | elin2d 4205 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (𝐻‘𝑚) ∈ (ℝ ×
ℝ)) |
| 74 | | xp2nd 8047 |
. . . . . . . . 9
⊢ ((𝐻‘𝑚) ∈ (ℝ × ℝ) →
(2nd ‘(𝐻‘𝑚)) ∈ ℝ) |
| 75 | 73, 74 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (2nd ‘(𝐻‘𝑚)) ∈ ℝ) |
| 76 | | xp1st 8046 |
. . . . . . . . 9
⊢ ((𝐻‘𝑚) ∈ (ℝ × ℝ) →
(1st ‘(𝐻‘𝑚)) ∈ ℝ) |
| 77 | 73, 76 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → (1st ‘(𝐻‘𝑚)) ∈ ℝ) |
| 78 | 75, 77 | resubcld 11691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻‘𝑚)) − (1st ‘(𝐻‘𝑚))) ∈ ℝ) |
| 79 | 78 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻‘𝑚)) − (1st ‘(𝐻‘𝑚))) ∈ ℂ) |
| 80 | 66, 79 | eqeltrrd 2842 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...𝐾)) → ((2nd ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚)))) − (1st
‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚))))) ∈ ℂ) |
| 81 | 67, 70, 80 | fsumser 15766 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (1...𝐾)((2nd ‘((𝐹‘(1st ‘(𝐽‘𝑚)))‘(2nd ‘(𝐽‘𝑚)))) − (1st ‘((𝐹‘(1st
‘(𝐽‘𝑚)))‘(2nd
‘(𝐽‘𝑚))))) = (seq1( + , ((abs ∘
− ) ∘ 𝐻))‘𝐾)) |
| 82 | 39, 81 | eqtrd 2777 |
. . 3
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) = (seq1( + ,
((abs ∘ − ) ∘ 𝐻))‘𝐾)) |
| 83 | | ovoliun.u |
. . . 4
⊢ 𝑈 = seq1( + , ((abs ∘
− ) ∘ 𝐻)) |
| 84 | 83 | fveq1i 6907 |
. . 3
⊢ (𝑈‘𝐾) = (seq1( + , ((abs ∘ − )
∘ 𝐻))‘𝐾) |
| 85 | 82, 84 | eqtr4di 2795 |
. 2
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) = (𝑈‘𝐾)) |
| 86 | | f1oeng 9011 |
. . . . . . 7
⊢
(((1...𝐾) ∈ Fin
∧ (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾))) → (1...𝐾) ≈ (𝐽 “ (1...𝐾))) |
| 87 | 7, 13, 86 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (1...𝐾) ≈ (𝐽 “ (1...𝐾))) |
| 88 | 87 | ensymd 9045 |
. . . . 5
⊢ (𝜑 → (𝐽 “ (1...𝐾)) ≈ (1...𝐾)) |
| 89 | | enfii 9226 |
. . . . 5
⊢
(((1...𝐾) ∈ Fin
∧ (𝐽 “ (1...𝐾)) ≈ (1...𝐾)) → (𝐽 “ (1...𝐾)) ∈ Fin) |
| 90 | 7, 88, 89 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐽 “ (1...𝐾)) ∈ Fin) |
| 91 | 90, 37 | fsumrecl 15770 |
. . 3
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) ∈
ℝ) |
| 92 | | fzfid 14014 |
. . . . 5
⊢ (𝜑 → (1...𝐿) ∈ Fin) |
| 93 | | elfznn 13593 |
. . . . . 6
⊢ (𝑛 ∈ (1...𝐿) → 𝑛 ∈ ℕ) |
| 94 | | ovoliun.v |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol*‘𝐴) ∈
ℝ) |
| 95 | 93, 94 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈ ℝ) |
| 96 | 92, 95 | fsumrecl 15770 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ℝ) |
| 97 | | ovoliun.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ+) |
| 98 | 97 | rpred 13077 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 99 | | 2nn 12339 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
| 100 | | nnnn0 12533 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
| 101 | | nnexpcl 14115 |
. . . . . . . 8
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
| 102 | 99, 100, 101 | sylancr 587 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℕ) |
| 103 | 93, 102 | syl 17 |
. . . . . 6
⊢ (𝑛 ∈ (1...𝐿) → (2↑𝑛) ∈ ℕ) |
| 104 | | nndivre 12307 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧
(2↑𝑛) ∈ ℕ)
→ (𝐵 / (2↑𝑛)) ∈
ℝ) |
| 105 | 98, 103, 104 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐵 / (2↑𝑛)) ∈ ℝ) |
| 106 | 92, 105 | fsumrecl 15770 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) ∈ ℝ) |
| 107 | 96, 106 | readdcld 11290 |
. . 3
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))) ∈ ℝ) |
| 108 | | ovoliun.r |
. . . 4
⊢ (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈
ℝ) |
| 109 | 108, 98 | readdcld 11290 |
. . 3
⊢ (𝜑 → (sup(ran 𝑇, ℝ*, < ) + 𝐵) ∈
ℝ) |
| 110 | | relxp 5703 |
. . . . . . . . . . . . . . 15
⊢ Rel
({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) |
| 111 | | relres 6023 |
. . . . . . . . . . . . . . 15
⊢ Rel
((𝐽 “ (1...𝐾)) ↾ {𝑛}) |
| 112 | | elsni 4643 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ {𝑛} → 𝑥 = 𝑛) |
| 113 | 112 | opeq1d 4879 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑛} → 〈𝑥, 𝑦〉 = 〈𝑛, 𝑦〉) |
| 114 | 113 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑛} → (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) ↔ 〈𝑛, 𝑦〉 ∈ (𝐽 “ (1...𝐾)))) |
| 115 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑛 ∈ V |
| 116 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑦 ∈ V |
| 117 | 115, 116 | elimasn 6108 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}) ↔ 〈𝑛, 𝑦〉 ∈ (𝐽 “ (1...𝐾))) |
| 118 | 114, 117 | bitr4di 289 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑛} → (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) ↔ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) |
| 119 | 118 | pm5.32i 574 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ {𝑛} ∧ 〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾))) ↔ (𝑥 ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) |
| 120 | 116 | opelresi 6005 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ ((𝐽 “ (1...𝐾)) ↾ {𝑛}) ↔ (𝑥 ∈ {𝑛} ∧ 〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)))) |
| 121 | | opelxp 5721 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ↔ (𝑥 ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) |
| 122 | 119, 120,
121 | 3bitr4ri 304 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ↔ 〈𝑥, 𝑦〉 ∈ ((𝐽 “ (1...𝐾)) ↾ {𝑛})) |
| 123 | 110, 111,
122 | eqrelriiv 5800 |
. . . . . . . . . . . . . 14
⊢ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ↾ {𝑛}) |
| 124 | | df-res 5697 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 “ (1...𝐾)) ↾ {𝑛}) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)) |
| 125 | 123, 124 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)) |
| 126 | 125 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V))) |
| 127 | 126 | iuneq2dv 5016 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ∪
𝑛 ∈ (1...𝐿)((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V))) |
| 128 | | iunin2 5071 |
. . . . . . . . . . 11
⊢ ∪ 𝑛 ∈ (1...𝐿)((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)) = ((𝐽 “ (1...𝐾)) ∩ ∪
𝑛 ∈ (1...𝐿)({𝑛} × V)) |
| 129 | 127, 128 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ ∪
𝑛 ∈ (1...𝐿)({𝑛} × V))) |
| 130 | | relxp 5703 |
. . . . . . . . . . . . . 14
⊢ Rel
(ℕ × ℕ) |
| 131 | | relss 5791 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ) →
(Rel (ℕ × ℕ) → Rel (𝐽 “ (1...𝐾)))) |
| 132 | 22, 130, 131 | mpisyl 21 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Rel (𝐽 “ (1...𝐾))) |
| 133 | | ovoliun.l2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿) |
| 134 | 20 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐽 Fn ℕ) |
| 135 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = (𝐽‘𝑤) → (1st ‘𝑗) = (1st
‘(𝐽‘𝑤))) |
| 136 | 135 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = (𝐽‘𝑤) → ((1st ‘𝑗) ≤ 𝐿 ↔ (1st ‘(𝐽‘𝑤)) ≤ 𝐿)) |
| 137 | 136 | ralima 7257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 Fn ℕ ∧ (1...𝐾) ⊆ ℕ) →
(∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st ‘𝑗) ≤ 𝐿 ↔ ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿)) |
| 138 | 134, 11, 137 | sylancl 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st ‘𝑗) ≤ 𝐿 ↔ ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽‘𝑤)) ≤ 𝐿)) |
| 139 | 133, 138 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st ‘𝑗) ≤ 𝐿) |
| 140 | 139 | r19.21bi 3251 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘𝑗) ≤ 𝐿) |
| 141 | 25, 69 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘𝑗) ∈
(ℤ≥‘1)) |
| 142 | | ovoliun.l1 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐿 ∈ ℤ) |
| 143 | 142 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝐿 ∈ ℤ) |
| 144 | | elfz5 13556 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1st ‘𝑗) ∈ (ℤ≥‘1)
∧ 𝐿 ∈ ℤ)
→ ((1st ‘𝑗) ∈ (1...𝐿) ↔ (1st ‘𝑗) ≤ 𝐿)) |
| 145 | 141, 143,
144 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → ((1st ‘𝑗) ∈ (1...𝐿) ↔ (1st ‘𝑗) ≤ 𝐿)) |
| 146 | 140, 145 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘𝑗) ∈ (1...𝐿)) |
| 147 | 146 | ralrimiva 3146 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st ‘𝑗) ∈ (1...𝐿)) |
| 148 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
| 149 | 148, 116 | op1std 8024 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 〈𝑥, 𝑦〉 → (1st ‘𝑗) = 𝑥) |
| 150 | 149 | eleq1d 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 〈𝑥, 𝑦〉 → ((1st ‘𝑗) ∈ (1...𝐿) ↔ 𝑥 ∈ (1...𝐿))) |
| 151 | 150 | rspccv 3619 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑗 ∈
(𝐽 “ (1...𝐾))(1st ‘𝑗) ∈ (1...𝐿) → (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) → 𝑥 ∈ (1...𝐿))) |
| 152 | 147, 151 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) → 𝑥 ∈ (1...𝐿))) |
| 153 | | opelxp 5721 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ (∪ 𝑛 ∈ (1...𝐿){𝑛} × V) ↔ (𝑥 ∈ ∪
𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V)) |
| 154 | 116 | biantru 529 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (1...𝐿){𝑛} ↔ (𝑥 ∈ ∪
𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V)) |
| 155 | | iunid 5060 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑛 ∈ (1...𝐿){𝑛} = (1...𝐿) |
| 156 | 155 | eleq2i 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ 𝑛 ∈ (1...𝐿){𝑛} ↔ 𝑥 ∈ (1...𝐿)) |
| 157 | 153, 154,
156 | 3bitr2i 299 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑦〉 ∈ (∪ 𝑛 ∈ (1...𝐿){𝑛} × V) ↔ 𝑥 ∈ (1...𝐿)) |
| 158 | 152, 157 | imbitrrdi 252 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ (𝐽 “ (1...𝐾)) → 〈𝑥, 𝑦〉 ∈ (∪ 𝑛 ∈ (1...𝐿){𝑛} × V))) |
| 159 | 132, 158 | relssdv 5798 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐽 “ (1...𝐾)) ⊆ (∪ 𝑛 ∈ (1...𝐿){𝑛} × V)) |
| 160 | | xpiundir 5757 |
. . . . . . . . . . . 12
⊢ (∪ 𝑛 ∈ (1...𝐿){𝑛} × V) = ∪ 𝑛 ∈ (1...𝐿)({𝑛} × V) |
| 161 | 159, 160 | sseqtrdi 4024 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐽 “ (1...𝐾)) ⊆ ∪ 𝑛 ∈ (1...𝐿)({𝑛} × V)) |
| 162 | | dfss2 3969 |
. . . . . . . . . . 11
⊢ ((𝐽 “ (1...𝐾)) ⊆ ∪ 𝑛 ∈ (1...𝐿)({𝑛} × V) ↔ ((𝐽 “ (1...𝐾)) ∩ ∪
𝑛 ∈ (1...𝐿)({𝑛} × V)) = (𝐽 “ (1...𝐾))) |
| 163 | 161, 162 | sylib 218 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐽 “ (1...𝐾)) ∩ ∪
𝑛 ∈ (1...𝐿)({𝑛} × V)) = (𝐽 “ (1...𝐾))) |
| 164 | 129, 163 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = (𝐽 “ (1...𝐾))) |
| 165 | 164, 90 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin) |
| 166 | | ssiun2 5047 |
. . . . . . . 8
⊢ (𝑛 ∈ (1...𝐿) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ⊆ ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) |
| 167 | | ssfi 9213 |
. . . . . . . 8
⊢
((∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ⊆ ∪ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin) |
| 168 | 165, 166,
167 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin) |
| 169 | | 2ndconst 8126 |
. . . . . . . . . 10
⊢ (𝑛 ∈ V → (2nd
↾ ({𝑛} ×
((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛})) |
| 170 | 169 | elv 3485 |
. . . . . . . . 9
⊢
(2nd ↾ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛}) |
| 171 | | f1oeng 9011 |
. . . . . . . . 9
⊢ ((({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ (2nd ↾
({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛})) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ≈ ((𝐽 “ (1...𝐾)) “ {𝑛})) |
| 172 | 168, 170,
171 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ≈ ((𝐽 “ (1...𝐾)) “ {𝑛})) |
| 173 | 172 | ensymd 9045 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ≈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) |
| 174 | | enfii 9226 |
. . . . . . 7
⊢ ((({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ ((𝐽 “ (1...𝐾)) “ {𝑛}) ≈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ∈ Fin) |
| 175 | 168, 173,
174 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ∈ Fin) |
| 176 | | ffvelcdm 7101 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ℕ⟶(( ≤ ∩
(ℝ × ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) |
| 177 | 16, 93, 176 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐹‘𝑛) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ)) |
| 178 | | elovolmlem 25509 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛) ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑m ℕ) ↔ (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 179 | 177, 178 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 180 | 179 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ))) |
| 181 | | imassrn 6089 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 “ (1...𝐾)) “ {𝑛}) ⊆ ran (𝐽 “ (1...𝐾)) |
| 182 | 22 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐽 “ (1...𝐾)) ⊆ (ℕ ×
ℕ)) |
| 183 | | rnss 5950 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ) →
ran (𝐽 “ (1...𝐾)) ⊆ ran (ℕ ×
ℕ)) |
| 184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran (𝐽 “ (1...𝐾)) ⊆ ran (ℕ ×
ℕ)) |
| 185 | | rnxpid 6193 |
. . . . . . . . . . . . . . 15
⊢ ran
(ℕ × ℕ) = ℕ |
| 186 | 184, 185 | sseqtrdi 4024 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran (𝐽 “ (1...𝐾)) ⊆ ℕ) |
| 187 | 181, 186 | sstrid 3995 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ⊆ ℕ) |
| 188 | 187 | sseld 3982 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}) → 𝑖 ∈ ℕ)) |
| 189 | 188 | impr 454 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → 𝑖 ∈ ℕ) |
| 190 | 180, 189 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐹‘𝑛)‘𝑖) ∈ ( ≤ ∩ (ℝ ×
ℝ))) |
| 191 | 190 | elin2d 4205 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐹‘𝑛)‘𝑖) ∈ (ℝ ×
ℝ)) |
| 192 | | xp2nd 8047 |
. . . . . . . . 9
⊢ (((𝐹‘𝑛)‘𝑖) ∈ (ℝ × ℝ) →
(2nd ‘((𝐹‘𝑛)‘𝑖)) ∈ ℝ) |
| 193 | 191, 192 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (2nd ‘((𝐹‘𝑛)‘𝑖)) ∈ ℝ) |
| 194 | | xp1st 8046 |
. . . . . . . . 9
⊢ (((𝐹‘𝑛)‘𝑖) ∈ (ℝ × ℝ) →
(1st ‘((𝐹‘𝑛)‘𝑖)) ∈ ℝ) |
| 195 | 191, 194 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (1st ‘((𝐹‘𝑛)‘𝑖)) ∈ ℝ) |
| 196 | 193, 195 | resubcld 11691 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ) |
| 197 | 196 | anassrs 467 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})) → ((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ) |
| 198 | 175, 197 | fsumrecl 15770 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ) |
| 199 | 98, 102, 104 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐵 / (2↑𝑛)) ∈ ℝ) |
| 200 | 94, 199 | readdcld 11290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ) |
| 201 | 93, 200 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ) |
| 202 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ∘ (𝐹‘𝑛)) = ((abs ∘ − ) ∘ (𝐹‘𝑛)) |
| 203 | | ovoliun.s |
. . . . . . . . . . . 12
⊢ 𝑆 = seq1( + , ((abs ∘
− ) ∘ (𝐹‘𝑛))) |
| 204 | 202, 203 | ovolsf 25507 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → 𝑆:ℕ⟶(0[,)+∞)) |
| 205 | 179, 204 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 𝑆:ℕ⟶(0[,)+∞)) |
| 206 | 205 | frnd 6744 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆ (0[,)+∞)) |
| 207 | | icossxr 13472 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ* |
| 208 | 206, 207 | sstrdi 3996 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆
ℝ*) |
| 209 | | supxrcl 13357 |
. . . . . . . 8
⊢ (ran
𝑆 ⊆
ℝ* → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
| 210 | 208, 209 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ*) |
| 211 | | mnfxr 11318 |
. . . . . . . . 9
⊢ -∞
∈ ℝ* |
| 212 | 211 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → -∞ ∈
ℝ*) |
| 213 | 95 | rexrd 11311 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈
ℝ*) |
| 214 | 95 | mnfltd 13166 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → -∞ < (vol*‘𝐴)) |
| 215 | | ovoliun.x1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛))) |
| 216 | 93, 215 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 𝐴 ⊆ ∪ ran
((,) ∘ (𝐹‘𝑛))) |
| 217 | 203 | ovollb 25514 |
. . . . . . . . 9
⊢ (((𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ 𝐴
⊆ ∪ ran ((,) ∘ (𝐹‘𝑛))) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |
| 218 | 179, 216,
217 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, <
)) |
| 219 | 212, 213,
210, 214, 218 | xrltletrd 13203 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → -∞ < sup(ran 𝑆, ℝ*, <
)) |
| 220 | | ovoliun.x2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < )
≤ ((vol*‘𝐴) +
(𝐵 / (2↑𝑛)))) |
| 221 | 93, 220 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) |
| 222 | | xrre 13211 |
. . . . . . 7
⊢
(((sup(ran 𝑆,
ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ) ∧ (-∞ <
sup(ran 𝑆,
ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤
((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ) |
| 223 | 210, 201,
219, 221, 222 | syl22anc 839 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ∈
ℝ) |
| 224 | | 1zzd 12648 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 1 ∈ ℤ) |
| 225 | 202 | ovolfsval 25505 |
. . . . . . . . 9
⊢ (((𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) ∧ 𝑖
∈ ℕ) → (((abs ∘ − ) ∘ (𝐹‘𝑛))‘𝑖) = ((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖)))) |
| 226 | 179, 225 | sylan 580 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((abs ∘
− ) ∘ (𝐹‘𝑛))‘𝑖) = ((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖)))) |
| 227 | 202 | ovolfsf 25506 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑛):ℕ⟶( ≤ ∩ (ℝ
× ℝ)) → ((abs ∘ − ) ∘ (𝐹‘𝑛)):ℕ⟶(0[,)+∞)) |
| 228 | 179, 227 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ((abs ∘ − ) ∘
(𝐹‘𝑛)):ℕ⟶(0[,)+∞)) |
| 229 | 228 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((abs ∘
− ) ∘ (𝐹‘𝑛))‘𝑖) ∈ (0[,)+∞)) |
| 230 | 226, 229 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → ((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ (0[,)+∞)) |
| 231 | | elrege0 13494 |
. . . . . . . . . 10
⊢
(((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ (0[,)+∞) ↔
(((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ ∧ 0 ≤
((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))))) |
| 232 | 230, 231 | sylib 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ ∧ 0 ≤
((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))))) |
| 233 | 232 | simpld 494 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → ((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℝ) |
| 234 | 232 | simprd 495 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → 0 ≤
((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖)))) |
| 235 | | supxrub 13366 |
. . . . . . . . . . . . . . 15
⊢ ((ran
𝑆 ⊆
ℝ* ∧ 𝑧
∈ ran 𝑆) → 𝑧 ≤ sup(ran 𝑆, ℝ*, <
)) |
| 236 | 208, 235 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑧 ∈ ran 𝑆) → 𝑧 ≤ sup(ran 𝑆, ℝ*, <
)) |
| 237 | 236 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ sup(ran 𝑆, ℝ*, <
)) |
| 238 | | brralrspcev 5203 |
. . . . . . . . . . . . 13
⊢ ((sup(ran
𝑆, ℝ*,
< ) ∈ ℝ ∧ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ sup(ran 𝑆, ℝ*, < )) →
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) |
| 239 | 223, 237,
238 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) |
| 240 | 205 | ffnd 6737 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 𝑆 Fn ℕ) |
| 241 | | breq1 5146 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑆‘𝑘) → (𝑧 ≤ 𝑥 ↔ (𝑆‘𝑘) ≤ 𝑥)) |
| 242 | 241 | ralrn 7108 |
. . . . . . . . . . . . . 14
⊢ (𝑆 Fn ℕ →
(∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)) |
| 243 | 240, 242 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)) |
| 244 | 243 | rexbidv 3179 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥)) |
| 245 | 239, 244 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑥) |
| 246 | 69, 203, 224, 226, 233, 234, 245 | isumsup2 15882 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 𝑆 ⇝ sup(ran 𝑆, ℝ, < )) |
| 247 | 203, 246 | eqbrtrrid 5179 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → seq1( + , ((abs ∘ − )
∘ (𝐹‘𝑛))) ⇝ sup(ran 𝑆, ℝ, <
)) |
| 248 | | climrel 15528 |
. . . . . . . . . 10
⊢ Rel
⇝ |
| 249 | 248 | releldmi 5959 |
. . . . . . . . 9
⊢ (seq1( +
, ((abs ∘ − ) ∘ (𝐹‘𝑛))) ⇝ sup(ran 𝑆, ℝ, < ) → seq1( + , ((abs
∘ − ) ∘ (𝐹‘𝑛))) ∈ dom ⇝ ) |
| 250 | 247, 249 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → seq1( + , ((abs ∘ − )
∘ (𝐹‘𝑛))) ∈ dom ⇝
) |
| 251 | 69, 224, 175, 187, 226, 233, 234, 250 | isumless 15881 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ≤ Σ𝑖 ∈ ℕ ((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖)))) |
| 252 | 69, 203, 224, 226, 233, 234, 245 | isumsup 15883 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ℕ ((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) = sup(ran 𝑆, ℝ, < )) |
| 253 | | rge0ssre 13496 |
. . . . . . . . . 10
⊢
(0[,)+∞) ⊆ ℝ |
| 254 | 206, 253 | sstrdi 3996 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆ ℝ) |
| 255 | | 1nn 12277 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ |
| 256 | 205 | fdmd 6746 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → dom 𝑆 = ℕ) |
| 257 | 255, 256 | eleqtrrid 2848 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → 1 ∈ dom 𝑆) |
| 258 | 257 | ne0d 4342 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → dom 𝑆 ≠ ∅) |
| 259 | | dm0rn0 5935 |
. . . . . . . . . . 11
⊢ (dom
𝑆 = ∅ ↔ ran
𝑆 =
∅) |
| 260 | 259 | necon3bii 2993 |
. . . . . . . . . 10
⊢ (dom
𝑆 ≠ ∅ ↔ ran
𝑆 ≠
∅) |
| 261 | 258, 260 | sylib 218 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → ran 𝑆 ≠ ∅) |
| 262 | | supxrre 13369 |
. . . . . . . . 9
⊢ ((ran
𝑆 ⊆ ℝ ∧ ran
𝑆 ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑧 ∈ ran 𝑆 𝑧 ≤ 𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran
𝑆, ℝ, <
)) |
| 263 | 254, 261,
239, 262 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) = sup(ran
𝑆, ℝ, <
)) |
| 264 | 252, 263 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ℕ ((2nd
‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) = sup(ran 𝑆, ℝ*, <
)) |
| 265 | 251, 264 | breqtrd 5169 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ≤ sup(ran 𝑆, ℝ*, <
)) |
| 266 | 198, 223,
201, 265, 221 | letrd 11418 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) |
| 267 | 92, 198, 201, 266 | fsumle 15835 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ≤ Σ𝑛 ∈ (1...𝐿)((vol*‘𝐴) + (𝐵 / (2↑𝑛)))) |
| 268 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑖 ∈ V |
| 269 | 115, 268 | op1std 8024 |
. . . . . . . . . 10
⊢ (𝑗 = 〈𝑛, 𝑖〉 → (1st ‘𝑗) = 𝑛) |
| 270 | 269 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑗 = 〈𝑛, 𝑖〉 → (𝐹‘(1st ‘𝑗)) = (𝐹‘𝑛)) |
| 271 | 115, 268 | op2ndd 8025 |
. . . . . . . . 9
⊢ (𝑗 = 〈𝑛, 𝑖〉 → (2nd ‘𝑗) = 𝑖) |
| 272 | 270, 271 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑗 = 〈𝑛, 𝑖〉 → ((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)) = ((𝐹‘𝑛)‘𝑖)) |
| 273 | 272 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑗 = 〈𝑛, 𝑖〉 → (2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) = (2nd
‘((𝐹‘𝑛)‘𝑖))) |
| 274 | 272 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑗 = 〈𝑛, 𝑖〉 → (1st ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) = (1st
‘((𝐹‘𝑛)‘𝑖))) |
| 275 | 273, 274 | oveq12d 7449 |
. . . . . 6
⊢ (𝑗 = 〈𝑛, 𝑖〉 → ((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) =
((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖)))) |
| 276 | 196 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) ∈ ℂ) |
| 277 | 275, 92, 175, 276 | fsum2d 15807 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) = Σ𝑗 ∈ ∪
𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗))))) |
| 278 | 164 | sumeq1d 15736 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ ∪
𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) = Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗))))) |
| 279 | 277, 278 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹‘𝑛)‘𝑖)) − (1st ‘((𝐹‘𝑛)‘𝑖))) = Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗))))) |
| 280 | 95 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈ ℂ) |
| 281 | 105 | recnd 11289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐵 / (2↑𝑛)) ∈ ℂ) |
| 282 | 92, 280, 281 | fsumadd 15776 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)((vol*‘𝐴) + (𝐵 / (2↑𝑛))) = (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)))) |
| 283 | 267, 279,
282 | 3brtr3d 5174 |
. . 3
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) ≤
(Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)))) |
| 284 | | 1zzd 12648 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
| 285 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
| 286 | | ovoliun.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴)) |
| 287 | 286 | fvmpt2 7027 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ∧
(vol*‘𝐴) ∈
ℝ) → (𝐺‘𝑛) = (vol*‘𝐴)) |
| 288 | 285, 94, 287 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = (vol*‘𝐴)) |
| 289 | 288, 94 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℝ) |
| 290 | 69, 284, 289 | serfre 14072 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ) |
| 291 | | ovoliun.t |
. . . . . . . . 9
⊢ 𝑇 = seq1( + , 𝐺) |
| 292 | 291 | feq1i 6727 |
. . . . . . . 8
⊢ (𝑇:ℕ⟶ℝ ↔
seq1( + , 𝐺):ℕ⟶ℝ) |
| 293 | 290, 292 | sylibr 234 |
. . . . . . 7
⊢ (𝜑 → 𝑇:ℕ⟶ℝ) |
| 294 | 293 | frnd 6744 |
. . . . . 6
⊢ (𝜑 → ran 𝑇 ⊆ ℝ) |
| 295 | | ressxr 11305 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
| 296 | 294, 295 | sstrdi 3996 |
. . . . 5
⊢ (𝜑 → ran 𝑇 ⊆
ℝ*) |
| 297 | 93, 288 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝐿)) → (𝐺‘𝑛) = (vol*‘𝐴)) |
| 298 | | 1red 11262 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
| 299 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝐽:ℕ⟶(ℕ ×
ℕ) ∧ 1 ∈ ℕ) → (𝐽‘1) ∈ (ℕ ×
ℕ)) |
| 300 | 20, 255, 299 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐽‘1) ∈ (ℕ ×
ℕ)) |
| 301 | | xp1st 8046 |
. . . . . . . . . . . 12
⊢ ((𝐽‘1) ∈ (ℕ
× ℕ) → (1st ‘(𝐽‘1)) ∈ ℕ) |
| 302 | 300, 301 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (1st
‘(𝐽‘1)) ∈
ℕ) |
| 303 | 302 | nnred 12281 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘(𝐽‘1)) ∈
ℝ) |
| 304 | 142 | zred 12722 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ ℝ) |
| 305 | 302 | nnge1d 12314 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≤ (1st
‘(𝐽‘1))) |
| 306 | | 2fveq3 6911 |
. . . . . . . . . . . 12
⊢ (𝑤 = 1 → (1st
‘(𝐽‘𝑤)) = (1st
‘(𝐽‘1))) |
| 307 | 306 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (𝑤 = 1 → ((1st
‘(𝐽‘𝑤)) ≤ 𝐿 ↔ (1st ‘(𝐽‘1)) ≤ 𝐿)) |
| 308 | | eluzfz1 13571 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈
(ℤ≥‘1) → 1 ∈ (1...𝐾)) |
| 309 | 70, 308 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈ (1...𝐾)) |
| 310 | 307, 133,
309 | rspcdva 3623 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘(𝐽‘1)) ≤
𝐿) |
| 311 | 298, 303,
304, 305, 310 | letrd 11418 |
. . . . . . . . 9
⊢ (𝜑 → 1 ≤ 𝐿) |
| 312 | | elnnz1 12643 |
. . . . . . . . 9
⊢ (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 1 ≤
𝐿)) |
| 313 | 142, 311,
312 | sylanbrc 583 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ ℕ) |
| 314 | 313, 69 | eleqtrdi 2851 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈
(ℤ≥‘1)) |
| 315 | 297, 314,
280 | fsumser 15766 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) = (seq1( + , 𝐺)‘𝐿)) |
| 316 | | seqfn 14054 |
. . . . . . . . 9
⊢ (1 ∈
ℤ → seq1( + , 𝐺)
Fn (ℤ≥‘1)) |
| 317 | 284, 316 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐺) Fn
(ℤ≥‘1)) |
| 318 | | fnfvelrn 7100 |
. . . . . . . 8
⊢ ((seq1( +
, 𝐺) Fn
(ℤ≥‘1) ∧ 𝐿 ∈ (ℤ≥‘1))
→ (seq1( + , 𝐺)‘𝐿) ∈ ran seq1( + , 𝐺)) |
| 319 | 317, 314,
318 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (seq1( + , 𝐺)‘𝐿) ∈ ran seq1( + , 𝐺)) |
| 320 | 291 | rneqi 5948 |
. . . . . . 7
⊢ ran 𝑇 = ran seq1( + , 𝐺) |
| 321 | 319, 320 | eleqtrrdi 2852 |
. . . . . 6
⊢ (𝜑 → (seq1( + , 𝐺)‘𝐿) ∈ ran 𝑇) |
| 322 | 315, 321 | eqeltrd 2841 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ran 𝑇) |
| 323 | | supxrub 13366 |
. . . . 5
⊢ ((ran
𝑇 ⊆
ℝ* ∧ Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ran 𝑇) → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) |
| 324 | 296, 322,
323 | syl2anc 584 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, <
)) |
| 325 | 98 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) |
| 326 | | geo2sum 15909 |
. . . . . 6
⊢ ((𝐿 ∈ ℕ ∧ 𝐵 ∈ ℂ) →
Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) = (𝐵 − (𝐵 / (2↑𝐿)))) |
| 327 | 313, 325,
326 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) = (𝐵 − (𝐵 / (2↑𝐿)))) |
| 328 | 313 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈
ℕ0) |
| 329 | | nnexpcl 14115 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝐿
∈ ℕ0) → (2↑𝐿) ∈ ℕ) |
| 330 | 99, 328, 329 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝐿) ∈ ℕ) |
| 331 | 330 | nnrpd 13075 |
. . . . . . . 8
⊢ (𝜑 → (2↑𝐿) ∈
ℝ+) |
| 332 | 97, 331 | rpdivcld 13094 |
. . . . . . 7
⊢ (𝜑 → (𝐵 / (2↑𝐿)) ∈
ℝ+) |
| 333 | 332 | rpge0d 13081 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐵 / (2↑𝐿))) |
| 334 | 98, 330 | nndivred 12320 |
. . . . . . 7
⊢ (𝜑 → (𝐵 / (2↑𝐿)) ∈ ℝ) |
| 335 | 98, 334 | subge02d 11855 |
. . . . . 6
⊢ (𝜑 → (0 ≤ (𝐵 / (2↑𝐿)) ↔ (𝐵 − (𝐵 / (2↑𝐿))) ≤ 𝐵)) |
| 336 | 333, 335 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝐵 − (𝐵 / (2↑𝐿))) ≤ 𝐵) |
| 337 | 327, 336 | eqbrtrd 5165 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) ≤ 𝐵) |
| 338 | 96, 106, 108, 98, 324, 337 | le2addd 11882 |
. . 3
⊢ (𝜑 → (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |
| 339 | 91, 107, 109, 283, 338 | letrd 11418 |
. 2
⊢ (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st
‘𝑗))‘(2nd ‘𝑗))) − (1st
‘((𝐹‘(1st ‘𝑗))‘(2nd
‘𝑗)))) ≤ (sup(ran
𝑇, ℝ*,
< ) + 𝐵)) |
| 340 | 85, 339 | eqbrtrrd 5167 |
1
⊢ (𝜑 → (𝑈‘𝐾) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵)) |