MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovoliunlem1 Structured version   Visualization version   GIF version

Theorem ovoliunlem1 24772
Description: Lemma for ovoliun 24775. (Contributed by Mario Carneiro, 12-Jun-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
Hypotheses
Ref Expression
ovoliun.t 𝑇 = seq1( + , 𝐺)
ovoliun.g 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))
ovoliun.a ((𝜑𝑛 ∈ ℕ) → 𝐴 ⊆ ℝ)
ovoliun.v ((𝜑𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
ovoliun.r (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
ovoliun.b (𝜑𝐵 ∈ ℝ+)
ovoliun.s 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛)))
ovoliun.u 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
ovoliun.h 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽𝑘)))‘(2nd ‘(𝐽𝑘))))
ovoliun.j (𝜑𝐽:ℕ–1-1-onto→(ℕ × ℕ))
ovoliun.f (𝜑𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
ovoliun.x1 ((𝜑𝑛 ∈ ℕ) → 𝐴 ran ((,) ∘ (𝐹𝑛)))
ovoliun.x2 ((𝜑𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))
ovoliun.k (𝜑𝐾 ∈ ℕ)
ovoliun.l1 (𝜑𝐿 ∈ ℤ)
ovoliun.l2 (𝜑 → ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽𝑤)) ≤ 𝐿)
Assertion
Ref Expression
ovoliunlem1 (𝜑 → (𝑈𝐾) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Distinct variable groups:   𝐴,𝑘   𝑘,𝑛,𝐵   𝑘,𝐹,𝑛   𝑤,𝑘,𝐽,𝑛   𝑛,𝐾,𝑤   𝑘,𝐿,𝑛,𝑤   𝑛,𝐻   𝜑,𝑘,𝑛   𝑆,𝑘   𝑘,𝐺   𝑇,𝑘   𝑛,𝐺   𝑇,𝑛
Allowed substitution hints:   𝜑(𝑤)   𝐴(𝑤,𝑛)   𝐵(𝑤)   𝑆(𝑤,𝑛)   𝑇(𝑤)   𝑈(𝑤,𝑘,𝑛)   𝐹(𝑤)   𝐺(𝑤)   𝐻(𝑤,𝑘)   𝐾(𝑘)

Proof of Theorem ovoliunlem1
Dummy variables 𝑗 𝑚 𝑥 𝑦 𝑧 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2fveq3 6830 . . . . . . . 8 (𝑗 = (𝐽𝑚) → (𝐹‘(1st𝑗)) = (𝐹‘(1st ‘(𝐽𝑚))))
2 fveq2 6825 . . . . . . . 8 (𝑗 = (𝐽𝑚) → (2nd𝑗) = (2nd ‘(𝐽𝑚)))
31, 2fveq12d 6832 . . . . . . 7 (𝑗 = (𝐽𝑚) → ((𝐹‘(1st𝑗))‘(2nd𝑗)) = ((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))
43fveq2d 6829 . . . . . 6 (𝑗 = (𝐽𝑚) → (2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) = (2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))))
53fveq2d 6829 . . . . . 6 (𝑗 = (𝐽𝑚) → (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) = (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))))
64, 5oveq12d 7355 . . . . 5 (𝑗 = (𝐽𝑚) → ((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = ((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))))
7 fzfid 13794 . . . . 5 (𝜑 → (1...𝐾) ∈ Fin)
8 ovoliun.j . . . . . . 7 (𝜑𝐽:ℕ–1-1-onto→(ℕ × ℕ))
9 f1of1 6766 . . . . . . 7 (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → 𝐽:ℕ–1-1→(ℕ × ℕ))
108, 9syl 17 . . . . . 6 (𝜑𝐽:ℕ–1-1→(ℕ × ℕ))
11 fz1ssnn 13388 . . . . . 6 (1...𝐾) ⊆ ℕ
12 f1ores 6781 . . . . . 6 ((𝐽:ℕ–1-1→(ℕ × ℕ) ∧ (1...𝐾) ⊆ ℕ) → (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾)))
1310, 11, 12sylancl 586 . . . . 5 (𝜑 → (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾)))
14 fvres 6844 . . . . . 6 (𝑚 ∈ (1...𝐾) → ((𝐽 ↾ (1...𝐾))‘𝑚) = (𝐽𝑚))
1514adantl 482 . . . . 5 ((𝜑𝑚 ∈ (1...𝐾)) → ((𝐽 ↾ (1...𝐾))‘𝑚) = (𝐽𝑚))
16 ovoliun.f . . . . . . . . . . . . 13 (𝜑𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
1716adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
18 imassrn 6010 . . . . . . . . . . . . . . 15 (𝐽 “ (1...𝐾)) ⊆ ran 𝐽
19 f1of 6767 . . . . . . . . . . . . . . . . 17 (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → 𝐽:ℕ⟶(ℕ × ℕ))
208, 19syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐽:ℕ⟶(ℕ × ℕ))
2120frnd 6659 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐽 ⊆ (ℕ × ℕ))
2218, 21sstrid 3943 . . . . . . . . . . . . . 14 (𝜑 → (𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ))
2322sselda 3932 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝑗 ∈ (ℕ × ℕ))
24 xp1st 7931 . . . . . . . . . . . . 13 (𝑗 ∈ (ℕ × ℕ) → (1st𝑗) ∈ ℕ)
2523, 24syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st𝑗) ∈ ℕ)
2617, 25ffvelcdmd 7018 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (𝐹‘(1st𝑗)) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
27 elovolmlem 24744 . . . . . . . . . . 11 ((𝐹‘(1st𝑗)) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ↔ (𝐹‘(1st𝑗)):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2826, 27sylib 217 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (𝐹‘(1st𝑗)):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
29 xp2nd 7932 . . . . . . . . . . 11 (𝑗 ∈ (ℕ × ℕ) → (2nd𝑗) ∈ ℕ)
3023, 29syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (2nd𝑗) ∈ ℕ)
3128, 30ffvelcdmd 7018 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → ((𝐹‘(1st𝑗))‘(2nd𝑗)) ∈ ( ≤ ∩ (ℝ × ℝ)))
3231elin2d 4146 . . . . . . . 8 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → ((𝐹‘(1st𝑗))‘(2nd𝑗)) ∈ (ℝ × ℝ))
33 xp2nd 7932 . . . . . . . 8 (((𝐹‘(1st𝑗))‘(2nd𝑗)) ∈ (ℝ × ℝ) → (2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) ∈ ℝ)
3432, 33syl 17 . . . . . . 7 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) ∈ ℝ)
35 xp1st 7931 . . . . . . . 8 (((𝐹‘(1st𝑗))‘(2nd𝑗)) ∈ (ℝ × ℝ) → (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) ∈ ℝ)
3632, 35syl 17 . . . . . . 7 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) ∈ ℝ)
3734, 36resubcld 11504 . . . . . 6 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → ((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) ∈ ℝ)
3837recnd 11104 . . . . 5 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → ((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) ∈ ℂ)
396, 7, 13, 15, 38fsumf1o 15534 . . . 4 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = Σ𝑚 ∈ (1...𝐾)((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))))
4016adantr 481 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
4120ffvelcdmda 7017 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐽𝑘) ∈ (ℕ × ℕ))
42 xp1st 7931 . . . . . . . . . . . 12 ((𝐽𝑘) ∈ (ℕ × ℕ) → (1st ‘(𝐽𝑘)) ∈ ℕ)
4341, 42syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐽𝑘)) ∈ ℕ)
4440, 43ffvelcdmd 7018 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽𝑘))) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
45 elovolmlem 24744 . . . . . . . . . 10 ((𝐹‘(1st ‘(𝐽𝑘))) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ↔ (𝐹‘(1st ‘(𝐽𝑘))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
4644, 45sylib 217 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽𝑘))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
47 xp2nd 7932 . . . . . . . . . 10 ((𝐽𝑘) ∈ (ℕ × ℕ) → (2nd ‘(𝐽𝑘)) ∈ ℕ)
4841, 47syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐽𝑘)) ∈ ℕ)
4946, 48ffvelcdmd 7018 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((𝐹‘(1st ‘(𝐽𝑘)))‘(2nd ‘(𝐽𝑘))) ∈ ( ≤ ∩ (ℝ × ℝ)))
50 ovoliun.h . . . . . . . 8 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽𝑘)))‘(2nd ‘(𝐽𝑘))))
5149, 50fmptd 7044 . . . . . . 7 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
52 elfznn 13386 . . . . . . 7 (𝑚 ∈ (1...𝐾) → 𝑚 ∈ ℕ)
53 eqid 2736 . . . . . . . 8 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
5453ovolfsval 24740 . . . . . . 7 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑚) = ((2nd ‘(𝐻𝑚)) − (1st ‘(𝐻𝑚))))
5551, 52, 54syl2an 596 . . . . . 6 ((𝜑𝑚 ∈ (1...𝐾)) → (((abs ∘ − ) ∘ 𝐻)‘𝑚) = ((2nd ‘(𝐻𝑚)) − (1st ‘(𝐻𝑚))))
5652adantl 482 . . . . . . . . 9 ((𝜑𝑚 ∈ (1...𝐾)) → 𝑚 ∈ ℕ)
57 2fveq3 6830 . . . . . . . . . . . 12 (𝑘 = 𝑚 → (1st ‘(𝐽𝑘)) = (1st ‘(𝐽𝑚)))
5857fveq2d 6829 . . . . . . . . . . 11 (𝑘 = 𝑚 → (𝐹‘(1st ‘(𝐽𝑘))) = (𝐹‘(1st ‘(𝐽𝑚))))
59 2fveq3 6830 . . . . . . . . . . 11 (𝑘 = 𝑚 → (2nd ‘(𝐽𝑘)) = (2nd ‘(𝐽𝑚)))
6058, 59fveq12d 6832 . . . . . . . . . 10 (𝑘 = 𝑚 → ((𝐹‘(1st ‘(𝐽𝑘)))‘(2nd ‘(𝐽𝑘))) = ((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))
61 fvex 6838 . . . . . . . . . 10 ((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))) ∈ V
6260, 50, 61fvmpt 6931 . . . . . . . . 9 (𝑚 ∈ ℕ → (𝐻𝑚) = ((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))
6356, 62syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ (1...𝐾)) → (𝐻𝑚) = ((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))
6463fveq2d 6829 . . . . . . 7 ((𝜑𝑚 ∈ (1...𝐾)) → (2nd ‘(𝐻𝑚)) = (2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))))
6563fveq2d 6829 . . . . . . 7 ((𝜑𝑚 ∈ (1...𝐾)) → (1st ‘(𝐻𝑚)) = (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))))
6664, 65oveq12d 7355 . . . . . 6 ((𝜑𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻𝑚)) − (1st ‘(𝐻𝑚))) = ((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))))
6755, 66eqtrd 2776 . . . . 5 ((𝜑𝑚 ∈ (1...𝐾)) → (((abs ∘ − ) ∘ 𝐻)‘𝑚) = ((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))))
68 ovoliun.k . . . . . 6 (𝜑𝐾 ∈ ℕ)
69 nnuz 12722 . . . . . 6 ℕ = (ℤ‘1)
7068, 69eleqtrdi 2847 . . . . 5 (𝜑𝐾 ∈ (ℤ‘1))
71 ffvelcdm 7015 . . . . . . . . . . 11 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (𝐻𝑚) ∈ ( ≤ ∩ (ℝ × ℝ)))
7251, 52, 71syl2an 596 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1...𝐾)) → (𝐻𝑚) ∈ ( ≤ ∩ (ℝ × ℝ)))
7372elin2d 4146 . . . . . . . . 9 ((𝜑𝑚 ∈ (1...𝐾)) → (𝐻𝑚) ∈ (ℝ × ℝ))
74 xp2nd 7932 . . . . . . . . 9 ((𝐻𝑚) ∈ (ℝ × ℝ) → (2nd ‘(𝐻𝑚)) ∈ ℝ)
7573, 74syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ (1...𝐾)) → (2nd ‘(𝐻𝑚)) ∈ ℝ)
76 xp1st 7931 . . . . . . . . 9 ((𝐻𝑚) ∈ (ℝ × ℝ) → (1st ‘(𝐻𝑚)) ∈ ℝ)
7773, 76syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ (1...𝐾)) → (1st ‘(𝐻𝑚)) ∈ ℝ)
7875, 77resubcld 11504 . . . . . . 7 ((𝜑𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻𝑚)) − (1st ‘(𝐻𝑚))) ∈ ℝ)
7978recnd 11104 . . . . . 6 ((𝜑𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻𝑚)) − (1st ‘(𝐻𝑚))) ∈ ℂ)
8066, 79eqeltrrd 2838 . . . . 5 ((𝜑𝑚 ∈ (1...𝐾)) → ((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))) ∈ ℂ)
8167, 70, 80fsumser 15541 . . . 4 (𝜑 → Σ𝑚 ∈ (1...𝐾)((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝐾))
8239, 81eqtrd 2776 . . 3 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝐾))
83 ovoliun.u . . . 4 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
8483fveq1i 6826 . . 3 (𝑈𝐾) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝐾)
8582, 84eqtr4di 2794 . 2 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = (𝑈𝐾))
86 f1oeng 8832 . . . . . . 7 (((1...𝐾) ∈ Fin ∧ (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾))) → (1...𝐾) ≈ (𝐽 “ (1...𝐾)))
877, 13, 86syl2anc 584 . . . . . 6 (𝜑 → (1...𝐾) ≈ (𝐽 “ (1...𝐾)))
8887ensymd 8866 . . . . 5 (𝜑 → (𝐽 “ (1...𝐾)) ≈ (1...𝐾))
89 enfii 9054 . . . . 5 (((1...𝐾) ∈ Fin ∧ (𝐽 “ (1...𝐾)) ≈ (1...𝐾)) → (𝐽 “ (1...𝐾)) ∈ Fin)
907, 88, 89syl2anc 584 . . . 4 (𝜑 → (𝐽 “ (1...𝐾)) ∈ Fin)
9190, 37fsumrecl 15545 . . 3 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) ∈ ℝ)
92 fzfid 13794 . . . . 5 (𝜑 → (1...𝐿) ∈ Fin)
93 elfznn 13386 . . . . . 6 (𝑛 ∈ (1...𝐿) → 𝑛 ∈ ℕ)
94 ovoliun.v . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
9593, 94sylan2 593 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈ ℝ)
9692, 95fsumrecl 15545 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ℝ)
97 ovoliun.b . . . . . . 7 (𝜑𝐵 ∈ ℝ+)
9897rpred 12873 . . . . . 6 (𝜑𝐵 ∈ ℝ)
99 2nn 12147 . . . . . . . 8 2 ∈ ℕ
100 nnnn0 12341 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
101 nnexpcl 13896 . . . . . . . 8 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
10299, 100, 101sylancr 587 . . . . . . 7 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
10393, 102syl 17 . . . . . 6 (𝑛 ∈ (1...𝐿) → (2↑𝑛) ∈ ℕ)
104 nndivre 12115 . . . . . 6 ((𝐵 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝐵 / (2↑𝑛)) ∈ ℝ)
10598, 103, 104syl2an 596 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐵 / (2↑𝑛)) ∈ ℝ)
10692, 105fsumrecl 15545 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) ∈ ℝ)
10796, 106readdcld 11105 . . 3 (𝜑 → (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))) ∈ ℝ)
108 ovoliun.r . . . 4 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
109108, 98readdcld 11105 . . 3 (𝜑 → (sup(ran 𝑇, ℝ*, < ) + 𝐵) ∈ ℝ)
110 relxp 5638 . . . . . . . . . . . . . . 15 Rel ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))
111 relres 5952 . . . . . . . . . . . . . . 15 Rel ((𝐽 “ (1...𝐾)) ↾ {𝑛})
112 elsni 4590 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ {𝑛} → 𝑥 = 𝑛)
113112opeq1d 4823 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑛} → ⟨𝑥, 𝑦⟩ = ⟨𝑛, 𝑦⟩)
114113eleq1d 2821 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑛} → (⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)) ↔ ⟨𝑛, 𝑦⟩ ∈ (𝐽 “ (1...𝐾))))
115 vex 3445 . . . . . . . . . . . . . . . . . . 19 𝑛 ∈ V
116 vex 3445 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
117115, 116elimasn 6027 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}) ↔ ⟨𝑛, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)))
118114, 117bitr4di 288 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑛} → (⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)) ↔ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})))
119118pm5.32i 575 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ {𝑛} ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾))) ↔ (𝑥 ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})))
120116opelresi 5931 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ((𝐽 “ (1...𝐾)) ↾ {𝑛}) ↔ (𝑥 ∈ {𝑛} ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾))))
121 opelxp 5656 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ↔ (𝑥 ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})))
122119, 120, 1213bitr4ri 303 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝐽 “ (1...𝐾)) ↾ {𝑛}))
123110, 111, 122eqrelriiv 5732 . . . . . . . . . . . . . 14 ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ↾ {𝑛})
124 df-res 5632 . . . . . . . . . . . . . 14 ((𝐽 “ (1...𝐾)) ↾ {𝑛}) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V))
125123, 124eqtri 2764 . . . . . . . . . . . . 13 ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V))
126125a1i 11 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)))
127126iuneq2dv 4965 . . . . . . . . . . 11 (𝜑 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = 𝑛 ∈ (1...𝐿)((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)))
128 iunin2 5018 . . . . . . . . . . 11 𝑛 ∈ (1...𝐿)((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)) = ((𝐽 “ (1...𝐾)) ∩ 𝑛 ∈ (1...𝐿)({𝑛} × V))
129127, 128eqtrdi 2792 . . . . . . . . . 10 (𝜑 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ 𝑛 ∈ (1...𝐿)({𝑛} × V)))
130 relxp 5638 . . . . . . . . . . . . . 14 Rel (ℕ × ℕ)
131 relss 5723 . . . . . . . . . . . . . 14 ((𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ) → (Rel (ℕ × ℕ) → Rel (𝐽 “ (1...𝐾))))
13222, 130, 131mpisyl 21 . . . . . . . . . . . . 13 (𝜑 → Rel (𝐽 “ (1...𝐾)))
133 ovoliun.l2 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽𝑤)) ≤ 𝐿)
13420ffnd 6652 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽 Fn ℕ)
135 fveq2 6825 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝐽𝑤) → (1st𝑗) = (1st ‘(𝐽𝑤)))
136135breq1d 5102 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝐽𝑤) → ((1st𝑗) ≤ 𝐿 ↔ (1st ‘(𝐽𝑤)) ≤ 𝐿))
137136ralima 7170 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 Fn ℕ ∧ (1...𝐾) ⊆ ℕ) → (∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st𝑗) ≤ 𝐿 ↔ ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽𝑤)) ≤ 𝐿))
138134, 11, 137sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st𝑗) ≤ 𝐿 ↔ ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽𝑤)) ≤ 𝐿))
139133, 138mpbird 256 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st𝑗) ≤ 𝐿)
140139r19.21bi 3230 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st𝑗) ≤ 𝐿)
14125, 69eleqtrdi 2847 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st𝑗) ∈ (ℤ‘1))
142 ovoliun.l1 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐿 ∈ ℤ)
143142adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝐿 ∈ ℤ)
144 elfz5 13349 . . . . . . . . . . . . . . . . . 18 (((1st𝑗) ∈ (ℤ‘1) ∧ 𝐿 ∈ ℤ) → ((1st𝑗) ∈ (1...𝐿) ↔ (1st𝑗) ≤ 𝐿))
145141, 143, 144syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → ((1st𝑗) ∈ (1...𝐿) ↔ (1st𝑗) ≤ 𝐿))
146140, 145mpbird 256 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st𝑗) ∈ (1...𝐿))
147146ralrimiva 3139 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st𝑗) ∈ (1...𝐿))
148 vex 3445 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
149148, 116op1std 7909 . . . . . . . . . . . . . . . . 17 (𝑗 = ⟨𝑥, 𝑦⟩ → (1st𝑗) = 𝑥)
150149eleq1d 2821 . . . . . . . . . . . . . . . 16 (𝑗 = ⟨𝑥, 𝑦⟩ → ((1st𝑗) ∈ (1...𝐿) ↔ 𝑥 ∈ (1...𝐿)))
151150rspccv 3567 . . . . . . . . . . . . . . 15 (∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st𝑗) ∈ (1...𝐿) → (⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)) → 𝑥 ∈ (1...𝐿)))
152147, 151syl 17 . . . . . . . . . . . . . 14 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)) → 𝑥 ∈ (1...𝐿)))
153 opelxp 5656 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ( 𝑛 ∈ (1...𝐿){𝑛} × V) ↔ (𝑥 𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V))
154116biantru 530 . . . . . . . . . . . . . . 15 (𝑥 𝑛 ∈ (1...𝐿){𝑛} ↔ (𝑥 𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V))
155 iunid 5007 . . . . . . . . . . . . . . . 16 𝑛 ∈ (1...𝐿){𝑛} = (1...𝐿)
156155eleq2i 2828 . . . . . . . . . . . . . . 15 (𝑥 𝑛 ∈ (1...𝐿){𝑛} ↔ 𝑥 ∈ (1...𝐿))
157153, 154, 1563bitr2i 298 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ ( 𝑛 ∈ (1...𝐿){𝑛} × V) ↔ 𝑥 ∈ (1...𝐿))
158152, 157syl6ibr 251 . . . . . . . . . . . . 13 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)) → ⟨𝑥, 𝑦⟩ ∈ ( 𝑛 ∈ (1...𝐿){𝑛} × V)))
159132, 158relssdv 5730 . . . . . . . . . . . 12 (𝜑 → (𝐽 “ (1...𝐾)) ⊆ ( 𝑛 ∈ (1...𝐿){𝑛} × V))
160 xpiundir 5689 . . . . . . . . . . . 12 ( 𝑛 ∈ (1...𝐿){𝑛} × V) = 𝑛 ∈ (1...𝐿)({𝑛} × V)
161159, 160sseqtrdi 3982 . . . . . . . . . . 11 (𝜑 → (𝐽 “ (1...𝐾)) ⊆ 𝑛 ∈ (1...𝐿)({𝑛} × V))
162 df-ss 3915 . . . . . . . . . . 11 ((𝐽 “ (1...𝐾)) ⊆ 𝑛 ∈ (1...𝐿)({𝑛} × V) ↔ ((𝐽 “ (1...𝐾)) ∩ 𝑛 ∈ (1...𝐿)({𝑛} × V)) = (𝐽 “ (1...𝐾)))
163161, 162sylib 217 . . . . . . . . . 10 (𝜑 → ((𝐽 “ (1...𝐾)) ∩ 𝑛 ∈ (1...𝐿)({𝑛} × V)) = (𝐽 “ (1...𝐾)))
164129, 163eqtrd 2776 . . . . . . . . 9 (𝜑 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = (𝐽 “ (1...𝐾)))
165164, 90eqeltrd 2837 . . . . . . . 8 (𝜑 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin)
166 ssiun2 4994 . . . . . . . 8 (𝑛 ∈ (1...𝐿) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ⊆ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})))
167 ssfi 9038 . . . . . . . 8 (( 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ⊆ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin)
168165, 166, 167syl2an 596 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin)
169 2ndconst 8009 . . . . . . . . . 10 (𝑛 ∈ V → (2nd ↾ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛}))
170169elv 3447 . . . . . . . . 9 (2nd ↾ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛})
171 f1oeng 8832 . . . . . . . . 9 ((({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ (2nd ↾ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛})) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ≈ ((𝐽 “ (1...𝐾)) “ {𝑛}))
172168, 170, 171sylancl 586 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ≈ ((𝐽 “ (1...𝐾)) “ {𝑛}))
173172ensymd 8866 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ≈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})))
174 enfii 9054 . . . . . . 7 ((({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ ((𝐽 “ (1...𝐾)) “ {𝑛}) ≈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ∈ Fin)
175168, 173, 174syl2anc 584 . . . . . 6 ((𝜑𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ∈ Fin)
176 ffvelcdm 7015 . . . . . . . . . . . . . 14 ((𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
17716, 93, 176syl2an 596 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐹𝑛) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
178 elovolmlem 24744 . . . . . . . . . . . . 13 ((𝐹𝑛) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ↔ (𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
179177, 178sylib 217 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
180179adantrr 714 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
181 imassrn 6010 . . . . . . . . . . . . . 14 ((𝐽 “ (1...𝐾)) “ {𝑛}) ⊆ ran (𝐽 “ (1...𝐾))
18222adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ))
183 rnss 5880 . . . . . . . . . . . . . . . 16 ((𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ) → ran (𝐽 “ (1...𝐾)) ⊆ ran (ℕ × ℕ))
184182, 183syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝐿)) → ran (𝐽 “ (1...𝐾)) ⊆ ran (ℕ × ℕ))
185 rnxpid 6111 . . . . . . . . . . . . . . 15 ran (ℕ × ℕ) = ℕ
186184, 185sseqtrdi 3982 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝐿)) → ran (𝐽 “ (1...𝐾)) ⊆ ℕ)
187181, 186sstrid 3943 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ⊆ ℕ)
188187sseld 3931 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → (𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}) → 𝑖 ∈ ℕ))
189188impr 455 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → 𝑖 ∈ ℕ)
190180, 189ffvelcdmd 7018 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐹𝑛)‘𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
191190elin2d 4146 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐹𝑛)‘𝑖) ∈ (ℝ × ℝ))
192 xp2nd 7932 . . . . . . . . 9 (((𝐹𝑛)‘𝑖) ∈ (ℝ × ℝ) → (2nd ‘((𝐹𝑛)‘𝑖)) ∈ ℝ)
193191, 192syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (2nd ‘((𝐹𝑛)‘𝑖)) ∈ ℝ)
194 xp1st 7931 . . . . . . . . 9 (((𝐹𝑛)‘𝑖) ∈ (ℝ × ℝ) → (1st ‘((𝐹𝑛)‘𝑖)) ∈ ℝ)
195191, 194syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (1st ‘((𝐹𝑛)‘𝑖)) ∈ ℝ)
196193, 195resubcld 11504 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ)
197196anassrs 468 . . . . . 6 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})) → ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ)
198175, 197fsumrecl 15545 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ)
19998, 102, 104syl2an 596 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐵 / (2↑𝑛)) ∈ ℝ)
20094, 199readdcld 11105 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ)
20193, 200sylan2 593 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ)
202 eqid 2736 . . . . . . . . . . . 12 ((abs ∘ − ) ∘ (𝐹𝑛)) = ((abs ∘ − ) ∘ (𝐹𝑛))
203 ovoliun.s . . . . . . . . . . . 12 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛)))
204202, 203ovolsf 24742 . . . . . . . . . . 11 ((𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
205179, 204syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝐿)) → 𝑆:ℕ⟶(0[,)+∞))
206205frnd 6659 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆ (0[,)+∞))
207 icossxr 13265 . . . . . . . . 9 (0[,)+∞) ⊆ ℝ*
208206, 207sstrdi 3944 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆ ℝ*)
209 supxrcl 13150 . . . . . . . 8 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
210208, 209syl 17 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
211 mnfxr 11133 . . . . . . . . 9 -∞ ∈ ℝ*
212211a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → -∞ ∈ ℝ*)
21395rexrd 11126 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈ ℝ*)
21495mnfltd 12961 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → -∞ < (vol*‘𝐴))
215 ovoliun.x1 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝐴 ran ((,) ∘ (𝐹𝑛)))
21693, 215sylan2 593 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝐿)) → 𝐴 ran ((,) ∘ (𝐹𝑛)))
217203ovollb 24749 . . . . . . . . 9 (((𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ran ((,) ∘ (𝐹𝑛))) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
218179, 216, 217syl2anc 584 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
219212, 213, 210, 214, 218xrltletrd 12996 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → -∞ < sup(ran 𝑆, ℝ*, < ))
220 ovoliun.x2 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))
22193, 220sylan2 593 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))
222 xrre 13004 . . . . . . 7 (((sup(ran 𝑆, ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
223210, 201, 219, 221, 222syl22anc 836 . . . . . 6 ((𝜑𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
224 1zzd 12452 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → 1 ∈ ℤ)
225202ovolfsval 24740 . . . . . . . . 9 (((𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((abs ∘ − ) ∘ (𝐹𝑛))‘𝑖) = ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))))
226179, 225sylan 580 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((abs ∘ − ) ∘ (𝐹𝑛))‘𝑖) = ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))))
227202ovolfsf 24741 . . . . . . . . . . . . 13 ((𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ (𝐹𝑛)):ℕ⟶(0[,)+∞))
228179, 227syl 17 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → ((abs ∘ − ) ∘ (𝐹𝑛)):ℕ⟶(0[,)+∞))
229228ffvelcdmda 7017 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((abs ∘ − ) ∘ (𝐹𝑛))‘𝑖) ∈ (0[,)+∞))
230226, 229eqeltrrd 2838 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ (0[,)+∞))
231 elrege0 13287 . . . . . . . . . 10 (((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ (0[,)+∞) ↔ (((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ ∧ 0 ≤ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖)))))
232230, 231sylib 217 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ ∧ 0 ≤ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖)))))
233232simpld 495 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ)
234232simprd 496 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → 0 ≤ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))))
235 supxrub 13159 . . . . . . . . . . . . . . 15 ((ran 𝑆 ⊆ ℝ*𝑧 ∈ ran 𝑆) → 𝑧 ≤ sup(ran 𝑆, ℝ*, < ))
236208, 235sylan 580 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑧 ∈ ran 𝑆) → 𝑧 ≤ sup(ran 𝑆, ℝ*, < ))
237236ralrimiva 3139 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝐿)) → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ sup(ran 𝑆, ℝ*, < ))
238 brralrspcev 5152 . . . . . . . . . . . . 13 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥)
239223, 237, 238syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥)
240205ffnd 6652 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝐿)) → 𝑆 Fn ℕ)
241 breq1 5095 . . . . . . . . . . . . . . 15 (𝑧 = (𝑆𝑘) → (𝑧𝑥 ↔ (𝑆𝑘) ≤ 𝑥))
242241ralrn 7020 . . . . . . . . . . . . . 14 (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
243240, 242syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝐿)) → (∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
244243rexbidv 3171 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
245239, 244mpbid 231 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝐿)) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥)
24669, 203, 224, 226, 233, 234, 245isumsup2 15657 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝐿)) → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
247203, 246eqbrtrrid 5128 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝐿)) → seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛))) ⇝ sup(ran 𝑆, ℝ, < ))
248 climrel 15300 . . . . . . . . . 10 Rel ⇝
249248releldmi 5889 . . . . . . . . 9 (seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛))) ⇝ sup(ran 𝑆, ℝ, < ) → seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛))) ∈ dom ⇝ )
250247, 249syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛))) ∈ dom ⇝ )
25169, 224, 175, 187, 226, 233, 234, 250isumless 15656 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ≤ Σ𝑖 ∈ ℕ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))))
25269, 203, 224, 226, 233, 234, 245isumsup 15658 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ℕ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) = sup(ran 𝑆, ℝ, < ))
253 rge0ssre 13289 . . . . . . . . . 10 (0[,)+∞) ⊆ ℝ
254206, 253sstrdi 3944 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆ ℝ)
255 1nn 12085 . . . . . . . . . . . 12 1 ∈ ℕ
256205fdmd 6662 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → dom 𝑆 = ℕ)
257255, 256eleqtrrid 2844 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝐿)) → 1 ∈ dom 𝑆)
258257ne0d 4282 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝐿)) → dom 𝑆 ≠ ∅)
259 dm0rn0 5866 . . . . . . . . . . 11 (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
260259necon3bii 2993 . . . . . . . . . 10 (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
261258, 260sylib 217 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝐿)) → ran 𝑆 ≠ ∅)
262 supxrre 13162 . . . . . . . . 9 ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
263254, 261, 239, 262syl3anc 1370 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
264252, 263eqtr4d 2779 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ℕ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) = sup(ran 𝑆, ℝ*, < ))
265251, 264breqtrd 5118 . . . . . 6 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ≤ sup(ran 𝑆, ℝ*, < ))
266198, 223, 201, 265, 221letrd 11233 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))
26792, 198, 201, 266fsumle 15610 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ≤ Σ𝑛 ∈ (1...𝐿)((vol*‘𝐴) + (𝐵 / (2↑𝑛))))
268 vex 3445 . . . . . . . . . . 11 𝑖 ∈ V
269115, 268op1std 7909 . . . . . . . . . 10 (𝑗 = ⟨𝑛, 𝑖⟩ → (1st𝑗) = 𝑛)
270269fveq2d 6829 . . . . . . . . 9 (𝑗 = ⟨𝑛, 𝑖⟩ → (𝐹‘(1st𝑗)) = (𝐹𝑛))
271115, 268op2ndd 7910 . . . . . . . . 9 (𝑗 = ⟨𝑛, 𝑖⟩ → (2nd𝑗) = 𝑖)
272270, 271fveq12d 6832 . . . . . . . 8 (𝑗 = ⟨𝑛, 𝑖⟩ → ((𝐹‘(1st𝑗))‘(2nd𝑗)) = ((𝐹𝑛)‘𝑖))
273272fveq2d 6829 . . . . . . 7 (𝑗 = ⟨𝑛, 𝑖⟩ → (2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) = (2nd ‘((𝐹𝑛)‘𝑖)))
274272fveq2d 6829 . . . . . . 7 (𝑗 = ⟨𝑛, 𝑖⟩ → (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) = (1st ‘((𝐹𝑛)‘𝑖)))
275273, 274oveq12d 7355 . . . . . 6 (𝑗 = ⟨𝑛, 𝑖⟩ → ((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))))
276196recnd 11104 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℂ)
277275, 92, 175, 276fsum2d 15582 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...𝐿𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) = Σ𝑗 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))))
278164sumeq1d 15512 . . . . 5 (𝜑 → Σ𝑗 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))))
279277, 278eqtrd 2776 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) = Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))))
28095recnd 11104 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈ ℂ)
281105recnd 11104 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐵 / (2↑𝑛)) ∈ ℂ)
28292, 280, 281fsumadd 15551 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿)((vol*‘𝐴) + (𝐵 / (2↑𝑛))) = (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))))
283267, 279, 2823brtr3d 5123 . . 3 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) ≤ (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))))
284 1zzd 12452 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
285 simpr 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
286 ovoliun.g . . . . . . . . . . . 12 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))
287286fvmpt2 6942 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (vol*‘𝐴) ∈ ℝ) → (𝐺𝑛) = (vol*‘𝐴))
288285, 94, 287syl2anc 584 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = (vol*‘𝐴))
289288, 94eqeltrd 2837 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ ℝ)
29069, 284, 289serfre 13853 . . . . . . . 8 (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ)
291 ovoliun.t . . . . . . . . 9 𝑇 = seq1( + , 𝐺)
292291feq1i 6642 . . . . . . . 8 (𝑇:ℕ⟶ℝ ↔ seq1( + , 𝐺):ℕ⟶ℝ)
293290, 292sylibr 233 . . . . . . 7 (𝜑𝑇:ℕ⟶ℝ)
294293frnd 6659 . . . . . 6 (𝜑 → ran 𝑇 ⊆ ℝ)
295 ressxr 11120 . . . . . 6 ℝ ⊆ ℝ*
296294, 295sstrdi 3944 . . . . 5 (𝜑 → ran 𝑇 ⊆ ℝ*)
29793, 288sylan2 593 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐺𝑛) = (vol*‘𝐴))
298 1red 11077 . . . . . . . . . 10 (𝜑 → 1 ∈ ℝ)
299 ffvelcdm 7015 . . . . . . . . . . . . 13 ((𝐽:ℕ⟶(ℕ × ℕ) ∧ 1 ∈ ℕ) → (𝐽‘1) ∈ (ℕ × ℕ))
30020, 255, 299sylancl 586 . . . . . . . . . . . 12 (𝜑 → (𝐽‘1) ∈ (ℕ × ℕ))
301 xp1st 7931 . . . . . . . . . . . 12 ((𝐽‘1) ∈ (ℕ × ℕ) → (1st ‘(𝐽‘1)) ∈ ℕ)
302300, 301syl 17 . . . . . . . . . . 11 (𝜑 → (1st ‘(𝐽‘1)) ∈ ℕ)
303302nnred 12089 . . . . . . . . . 10 (𝜑 → (1st ‘(𝐽‘1)) ∈ ℝ)
304142zred 12527 . . . . . . . . . 10 (𝜑𝐿 ∈ ℝ)
305302nnge1d 12122 . . . . . . . . . 10 (𝜑 → 1 ≤ (1st ‘(𝐽‘1)))
306 2fveq3 6830 . . . . . . . . . . . 12 (𝑤 = 1 → (1st ‘(𝐽𝑤)) = (1st ‘(𝐽‘1)))
307306breq1d 5102 . . . . . . . . . . 11 (𝑤 = 1 → ((1st ‘(𝐽𝑤)) ≤ 𝐿 ↔ (1st ‘(𝐽‘1)) ≤ 𝐿))
308 eluzfz1 13364 . . . . . . . . . . . 12 (𝐾 ∈ (ℤ‘1) → 1 ∈ (1...𝐾))
30970, 308syl 17 . . . . . . . . . . 11 (𝜑 → 1 ∈ (1...𝐾))
310307, 133, 309rspcdva 3571 . . . . . . . . . 10 (𝜑 → (1st ‘(𝐽‘1)) ≤ 𝐿)
311298, 303, 304, 305, 310letrd 11233 . . . . . . . . 9 (𝜑 → 1 ≤ 𝐿)
312 elnnz1 12447 . . . . . . . . 9 (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 1 ≤ 𝐿))
313142, 311, 312sylanbrc 583 . . . . . . . 8 (𝜑𝐿 ∈ ℕ)
314313, 69eleqtrdi 2847 . . . . . . 7 (𝜑𝐿 ∈ (ℤ‘1))
315297, 314, 280fsumser 15541 . . . . . 6 (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) = (seq1( + , 𝐺)‘𝐿))
316 seqfn 13834 . . . . . . . . 9 (1 ∈ ℤ → seq1( + , 𝐺) Fn (ℤ‘1))
317284, 316syl 17 . . . . . . . 8 (𝜑 → seq1( + , 𝐺) Fn (ℤ‘1))
318 fnfvelrn 7014 . . . . . . . 8 ((seq1( + , 𝐺) Fn (ℤ‘1) ∧ 𝐿 ∈ (ℤ‘1)) → (seq1( + , 𝐺)‘𝐿) ∈ ran seq1( + , 𝐺))
319317, 314, 318syl2anc 584 . . . . . . 7 (𝜑 → (seq1( + , 𝐺)‘𝐿) ∈ ran seq1( + , 𝐺))
320291rneqi 5878 . . . . . . 7 ran 𝑇 = ran seq1( + , 𝐺)
321319, 320eleqtrrdi 2848 . . . . . 6 (𝜑 → (seq1( + , 𝐺)‘𝐿) ∈ ran 𝑇)
322315, 321eqeltrd 2837 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ran 𝑇)
323 supxrub 13159 . . . . 5 ((ran 𝑇 ⊆ ℝ* ∧ Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ran 𝑇) → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
324296, 322, 323syl2anc 584 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
32598recnd 11104 . . . . . 6 (𝜑𝐵 ∈ ℂ)
326 geo2sum 15684 . . . . . 6 ((𝐿 ∈ ℕ ∧ 𝐵 ∈ ℂ) → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) = (𝐵 − (𝐵 / (2↑𝐿))))
327313, 325, 326syl2anc 584 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) = (𝐵 − (𝐵 / (2↑𝐿))))
328313nnnn0d 12394 . . . . . . . . . 10 (𝜑𝐿 ∈ ℕ0)
329 nnexpcl 13896 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝐿 ∈ ℕ0) → (2↑𝐿) ∈ ℕ)
33099, 328, 329sylancr 587 . . . . . . . . 9 (𝜑 → (2↑𝐿) ∈ ℕ)
331330nnrpd 12871 . . . . . . . 8 (𝜑 → (2↑𝐿) ∈ ℝ+)
33297, 331rpdivcld 12890 . . . . . . 7 (𝜑 → (𝐵 / (2↑𝐿)) ∈ ℝ+)
333332rpge0d 12877 . . . . . 6 (𝜑 → 0 ≤ (𝐵 / (2↑𝐿)))
33498, 330nndivred 12128 . . . . . . 7 (𝜑 → (𝐵 / (2↑𝐿)) ∈ ℝ)
33598, 334subge02d 11668 . . . . . 6 (𝜑 → (0 ≤ (𝐵 / (2↑𝐿)) ↔ (𝐵 − (𝐵 / (2↑𝐿))) ≤ 𝐵))
336333, 335mpbid 231 . . . . 5 (𝜑 → (𝐵 − (𝐵 / (2↑𝐿))) ≤ 𝐵)
337327, 336eqbrtrd 5114 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) ≤ 𝐵)
33896, 106, 108, 98, 324, 337le2addd 11695 . . 3 (𝜑 → (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
33991, 107, 109, 283, 338letrd 11233 . 2 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
34085, 339eqbrtrrd 5116 1 (𝜑 → (𝑈𝐾) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wne 2940  wral 3061  wrex 3070  Vcvv 3441  cin 3897  wss 3898  c0 4269  {csn 4573  cop 4579   cuni 4852   ciun 4941   class class class wbr 5092  cmpt 5175   × cxp 5618  dom cdm 5620  ran crn 5621  cres 5622  cima 5623  ccom 5624  Rel wrel 5625   Fn wfn 6474  wf 6475  1-1wf1 6476  1-1-ontowf1o 6478  cfv 6479  (class class class)co 7337  1st c1st 7897  2nd c2nd 7898  m cmap 8686  cen 8801  Fincfn 8804  supcsup 9297  cc 10970  cr 10971  0cc0 10972  1c1 10973   + caddc 10975  +∞cpnf 11107  -∞cmnf 11108  *cxr 11109   < clt 11110  cle 11111  cmin 11306   / cdiv 11733  cn 12074  2c2 12129  0cn0 12334  cz 12420  cuz 12683  +crp 12831  (,)cioo 13180  [,)cico 13182  ...cfz 13340  seqcseq 13822  cexp 13883  abscabs 15044  cli 15292  Σcsu 15496  vol*covol 24732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-om 7781  df-1st 7899  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-er 8569  df-map 8688  df-pm 8689  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-sup 9299  df-inf 9300  df-oi 9367  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-n0 12335  df-z 12421  df-uz 12684  df-rp 12832  df-ioo 13184  df-ico 13186  df-fz 13341  df-fzo 13484  df-fl 13613  df-seq 13823  df-exp 13884  df-hash 14146  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-clim 15296  df-rlim 15297  df-sum 15497  df-ovol 24734
This theorem is referenced by:  ovoliunlem2  24773
  Copyright terms: Public domain W3C validator