Metamath Proof Explorer

Theorem itg2gt0

Description: If the function F is strictly positive on a set of positive measure, then the integral of the function is positive. (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Hypotheses itg2gt0.1 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
itg2gt0.2 ⊢ ( 𝜑 → 0 < ( vol ‘ 𝐴 ) )
itg2gt0.3 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2gt0.4 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
itg2gt0.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 < ( 𝐹 ‘ 𝑥 ) )
Assertion itg2gt0 ( 𝜑 → 0 < ( ∫2 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 itg2gt0.1 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
2 itg2gt0.2 ⊢ ( 𝜑 → 0 < ( vol ‘ 𝐴 ) )
3 itg2gt0.3 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
4 itg2gt0.4 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
5 itg2gt0.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 < ( 𝐹 ‘ 𝑥 ) )
6 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
7 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
8 7 ffvelrni ⊢ ( 𝐴 ∈ dom vol → ( vol ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
9 6 8 sselid ⊢ ( 𝐴 ∈ dom vol → ( vol ‘ 𝐴 ) ∈ ℝ* )
10 1 9 syl ⊢ ( 𝜑 → ( vol ‘ 𝐴 ) ∈ ℝ* )
11 10 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ( vol ‘ 𝐴 ) ∈ ℝ* )
12 4 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
13 cnvexg ⊢ ( 𝐹 ∈ V → ◡ 𝐹 ∈ V )
14 12 13 syl ⊢ ( 𝜑 → ◡ 𝐹 ∈ V )
15 imaexg ⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ∈ V )
16 14 15 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ∈ V )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ∈ V )
18 17 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) : ℕ ⟶ V )
19 18 ffnd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) Fn ℕ )
20 fniunfv ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) Fn ℕ → ∪ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) )
21 19 20 syl ⊢ ( 𝜑 → ∪ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) )
22 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
23 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
24 3 22 23 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
25 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : ℝ ⟶ ℝ ) → ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ∈ dom vol )
26 4 24 25 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ∈ dom vol )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ∈ dom vol )
28 27 fmpttd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) : ℕ ⟶ dom vol )
29 28 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ∈ dom vol )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ∈ dom vol )
31 iunmbl ⊢ ( ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ∈ dom vol → ∪ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ∈ dom vol )
32 30 31 syl ⊢ ( 𝜑 → ∪ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ∈ dom vol )
33 21 32 eqeltrrd ⊢ ( 𝜑 → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ∈ dom vol )
34 mblss ⊢ ( ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ∈ dom vol → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ⊆ ℝ )
35 33 34 syl ⊢ ( 𝜑 → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ⊆ ℝ )
36 ovolcl ⊢ ( ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ⊆ ℝ → ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) ∈ ℝ* )
37 35 36 syl ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) ∈ ℝ* )
38 37 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) ∈ ℝ* )
39 0xr ⊢ 0 ∈ ℝ*
40 39 a1i ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → 0 ∈ ℝ* )
41 mblvol ⊢ ( 𝐴 ∈ dom vol → ( vol ‘ 𝐴 ) = ( vol* ‘ 𝐴 ) )
42 1 41 syl ⊢ ( 𝜑 → ( vol ‘ 𝐴 ) = ( vol* ‘ 𝐴 ) )
43 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
44 1 43 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
45 44 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
46 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
47 elrege0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
48 46 47 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
49 48 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
50 45 49 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
51 nnrecl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) )
52 50 5 51 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) )
53 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℝ )
54 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝐹 Fn ℝ )
55 elpreima ⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) )
56 54 55 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) )
57 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ ℝ )
58 57 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 1 / 𝑘 ) (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) )
59 nnrecre ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
60 59 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ )
61 60 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ* )
62 61 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ* )
63 elioopnf ⊢ ( ( 1 / 𝑘 ) ∈ ℝ* → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 1 / 𝑘 ) (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) ) ) )
64 62 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 1 / 𝑘 ) (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) ) ) )
65 56 58 64 3bitr2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) ) ) )
66 id ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ )
67 imaexg ⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ V )
68 14 67 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ V )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ V )
70 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 1 / 𝑛 ) = ( 1 / 𝑘 ) )
71 70 oveq1d ⊢ ( 𝑛 = 𝑘 → ( ( 1 / 𝑛 ) (,) +∞ ) = ( ( 1 / 𝑘 ) (,) +∞ ) )
72 71 imaeq2d ⊢ ( 𝑛 = 𝑘 → ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) = ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) )
73 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) )
74 72 73 fvmptg ⊢ ( ( 𝑘 ∈ ℕ ∧ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) = ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) )
75 66 69 74 syl2anr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) = ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) )
76 75 eleq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) )
77 50 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
78 77 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) ) ) )
79 65 76 78 3bitr4rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 ∈ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) )
80 79 rexbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑘 ∈ ℕ ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑘 ∈ ℕ 𝑥 ∈ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) )
81 52 80 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑘 ∈ ℕ 𝑥 ∈ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) )
82 81 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ∃ 𝑘 ∈ ℕ 𝑥 ∈ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) )
83 eluni2 ⊢ ( 𝑥 ∈ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ↔ ∃ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) 𝑥 ∈ 𝑧 )
84 eleq2 ⊢ ( 𝑧 = ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) )
85 84 rexrn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) Fn ℕ → ( ∃ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) 𝑥 ∈ 𝑧 ↔ ∃ 𝑘 ∈ ℕ 𝑥 ∈ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) )
86 19 85 syl ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) 𝑥 ∈ 𝑧 ↔ ∃ 𝑘 ∈ ℕ 𝑥 ∈ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) )
87 83 86 syl5bb ⊢ ( 𝜑 → ( 𝑥 ∈ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ↔ ∃ 𝑘 ∈ ℕ 𝑥 ∈ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) )
88 82 87 sylibrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) )
89 88 ssrdv ⊢ ( 𝜑 → 𝐴 ⊆ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) )
90 ovolss ⊢ ( ( 𝐴 ⊆ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ∧ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ⊆ ℝ ) → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) )
91 89 35 90 syl2anc ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) ≤ ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) )
92 42 91 eqbrtrd ⊢ ( 𝜑 → ( vol ‘ 𝐴 ) ≤ ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) )
93 92 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ( vol ‘ 𝐴 ) ≤ ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) )
94 mblvol ⊢ ( ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ∈ dom vol → ( vol ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) = ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) )
95 33 94 syl ⊢ ( 𝜑 → ( vol ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) = ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) )
96 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
97 96 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
98 nnrecre ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 1 / ( 𝑘 + 1 ) ) ∈ ℝ )
99 97 98 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / ( 𝑘 + 1 ) ) ∈ ℝ )
100 99 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / ( 𝑘 + 1 ) ) ∈ ℝ* )
101 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
102 101 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ )
103 102 lep1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ≤ ( 𝑘 + 1 ) )
104 nngt0 ⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
105 104 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 < 𝑘 )
106 97 nnred ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℝ )
107 97 nngt0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 < ( 𝑘 + 1 ) )
108 lerec ⊢ ( ( ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ∧ ( ( 𝑘 + 1 ) ∈ ℝ ∧ 0 < ( 𝑘 + 1 ) ) ) → ( 𝑘 ≤ ( 𝑘 + 1 ) ↔ ( 1 / ( 𝑘 + 1 ) ) ≤ ( 1 / 𝑘 ) ) )
109 102 105 106 107 108 syl22anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 ≤ ( 𝑘 + 1 ) ↔ ( 1 / ( 𝑘 + 1 ) ) ≤ ( 1 / 𝑘 ) ) )
110 103 109 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / ( 𝑘 + 1 ) ) ≤ ( 1 / 𝑘 ) )
111 iooss1 ⊢ ( ( ( 1 / ( 𝑘 + 1 ) ) ∈ ℝ* ∧ ( 1 / ( 𝑘 + 1 ) ) ≤ ( 1 / 𝑘 ) ) → ( ( 1 / 𝑘 ) (,) +∞ ) ⊆ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) )
112 100 110 111 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑘 ) (,) +∞ ) ⊆ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) )
113 imass2 ⊢ ( ( ( 1 / 𝑘 ) (,) +∞ ) ⊆ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) → ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ⊆ ( ◡ 𝐹 “ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) ) )
114 112 113 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ⊆ ( ◡ 𝐹 “ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) ) )
115 66 68 74 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) = ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) )
116 imaexg ⊢ ( ◡ 𝐹 ∈ V → ( ◡ 𝐹 “ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) ) ∈ V )
117 14 116 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) ) ∈ V )
118 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 1 / 𝑛 ) = ( 1 / ( 𝑘 + 1 ) ) )
119 118 oveq1d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 1 / 𝑛 ) (,) +∞ ) = ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) )
120 119 imaeq2d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) = ( ◡ 𝐹 “ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) ) )
121 120 73 fvmptg ⊢ ( ( ( 𝑘 + 1 ) ∈ ℕ ∧ ( ◡ 𝐹 “ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) ) ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ◡ 𝐹 “ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) ) )
122 96 117 121 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ ( 𝑘 + 1 ) ) = ( ◡ 𝐹 “ ( ( 1 / ( 𝑘 + 1 ) ) (,) +∞ ) ) )
123 114 115 122 3sstr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ ( 𝑘 + 1 ) ) )
124 123 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ ( 𝑘 + 1 ) ) )
125 volsup ⊢ ( ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) : ℕ ⟶ dom vol ∧ ∀ 𝑘 ∈ ℕ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ⊆ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ ( 𝑘 + 1 ) ) ) → ( vol ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) = sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) , ℝ* , < ) )
126 28 124 125 syl2anc ⊢ ( 𝜑 → ( vol ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) = sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) , ℝ* , < ) )
127 95 126 eqtr3d ⊢ ( 𝜑 → ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) = sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) , ℝ* , < ) )
128 127 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) = sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) , ℝ* , < ) )
129 68 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ V )
130 66 129 74 syl2anr ⊢ ( ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) = ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) )
131 130 fveq2d ⊢ ( ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) = ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) )
132 39 a1i ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → 0 ∈ ℝ* )
133 nnrecgt0 ⊢ ( 𝑘 ∈ ℕ → 0 < ( 1 / 𝑘 ) )
134 133 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 < ( 1 / 𝑘 ) )
135 0re ⊢ 0 ∈ ℝ
136 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( 1 / 𝑘 ) ∈ ℝ ) → ( 0 < ( 1 / 𝑘 ) → 0 ≤ ( 1 / 𝑘 ) ) )
137 135 60 136 sylancr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 0 < ( 1 / 𝑘 ) → 0 ≤ ( 1 / 𝑘 ) ) )
138 134 137 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 ≤ ( 1 / 𝑘 ) )
139 elxrge0 ⊢ ( ( 1 / 𝑘 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 1 / 𝑘 ) ∈ ℝ* ∧ 0 ≤ ( 1 / 𝑘 ) ) )
140 61 138 139 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ( 0 [,] +∞ ) )
141 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
142 ifcl ⊢ ( ( ( 1 / 𝑘 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ∈ ( 0 [,] +∞ ) )
143 140 141 142 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ∈ ( 0 [,] +∞ ) )
144 143 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ∈ ( 0 [,] +∞ ) )
145 144 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
146 145 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
147 itg2cl ⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ∈ ℝ* )
148 146 147 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ∈ ℝ* )
149 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
150 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
151 3 149 150 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
152 itg2cl ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
153 151 152 syl ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
154 153 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
155 0nrp ⊢ ¬ 0 ∈ ℝ+
156 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) )
157 115 29 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ dom vol )
158 157 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ dom vol )
159 158 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ dom vol )
160 156 135 eqeltrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ∈ ℝ )
161 60 134 elrpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ+ )
162 161 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( 1 / 𝑘 ) ∈ ℝ+ )
163 162 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → ( 1 / 𝑘 ) ∈ ℝ+ )
164 itg2const2 ⊢ ( ( ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ dom vol ∧ ( 1 / 𝑘 ) ∈ ℝ+ ) → ( ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ∈ ℝ ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ∈ ℝ ) )
165 159 163 164 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → ( ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ∈ ℝ ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ∈ ℝ ) )
166 160 165 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ∈ ℝ )
167 elrege0 ⊢ ( ( 1 / 𝑘 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 1 / 𝑘 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝑘 ) ) )
168 60 138 167 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ( 0 [,) +∞ ) )
169 168 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( 1 / 𝑘 ) ∈ ( 0 [,) +∞ ) )
170 169 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → ( 1 / 𝑘 ) ∈ ( 0 [,) +∞ ) )
171 itg2const ⊢ ( ( ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ dom vol ∧ ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ∈ ℝ ∧ ( 1 / 𝑘 ) ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) = ( ( 1 / 𝑘 ) · ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) )
172 159 166 170 171 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) = ( ( 1 / 𝑘 ) · ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) )
173 156 172 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → 0 = ( ( 1 / 𝑘 ) · ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) )
174 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) )
175 166 174 elrpd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ∈ ℝ+ )
176 163 175 rpmulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → ( ( 1 / 𝑘 ) · ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ∈ ℝ+ )
177 173 176 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) ∧ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) → 0 ∈ ℝ+ )
178 177 ex ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) → 0 ∈ ℝ+ ) )
179 155 178 mtoi ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ¬ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) )
180 itg2ge0 ⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) → 0 ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) )
181 146 180 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → 0 ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) )
182 xrleloe ⊢ ( ( 0 ∈ ℝ* ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ∈ ℝ* ) → ( 0 ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ↔ ( 0 < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ∨ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) ) )
183 39 148 182 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( 0 ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ↔ ( 0 < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ∨ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) ) )
184 181 183 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( 0 < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ∨ 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) )
185 184 ord ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( ¬ 0 < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) → 0 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ) )
186 179 185 mt3d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → 0 < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) )
187 151 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
188 60 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → ( 1 / 𝑘 ) ∈ ℝ )
189 53 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐹 Fn ℝ )
190 189 55 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) )
191 190 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 1 / 𝑘 ) (,) +∞ ) ) )
192 191 simpld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → 𝑥 ∈ ℝ )
193 49 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
194 192 193 syldan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
195 61 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → ( 1 / 𝑘 ) ∈ ℝ* )
196 191 simprd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 1 / 𝑘 ) (,) +∞ ) )
197 simpr ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) ) → ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) )
198 63 197 syl6bi ⊢ ( ( 1 / 𝑘 ) ∈ ℝ* → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 1 / 𝑘 ) (,) +∞ ) → ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) ) )
199 195 196 198 sylc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → ( 1 / 𝑘 ) < ( 𝐹 ‘ 𝑥 ) )
200 188 194 199 ltled ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → ( 1 / 𝑘 ) ≤ ( 𝐹 ‘ 𝑥 ) )
201 48 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
202 201 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
203 192 202 syldan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
204 breq1 ⊢ ( ( 1 / 𝑘 ) = if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) → ( ( 1 / 𝑘 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
205 breq1 ⊢ ( 0 = if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
206 204 205 ifboth ⊢ ( ( ( 1 / 𝑘 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
207 200 203 206 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
208 207 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
209 iffalse ⊢ ( ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) = 0 )
210 209 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) = 0 )
211 202 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
212 210 211 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
213 208 212 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
214 213 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
215 214 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
216 reex ⊢ ℝ ∈ V
217 216 a1i ⊢ ( 𝜑 → ℝ ∈ V )
218 ovex ⊢ ( 1 / 𝑘 ) ∈ V
219 c0ex ⊢ 0 ∈ V
220 218 219 ifex ⊢ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ∈ V
221 220 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ∈ V )
222 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ V )
223 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) )
224 3 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
225 217 221 222 223 224 ofrfval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
226 225 biimpar ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ∘r ≤ 𝐹 )
227 215 226 syldan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ∘r ≤ 𝐹 )
228 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
229 146 187 227 228 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) , ( 1 / 𝑘 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
230 132 148 154 186 229 xrltletrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) ) → 0 < ( ∫2 ‘ 𝐹 ) )
231 230 expr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) → 0 < ( ∫2 ‘ 𝐹 ) ) )
232 231 con3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ¬ 0 < ( ∫2 ‘ 𝐹 ) → ¬ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) )
233 7 ffvelrni ⊢ ( ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ∈ ( 0 [,] +∞ ) )
234 6 233 sselid ⊢ ( ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ∈ ℝ* )
235 157 234 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ∈ ℝ* )
236 xrlenlt ⊢ ( ( ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ≤ 0 ↔ ¬ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) )
237 235 39 236 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ≤ 0 ↔ ¬ 0 < ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ) )
238 232 237 sylibrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ¬ 0 < ( ∫2 ‘ 𝐹 ) → ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ≤ 0 ) )
239 238 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ≤ 0 )
240 239 an32s ⊢ ( ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ◡ 𝐹 “ ( ( 1 / 𝑘 ) (,) +∞ ) ) ) ≤ 0 )
241 131 240 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) ∧ 𝑘 ∈ ℕ ) → ( vol ‘ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) ≤ 0 )
242 241 ralrimiva ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ∀ 𝑘 ∈ ℕ ( vol ‘ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) ≤ 0 )
243 ffn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) : ℕ ⟶ V → ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) Fn ℕ )
244 fveq2 ⊢ ( 𝑧 = ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) → ( vol ‘ 𝑧 ) = ( vol ‘ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) )
245 244 breq1d ⊢ ( 𝑧 = ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) → ( ( vol ‘ 𝑧 ) ≤ 0 ↔ ( vol ‘ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) ≤ 0 ) )
246 245 ralrn ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) Fn ℕ → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ( vol ‘ 𝑧 ) ≤ 0 ↔ ∀ 𝑘 ∈ ℕ ( vol ‘ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) ≤ 0 ) )
247 18 243 246 3syl ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ( vol ‘ 𝑧 ) ≤ 0 ↔ ∀ 𝑘 ∈ ℕ ( vol ‘ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) ≤ 0 ) )
248 247 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ( ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ( vol ‘ 𝑧 ) ≤ 0 ↔ ∀ 𝑘 ∈ ℕ ( vol ‘ ( ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ‘ 𝑘 ) ) ≤ 0 ) )
249 242 248 mpbird ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ( vol ‘ 𝑧 ) ≤ 0 )
250 ffn ⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) → vol Fn dom vol )
251 7 250 ax-mp ⊢ vol Fn dom vol
252 28 frnd ⊢ ( 𝜑 → ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ⊆ dom vol )
253 252 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ⊆ dom vol )
254 breq1 ⊢ ( 𝑥 = ( vol ‘ 𝑧 ) → ( 𝑥 ≤ 0 ↔ ( vol ‘ 𝑧 ) ≤ 0 ) )
255 254 ralima ⊢ ( ( vol Fn dom vol ∧ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ⊆ dom vol ) → ( ∀ 𝑥 ∈ ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) 𝑥 ≤ 0 ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ( vol ‘ 𝑧 ) ≤ 0 ) )
256 251 253 255 sylancr ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ( ∀ 𝑥 ∈ ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) 𝑥 ≤ 0 ↔ ∀ 𝑧 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ( vol ‘ 𝑧 ) ≤ 0 ) )
257 249 256 mpbird ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ∀ 𝑥 ∈ ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) 𝑥 ≤ 0 )
258 imassrn ⊢ ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) ⊆ ran vol
259 frn ⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) → ran vol ⊆ ( 0 [,] +∞ ) )
260 7 259 ax-mp ⊢ ran vol ⊆ ( 0 [,] +∞ )
261 260 6 sstri ⊢ ran vol ⊆ ℝ*
262 258 261 sstri ⊢ ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) ⊆ ℝ*
263 supxrleub ⊢ ( ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) ⊆ ℝ* ∧ 0 ∈ ℝ* ) → ( sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) , ℝ* , < ) ≤ 0 ↔ ∀ 𝑥 ∈ ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) 𝑥 ≤ 0 ) )
264 262 39 263 mp2an ⊢ ( sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) , ℝ* , < ) ≤ 0 ↔ ∀ 𝑥 ∈ ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) 𝑥 ≤ 0 )
265 257 264 sylibr ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → sup ( ( vol “ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) , ℝ* , < ) ≤ 0 )
266 128 265 eqbrtrd ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ( vol* ‘ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ◡ 𝐹 “ ( ( 1 / 𝑛 ) (,) +∞ ) ) ) ) ≤ 0 )
267 11 38 40 93 266 xrletrd ⊢ ( ( 𝜑 ∧ ¬ 0 < ( ∫2 ‘ 𝐹 ) ) → ( vol ‘ 𝐴 ) ≤ 0 )
268 267 ex ⊢ ( 𝜑 → ( ¬ 0 < ( ∫2 ‘ 𝐹 ) → ( vol ‘ 𝐴 ) ≤ 0 ) )
269 xrlenlt ⊢ ( ( ( vol ‘ 𝐴 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( vol ‘ 𝐴 ) ≤ 0 ↔ ¬ 0 < ( vol ‘ 𝐴 ) ) )
270 10 39 269 sylancl ⊢ ( 𝜑 → ( ( vol ‘ 𝐴 ) ≤ 0 ↔ ¬ 0 < ( vol ‘ 𝐴 ) ) )
271 268 270 sylibd ⊢ ( 𝜑 → ( ¬ 0 < ( ∫2 ‘ 𝐹 ) → ¬ 0 < ( vol ‘ 𝐴 ) ) )
272 2 271 mt4d ⊢ ( 𝜑 → 0 < ( ∫2 ‘ 𝐹 ) )