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 13275 . . . . . . . 8 (0[,]+∞) βŠ† ℝ*
4 volf 24815 . . . . . . . . 9 vol:dom vol⟢(0[,]+∞)
54ffvelcdmi 7028 . . . . . . . 8 (𝐴 ∈ dom vol β†’ (volβ€˜π΄) ∈ (0[,]+∞))
63, 5sselid 3940 . . . . . . 7 (𝐴 ∈ dom vol β†’ (volβ€˜π΄) ∈ ℝ*)
72, 6syl 17 . . . . . 6 (πœ‘ β†’ (volβ€˜π΄) ∈ ℝ*)
87adantr 481 . . . . 5 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (volβ€˜π΄) ∈ ℝ*)
9 itg2gt0.4 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹 ∈ MblFn)
109elexd 3463 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹 ∈ V)
11 cnvexg 7851 . . . . . . . . . . . . . . 15 (𝐹 ∈ V β†’ ◑𝐹 ∈ V)
1210, 11syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ ◑𝐹 ∈ V)
13 imaexg 7842 . . . . . . . . . . . . . 14 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ V)
1412, 13syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ V)
1514adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ V)
1615fmpttd 7057 . . . . . . . . . . 11 (πœ‘ β†’ (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))):β„•βŸΆV)
1716ffnd 6664 . . . . . . . . . 10 (πœ‘ β†’ (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) Fn β„•)
18 fniunfv 7188 . . . . . . . . . 10 ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) Fn β„• β†’ βˆͺ π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))
1917, 18syl 17 . . . . . . . . 9 (πœ‘ β†’ βˆͺ π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))
20 itg2gt0.3 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹:β„βŸΆ(0[,)+∞))
21 rge0ssre 13301 . . . . . . . . . . . . . . . 16 (0[,)+∞) βŠ† ℝ
22 fss 6680 . . . . . . . . . . . . . . . 16 ((𝐹:β„βŸΆ(0[,)+∞) ∧ (0[,)+∞) βŠ† ℝ) β†’ 𝐹:β„βŸΆβ„)
2320, 21, 22sylancl 586 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
24 mbfima 24916 . . . . . . . . . . . . . . 15 ((𝐹 ∈ MblFn ∧ 𝐹:β„βŸΆβ„) β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ dom vol)
259, 23, 24syl2anc 584 . . . . . . . . . . . . . 14 (πœ‘ β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ dom vol)
2625adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ β„•) β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) ∈ dom vol)
2726fmpttd 7057 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))):β„•βŸΆdom vol)
2827ffvelcdmda 7029 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ∈ dom vol)
2928ralrimiva 3141 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ∈ dom vol)
30 iunmbl 24839 . . . . . . . . . 10 (βˆ€π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ∈ dom vol β†’ βˆͺ π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ∈ dom vol)
3129, 30syl 17 . . . . . . . . 9 (πœ‘ β†’ βˆͺ π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ∈ dom vol)
3219, 31eqeltrrd 2839 . . . . . . . 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 481 . . . . 5 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) ∈ ℝ*)
38 0xr 11135 . . . . . 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 3942 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ ℝ)
4520ffvelcdmda 7029 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ (0[,)+∞))
46 elrege0 13299 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘₯) ∈ (0[,)+∞) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)))
4745, 46sylib 217 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)))
4847simpld 495 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
4944, 48syldan 591 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
50 itg2gt0.5 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 0 < (πΉβ€˜π‘₯))
51 nnrecl 12344 . . . . . . . . . . . . 13 (((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 < (πΉβ€˜π‘₯)) β†’ βˆƒπ‘˜ ∈ β„• (1 / π‘˜) < (πΉβ€˜π‘₯))
5249, 50, 51syl2anc 584 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ βˆƒπ‘˜ ∈ β„• (1 / π‘˜) < (πΉβ€˜π‘₯))
5320ffnd 6664 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹 Fn ℝ)
5453ad2antrr 724 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ 𝐹 Fn ℝ)
55 elpreima 7003 . . . . . . . . . . . . . . . 16 (𝐹 Fn ℝ β†’ (π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ↔ (π‘₯ ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞))))
5654, 55syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ↔ (π‘₯ ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞))))
5744adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ π‘₯ ∈ ℝ)
5857biantrurd 533 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞) ↔ (π‘₯ ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞))))
59 nnrecre 12128 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ β„• β†’ (1 / π‘˜) ∈ ℝ)
6059adantl 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ ℝ)
6160rexrd 11138 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ ℝ*)
6261adantlr 713 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ ℝ*)
63 elioopnf 13288 . . . . . . . . . . . . . . . 16 ((1 / π‘˜) ∈ ℝ* β†’ ((πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ (1 / π‘˜) < (πΉβ€˜π‘₯))))
6462, 63syl 17 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ ((πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ (1 / π‘˜) < (πΉβ€˜π‘₯))))
6556, 58, 643bitr2d 306 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ (1 / π‘˜) < (πΉβ€˜π‘₯))))
66 id 22 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•)
67 imaexg 7842 . . . . . . . . . . . . . . . . . 18 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ V)
6812, 67syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ V)
6968adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ V)
70 oveq2 7357 . . . . . . . . . . . . . . . . . . 19 (𝑛 = π‘˜ β†’ (1 / 𝑛) = (1 / π‘˜))
7170oveq1d 7364 . . . . . . . . . . . . . . . . . 18 (𝑛 = π‘˜ β†’ ((1 / 𝑛)(,)+∞) = ((1 / π‘˜)(,)+∞))
7271imaeq2d 6009 . . . . . . . . . . . . . . . . 17 (𝑛 = π‘˜ β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) = (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))
73 eqid 2737 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) = (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))
7472, 73fvmptg 6941 . . . . . . . . . . . . . . . 16 ((π‘˜ ∈ β„• ∧ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ V) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))
7566, 69, 74syl2anr 597 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))
7675eleq2d 2823 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) ↔ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))
7749adantr 481 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
7877biantrurd 533 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ ((1 / π‘˜) < (πΉβ€˜π‘₯) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ (1 / π‘˜) < (πΉβ€˜π‘₯))))
7965, 76, 783bitr4rd 311 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ 𝐴) ∧ π‘˜ ∈ β„•) β†’ ((1 / π‘˜) < (πΉβ€˜π‘₯) ↔ π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8079rexbidva 3171 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ (βˆƒπ‘˜ ∈ β„• (1 / π‘˜) < (πΉβ€˜π‘₯) ↔ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8152, 80mpbid 231 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜))
8281ex 413 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ 𝐴 β†’ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
83 eluni2 4867 . . . . . . . . . . 11 (π‘₯ ∈ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) ↔ βˆƒπ‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))π‘₯ ∈ 𝑧)
84 eleq2 2826 . . . . . . . . . . . . 13 (𝑧 = ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) β†’ (π‘₯ ∈ 𝑧 ↔ π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8584rexrn 7031 . . . . . . . . . . . 12 ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) Fn β„• β†’ (βˆƒπ‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))π‘₯ ∈ 𝑧 ↔ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8617, 85syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (βˆƒπ‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))π‘₯ ∈ 𝑧 ↔ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8783, 86bitrid 282 . . . . . . . . . 10 (πœ‘ β†’ (π‘₯ ∈ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) ↔ βˆƒπ‘˜ ∈ β„• π‘₯ ∈ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
8882, 87sylibrd 258 . . . . . . . . 9 (πœ‘ β†’ (π‘₯ ∈ 𝐴 β†’ π‘₯ ∈ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
8988ssrdv 3948 . . . . . . . 8 (πœ‘ β†’ 𝐴 βŠ† βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))
90 ovolss 24771 . . . . . . . 8 ((𝐴 βŠ† βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) ∧ βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† ℝ) β†’ (vol*β€˜π΄) ≀ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
9189, 34, 90syl2anc 584 . . . . . . 7 (πœ‘ β†’ (vol*β€˜π΄) ≀ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
9241, 91eqbrtrd 5125 . . . . . 6 (πœ‘ β†’ (volβ€˜π΄) ≀ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))))
9392adantr 481 . . . . 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 12098 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
9796adantl 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„•)
98 nnrecre 12128 . . . . . . . . . . . . . . 15 ((π‘˜ + 1) ∈ β„• β†’ (1 / (π‘˜ + 1)) ∈ ℝ)
9997, 98syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / (π‘˜ + 1)) ∈ ℝ)
10099rexrd 11138 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / (π‘˜ + 1)) ∈ ℝ*)
101 nnre 12093 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ π‘˜ ∈ ℝ)
102101adantl 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ ℝ)
103102lep1d 12019 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ≀ (π‘˜ + 1))
104 nngt0 12117 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ 0 < π‘˜)
105104adantl 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 0 < π‘˜)
10697nnred 12101 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ ℝ)
10797nngt0d 12135 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 0 < (π‘˜ + 1))
108 lerec 11971 . . . . . . . . . . . . . . 15 (((π‘˜ ∈ ℝ ∧ 0 < π‘˜) ∧ ((π‘˜ + 1) ∈ ℝ ∧ 0 < (π‘˜ + 1))) β†’ (π‘˜ ≀ (π‘˜ + 1) ↔ (1 / (π‘˜ + 1)) ≀ (1 / π‘˜)))
109102, 105, 106, 107, 108syl22anc 837 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ ≀ (π‘˜ + 1) ↔ (1 / (π‘˜ + 1)) ≀ (1 / π‘˜)))
110103, 109mpbid 231 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / (π‘˜ + 1)) ≀ (1 / π‘˜))
111 iooss1 13227 . . . . . . . . . . . . 13 (((1 / (π‘˜ + 1)) ∈ ℝ* ∧ (1 / (π‘˜ + 1)) ≀ (1 / π‘˜)) β†’ ((1 / π‘˜)(,)+∞) βŠ† ((1 / (π‘˜ + 1))(,)+∞))
112100, 110, 111syl2anc 584 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((1 / π‘˜)(,)+∞) βŠ† ((1 / (π‘˜ + 1))(,)+∞))
113 imass2 6050 . . . . . . . . . . . 12 (((1 / π‘˜)(,)+∞) βŠ† ((1 / (π‘˜ + 1))(,)+∞) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) βŠ† (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)))
114112, 113syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) βŠ† (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)))
11566, 68, 74syl2anr 597 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))
116 imaexg 7842 . . . . . . . . . . . . 13 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)) ∈ V)
11712, 116syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)) ∈ V)
118 oveq2 7357 . . . . . . . . . . . . . . 15 (𝑛 = (π‘˜ + 1) β†’ (1 / 𝑛) = (1 / (π‘˜ + 1)))
119118oveq1d 7364 . . . . . . . . . . . . . 14 (𝑛 = (π‘˜ + 1) β†’ ((1 / 𝑛)(,)+∞) = ((1 / (π‘˜ + 1))(,)+∞))
120119imaeq2d 6009 . . . . . . . . . . . . 13 (𝑛 = (π‘˜ + 1) β†’ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)) = (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)))
121120, 73fvmptg 6941 . . . . . . . . . . . 12 (((π‘˜ + 1) ∈ β„• ∧ (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)) ∈ V) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜(π‘˜ + 1)) = (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)))
12296, 117, 121syl2anr 597 . . . . . . . . . . 11 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜(π‘˜ + 1)) = (◑𝐹 β€œ ((1 / (π‘˜ + 1))(,)+∞)))
123114, 115, 1223sstr4d 3989 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) βŠ† ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜(π‘˜ + 1)))
124123ralrimiva 3141 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) βŠ† ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜(π‘˜ + 1)))
125 volsup 24842 . . . . . . . . 9 (((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))):β„•βŸΆdom vol ∧ βˆ€π‘˜ ∈ β„• ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) βŠ† ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜(π‘˜ + 1))) β†’ (volβ€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) = sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ))
12627, 124, 125syl2anc 584 . . . . . . . 8 (πœ‘ β†’ (volβ€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) = sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ))
12795, 126eqtr3d 2779 . . . . . . 7 (πœ‘ β†’ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) = sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ))
128127adantr 481 . . . . . 6 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) = sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ))
12968adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ V)
13066, 129, 74syl2anr 597 . . . . . . . . . . . 12 (((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) ∧ π‘˜ ∈ β„•) β†’ ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) = (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))
131130fveq2d 6841 . . . . . . . . . . 11 (((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) ∧ π‘˜ ∈ β„•) β†’ (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) = (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))
13238a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ 0 ∈ ℝ*)
133 nnrecgt0 12129 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ ∈ β„• β†’ 0 < (1 / π‘˜))
134133adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 0 < (1 / π‘˜))
135 0re 11090 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ ℝ
136 ltle 11176 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 ∈ ℝ ∧ (1 / π‘˜) ∈ ℝ) β†’ (0 < (1 / π‘˜) β†’ 0 ≀ (1 / π‘˜)))
137135, 60, 136sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (0 < (1 / π‘˜) β†’ 0 ≀ (1 / π‘˜)))
138134, 137mpd 15 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 0 ≀ (1 / π‘˜))
139 elxrge0 13302 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 / π‘˜) ∈ (0[,]+∞) ↔ ((1 / π‘˜) ∈ ℝ* ∧ 0 ≀ (1 / π‘˜)))
14061, 138, 139sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ (0[,]+∞))
141 0e0iccpnf 13304 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ (0[,]+∞)
142 ifcl 4529 . . . . . . . . . . . . . . . . . . . . . 22 (((1 / π‘˜) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ∈ (0[,]+∞))
143140, 141, 142sylancl 586 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ∈ (0[,]+∞))
144143adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ∈ (0[,]+∞))
145144fmpttd 7057 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)):β„βŸΆ(0[,]+∞))
146145adantrr 715 . . . . . . . . . . . . . . . . . 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 13281 . . . . . . . . . . . . . . . . . . . 20 (0[,)+∞) βŠ† (0[,]+∞)
150 fss 6680 . . . . . . . . . . . . . . . . . . . 20 ((𝐹:β„βŸΆ(0[,)+∞) ∧ (0[,)+∞) βŠ† (0[,]+∞)) β†’ 𝐹:β„βŸΆ(0[,]+∞))
15120, 149, 150sylancl 586 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐹:β„βŸΆ(0[,]+∞))
152 itg2cl 25019 . . . . . . . . . . . . . . . . . . 19 (𝐹:β„βŸΆ(0[,]+∞) β†’ (∫2β€˜πΉ) ∈ ℝ*)
153151, 152syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (∫2β€˜πΉ) ∈ ℝ*)
154153adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (∫2β€˜πΉ) ∈ ℝ*)
155 0nrp 12878 . . . . . . . . . . . . . . . . . . 19 Β¬ 0 ∈ ℝ+
156 simpr 485 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))))
157115, 28eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol)
158157adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol)
159158adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol)
160156, 135eqeltrrdi 2847 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∈ ℝ)
16160, 134elrpd 12882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ ℝ+)
162161adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (1 / π‘˜) ∈ ℝ+)
163162adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ ((volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ ↔ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ∈ ℝ))
166160, 165mpbird 256 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ)
167 elrege0 13299 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 / π‘˜) ∈ (0[,)+∞) ↔ ((1 / π‘˜) ∈ ℝ ∧ 0 ≀ (1 / π‘˜)))
16860, 138, 167sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (1 / π‘˜) ∈ (0[,)+∞))
169168adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (1 / π‘˜) ∈ (0[,)+∞))
170169adantr 481 . . . . . . . . . . . . . . . . . . . . . . 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 1371 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) = ((1 / π‘˜) Β· (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
173156, 172eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ 0 = ((1 / π‘˜) Β· (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
174 simplrr 776 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))
175166, 174elrpd 12882 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ+)
176163, 175rpmulcld 12901 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ ((1 / π‘˜) Β· (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))) ∈ ℝ+)
177173, 176eqeltrd 2838 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) ∧ 0 = (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))) β†’ 0 ∈ ℝ+)
178177ex 413 . . . . . . . . . . . . . . . . . . 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 12991 . . . . . . . . . . . . . . . . . . . . 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 587 . . . . . . . . . . . . . . . . . . . 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 862 . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ 𝐹:β„βŸΆ(0[,]+∞))
18860adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (1 / π‘˜) ∈ ℝ)
18953adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ 𝐹 Fn ℝ)
190189, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ↔ (π‘₯ ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞))))
191190biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (π‘₯ ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞)))
192191simpld 495 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ π‘₯ ∈ ℝ)
19348adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
194192, 193syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
19561adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (1 / π‘˜) ∈ ℝ*)
196191simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞))
197 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πΉβ€˜π‘₯) ∈ ℝ ∧ (1 / π‘˜) < (πΉβ€˜π‘₯)) β†’ (1 / π‘˜) < (πΉβ€˜π‘₯))
19863, 197syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1 / π‘˜) ∈ ℝ* β†’ ((πΉβ€˜π‘₯) ∈ ((1 / π‘˜)(,)+∞) β†’ (1 / π‘˜) < (πΉβ€˜π‘₯)))
199195, 196, 198sylc 65 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (1 / π‘˜) < (πΉβ€˜π‘₯))
200188, 194, 199ltled 11236 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ (1 / π‘˜) ≀ (πΉβ€˜π‘₯))
20147simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (πΉβ€˜π‘₯))
202201adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ 0 ≀ (πΉβ€˜π‘₯))
203192, 202syldan 591 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ 0 ≀ (πΉβ€˜π‘₯))
204 breq1 5106 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 / π‘˜) = if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) β†’ ((1 / π‘˜) ≀ (πΉβ€˜π‘₯) ↔ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯)))
205 breq1 5106 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 = if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) β†’ (0 ≀ (πΉβ€˜π‘₯) ↔ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯)))
206204, 205ifboth 4523 . . . . . . . . . . . . . . . . . . . . . . . 24 (((1 / π‘˜) ≀ (πΉβ€˜π‘₯) ∧ 0 ≀ (πΉβ€˜π‘₯)) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
207200, 203, 206syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
208207adantlr 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
209 iffalse 4493 . . . . . . . . . . . . . . . . . . . . . . . 24 (Β¬ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) = 0)
210209adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) = 0)
211202adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ 0 ≀ (πΉβ€˜π‘₯))
212210, 211eqbrtrd 5125 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) ∧ Β¬ π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
213208, 212pm2.61dan 811 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
214213ralrimiva 3141 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
215214adantrr 715 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯))
216 reex 11075 . . . . . . . . . . . . . . . . . . . . . 22 ℝ ∈ V
217216a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ℝ ∈ V)
218 ovex 7382 . . . . . . . . . . . . . . . . . . . . . . 23 (1 / π‘˜) ∈ V
219 c0ex 11082 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ V
220218, 219ifex 4534 . . . . . . . . . . . . . . . . . . . . . 22 if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ∈ V
221220a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ∈ V)
222 fvexd 6852 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜π‘₯) ∈ V)
223 eqidd 2738 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)))
22420feqmptd 6905 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐹 = (π‘₯ ∈ ℝ ↦ (πΉβ€˜π‘₯)))
225217, 221, 222, 223, 224ofrfval2 7628 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)) ∘r ≀ 𝐹 ↔ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯)))
226225biimpar 478 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ βˆ€π‘₯ ∈ ℝ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0) ≀ (πΉβ€˜π‘₯)) β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0)) ∘r ≀ 𝐹)
227215, 226syldan 591 . . . . . . . . . . . . . . . . . 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 1371 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ (∫2β€˜(π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (◑𝐹 β€œ ((1 / π‘˜)(,)+∞)), (1 / π‘˜), 0))) ≀ (∫2β€˜πΉ))
230132, 148, 154, 186, 229xrltletrd 13008 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π‘˜ ∈ β„• ∧ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))))) β†’ 0 < (∫2β€˜πΉ))
231230expr 457 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) β†’ 0 < (∫2β€˜πΉ)))
232231con3d 152 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (Β¬ 0 < (∫2β€˜πΉ) β†’ Β¬ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
2334ffvelcdmi 7028 . . . . . . . . . . . . . . . . 17 ((◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ (0[,]+∞))
2343, 233sselid 3940 . . . . . . . . . . . . . . . 16 ((◑𝐹 β€œ ((1 / π‘˜)(,)+∞)) ∈ dom vol β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ*)
235157, 234syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ*)
236 xrlenlt 11153 . . . . . . . . . . . . . . 15 (((volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ∈ ℝ* ∧ 0 ∈ ℝ*) β†’ ((volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ≀ 0 ↔ Β¬ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
237235, 38, 236sylancl 586 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ ((volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ≀ 0 ↔ Β¬ 0 < (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞)))))
238232, 237sylibrd 258 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘˜ ∈ β„•) β†’ (Β¬ 0 < (∫2β€˜πΉ) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ≀ 0))
239238imp 407 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘˜ ∈ β„•) ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ≀ 0)
240239an32s 650 . . . . . . . . . . 11 (((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) ∧ π‘˜ ∈ β„•) β†’ (volβ€˜(◑𝐹 β€œ ((1 / π‘˜)(,)+∞))) ≀ 0)
241131, 240eqbrtrd 5125 . . . . . . . . . 10 (((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) ∧ π‘˜ ∈ β„•) β†’ (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0)
242241ralrimiva 3141 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ βˆ€π‘˜ ∈ β„• (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0)
243 ffn 6663 . . . . . . . . . . 11 ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))):β„•βŸΆV β†’ (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) Fn β„•)
244 fveq2 6837 . . . . . . . . . . . . 13 (𝑧 = ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) β†’ (volβ€˜π‘§) = (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)))
245244breq1d 5113 . . . . . . . . . . . 12 (𝑧 = ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜) β†’ ((volβ€˜π‘§) ≀ 0 ↔ (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0))
246245ralrn 7032 . . . . . . . . . . 11 ((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) Fn β„• β†’ (βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0 ↔ βˆ€π‘˜ ∈ β„• (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0))
24716, 243, 2463syl 18 . . . . . . . . . 10 (πœ‘ β†’ (βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0 ↔ βˆ€π‘˜ ∈ β„• (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0))
248247adantr 481 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0 ↔ βˆ€π‘˜ ∈ β„• (volβ€˜((𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))β€˜π‘˜)) ≀ 0))
249242, 248mpbird 256 . . . . . . . 8 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0)
250 ffn 6663 . . . . . . . . . 10 (vol:dom vol⟢(0[,]+∞) β†’ vol Fn dom vol)
2514, 250ax-mp 5 . . . . . . . . 9 vol Fn dom vol
25227frnd 6671 . . . . . . . . . 10 (πœ‘ β†’ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† dom vol)
253252adantr 481 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† dom vol)
254 breq1 5106 . . . . . . . . . 10 (π‘₯ = (volβ€˜π‘§) β†’ (π‘₯ ≀ 0 ↔ (volβ€˜π‘§) ≀ 0))
255254ralima 7182 . . . . . . . . 9 ((vol Fn dom vol ∧ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))) βŠ† dom vol) β†’ (βˆ€π‘₯ ∈ (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))π‘₯ ≀ 0 ↔ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0))
256251, 253, 255sylancr 587 . . . . . . . 8 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (βˆ€π‘₯ ∈ (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))π‘₯ ≀ 0 ↔ βˆ€π‘§ ∈ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))(volβ€˜π‘§) ≀ 0))
257249, 256mpbird 256 . . . . . . 7 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ βˆ€π‘₯ ∈ (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))π‘₯ ≀ 0)
258 imassrn 6020 . . . . . . . . 9 (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) βŠ† ran vol
259 frn 6670 . . . . . . . . . . 11 (vol:dom vol⟢(0[,]+∞) β†’ ran vol βŠ† (0[,]+∞))
2604, 259ax-mp 5 . . . . . . . . . 10 ran vol βŠ† (0[,]+∞)
261260, 3sstri 3951 . . . . . . . . 9 ran vol βŠ† ℝ*
262258, 261sstri 3951 . . . . . . . 8 (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) βŠ† ℝ*
263 supxrleub 13173 . . . . . . . 8 (((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) βŠ† ℝ* ∧ 0 ∈ ℝ*) β†’ (sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ) ≀ 0 ↔ βˆ€π‘₯ ∈ (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))π‘₯ ≀ 0))
264262, 38, 263mp2an 690 . . . . . . 7 (sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ) ≀ 0 ↔ βˆ€π‘₯ ∈ (vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞))))π‘₯ ≀ 0)
265257, 264sylibr 233 . . . . . 6 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ sup((vol β€œ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))), ℝ*, < ) ≀ 0)
266128, 265eqbrtrd 5125 . . . . 5 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (vol*β€˜βˆͺ ran (𝑛 ∈ β„• ↦ (◑𝐹 β€œ ((1 / 𝑛)(,)+∞)))) ≀ 0)
2678, 37, 39, 93, 266xrletrd 13009 . . . 4 ((πœ‘ ∧ Β¬ 0 < (∫2β€˜πΉ)) β†’ (volβ€˜π΄) ≀ 0)
268267ex 413 . . 3 (πœ‘ β†’ (Β¬ 0 < (∫2β€˜πΉ) β†’ (volβ€˜π΄) ≀ 0))
269 xrlenlt 11153 . . . 4 (((volβ€˜π΄) ∈ ℝ* ∧ 0 ∈ ℝ*) β†’ ((volβ€˜π΄) ≀ 0 ↔ Β¬ 0 < (volβ€˜π΄)))
2707, 38, 269sylancl 586 . . 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 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3443   βŠ† wss 3908  ifcif 4484  βˆͺ cuni 4863  βˆͺ ciun 4952   class class class wbr 5103   ↦ cmpt 5186  β—‘ccnv 5629  dom cdm 5630  ran crn 5631   β€œ cima 5633   Fn wfn 6486  βŸΆwf 6487  β€˜cfv 6491  (class class class)co 7349   ∘r cofr 7606  supcsup 9309  β„cr 10983  0cc0 10984  1c1 10985   + caddc 10987   Β· cmul 10989  +∞cpnf 11119  β„*cxr 11121   < clt 11122   ≀ cle 11123   / cdiv 11745  β„•cn 12086  β„+crp 12843  (,)cioo 13192  [,)cico 13194  [,]cicc 13195  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 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 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7662  ax-inf2 9510  ax-cc 10304  ax-cnex 11040  ax-resscn 11041  ax-1cn 11042  ax-icn 11043  ax-addcl 11044  ax-addrcl 11045  ax-mulcl 11046  ax-mulrcl 11047  ax-mulcom 11048  ax-addass 11049  ax-mulass 11050  ax-distr 11051  ax-i2m1 11052  ax-1ne0 11053  ax-1rid 11054  ax-rnegex 11055  ax-rrecex 11056  ax-cnre 11057  ax-pre-lttri 11058  ax-pre-lttrn 11059  ax-pre-ltadd 11060  ax-pre-mulgt0 11061  ax-pre-sup 11062  ax-addf 11063
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-disj 5069  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5528  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5585  df-se 5586  df-we 5587  df-xp 5636  df-rel 5637  df-cnv 5638  df-co 5639  df-dm 5640  df-rn 5641  df-res 5642  df-ima 5643  df-pred 6249  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6443  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-isom 6500  df-riota 7305  df-ov 7352  df-oprab 7353  df-mpo 7354  df-of 7607  df-ofr 7608  df-om 7793  df-1st 7911  df-2nd 7912  df-frecs 8179  df-wrecs 8210  df-recs 8284  df-rdg 8323  df-1o 8379  df-2o 8380  df-er 8581  df-map 8700  df-pm 8701  df-en 8817  df-dom 8818  df-sdom 8819  df-fin 8820  df-fi 9280  df-sup 9311  df-inf 9312  df-oi 9379  df-dju 9770  df-card 9808  df-pnf 11124  df-mnf 11125  df-xr 11126  df-ltxr 11127  df-le 11128  df-sub 11320  df-neg 11321  df-div 11746  df-nn 12087  df-2 12149  df-3 12150  df-n0 12347  df-z 12433  df-uz 12696  df-q 12802  df-rp 12844  df-xneg 12961  df-xadd 12962  df-xmul 12963  df-ioo 13196  df-ico 13198  df-icc 13199  df-fz 13353  df-fzo 13496  df-fl 13625  df-seq 13835  df-exp 13896  df-hash 14158  df-cj 14917  df-re 14918  df-im 14919  df-sqrt 15053  df-abs 15054  df-clim 15304  df-rlim 15305  df-sum 15505  df-rest 17238  df-topgen 17259  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