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

Theorem itg2gt0 25047
Description: If the function 𝐹 is strictly positive on a set of positive measure, then the integral of the function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.)
Hypotheses
Ref Expression
itg2gt0.1 (πœ‘ β†’ 𝐴 ∈ dom vol)
itg2gt0.2 (πœ‘ β†’ 0 < (volβ€˜π΄))
itg2gt0.3 (πœ‘ β†’ 𝐹:β„βŸΆ(0[,)+∞))
itg2gt0.4 (πœ‘ β†’ 𝐹 ∈ MblFn)
itg2gt0.5 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 0 < (πΉβ€˜π‘₯))
Assertion
Ref Expression
itg2gt0 (πœ‘ β†’ 0 < (∫2β€˜πΉ))
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐹   πœ‘,π‘₯

Proof of Theorem itg2gt0
Dummy variables π‘˜ 𝑛 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itg2gt0.2 . 2 (πœ‘ β†’ 0 < (volβ€˜π΄))
2 itg2gt0.1 . . . . . . 7 (πœ‘ β†’ 𝐴 ∈ dom vol)
3 iccssxr 13276 . . . . . . . 8 (0[,]+∞) βŠ† ℝ*
4 volf 24815 . . . . . . . . 9 vol:dom vol⟢(0[,]+∞)
54ffvelcdmi 7029 . . . . . . . 8 (𝐴 ∈ dom vol β†’ (volβ€˜π΄) ∈ (0[,]+∞))
63, 5sselid 3941 . . . . . . 7 (𝐴 ∈ dom vol β†’ (volβ€˜π΄) ∈ ℝ*)
72, 6syl 17 . . . . . 6 (πœ‘ β†’ (volβ€˜π΄) ∈ ℝ*)
87adantr 482 . . . . 5 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (volβ€˜π΄) ∈ ℝ*)
9 itg2gt0.4 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹 ∈ MblFn)
109elexd 3464 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹 ∈ V)
11 cnvexg 7852 . . . . . . . . . . . . . . 15 (𝐹 ∈ V β†’ ◑𝐹 ∈ V)
1210, 11syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ◑𝐹 ∈ V)
13 imaexg 7843 . . . . . . . . . . . . . 14 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ V)
1412, 13syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ V)
1514adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ V)
1615fmpttd 7058 . . . . . . . . . . 11 (πœ‘ β†’ (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))):β„•βŸΆV)
1716ffnd 6665 . . . . . . . . . 10 (πœ‘ β†’ (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) Fn β„•)
18 fniunfv 7189 . . . . . . . . . 10 ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) Fn β„• β†’ βˆͺ π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))
1917, 18syl 17 . . . . . . . . 9 (πœ‘ β†’ βˆͺ π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))
20 itg2gt0.3 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹:β„βŸΆ(0[,)+∞))
21 rge0ssre 13302 . . . . . . . . . . . . . . . 16 (0[,)+∞) βŠ† ℝ
22 fss 6681 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,)+∞) ∧ (0[,)+∞) βŠ† ℝ) β†’ 𝐹:β„βŸΆβ„)
2320, 21, 22sylancl 587 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
24 mbfima 24916 . . . . . . . . . . . . . . 15 ((𝐹 ∈ MblFn ∧ 𝐹:β„βŸΆβ„) β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ dom vol)
259, 23, 24syl2anc 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ dom vol)
2625adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ dom vol)
2726fmpttd 7058 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))):β„•βŸΆdom vol)
2827ffvelcdmda 7030 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ∈ dom vol)
2928ralrimiva 3142 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ∈ dom vol)
30 iunmbl 24839 . . . . . . . . . 10 (βˆ€π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ∈ dom vol β†’ βˆͺ π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ∈ dom vol)
3129, 30syl 17 . . . . . . . . 9 (πœ‘ β†’ βˆͺ π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ∈ dom vol)
3219, 31eqeltrrd 2840 . . . . . . . 8 (πœ‘ β†’ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) ∈ dom vol)
33 mblss 24817 . . . . . . . 8 (βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) ∈ dom vol β†’ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† ℝ)
3432, 33syl 17 . . . . . . 7 (πœ‘ β†’ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† ℝ)
35 ovolcl 24764 . . . . . . 7 (βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† ℝ β†’ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) ∈ ℝ*)
3634, 35syl 17 . . . . . 6 (πœ‘ β†’ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) ∈ ℝ*)
3736adantr 482 . . . . 5 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) ∈ ℝ*)
38 0xr 11136 . . . . . 6 0 ∈ ℝ*
3938a1i 11 . . . . 5 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ 0 ∈ ℝ*)
40 mblvol 24816 . . . . . . . 8 (𝐴 ∈ dom vol β†’ (volβ€˜π΄) = (vol*β€˜π΄))
412, 40syl 17 . . . . . . 7 (πœ‘ β†’ (volβ€˜π΄) = (vol*β€˜π΄))
42 mblss 24817 . . . . . . . . . . . . . . . 16 (𝐴 ∈ dom vol β†’ 𝐴 βŠ† ℝ)
432, 42syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐴 βŠ† ℝ)
4443sselda 3943 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ ℝ)
4520ffvelcdmda 7030 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ (0[,)+∞))
46 elrege0 13300 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘₯) ∈ (0[,)+∞) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)))
4745, 46sylib 217 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)))
4847simpld 496 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
4944, 48syldan 592 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
50 itg2gt0.5 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 0 < (πΉβ€˜π‘₯))
51 nnrecl 12345 . . . . . . . . . . . . 13 (((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 < (πΉβ€˜π‘₯)) β†’ βˆƒπ‘˜ ∈ β„• (1 / π‘˜) < (πΉβ€˜π‘₯))
5249, 50, 51syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ βˆƒπ‘˜ ∈ β„• (1 / π‘˜) < (πΉβ€˜π‘₯))
5320ffnd 6665 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹 Fn ℝ)
5453ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ 𝐹 Fn ℝ)
55 elpreima 7004 . . . . . . . . . . . . . . . 16 (𝐹 Fn ℝ β†’ (π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ↔ (π‘₯ ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞))))
5654, 55syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ↔ (π‘₯ ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞))))
5744adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ π‘₯ ∈ ℝ)
5857biantrurd 534 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞) ↔ (π‘₯ ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞))))
59 nnrecre 12129 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„• β†’ (1 / π‘˜) ∈ ℝ)
6059adantl 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ ℝ)
6160rexrd 11139 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ ℝ*)
6261adantlr 714 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ ℝ*)
63 elioopnf 13289 . . . . . . . . . . . . . . . 16 ((1 / π‘˜) ∈ ℝ* β†’ ((πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ (1 / π‘˜) < (πΉβ€˜π‘₯))))
6462, 63syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ (1 / π‘˜) < (πΉβ€˜π‘₯))))
6556, 58, 643bitr2d 307 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ (1 / π‘˜) < (πΉβ€˜π‘₯))))
66 id 22 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•)
67 imaexg 7843 . . . . . . . . . . . . . . . . . 18 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ V)
6812, 67syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ V)
6968adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ V)
70 oveq2 7358 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘˜ β†’ (1 / 𝑛) = (1 / π‘˜))
7170oveq1d 7365 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘˜ β†’ ((1 / 𝑛)(,)+∞) = ((1 / π‘˜)(,)+∞))
7271imaeq2d 6010 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘˜ β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) = (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))
73 eqid 2738 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) = (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))
7472, 73fvmptg 6942 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ β„• ∧ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ V) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))
7566, 69, 74syl2anr 598 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))
7675eleq2d 2824 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ↔ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))
7749adantr 482 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
7877biantrurd 534 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ ((1 / π‘˜) < (πΉβ€˜π‘₯) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ (1 / π‘˜) < (πΉβ€˜π‘₯))))
7965, 76, 783bitr4rd 312 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ ((1 / π‘˜) < (πΉβ€˜π‘₯) ↔ π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8079rexbidva 3172 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (βˆƒπ‘˜ ∈ β„• (1 / π‘˜) < (πΉβ€˜π‘₯) ↔ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8152, 80mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜))
8281ex 414 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐴 β†’ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
83 eluni2 4868 . . . . . . . . . . 11 (π‘₯ ∈ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) ↔ βˆƒπ‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))π‘₯ ∈ 𝑧)
84 eleq2 2827 . . . . . . . . . . . . 13 (𝑧 = ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) β†’ (π‘₯ ∈ 𝑧 ↔ π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8584rexrn 7032 . . . . . . . . . . . 12 ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) Fn β„• β†’ (βˆƒπ‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))π‘₯ ∈ 𝑧 ↔ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8617, 85syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (βˆƒπ‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))π‘₯ ∈ 𝑧 ↔ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8783, 86bitrid 283 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) ↔ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8882, 87sylibrd 259 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 β†’ π‘₯ ∈ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
8988ssrdv 3949 . . . . . . . 8 (πœ‘ β†’ 𝐴 βŠ† βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))
90 ovolss 24771 . . . . . . . 8 ((𝐴 βŠ† βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) ∧ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† ℝ) β†’ (vol*β€˜π΄) ≀ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
9189, 34, 90syl2anc 585 . . . . . . 7 (πœ‘ β†’ (vol*β€˜π΄) ≀ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
9241, 91eqbrtrd 5126 . . . . . 6 (πœ‘ β†’ (volβ€˜π΄) ≀ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
9392adantr 482 . . . . 5 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (volβ€˜π΄) ≀ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
94 mblvol 24816 . . . . . . . . 9 (βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) ∈ dom vol β†’ (volβ€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) = (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
9532, 94syl 17 . . . . . . . 8 (πœ‘ β†’ (volβ€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) = (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
96 peano2nn 12099 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
9796adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„•)
98 nnrecre 12129 . . . . . . . . . . . . . . 15 ((π‘˜ + 1) ∈ β„• β†’ (1 / (π‘˜ + 1)) ∈ ℝ)
9997, 98syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / (π‘˜ + 1)) ∈ ℝ)
10099rexrd 11139 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / (π‘˜ + 1)) ∈ ℝ*)
101 nnre 12094 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ)
102101adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ ℝ)
103102lep1d 12020 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ≀ (π‘˜ + 1))
104 nngt0 12118 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ 0 < π‘˜)
105104adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 0 < π‘˜)
10697nnred 12102 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ ℝ)
10797nngt0d 12136 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 0 < (π‘˜ + 1))
108 lerec 11972 . . . . . . . . . . . . . . 15 (((π‘˜ ∈ ℝ ∧ 0 < π‘˜) ∧ ((π‘˜ + 1) ∈ ℝ ∧ 0 < (π‘˜ + 1))) β†’ (π‘˜ ≀ (π‘˜ + 1) ↔ (1 / (π‘˜ + 1)) ≀ (1 / π‘˜)))
109102, 105, 106, 107, 108syl22anc 838 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ ≀ (π‘˜ + 1) ↔ (1 / (π‘˜ + 1)) ≀ (1 / π‘˜)))
110103, 109mpbid 231 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / (π‘˜ + 1)) ≀ (1 / π‘˜))
111 iooss1 13228 . . . . . . . . . . . . 13 (((1 / (π‘˜ + 1)) ∈ ℝ* ∧ (1 / (π‘˜ + 1)) ≀ (1 / π‘˜)) β†’ ((1 / π‘˜)(,)+∞) βŠ† ((1 / (π‘˜ + 1))(,)+∞))
112100, 110, 111syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((1 / π‘˜)(,)+∞) βŠ† ((1 / (π‘˜ + 1))(,)+∞))
113 imass2 6051 . . . . . . . . . . . 12 (((1 / π‘˜)(,)+∞) βŠ† ((1 / (π‘˜ + 1))(,)+∞) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) βŠ† (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)))
114112, 113syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) βŠ† (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)))
11566, 68, 74syl2anr 598 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))
116 imaexg 7843 . . . . . . . . . . . . 13 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)) ∈ V)
11712, 116syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)) ∈ V)
118 oveq2 7358 . . . . . . . . . . . . . . 15 (𝑛 = (π‘˜ + 1) β†’ (1 / 𝑛) = (1 / (π‘˜ + 1)))
119118oveq1d 7365 . . . . . . . . . . . . . 14 (𝑛 = (π‘˜ + 1) β†’ ((1 / 𝑛)(,)+∞) = ((1 / (π‘˜ + 1))(,)+∞))
120119imaeq2d 6010 . . . . . . . . . . . . 13 (𝑛 = (π‘˜ + 1) β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) = (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)))
121120, 73fvmptg 6942 . . . . . . . . . . . 12 (((π‘˜ + 1) ∈ β„• ∧ (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)) ∈ V) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜(π‘˜ + 1)) = (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)))
12296, 117, 121syl2anr 598 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜(π‘˜ + 1)) = (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)))
123114, 115, 1223sstr4d 3990 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) βŠ† ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜(π‘˜ + 1)))
124123ralrimiva 3142 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) βŠ† ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜(π‘˜ + 1)))
125 volsup 24842 . . . . . . . . 9 (((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))):β„•βŸΆdom vol ∧ βˆ€π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) βŠ† ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜(π‘˜ + 1))) β†’ (volβ€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) = sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ))
12627, 124, 125syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (volβ€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) = sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ))
12795, 126eqtr3d 2780 . . . . . . 7 (πœ‘ β†’ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) = sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ))
128127adantr 482 . . . . . 6 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) = sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ))
12968adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ V)
13066, 129, 74syl2anr 598 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))
131130fveq2d 6842 . . . . . . . . . . 11 (((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) ∧ π‘˜ ∈ β„•) β†’ (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) = (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))
13238a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ 0 ∈ ℝ*)
133 nnrecgt0 12130 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ ∈ β„• β†’ 0 < (1 / π‘˜))
134133adantl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 0 < (1 / π‘˜))
135 0re 11091 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ ℝ
136 ltle 11177 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 ∈ ℝ ∧ (1 / π‘˜) ∈ ℝ) β†’ (0 < (1 / π‘˜) β†’ 0 ≀ (1 / π‘˜)))
137135, 60, 136sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (0 < (1 / π‘˜) β†’ 0 ≀ (1 / π‘˜)))
138134, 137mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 0 ≀ (1 / π‘˜))
139 elxrge0 13303 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 / π‘˜) ∈ (0[,]+∞) ↔ ((1 / π‘˜) ∈ ℝ* ∧ 0 ≀ (1 / π‘˜)))
14061, 138, 139sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ (0[,]+∞))
141 0e0iccpnf 13305 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ (0[,]+∞)
142 ifcl 4530 . . . . . . . . . . . . . . . . . . . . . 22 (((1 / π‘˜) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ∈ (0[,]+∞))
143140, 141, 142sylancl 587 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ∈ (0[,]+∞))
144143adantr 482 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ∈ (0[,]+∞))
145144fmpttd 7058 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)):β„βŸΆ(0[,]+∞))
146145adantrr 716 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)):β„βŸΆ(0[,]+∞))
147 itg2cl 25019 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)):β„βŸΆ(0[,]+∞) β†’ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∈ ℝ*)
148146, 147syl 17 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∈ ℝ*)
149 icossicc 13282 . . . . . . . . . . . . . . . . . . . 20 (0[,)+∞) βŠ† (0[,]+∞)
150 fss 6681 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:β„βŸΆ(0[,)+∞) ∧ (0[,)+∞) βŠ† (0[,]+∞)) β†’ 𝐹:β„βŸΆ(0[,]+∞))
15120, 149, 150sylancl 587 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐹:β„βŸΆ(0[,]+∞))
152 itg2cl 25019 . . . . . . . . . . . . . . . . . . 19 (𝐹:β„βŸΆ(0[,]+∞) β†’ (∫2β€˜πΉ) ∈ ℝ*)
153151, 152syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (∫2β€˜πΉ) ∈ ℝ*)
154153adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (∫2β€˜πΉ) ∈ ℝ*)
155 0nrp 12879 . . . . . . . . . . . . . . . . . . 19 Β¬ 0 ∈ ℝ+
156 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))))
157115, 28eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol)
158157adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol)
159158adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol)
160156, 135eqeltrrdi 2848 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∈ ℝ)
16160, 134elrpd 12883 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ ℝ+)
162161adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (1 / π‘˜) ∈ ℝ+)
163162adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (1 / π‘˜) ∈ ℝ+)
164 itg2const2 25028 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol ∧ (1 / π‘˜) ∈ ℝ+) β†’ ((volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ ↔ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∈ ℝ))
165159, 163, 164syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ ((volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ ↔ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∈ ℝ))
166160, 165mpbird 257 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ)
167 elrege0 13300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 / π‘˜) ∈ (0[,)+∞) ↔ ((1 / π‘˜) ∈ ℝ ∧ 0 ≀ (1 / π‘˜)))
16860, 138, 167sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ (0[,)+∞))
169168adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (1 / π‘˜) ∈ (0[,)+∞))
170169adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (1 / π‘˜) ∈ (0[,)+∞))
171 itg2const 25027 . . . . . . . . . . . . . . . . . . . . . . 23 (((◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol ∧ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ ∧ (1 / π‘˜) ∈ (0[,)+∞)) β†’ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) = ((1 / π‘˜) Β· (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
172159, 166, 170, 171syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) = ((1 / π‘˜) Β· (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
173156, 172eqtrd 2778 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ 0 = ((1 / π‘˜) Β· (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
174 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))
175166, 174elrpd 12883 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ+)
176163, 175rpmulcld 12902 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ ((1 / π‘˜) Β· (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))) ∈ ℝ+)
177173, 176eqeltrd 2839 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ 0 ∈ ℝ+)
178177ex 414 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) β†’ 0 ∈ ℝ+))
179155, 178mtoi 198 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ Β¬ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))))
180 itg2ge0 25022 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)):β„βŸΆ(0[,]+∞) β†’ 0 ≀ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))))
181146, 180syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ 0 ≀ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))))
182 xrleloe 12992 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ* ∧ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∈ ℝ*) β†’ (0 ≀ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ↔ (0 < (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∨ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))))))
18338, 148, 182sylancr 588 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (0 ≀ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ↔ (0 < (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∨ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))))))
184181, 183mpbid 231 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (0 < (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∨ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))))
185184ord 863 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (Β¬ 0 < (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) β†’ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))))
186179, 185mt3d 148 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ 0 < (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))))
187151adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ 𝐹:β„βŸΆ(0[,]+∞))
18860adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (1 / π‘˜) ∈ ℝ)
18953adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐹 Fn ℝ)
190189, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ↔ (π‘₯ ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞))))
191190biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (π‘₯ ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞)))
192191simpld 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ π‘₯ ∈ ℝ)
19348adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
194192, 193syldan 592 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
19561adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (1 / π‘˜) ∈ ℝ*)
196191simprd 497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞))
197 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πΉβ€˜π‘₯) ∈ ℝ ∧ (1 / π‘˜) < (πΉβ€˜π‘₯)) β†’ (1 / π‘˜) < (πΉβ€˜π‘₯))
19863, 197syl6bi 253 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 / π‘˜) ∈ ℝ* β†’ ((πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞) β†’ (1 / π‘˜) < (πΉβ€˜π‘₯)))
199195, 196, 198sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (1 / π‘˜) < (πΉβ€˜π‘₯))
200188, 194, 199ltled 11237 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (1 / π‘˜) ≀ (πΉβ€˜π‘₯))
20147simprd 497 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (πΉβ€˜π‘₯))
202201adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (πΉβ€˜π‘₯))
203192, 202syldan 592 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ 0 ≀ (πΉβ€˜π‘₯))
204 breq1 5107 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 / π‘˜) = if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) β†’ ((1 / π‘˜) ≀ (πΉβ€˜π‘₯) ↔ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯)))
205 breq1 5107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 = if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) β†’ (0 ≀ (πΉβ€˜π‘₯) ↔ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯)))
206204, 205ifboth 4524 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1 / π‘˜) ≀ (πΉβ€˜π‘₯) ∧ 0 ≀ (πΉβ€˜π‘₯)) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
207200, 203, 206syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
208207adantlr 714 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
209 iffalse 4494 . . . . . . . . . . . . . . . . . . . . . . . 24 (Β¬ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) = 0)
210209adantl 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) = 0)
211202adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ 0 ≀ (πΉβ€˜π‘₯))
212210, 211eqbrtrd 5126 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
213208, 212pm2.61dan 812 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
214213ralrimiva 3142 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
215214adantrr 716 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
216 reex 11076 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ V
217216a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ℝ ∈ V)
218 ovex 7383 . . . . . . . . . . . . . . . . . . . . . . 23 (1 / π‘˜) ∈ V
219 c0ex 11083 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ V
220218, 219ifex 4535 . . . . . . . . . . . . . . . . . . . . . 22 if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ∈ V
221220a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ∈ V)
222 fvexd 6853 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ V)
223 eqidd 2739 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))
22420feqmptd 6906 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐹 = (π‘₯ ∈ ℝ ↦ (πΉβ€˜π‘₯)))
225217, 221, 222, 223, 224ofrfval2 7629 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)) ∘r ≀ 𝐹 ↔ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯)))
226225biimpar 479 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯)) β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)) ∘r ≀ 𝐹)
227215, 226syldan 592 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)) ∘r ≀ 𝐹)
228 itg2le 25026 . . . . . . . . . . . . . . . . . 18 (((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)):β„βŸΆ(0[,]+∞) ∧ 𝐹:β„βŸΆ(0[,]+∞) ∧ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)) ∘r ≀ 𝐹) β†’ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ≀ (∫2β€˜πΉ))
229146, 187, 227, 228syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ≀ (∫2β€˜πΉ))
230132, 148, 154, 186, 229xrltletrd 13009 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ 0 < (∫2β€˜πΉ))
231230expr 458 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ 0 < (∫2β€˜πΉ)))
232231con3d 152 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (Β¬ 0 < (∫2β€˜πΉ) β†’ Β¬ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
2334ffvelcdmi 7029 . . . . . . . . . . . . . . . . 17 ((◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ (0[,]+∞))
2343, 233sselid 3941 . . . . . . . . . . . . . . . 16 ((◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ*)
235157, 234syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ*)
236 xrlenlt 11154 . . . . . . . . . . . . . . 15 (((volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ* ∧ 0 ∈ ℝ*) β†’ ((volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ≀ 0 ↔ Β¬ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
237235, 38, 236sylancl 587 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ≀ 0 ↔ Β¬ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
238232, 237sylibrd 259 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (Β¬ 0 < (∫2β€˜πΉ) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ≀ 0))
239238imp 408 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ≀ 0)
240239an32s 651 . . . . . . . . . . 11 (((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) ∧ π‘˜ ∈ β„•) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ≀ 0)
241131, 240eqbrtrd 5126 . . . . . . . . . 10 (((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) ∧ π‘˜ ∈ β„•) β†’ (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0)
242241ralrimiva 3142 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ βˆ€π‘˜ ∈ β„• (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0)
243 ffn 6664 . . . . . . . . . . 11 ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))):β„•βŸΆV β†’ (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) Fn β„•)
244 fveq2 6838 . . . . . . . . . . . . 13 (𝑧 = ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) β†’ (volβ€˜π‘§) = (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
245244breq1d 5114 . . . . . . . . . . . 12 (𝑧 = ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) β†’ ((volβ€˜π‘§) ≀ 0 ↔ (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0))
246245ralrn 7033 . . . . . . . . . . 11 ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) Fn β„• β†’ (βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0 ↔ βˆ€π‘˜ ∈ β„• (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0))
24716, 243, 2463syl 18 . . . . . . . . . 10 (πœ‘ β†’ (βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0 ↔ βˆ€π‘˜ ∈ β„• (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0))
248247adantr 482 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0 ↔ βˆ€π‘˜ ∈ β„• (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0))
249242, 248mpbird 257 . . . . . . . 8 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0)
250 ffn 6664 . . . . . . . . . 10 (vol:dom vol⟢(0[,]+∞) β†’ vol Fn dom vol)
2514, 250ax-mp 5 . . . . . . . . 9 vol Fn dom vol
25227frnd 6672 . . . . . . . . . 10 (πœ‘ β†’ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† dom vol)
253252adantr 482 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† dom vol)
254 breq1 5107 . . . . . . . . . 10 (π‘₯ = (volβ€˜π‘§) β†’ (π‘₯ ≀ 0 ↔ (volβ€˜π‘§) ≀ 0))
255254ralima 7183 . . . . . . . . 9 ((vol Fn dom vol ∧ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† dom vol) β†’ (βˆ€π‘₯ ∈ (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))π‘₯ ≀ 0 ↔ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0))
256251, 253, 255sylancr 588 . . . . . . . 8 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (βˆ€π‘₯ ∈ (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))π‘₯ ≀ 0 ↔ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0))
257249, 256mpbird 257 . . . . . . 7 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ βˆ€π‘₯ ∈ (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))π‘₯ ≀ 0)
258 imassrn 6021 . . . . . . . . 9 (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) βŠ† ran vol
259 frn 6671 . . . . . . . . . . 11 (vol:dom vol⟢(0[,]+∞) β†’ ran vol βŠ† (0[,]+∞))
2604, 259ax-mp 5 . . . . . . . . . 10 ran vol βŠ† (0[,]+∞)
261260, 3sstri 3952 . . . . . . . . 9 ran vol βŠ† ℝ*
262258, 261sstri 3952 . . . . . . . 8 (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) βŠ† ℝ*
263 supxrleub 13174 . . . . . . . 8 (((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) βŠ† ℝ* ∧ 0 ∈ ℝ*) β†’ (sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ) ≀ 0 ↔ βˆ€π‘₯ ∈ (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))π‘₯ ≀ 0))
264262, 38, 263mp2an 691 . . . . . . 7 (sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ) ≀ 0 ↔ βˆ€π‘₯ ∈ (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))π‘₯ ≀ 0)
265257, 264sylibr 233 . . . . . 6 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ) ≀ 0)
266128, 265eqbrtrd 5126 . . . . 5 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) ≀ 0)
2678, 37, 39, 93, 266xrletrd 13010 . . . 4 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (volβ€˜π΄) ≀ 0)
268267ex 414 . . 3 (πœ‘ β†’ (Β¬ 0 < (∫2β€˜πΉ) β†’ (volβ€˜π΄) ≀ 0))
269 xrlenlt 11154 . . . 4 (((volβ€˜π΄) ∈ ℝ* ∧ 0 ∈ ℝ*) β†’ ((volβ€˜π΄) ≀ 0 ↔ Β¬ 0 < (volβ€˜π΄)))
2707, 38, 269sylancl 587 . . 3 (πœ‘ β†’ ((volβ€˜π΄) ≀ 0 ↔ Β¬ 0 < (volβ€˜π΄)))
271268, 270sylibd 238 . 2 (πœ‘ β†’ (Β¬ 0 < (∫2β€˜πΉ) β†’ Β¬ 0 < (volβ€˜π΄)))
2721, 271mt4d 117 1 (πœ‘ β†’ 0 < (∫2β€˜πΉ))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107  βˆ€wral 3063  βˆƒwrex 3072  Vcvv 3444   βŠ† wss 3909  ifcif 4485  βˆͺ cuni 4864  βˆͺ ciun 4953   class class class wbr 5104   ↦ cmpt 5187  β—‘ccnv 5630  dom cdm 5631  ran crn 5632   β€œ cima 5634   Fn wfn 6487  βŸΆwf 6488  β€˜cfv 6492  (class class class)co 7350   ∘r cofr 7607  supcsup 9310  β„cr 10984  0cc0 10985  1c1 10986   + caddc 10988   Β· cmul 10990  +∞cpnf 11120  β„*cxr 11122   < clt 11123   ≀ cle 11124   / cdiv 11746  β„•cn 12087  β„+crp 12844  (,)cioo 13193  [,)cico 13195  [,]cicc 13196  vol*covol 24748  volcvol 24749  MblFncmbf 24900  βˆ«2citg2 24902
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 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-inf2 9511  ax-cc 10305  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063  ax-addf 11064
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 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-disj 5070  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-of 7608  df-ofr 7609  df-om 7794  df-1st 7912  df-2nd 7913  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8582  df-map 8701  df-pm 8702  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-fi 9281  df-sup 9312  df-inf 9313  df-oi 9380  df-dju 9771  df-card 9809  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-n0 12348  df-z 12434  df-uz 12697  df-q 12803  df-rp 12845  df-xneg 12962  df-xadd 12963  df-xmul 12964  df-ioo 13197  df-ico 13199  df-icc 13200  df-fz 13354  df-fzo 13497  df-fl 13626  df-seq 13836  df-exp 13897  df-hash 14159  df-cj 14918  df-re 14919  df-im 14920  df-sqrt 15054  df-abs 15055  df-clim 15305  df-rlim 15306  df-sum 15506  df-rest 17239  df-topgen 17260  df-psmet 20711  df-xmet 20712  df-met 20713  df-bl 20714  df-mopn 20715  df-top 22165  df-topon 22182  df-bases 22218  df-cmp 22660  df-cncf 24163  df-ovol 24750  df-vol 24751  df-mbf 24905  df-itg1 24906  df-itg2 24907  df-0p 24956
This theorem is referenced by:  itggt0  25130
  Copyright terms: Public domain W3C validator