MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovoliunlem1 Structured version   Visualization version   GIF version
Theorem ovoliunlem1 25010
Description: Lemma for ovoliun 25013. (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 6893 . . . . . . . 8 (𝑗 = (π½β€˜π‘š) β†’ (πΉβ€˜(1st β€˜π‘—)) = (πΉβ€˜(1st β€˜(π½β€˜π‘š))))
2 fveq2 6888 . . . . . . . 8 (𝑗 = (π½β€˜π‘š) β†’ (2nd β€˜π‘—) = (2nd β€˜(π½β€˜π‘š)))
31, 2fveq12d 6895 . . . . . . 7 (𝑗 = (π½β€˜π‘š) β†’ ((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) = ((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))
43fveq2d 6892 . . . . . 6 (𝑗 = (π½β€˜π‘š) β†’ (2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) = (2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))))
53fveq2d 6892 . . . . . 6 (𝑗 = (π½β€˜π‘š) β†’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) = (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))))
64, 5oveq12d 7423 . . . . 5 (𝑗 = (π½β€˜π‘š) β†’ ((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = ((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))))
7 fzfid 13934 . . . . 5 (πœ‘ β†’ (1...𝐾) ∈ Fin)
8 ovoliun.j . . . . . . 7 (πœ‘ β†’ 𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•))
9 f1of1 6829 . . . . . . 7 (𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•) β†’ 𝐽:ℕ–1-1β†’(β„• Γ— β„•))
108, 9syl 17 . . . . . 6 (πœ‘ β†’ 𝐽:ℕ–1-1β†’(β„• Γ— β„•))
11 fz1ssnn 13528 . . . . . 6 (1...𝐾) βŠ† β„•
12 f1ores 6844 . . . . . 6 ((𝐽:ℕ–1-1β†’(β„• Γ— β„•) ∧ (1...𝐾) βŠ† β„•) β†’ (𝐽 β†Ύ (1...𝐾)):(1...𝐾)–1-1-ontoβ†’(𝐽 β€œ (1...𝐾)))
1310, 11, 12sylancl 586 . . . . 5 (πœ‘ β†’ (𝐽 β†Ύ (1...𝐾)):(1...𝐾)–1-1-ontoβ†’(𝐽 β€œ (1...𝐾)))
14 fvres 6907 . . . . . 6 (π‘š ∈ (1...𝐾) β†’ ((𝐽 β†Ύ (1...𝐾))β€˜π‘š) = (π½β€˜π‘š))
1514adantl 482 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ ((𝐽 β†Ύ (1...𝐾))β€˜π‘š) = (π½β€˜π‘š))
16 ovoliun.f . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
1716adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
18 imassrn 6068 . . . . . . . . . . . . . . 15 (𝐽 β€œ (1...𝐾)) βŠ† ran 𝐽
19 f1of 6830 . . . . . . . . . . . . . . . . 17 (𝐽:ℕ–1-1-ontoβ†’(β„• Γ— β„•) β†’ 𝐽:β„•βŸΆ(β„• Γ— β„•))
208, 19syl 17 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐽:β„•βŸΆ(β„• Γ— β„•))
2120frnd 6722 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ran 𝐽 βŠ† (β„• Γ— β„•))
2218, 21sstrid 3992 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐽 β€œ (1...𝐾)) βŠ† (β„• Γ— β„•))
2322sselda 3981 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ 𝑗 ∈ (β„• Γ— β„•))
24 xp1st 8003 . . . . . . . . . . . . 13 (𝑗 ∈ (β„• Γ— β„•) β†’ (1st β€˜π‘—) ∈ β„•)
2523, 24syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (1st β€˜π‘—) ∈ β„•)
2617, 25ffvelcdmd 7084 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (πΉβ€˜(1st β€˜π‘—)) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
27 elovolmlem 24982 . . . . . . . . . . 11 ((πΉβ€˜(1st β€˜π‘—)) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ (πΉβ€˜(1st β€˜π‘—)):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
2826, 27sylib 217 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (πΉβ€˜(1st β€˜π‘—)):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
29 xp2nd 8004 . . . . . . . . . . 11 (𝑗 ∈ (β„• Γ— β„•) β†’ (2nd β€˜π‘—) ∈ β„•)
3023, 29syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (2nd β€˜π‘—) ∈ β„•)
3128, 30ffvelcdmd 7084 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ ((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
3231elin2d 4198 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ ((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) ∈ (ℝ Γ— ℝ))
33 xp2nd 8004 . . . . . . . 8 (((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) ∈ ℝ)
3432, 33syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) ∈ ℝ)
35 xp1st 8003 . . . . . . . 8 (((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) ∈ (ℝ Γ— ℝ) β†’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) ∈ ℝ)
3632, 35syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) ∈ ℝ)
3734, 36resubcld 11638 . . . . . 6 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ ((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) ∈ ℝ)
3837recnd 11238 . . . . 5 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ ((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) ∈ β„‚)
396, 7, 13, 15, 38fsumf1o 15665 . . . 4 (πœ‘ β†’ Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = Ξ£π‘š ∈ (1...𝐾)((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))))
4016adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
4120ffvelcdmda 7083 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π½β€˜π‘˜) ∈ (β„• Γ— β„•))
42 xp1st 8003 . . . . . . . . . . . 12 ((π½β€˜π‘˜) ∈ (β„• Γ— β„•) β†’ (1st β€˜(π½β€˜π‘˜)) ∈ β„•)
4341, 42syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1st β€˜(π½β€˜π‘˜)) ∈ β„•)
4440, 43ffvelcdmd 7084 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
45 elovolmlem 24982 . . . . . . . . . 10 ((πΉβ€˜(1st β€˜(π½β€˜π‘˜))) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
4644, 45sylib 217 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
47 xp2nd 8004 . . . . . . . . . 10 ((π½β€˜π‘˜) ∈ (β„• Γ— β„•) β†’ (2nd β€˜(π½β€˜π‘˜)) ∈ β„•)
4841, 47syl 17 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (2nd β€˜(π½β€˜π‘˜)) ∈ β„•)
4946, 48ffvelcdmd 7084 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
50 ovoliun.h . . . . . . . 8 𝐻 = (π‘˜ ∈ β„• ↦ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))))
5149, 50fmptd 7110 . . . . . . 7 (πœ‘ β†’ 𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
52 elfznn 13526 . . . . . . 7 (π‘š ∈ (1...𝐾) β†’ π‘š ∈ β„•)
53 eqid 2732 . . . . . . . 8 ((abs ∘ βˆ’ ) ∘ 𝐻) = ((abs ∘ βˆ’ ) ∘ 𝐻)
5453ovolfsval 24978 . . . . . . 7 ((𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ π‘š ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘š) = ((2nd β€˜(π»β€˜π‘š)) βˆ’ (1st β€˜(π»β€˜π‘š))))
5551, 52, 54syl2an 596 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘š) = ((2nd β€˜(π»β€˜π‘š)) βˆ’ (1st β€˜(π»β€˜π‘š))))
5652adantl 482 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ π‘š ∈ β„•)
57 2fveq3 6893 . . . . . . . . . . . 12 (π‘˜ = π‘š β†’ (1st β€˜(π½β€˜π‘˜)) = (1st β€˜(π½β€˜π‘š)))
5857fveq2d 6892 . . . . . . . . . . 11 (π‘˜ = π‘š β†’ (πΉβ€˜(1st β€˜(π½β€˜π‘˜))) = (πΉβ€˜(1st β€˜(π½β€˜π‘š))))
59 2fveq3 6893 . . . . . . . . . . 11 (π‘˜ = π‘š β†’ (2nd β€˜(π½β€˜π‘˜)) = (2nd β€˜(π½β€˜π‘š)))
6058, 59fveq12d 6895 . . . . . . . . . 10 (π‘˜ = π‘š β†’ ((πΉβ€˜(1st β€˜(π½β€˜π‘˜)))β€˜(2nd β€˜(π½β€˜π‘˜))) = ((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))
61 fvex 6901 . . . . . . . . . 10 ((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))) ∈ V
6260, 50, 61fvmpt 6995 . . . . . . . . 9 (π‘š ∈ β„• β†’ (π»β€˜π‘š) = ((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))
6356, 62syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (π»β€˜π‘š) = ((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))
6463fveq2d 6892 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (2nd β€˜(π»β€˜π‘š)) = (2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))))
6563fveq2d 6892 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (1st β€˜(π»β€˜π‘š)) = (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))))
6664, 65oveq12d 7423 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ ((2nd β€˜(π»β€˜π‘š)) βˆ’ (1st β€˜(π»β€˜π‘š))) = ((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))))
6755, 66eqtrd 2772 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (((abs ∘ βˆ’ ) ∘ 𝐻)β€˜π‘š) = ((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))))
68 ovoliun.k . . . . . 6 (πœ‘ β†’ 𝐾 ∈ β„•)
69 nnuz 12861 . . . . . 6 β„• = (β„€β‰₯β€˜1)
7068, 69eleqtrdi 2843 . . . . 5 (πœ‘ β†’ 𝐾 ∈ (β„€β‰₯β€˜1))
71 ffvelcdm 7080 . . . . . . . . . . 11 ((𝐻:β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ π‘š ∈ β„•) β†’ (π»β€˜π‘š) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
7251, 52, 71syl2an 596 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (π»β€˜π‘š) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
7372elin2d 4198 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (π»β€˜π‘š) ∈ (ℝ Γ— ℝ))
74 xp2nd 8004 . . . . . . . . 9 ((π»β€˜π‘š) ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜(π»β€˜π‘š)) ∈ ℝ)
7573, 74syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (2nd β€˜(π»β€˜π‘š)) ∈ ℝ)
76 xp1st 8003 . . . . . . . . 9 ((π»β€˜π‘š) ∈ (ℝ Γ— ℝ) β†’ (1st β€˜(π»β€˜π‘š)) ∈ ℝ)
7773, 76syl 17 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ (1st β€˜(π»β€˜π‘š)) ∈ ℝ)
7875, 77resubcld 11638 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ ((2nd β€˜(π»β€˜π‘š)) βˆ’ (1st β€˜(π»β€˜π‘š))) ∈ ℝ)
7978recnd 11238 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ ((2nd β€˜(π»β€˜π‘š)) βˆ’ (1st β€˜(π»β€˜π‘š))) ∈ β„‚)
8066, 79eqeltrrd 2834 . . . . 5 ((πœ‘ ∧ π‘š ∈ (1...𝐾)) β†’ ((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))) ∈ β„‚)
8167, 70, 80fsumser 15672 . . . 4 (πœ‘ β†’ Ξ£π‘š ∈ (1...𝐾)((2nd β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š)))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜(π½β€˜π‘š)))β€˜(2nd β€˜(π½β€˜π‘š))))) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜πΎ))
8239, 81eqtrd 2772 . . 3 (πœ‘ β†’ Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜πΎ))
83 ovoliun.u . . . 4 π‘ˆ = seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))
8483fveq1i 6889 . . 3 (π‘ˆβ€˜πΎ) = (seq1( + , ((abs ∘ βˆ’ ) ∘ 𝐻))β€˜πΎ)
8582, 84eqtr4di 2790 . 2 (πœ‘ β†’ Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = (π‘ˆβ€˜πΎ))
86 f1oeng 8963 . . . . . . 7 (((1...𝐾) ∈ Fin ∧ (𝐽 β†Ύ (1...𝐾)):(1...𝐾)–1-1-ontoβ†’(𝐽 β€œ (1...𝐾))) β†’ (1...𝐾) β‰ˆ (𝐽 β€œ (1...𝐾)))
877, 13, 86syl2anc 584 . . . . . 6 (πœ‘ β†’ (1...𝐾) β‰ˆ (𝐽 β€œ (1...𝐾)))
8887ensymd 8997 . . . . 5 (πœ‘ β†’ (𝐽 β€œ (1...𝐾)) β‰ˆ (1...𝐾))
89 enfii 9185 . . . . 5 (((1...𝐾) ∈ Fin ∧ (𝐽 β€œ (1...𝐾)) β‰ˆ (1...𝐾)) β†’ (𝐽 β€œ (1...𝐾)) ∈ Fin)
907, 88, 89syl2anc 584 . . . 4 (πœ‘ β†’ (𝐽 β€œ (1...𝐾)) ∈ Fin)
9190, 37fsumrecl 15676 . . 3 (πœ‘ β†’ Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) ∈ ℝ)
92 fzfid 13934 . . . . 5 (πœ‘ β†’ (1...𝐿) ∈ Fin)
93 elfznn 13526 . . . . . 6 (𝑛 ∈ (1...𝐿) β†’ 𝑛 ∈ β„•)
94 ovoliun.v . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (vol*β€˜π΄) ∈ ℝ)
9593, 94sylan2 593 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (vol*β€˜π΄) ∈ ℝ)
9692, 95fsumrecl 15676 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) ∈ ℝ)
97 ovoliun.b . . . . . . 7 (πœ‘ β†’ 𝐡 ∈ ℝ+)
9897rpred 13012 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ ℝ)
99 2nn 12281 . . . . . . . 8 2 ∈ β„•
100 nnnn0 12475 . . . . . . . 8 (𝑛 ∈ β„• β†’ 𝑛 ∈ β„•0)
101 nnexpcl 14036 . . . . . . . 8 ((2 ∈ β„• ∧ 𝑛 ∈ β„•0) β†’ (2↑𝑛) ∈ β„•)
10299, 100, 101sylancr 587 . . . . . . 7 (𝑛 ∈ β„• β†’ (2↑𝑛) ∈ β„•)
10393, 102syl 17 . . . . . 6 (𝑛 ∈ (1...𝐿) β†’ (2↑𝑛) ∈ β„•)
104 nndivre 12249 . . . . . 6 ((𝐡 ∈ ℝ ∧ (2↑𝑛) ∈ β„•) β†’ (𝐡 / (2↑𝑛)) ∈ ℝ)
10598, 103, 104syl2an 596 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (𝐡 / (2↑𝑛)) ∈ ℝ)
10692, 105fsumrecl 15676 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛)) ∈ ℝ)
10796, 106readdcld 11239 . . 3 (πœ‘ β†’ (Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) + Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛))) ∈ ℝ)
108 ovoliun.r . . . 4 (πœ‘ β†’ sup(ran 𝑇, ℝ*, < ) ∈ ℝ)
109108, 98readdcld 11239 . . 3 (πœ‘ β†’ (sup(ran 𝑇, ℝ*, < ) + 𝐡) ∈ ℝ)
110 relxp 5693 . . . . . . . . . . . . . . 15 Rel ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))
111 relres 6008 . . . . . . . . . . . . . . 15 Rel ((𝐽 β€œ (1...𝐾)) β†Ύ {𝑛})
112 elsni 4644 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ {𝑛} β†’ π‘₯ = 𝑛)
113112opeq1d 4878 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ {𝑛} β†’ ⟨π‘₯, π‘¦βŸ© = βŸ¨π‘›, π‘¦βŸ©)
114113eleq1d 2818 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ {𝑛} β†’ (⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)) ↔ βŸ¨π‘›, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾))))
115 vex 3478 . . . . . . . . . . . . . . . . . . 19 𝑛 ∈ V
116 vex 3478 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
117115, 116elimasn 6085 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) ↔ βŸ¨π‘›, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)))
118114, 117bitr4di 288 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ {𝑛} β†’ (⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)) ↔ 𝑦 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})))
119118pm5.32i 575 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ {𝑛} ∧ ⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾))) ↔ (π‘₯ ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})))
120116opelresi 5987 . . . . . . . . . . . . . . . 16 (⟨π‘₯, π‘¦βŸ© ∈ ((𝐽 β€œ (1...𝐾)) β†Ύ {𝑛}) ↔ (π‘₯ ∈ {𝑛} ∧ ⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾))))
121 opelxp 5711 . . . . . . . . . . . . . . . 16 (⟨π‘₯, π‘¦βŸ© ∈ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ↔ (π‘₯ ∈ {𝑛} ∧ 𝑦 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})))
122119, 120, 1213bitr4ri 303 . . . . . . . . . . . . . . 15 (⟨π‘₯, π‘¦βŸ© ∈ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ↔ ⟨π‘₯, π‘¦βŸ© ∈ ((𝐽 β€œ (1...𝐾)) β†Ύ {𝑛}))
123110, 111, 122eqrelriiv 5788 . . . . . . . . . . . . . 14 ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = ((𝐽 β€œ (1...𝐾)) β†Ύ {𝑛})
124 df-res 5687 . . . . . . . . . . . . . 14 ((𝐽 β€œ (1...𝐾)) β†Ύ {𝑛}) = ((𝐽 β€œ (1...𝐾)) ∩ ({𝑛} Γ— V))
125123, 124eqtri 2760 . . . . . . . . . . . . 13 ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = ((𝐽 β€œ (1...𝐾)) ∩ ({𝑛} Γ— V))
126125a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = ((𝐽 β€œ (1...𝐾)) ∩ ({𝑛} Γ— V)))
127126iuneq2dv 5020 . . . . . . . . . . 11 (πœ‘ β†’ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = βˆͺ 𝑛 ∈ (1...𝐿)((𝐽 β€œ (1...𝐾)) ∩ ({𝑛} Γ— V)))
128 iunin2 5073 . . . . . . . . . . 11 βˆͺ 𝑛 ∈ (1...𝐿)((𝐽 β€œ (1...𝐾)) ∩ ({𝑛} Γ— V)) = ((𝐽 β€œ (1...𝐾)) ∩ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V))
129127, 128eqtrdi 2788 . . . . . . . . . 10 (πœ‘ β†’ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = ((𝐽 β€œ (1...𝐾)) ∩ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V)))
130 relxp 5693 . . . . . . . . . . . . . 14 Rel (β„• Γ— β„•)
131 relss 5779 . . . . . . . . . . . . . 14 ((𝐽 β€œ (1...𝐾)) βŠ† (β„• Γ— β„•) β†’ (Rel (β„• Γ— β„•) β†’ Rel (𝐽 β€œ (1...𝐾))))
13222, 130, 131mpisyl 21 . . . . . . . . . . . . 13 (πœ‘ β†’ Rel (𝐽 β€œ (1...𝐾)))
133 ovoliun.l2 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ βˆ€π‘€ ∈ (1...𝐾)(1st β€˜(π½β€˜π‘€)) ≀ 𝐿)
13420ffnd 6715 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 Fn β„•)
135 fveq2 6888 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (π½β€˜π‘€) β†’ (1st β€˜π‘—) = (1st β€˜(π½β€˜π‘€)))
136135breq1d 5157 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (π½β€˜π‘€) β†’ ((1st β€˜π‘—) ≀ 𝐿 ↔ (1st β€˜(π½β€˜π‘€)) ≀ 𝐿))
137136ralima 7236 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 Fn β„• ∧ (1...𝐾) βŠ† β„•) β†’ (βˆ€π‘— ∈ (𝐽 β€œ (1...𝐾))(1st β€˜π‘—) ≀ 𝐿 ↔ βˆ€π‘€ ∈ (1...𝐾)(1st β€˜(π½β€˜π‘€)) ≀ 𝐿))
138134, 11, 137sylancl 586 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (βˆ€π‘— ∈ (𝐽 β€œ (1...𝐾))(1st β€˜π‘—) ≀ 𝐿 ↔ βˆ€π‘€ ∈ (1...𝐾)(1st β€˜(π½β€˜π‘€)) ≀ 𝐿))
139133, 138mpbird 256 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ βˆ€π‘— ∈ (𝐽 β€œ (1...𝐾))(1st β€˜π‘—) ≀ 𝐿)
140139r19.21bi 3248 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (1st β€˜π‘—) ≀ 𝐿)
14125, 69eleqtrdi 2843 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (1st β€˜π‘—) ∈ (β„€β‰₯β€˜1))
142 ovoliun.l1 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐿 ∈ β„€)
143142adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ 𝐿 ∈ β„€)
144 elfz5 13489 . . . . . . . . . . . . . . . . . 18 (((1st β€˜π‘—) ∈ (β„€β‰₯β€˜1) ∧ 𝐿 ∈ β„€) β†’ ((1st β€˜π‘—) ∈ (1...𝐿) ↔ (1st β€˜π‘—) ≀ 𝐿))
145141, 143, 144syl2anc 584 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ ((1st β€˜π‘—) ∈ (1...𝐿) ↔ (1st β€˜π‘—) ≀ 𝐿))
146140, 145mpbird 256 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ (𝐽 β€œ (1...𝐾))) β†’ (1st β€˜π‘—) ∈ (1...𝐿))
147146ralrimiva 3146 . . . . . . . . . . . . . . 15 (πœ‘ β†’ βˆ€π‘— ∈ (𝐽 β€œ (1...𝐾))(1st β€˜π‘—) ∈ (1...𝐿))
148 vex 3478 . . . . . . . . . . . . . . . . . 18 π‘₯ ∈ V
149148, 116op1std 7981 . . . . . . . . . . . . . . . . 17 (𝑗 = ⟨π‘₯, π‘¦βŸ© β†’ (1st β€˜π‘—) = π‘₯)
150149eleq1d 2818 . . . . . . . . . . . . . . . 16 (𝑗 = ⟨π‘₯, π‘¦βŸ© β†’ ((1st β€˜π‘—) ∈ (1...𝐿) ↔ π‘₯ ∈ (1...𝐿)))
151150rspccv 3609 . . . . . . . . . . . . . . 15 (βˆ€π‘— ∈ (𝐽 β€œ (1...𝐾))(1st β€˜π‘—) ∈ (1...𝐿) β†’ (⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)) β†’ π‘₯ ∈ (1...𝐿)))
152147, 151syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)) β†’ π‘₯ ∈ (1...𝐿)))
153 opelxp 5711 . . . . . . . . . . . . . . 15 (⟨π‘₯, π‘¦βŸ© ∈ (βˆͺ 𝑛 ∈ (1...𝐿){𝑛} Γ— V) ↔ (π‘₯ ∈ βˆͺ 𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V))
154116biantru 530 . . . . . . . . . . . . . . 15 (π‘₯ ∈ βˆͺ 𝑛 ∈ (1...𝐿){𝑛} ↔ (π‘₯ ∈ βˆͺ 𝑛 ∈ (1...𝐿){𝑛} ∧ 𝑦 ∈ V))
155 iunid 5062 . . . . . . . . . . . . . . . 16 βˆͺ 𝑛 ∈ (1...𝐿){𝑛} = (1...𝐿)
156155eleq2i 2825 . . . . . . . . . . . . . . 15 (π‘₯ ∈ βˆͺ 𝑛 ∈ (1...𝐿){𝑛} ↔ π‘₯ ∈ (1...𝐿))
157153, 154, 1563bitr2i 298 . . . . . . . . . . . . . 14 (⟨π‘₯, π‘¦βŸ© ∈ (βˆͺ 𝑛 ∈ (1...𝐿){𝑛} Γ— V) ↔ π‘₯ ∈ (1...𝐿))
158152, 157syl6ibr 251 . . . . . . . . . . . . 13 (πœ‘ β†’ (⟨π‘₯, π‘¦βŸ© ∈ (𝐽 β€œ (1...𝐾)) β†’ ⟨π‘₯, π‘¦βŸ© ∈ (βˆͺ 𝑛 ∈ (1...𝐿){𝑛} Γ— V)))
159132, 158relssdv 5786 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐽 β€œ (1...𝐾)) βŠ† (βˆͺ 𝑛 ∈ (1...𝐿){𝑛} Γ— V))
160 xpiundir 5745 . . . . . . . . . . . 12 (βˆͺ 𝑛 ∈ (1...𝐿){𝑛} Γ— V) = βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V)
161159, 160sseqtrdi 4031 . . . . . . . . . . 11 (πœ‘ β†’ (𝐽 β€œ (1...𝐾)) βŠ† βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V))
162 df-ss 3964 . . . . . . . . . . 11 ((𝐽 β€œ (1...𝐾)) βŠ† βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V) ↔ ((𝐽 β€œ (1...𝐾)) ∩ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V)) = (𝐽 β€œ (1...𝐾)))
163161, 162sylib 217 . . . . . . . . . 10 (πœ‘ β†’ ((𝐽 β€œ (1...𝐾)) ∩ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— V)) = (𝐽 β€œ (1...𝐾)))
164129, 163eqtrd 2772 . . . . . . . . 9 (πœ‘ β†’ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) = (𝐽 β€œ (1...𝐾)))
165164, 90eqeltrd 2833 . . . . . . . 8 (πœ‘ β†’ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin)
166 ssiun2 5049 . . . . . . . 8 (𝑛 ∈ (1...𝐿) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) βŠ† βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})))
167 ssfi 9169 . . . . . . . 8 ((βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin ∧ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) βŠ† βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin)
168165, 166, 167syl2an 596 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin)
169 2ndconst 8083 . . . . . . . . . 10 (𝑛 ∈ V β†’ (2nd β†Ύ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))):({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))–1-1-ontoβ†’((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))
170169elv 3480 . . . . . . . . 9 (2nd β†Ύ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))):({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))–1-1-ontoβ†’((𝐽 β€œ (1...𝐾)) β€œ {𝑛})
171 f1oeng 8963 . . . . . . . . 9 ((({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin ∧ (2nd β†Ύ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))):({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))–1-1-ontoβ†’((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) β‰ˆ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))
172168, 170, 171sylancl 586 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) β‰ˆ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))
173172ensymd 8997 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) β‰ˆ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})))
174 enfii 9185 . . . . . . 7 ((({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) ∈ Fin ∧ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) β‰ˆ ({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) ∈ Fin)
175168, 173, 174syl2anc 584 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) ∈ Fin)
176 ffvelcdm 7080 . . . . . . . . . . . . . 14 ((𝐹:β„•βŸΆ(( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ∧ 𝑛 ∈ β„•) β†’ (πΉβ€˜π‘›) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
17716, 93, 176syl2an 596 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (πΉβ€˜π‘›) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•))
178 elovolmlem 24982 . . . . . . . . . . . . 13 ((πΉβ€˜π‘›) ∈ (( ≀ ∩ (ℝ Γ— ℝ)) ↑m β„•) ↔ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
179177, 178sylib 217 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
180179adantrr 715 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ (πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)))
181 imassrn 6068 . . . . . . . . . . . . . 14 ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) βŠ† ran (𝐽 β€œ (1...𝐾))
18222adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (𝐽 β€œ (1...𝐾)) βŠ† (β„• Γ— β„•))
183 rnss 5936 . . . . . . . . . . . . . . . 16 ((𝐽 β€œ (1...𝐾)) βŠ† (β„• Γ— β„•) β†’ ran (𝐽 β€œ (1...𝐾)) βŠ† ran (β„• Γ— β„•))
184182, 183syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran (𝐽 β€œ (1...𝐾)) βŠ† ran (β„• Γ— β„•))
185 rnxpid 6169 . . . . . . . . . . . . . . 15 ran (β„• Γ— β„•) = β„•
186184, 185sseqtrdi 4031 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran (𝐽 β€œ (1...𝐾)) βŠ† β„•)
187181, 186sstrid 3992 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) βŠ† β„•)
188187sseld 3980 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}) β†’ 𝑖 ∈ β„•))
189188impr 455 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ 𝑖 ∈ β„•)
190180, 189ffvelcdmd 7084 . . . . . . . . . 10 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ((πΉβ€˜π‘›)β€˜π‘–) ∈ ( ≀ ∩ (ℝ Γ— ℝ)))
191190elin2d 4198 . . . . . . . . 9 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ((πΉβ€˜π‘›)β€˜π‘–) ∈ (ℝ Γ— ℝ))
192 xp2nd 8004 . . . . . . . . 9 (((πΉβ€˜π‘›)β€˜π‘–) ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) ∈ ℝ)
193191, 192syl 17 . . . . . . . 8 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ (2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) ∈ ℝ)
194 xp1st 8003 . . . . . . . . 9 (((πΉβ€˜π‘›)β€˜π‘–) ∈ (ℝ Γ— ℝ) β†’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–)) ∈ ℝ)
195191, 194syl 17 . . . . . . . 8 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–)) ∈ ℝ)
196193, 195resubcld 11638 . . . . . . 7 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ ℝ)
197196anassrs 468 . . . . . 6 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})) β†’ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ ℝ)
198175, 197fsumrecl 15676 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ ℝ)
19998, 102, 104syl2an 596 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (𝐡 / (2↑𝑛)) ∈ ℝ)
20094, 199readdcld 11239 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))) ∈ ℝ)
20193, 200sylan2 593 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))) ∈ ℝ)
202 eqid 2732 . . . . . . . . . . . 12 ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›)) = ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))
203 ovoliun.s . . . . . . . . . . . 12 𝑆 = seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›)))
204202, 203ovolsf 24980 . . . . . . . . . . 11 ((πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ 𝑆:β„•βŸΆ(0[,)+∞))
205179, 204syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 𝑆:β„•βŸΆ(0[,)+∞))
206205frnd 6722 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran 𝑆 βŠ† (0[,)+∞))
207 icossxr 13405 . . . . . . . . 9 (0[,)+∞) βŠ† ℝ*
208206, 207sstrdi 3993 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran 𝑆 βŠ† ℝ*)
209 supxrcl 13290 . . . . . . . 8 (ran 𝑆 βŠ† ℝ* β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
210208, 209syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ*)
211 mnfxr 11267 . . . . . . . . 9 -∞ ∈ ℝ*
212211a1i 11 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ -∞ ∈ ℝ*)
21395rexrd 11260 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (vol*β€˜π΄) ∈ ℝ*)
21495mnfltd 13100 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ -∞ < (vol*β€˜π΄))
215 ovoliun.x1 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
21693, 215sylan2 593 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›)))
217203ovollb 24987 . . . . . . . . 9 (((πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ 𝐴 βŠ† βˆͺ ran ((,) ∘ (πΉβ€˜π‘›))) β†’ (vol*β€˜π΄) ≀ sup(ran 𝑆, ℝ*, < ))
218179, 216, 217syl2anc 584 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (vol*β€˜π΄) ≀ sup(ran 𝑆, ℝ*, < ))
219212, 213, 210, 214, 218xrltletrd 13136 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ -∞ < sup(ran 𝑆, ℝ*, < ))
220 ovoliun.x2 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
22193, 220sylan2 593 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
222 xrre 13144 . . . . . . 7 (((sup(ran 𝑆, ℝ*, < ) ∈ ℝ* ∧ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))) ∈ ℝ) ∧ (-∞ < sup(ran 𝑆, ℝ*, < ) ∧ sup(ran 𝑆, ℝ*, < ) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))) β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
223210, 201, 219, 221, 222syl22anc 837 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ sup(ran 𝑆, ℝ*, < ) ∈ ℝ)
224 1zzd 12589 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 1 ∈ β„€)
225202ovolfsval 24978 . . . . . . . . 9 (((πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) ∧ 𝑖 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))β€˜π‘–) = ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))))
226179, 225sylan 580 . . . . . . . 8 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))β€˜π‘–) = ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))))
227202ovolfsf 24979 . . . . . . . . . . . . 13 ((πΉβ€˜π‘›):β„•βŸΆ( ≀ ∩ (ℝ Γ— ℝ)) β†’ ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›)):β„•βŸΆ(0[,)+∞))
228179, 227syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›)):β„•βŸΆ(0[,)+∞))
229228ffvelcdmda 7083 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ β„•) β†’ (((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))β€˜π‘–) ∈ (0[,)+∞))
230226, 229eqeltrrd 2834 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑖 ∈ β„•) β†’ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ (0[,)+∞))
231 elrege0 13427 . . . . . . . . . 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 13299 . . . . . . . . . . . . . . 15 ((ran 𝑆 βŠ† ℝ* ∧ 𝑧 ∈ ran 𝑆) β†’ 𝑧 ≀ sup(ran 𝑆, ℝ*, < ))
236208, 235sylan 580 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) ∧ 𝑧 ∈ ran 𝑆) β†’ 𝑧 ≀ sup(ran 𝑆, ℝ*, < ))
237236ralrimiva 3146 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ sup(ran 𝑆, ℝ*, < ))
238 brralrspcev 5207 . . . . . . . . . . . . 13 ((sup(ran 𝑆, ℝ*, < ) ∈ ℝ ∧ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ sup(ran 𝑆, ℝ*, < )) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯)
239223, 237, 238syl2anc 584 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯)
240205ffnd 6715 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 𝑆 Fn β„•)
241 breq1 5150 . . . . . . . . . . . . . . 15 (𝑧 = (π‘†β€˜π‘˜) β†’ (𝑧 ≀ π‘₯ ↔ (π‘†β€˜π‘˜) ≀ π‘₯))
242241ralrn 7086 . . . . . . . . . . . . . 14 (𝑆 Fn β„• β†’ (βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯ ↔ βˆ€π‘˜ ∈ β„• (π‘†β€˜π‘˜) ≀ π‘₯))
243240, 242syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯ ↔ βˆ€π‘˜ ∈ β„• (π‘†β€˜π‘˜) ≀ π‘₯))
244243rexbidv 3178 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯ ↔ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (π‘†β€˜π‘˜) ≀ π‘₯))
245239, 244mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (π‘†β€˜π‘˜) ≀ π‘₯)
24669, 203, 224, 226, 233, 234, 245isumsup2 15788 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 𝑆 ⇝ sup(ran 𝑆, ℝ, < ))
247203, 246eqbrtrrid 5183 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))) ⇝ sup(ran 𝑆, ℝ, < ))
248 climrel 15432 . . . . . . . . . 10 Rel ⇝
249248releldmi 5945 . . . . . . . . 9 (seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))) ⇝ sup(ran 𝑆, ℝ, < ) β†’ seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))) ∈ dom ⇝ )
250247, 249syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ seq1( + , ((abs ∘ βˆ’ ) ∘ (πΉβ€˜π‘›))) ∈ dom ⇝ )
25169, 224, 175, 187, 226, 233, 234, 250isumless 15787 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ≀ Σ𝑖 ∈ β„• ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))))
25269, 203, 224, 226, 233, 234, 245isumsup 15789 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ β„• ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) = sup(ran 𝑆, ℝ, < ))
253 rge0ssre 13429 . . . . . . . . . 10 (0[,)+∞) βŠ† ℝ
254206, 253sstrdi 3993 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran 𝑆 βŠ† ℝ)
255 1nn 12219 . . . . . . . . . . . 12 1 ∈ β„•
256205fdmd 6725 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ dom 𝑆 = β„•)
257255, 256eleqtrrid 2840 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ 1 ∈ dom 𝑆)
258257ne0d 4334 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ dom 𝑆 β‰  βˆ…)
259 dm0rn0 5922 . . . . . . . . . . 11 (dom 𝑆 = βˆ… ↔ ran 𝑆 = βˆ…)
260259necon3bii 2993 . . . . . . . . . 10 (dom 𝑆 β‰  βˆ… ↔ ran 𝑆 β‰  βˆ…)
261258, 260sylib 217 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ ran 𝑆 β‰  βˆ…)
262 supxrre 13302 . . . . . . . . 9 ((ran 𝑆 βŠ† ℝ ∧ ran 𝑆 β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran 𝑆 𝑧 ≀ π‘₯) β†’ sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
263254, 261, 239, 262syl3anc 1371 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ sup(ran 𝑆, ℝ*, < ) = sup(ran 𝑆, ℝ, < ))
264252, 263eqtr4d 2775 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ β„• ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) = sup(ran 𝑆, ℝ*, < ))
265251, 264breqtrd 5173 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ≀ sup(ran 𝑆, ℝ*, < ))
266198, 223, 201, 265, 221letrd 11367 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ≀ ((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
26792, 198, 201, 266fsumle 15741 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ≀ Σ𝑛 ∈ (1...𝐿)((vol*β€˜π΄) + (𝐡 / (2↑𝑛))))
268 vex 3478 . . . . . . . . . . 11 𝑖 ∈ V
269115, 268op1std 7981 . . . . . . . . . 10 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ (1st β€˜π‘—) = 𝑛)
270269fveq2d 6892 . . . . . . . . 9 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ (πΉβ€˜(1st β€˜π‘—)) = (πΉβ€˜π‘›))
271115, 268op2ndd 7982 . . . . . . . . 9 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ (2nd β€˜π‘—) = 𝑖)
272270, 271fveq12d 6895 . . . . . . . 8 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ ((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)) = ((πΉβ€˜π‘›)β€˜π‘–))
273272fveq2d 6892 . . . . . . 7 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ (2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) = (2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)))
274272fveq2d 6892 . . . . . . 7 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) = (1st β€˜((πΉβ€˜π‘›)β€˜π‘–)))
275273, 274oveq12d 7423 . . . . . 6 (𝑗 = βŸ¨π‘›, π‘–βŸ© β†’ ((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))))
276196recnd 11238 . . . . . 6 ((πœ‘ ∧ (𝑛 ∈ (1...𝐿) ∧ 𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))) β†’ ((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) ∈ β„‚)
277275, 92, 175, 276fsum2d 15713 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) = Σ𝑗 ∈ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))))
278164sumeq1d 15643 . . . . 5 (πœ‘ β†’ Σ𝑗 ∈ βˆͺ 𝑛 ∈ (1...𝐿)({𝑛} Γ— ((𝐽 β€œ (1...𝐾)) β€œ {𝑛}))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))) = Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))))
279277, 278eqtrd 2772 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)Σ𝑖 ∈ ((𝐽 β€œ (1...𝐾)) β€œ {𝑛})((2nd β€˜((πΉβ€˜π‘›)β€˜π‘–)) βˆ’ (1st β€˜((πΉβ€˜π‘›)β€˜π‘–))) = Σ𝑗 ∈ (𝐽 β€œ (1...𝐾))((2nd β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—))) βˆ’ (1st β€˜((πΉβ€˜(1st β€˜π‘—))β€˜(2nd β€˜π‘—)))))
28095recnd 11238 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (vol*β€˜π΄) ∈ β„‚)
281105recnd 11238 . . . . 5 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (𝐡 / (2↑𝑛)) ∈ β„‚)
28292, 280, 281fsumadd 15682 . . . 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 12589 . . . . . . . . 9 (πœ‘ β†’ 1 ∈ β„€)
285 simpr 485 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ 𝑛 ∈ β„•)
286 ovoliun.g . . . . . . . . . . . 12 𝐺 = (𝑛 ∈ β„• ↦ (vol*β€˜π΄))
287286fvmpt2 7006 . . . . . . . . . . 11 ((𝑛 ∈ β„• ∧ (vol*β€˜π΄) ∈ ℝ) β†’ (πΊβ€˜π‘›) = (vol*β€˜π΄))
288285, 94, 287syl2anc 584 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΊβ€˜π‘›) = (vol*β€˜π΄))
289288, 94eqeltrd 2833 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (πΊβ€˜π‘›) ∈ ℝ)
29069, 284, 289serfre 13993 . . . . . . . 8 (πœ‘ β†’ seq1( + , 𝐺):β„•βŸΆβ„)
291 ovoliun.t . . . . . . . . 9 𝑇 = seq1( + , 𝐺)
292291feq1i 6705 . . . . . . . 8 (𝑇:β„•βŸΆβ„ ↔ seq1( + , 𝐺):β„•βŸΆβ„)
293290, 292sylibr 233 . . . . . . 7 (πœ‘ β†’ 𝑇:β„•βŸΆβ„)
294293frnd 6722 . . . . . 6 (πœ‘ β†’ ran 𝑇 βŠ† ℝ)
295 ressxr 11254 . . . . . 6 ℝ βŠ† ℝ*
296294, 295sstrdi 3993 . . . . 5 (πœ‘ β†’ ran 𝑇 βŠ† ℝ*)
29793, 288sylan2 593 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ (1...𝐿)) β†’ (πΊβ€˜π‘›) = (vol*β€˜π΄))
298 1red 11211 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ ℝ)
299 ffvelcdm 7080 . . . . . . . . . . . . 13 ((𝐽:β„•βŸΆ(β„• Γ— β„•) ∧ 1 ∈ β„•) β†’ (π½β€˜1) ∈ (β„• Γ— β„•))
30020, 255, 299sylancl 586 . . . . . . . . . . . 12 (πœ‘ β†’ (π½β€˜1) ∈ (β„• Γ— β„•))
301 xp1st 8003 . . . . . . . . . . . 12 ((π½β€˜1) ∈ (β„• Γ— β„•) β†’ (1st β€˜(π½β€˜1)) ∈ β„•)
302300, 301syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (1st β€˜(π½β€˜1)) ∈ β„•)
303302nnred 12223 . . . . . . . . . 10 (πœ‘ β†’ (1st β€˜(π½β€˜1)) ∈ ℝ)
304142zred 12662 . . . . . . . . . 10 (πœ‘ β†’ 𝐿 ∈ ℝ)
305302nnge1d 12256 . . . . . . . . . 10 (πœ‘ β†’ 1 ≀ (1st β€˜(π½β€˜1)))
306 2fveq3 6893 . . . . . . . . . . . 12 (𝑀 = 1 β†’ (1st β€˜(π½β€˜π‘€)) = (1st β€˜(π½β€˜1)))
307306breq1d 5157 . . . . . . . . . . 11 (𝑀 = 1 β†’ ((1st β€˜(π½β€˜π‘€)) ≀ 𝐿 ↔ (1st β€˜(π½β€˜1)) ≀ 𝐿))
308 eluzfz1 13504 . . . . . . . . . . . 12 (𝐾 ∈ (β„€β‰₯β€˜1) β†’ 1 ∈ (1...𝐾))
30970, 308syl 17 . . . . . . . . . . 11 (πœ‘ β†’ 1 ∈ (1...𝐾))
310307, 133, 309rspcdva 3613 . . . . . . . . . 10 (πœ‘ β†’ (1st β€˜(π½β€˜1)) ≀ 𝐿)
311298, 303, 304, 305, 310letrd 11367 . . . . . . . . 9 (πœ‘ β†’ 1 ≀ 𝐿)
312 elnnz1 12584 . . . . . . . . 9 (𝐿 ∈ β„• ↔ (𝐿 ∈ β„€ ∧ 1 ≀ 𝐿))
313142, 311, 312sylanbrc 583 . . . . . . . 8 (πœ‘ β†’ 𝐿 ∈ β„•)
314313, 69eleqtrdi 2843 . . . . . . 7 (πœ‘ β†’ 𝐿 ∈ (β„€β‰₯β€˜1))
315297, 314, 280fsumser 15672 . . . . . 6 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) = (seq1( + , 𝐺)β€˜πΏ))
316 seqfn 13974 . . . . . . . . 9 (1 ∈ β„€ β†’ seq1( + , 𝐺) Fn (β„€β‰₯β€˜1))
317284, 316syl 17 . . . . . . . 8 (πœ‘ β†’ seq1( + , 𝐺) Fn (β„€β‰₯β€˜1))
318 fnfvelrn 7079 . . . . . . . 8 ((seq1( + , 𝐺) Fn (β„€β‰₯β€˜1) ∧ 𝐿 ∈ (β„€β‰₯β€˜1)) β†’ (seq1( + , 𝐺)β€˜πΏ) ∈ ran seq1( + , 𝐺))
319317, 314, 318syl2anc 584 . . . . . . 7 (πœ‘ β†’ (seq1( + , 𝐺)β€˜πΏ) ∈ ran seq1( + , 𝐺))
320291rneqi 5934 . . . . . . 7 ran 𝑇 = ran seq1( + , 𝐺)
321319, 320eleqtrrdi 2844 . . . . . 6 (πœ‘ β†’ (seq1( + , 𝐺)β€˜πΏ) ∈ ran 𝑇)
322315, 321eqeltrd 2833 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) ∈ ran 𝑇)
323 supxrub 13299 . . . . 5 ((ran 𝑇 βŠ† ℝ* ∧ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) ∈ ran 𝑇) β†’ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) ≀ sup(ran 𝑇, ℝ*, < ))
324296, 322, 323syl2anc 584 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) ≀ sup(ran 𝑇, ℝ*, < ))
32598recnd 11238 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ β„‚)
326 geo2sum 15815 . . . . . 6 ((𝐿 ∈ β„• ∧ 𝐡 ∈ β„‚) β†’ Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛)) = (𝐡 βˆ’ (𝐡 / (2↑𝐿))))
327313, 325, 326syl2anc 584 . . . . 5 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛)) = (𝐡 βˆ’ (𝐡 / (2↑𝐿))))
328313nnnn0d 12528 . . . . . . . . . 10 (πœ‘ β†’ 𝐿 ∈ β„•0)
329 nnexpcl 14036 . . . . . . . . . 10 ((2 ∈ β„• ∧ 𝐿 ∈ β„•0) β†’ (2↑𝐿) ∈ β„•)
33099, 328, 329sylancr 587 . . . . . . . . 9 (πœ‘ β†’ (2↑𝐿) ∈ β„•)
331330nnrpd 13010 . . . . . . . 8 (πœ‘ β†’ (2↑𝐿) ∈ ℝ+)
33297, 331rpdivcld 13029 . . . . . . 7 (πœ‘ β†’ (𝐡 / (2↑𝐿)) ∈ ℝ+)
333332rpge0d 13016 . . . . . 6 (πœ‘ β†’ 0 ≀ (𝐡 / (2↑𝐿)))
33498, 330nndivred 12262 . . . . . . 7 (πœ‘ β†’ (𝐡 / (2↑𝐿)) ∈ ℝ)
33598, 334subge02d 11802 . . . . . 6 (πœ‘ β†’ (0 ≀ (𝐡 / (2↑𝐿)) ↔ (𝐡 βˆ’ (𝐡 / (2↑𝐿))) ≀ 𝐡))
336333, 335mpbid 231 . . . . 5 (πœ‘ β†’ (𝐡 βˆ’ (𝐡 / (2↑𝐿))) ≀ 𝐡)
337327, 336eqbrtrd 5169 . . . 4 (πœ‘ β†’ Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛)) ≀ 𝐡)
33896, 106, 108, 98, 324, 337le2addd 11829 . . 3 (πœ‘ β†’ (Σ𝑛 ∈ (1...𝐿)(vol*β€˜π΄) + Σ𝑛 ∈ (1...𝐿)(𝐡 / (2↑𝑛))) ≀ (sup(ran 𝑇, ℝ*, < ) + 𝐡))
33991, 107, 109, 283, 338letrd 11367 . 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 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  {csn 4627  βŸ¨cop 4633  βˆͺ cuni 4907  βˆͺ ciun 4996   class class class wbr 5147   ↦ cmpt 5230   Γ— cxp 5673  dom cdm 5675  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678   ∘ ccom 5679  Rel wrel 5680   Fn wfn 6535  βŸΆwf 6536  β€“1-1β†’wf1 6537  β€“1-1-ontoβ†’wf1o 6539  β€˜cfv 6540  (class class class)co 7405  1st c1st 7969  2nd c2nd 7970   ↑m cmap 8816   β‰ˆ cen 8932  Fincfn 8935  supcsup 9431  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109  +∞cpnf 11241  -∞cmnf 11242  β„*cxr 11243   < clt 11244   ≀ cle 11245   βˆ’ cmin 11440   / cdiv 11867  β„•cn 12208  2c2 12263  β„•0cn0 12468  β„€cz 12554  β„€β‰₯cuz 12818  β„+crp 12970  (,)cioo 13320  [,)cico 13322  ...cfz 13480  seqcseq 13962  β†‘cexp 14023  abscabs 15177   ⇝ cli 15424  Ξ£csu 15628  vol*covol 24970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-ioo 13324  df-ico 13326  df-fz 13481  df-fzo 13624  df-fl 13753  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-rlim 15429  df-sum 15629  df-ovol 24972
This theorem is referenced by:  ovoliunlem2  25011
  Copyright terms: Public domain W3C validator