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

Theorem ovoliunlem1 24882
Description: Lemma for ovoliun 24885. (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 6852 . . . . . . . 8 (𝑗 = (π½β€˜π‘š) β†’ (πΉβ€˜(1st β€˜π‘—)) = (πΉβ€˜(1st β€˜(π½β€˜π‘š))))
2 fveq2 6847 . . . . . . . 8 (𝑗 = (π½β€˜π‘š) β†’ (2nd β€˜π‘—) = (2nd β€˜(π½β€˜π‘š)))
31, 2fveq12d 6854 . . . . . . 7 (𝑗 = (π½β€˜π‘š) β†’ ((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) = ((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))
43fveq2d 6851 . . . . . 6 (𝑗 = (π½β€˜π‘š) β†’ (2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) = (2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))))
53fveq2d 6851 . . . . . 6 (𝑗 = (π½β€˜π‘š) β†’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) = (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))))
64, 5oveq12d 7380 . . . . 5 (𝑗 = (π½β€˜π‘š) β†’ ((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = ((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))))
7 fzfid 13885 . . . . 5 (πœ‘ β†’ (1...𝐾) ∈ Fin)
8 ovoliun.j . . . . . . 7 (πœ‘ β†’ 𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•))
9 f1of1 6788 . . . . . . 7 (𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•) β†’ 𝐽:ℕ–1-1β†’(β„• Γ— β„•))
108, 9syl 17 . . . . . 6 (πœ‘ β†’ 𝐽:ℕ–1-1β†’(β„• Γ— β„•))
11 fz1ssnn 13479 . . . . . 6 (1...𝐾) βŠ† β„•
12 f1ores 6803 . . . . . 6 ((𝐽:ℕ–1-1β†’(β„• Γ— β„•) ∧ (1...𝐾) βŠ† β„•) β†’ (𝐽 β†Ύ (1...𝐾)):(1...𝐾)–1-1-ontoβ†’(𝐽 β€œ (1...𝐾)))
1310, 11, 12sylancl 587 . . . . 5 (πœ‘ β†’ (𝐽 β†Ύ (1...𝐾)):(1...𝐾)–1-1-ontoβ†’(𝐽 β€œ (1...𝐾)))
14 fvres 6866 . . . . . 6 (π‘š ∈ (1...𝐾) β†’ ((𝐽 β†Ύ (1...𝐾))β€˜π‘š) = (π½β€˜π‘š))
1514adantl 483 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ ((𝐽 β†Ύ (1...𝐾))β€˜π‘š) = (π½β€˜π‘š))
16 ovoliun.f . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
1716adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
18 imassrn 6029 . . . . . . . . . . . . . . 15 (𝐽 β€œ (1...𝐾)) βŠ† ran 𝐽
19 f1of 6789 . . . . . . . . . . . . . . . . 17 (𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•) β†’ 𝐽:β„•βŸΆ(β„• Γ— β„•))
208, 19syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐽:β„•βŸΆ(β„• Γ— β„•))
2120frnd 6681 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ran 𝐽 βŠ† (β„• Γ— β„•))
2218, 21sstrid 3960 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐽 β€œ (1...𝐾)) βŠ† (β„• Γ— β„•))
2322sselda 3949 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ 𝑗 ∈ (β„• Γ— β„•))
24 xp1st 7958 . . . . . . . . . . . . 13 (𝑗 ∈ (β„• Γ— β„•) β†’ (1st β€˜π‘—) ∈ β„•)
2523, 24syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (1st β€˜π‘—) ∈ β„•)
2617, 25ffvelcdmd 7041 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (πΉβ€˜(1st β€˜π‘—)) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
27 elovolmlem 24854 . . . . . . . . . . 11 ((πΉβ€˜(1st β€˜π‘—)) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ (πΉβ€˜(1st β€˜π‘—)):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
2826, 27sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (πΉβ€˜(1st β€˜π‘—)):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
29 xp2nd 7959 . . . . . . . . . . 11 (𝑗 ∈ (β„• Γ— β„•) β†’ (2nd β€˜π‘—) ∈ β„•)
3023, 29syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (2nd β€˜π‘—) ∈ β„•)
3128, 30ffvelcdmd 7041 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ ((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
3231elin2d 4164 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ ((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) ∈ (ℝ Γ— ℝ))
33 xp2nd 7959 . . . . . . . 8 (((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) ∈ ℝ)
3432, 33syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) ∈ ℝ)
35 xp1st 7958 . . . . . . . 8 (((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) ∈ (ℝ Γ— ℝ) β†’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) ∈ ℝ)
3632, 35syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) ∈ ℝ)
3734, 36resubcld 11590 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ ((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) ∈ ℝ)
3837recnd 11190 . . . . 5 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ ((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) ∈ β„‚)
396, 7, 13, 15, 38fsumf1o 15615 . . . 4 (πœ‘ β†’ Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = Ξ£π‘š ∈ (1...𝐾)((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))))
4016adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
4120ffvelcdmda 7040 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) ∈ (β„• Γ— β„•))
42 xp1st 7958 . . . . . . . . . . . 12 ((π½β€˜π‘˜) ∈ (β„• Γ— β„•) β†’ (1st β€˜(π½β€˜π‘˜)) ∈ β„•)
4341, 42syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(π½β€˜π‘˜)) ∈ β„•)
4440, 43ffvelcdmd 7041 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
45 elovolmlem 24854 . . . . . . . . . 10 ((πΉβ€˜(1st β€˜(π½β€˜π‘˜))) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
4644, 45sylib 217 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
47 xp2nd 7959 . . . . . . . . . 10 ((π½β€˜π‘˜) ∈ (β„• Γ— β„•) β†’ (2nd β€˜(π½β€˜π‘˜)) ∈ β„•)
4841, 47syl 17 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2nd β€˜(π½β€˜π‘˜)) ∈ β„•)
4946, 48ffvelcdmd 7041 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
50 ovoliun.h . . . . . . . 8 𝐻 = (π‘˜ ∈ β„• ↦ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))))
5149, 50fmptd 7067 . . . . . . 7 (πœ‘ β†’ 𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
52 elfznn 13477 . . . . . . 7 (π‘š ∈ (1...𝐾) β†’ π‘š ∈ β„•)
53 eqid 2737 . . . . . . . 8 ((abs ∘ βˆ’ ) ∘ 𝐻) = ((abs ∘ βˆ’ ) ∘ 𝐻)
5453ovolfsval 24850 . . . . . . 7 ((𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ π‘š ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘š) = ((2nd β€˜(π»β€˜π‘š)) βˆ’ (1st β€˜(π»β€˜π‘š))))
5551, 52, 54syl2an 597 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘š) = ((2nd β€˜(π»β€˜π‘š)) βˆ’ (1st β€˜(π»β€˜π‘š))))
5652adantl 483 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ π‘š ∈ β„•)
57 2fveq3 6852 . . . . . . . . . . . 12 (π‘˜ = π‘š β†’ (1st β€˜(π½β€˜π‘˜)) = (1st β€˜(π½β€˜π‘š)))
5857fveq2d 6851 . . . . . . . . . . 11 (π‘˜ = π‘š β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))) = (πΉβ€˜(1st β€˜(π½β€˜π‘š))))
59 2fveq3 6852 . . . . . . . . . . 11 (π‘˜ = π‘š β†’ (2nd β€˜(π½β€˜π‘˜)) = (2nd β€˜(π½β€˜π‘š)))
6058, 59fveq12d 6854 . . . . . . . . . 10 (π‘˜ = π‘š β†’ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))) = ((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))
61 fvex 6860 . . . . . . . . . 10 ((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))) ∈ V
6260, 50, 61fvmpt 6953 . . . . . . . . 9 (π‘š ∈ β„• β†’ (π»β€˜π‘š) = ((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))
6356, 62syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (π»β€˜π‘š) = ((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))
6463fveq2d 6851 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (2nd β€˜(π»β€˜π‘š)) = (2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))))
6563fveq2d 6851 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (1st β€˜(π»β€˜π‘š)) = (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))))
6664, 65oveq12d 7380 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ ((2nd β€˜(π»β€˜π‘š)) βˆ’ (1st β€˜(π»β€˜π‘š))) = ((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))))
6755, 66eqtrd 2777 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘š) = ((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))))
68 ovoliun.k . . . . . 6 (πœ‘ β†’ 𝐾 ∈ β„•)
69 nnuz 12813 . . . . . 6 β„• = (β„€β‰₯β€˜1)
7068, 69eleqtrdi 2848 . . . . 5 (πœ‘ β†’ 𝐾 ∈ (β„€β‰₯β€˜1))
71 ffvelcdm 7037 . . . . . . . . . . 11 ((𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ π‘š ∈ β„•) β†’ (π»β€˜π‘š) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
7251, 52, 71syl2an 597 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (π»β€˜π‘š) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
7372elin2d 4164 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (π»β€˜π‘š) ∈ (ℝ Γ— ℝ))
74 xp2nd 7959 . . . . . . . . 9 ((π»β€˜π‘š) ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜(π»β€˜π‘š)) ∈ ℝ)
7573, 74syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (2nd β€˜(π»β€˜π‘š)) ∈ ℝ)
76 xp1st 7958 . . . . . . . . 9 ((π»β€˜π‘š) ∈ (ℝ Γ— ℝ) β†’ (1st β€˜(π»β€˜π‘š)) ∈ ℝ)
7773, 76syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (1st β€˜(π»β€˜π‘š)) ∈ ℝ)
7875, 77resubcld 11590 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ ((2nd β€˜(π»β€˜π‘š)) βˆ’ (1st β€˜(π»β€˜π‘š))) ∈ ℝ)
7978recnd 11190 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ ((2nd β€˜(π»β€˜π‘š)) βˆ’ (1st β€˜(π»β€˜π‘š))) ∈ β„‚)
8066, 79eqeltrrd 2839 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ ((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))) ∈ β„‚)
8167, 70, 80fsumser 15622 . . . 4 (πœ‘ β†’ Ξ£π‘š ∈ (1...𝐾)((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜πΎ))
8239, 81eqtrd 2777 . . 3 (πœ‘ β†’ Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜πΎ))
83 ovoliun.u . . . 4 π‘ˆ = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))
8483fveq1i 6848 . . 3 (π‘ˆβ€˜πΎ) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜πΎ)
8582, 84eqtr4di 2795 . 2 (πœ‘ β†’ Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = (π‘ˆβ€˜πΎ))
86 f1oeng 8918 . . . . . . 7 (((1...𝐾) ∈ Fin ∧ (𝐽 β†Ύ (1...𝐾)):(1...𝐾)–1-1-ontoβ†’(𝐽 β€œ (1...𝐾))) β†’ (1...𝐾) β‰ˆ (𝐽 β€œ (1...𝐾)))
877, 13, 86syl2anc 585 . . . . . 6 (πœ‘ β†’ (1...𝐾) β‰ˆ (𝐽 β€œ (1...𝐾)))
8887ensymd 8952 . . . . 5 (πœ‘ β†’ (𝐽 β€œ (1...𝐾)) β‰ˆ (1...𝐾))
89 enfii 9140 . . . . 5 (((1...𝐾) ∈ Fin ∧ (𝐽 β€œ (1...𝐾)) β‰ˆ (1...𝐾)) β†’ (𝐽 β€œ (1...𝐾)) ∈ Fin)
907, 88, 89syl2anc 585 . . . 4 (πœ‘ β†’ (𝐽 β€œ (1...𝐾)) ∈ Fin)
9190, 37fsumrecl 15626 . . 3 (πœ‘ β†’ Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) ∈ ℝ)
92 fzfid 13885 . . . . 5 (πœ‘ β†’ (1...𝐿) ∈ Fin)
93 elfznn 13477 . . . . . 6 (𝑛 ∈ (1...𝐿) β†’ 𝑛 ∈ β„•)
94 ovoliun.v . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (vol*β€˜π΄) ∈ ℝ)
9593, 94sylan2 594 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (vol*β€˜π΄) ∈ ℝ)
9692, 95fsumrecl 15626 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) ∈ ℝ)
97 ovoliun.b . . . . . . 7 (πœ‘ β†’ 𝐡 ∈ ℝ+)
9897rpred 12964 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ ℝ)
99 2nn 12233 . . . . . . . 8 2 ∈ β„•
100 nnnn0 12427 . . . . . . . 8 (𝑛 ∈ β„• β†’ 𝑛 ∈ β„•0)
101 nnexpcl 13987 . . . . . . . 8 ((2 ∈ β„• ∧ 𝑛 ∈ β„•0) β†’ (2↑𝑛) ∈ β„•)
10299, 100, 101sylancr 588 . . . . . . 7 (𝑛 ∈ β„• β†’ (2↑𝑛) ∈ β„•)
10393, 102syl 17 . . . . . 6 (𝑛 ∈ (1...𝐿) β†’ (2↑𝑛) ∈ β„•)
104 nndivre 12201 . . . . . 6 ((𝐡 ∈ ℝ ∧ (2↑𝑛) ∈ β„•) β†’ (𝐡 / (2↑𝑛)) ∈ ℝ)
10598, 103, 104syl2an 597 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (𝐡 / (2↑𝑛)) ∈ ℝ)
10692, 105fsumrecl 15626 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛)) ∈ ℝ)
10796, 106readdcld 11191 . . 3 (πœ‘ β†’ (Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) + Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛))) ∈ ℝ)
108 ovoliun.r . . . 4 (πœ‘ β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
109108, 98readdcld 11191 . . 3 (πœ‘ β†’ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ∈ ℝ)
110 relxp 5656 . . . . . . . . . . . . . . 15 Rel ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))
111 relres 5971 . . . . . . . . . . . . . . 15 Rel ((𝐽 β€œ (1...𝐾)) β†Ύ {𝑛})
112 elsni 4608 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ {𝑛} β†’ π‘₯ = 𝑛)
113112opeq1d 4841 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ {𝑛} β†’ ⟨π‘₯, π‘¦βŸ© = βŸ¨π‘›, π‘¦βŸ©)
114113eleq1d 2823 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ {𝑛} β†’ (⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)) ↔ βŸ¨π‘›, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾))))
115 vex 3452 . . . . . . . . . . . . . . . . . . 19 𝑛 ∈ V
116 vex 3452 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
117115, 116elimasn 6046 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) ↔ βŸ¨π‘›, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)))
118114, 117bitr4di 289 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ {𝑛} β†’ (⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)) ↔ 𝑦 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})))
119118pm5.32i 576 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ {𝑛} ∧ ⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾))) ↔ (π‘₯ ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})))
120116opelresi 5950 . . . . . . . . . . . . . . . 16 (⟨π‘₯, π‘¦βŸ© ∈ ((𝐽 β€œ (1...𝐾)) β†Ύ {𝑛}) ↔ (π‘₯ ∈ {𝑛} ∧ ⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾))))
121 opelxp 5674 . . . . . . . . . . . . . . . 16 (⟨π‘₯, π‘¦βŸ© ∈ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ↔ (π‘₯ ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})))
122119, 120, 1213bitr4ri 304 . . . . . . . . . . . . . . 15 (⟨π‘₯, π‘¦βŸ© ∈ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ↔ ⟨π‘₯, π‘¦βŸ© ∈ ((𝐽 β€œ (1...𝐾)) β†Ύ {𝑛}))
123110, 111, 122eqrelriiv 5751 . . . . . . . . . . . . . 14 ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = ((𝐽 β€œ (1...𝐾)) β†Ύ {𝑛})
124 df-res 5650 . . . . . . . . . . . . . 14 ((𝐽 β€œ (1...𝐾)) β†Ύ {𝑛}) = ((𝐽 β€œ (1...𝐾)) ∩ ({𝑛} Γ— V))
125123, 124eqtri 2765 . . . . . . . . . . . . 13 ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = ((𝐽 β€œ (1...𝐾)) ∩ ({𝑛} Γ— V))
126125a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = ((𝐽 β€œ (1...𝐾)) ∩ ({𝑛} Γ— V)))
127126iuneq2dv 4983 . . . . . . . . . . 11 (πœ‘ β†’ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = βˆͺ 𝑛 ∈ (1...𝐿)((𝐽 β€œ (1...𝐾)) ∩ ({𝑛} Γ— V)))
128 iunin2 5036 . . . . . . . . . . 11 βˆͺ 𝑛 ∈ (1...𝐿)((𝐽 β€œ (1...𝐾)) ∩ ({𝑛} Γ— V)) = ((𝐽 β€œ (1...𝐾)) ∩ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V))
129127, 128eqtrdi 2793 . . . . . . . . . 10 (πœ‘ β†’ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = ((𝐽 β€œ (1...𝐾)) ∩ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V)))
130 relxp 5656 . . . . . . . . . . . . . 14 Rel (β„• Γ— β„•)
131 relss 5742 . . . . . . . . . . . . . 14 ((𝐽 β€œ (1...𝐾)) βŠ† (β„• Γ— β„•) β†’ (Rel (β„• Γ— β„•) β†’ Rel (𝐽 β€œ (1...𝐾))))
13222, 130, 131mpisyl 21 . . . . . . . . . . . . 13 (πœ‘ β†’ Rel (𝐽 β€œ (1...𝐾)))
133 ovoliun.l2 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘€ ∈ (1...𝐾)(1st β€˜(π½β€˜π‘€)) ≀ 𝐿)
13420ffnd 6674 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 Fn β„•)
135 fveq2 6847 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (π½β€˜π‘€) β†’ (1st β€˜π‘—) = (1st β€˜(π½β€˜π‘€)))
136135breq1d 5120 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (π½β€˜π‘€) β†’ ((1st β€˜π‘—) ≀ 𝐿 ↔ (1st β€˜(π½β€˜π‘€)) ≀ 𝐿))
137136ralima 7193 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 Fn β„• ∧ (1...𝐾) βŠ† β„•) β†’ (βˆ€π‘— ∈ (𝐽 β€œ (1...𝐾))(1st β€˜π‘—) ≀ 𝐿 ↔ βˆ€π‘€ ∈ (1...𝐾)(1st β€˜(π½β€˜π‘€)) ≀ 𝐿))
138134, 11, 137sylancl 587 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (βˆ€π‘— ∈ (𝐽 β€œ (1...𝐾))(1st β€˜π‘—) ≀ 𝐿 ↔ βˆ€π‘€ ∈ (1...𝐾)(1st β€˜(π½β€˜π‘€)) ≀ 𝐿))
139133, 138mpbird 257 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ βˆ€π‘— ∈ (𝐽 β€œ (1...𝐾))(1st β€˜π‘—) ≀ 𝐿)
140139r19.21bi 3237 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (1st β€˜π‘—) ≀ 𝐿)
14125, 69eleqtrdi 2848 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (1st β€˜π‘—) ∈ (β„€β‰₯β€˜1))
142 ovoliun.l1 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐿 ∈ β„€)
143142adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ 𝐿 ∈ β„€)
144 elfz5 13440 . . . . . . . . . . . . . . . . . 18 (((1st β€˜π‘—) ∈ (β„€β‰₯β€˜1) ∧ 𝐿 ∈ β„€) β†’ ((1st β€˜π‘—) ∈ (1...𝐿) ↔ (1st β€˜π‘—) ≀ 𝐿))
145141, 143, 144syl2anc 585 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ ((1st β€˜π‘—) ∈ (1...𝐿) ↔ (1st β€˜π‘—) ≀ 𝐿))
146140, 145mpbird 257 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (1st β€˜π‘—) ∈ (1...𝐿))
147146ralrimiva 3144 . . . . . . . . . . . . . . 15 (πœ‘ β†’ βˆ€π‘— ∈ (𝐽 β€œ (1...𝐾))(1st β€˜π‘—) ∈ (1...𝐿))
148 vex 3452 . . . . . . . . . . . . . . . . . 18 π‘₯ ∈ V
149148, 116op1std 7936 . . . . . . . . . . . . . . . . 17 (𝑗 = ⟨π‘₯, π‘¦βŸ© β†’ (1st β€˜π‘—) = π‘₯)
150149eleq1d 2823 . . . . . . . . . . . . . . . 16 (𝑗 = ⟨π‘₯, π‘¦βŸ© β†’ ((1st β€˜π‘—) ∈ (1...𝐿) ↔ π‘₯ ∈ (1...𝐿)))
151150rspccv 3581 . . . . . . . . . . . . . . 15 (βˆ€π‘— ∈ (𝐽 β€œ (1...𝐾))(1st β€˜π‘—) ∈ (1...𝐿) β†’ (⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)) β†’ π‘₯ ∈ (1...𝐿)))
152147, 151syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)) β†’ π‘₯ ∈ (1...𝐿)))
153 opelxp 5674 . . . . . . . . . . . . . . 15 (⟨π‘₯, π‘¦βŸ© ∈ (βˆͺ 𝑛 ∈ (1...𝐿){𝑛} Γ— V) ↔ (π‘₯ ∈ βˆͺ 𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V))
154116biantru 531 . . . . . . . . . . . . . . 15 (π‘₯ ∈ βˆͺ 𝑛 ∈ (1...𝐿){𝑛} ↔ (π‘₯ ∈ βˆͺ 𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V))
155 iunid 5025 . . . . . . . . . . . . . . . 16 βˆͺ 𝑛 ∈ (1...𝐿){𝑛} = (1...𝐿)
156155eleq2i 2830 . . . . . . . . . . . . . . 15 (π‘₯ ∈ βˆͺ 𝑛 ∈ (1...𝐿){𝑛} ↔ π‘₯ ∈ (1...𝐿))
157153, 154, 1563bitr2i 299 . . . . . . . . . . . . . 14 (⟨π‘₯, π‘¦βŸ© ∈ (βˆͺ 𝑛 ∈ (1...𝐿){𝑛} Γ— V) ↔ π‘₯ ∈ (1...𝐿))
158152, 157syl6ibr 252 . . . . . . . . . . . . 13 (πœ‘ β†’ (⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)) β†’ ⟨π‘₯, π‘¦βŸ© ∈ (βˆͺ 𝑛 ∈ (1...𝐿){𝑛} Γ— V)))
159132, 158relssdv 5749 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐽 β€œ (1...𝐾)) βŠ† (βˆͺ 𝑛 ∈ (1...𝐿){𝑛} Γ— V))
160 xpiundir 5708 . . . . . . . . . . . 12 (βˆͺ 𝑛 ∈ (1...𝐿){𝑛} Γ— V) = βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V)
161159, 160sseqtrdi 3999 . . . . . . . . . . 11 (πœ‘ β†’ (𝐽 β€œ (1...𝐾)) βŠ† βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V))
162 df-ss 3932 . . . . . . . . . . 11 ((𝐽 β€œ (1...𝐾)) βŠ† βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V) ↔ ((𝐽 β€œ (1...𝐾)) ∩ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V)) = (𝐽 β€œ (1...𝐾)))
163161, 162sylib 217 . . . . . . . . . 10 (πœ‘ β†’ ((𝐽 β€œ (1...𝐾)) ∩ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V)) = (𝐽 β€œ (1...𝐾)))
164129, 163eqtrd 2777 . . . . . . . . 9 (πœ‘ β†’ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = (𝐽 β€œ (1...𝐾)))
165164, 90eqeltrd 2838 . . . . . . . 8 (πœ‘ β†’ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin)
166 ssiun2 5012 . . . . . . . 8 (𝑛 ∈ (1...𝐿) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) βŠ† βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})))
167 ssfi 9124 . . . . . . . 8 ((βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin ∧ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) βŠ† βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin)
168165, 166, 167syl2an 597 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin)
169 2ndconst 8038 . . . . . . . . . 10 (𝑛 ∈ V β†’ (2nd β†Ύ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))):({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))–1-1-ontoβ†’((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))
170169elv 3454 . . . . . . . . 9 (2nd β†Ύ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))):({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))–1-1-ontoβ†’((𝐽 β€œ (1...𝐾)) β€œ {𝑛})
171 f1oeng 8918 . . . . . . . . 9 ((({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin ∧ (2nd β†Ύ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))):({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))–1-1-ontoβ†’((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) β‰ˆ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))
172168, 170, 171sylancl 587 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) β‰ˆ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))
173172ensymd 8952 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) β‰ˆ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})))
174 enfii 9140 . . . . . . 7 ((({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin ∧ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) β‰ˆ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) ∈ Fin)
175168, 173, 174syl2anc 585 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) ∈ Fin)
176 ffvelcdm 7037 . . . . . . . . . . . . . 14 ((𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
17716, 93, 176syl2an 597 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (πΉβ€˜π‘›) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
178 elovolmlem 24854 . . . . . . . . . . . . 13 ((πΉβ€˜π‘›) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
179177, 178sylib 217 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
180179adantrr 716 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
181 imassrn 6029 . . . . . . . . . . . . . 14 ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) βŠ† ran (𝐽 β€œ (1...𝐾))
18222adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (𝐽 β€œ (1...𝐾)) βŠ† (β„• Γ— β„•))
183 rnss 5899 . . . . . . . . . . . . . . . 16 ((𝐽 β€œ (1...𝐾)) βŠ† (β„• Γ— β„•) β†’ ran (𝐽 β€œ (1...𝐾)) βŠ† ran (β„• Γ— β„•))
184182, 183syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran (𝐽 β€œ (1...𝐾)) βŠ† ran (β„• Γ— β„•))
185 rnxpid 6130 . . . . . . . . . . . . . . 15 ran (β„• Γ— β„•) = β„•
186184, 185sseqtrdi 3999 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran (𝐽 β€œ (1...𝐾)) βŠ† β„•)
187181, 186sstrid 3960 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) βŠ† β„•)
188187sseld 3948 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) β†’ 𝑖 ∈ β„•))
189188impr 456 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ 𝑖 ∈ β„•)
190180, 189ffvelcdmd 7041 . . . . . . . . . 10 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ((πΉβ€˜π‘›)β€˜π‘–) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
191190elin2d 4164 . . . . . . . . 9 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ((πΉβ€˜π‘›)β€˜π‘–) ∈ (ℝ Γ— ℝ))
192 xp2nd 7959 . . . . . . . . 9 (((πΉβ€˜π‘›)β€˜π‘–) ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) ∈ ℝ)
193191, 192syl 17 . . . . . . . 8 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ (2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) ∈ ℝ)
194 xp1st 7958 . . . . . . . . 9 (((πΉβ€˜π‘›)β€˜π‘–) ∈ (ℝ Γ— ℝ) β†’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–)) ∈ ℝ)
195191, 194syl 17 . . . . . . . 8 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–)) ∈ ℝ)
196193, 195resubcld 11590 . . . . . . 7 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ ℝ)
197196anassrs 469 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) β†’ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ ℝ)
198175, 197fsumrecl 15626 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ ℝ)
19998, 102, 104syl2an 597 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐡 / (2↑𝑛)) ∈ ℝ)
20094, 199readdcld 11191 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))) ∈ ℝ)
20193, 200sylan2 594 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))) ∈ ℝ)
202 eqid 2737 . . . . . . . . . . . 12 ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›)) = ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))
203 ovoliun.s . . . . . . . . . . . 12 𝑆 = seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›)))
204202, 203ovolsf 24852 . . . . . . . . . . 11 ((πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ 𝑆:β„•βŸΆ(0[,)+∞))
205179, 204syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 𝑆:β„•βŸΆ(0[,)+∞))
206205frnd 6681 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran 𝑆 βŠ† (0[,)+∞))
207 icossxr 13356 . . . . . . . . 9 (0[,)+∞) βŠ† ℝ*
208206, 207sstrdi 3961 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran 𝑆 βŠ† ℝ*)
209 supxrcl 13241 . . . . . . . 8 (ran 𝑆 βŠ† ℝ* β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
210208, 209syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
211 mnfxr 11219 . . . . . . . . 9 -∞ ∈ ℝ*
212211a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ -∞ ∈ ℝ*)
21395rexrd 11212 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (vol*β€˜π΄) ∈ ℝ*)
21495mnfltd 13052 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ -∞ < (vol*β€˜π΄))
215 ovoliun.x1 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
21693, 215sylan2 594 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
217203ovollb 24859 . . . . . . . . 9 (((πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›))) β†’ (vol*β€˜π΄) ≀ sup(ran 𝑆, ℝ*, < ))
218179, 216, 217syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (vol*β€˜π΄) ≀ sup(ran 𝑆, ℝ*, < ))
219212, 213, 210, 214, 218xrltletrd 13087 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ -∞ < sup(ran 𝑆, ℝ*, < ))
220 ovoliun.x2 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
22193, 220sylan2 594 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
222 xrre 13095 . . . . . . 7 (((sup(ran 𝑆, ℝ*, < ) ∈ ℝ* ∧ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))) β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
223210, 201, 219, 221, 222syl22anc 838 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
224 1zzd 12541 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 1 ∈ β„€)
225202ovolfsval 24850 . . . . . . . . 9 (((πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ 𝑖 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))β€˜π‘–) = ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))))
226179, 225sylan 581 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))β€˜π‘–) = ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))))
227202ovolfsf 24851 . . . . . . . . . . . . 13 ((πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›)):β„•βŸΆ(0[,)+∞))
228179, 227syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›)):β„•βŸΆ(0[,)+∞))
229228ffvelcdmda 7040 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))β€˜π‘–) ∈ (0[,)+∞))
230226, 229eqeltrrd 2839 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ β„•) β†’ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ (0[,)+∞))
231 elrege0 13378 . . . . . . . . . 10 (((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ (0[,)+∞) ↔ (((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ ℝ ∧ 0 ≀ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–)))))
232230, 231sylib 217 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ β„•) β†’ (((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ ℝ ∧ 0 ≀ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–)))))
233232simpld 496 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ β„•) β†’ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ ℝ)
234232simprd 497 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ β„•) β†’ 0 ≀ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))))
235 supxrub 13250 . . . . . . . . . . . . . . 15 ((ran 𝑆 βŠ† ℝ* ∧ 𝑧 ∈ ran 𝑆) β†’ 𝑧 ≀ sup(ran 𝑆, ℝ*, < ))
236208, 235sylan 581 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑧 ∈ ran 𝑆) β†’ 𝑧 ≀ sup(ran 𝑆, ℝ*, < ))
237236ralrimiva 3144 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ sup(ran 𝑆, ℝ*, < ))
238 brralrspcev 5170 . . . . . . . . . . . . 13 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ sup(ran 𝑆, ℝ*, < )) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯)
239223, 237, 238syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯)
240205ffnd 6674 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 𝑆 Fn β„•)
241 breq1 5113 . . . . . . . . . . . . . . 15 (𝑧 = (π‘†β€˜π‘˜) β†’ (𝑧 ≀ π‘₯ ↔ (π‘†β€˜π‘˜) ≀ π‘₯))
242241ralrn 7043 . . . . . . . . . . . . . 14 (𝑆 Fn β„• β†’ (βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯ ↔ βˆ€π‘˜ ∈ β„• (π‘†β€˜π‘˜) ≀ π‘₯))
243240, 242syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯ ↔ βˆ€π‘˜ ∈ β„• (π‘†β€˜π‘˜) ≀ π‘₯))
244243rexbidv 3176 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯ ↔ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (π‘†β€˜π‘˜) ≀ π‘₯))
245239, 244mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (π‘†β€˜π‘˜) ≀ π‘₯)
24669, 203, 224, 226, 233, 234, 245isumsup2 15738 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
247203, 246eqbrtrrid 5146 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))) ⇝ sup(ran 𝑆, ℝ, < ))
248 climrel 15381 . . . . . . . . . 10 Rel ⇝
249248releldmi 5908 . . . . . . . . 9 (seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))) ⇝ sup(ran 𝑆, ℝ, < ) β†’ seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))) ∈ dom ⇝ )
250247, 249syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))) ∈ dom ⇝ )
25169, 224, 175, 187, 226, 233, 234, 250isumless 15737 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ≀ Σ𝑖 ∈ β„• ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))))
25269, 203, 224, 226, 233, 234, 245isumsup 15739 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ β„• ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) = sup(ran 𝑆, ℝ, < ))
253 rge0ssre 13380 . . . . . . . . . 10 (0[,)+∞) βŠ† ℝ
254206, 253sstrdi 3961 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran 𝑆 βŠ† ℝ)
255 1nn 12171 . . . . . . . . . . . 12 1 ∈ β„•
256205fdmd 6684 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ dom 𝑆 = β„•)
257255, 256eleqtrrid 2845 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 1 ∈ dom 𝑆)
258257ne0d 4300 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ dom 𝑆 β‰  βˆ…)
259 dm0rn0 5885 . . . . . . . . . . 11 (dom 𝑆 = βˆ… ↔ ran 𝑆 = βˆ…)
260259necon3bii 2997 . . . . . . . . . 10 (dom 𝑆 β‰  βˆ… ↔ ran 𝑆 β‰  βˆ…)
261258, 260sylib 217 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran 𝑆 β‰  βˆ…)
262 supxrre 13253 . . . . . . . . 9 ((ran 𝑆 βŠ† ℝ ∧ ran 𝑆 β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯) β†’ sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
263254, 261, 239, 262syl3anc 1372 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
264252, 263eqtr4d 2780 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ β„• ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) = sup(ran 𝑆, ℝ*, < ))
265251, 264breqtrd 5136 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ≀ sup(ran 𝑆, ℝ*, < ))
266198, 223, 201, 265, 221letrd 11319 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
26792, 198, 201, 266fsumle 15691 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ≀ Σ𝑛 ∈ (1...𝐿)((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
268 vex 3452 . . . . . . . . . . 11 𝑖 ∈ V
269115, 268op1std 7936 . . . . . . . . . 10 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ (1st β€˜π‘—) = 𝑛)
270269fveq2d 6851 . . . . . . . . 9 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ (πΉβ€˜(1st β€˜π‘—)) = (πΉβ€˜π‘›))
271115, 268op2ndd 7937 . . . . . . . . 9 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ (2nd β€˜π‘—) = 𝑖)
272270, 271fveq12d 6854 . . . . . . . 8 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ ((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) = ((πΉβ€˜π‘›)β€˜π‘–))
273272fveq2d 6851 . . . . . . 7 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ (2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) = (2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)))
274272fveq2d 6851 . . . . . . 7 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) = (1st β€˜((πΉβ€˜π‘›)β€˜π‘–)))
275273, 274oveq12d 7380 . . . . . 6 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ ((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))))
276196recnd 11190 . . . . . 6 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ β„‚)
277275, 92, 175, 276fsum2d 15663 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) = Σ𝑗 ∈ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))))
278164sumeq1d 15593 . . . . 5 (πœ‘ β†’ Σ𝑗 ∈ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))))
279277, 278eqtrd 2777 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) = Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))))
28095recnd 11190 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (vol*β€˜π΄) ∈ β„‚)
281105recnd 11190 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (𝐡 / (2↑𝑛)) ∈ β„‚)
28292, 280, 281fsumadd 15632 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)((vol*β€˜π΄) + (𝐡 / (2↑𝑛))) = (Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) + Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛))))
283267, 279, 2823brtr3d 5141 . . 3 (πœ‘ β†’ Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) ≀ (Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) + Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛))))
284 1zzd 12541 . . . . . . . . 9 (πœ‘ β†’ 1 ∈ β„€)
285 simpr 486 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
286 ovoliun.g . . . . . . . . . . . 12 𝐺 = (𝑛 ∈ β„• ↦ (vol*β€˜π΄))
287286fvmpt2 6964 . . . . . . . . . . 11 ((𝑛 ∈ β„• ∧ (vol*β€˜π΄) ∈ ℝ) β†’ (πΊβ€˜π‘›) = (vol*β€˜π΄))
288285, 94, 287syl2anc 585 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΊβ€˜π‘›) = (vol*β€˜π΄))
289288, 94eqeltrd 2838 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΊβ€˜π‘›) ∈ ℝ)
29069, 284, 289serfre 13944 . . . . . . . 8 (πœ‘ β†’ seq1( + , 𝐺):β„•βŸΆβ„)
291 ovoliun.t . . . . . . . . 9 𝑇 = seq1( + , 𝐺)
292291feq1i 6664 . . . . . . . 8 (𝑇:β„•βŸΆβ„ ↔ seq1( + , 𝐺):β„•βŸΆβ„)
293290, 292sylibr 233 . . . . . . 7 (πœ‘ β†’ 𝑇:β„•βŸΆβ„)
294293frnd 6681 . . . . . 6 (πœ‘ β†’ ran 𝑇 βŠ† ℝ)
295 ressxr 11206 . . . . . 6 ℝ βŠ† ℝ*
296294, 295sstrdi 3961 . . . . 5 (πœ‘ β†’ ran 𝑇 βŠ† ℝ*)
29793, 288sylan2 594 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (πΊβ€˜π‘›) = (vol*β€˜π΄))
298 1red 11163 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ ℝ)
299 ffvelcdm 7037 . . . . . . . . . . . . 13 ((𝐽:β„•βŸΆ(β„• Γ— β„•) ∧ 1 ∈ β„•) β†’ (π½β€˜1) ∈ (β„• Γ— β„•))
30020, 255, 299sylancl 587 . . . . . . . . . . . 12 (πœ‘ β†’ (π½β€˜1) ∈ (β„• Γ— β„•))
301 xp1st 7958 . . . . . . . . . . . 12 ((π½β€˜1) ∈ (β„• Γ— β„•) β†’ (1st β€˜(π½β€˜1)) ∈ β„•)
302300, 301syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (1st β€˜(π½β€˜1)) ∈ β„•)
303302nnred 12175 . . . . . . . . . 10 (πœ‘ β†’ (1st β€˜(π½β€˜1)) ∈ ℝ)
304142zred 12614 . . . . . . . . . 10 (πœ‘ β†’ 𝐿 ∈ ℝ)
305302nnge1d 12208 . . . . . . . . . 10 (πœ‘ β†’ 1 ≀ (1st β€˜(π½β€˜1)))
306 2fveq3 6852 . . . . . . . . . . . 12 (𝑀 = 1 β†’ (1st β€˜(π½β€˜π‘€)) = (1st β€˜(π½β€˜1)))
307306breq1d 5120 . . . . . . . . . . 11 (𝑀 = 1 β†’ ((1st β€˜(π½β€˜π‘€)) ≀ 𝐿 ↔ (1st β€˜(π½β€˜1)) ≀ 𝐿))
308 eluzfz1 13455 . . . . . . . . . . . 12 (𝐾 ∈ (β„€β‰₯β€˜1) β†’ 1 ∈ (1...𝐾))
30970, 308syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 1 ∈ (1...𝐾))
310307, 133, 309rspcdva 3585 . . . . . . . . . 10 (πœ‘ β†’ (1st β€˜(π½β€˜1)) ≀ 𝐿)
311298, 303, 304, 305, 310letrd 11319 . . . . . . . . 9 (πœ‘ β†’ 1 ≀ 𝐿)
312 elnnz1 12536 . . . . . . . . 9 (𝐿 ∈ β„• ↔ (𝐿 ∈ β„€ ∧ 1 ≀ 𝐿))
313142, 311, 312sylanbrc 584 . . . . . . . 8 (πœ‘ β†’ 𝐿 ∈ β„•)
314313, 69eleqtrdi 2848 . . . . . . 7 (πœ‘ β†’ 𝐿 ∈ (β„€β‰₯β€˜1))
315297, 314, 280fsumser 15622 . . . . . 6 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) = (seq1( + , 𝐺)β€˜πΏ))
316 seqfn 13925 . . . . . . . . 9 (1 ∈ β„€ β†’ seq1( + , 𝐺) Fn (β„€β‰₯β€˜1))
317284, 316syl 17 . . . . . . . 8 (πœ‘ β†’ seq1( + , 𝐺) Fn (β„€β‰₯β€˜1))
318 fnfvelrn 7036 . . . . . . . 8 ((seq1( + , 𝐺) Fn (β„€β‰₯β€˜1) ∧ 𝐿 ∈ (β„€β‰₯β€˜1)) β†’ (seq1( + , 𝐺)β€˜πΏ) ∈ ran seq1( + , 𝐺))
319317, 314, 318syl2anc 585 . . . . . . 7 (πœ‘ β†’ (seq1( + , 𝐺)β€˜πΏ) ∈ ran seq1( + , 𝐺))
320291rneqi 5897 . . . . . . 7 ran 𝑇 = ran seq1( + , 𝐺)
321319, 320eleqtrrdi 2849 . . . . . 6 (πœ‘ β†’ (seq1( + , 𝐺)β€˜πΏ) ∈ ran 𝑇)
322315, 321eqeltrd 2838 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) ∈ ran 𝑇)
323 supxrub 13250 . . . . 5 ((ran 𝑇 βŠ† ℝ* ∧ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) ∈ ran 𝑇) β†’ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) ≀ sup(ran 𝑇, ℝ*, < ))
324296, 322, 323syl2anc 585 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) ≀ sup(ran 𝑇, ℝ*, < ))
32598recnd 11190 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ β„‚)
326 geo2sum 15765 . . . . . 6 ((𝐿 ∈ β„• ∧ 𝐡 ∈ β„‚) β†’ Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛)) = (𝐡 βˆ’ (𝐡 / (2↑𝐿))))
327313, 325, 326syl2anc 585 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛)) = (𝐡 βˆ’ (𝐡 / (2↑𝐿))))
328313nnnn0d 12480 . . . . . . . . . 10 (πœ‘ β†’ 𝐿 ∈ β„•0)
329 nnexpcl 13987 . . . . . . . . . 10 ((2 ∈ β„• ∧ 𝐿 ∈ β„•0) β†’ (2↑𝐿) ∈ β„•)
33099, 328, 329sylancr 588 . . . . . . . . 9 (πœ‘ β†’ (2↑𝐿) ∈ β„•)
331330nnrpd 12962 . . . . . . . 8 (πœ‘ β†’ (2↑𝐿) ∈ ℝ+)
33297, 331rpdivcld 12981 . . . . . . 7 (πœ‘ β†’ (𝐡 / (2↑𝐿)) ∈ ℝ+)
333332rpge0d 12968 . . . . . 6 (πœ‘ β†’ 0 ≀ (𝐡 / (2↑𝐿)))
33498, 330nndivred 12214 . . . . . . 7 (πœ‘ β†’ (𝐡 / (2↑𝐿)) ∈ ℝ)
33598, 334subge02d 11754 . . . . . 6 (πœ‘ β†’ (0 ≀ (𝐡 / (2↑𝐿)) ↔ (𝐡 βˆ’ (𝐡 / (2↑𝐿))) ≀ 𝐡))
336333, 335mpbid 231 . . . . 5 (πœ‘ β†’ (𝐡 βˆ’ (𝐡 / (2↑𝐿))) ≀ 𝐡)
337327, 336eqbrtrd 5132 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛)) ≀ 𝐡)
33896, 106, 108, 98, 324, 337le2addd 11781 . . 3 (πœ‘ β†’ (Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) + Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛))) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
33991, 107, 109, 283, 338letrd 11319 . 2 (πœ‘ β†’ Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
34085, 339eqbrtrrd 5134 1 (πœ‘ β†’ (π‘ˆβ€˜πΎ) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  βˆƒwrex 3074  Vcvv 3448   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  {csn 4591  βŸ¨cop 4597  βˆͺ cuni 4870  βˆͺ ciun 4959   class class class wbr 5110   ↦ cmpt 5193   Γ— cxp 5636  dom cdm 5638  ran crn 5639   β†Ύ cres 5640   β€œ cima 5641   ∘ ccom 5642  Rel wrel 5643   Fn wfn 6496  βŸΆwf 6497  β€“1-1β†’wf1 6498  β€“1-1-ontoβ†’wf1o 6500  β€˜cfv 6501  (class class class)co 7362  1st c1st 7924  2nd c2nd 7925   ↑m cmap 8772   β‰ˆ cen 8887  Fincfn 8890  supcsup 9383  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061  +∞cpnf 11193  -∞cmnf 11194  β„*cxr 11195   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392   / cdiv 11819  β„•cn 12160  2c2 12215  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  (,)cioo 13271  [,)cico 13273  ...cfz 13431  seqcseq 13913  β†‘cexp 13974  abscabs 15126   ⇝ cli 15373  Ξ£csu 15577  vol*covol 24842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-ioo 13275  df-ico 13277  df-fz 13432  df-fzo 13575  df-fl 13704  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-rlim 15378  df-sum 15578  df-ovol 24844
This theorem is referenced by:  ovoliunlem2  24883
  Copyright terms: Public domain W3C validator