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

Theorem ovoliunlem1 25550
Description: Lemma for ovoliun 25553. (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 6911 . . . . . . . 8 (𝑗 = (𝐽𝑚) → (𝐹‘(1st𝑗)) = (𝐹‘(1st ‘(𝐽𝑚))))
2 fveq2 6906 . . . . . . . 8 (𝑗 = (𝐽𝑚) → (2nd𝑗) = (2nd ‘(𝐽𝑚)))
31, 2fveq12d 6913 . . . . . . 7 (𝑗 = (𝐽𝑚) → ((𝐹‘(1st𝑗))‘(2nd𝑗)) = ((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))
43fveq2d 6910 . . . . . 6 (𝑗 = (𝐽𝑚) → (2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) = (2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))))
53fveq2d 6910 . . . . . 6 (𝑗 = (𝐽𝑚) → (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) = (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))))
64, 5oveq12d 7448 . . . . 5 (𝑗 = (𝐽𝑚) → ((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = ((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))))
7 fzfid 14010 . . . . 5 (𝜑 → (1...𝐾) ∈ Fin)
8 ovoliun.j . . . . . . 7 (𝜑𝐽:ℕ–1-1-onto→(ℕ × ℕ))
9 f1of1 6847 . . . . . . 7 (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → 𝐽:ℕ–1-1→(ℕ × ℕ))
108, 9syl 17 . . . . . 6 (𝜑𝐽:ℕ–1-1→(ℕ × ℕ))
11 fz1ssnn 13591 . . . . . 6 (1...𝐾) ⊆ ℕ
12 f1ores 6862 . . . . . 6 ((𝐽:ℕ–1-1→(ℕ × ℕ) ∧ (1...𝐾) ⊆ ℕ) → (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾)))
1310, 11, 12sylancl 586 . . . . 5 (𝜑 → (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾)))
14 fvres 6925 . . . . . 6 (𝑚 ∈ (1...𝐾) → ((𝐽 ↾ (1...𝐾))‘𝑚) = (𝐽𝑚))
1514adantl 481 . . . . 5 ((𝜑𝑚 ∈ (1...𝐾)) → ((𝐽 ↾ (1...𝐾))‘𝑚) = (𝐽𝑚))
16 ovoliun.f . . . . . . . . . . . . 13 (𝜑𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
1716adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
18 imassrn 6090 . . . . . . . . . . . . . . 15 (𝐽 “ (1...𝐾)) ⊆ ran 𝐽
19 f1of 6848 . . . . . . . . . . . . . . . . 17 (𝐽:ℕ–1-1-onto→(ℕ × ℕ) → 𝐽:ℕ⟶(ℕ × ℕ))
208, 19syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐽:ℕ⟶(ℕ × ℕ))
2120frnd 6744 . . . . . . . . . . . . . . 15 (𝜑 → ran 𝐽 ⊆ (ℕ × ℕ))
2218, 21sstrid 4006 . . . . . . . . . . . . . 14 (𝜑 → (𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ))
2322sselda 3994 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝑗 ∈ (ℕ × ℕ))
24 xp1st 8044 . . . . . . . . . . . . 13 (𝑗 ∈ (ℕ × ℕ) → (1st𝑗) ∈ ℕ)
2523, 24syl 17 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st𝑗) ∈ ℕ)
2617, 25ffvelcdmd 7104 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (𝐹‘(1st𝑗)) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
27 elovolmlem 25522 . . . . . . . . . . 11 ((𝐹‘(1st𝑗)) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ↔ (𝐹‘(1st𝑗)):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
2826, 27sylib 218 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (𝐹‘(1st𝑗)):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
29 xp2nd 8045 . . . . . . . . . . 11 (𝑗 ∈ (ℕ × ℕ) → (2nd𝑗) ∈ ℕ)
3023, 29syl 17 . . . . . . . . . 10 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (2nd𝑗) ∈ ℕ)
3128, 30ffvelcdmd 7104 . . . . . . . . 9 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → ((𝐹‘(1st𝑗))‘(2nd𝑗)) ∈ ( ≤ ∩ (ℝ × ℝ)))
3231elin2d 4214 . . . . . . . 8 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → ((𝐹‘(1st𝑗))‘(2nd𝑗)) ∈ (ℝ × ℝ))
33 xp2nd 8045 . . . . . . . 8 (((𝐹‘(1st𝑗))‘(2nd𝑗)) ∈ (ℝ × ℝ) → (2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) ∈ ℝ)
3432, 33syl 17 . . . . . . 7 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) ∈ ℝ)
35 xp1st 8044 . . . . . . . 8 (((𝐹‘(1st𝑗))‘(2nd𝑗)) ∈ (ℝ × ℝ) → (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) ∈ ℝ)
3632, 35syl 17 . . . . . . 7 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) ∈ ℝ)
3734, 36resubcld 11688 . . . . . 6 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → ((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) ∈ ℝ)
3837recnd 11286 . . . . 5 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → ((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) ∈ ℂ)
396, 7, 13, 15, 38fsumf1o 15755 . . . 4 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = Σ𝑚 ∈ (1...𝐾)((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))))
4016adantr 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → 𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
4120ffvelcdmda 7103 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐽𝑘) ∈ (ℕ × ℕ))
42 xp1st 8044 . . . . . . . . . . . 12 ((𝐽𝑘) ∈ (ℕ × ℕ) → (1st ‘(𝐽𝑘)) ∈ ℕ)
4341, 42syl 17 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ℕ) → (1st ‘(𝐽𝑘)) ∈ ℕ)
4440, 43ffvelcdmd 7104 . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽𝑘))) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
45 elovolmlem 25522 . . . . . . . . . 10 ((𝐹‘(1st ‘(𝐽𝑘))) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ↔ (𝐹‘(1st ‘(𝐽𝑘))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
4644, 45sylib 218 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐹‘(1st ‘(𝐽𝑘))):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
47 xp2nd 8045 . . . . . . . . . 10 ((𝐽𝑘) ∈ (ℕ × ℕ) → (2nd ‘(𝐽𝑘)) ∈ ℕ)
4841, 47syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (2nd ‘(𝐽𝑘)) ∈ ℕ)
4946, 48ffvelcdmd 7104 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → ((𝐹‘(1st ‘(𝐽𝑘)))‘(2nd ‘(𝐽𝑘))) ∈ ( ≤ ∩ (ℝ × ℝ)))
50 ovoliun.h . . . . . . . 8 𝐻 = (𝑘 ∈ ℕ ↦ ((𝐹‘(1st ‘(𝐽𝑘)))‘(2nd ‘(𝐽𝑘))))
5149, 50fmptd 7133 . . . . . . 7 (𝜑𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)))
52 elfznn 13589 . . . . . . 7 (𝑚 ∈ (1...𝐾) → 𝑚 ∈ ℕ)
53 eqid 2734 . . . . . . . 8 ((abs ∘ − ) ∘ 𝐻) = ((abs ∘ − ) ∘ 𝐻)
5453ovolfsval 25518 . . . . . . 7 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (((abs ∘ − ) ∘ 𝐻)‘𝑚) = ((2nd ‘(𝐻𝑚)) − (1st ‘(𝐻𝑚))))
5551, 52, 54syl2an 596 . . . . . 6 ((𝜑𝑚 ∈ (1...𝐾)) → (((abs ∘ − ) ∘ 𝐻)‘𝑚) = ((2nd ‘(𝐻𝑚)) − (1st ‘(𝐻𝑚))))
5652adantl 481 . . . . . . . . 9 ((𝜑𝑚 ∈ (1...𝐾)) → 𝑚 ∈ ℕ)
57 2fveq3 6911 . . . . . . . . . . . 12 (𝑘 = 𝑚 → (1st ‘(𝐽𝑘)) = (1st ‘(𝐽𝑚)))
5857fveq2d 6910 . . . . . . . . . . 11 (𝑘 = 𝑚 → (𝐹‘(1st ‘(𝐽𝑘))) = (𝐹‘(1st ‘(𝐽𝑚))))
59 2fveq3 6911 . . . . . . . . . . 11 (𝑘 = 𝑚 → (2nd ‘(𝐽𝑘)) = (2nd ‘(𝐽𝑚)))
6058, 59fveq12d 6913 . . . . . . . . . 10 (𝑘 = 𝑚 → ((𝐹‘(1st ‘(𝐽𝑘)))‘(2nd ‘(𝐽𝑘))) = ((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))
61 fvex 6919 . . . . . . . . . 10 ((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))) ∈ V
6260, 50, 61fvmpt 7015 . . . . . . . . 9 (𝑚 ∈ ℕ → (𝐻𝑚) = ((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))
6356, 62syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ (1...𝐾)) → (𝐻𝑚) = ((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))
6463fveq2d 6910 . . . . . . 7 ((𝜑𝑚 ∈ (1...𝐾)) → (2nd ‘(𝐻𝑚)) = (2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))))
6563fveq2d 6910 . . . . . . 7 ((𝜑𝑚 ∈ (1...𝐾)) → (1st ‘(𝐻𝑚)) = (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))))
6664, 65oveq12d 7448 . . . . . 6 ((𝜑𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻𝑚)) − (1st ‘(𝐻𝑚))) = ((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))))
6755, 66eqtrd 2774 . . . . 5 ((𝜑𝑚 ∈ (1...𝐾)) → (((abs ∘ − ) ∘ 𝐻)‘𝑚) = ((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))))
68 ovoliun.k . . . . . 6 (𝜑𝐾 ∈ ℕ)
69 nnuz 12918 . . . . . 6 ℕ = (ℤ‘1)
7068, 69eleqtrdi 2848 . . . . 5 (𝜑𝐾 ∈ (ℤ‘1))
71 ffvelcdm 7100 . . . . . . . . . . 11 ((𝐻:ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑚 ∈ ℕ) → (𝐻𝑚) ∈ ( ≤ ∩ (ℝ × ℝ)))
7251, 52, 71syl2an 596 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1...𝐾)) → (𝐻𝑚) ∈ ( ≤ ∩ (ℝ × ℝ)))
7372elin2d 4214 . . . . . . . . 9 ((𝜑𝑚 ∈ (1...𝐾)) → (𝐻𝑚) ∈ (ℝ × ℝ))
74 xp2nd 8045 . . . . . . . . 9 ((𝐻𝑚) ∈ (ℝ × ℝ) → (2nd ‘(𝐻𝑚)) ∈ ℝ)
7573, 74syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ (1...𝐾)) → (2nd ‘(𝐻𝑚)) ∈ ℝ)
76 xp1st 8044 . . . . . . . . 9 ((𝐻𝑚) ∈ (ℝ × ℝ) → (1st ‘(𝐻𝑚)) ∈ ℝ)
7773, 76syl 17 . . . . . . . 8 ((𝜑𝑚 ∈ (1...𝐾)) → (1st ‘(𝐻𝑚)) ∈ ℝ)
7875, 77resubcld 11688 . . . . . . 7 ((𝜑𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻𝑚)) − (1st ‘(𝐻𝑚))) ∈ ℝ)
7978recnd 11286 . . . . . 6 ((𝜑𝑚 ∈ (1...𝐾)) → ((2nd ‘(𝐻𝑚)) − (1st ‘(𝐻𝑚))) ∈ ℂ)
8066, 79eqeltrrd 2839 . . . . 5 ((𝜑𝑚 ∈ (1...𝐾)) → ((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))) ∈ ℂ)
8167, 70, 80fsumser 15762 . . . 4 (𝜑 → Σ𝑚 ∈ (1...𝐾)((2nd ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚)))) − (1st ‘((𝐹‘(1st ‘(𝐽𝑚)))‘(2nd ‘(𝐽𝑚))))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝐾))
8239, 81eqtrd 2774 . . 3 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝐾))
83 ovoliun.u . . . 4 𝑈 = seq1( + , ((abs ∘ − ) ∘ 𝐻))
8483fveq1i 6907 . . 3 (𝑈𝐾) = (seq1( + , ((abs ∘ − ) ∘ 𝐻))‘𝐾)
8582, 84eqtr4di 2792 . 2 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = (𝑈𝐾))
86 f1oeng 9009 . . . . . . 7 (((1...𝐾) ∈ Fin ∧ (𝐽 ↾ (1...𝐾)):(1...𝐾)–1-1-onto→(𝐽 “ (1...𝐾))) → (1...𝐾) ≈ (𝐽 “ (1...𝐾)))
877, 13, 86syl2anc 584 . . . . . 6 (𝜑 → (1...𝐾) ≈ (𝐽 “ (1...𝐾)))
8887ensymd 9043 . . . . 5 (𝜑 → (𝐽 “ (1...𝐾)) ≈ (1...𝐾))
89 enfii 9223 . . . . 5 (((1...𝐾) ∈ Fin ∧ (𝐽 “ (1...𝐾)) ≈ (1...𝐾)) → (𝐽 “ (1...𝐾)) ∈ Fin)
907, 88, 89syl2anc 584 . . . 4 (𝜑 → (𝐽 “ (1...𝐾)) ∈ Fin)
9190, 37fsumrecl 15766 . . 3 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) ∈ ℝ)
92 fzfid 14010 . . . . 5 (𝜑 → (1...𝐿) ∈ Fin)
93 elfznn 13589 . . . . . 6 (𝑛 ∈ (1...𝐿) → 𝑛 ∈ ℕ)
94 ovoliun.v . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (vol*‘𝐴) ∈ ℝ)
9593, 94sylan2 593 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈ ℝ)
9692, 95fsumrecl 15766 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ℝ)
97 ovoliun.b . . . . . . 7 (𝜑𝐵 ∈ ℝ+)
9897rpred 13074 . . . . . 6 (𝜑𝐵 ∈ ℝ)
99 2nn 12336 . . . . . . . 8 2 ∈ ℕ
100 nnnn0 12530 . . . . . . . 8 (𝑛 ∈ ℕ → 𝑛 ∈ ℕ0)
101 nnexpcl 14111 . . . . . . . 8 ((2 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (2↑𝑛) ∈ ℕ)
10299, 100, 101sylancr 587 . . . . . . 7 (𝑛 ∈ ℕ → (2↑𝑛) ∈ ℕ)
10393, 102syl 17 . . . . . 6 (𝑛 ∈ (1...𝐿) → (2↑𝑛) ∈ ℕ)
104 nndivre 12304 . . . . . 6 ((𝐵 ∈ ℝ ∧ (2↑𝑛) ∈ ℕ) → (𝐵 / (2↑𝑛)) ∈ ℝ)
10598, 103, 104syl2an 596 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐵 / (2↑𝑛)) ∈ ℝ)
10692, 105fsumrecl 15766 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) ∈ ℝ)
10796, 106readdcld 11287 . . 3 (𝜑 → (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))) ∈ ℝ)
108 ovoliun.r . . . 4 (𝜑 → sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
109108, 98readdcld 11287 . . 3 (𝜑 → (sup(ran 𝑇, ℝ*, < ) + 𝐵) ∈ ℝ)
110 relxp 5706 . . . . . . . . . . . . . . 15 Rel ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))
111 relres 6025 . . . . . . . . . . . . . . 15 Rel ((𝐽 “ (1...𝐾)) ↾ {𝑛})
112 elsni 4647 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ {𝑛} → 𝑥 = 𝑛)
113112opeq1d 4883 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑛} → ⟨𝑥, 𝑦⟩ = ⟨𝑛, 𝑦⟩)
114113eleq1d 2823 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ {𝑛} → (⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)) ↔ ⟨𝑛, 𝑦⟩ ∈ (𝐽 “ (1...𝐾))))
115 vex 3481 . . . . . . . . . . . . . . . . . . 19 𝑛 ∈ V
116 vex 3481 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
117115, 116elimasn 6109 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}) ↔ ⟨𝑛, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)))
118114, 117bitr4di 289 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑛} → (⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)) ↔ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})))
119118pm5.32i 574 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ {𝑛} ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾))) ↔ (𝑥 ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})))
120116opelresi 6007 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ((𝐽 “ (1...𝐾)) ↾ {𝑛}) ↔ (𝑥 ∈ {𝑛} ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾))))
121 opelxp 5724 . . . . . . . . . . . . . . . 16 (⟨𝑥, 𝑦⟩ ∈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ↔ (𝑥 ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})))
122119, 120, 1213bitr4ri 304 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ↔ ⟨𝑥, 𝑦⟩ ∈ ((𝐽 “ (1...𝐾)) ↾ {𝑛}))
123110, 111, 122eqrelriiv 5802 . . . . . . . . . . . . . 14 ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ↾ {𝑛})
124 df-res 5700 . . . . . . . . . . . . . 14 ((𝐽 “ (1...𝐾)) ↾ {𝑛}) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V))
125123, 124eqtri 2762 . . . . . . . . . . . . 13 ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V))
126125a1i 11 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)))
127126iuneq2dv 5020 . . . . . . . . . . 11 (𝜑 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = 𝑛 ∈ (1...𝐿)((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)))
128 iunin2 5075 . . . . . . . . . . 11 𝑛 ∈ (1...𝐿)((𝐽 “ (1...𝐾)) ∩ ({𝑛} × V)) = ((𝐽 “ (1...𝐾)) ∩ 𝑛 ∈ (1...𝐿)({𝑛} × V))
129127, 128eqtrdi 2790 . . . . . . . . . 10 (𝜑 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = ((𝐽 “ (1...𝐾)) ∩ 𝑛 ∈ (1...𝐿)({𝑛} × V)))
130 relxp 5706 . . . . . . . . . . . . . 14 Rel (ℕ × ℕ)
131 relss 5793 . . . . . . . . . . . . . 14 ((𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ) → (Rel (ℕ × ℕ) → Rel (𝐽 “ (1...𝐾))))
13222, 130, 131mpisyl 21 . . . . . . . . . . . . 13 (𝜑 → Rel (𝐽 “ (1...𝐾)))
133 ovoliun.l2 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽𝑤)) ≤ 𝐿)
13420ffnd 6737 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐽 Fn ℕ)
135 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝐽𝑤) → (1st𝑗) = (1st ‘(𝐽𝑤)))
136135breq1d 5157 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝐽𝑤) → ((1st𝑗) ≤ 𝐿 ↔ (1st ‘(𝐽𝑤)) ≤ 𝐿))
137136ralima 7256 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 Fn ℕ ∧ (1...𝐾) ⊆ ℕ) → (∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st𝑗) ≤ 𝐿 ↔ ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽𝑤)) ≤ 𝐿))
138134, 11, 137sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st𝑗) ≤ 𝐿 ↔ ∀𝑤 ∈ (1...𝐾)(1st ‘(𝐽𝑤)) ≤ 𝐿))
139133, 138mpbird 257 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st𝑗) ≤ 𝐿)
140139r19.21bi 3248 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st𝑗) ≤ 𝐿)
14125, 69eleqtrdi 2848 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st𝑗) ∈ (ℤ‘1))
142 ovoliun.l1 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐿 ∈ ℤ)
143142adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → 𝐿 ∈ ℤ)
144 elfz5 13552 . . . . . . . . . . . . . . . . . 18 (((1st𝑗) ∈ (ℤ‘1) ∧ 𝐿 ∈ ℤ) → ((1st𝑗) ∈ (1...𝐿) ↔ (1st𝑗) ≤ 𝐿))
145141, 143, 144syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → ((1st𝑗) ∈ (1...𝐿) ↔ (1st𝑗) ≤ 𝐿))
146140, 145mpbird 257 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (𝐽 “ (1...𝐾))) → (1st𝑗) ∈ (1...𝐿))
147146ralrimiva 3143 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st𝑗) ∈ (1...𝐿))
148 vex 3481 . . . . . . . . . . . . . . . . . 18 𝑥 ∈ V
149148, 116op1std 8022 . . . . . . . . . . . . . . . . 17 (𝑗 = ⟨𝑥, 𝑦⟩ → (1st𝑗) = 𝑥)
150149eleq1d 2823 . . . . . . . . . . . . . . . 16 (𝑗 = ⟨𝑥, 𝑦⟩ → ((1st𝑗) ∈ (1...𝐿) ↔ 𝑥 ∈ (1...𝐿)))
151150rspccv 3618 . . . . . . . . . . . . . . 15 (∀𝑗 ∈ (𝐽 “ (1...𝐾))(1st𝑗) ∈ (1...𝐿) → (⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)) → 𝑥 ∈ (1...𝐿)))
152147, 151syl 17 . . . . . . . . . . . . . 14 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)) → 𝑥 ∈ (1...𝐿)))
153 opelxp 5724 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ ( 𝑛 ∈ (1...𝐿){𝑛} × V) ↔ (𝑥 𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V))
154116biantru 529 . . . . . . . . . . . . . . 15 (𝑥 𝑛 ∈ (1...𝐿){𝑛} ↔ (𝑥 𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V))
155 iunid 5064 . . . . . . . . . . . . . . . 16 𝑛 ∈ (1...𝐿){𝑛} = (1...𝐿)
156155eleq2i 2830 . . . . . . . . . . . . . . 15 (𝑥 𝑛 ∈ (1...𝐿){𝑛} ↔ 𝑥 ∈ (1...𝐿))
157153, 154, 1563bitr2i 299 . . . . . . . . . . . . . 14 (⟨𝑥, 𝑦⟩ ∈ ( 𝑛 ∈ (1...𝐿){𝑛} × V) ↔ 𝑥 ∈ (1...𝐿))
158152, 157imbitrrdi 252 . . . . . . . . . . . . 13 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ (𝐽 “ (1...𝐾)) → ⟨𝑥, 𝑦⟩ ∈ ( 𝑛 ∈ (1...𝐿){𝑛} × V)))
159132, 158relssdv 5800 . . . . . . . . . . . 12 (𝜑 → (𝐽 “ (1...𝐾)) ⊆ ( 𝑛 ∈ (1...𝐿){𝑛} × V))
160 xpiundir 5759 . . . . . . . . . . . 12 ( 𝑛 ∈ (1...𝐿){𝑛} × V) = 𝑛 ∈ (1...𝐿)({𝑛} × V)
161159, 160sseqtrdi 4045 . . . . . . . . . . 11 (𝜑 → (𝐽 “ (1...𝐾)) ⊆ 𝑛 ∈ (1...𝐿)({𝑛} × V))
162 dfss2 3980 . . . . . . . . . . 11 ((𝐽 “ (1...𝐾)) ⊆ 𝑛 ∈ (1...𝐿)({𝑛} × V) ↔ ((𝐽 “ (1...𝐾)) ∩ 𝑛 ∈ (1...𝐿)({𝑛} × V)) = (𝐽 “ (1...𝐾)))
163161, 162sylib 218 . . . . . . . . . 10 (𝜑 → ((𝐽 “ (1...𝐾)) ∩ 𝑛 ∈ (1...𝐿)({𝑛} × V)) = (𝐽 “ (1...𝐾)))
164129, 163eqtrd 2774 . . . . . . . . 9 (𝜑 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) = (𝐽 “ (1...𝐾)))
165164, 90eqeltrd 2838 . . . . . . . 8 (𝜑 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin)
166 ssiun2 5051 . . . . . . . 8 (𝑛 ∈ (1...𝐿) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ⊆ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})))
167 ssfi 9211 . . . . . . . 8 (( 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ⊆ 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin)
168165, 166, 167syl2an 596 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin)
169 2ndconst 8124 . . . . . . . . . 10 (𝑛 ∈ V → (2nd ↾ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛}))
170169elv 3482 . . . . . . . . 9 (2nd ↾ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛})
171 f1oeng 9009 . . . . . . . . 9 ((({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ (2nd ↾ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))):({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))–1-1-onto→((𝐽 “ (1...𝐾)) “ {𝑛})) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ≈ ((𝐽 “ (1...𝐾)) “ {𝑛}))
172168, 170, 171sylancl 586 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ≈ ((𝐽 “ (1...𝐾)) “ {𝑛}))
173172ensymd 9043 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ≈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})))
174 enfii 9223 . . . . . . 7 ((({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛})) ∈ Fin ∧ ((𝐽 “ (1...𝐾)) “ {𝑛}) ≈ ({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ∈ Fin)
175168, 173, 174syl2anc 584 . . . . . 6 ((𝜑𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ∈ Fin)
176 ffvelcdm 7100 . . . . . . . . . . . . . 14 ((𝐹:ℕ⟶(( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
17716, 93, 176syl2an 596 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐹𝑛) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ))
178 elovolmlem 25522 . . . . . . . . . . . . 13 ((𝐹𝑛) ∈ (( ≤ ∩ (ℝ × ℝ)) ↑m ℕ) ↔ (𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
179177, 178sylib 218 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
180179adantrr 717 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)))
181 imassrn 6090 . . . . . . . . . . . . . 14 ((𝐽 “ (1...𝐾)) “ {𝑛}) ⊆ ran (𝐽 “ (1...𝐾))
18222adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ))
183 rnss 5952 . . . . . . . . . . . . . . . 16 ((𝐽 “ (1...𝐾)) ⊆ (ℕ × ℕ) → ran (𝐽 “ (1...𝐾)) ⊆ ran (ℕ × ℕ))
184182, 183syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ (1...𝐿)) → ran (𝐽 “ (1...𝐾)) ⊆ ran (ℕ × ℕ))
185 rnxpid 6194 . . . . . . . . . . . . . . 15 ran (ℕ × ℕ) = ℕ
186184, 185sseqtrdi 4045 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝐿)) → ran (𝐽 “ (1...𝐾)) ⊆ ℕ)
187181, 186sstrid 4006 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝐿)) → ((𝐽 “ (1...𝐾)) “ {𝑛}) ⊆ ℕ)
188187sseld 3993 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → (𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}) → 𝑖 ∈ ℕ))
189188impr 454 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → 𝑖 ∈ ℕ)
190180, 189ffvelcdmd 7104 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐹𝑛)‘𝑖) ∈ ( ≤ ∩ (ℝ × ℝ)))
191190elin2d 4214 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((𝐹𝑛)‘𝑖) ∈ (ℝ × ℝ))
192 xp2nd 8045 . . . . . . . . 9 (((𝐹𝑛)‘𝑖) ∈ (ℝ × ℝ) → (2nd ‘((𝐹𝑛)‘𝑖)) ∈ ℝ)
193191, 192syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (2nd ‘((𝐹𝑛)‘𝑖)) ∈ ℝ)
194 xp1st 8044 . . . . . . . . 9 (((𝐹𝑛)‘𝑖) ∈ (ℝ × ℝ) → (1st ‘((𝐹𝑛)‘𝑖)) ∈ ℝ)
195191, 194syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → (1st ‘((𝐹𝑛)‘𝑖)) ∈ ℝ)
196193, 195resubcld 11688 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ)
197196anassrs 467 . . . . . 6 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})) → ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ)
198175, 197fsumrecl 15766 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ)
19998, 102, 104syl2an 596 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝐵 / (2↑𝑛)) ∈ ℝ)
20094, 199readdcld 11287 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ)
20193, 200sylan2 593 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ)
202 eqid 2734 . . . . . . . . . . . 12 ((abs ∘ − ) ∘ (𝐹𝑛)) = ((abs ∘ − ) ∘ (𝐹𝑛))
203 ovoliun.s . . . . . . . . . . . 12 𝑆 = seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛)))
204202, 203ovolsf 25520 . . . . . . . . . . 11 ((𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → 𝑆:ℕ⟶(0[,)+∞))
205179, 204syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝐿)) → 𝑆:ℕ⟶(0[,)+∞))
206205frnd 6744 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆ (0[,)+∞))
207 icossxr 13468 . . . . . . . . 9 (0[,)+∞) ⊆ ℝ*
208206, 207sstrdi 4007 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆ ℝ*)
209 supxrcl 13353 . . . . . . . 8 (ran 𝑆 ⊆ ℝ* → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
210208, 209syl 17 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
211 mnfxr 11315 . . . . . . . . 9 -∞ ∈ ℝ*
212211a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → -∞ ∈ ℝ*)
21395rexrd 11308 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈ ℝ*)
21495mnfltd 13163 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → -∞ < (vol*‘𝐴))
215 ovoliun.x1 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 𝐴 ran ((,) ∘ (𝐹𝑛)))
21693, 215sylan2 593 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝐿)) → 𝐴 ran ((,) ∘ (𝐹𝑛)))
217203ovollb 25527 . . . . . . . . 9 (((𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝐴 ran ((,) ∘ (𝐹𝑛))) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
218179, 216, 217syl2anc 584 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ≤ sup(ran 𝑆, ℝ*, < ))
219212, 213, 210, 214, 218xrltletrd 13199 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → -∞ < sup(ran 𝑆, ℝ*, < ))
220 ovoliun.x2 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))
22193, 220sylan2 593 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))
222 xrre 13207 . . . . . . 7 (((sup(ran 𝑆, ℝ*, < ) ∈ ℝ* ∧ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
223210, 201, 219, 221, 222syl22anc 839 . . . . . 6 ((𝜑𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
224 1zzd 12645 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → 1 ∈ ℤ)
225202ovolfsval 25518 . . . . . . . . 9 (((𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)) ∧ 𝑖 ∈ ℕ) → (((abs ∘ − ) ∘ (𝐹𝑛))‘𝑖) = ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))))
226179, 225sylan 580 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((abs ∘ − ) ∘ (𝐹𝑛))‘𝑖) = ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))))
227202ovolfsf 25519 . . . . . . . . . . . . 13 ((𝐹𝑛):ℕ⟶( ≤ ∩ (ℝ × ℝ)) → ((abs ∘ − ) ∘ (𝐹𝑛)):ℕ⟶(0[,)+∞))
228179, 227syl 17 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → ((abs ∘ − ) ∘ (𝐹𝑛)):ℕ⟶(0[,)+∞))
229228ffvelcdmda 7103 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((abs ∘ − ) ∘ (𝐹𝑛))‘𝑖) ∈ (0[,)+∞))
230226, 229eqeltrrd 2839 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ (0[,)+∞))
231 elrege0 13490 . . . . . . . . . 10 (((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ (0[,)+∞) ↔ (((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ ∧ 0 ≤ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖)))))
232230, 231sylib 218 . . . . . . . . 9 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → (((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ ∧ 0 ≤ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖)))))
233232simpld 494 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℝ)
234232simprd 495 . . . . . . . 8 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ℕ) → 0 ≤ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))))
235 supxrub 13362 . . . . . . . . . . . . . . 15 ((ran 𝑆 ⊆ ℝ*𝑧 ∈ ran 𝑆) → 𝑧 ≤ sup(ran 𝑆, ℝ*, < ))
236208, 235sylan 580 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ (1...𝐿)) ∧ 𝑧 ∈ ran 𝑆) → 𝑧 ≤ sup(ran 𝑆, ℝ*, < ))
237236ralrimiva 3143 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝐿)) → ∀𝑧 ∈ ran 𝑆 𝑧 ≤ sup(ran 𝑆, ℝ*, < ))
238 brralrspcev 5207 . . . . . . . . . . . . 13 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ ∀𝑧 ∈ ran 𝑆 𝑧 ≤ sup(ran 𝑆, ℝ*, < )) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥)
239223, 237, 238syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥)
240205ffnd 6737 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...𝐿)) → 𝑆 Fn ℕ)
241 breq1 5150 . . . . . . . . . . . . . . 15 (𝑧 = (𝑆𝑘) → (𝑧𝑥 ↔ (𝑆𝑘) ≤ 𝑥))
242241ralrn 7107 . . . . . . . . . . . . . 14 (𝑆 Fn ℕ → (∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
243240, 242syl 17 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...𝐿)) → (∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
244243rexbidv 3176 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥))
245239, 244mpbid 232 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝐿)) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆𝑘) ≤ 𝑥)
24669, 203, 224, 226, 233, 234, 245isumsup2 15878 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝐿)) → 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
247203, 246eqbrtrrid 5183 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝐿)) → seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛))) ⇝ sup(ran 𝑆, ℝ, < ))
248 climrel 15524 . . . . . . . . . 10 Rel ⇝
249248releldmi 5961 . . . . . . . . 9 (seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛))) ⇝ sup(ran 𝑆, ℝ, < ) → seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛))) ∈ dom ⇝ )
250247, 249syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → seq1( + , ((abs ∘ − ) ∘ (𝐹𝑛))) ∈ dom ⇝ )
25169, 224, 175, 187, 226, 233, 234, 250isumless 15877 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ≤ Σ𝑖 ∈ ℕ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))))
25269, 203, 224, 226, 233, 234, 245isumsup 15879 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ℕ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) = sup(ran 𝑆, ℝ, < ))
253 rge0ssre 13492 . . . . . . . . . 10 (0[,)+∞) ⊆ ℝ
254206, 253sstrdi 4007 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝐿)) → ran 𝑆 ⊆ ℝ)
255 1nn 12274 . . . . . . . . . . . 12 1 ∈ ℕ
256205fdmd 6746 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...𝐿)) → dom 𝑆 = ℕ)
257255, 256eleqtrrid 2845 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...𝐿)) → 1 ∈ dom 𝑆)
258257ne0d 4347 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...𝐿)) → dom 𝑆 ≠ ∅)
259 dm0rn0 5937 . . . . . . . . . . 11 (dom 𝑆 = ∅ ↔ ran 𝑆 = ∅)
260259necon3bii 2990 . . . . . . . . . 10 (dom 𝑆 ≠ ∅ ↔ ran 𝑆 ≠ ∅)
261258, 260sylib 218 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...𝐿)) → ran 𝑆 ≠ ∅)
262 supxrre 13365 . . . . . . . . 9 ((ran 𝑆 ⊆ ℝ ∧ ran 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran 𝑆 𝑧𝑥) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
263254, 261, 239, 262syl3anc 1370 . . . . . . . 8 ((𝜑𝑛 ∈ (1...𝐿)) → sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
264252, 263eqtr4d 2777 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ℕ ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) = sup(ran 𝑆, ℝ*, < ))
265251, 264breqtrd 5173 . . . . . 6 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ≤ sup(ran 𝑆, ℝ*, < ))
266198, 223, 201, 265, 221letrd 11415 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → Σ𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ≤ ((vol*‘𝐴) + (𝐵 / (2↑𝑛))))
26792, 198, 201, 266fsumle 15831 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ≤ Σ𝑛 ∈ (1...𝐿)((vol*‘𝐴) + (𝐵 / (2↑𝑛))))
268 vex 3481 . . . . . . . . . . 11 𝑖 ∈ V
269115, 268op1std 8022 . . . . . . . . . 10 (𝑗 = ⟨𝑛, 𝑖⟩ → (1st𝑗) = 𝑛)
270269fveq2d 6910 . . . . . . . . 9 (𝑗 = ⟨𝑛, 𝑖⟩ → (𝐹‘(1st𝑗)) = (𝐹𝑛))
271115, 268op2ndd 8023 . . . . . . . . 9 (𝑗 = ⟨𝑛, 𝑖⟩ → (2nd𝑗) = 𝑖)
272270, 271fveq12d 6913 . . . . . . . 8 (𝑗 = ⟨𝑛, 𝑖⟩ → ((𝐹‘(1st𝑗))‘(2nd𝑗)) = ((𝐹𝑛)‘𝑖))
273272fveq2d 6910 . . . . . . 7 (𝑗 = ⟨𝑛, 𝑖⟩ → (2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) = (2nd ‘((𝐹𝑛)‘𝑖)))
274272fveq2d 6910 . . . . . . 7 (𝑗 = ⟨𝑛, 𝑖⟩ → (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) = (1st ‘((𝐹𝑛)‘𝑖)))
275273, 274oveq12d 7448 . . . . . 6 (𝑗 = ⟨𝑛, 𝑖⟩ → ((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))))
276196recnd 11286 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛}))) → ((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) ∈ ℂ)
277275, 92, 175, 276fsum2d 15803 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...𝐿𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) = Σ𝑗 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))))
278164sumeq1d 15732 . . . . 5 (𝜑 → Σ𝑗 𝑛 ∈ (1...𝐿)({𝑛} × ((𝐽 “ (1...𝐾)) “ {𝑛}))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) = Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))))
279277, 278eqtrd 2774 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿𝑖 ∈ ((𝐽 “ (1...𝐾)) “ {𝑛})((2nd ‘((𝐹𝑛)‘𝑖)) − (1st ‘((𝐹𝑛)‘𝑖))) = Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))))
28095recnd 11286 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → (vol*‘𝐴) ∈ ℂ)
281105recnd 11286 . . . . 5 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐵 / (2↑𝑛)) ∈ ℂ)
28292, 280, 281fsumadd 15772 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿)((vol*‘𝐴) + (𝐵 / (2↑𝑛))) = (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))))
283267, 279, 2823brtr3d 5178 . . 3 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) ≤ (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))))
284 1zzd 12645 . . . . . . . . 9 (𝜑 → 1 ∈ ℤ)
285 simpr 484 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
286 ovoliun.g . . . . . . . . . . . 12 𝐺 = (𝑛 ∈ ℕ ↦ (vol*‘𝐴))
287286fvmpt2 7026 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (vol*‘𝐴) ∈ ℝ) → (𝐺𝑛) = (vol*‘𝐴))
288285, 94, 287syl2anc 584 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) = (vol*‘𝐴))
289288, 94eqeltrd 2838 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝐺𝑛) ∈ ℝ)
29069, 284, 289serfre 14068 . . . . . . . 8 (𝜑 → seq1( + , 𝐺):ℕ⟶ℝ)
291 ovoliun.t . . . . . . . . 9 𝑇 = seq1( + , 𝐺)
292291feq1i 6727 . . . . . . . 8 (𝑇:ℕ⟶ℝ ↔ seq1( + , 𝐺):ℕ⟶ℝ)
293290, 292sylibr 234 . . . . . . 7 (𝜑𝑇:ℕ⟶ℝ)
294293frnd 6744 . . . . . 6 (𝜑 → ran 𝑇 ⊆ ℝ)
295 ressxr 11302 . . . . . 6 ℝ ⊆ ℝ*
296294, 295sstrdi 4007 . . . . 5 (𝜑 → ran 𝑇 ⊆ ℝ*)
29793, 288sylan2 593 . . . . . . 7 ((𝜑𝑛 ∈ (1...𝐿)) → (𝐺𝑛) = (vol*‘𝐴))
298 1red 11259 . . . . . . . . . 10 (𝜑 → 1 ∈ ℝ)
299 ffvelcdm 7100 . . . . . . . . . . . . 13 ((𝐽:ℕ⟶(ℕ × ℕ) ∧ 1 ∈ ℕ) → (𝐽‘1) ∈ (ℕ × ℕ))
30020, 255, 299sylancl 586 . . . . . . . . . . . 12 (𝜑 → (𝐽‘1) ∈ (ℕ × ℕ))
301 xp1st 8044 . . . . . . . . . . . 12 ((𝐽‘1) ∈ (ℕ × ℕ) → (1st ‘(𝐽‘1)) ∈ ℕ)
302300, 301syl 17 . . . . . . . . . . 11 (𝜑 → (1st ‘(𝐽‘1)) ∈ ℕ)
303302nnred 12278 . . . . . . . . . 10 (𝜑 → (1st ‘(𝐽‘1)) ∈ ℝ)
304142zred 12719 . . . . . . . . . 10 (𝜑𝐿 ∈ ℝ)
305302nnge1d 12311 . . . . . . . . . 10 (𝜑 → 1 ≤ (1st ‘(𝐽‘1)))
306 2fveq3 6911 . . . . . . . . . . . 12 (𝑤 = 1 → (1st ‘(𝐽𝑤)) = (1st ‘(𝐽‘1)))
307306breq1d 5157 . . . . . . . . . . 11 (𝑤 = 1 → ((1st ‘(𝐽𝑤)) ≤ 𝐿 ↔ (1st ‘(𝐽‘1)) ≤ 𝐿))
308 eluzfz1 13567 . . . . . . . . . . . 12 (𝐾 ∈ (ℤ‘1) → 1 ∈ (1...𝐾))
30970, 308syl 17 . . . . . . . . . . 11 (𝜑 → 1 ∈ (1...𝐾))
310307, 133, 309rspcdva 3622 . . . . . . . . . 10 (𝜑 → (1st ‘(𝐽‘1)) ≤ 𝐿)
311298, 303, 304, 305, 310letrd 11415 . . . . . . . . 9 (𝜑 → 1 ≤ 𝐿)
312 elnnz1 12640 . . . . . . . . 9 (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 1 ≤ 𝐿))
313142, 311, 312sylanbrc 583 . . . . . . . 8 (𝜑𝐿 ∈ ℕ)
314313, 69eleqtrdi 2848 . . . . . . 7 (𝜑𝐿 ∈ (ℤ‘1))
315297, 314, 280fsumser 15762 . . . . . 6 (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) = (seq1( + , 𝐺)‘𝐿))
316 seqfn 14050 . . . . . . . . 9 (1 ∈ ℤ → seq1( + , 𝐺) Fn (ℤ‘1))
317284, 316syl 17 . . . . . . . 8 (𝜑 → seq1( + , 𝐺) Fn (ℤ‘1))
318 fnfvelrn 7099 . . . . . . . 8 ((seq1( + , 𝐺) Fn (ℤ‘1) ∧ 𝐿 ∈ (ℤ‘1)) → (seq1( + , 𝐺)‘𝐿) ∈ ran seq1( + , 𝐺))
319317, 314, 318syl2anc 584 . . . . . . 7 (𝜑 → (seq1( + , 𝐺)‘𝐿) ∈ ran seq1( + , 𝐺))
320291rneqi 5950 . . . . . . 7 ran 𝑇 = ran seq1( + , 𝐺)
321319, 320eleqtrrdi 2849 . . . . . 6 (𝜑 → (seq1( + , 𝐺)‘𝐿) ∈ ran 𝑇)
322315, 321eqeltrd 2838 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ran 𝑇)
323 supxrub 13362 . . . . 5 ((ran 𝑇 ⊆ ℝ* ∧ Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ∈ ran 𝑇) → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
324296, 322, 323syl2anc 584 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) ≤ sup(ran 𝑇, ℝ*, < ))
32598recnd 11286 . . . . . 6 (𝜑𝐵 ∈ ℂ)
326 geo2sum 15905 . . . . . 6 ((𝐿 ∈ ℕ ∧ 𝐵 ∈ ℂ) → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) = (𝐵 − (𝐵 / (2↑𝐿))))
327313, 325, 326syl2anc 584 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) = (𝐵 − (𝐵 / (2↑𝐿))))
328313nnnn0d 12584 . . . . . . . . . 10 (𝜑𝐿 ∈ ℕ0)
329 nnexpcl 14111 . . . . . . . . . 10 ((2 ∈ ℕ ∧ 𝐿 ∈ ℕ0) → (2↑𝐿) ∈ ℕ)
33099, 328, 329sylancr 587 . . . . . . . . 9 (𝜑 → (2↑𝐿) ∈ ℕ)
331330nnrpd 13072 . . . . . . . 8 (𝜑 → (2↑𝐿) ∈ ℝ+)
33297, 331rpdivcld 13091 . . . . . . 7 (𝜑 → (𝐵 / (2↑𝐿)) ∈ ℝ+)
333332rpge0d 13078 . . . . . 6 (𝜑 → 0 ≤ (𝐵 / (2↑𝐿)))
33498, 330nndivred 12317 . . . . . . 7 (𝜑 → (𝐵 / (2↑𝐿)) ∈ ℝ)
33598, 334subge02d 11852 . . . . . 6 (𝜑 → (0 ≤ (𝐵 / (2↑𝐿)) ↔ (𝐵 − (𝐵 / (2↑𝐿))) ≤ 𝐵))
336333, 335mpbid 232 . . . . 5 (𝜑 → (𝐵 − (𝐵 / (2↑𝐿))) ≤ 𝐵)
337327, 336eqbrtrd 5169 . . . 4 (𝜑 → Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛)) ≤ 𝐵)
33896, 106, 108, 98, 324, 337le2addd 11879 . . 3 (𝜑 → (Σ𝑛 ∈ (1...𝐿)(vol*‘𝐴) + Σ𝑛 ∈ (1...𝐿)(𝐵 / (2↑𝑛))) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
33991, 107, 109, 283, 338letrd 11415 . 2 (𝜑 → Σ𝑗 ∈ (𝐽 “ (1...𝐾))((2nd ‘((𝐹‘(1st𝑗))‘(2nd𝑗))) − (1st ‘((𝐹‘(1st𝑗))‘(2nd𝑗)))) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
34085, 339eqbrtrrd 5171 1 (𝜑 → (𝑈𝐾) ≤ (sup(ran 𝑇, ℝ*, < ) + 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cin 3961  wss 3962  c0 4338  {csn 4630  cop 4636   cuni 4911   ciun 4995   class class class wbr 5147  cmpt 5230   × cxp 5686  dom cdm 5688  ran crn 5689  cres 5690  cima 5691  ccom 5692  Rel wrel 5693   Fn wfn 6557  wf 6558  1-1wf1 6559  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  1st c1st 8010  2nd c2nd 8011  m cmap 8864  cen 8980  Fincfn 8983  supcsup 9477  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155  +∞cpnf 11289  -∞cmnf 11290  *cxr 11291   < clt 11292  cle 11293  cmin 11489   / cdiv 11917  cn 12263  2c2 12318  0cn0 12523  cz 12610  cuz 12875  +crp 13031  (,)cioo 13383  [,)cico 13385  ...cfz 13543  seqcseq 14038  cexp 14098  abscabs 15269  cli 15516  Σcsu 15718  vol*covol 25510
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-ioo 13387  df-ico 13389  df-fz 13544  df-fzo 13691  df-fl 13828  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-rlim 15521  df-sum 15719  df-ovol 25512
This theorem is referenced by:  ovoliunlem2  25551
  Copyright terms: Public domain W3C validator