Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itg2addnclem2 Structured version   Visualization version   GIF version

Theorem itg2addnclem2 33793
Description: Lemma for itg2addnc 33795. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.)
Hypotheses
Ref Expression
itg2addnc.f1 (𝜑𝐹 ∈ MblFn)
itg2addnc.f2 (𝜑𝐹:ℝ⟶(0[,)+∞))
Assertion
Ref Expression
itg2addnclem2 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∈ dom ∫1)
Distinct variable groups:   𝑥,𝑣,,𝐹   𝜑,𝑣,𝑥,

Proof of Theorem itg2addnclem2
Dummy variables 𝑡 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itg2addnc.f2 . . . . . . . . . . 11 (𝜑𝐹:ℝ⟶(0[,)+∞))
2 rge0ssre 12520 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ
3 fss 6279 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
41, 2, 3sylancl 576 . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
54ad2antrr 708 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝐹:ℝ⟶ℝ)
65ffvelrnda 6591 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
7 rpre 12073 . . . . . . . . . 10 (𝑣 ∈ ℝ+𝑣 ∈ ℝ)
8 3re 11393 . . . . . . . . . . 11 3 ∈ ℝ
9 3ne0 11426 . . . . . . . . . . 11 3 ≠ 0
108, 9pm3.2i 458 . . . . . . . . . 10 (3 ∈ ℝ ∧ 3 ≠ 0)
11 redivcl 11039 . . . . . . . . . . 11 ((𝑣 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (𝑣 / 3) ∈ ℝ)
12113expb 1142 . . . . . . . . . 10 ((𝑣 ∈ ℝ ∧ (3 ∈ ℝ ∧ 3 ≠ 0)) → (𝑣 / 3) ∈ ℝ)
137, 10, 12sylancl 576 . . . . . . . . 9 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℝ)
1413ad2antlr 709 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
15 rpcnne0 12084 . . . . . . . . . 10 (𝑣 ∈ ℝ+ → (𝑣 ∈ ℂ ∧ 𝑣 ≠ 0))
16 3cn 11394 . . . . . . . . . . 11 3 ∈ ℂ
1716, 9pm3.2i 458 . . . . . . . . . 10 (3 ∈ ℂ ∧ 3 ≠ 0)
18 divne0 10992 . . . . . . . . . 10 (((𝑣 ∈ ℂ ∧ 𝑣 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (𝑣 / 3) ≠ 0)
1915, 17, 18sylancl 576 . . . . . . . . 9 (𝑣 ∈ ℝ+ → (𝑣 / 3) ≠ 0)
2019ad2antlr 709 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
216, 14, 20redivcld 11148 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
22 reflcl 12841 . . . . . . 7 (((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
2321, 22syl 17 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
24 peano2rem 10643 . . . . . 6 ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
2523, 24syl 17 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
2625, 14remulcld 10365 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ)
27 i1ff 23680 . . . . . 6 ( ∈ dom ∫1:ℝ⟶ℝ)
2827ad2antlr 709 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → :ℝ⟶ℝ)
2928ffvelrnda 6591 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ ℝ)
3026, 29ifcld 4335 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ ℝ)
3130fmpttd 6617 . 2 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))):ℝ⟶ℝ)
32 fzfi 13015 . . . . 5 (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ∈ Fin
33 ovex 6916 . . . . . . 7 ((𝑡 − 1) · (𝑣 / 3)) ∈ V
34 eqid 2817 . . . . . . 7 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) = (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3)))
3533, 34fnmpti 6243 . . . . . 6 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) Fn (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
36 dffn4 6347 . . . . . 6 ((𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) Fn (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↔ (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))):(0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))–onto→ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))))
3735, 36mpbi 221 . . . . 5 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))):(0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))–onto→ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3)))
38 fofi 8501 . . . . 5 (((0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ∈ Fin ∧ (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))):(0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))–onto→ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3)))) → ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∈ Fin)
3932, 37, 38mp2an 675 . . . 4 ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∈ Fin
40 i1frn 23681 . . . . 5 ( ∈ dom ∫1 → ran ∈ Fin)
4140ad2antlr 709 . . . 4 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran ∈ Fin)
42 unfi 8476 . . . 4 ((ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∈ Fin ∧ ran ∈ Fin) → (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ) ∈ Fin)
4339, 41, 42sylancr 577 . . 3 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ) ∈ Fin)
44 3nn 11392 . . . . . . . . . . . . . . . . 17 3 ∈ ℕ
45 nnrp 12076 . . . . . . . . . . . . . . . . 17 (3 ∈ ℕ → 3 ∈ ℝ+)
4644, 45ax-mp 5 . . . . . . . . . . . . . . . 16 3 ∈ ℝ+
47 rpdivcl 12090 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ℝ+ ∧ 3 ∈ ℝ+) → (𝑣 / 3) ∈ ℝ+)
4846, 47mpan2 674 . . . . . . . . . . . . . . 15 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℝ+)
4948ad2antlr 709 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
501ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
5150ffvelrnda 6591 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
52 elrege0 12518 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
5351, 52sylib 209 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
5453simprd 485 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹𝑥))
556, 49, 54divge0d 12146 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹𝑥) / (𝑣 / 3)))
56 flge0nn0 12865 . . . . . . . . . . . . 13 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ 0 ≤ ((𝐹𝑥) / (𝑣 / 3))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℕ0)
5721, 55, 56syl2anc 575 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℕ0)
5857nn0ge0d 11640 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ (⌊‘((𝐹𝑥) / (𝑣 / 3))))
5958adantr 468 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → 0 ≤ (⌊‘((𝐹𝑥) / (𝑣 / 3))))
6027frnd 6273 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ran ⊆ ℝ)
61 i1f0rn 23686 . . . . . . . . . . . . . . . . . 18 ( ∈ dom ∫1 → 0 ∈ ran )
62 elex2 3421 . . . . . . . . . . . . . . . . . 18 (0 ∈ ran → ∃𝑥 𝑥 ∈ ran )
6361, 62syl 17 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → ∃𝑥 𝑥 ∈ ran )
64 n0 4143 . . . . . . . . . . . . . . . . 17 (ran ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ran )
6563, 64sylibr 225 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ran ≠ ∅)
66 fimaxre2 11264 . . . . . . . . . . . . . . . . 17 ((ran ⊆ ℝ ∧ ran ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥)
6760, 40, 66syl2anc 575 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥)
6860, 65, 673jca 1151 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → (ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥))
6968ad3antlr 713 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥))
70 ffn 6266 . . . . . . . . . . . . . . . . . 18 (:ℝ⟶ℝ → Fn ℝ)
7127, 70syl 17 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 Fn ℝ)
72 dffn3 6277 . . . . . . . . . . . . . . . . 17 ( Fn ℝ ↔ :ℝ⟶ran )
7371, 72sylib 209 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1:ℝ⟶ran )
7473ad2antlr 709 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → :ℝ⟶ran )
7574ffvelrnda 6591 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ ran )
76 suprub 11279 . . . . . . . . . . . . . 14 (((ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥) ∧ (𝑥) ∈ ran ) → (𝑥) ≤ sup(ran , ℝ, < ))
7769, 75, 76syl2anc 575 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ≤ sup(ran , ℝ, < ))
78 suprcl 11278 . . . . . . . . . . . . . . . . 17 ((ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥) → sup(ran , ℝ, < ) ∈ ℝ)
7960, 65, 67, 78syl3anc 1483 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → sup(ran , ℝ, < ) ∈ ℝ)
8079ad3antlr 713 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → sup(ran , ℝ, < ) ∈ ℝ)
81 letr 10426 . . . . . . . . . . . . . . 15 (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ ∧ (𝑥) ∈ ℝ ∧ sup(ran , ℝ, < ) ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < )))
8226, 29, 80, 81syl3anc 1483 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < )))
8325, 80, 49lemuldivd 12155 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) ↔ ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (sup(ran , ℝ, < ) / (𝑣 / 3))))
84 1red 10336 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
8580, 14, 20redivcld 11148 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (sup(ran , ℝ, < ) / (𝑣 / 3)) ∈ ℝ)
8623, 84, 85lesubaddd 10919 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (sup(ran , ℝ, < ) / (𝑣 / 3)) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
8783, 86bitrd 270 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
88 peano2re 10504 . . . . . . . . . . . . . . . . . 18 ((sup(ran , ℝ, < ) / (𝑣 / 3)) ∈ ℝ → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ)
8985, 88syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ)
90 ceige 12888 . . . . . . . . . . . . . . . . 17 (((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
9189, 90syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
92 ceicl 12886 . . . . . . . . . . . . . . . . . . 19 (((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
9389, 92syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
9493zred 11768 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℝ)
95 letr 10426 . . . . . . . . . . . . . . . . 17 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ ∧ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ ∧ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∧ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
9623, 89, 94, 95syl3anc 1483 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∧ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
9791, 96mpan2d 677 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
9887, 97sylbid 231 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
9982, 98syld 47 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10077, 99mpan2d 677 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
101100adantrd 481 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
102101imp 395 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
10321flcld 12843 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
104103adantr 468 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
105 0zd 11675 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → 0 ∈ ℤ)
10693adantr 468 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
107 elfz 12575 . . . . . . . . . . 11 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ ∧ 0 ∈ ℤ ∧ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↔ (0 ≤ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∧ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))))
108104, 105, 106, 107syl3anc 1483 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↔ (0 ≤ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∧ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))))
10959, 102, 108mpbir2and 695 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
110 eqid 2817 . . . . . . . . 9 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))
111 oveq1 6891 . . . . . . . . . . 11 (𝑡 = (⌊‘((𝐹𝑥) / (𝑣 / 3))) → (𝑡 − 1) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1))
112111oveq1d 6899 . . . . . . . . . 10 (𝑡 = (⌊‘((𝐹𝑥) / (𝑣 / 3))) → ((𝑡 − 1) · (𝑣 / 3)) = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))
113112rspceeqv 3531 . . . . . . . . 9 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ∧ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) → ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3)))
114109, 110, 113sylancl 576 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3)))
115 ovex 6916 . . . . . . . . 9 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ V
11634elrnmpt 5587 . . . . . . . . 9 ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ V → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ↔ ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3))))
117115, 116ax-mp 5 . . . . . . . 8 ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ↔ ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3)))
118114, 117sylibr 225 . . . . . . 7 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))))
119 elun1 3990 . . . . . . 7 ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
120118, 119syl 17 . . . . . 6 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
121 elun2 3991 . . . . . . . 8 ((𝑥) ∈ ran → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
12275, 121syl 17 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
123122adantr 468 . . . . . 6 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
124120, 123ifclda 4324 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
125124fmpttd 6617 . . . 4 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))):ℝ⟶(ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
126125frnd 6273 . . 3 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ⊆ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
127 ssfi 8429 . . 3 (((ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ) ∈ Fin ∧ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ⊆ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran )) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∈ Fin)
12843, 126, 127syl2anc 575 . 2 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∈ Fin)
129 eqid 2817 . . . . 5 (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
130129mptpreima 5856 . . . 4 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}}
131 unrab 4110 . . . . 5 ({𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))} ∪ {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))}) = {𝑥 ∈ ℝ ∣ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥)))}
132 inrab 4111 . . . . . . . 8 ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) = {𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)}
133132ineq1i 4020 . . . . . . 7 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = ({𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))})
134 inrab 4111 . . . . . . 7 ({𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = {𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))}
135133, 134eqtri 2839 . . . . . 6 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = {𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))}
136 unrab 4110 . . . . . . . 8 ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) = {𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)}
137136ineq1i 4020 . . . . . . 7 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = ({𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
138 inrab 4111 . . . . . . 7 ({𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))}
139137, 138eqtri 2839 . . . . . 6 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))}
140135, 139uneq12i 3975 . . . . 5 ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})) = ({𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))} ∪ {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))})
141 eqcom 2824 . . . . . . 7 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 𝑡𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
142 fvex 6431 . . . . . . . . 9 (𝑥) ∈ V
143115, 142ifex 4338 . . . . . . . 8 if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ V
144143elsn 4396 . . . . . . 7 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 𝑡)
145 ianor 995 . . . . . . . . . . 11 (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ↔ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ ¬ (𝑥) ≠ 0))
146 nne 2993 . . . . . . . . . . . 12 (¬ (𝑥) ≠ 0 ↔ (𝑥) = 0)
147146orbi2i 927 . . . . . . . . . . 11 ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ ¬ (𝑥) ≠ 0) ↔ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0))
148145, 147bitr2i 267 . . . . . . . . . 10 ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ↔ ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0))
149148anbi1i 612 . . . . . . . . 9 (((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥)) ↔ (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (𝑥)))
150149orbi2i 927 . . . . . . . 8 (((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))) ↔ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (𝑥))))
151 eqif 4330 . . . . . . . 8 (𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ↔ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (𝑥))))
152150, 151bitr4i 269 . . . . . . 7 (((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))) ↔ 𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
153141, 144, 1523bitr4i 294 . . . . . 6 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))))
154153rabbii 3386 . . . . 5 {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} = {𝑥 ∈ ℝ ∣ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥)))}
155131, 140, 1543eqtr4ri 2850 . . . 4 {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} = ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}))
156130, 155eqtri 2839 . . 3 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}))
157 eldifi 3942 . . . . . 6 (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → 𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))))
15831frnd 6273 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ⊆ ℝ)
159158sseld 3808 . . . . . 6 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) → 𝑡 ∈ ℝ))
160157, 159syl5 34 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → 𝑡 ∈ ℝ))
161160imdistani 560 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ))
162 rabiun 33714 . . . . . . . . . 10 {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)}
163 cnvimarndm 5710 . . . . . . . . . . . . . 14 ( “ ran ) = dom
164 iunid 4778 . . . . . . . . . . . . . . . 16 𝑡 ∈ ran {𝑡} = ran
165164imaeq2i 5688 . . . . . . . . . . . . . . 15 ( 𝑡 ∈ ran {𝑡}) = ( “ ran )
166 imaiun 6737 . . . . . . . . . . . . . . 15 ( 𝑡 ∈ ran {𝑡}) = 𝑡 ∈ ran ( “ {𝑡})
167165, 166eqtr3i 2841 . . . . . . . . . . . . . 14 ( “ ran ) = 𝑡 ∈ ran ( “ {𝑡})
168163, 167eqtr3i 2841 . . . . . . . . . . . . 13 dom = 𝑡 ∈ ran ( “ {𝑡})
16927fdmd 6275 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → dom = ℝ)
170168, 169syl5eqr 2865 . . . . . . . . . . . 12 ( ∈ dom ∫1 𝑡 ∈ ran ( “ {𝑡}) = ℝ)
171170ad2antlr 709 . . . . . . . . . . 11 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran ( “ {𝑡}) = ℝ)
172 rabeq 3393 . . . . . . . . . . 11 ( 𝑡 ∈ ran ( “ {𝑡}) = ℝ → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
173171, 172syl 17 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
174162, 173syl5eqr 2865 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
175 fniniseg 6570 . . . . . . . . . . . . . . . . . 18 ( Fn ℝ → (𝑥 ∈ ( “ {𝑡}) ↔ (𝑥 ∈ ℝ ∧ (𝑥) = 𝑡)))
17627, 70, 1753syl 18 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → (𝑥 ∈ ( “ {𝑡}) ↔ (𝑥 ∈ ℝ ∧ (𝑥) = 𝑡)))
177176simplbda 489 . . . . . . . . . . . . . . . 16 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → (𝑥) = 𝑡)
178177breq2d 4867 . . . . . . . . . . . . . . 15 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ↔ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
179178rabbidva 3389 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
180 inrab2 4112 . . . . . . . . . . . . . . 15 ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡}
181 imassrn 5701 . . . . . . . . . . . . . . . . . 18 ( “ {𝑡}) ⊆ ran
182 dfdm4 5531 . . . . . . . . . . . . . . . . . . 19 dom = ran
183182, 169syl5eqr 2865 . . . . . . . . . . . . . . . . . 18 ( ∈ dom ∫1 → ran = ℝ)
184181, 183syl5sseq 3861 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → ( “ {𝑡}) ⊆ ℝ)
185 sseqin2 4027 . . . . . . . . . . . . . . . . 17 (( “ {𝑡}) ⊆ ℝ ↔ (ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}))
186184, 185sylib 209 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → (ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}))
187 rabeq 3393 . . . . . . . . . . . . . . . 16 ((ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}) → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
188186, 187syl 17 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
189180, 188syl5eq 2863 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
190179, 189eqtr4d 2854 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
191190ad3antlr 713 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
19225adantlr 697 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
19360ad2antlr 709 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran ⊆ ℝ)
194193sselda 3809 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → 𝑡 ∈ ℝ)
195194adantr 468 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℝ)
19648ad3antlr 713 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
197192, 195, 196lemuldivd 12155 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡 ↔ ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (𝑡 / (𝑣 / 3))))
19823adantlr 697 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
199 1red 10336 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
20013ad3antlr 713 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
20119ad3antlr 713 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
202195, 200, 201redivcld 11148 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
203198, 199, 202lesubaddd 10919 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (𝑡 / (𝑣 / 3)) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1)))
2046adantlr 697 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
205 peano2re 10504 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 / (𝑣 / 3)) ∈ ℝ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
206202, 205syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
207 reflcl 12841 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ → (⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ)
209 peano2re 10504 . . . . . . . . . . . . . . . . . . . 20 ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ → ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ∈ ℝ)
210208, 209syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ∈ ℝ)
211204, 210, 196ltdivmuld 12157 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ↔ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))))
21221adantlr 697 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
213 flflp1 12852 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ ((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))
214212, 206, 213syl2anc 575 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ ((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))
215200, 210remulcld 10365 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ)
216215rexrd 10384 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ*)
217 elioomnf 12507 . . . . . . . . . . . . . . . . . . . 20 (((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
218216, 217syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
219204biantrurd 524 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
220218, 219bitr4d 273 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))))
221211, 214, 2203bitr4d 302 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
222197, 203, 2213bitrd 296 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡 ↔ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
223222rabbidva 3389 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
2241feqmptd 6480 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
225224cnveqd 5513 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
226225imaeq1d 5689 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
227 eqid 2817 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ ↦ (𝐹𝑥)) = (𝑥 ∈ ℝ ↦ (𝐹𝑥))
228227mptpreima 5856 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))}
229226, 228syl6eq 2867 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
230229ad3antrrr 712 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
231223, 230eqtr4d 2854 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
232 itg2addnc.f1 . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ MblFn)
233 mbfima 23634 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
234232, 4, 233syl2anc 575 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
235234ad3antrrr 712 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
236231, 235eqeltrd 2896 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
23760sseld 3808 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → (𝑡 ∈ ran 𝑡 ∈ ℝ))
238237ad2antlr 709 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ ran 𝑡 ∈ ℝ))
239238imdistani 560 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ))
240 i1fmbf 23679 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 ∈ MblFn)
241240, 27jca 503 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ( ∈ MblFn ∧ :ℝ⟶ℝ))
242241ad2antlr 709 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ( ∈ MblFn ∧ :ℝ⟶ℝ))
243 mbfimasn 23636 . . . . . . . . . . . . . . . 16 (( ∈ MblFn ∧ :ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
2442433expa 1140 . . . . . . . . . . . . . . 15 ((( ∈ MblFn ∧ :ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
245242, 244sylan 571 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
246239, 245syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ( “ {𝑡}) ∈ dom vol)
247 inmbl 23546 . . . . . . . . . . . . 13 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol ∧ ( “ {𝑡}) ∈ dom vol) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
248236, 246, 247syl2anc 575 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
249191, 248eqeltrd 2896 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
250249ralrimiva 3165 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
251 finiunmbl 23548 . . . . . . . . . 10 ((ran ∈ Fin ∧ ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
25241, 250, 251syl2anc 575 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
253174, 252eqeltrrd 2897 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
254 unrab 4110 . . . . . . . . . . 11 ({𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}) = {𝑥 ∈ ℝ ∣ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))}
25527feqmptd 6480 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 = (𝑥 ∈ ℝ ↦ (𝑥)))
256255cnveqd 5513 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 = (𝑥 ∈ ℝ ↦ (𝑥)))
257256imaeq1d 5689 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → ( “ (-∞(,)0)) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ (-∞(,)0)))
258 eqid 2817 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ (𝑥)) = (𝑥 ∈ ℝ ↦ (𝑥))
259258mptpreima 5856 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ↦ (𝑥)) “ (-∞(,)0)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)}
260257, 259syl6eq 2867 . . . . . . . . . . . 12 ( ∈ dom ∫1 → ( “ (-∞(,)0)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)})
261256imaeq1d 5689 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → ( “ (0(,)+∞)) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ (0(,)+∞)))
262258mptpreima 5856 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ↦ (𝑥)) “ (0(,)+∞)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}
263261, 262syl6eq 2867 . . . . . . . . . . . 12 ( ∈ dom ∫1 → ( “ (0(,)+∞)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)})
264260, 263uneq12d 3978 . . . . . . . . . . 11 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) = ({𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}))
26527ffvelrnda 6591 . . . . . . . . . . . . 13 (( ∈ dom ∫1𝑥 ∈ ℝ) → (𝑥) ∈ ℝ)
266 0re 10337 . . . . . . . . . . . . . . 15 0 ∈ ℝ
267 lttri2 10415 . . . . . . . . . . . . . . 15 (((𝑥) ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥) ≠ 0 ↔ ((𝑥) < 0 ∨ 0 < (𝑥))))
268266, 267mpan2 674 . . . . . . . . . . . . . 14 ((𝑥) ∈ ℝ → ((𝑥) ≠ 0 ↔ ((𝑥) < 0 ∨ 0 < (𝑥))))
269 ibar 520 . . . . . . . . . . . . . . 15 ((𝑥) ∈ ℝ → (((𝑥) < 0 ∨ 0 < (𝑥)) ↔ ((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥)))))
270 andi 1021 . . . . . . . . . . . . . . . 16 (((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥))) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
271 0xr 10381 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
272 elioomnf 12507 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ* → ((𝑥) ∈ (-∞(,)0) ↔ ((𝑥) ∈ ℝ ∧ (𝑥) < 0)))
273 elioopnf 12506 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ* → ((𝑥) ∈ (0(,)+∞) ↔ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
274272, 273orbi12d 933 . . . . . . . . . . . . . . . . 17 (0 ∈ ℝ* → (((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥)))))
275271, 274ax-mp 5 . . . . . . . . . . . . . . . 16 (((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
276270, 275bitr4i 269 . . . . . . . . . . . . . . 15 (((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥))) ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)))
277269, 276syl6bb 278 . . . . . . . . . . . . . 14 ((𝑥) ∈ ℝ → (((𝑥) < 0 ∨ 0 < (𝑥)) ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
278268, 277bitrd 270 . . . . . . . . . . . . 13 ((𝑥) ∈ ℝ → ((𝑥) ≠ 0 ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
279265, 278syl 17 . . . . . . . . . . . 12 (( ∈ dom ∫1𝑥 ∈ ℝ) → ((𝑥) ≠ 0 ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
280279rabbidva 3389 . . . . . . . . . . 11 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} = {𝑥 ∈ ℝ ∣ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))})
281254, 264, 2803eqtr4a 2877 . . . . . . . . . 10 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) = {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0})
282 i1fima 23682 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ (-∞(,)0)) ∈ dom vol)
283 i1fima 23682 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ (0(,)+∞)) ∈ dom vol)
284 unmbl 23541 . . . . . . . . . . 11 ((( “ (-∞(,)0)) ∈ dom vol ∧ ( “ (0(,)+∞)) ∈ dom vol) → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) ∈ dom vol)
285282, 283, 284syl2anc 575 . . . . . . . . . 10 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) ∈ dom vol)
286281, 285eqeltrrd 2897 . . . . . . . . 9 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol)
287286ad2antlr 709 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol)
288 inmbl 23546 . . . . . . . 8 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
289253, 287, 288syl2anc 575 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
290289adantr 468 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
29123recnd 10363 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℂ)
292291adantlr 697 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℂ)
293 1cnd 10330 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
294 simplr 776 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℝ)
29513ad3antlr 713 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
29619ad3antlr 713 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
297294, 295, 296redivcld 11148 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
298297recnd 10363 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℂ)
299292, 293, 298subadd2d 10706 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
300 eqcom 2824 . . . . . . . . . 10 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ (𝑡 / (𝑣 / 3)) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1))
301 recn 10321 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
302301ad2antlr 709 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℂ)
30325recnd 10363 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℂ)
304303adantlr 697 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℂ)
30513recnd 10363 . . . . . . . . . . . 12 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℂ)
306305ad3antlr 713 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℂ)
307302, 304, 306, 296divmul3d 11130 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
308300, 307syl5bb 274 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
309299, 308bitr3d 272 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
310309rabbidva 3389 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))})
311 imaundi 5770 . . . . . . . . . . 11 (𝐹 “ ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
312225ad4antr 715 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
313 zre 11667 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
314313adantl 469 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
31513ad3antlr 713 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ)
316314, 315remulcld 10365 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ)
317316rexrd 10384 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ*)
318 peano2z 11704 . . . . . . . . . . . . . . . . 17 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℤ)
319318zred 11768 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
320319adantl 469 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
321315, 320remulcld 10365 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
322321rexrd 10384 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ*)
323 zcn 11668 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℂ)
324323adantl 469 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℂ)
325305ad3antlr 713 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℂ)
326324, 325mulcomd 10356 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) = ((𝑣 / 3) · ((𝑡 / (𝑣 / 3)) + 1)))
32748ad3antlr 713 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ+)
328313ltp1d 11249 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) < (((𝑡 / (𝑣 / 3)) + 1) + 1))
329328adantl 469 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) < (((𝑡 / (𝑣 / 3)) + 1) + 1))
330314, 320, 327, 329ltmul2dd 12162 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · ((𝑡 / (𝑣 / 3)) + 1)) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))
331326, 330eqbrtrd 4877 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))
332 snunioo 12541 . . . . . . . . . . . . 13 (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ* ∧ ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ* ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) → ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))
333317, 322, 331, 332syl3anc 1483 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))
334312, 333imaeq12d 5691 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
335311, 334syl5eqr 2865 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
336227mptpreima 5856 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))}
3374ad3antrrr 712 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → 𝐹:ℝ⟶ℝ)
338337ffvelrnda 6591 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
3393383biant1d 1595 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
340339adantr 468 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
341313adantl 469 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
342338adantr 468 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹𝑥) ∈ ℝ)
34348ad4antlr 717 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ+)
344341, 342, 343lemuldivd 12155 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ ((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3))))
345319adantl 469 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
346342, 345, 343ltdivmuld 12157 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1) ↔ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))
347346bicomd 214 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ↔ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1)))
348344, 347anbi12d 618 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
349340, 348bitr3d 272 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
350 elico2 12475 . . . . . . . . . . . . . . . 16 (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ ∧ ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ*) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
351316, 322, 350syl2anc 575 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
352351adantlr 697 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
353 eqcom 2824 . . . . . . . . . . . . . . 15 (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1))
35421adantlr 697 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
355 flbi 12861 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
356354, 355sylan 571 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
357353, 356syl5bb 274 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
358349, 352, 3573bitr4d 302 . . . . . . . . . . . . 13 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
359358an32s 634 . . . . . . . . . . . 12 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
360359rabbidva 3389 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))} = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
361336, 360syl5eq 2863 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
362335, 361eqtrd 2851 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
363232ad4antr 715 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹 ∈ MblFn)
3644ad4antr 715 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹:ℝ⟶ℝ)
365 mbfimasn 23636 . . . . . . . . . . 11 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ) → (𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∈ dom vol)
366363, 364, 316, 365syl3anc 1483 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∈ dom vol)
367 mbfima 23634 . . . . . . . . . . . 12 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
368232, 4, 367syl2anc 575 . . . . . . . . . . 11 (𝜑 → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
369368ad4antr 715 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
370 unmbl 23541 . . . . . . . . . 10 (((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∈ dom vol ∧ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) ∈ dom vol)
371366, 369, 370syl2anc 575 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) ∈ dom vol)
372362, 371eqeltrrd 2897 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
373 simpr 473 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
374354flcld 12843 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
375374adantr 468 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
376373, 375eqeltrd 2896 . . . . . . . . . . . . 13 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ)
377376stoic1a 1852 . . . . . . . . . . . 12 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
378377an32s 634 . . . . . . . . . . 11 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) ∧ 𝑥 ∈ ℝ) → ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
379378ralrimiva 3165 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ∀𝑥 ∈ ℝ ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
380 rabeq0 4168 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
381379, 380sylibr 225 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = ∅)
382 0mbl 23543 . . . . . . . . 9 ∅ ∈ dom vol
383381, 382syl6eqel 2904 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
384372, 383pm2.61dan 838 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
385310, 384eqeltrrd 2897 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))} ∈ dom vol)
386 inmbl 23546 . . . . . 6 ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))} ∈ dom vol) → (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∈ dom vol)
387290, 385, 386syl2anc 575 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∈ dom vol)
388 rabiun 33714 . . . . . . . . . . 11 {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)}
389 rabeq 3393 . . . . . . . . . . . 12 ( 𝑡 ∈ ran ( “ {𝑡}) = ℝ → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
390170, 389syl 17 . . . . . . . . . . 11 ( ∈ dom ∫1 → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
391388, 390syl5eqr 2865 . . . . . . . . . 10 ( ∈ dom ∫1 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
392391ad2antlr 709 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
393178notbid 309 . . . . . . . . . . . . . . 15 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
394393rabbidva 3389 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
395 inrab2 4112 . . . . . . . . . . . . . . 15 ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡}
396 rabeq 3393 . . . . . . . . . . . . . . . 16 ((ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}) → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
397186, 396syl 17 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
398395, 397syl5eq 2863 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
399394, 398eqtr4d 2854 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
400399ad3antlr 713 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
401 imaundi 5770 . . . . . . . . . . . . . . . . 17 (𝐹 “ ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)))
40213, 19jca 503 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 ∈ ℝ+ → ((𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0))
403 redivcl 11039 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑡 ∈ ℝ ∧ (𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
4044033expb 1142 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ ℝ ∧ ((𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0)) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
405402, 404sylan2 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℝ ∧ 𝑣 ∈ ℝ+) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
406405ancoms 448 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
407406adantll 696 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
408407, 205syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
409 peano2re 10504 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
410 reflcl 12841 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
411408, 409, 4103syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
41213ad2antlr 709 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
413411, 412remulcld 10365 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ)
414413rexrd 10384 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ*)
415 pnfxr 10387 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
416415a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → +∞ ∈ ℝ*)
417 ltpnf 12190 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) < +∞)
418413, 417syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) < +∞)
419 snunioo 12541 . . . . . . . . . . . . . . . . . . 19 ((((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) < +∞) → ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) = (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞))
420414, 416, 418, 419syl3anc 1483 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) = (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞))
421420imaeq2d 5690 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
422401, 421syl5eqr 2865 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
423225imaeq1d 5689 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
424227mptpreima 5856 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)}
425423, 424syl6eq 2867 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)})
426425ad3antrrr 712 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)})
427408, 409syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
428427adantr 468 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
429 flflp1 12852 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ ∧ ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3)) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
430428, 354, 429syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3)) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
431413adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ)
432 elicopnf 12508 . . . . . . . . . . . . . . . . . . . . . 22 (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
433431, 432syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
434338biantrurd 524 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
435411adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
43648ad3antlr 713 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
437435, 338, 436lemuldivd 12155 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3))))
438433, 434, 4373bitr2d 298 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3))))
439408adantr 468 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
440354, 22syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
441 1red 10336 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
442439, 440, 441ltadd1d 10915 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
443430, 438, 4423bitr4d 302 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
444297, 441, 440ltaddsubd 10922 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1)))
445443, 444bitrd 270 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ (𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1)))
446440, 24syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
447294, 446, 436ltdivmul2d 12158 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ↔ 𝑡 < (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
448446, 295remulcld 10365 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ)
449294, 448ltnled 10479 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 < (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
450445, 447, 4493bitrd 296 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
451450rabbidva 3389 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
452422, 426, 4513eqtrd 2855 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
453232ad3antrrr 712 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → 𝐹 ∈ MblFn)
454 mbfimasn 23636 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ) → (𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∈ dom vol)
455453, 337, 413, 454syl3anc 1483 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∈ dom vol)
456 mbfima 23634 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
457232, 4, 456syl2anc 575 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
458457ad3antrrr 712 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
459 unmbl 23541 . . . . . . . . . . . . . . . 16 (((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∈ dom vol ∧ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) ∈ dom vol)
460455, 458, 459syl2anc 575 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) ∈ dom vol)
461452, 460eqeltrrd 2897 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
462239, 461syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
463 inmbl 23546 . . . . . . . . . . . . 13 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol ∧ ( “ {𝑡}) ∈ dom vol) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
464462, 246, 463syl2anc 575 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
465400, 464eqeltrd 2896 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
466465ralrimiva 3165 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
467 finiunmbl 23548 . . . . . . . . . 10 ((ran ∈ Fin ∧ ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
46841, 466, 467syl2anc 575 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
469392, 468eqeltrrd 2897 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
470256imaeq1d 5689 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ {0}) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}))
471258mptpreima 5856 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}
472142elsn 4396 . . . . . . . . . . . . 13 ((𝑥) ∈ {0} ↔ (𝑥) = 0)
473472rabbii 3386 . . . . . . . . . . . 12 {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}} = {𝑥 ∈ ℝ ∣ (𝑥) = 0}
474471, 473eqtri 2839 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) = 0}
475470, 474syl6eq 2867 . . . . . . . . . 10 ( ∈ dom ∫1 → ( “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) = 0})
476 i1fima 23682 . . . . . . . . . 10 ( ∈ dom ∫1 → ( “ {0}) ∈ dom vol)
477475, 476eqeltrrd 2897 . . . . . . . . 9 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol)
478477ad2antlr 709 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol)
479 unmbl 23541 . . . . . . . 8 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
480469, 478, 479syl2anc 575 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
481480adantr 468 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
482256imaeq1d 5689 . . . . . . . . 9 ( ∈ dom ∫1 → ( “ {𝑡}) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}))
483258mptpreima 5856 . . . . . . . . . 10 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {𝑡}}
484142elsn 4396 . . . . . . . . . . . 12 ((𝑥) ∈ {𝑡} ↔ (𝑥) = 𝑡)
485 eqcom 2824 . . . . . . . . . . . 12 ((𝑥) = 𝑡𝑡 = (𝑥))
486484, 485bitri 266 . . . . . . . . . . 11 ((𝑥) ∈ {𝑡} ↔ 𝑡 = (𝑥))
487486rabbii 3386 . . . . . . . . . 10 {𝑥 ∈ ℝ ∣ (𝑥) ∈ {𝑡}} = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}
488483, 487eqtri 2839 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}
489482, 488syl6eq 2867 . . . . . . . 8 ( ∈ dom ∫1 → ( “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
490489ad3antlr 713 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
491490, 245eqeltrrd 2897 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)} ∈ dom vol)
492 inmbl 23546 . . . . . 6 ((({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)} ∈ dom vol) → (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) ∈ dom vol)
493481, 491, 492syl2anc 575 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) ∈ dom vol)
494 unmbl 23541 . . . . 5 (((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∈ dom vol ∧ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) ∈ dom vol) → ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})) ∈ dom vol)
495387, 493, 494syl2anc 575 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})) ∈ dom vol)
496161, 495syl 17 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})) ∈ dom vol)
497156, 496syl5eqel 2900 . 2 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∈ dom vol)
498 mblvol 23534 . . . 4 (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∈ dom vol → (vol‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) = (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})))
499497, 498syl 17 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (vol‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) = (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})))
500 eldifsn 4519 . . . . . 6 (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) ↔ (𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∧ 𝑡 ≠ 0))
501159anim1d 600 . . . . . 6 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ((𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∧ 𝑡 ≠ 0) → (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
502500, 501syl5bi 233 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
503502imdistani 560 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
504130a1i 11 . . . . . . . . . . 11 ( ∈ dom ∫1 → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}})
505470, 471syl6eq 2867 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}})
506504, 505ineq12d 4025 . . . . . . . . . 10 ( ∈ dom ∫1 → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ({𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}))
507 inrab 4111 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})}
508506, 507syl6eq 2867 . . . . . . . . 9 ( ∈ dom ∫1 → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})})
509508ad3antlr 713 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})})
510146biimpri 219 . . . . . . . . . . . . . . . . . 18 ((𝑥) = 0 → ¬ (𝑥) ≠ 0)
511510intnand 478 . . . . . . . . . . . . . . . . 17 ((𝑥) = 0 → ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0))
512511iffalsed 4301 . . . . . . . . . . . . . . . 16 ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = (𝑥))
513 eqtr 2836 . . . . . . . . . . . . . . . 16 ((if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = (𝑥) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
514512, 513mpancom 671 . . . . . . . . . . . . . . 15 ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
515514adantl 469 . . . . . . . . . . . . . 14 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
516 simpll 774 . . . . . . . . . . . . . . 15 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → 𝑡 ≠ 0)
517516necomd 3044 . . . . . . . . . . . . . 14 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → 0 ≠ 𝑡)
518515, 517eqnetrd 3056 . . . . . . . . . . . . 13 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡)
519518ex 399 . . . . . . . . . . . 12 ((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) → ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
520 orcom 888 . . . . . . . . . . . . . 14 ((¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∨ ¬ (𝑥) ∈ {0}) ↔ (¬ (𝑥) ∈ {0} ∨ ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
521 ianor 995 . . . . . . . . . . . . . 14 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ (¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∨ ¬ (𝑥) ∈ {0}))
522 imor 871 . . . . . . . . . . . . . 14 (((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}) ↔ (¬ (𝑥) ∈ {0} ∨ ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
523520, 521, 5223bitr4i 294 . . . . . . . . . . . . 13 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ ((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
524144necon3bbii 3036 . . . . . . . . . . . . . 14 (¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡)
525472, 524imbi12i 341 . . . . . . . . . . . . 13 (((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}) ↔ ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
526523, 525bitri 266 . . . . . . . . . . . 12 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
527519, 526sylibr 225 . . . . . . . . . . 11 ((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) → ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
528527ralrimiva 3165 . . . . . . . . . 10 (𝑡 ≠ 0 → ∀𝑥 ∈ ℝ ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
529 rabeq0 4168 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
530528, 529sylibr 225 . . . . . . . . 9 (𝑡 ≠ 0 → {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅)
531530ad2antll 711 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅)
532509, 531eqtrd 2851 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ∅)
533 imassrn 5701 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
534 dfdm4 5531 . . . . . . . . . 10 dom (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
535143, 129dmmpti 6244 . . . . . . . . . 10 dom (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ℝ
536534, 535eqtr3i 2841 . . . . . . . . 9 ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ℝ
537533, 536sseqtri 3845 . . . . . . . 8 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ℝ
538 reldisj 4228 . . . . . . . 8 (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ℝ → ((((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ∅ ↔ ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ (ℝ ∖ ( “ {0}))))
539537, 538ax-mp 5 . . . . . . 7 ((((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ∅ ↔ ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ (ℝ ∖ ( “ {0})))
540532, 539sylib 209 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ (ℝ ∖ ( “ {0})))
541 ffun 6269 . . . . . . . . . 10 (:ℝ⟶ℝ → Fun )
542 difpreima 6575 . . . . . . . . . 10 (Fun → ( “ (ran ∖ {0})) = (( “ ran ) ∖ ( “ {0})))
543541, 542syl 17 . . . . . . . . 9 (:ℝ⟶ℝ → ( “ (ran ∖ {0})) = (( “ ran ) ∖ ( “ {0})))
544 fdm 6274 . . . . . . . . . . 11 (:ℝ⟶ℝ → dom = ℝ)
545163, 544syl5eq 2863 . . . . . . . . . 10 (:ℝ⟶ℝ → ( “ ran ) = ℝ)
546545difeq1d 3937 . . . . . . . . 9 (:ℝ⟶ℝ → (( “ ran ) ∖ ( “ {0})) = (ℝ ∖ ( “ {0})))
547543, 546eqtrd 2851 . . . . . . . 8 (:ℝ⟶ℝ → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
54827, 547syl 17 . . . . . . 7 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
549548ad3antlr 713 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
550540, 549sseqtr4d 3850 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ( “ (ran ∖ {0})))
551 imassrn 5701 . . . . . . 7 ( “ (ran ∖ {0})) ⊆ ran
552551, 183syl5sseq 3861 . . . . . 6 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) ⊆ ℝ)
553552ad3antlr 713 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ( “ (ran ∖ {0})) ⊆ ℝ)
554 i1fima 23682 . . . . . . . 8 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) ∈ dom vol)
555 mblvol 23534 . . . . . . . 8 (( “ (ran ∖ {0})) ∈ dom vol → (vol‘( “ (ran ∖ {0}))) = (vol*‘( “ (ran ∖ {0}))))
556554, 555syl 17 . . . . . . 7 ( ∈ dom ∫1 → (vol‘( “ (ran ∖ {0}))) = (vol*‘( “ (ran ∖ {0}))))
557 neldifsn 4524 . . . . . . . 8 ¬ 0 ∈ (ran ∖ {0})
558 i1fima2 23683 . . . . . . . 8 (( ∈ dom ∫1 ∧ ¬ 0 ∈ (ran ∖ {0})) → (vol‘( “ (ran ∖ {0}))) ∈ ℝ)
559557, 558mpan2 674 . . . . . . 7 ( ∈ dom ∫1 → (vol‘( “ (ran ∖ {0}))) ∈ ℝ)
560556, 559eqeltrrd 2897 . . . . . 6 ( ∈ dom ∫1 → (vol*‘( “ (ran ∖ {0}))) ∈ ℝ)
561560ad3antlr 713 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (vol*‘( “ (ran ∖ {0}))) ∈ ℝ)
562 ovolsscl 23490 . . . . 5 ((((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ( “ (ran ∖ {0})) ∧ ( “ (ran ∖ {0})) ⊆ ℝ ∧ (vol*‘( “ (ran ∖ {0}))) ∈ ℝ) → (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
563550, 553, 561, 562syl3anc 1483 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
564503, 563syl 17 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
565499, 564eqeltrd 2896 . 2 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (vol‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
56631, 128, 497, 565i1fd 23685 1 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∈ dom ∫1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wex 1859  wcel 2157  wne 2989  wral 3107  wrex 3108  {crab 3111  Vcvv 3402  cdif 3777  cun 3778  cin 3779  wss 3780  c0 4127  ifcif 4290  {csn 4381   ciun 4723   class class class wbr 4855  cmpt 4934  ccnv 5323  dom cdm 5324  ran crn 5325  cima 5327  Fun wfun 6105   Fn wfn 6106  wf 6107  ontowfo 6109  cfv 6111  (class class class)co 6884  Fincfn 8202  supcsup 8595  cc 10229  cr 10230  0cc0 10231  1c1 10232   + caddc 10234   · cmul 10236  +∞cpnf 10366  -∞cmnf 10367  *cxr 10368   < clt 10369  cle 10370  cmin 10561  -cneg 10562   / cdiv 10979  cn 11315  3c3 11369  0cn0 11579  cz 11663  +crp 12066  (,)cioo 12413  [,)cico 12415  ...cfz 12569  cfl 12835  vol*covol 23466  volcvol 23467  MblFncmbf 23618  1citg1 23619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-inf2 8795  ax-cnex 10287  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307  ax-pre-mulgt0 10308  ax-pre-sup 10309
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-of 7137  df-om 7306  df-1st 7408  df-2nd 7409  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-1o 7806  df-2o 7807  df-oadd 7810  df-er 7989  df-map 8104  df-pm 8105  df-en 8203  df-dom 8204  df-sdom 8205  df-fin 8206  df-fi 8566  df-sup 8597  df-inf 8598  df-oi 8664  df-card 9058  df-cda 9285  df-pnf 10371  df-mnf 10372  df-xr 10373  df-ltxr 10374  df-le 10375  df-sub 10563  df-neg 10564  df-div 10980  df-nn 11316  df-2 11376  df-3 11377  df-n0 11580  df-z 11664  df-uz 11925  df-q 12028  df-rp 12067  df-xneg 12182  df-xadd 12183  df-xmul 12184  df-ioo 12417  df-ico 12419  df-icc 12420  df-fz 12570  df-fzo 12710  df-fl 12837  df-seq 13045  df-exp 13104  df-hash 13358  df-cj 14082  df-re 14083  df-im 14084  df-sqrt 14218  df-abs 14219  df-clim 14462  df-sum 14660  df-rest 16308  df-topgen 16329  df-psmet 19966  df-xmet 19967  df-met 19968  df-bl 19969  df-mopn 19970  df-top 20933  df-topon 20950  df-bases 20985  df-cmp 21425  df-ovol 23468  df-vol 23469  df-mbf 23623  df-itg1 23624
This theorem is referenced by:  itg2addnclem3  33794
  Copyright terms: Public domain W3C validator