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

Theorem ovolscalem1 25458
Description: Lemma for ovolsca 25460. (Contributed by Mario Carneiro, 6-Apr-2015.)
Hypotheses
Ref Expression
ovolsca.1 (๐œ‘ โ†’ ๐ด โІ โ„)
ovolsca.2 (๐œ‘ โ†’ ๐ถ โˆˆ โ„+)
ovolsca.3 (๐œ‘ โ†’ ๐ต = {๐‘ฅ โˆˆ โ„ โˆฃ (๐ถ ยท ๐‘ฅ) โˆˆ ๐ด})
ovolsca.4 (๐œ‘ โ†’ (vol*โ€˜๐ด) โˆˆ โ„)
ovolsca.5 ๐‘† = seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐น))
ovolsca.6 ๐บ = (๐‘› โˆˆ โ„• โ†ฆ โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ)
ovolsca.7 (๐œ‘ โ†’ ๐น:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
ovolsca.8 (๐œ‘ โ†’ ๐ด โІ โˆช ran ((,) โˆ˜ ๐น))
ovolsca.9 (๐œ‘ โ†’ ๐‘… โˆˆ โ„+)
ovolsca.10 (๐œ‘ โ†’ sup(ran ๐‘†, โ„*, < ) โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)))
Assertion
Ref Expression
ovolscalem1 (๐œ‘ โ†’ (vol*โ€˜๐ต) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…))
Distinct variable groups:   ๐‘ฅ,๐‘›,๐ด   ๐ต,๐‘›   ๐‘›,๐น,๐‘ฅ   ๐‘›,๐บ   ๐‘ฅ,๐‘…   ๐ถ,๐‘›,๐‘ฅ   ๐œ‘,๐‘›   ๐‘ฅ,๐‘†
Allowed substitution hints:   ๐œ‘(๐‘ฅ)   ๐ต(๐‘ฅ)   ๐‘…(๐‘›)   ๐‘†(๐‘›)   ๐บ(๐‘ฅ)

Proof of Theorem ovolscalem1
Dummy variables ๐‘˜ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovolsca.3 . . . 4 (๐œ‘ โ†’ ๐ต = {๐‘ฅ โˆˆ โ„ โˆฃ (๐ถ ยท ๐‘ฅ) โˆˆ ๐ด})
2 ssrab2 4069 . . . 4 {๐‘ฅ โˆˆ โ„ โˆฃ (๐ถ ยท ๐‘ฅ) โˆˆ ๐ด} โІ โ„
31, 2eqsstrdi 4027 . . 3 (๐œ‘ โ†’ ๐ต โІ โ„)
4 ovolcl 25423 . . 3 (๐ต โІ โ„ โ†’ (vol*โ€˜๐ต) โˆˆ โ„*)
53, 4syl 17 . 2 (๐œ‘ โ†’ (vol*โ€˜๐ต) โˆˆ โ„*)
6 ovolsca.7 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐น:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
7 ovolfcl 25411 . . . . . . . . . . . 12 ((๐น:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)) โˆง ๐‘› โˆˆ โ„•) โ†’ ((1st โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„ โˆง (2nd โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„ โˆง (1st โ€˜(๐นโ€˜๐‘›)) โ‰ค (2nd โ€˜(๐นโ€˜๐‘›))))
86, 7sylan 578 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ ((1st โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„ โˆง (2nd โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„ โˆง (1st โ€˜(๐นโ€˜๐‘›)) โ‰ค (2nd โ€˜(๐นโ€˜๐‘›))))
98simp3d 1141 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (1st โ€˜(๐นโ€˜๐‘›)) โ‰ค (2nd โ€˜(๐นโ€˜๐‘›)))
108simp1d 1139 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (1st โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„)
118simp2d 1140 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (2nd โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„)
12 ovolsca.2 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ถ โˆˆ โ„+)
1312rpregt0d 13052 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ))
1413adantr 479 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ))
15 lediv1 12107 . . . . . . . . . . 11 (((1st โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„ โˆง (2nd โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„ โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ ((1st โ€˜(๐นโ€˜๐‘›)) โ‰ค (2nd โ€˜(๐นโ€˜๐‘›)) โ†” ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โ‰ค ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)))
1610, 11, 14, 15syl3anc 1368 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ ((1st โ€˜(๐นโ€˜๐‘›)) โ‰ค (2nd โ€˜(๐นโ€˜๐‘›)) โ†” ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โ‰ค ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)))
179, 16mpbid 231 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โ‰ค ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ))
18 df-br 5144 . . . . . . . . 9 (((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โ‰ค ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โ†” โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ โˆˆ โ‰ค )
1917, 18sylib 217 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ โˆˆ โ‰ค )
2012adantr 479 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ ๐ถ โˆˆ โ„+)
2110, 20rerpdivcld 13077 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โˆˆ โ„)
2211, 20rerpdivcld 13077 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โˆˆ โ„)
2321, 22opelxpd 5711 . . . . . . . 8 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ โˆˆ (โ„ ร— โ„))
2419, 23elind 4188 . . . . . . 7 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ โˆˆ ( โ‰ค โˆฉ (โ„ ร— โ„)))
25 ovolsca.6 . . . . . . 7 ๐บ = (๐‘› โˆˆ โ„• โ†ฆ โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ)
2624, 25fmptd 7118 . . . . . 6 (๐œ‘ โ†’ ๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
27 eqid 2725 . . . . . . 7 ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ) = ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)
28 eqid 2725 . . . . . . 7 seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)) = seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))
2927, 28ovolsf 25417 . . . . . 6 (๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)) โ†’ seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)):โ„•โŸถ(0[,)+โˆž))
3026, 29syl 17 . . . . 5 (๐œ‘ โ†’ seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)):โ„•โŸถ(0[,)+โˆž))
3130frnd 6724 . . . 4 (๐œ‘ โ†’ ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)) โІ (0[,)+โˆž))
32 icossxr 13439 . . . 4 (0[,)+โˆž) โІ โ„*
3331, 32sstrdi 3985 . . 3 (๐œ‘ โ†’ ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)) โІ โ„*)
34 supxrcl 13324 . . 3 (ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)) โІ โ„* โ†’ sup(ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)), โ„*, < ) โˆˆ โ„*)
3533, 34syl 17 . 2 (๐œ‘ โ†’ sup(ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)), โ„*, < ) โˆˆ โ„*)
36 ovolsca.4 . . . . 5 (๐œ‘ โ†’ (vol*โ€˜๐ด) โˆˆ โ„)
3736, 12rerpdivcld 13077 . . . 4 (๐œ‘ โ†’ ((vol*โ€˜๐ด) / ๐ถ) โˆˆ โ„)
38 ovolsca.9 . . . . 5 (๐œ‘ โ†’ ๐‘… โˆˆ โ„+)
3938rpred 13046 . . . 4 (๐œ‘ โ†’ ๐‘… โˆˆ โ„)
4037, 39readdcld 11271 . . 3 (๐œ‘ โ†’ (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โˆˆ โ„)
4140rexrd 11292 . 2 (๐œ‘ โ†’ (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โˆˆ โ„*)
421eleq2d 2811 . . . . . . 7 (๐œ‘ โ†’ (๐‘ฆ โˆˆ ๐ต โ†” ๐‘ฆ โˆˆ {๐‘ฅ โˆˆ โ„ โˆฃ (๐ถ ยท ๐‘ฅ) โˆˆ ๐ด}))
43 oveq2 7423 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ (๐ถ ยท ๐‘ฅ) = (๐ถ ยท ๐‘ฆ))
4443eleq1d 2810 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ ((๐ถ ยท ๐‘ฅ) โˆˆ ๐ด โ†” (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด))
4544elrab 3675 . . . . . . 7 (๐‘ฆ โˆˆ {๐‘ฅ โˆˆ โ„ โˆฃ (๐ถ ยท ๐‘ฅ) โˆˆ ๐ด} โ†” (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด))
4642, 45bitrdi 286 . . . . . 6 (๐œ‘ โ†’ (๐‘ฆ โˆˆ ๐ต โ†” (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)))
47 breq2 5147 . . . . . . . . . . 11 (๐‘ฅ = (๐ถ ยท ๐‘ฆ) โ†’ ((1st โ€˜(๐นโ€˜๐‘›)) < ๐‘ฅ โ†” (1st โ€˜(๐นโ€˜๐‘›)) < (๐ถ ยท ๐‘ฆ)))
48 breq1 5146 . . . . . . . . . . 11 (๐‘ฅ = (๐ถ ยท ๐‘ฆ) โ†’ (๐‘ฅ < (2nd โ€˜(๐นโ€˜๐‘›)) โ†” (๐ถ ยท ๐‘ฆ) < (2nd โ€˜(๐นโ€˜๐‘›))))
4947, 48anbi12d 630 . . . . . . . . . 10 (๐‘ฅ = (๐ถ ยท ๐‘ฆ) โ†’ (((1st โ€˜(๐นโ€˜๐‘›)) < ๐‘ฅ โˆง ๐‘ฅ < (2nd โ€˜(๐นโ€˜๐‘›))) โ†” ((1st โ€˜(๐นโ€˜๐‘›)) < (๐ถ ยท ๐‘ฆ) โˆง (๐ถ ยท ๐‘ฆ) < (2nd โ€˜(๐นโ€˜๐‘›)))))
5049rexbidv 3169 . . . . . . . . 9 (๐‘ฅ = (๐ถ ยท ๐‘ฆ) โ†’ (โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐นโ€˜๐‘›)) < ๐‘ฅ โˆง ๐‘ฅ < (2nd โ€˜(๐นโ€˜๐‘›))) โ†” โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐นโ€˜๐‘›)) < (๐ถ ยท ๐‘ฆ) โˆง (๐ถ ยท ๐‘ฆ) < (2nd โ€˜(๐นโ€˜๐‘›)))))
51 ovolsca.8 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ด โІ โˆช ran ((,) โˆ˜ ๐น))
52 ovolsca.1 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ด โІ โ„)
53 ovolfioo 25412 . . . . . . . . . . . 12 ((๐ด โІ โ„ โˆง ๐น:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„))) โ†’ (๐ด โІ โˆช ran ((,) โˆ˜ ๐น) โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐นโ€˜๐‘›)) < ๐‘ฅ โˆง ๐‘ฅ < (2nd โ€˜(๐นโ€˜๐‘›)))))
5452, 6, 53syl2anc 582 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ด โІ โˆช ran ((,) โˆ˜ ๐น) โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐นโ€˜๐‘›)) < ๐‘ฅ โˆง ๐‘ฅ < (2nd โ€˜(๐นโ€˜๐‘›)))))
5551, 54mpbid 231 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐ด โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐นโ€˜๐‘›)) < ๐‘ฅ โˆง ๐‘ฅ < (2nd โ€˜(๐นโ€˜๐‘›))))
5655adantr 479 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โ†’ โˆ€๐‘ฅ โˆˆ ๐ด โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐นโ€˜๐‘›)) < ๐‘ฅ โˆง ๐‘ฅ < (2nd โ€˜(๐นโ€˜๐‘›))))
57 simprr 771 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โ†’ (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)
5850, 56, 57rspcdva 3603 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โ†’ โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐นโ€˜๐‘›)) < (๐ถ ยท ๐‘ฆ) โˆง (๐ถ ยท ๐‘ฆ) < (2nd โ€˜(๐นโ€˜๐‘›))))
59 opex 5460 . . . . . . . . . . . . . . . 16 โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ โˆˆ V
6025fvmpt2 7010 . . . . . . . . . . . . . . . 16 ((๐‘› โˆˆ โ„• โˆง โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ โˆˆ V) โ†’ (๐บโ€˜๐‘›) = โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ)
6159, 60mpan2 689 . . . . . . . . . . . . . . 15 (๐‘› โˆˆ โ„• โ†’ (๐บโ€˜๐‘›) = โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ)
6261fveq2d 6895 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (1st โ€˜(๐บโ€˜๐‘›)) = (1st โ€˜โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ))
63 ovex 7448 . . . . . . . . . . . . . . 15 ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โˆˆ V
64 ovex 7448 . . . . . . . . . . . . . . 15 ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โˆˆ V
6563, 64op1st 7997 . . . . . . . . . . . . . 14 (1st โ€˜โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ) = ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ)
6662, 65eqtrdi 2781 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (1st โ€˜(๐บโ€˜๐‘›)) = ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ))
6766adantl 480 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ (1st โ€˜(๐บโ€˜๐‘›)) = ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ))
6867breq1d 5153 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ ((1st โ€˜(๐บโ€˜๐‘›)) < ๐‘ฆ โ†” ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ) < ๐‘ฆ))
6910adantlr 713 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ (1st โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„)
70 simplrl 775 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘ฆ โˆˆ โ„)
7114adantlr 713 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ))
72 ltdivmul 12117 . . . . . . . . . . . 12 (((1st โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„ โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ (((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ) < ๐‘ฆ โ†” (1st โ€˜(๐นโ€˜๐‘›)) < (๐ถ ยท ๐‘ฆ)))
7369, 70, 71, 72syl3anc 1368 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ (((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ) < ๐‘ฆ โ†” (1st โ€˜(๐นโ€˜๐‘›)) < (๐ถ ยท ๐‘ฆ)))
7468, 73bitr2d 279 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ ((1st โ€˜(๐นโ€˜๐‘›)) < (๐ถ ยท ๐‘ฆ) โ†” (1st โ€˜(๐บโ€˜๐‘›)) < ๐‘ฆ))
7511adantlr 713 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ (2nd โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„)
76 ltmuldiv2 12116 . . . . . . . . . . . 12 ((๐‘ฆ โˆˆ โ„ โˆง (2nd โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„ โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ ((๐ถ ยท ๐‘ฆ) < (2nd โ€˜(๐นโ€˜๐‘›)) โ†” ๐‘ฆ < ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)))
7770, 75, 71, 76syl3anc 1368 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ ((๐ถ ยท ๐‘ฆ) < (2nd โ€˜(๐นโ€˜๐‘›)) โ†” ๐‘ฆ < ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)))
7861fveq2d 6895 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†’ (2nd โ€˜(๐บโ€˜๐‘›)) = (2nd โ€˜โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ))
7963, 64op2nd 7998 . . . . . . . . . . . . . 14 (2nd โ€˜โŸจ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ), ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)โŸฉ) = ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)
8078, 79eqtrdi 2781 . . . . . . . . . . . . 13 (๐‘› โˆˆ โ„• โ†’ (2nd โ€˜(๐บโ€˜๐‘›)) = ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ))
8180adantl 480 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ (2nd โ€˜(๐บโ€˜๐‘›)) = ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ))
8281breq2d 5155 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘ฆ < (2nd โ€˜(๐บโ€˜๐‘›)) โ†” ๐‘ฆ < ((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ)))
8377, 82bitr4d 281 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ ((๐ถ ยท ๐‘ฆ) < (2nd โ€˜(๐นโ€˜๐‘›)) โ†” ๐‘ฆ < (2nd โ€˜(๐บโ€˜๐‘›))))
8474, 83anbi12d 630 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โˆง ๐‘› โˆˆ โ„•) โ†’ (((1st โ€˜(๐นโ€˜๐‘›)) < (๐ถ ยท ๐‘ฆ) โˆง (๐ถ ยท ๐‘ฆ) < (2nd โ€˜(๐นโ€˜๐‘›))) โ†” ((1st โ€˜(๐บโ€˜๐‘›)) < ๐‘ฆ โˆง ๐‘ฆ < (2nd โ€˜(๐บโ€˜๐‘›)))))
8584rexbidva 3167 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โ†’ (โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐นโ€˜๐‘›)) < (๐ถ ยท ๐‘ฆ) โˆง (๐ถ ยท ๐‘ฆ) < (2nd โ€˜(๐นโ€˜๐‘›))) โ†” โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐บโ€˜๐‘›)) < ๐‘ฆ โˆง ๐‘ฆ < (2nd โ€˜(๐บโ€˜๐‘›)))))
8658, 85mpbid 231 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด)) โ†’ โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐บโ€˜๐‘›)) < ๐‘ฆ โˆง ๐‘ฆ < (2nd โ€˜(๐บโ€˜๐‘›))))
8786ex 411 . . . . . 6 (๐œ‘ โ†’ ((๐‘ฆ โˆˆ โ„ โˆง (๐ถ ยท ๐‘ฆ) โˆˆ ๐ด) โ†’ โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐บโ€˜๐‘›)) < ๐‘ฆ โˆง ๐‘ฆ < (2nd โ€˜(๐บโ€˜๐‘›)))))
8846, 87sylbid 239 . . . . 5 (๐œ‘ โ†’ (๐‘ฆ โˆˆ ๐ต โ†’ โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐บโ€˜๐‘›)) < ๐‘ฆ โˆง ๐‘ฆ < (2nd โ€˜(๐บโ€˜๐‘›)))))
8988ralrimiv 3135 . . . 4 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ ๐ต โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐บโ€˜๐‘›)) < ๐‘ฆ โˆง ๐‘ฆ < (2nd โ€˜(๐บโ€˜๐‘›))))
90 ovolfioo 25412 . . . . 5 ((๐ต โІ โ„ โˆง ๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„))) โ†’ (๐ต โІ โˆช ran ((,) โˆ˜ ๐บ) โ†” โˆ€๐‘ฆ โˆˆ ๐ต โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐บโ€˜๐‘›)) < ๐‘ฆ โˆง ๐‘ฆ < (2nd โ€˜(๐บโ€˜๐‘›)))))
913, 26, 90syl2anc 582 . . . 4 (๐œ‘ โ†’ (๐ต โІ โˆช ran ((,) โˆ˜ ๐บ) โ†” โˆ€๐‘ฆ โˆˆ ๐ต โˆƒ๐‘› โˆˆ โ„• ((1st โ€˜(๐บโ€˜๐‘›)) < ๐‘ฆ โˆง ๐‘ฆ < (2nd โ€˜(๐บโ€˜๐‘›)))))
9289, 91mpbird 256 . . 3 (๐œ‘ โ†’ ๐ต โІ โˆช ran ((,) โˆ˜ ๐บ))
9328ovollb 25424 . . 3 ((๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)) โˆง ๐ต โІ โˆช ran ((,) โˆ˜ ๐บ)) โ†’ (vol*โ€˜๐ต) โ‰ค sup(ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)), โ„*, < ))
9426, 92, 93syl2anc 582 . 2 (๐œ‘ โ†’ (vol*โ€˜๐ต) โ‰ค sup(ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)), โ„*, < ))
95 fzfid 13968 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (1...๐‘˜) โˆˆ Fin)
9612rpcnd 13048 . . . . . . . . 9 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
9796adantr 479 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐ถ โˆˆ โ„‚)
98 simpl 481 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐œ‘)
99 elfznn 13560 . . . . . . . . . 10 (๐‘› โˆˆ (1...๐‘˜) โ†’ ๐‘› โˆˆ โ„•)
10011, 10resubcld 11670 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ ((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) โˆˆ โ„)
10198, 99, 100syl2an 594 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘˜)) โ†’ ((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) โˆˆ โ„)
102101recnd 11270 . . . . . . . 8 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘˜)) โ†’ ((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) โˆˆ โ„‚)
10312rpne0d 13051 . . . . . . . . 9 (๐œ‘ โ†’ ๐ถ โ‰  0)
104103adantr 479 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐ถ โ‰  0)
10595, 97, 102, 104fsumdivc 15762 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) = ฮฃ๐‘› โˆˆ (1...๐‘˜)(((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ))
10680, 66oveq12d 7433 . . . . . . . . . . 11 (๐‘› โˆˆ โ„• โ†’ ((2nd โ€˜(๐บโ€˜๐‘›)) โˆ’ (1st โ€˜(๐บโ€˜๐‘›))) = (((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โˆ’ ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ)))
107106adantl 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ ((2nd โ€˜(๐บโ€˜๐‘›)) โˆ’ (1st โ€˜(๐บโ€˜๐‘›))) = (((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โˆ’ ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ)))
10827ovolfsval 25415 . . . . . . . . . . 11 ((๐บ:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)) โˆง ๐‘› โˆˆ โ„•) โ†’ (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘›) = ((2nd โ€˜(๐บโ€˜๐‘›)) โˆ’ (1st โ€˜(๐บโ€˜๐‘›))))
10926, 108sylan 578 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘›) = ((2nd โ€˜(๐บโ€˜๐‘›)) โˆ’ (1st โ€˜(๐บโ€˜๐‘›))))
11011recnd 11270 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (2nd โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„‚)
11110recnd 11270 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (1st โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„‚)
11212rpcnne0d 13055 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0))
113112adantr 479 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0))
114 divsubdir 11936 . . . . . . . . . . 11 (((2nd โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„‚ โˆง (1st โ€˜(๐นโ€˜๐‘›)) โˆˆ โ„‚ โˆง (๐ถ โˆˆ โ„‚ โˆง ๐ถ โ‰  0)) โ†’ (((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) = (((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โˆ’ ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ)))
115110, 111, 113, 114syl3anc 1368 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) = (((2nd โ€˜(๐นโ€˜๐‘›)) / ๐ถ) โˆ’ ((1st โ€˜(๐นโ€˜๐‘›)) / ๐ถ)))
116107, 109, 1153eqtr4d 2775 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘›) = (((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ))
11798, 99, 116syl2an 594 . . . . . . . 8 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘˜)) โ†’ (((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)โ€˜๐‘›) = (((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ))
118 simpr 483 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ โ„•)
119 nnuz 12893 . . . . . . . . 9 โ„• = (โ„คโ‰ฅโ€˜1)
120118, 119eleqtrdi 2835 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜1))
121100, 20rerpdivcld 13077 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) โˆˆ โ„)
122121recnd 11270 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘› โˆˆ โ„•) โ†’ (((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) โˆˆ โ„‚)
12398, 99, 122syl2an 594 . . . . . . . 8 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘˜)) โ†’ (((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) โˆˆ โ„‚)
124117, 120, 123fsumser 15706 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ฮฃ๐‘› โˆˆ (1...๐‘˜)(((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) = (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))โ€˜๐‘˜))
125105, 124eqtrd 2765 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) = (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))โ€˜๐‘˜))
126 ovolsca.10 . . . . . . . . . . 11 (๐œ‘ โ†’ sup(ran ๐‘†, โ„*, < ) โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)))
127 eqid 2725 . . . . . . . . . . . . . . . 16 ((abs โˆ˜ โˆ’ ) โˆ˜ ๐น) = ((abs โˆ˜ โˆ’ ) โˆ˜ ๐น)
128 ovolsca.5 . . . . . . . . . . . . . . . 16 ๐‘† = seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐น))
129127, 128ovolsf 25417 . . . . . . . . . . . . . . 15 (๐น:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)) โ†’ ๐‘†:โ„•โŸถ(0[,)+โˆž))
1306, 129syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘†:โ„•โŸถ(0[,)+โˆž))
131130frnd 6724 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ran ๐‘† โІ (0[,)+โˆž))
132131, 32sstrdi 3985 . . . . . . . . . . . 12 (๐œ‘ โ†’ ran ๐‘† โІ โ„*)
13312, 38rpmulcld 13062 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ถ ยท ๐‘…) โˆˆ โ„+)
134133rpred 13046 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ถ ยท ๐‘…) โˆˆ โ„)
13536, 134readdcld 11271 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)) โˆˆ โ„)
136135rexrd 11292 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)) โˆˆ โ„*)
137 supxrleub 13335 . . . . . . . . . . . 12 ((ran ๐‘† โІ โ„* โˆง ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)) โˆˆ โ„*) โ†’ (sup(ran ๐‘†, โ„*, < ) โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)) โ†” โˆ€๐‘ฅ โˆˆ ran ๐‘† ๐‘ฅ โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…))))
138132, 136, 137syl2anc 582 . . . . . . . . . . 11 (๐œ‘ โ†’ (sup(ran ๐‘†, โ„*, < ) โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)) โ†” โˆ€๐‘ฅ โˆˆ ran ๐‘† ๐‘ฅ โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…))))
139126, 138mpbid 231 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ran ๐‘† ๐‘ฅ โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)))
140130ffnd 6717 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘† Fn โ„•)
141 breq1 5146 . . . . . . . . . . . 12 (๐‘ฅ = (๐‘†โ€˜๐‘˜) โ†’ (๐‘ฅ โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)) โ†” (๐‘†โ€˜๐‘˜) โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…))))
142141ralrn 7092 . . . . . . . . . . 11 (๐‘† Fn โ„• โ†’ (โˆ€๐‘ฅ โˆˆ ran ๐‘† ๐‘ฅ โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘†โ€˜๐‘˜) โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…))))
143140, 142syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (โˆ€๐‘ฅ โˆˆ ran ๐‘† ๐‘ฅ โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘†โ€˜๐‘˜) โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…))))
144139, 143mpbid 231 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘†โ€˜๐‘˜) โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)))
145144r19.21bi 3239 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐‘†โ€˜๐‘˜) โ‰ค ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)))
1466adantr 479 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ๐น:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)))
147127ovolfsval 25415 . . . . . . . . . . 11 ((๐น:โ„•โŸถ( โ‰ค โˆฉ (โ„ ร— โ„)) โˆง ๐‘› โˆˆ โ„•) โ†’ (((abs โˆ˜ โˆ’ ) โˆ˜ ๐น)โ€˜๐‘›) = ((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))))
148146, 99, 147syl2an 594 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โˆง ๐‘› โˆˆ (1...๐‘˜)) โ†’ (((abs โˆ˜ โˆ’ ) โˆ˜ ๐น)โ€˜๐‘›) = ((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))))
149148, 120, 102fsumser 15706 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) = (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐น))โ€˜๐‘˜))
150128fveq1i 6892 . . . . . . . . 9 (๐‘†โ€˜๐‘˜) = (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐น))โ€˜๐‘˜)
151149, 150eqtr4di 2783 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) = (๐‘†โ€˜๐‘˜))
15237recnd 11270 . . . . . . . . . . 11 (๐œ‘ โ†’ ((vol*โ€˜๐ด) / ๐ถ) โˆˆ โ„‚)
15338rpcnd 13048 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘… โˆˆ โ„‚)
15496, 152, 153adddid 11266 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ถ ยท (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…)) = ((๐ถ ยท ((vol*โ€˜๐ด) / ๐ถ)) + (๐ถ ยท ๐‘…)))
15536recnd 11270 . . . . . . . . . . . 12 (๐œ‘ โ†’ (vol*โ€˜๐ด) โˆˆ โ„‚)
156155, 96, 103divcan2d 12020 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ถ ยท ((vol*โ€˜๐ด) / ๐ถ)) = (vol*โ€˜๐ด))
157156oveq1d 7430 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ถ ยท ((vol*โ€˜๐ด) / ๐ถ)) + (๐ถ ยท ๐‘…)) = ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)))
158154, 157eqtrd 2765 . . . . . . . . 9 (๐œ‘ โ†’ (๐ถ ยท (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…)) = ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)))
159158adantr 479 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ถ ยท (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…)) = ((vol*โ€˜๐ด) + (๐ถ ยท ๐‘…)))
160145, 151, 1593brtr4d 5175 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) โ‰ค (๐ถ ยท (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…)))
16195, 101fsumrecl 15710 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) โˆˆ โ„)
16240adantr 479 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โˆˆ โ„)
16313adantr 479 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ))
164 ledivmul 12118 . . . . . . . 8 ((ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) โˆˆ โ„ โˆง (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โˆˆ โ„ โˆง (๐ถ โˆˆ โ„ โˆง 0 < ๐ถ)) โ†’ ((ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โ†” ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) โ‰ค (๐ถ ยท (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…))))
165161, 162, 163, 164syl3anc 1368 . . . . . . 7 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โ†” ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) โ‰ค (๐ถ ยท (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…))))
166160, 165mpbird 256 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (ฮฃ๐‘› โˆˆ (1...๐‘˜)((2nd โ€˜(๐นโ€˜๐‘›)) โˆ’ (1st โ€˜(๐นโ€˜๐‘›))) / ๐ถ) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…))
167125, 166eqbrtrrd 5167 . . . . 5 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„•) โ†’ (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))โ€˜๐‘˜) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…))
168167ralrimiva 3136 . . . 4 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ โ„• (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))โ€˜๐‘˜) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…))
16930ffnd 6717 . . . . 5 (๐œ‘ โ†’ seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)) Fn โ„•)
170 breq1 5146 . . . . . 6 (๐‘ฆ = (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))โ€˜๐‘˜) โ†’ (๐‘ฆ โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โ†” (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))โ€˜๐‘˜) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…)))
171170ralrn 7092 . . . . 5 (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)) Fn โ„• โ†’ (โˆ€๐‘ฆ โˆˆ ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))๐‘ฆ โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โ†” โˆ€๐‘˜ โˆˆ โ„• (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))โ€˜๐‘˜) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…)))
172169, 171syl 17 . . . 4 (๐œ‘ โ†’ (โˆ€๐‘ฆ โˆˆ ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))๐‘ฆ โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โ†” โˆ€๐‘˜ โˆˆ โ„• (seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))โ€˜๐‘˜) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…)))
173168, 172mpbird 256 . . 3 (๐œ‘ โ†’ โˆ€๐‘ฆ โˆˆ ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))๐‘ฆ โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…))
174 supxrleub 13335 . . . 4 ((ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)) โІ โ„* โˆง (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โˆˆ โ„*) โ†’ (sup(ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)), โ„*, < ) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โ†” โˆ€๐‘ฆ โˆˆ ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))๐‘ฆ โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…)))
17533, 41, 174syl2anc 582 . . 3 (๐œ‘ โ†’ (sup(ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)), โ„*, < ) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…) โ†” โˆ€๐‘ฆ โˆˆ ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ))๐‘ฆ โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…)))
176173, 175mpbird 256 . 2 (๐œ‘ โ†’ sup(ran seq1( + , ((abs โˆ˜ โˆ’ ) โˆ˜ ๐บ)), โ„*, < ) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…))
1775, 35, 41, 94, 176xrletrd 13171 1 (๐œ‘ โ†’ (vol*โ€˜๐ต) โ‰ค (((vol*โ€˜๐ด) / ๐ถ) + ๐‘…))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2930  โˆ€wral 3051  โˆƒwrex 3060  {crab 3419  Vcvv 3463   โˆฉ cin 3939   โІ wss 3940  โŸจcop 4630  โˆช cuni 4903   class class class wbr 5143   โ†ฆ cmpt 5226   ร— cxp 5670  ran crn 5673   โˆ˜ ccom 5676   Fn wfn 6537  โŸถwf 6538  โ€˜cfv 6542  (class class class)co 7415  1st c1st 7987  2nd c2nd 7988  supcsup 9461  โ„‚cc 11134  โ„cr 11135  0cc0 11136  1c1 11137   + caddc 11139   ยท cmul 11141  +โˆžcpnf 11273  โ„*cxr 11275   < clt 11276   โ‰ค cle 11277   โˆ’ cmin 11472   / cdiv 11899  โ„•cn 12240  โ„คโ‰ฅcuz 12850  โ„+crp 13004  (,)cioo 13354  [,)cico 13356  ...cfz 13514  seqcseq 13996  abscabs 15211  ฮฃcsu 15662  vol*covol 25407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7737  ax-inf2 9662  ax-cnex 11192  ax-resscn 11193  ax-1cn 11194  ax-icn 11195  ax-addcl 11196  ax-addrcl 11197  ax-mulcl 11198  ax-mulrcl 11199  ax-mulcom 11200  ax-addass 11201  ax-mulass 11202  ax-distr 11203  ax-i2m1 11204  ax-1ne0 11205  ax-1rid 11206  ax-rnegex 11207  ax-rrecex 11208  ax-cnre 11209  ax-pre-lttri 11210  ax-pre-lttrn 11211  ax-pre-ltadd 11212  ax-pre-mulgt0 11213  ax-pre-sup 11214
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3960  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7868  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8388  df-rdg 8427  df-1o 8483  df-er 8721  df-map 8843  df-en 8961  df-dom 8962  df-sdom 8963  df-fin 8964  df-sup 9463  df-inf 9464  df-oi 9531  df-card 9960  df-pnf 11278  df-mnf 11279  df-xr 11280  df-ltxr 11281  df-le 11282  df-sub 11474  df-neg 11475  df-div 11900  df-nn 12241  df-2 12303  df-3 12304  df-n0 12501  df-z 12587  df-uz 12851  df-rp 13005  df-ioo 13358  df-ico 13360  df-fz 13515  df-fzo 13658  df-seq 13997  df-exp 14057  df-hash 14320  df-cj 15076  df-re 15077  df-im 15078  df-sqrt 15212  df-abs 15213  df-clim 15462  df-sum 15663  df-ovol 25409
This theorem is referenced by:  ovolscalem2  25459
  Copyright terms: Public domain W3C validator