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 37993
Description: Lemma for itg2addnc 37995. 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 13409 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ
3 fss 6684 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
41, 2, 3sylancl 587 . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
54ad2antrr 727 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝐹:ℝ⟶ℝ)
65ffvelcdmda 7036 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
7 rpre 12951 . . . . . . . . . 10 (𝑣 ∈ ℝ+𝑣 ∈ ℝ)
8 3re 12261 . . . . . . . . . . 11 3 ∈ ℝ
9 3ne0 12287 . . . . . . . . . . 11 3 ≠ 0
108, 9pm3.2i 470 . . . . . . . . . 10 (3 ∈ ℝ ∧ 3 ≠ 0)
11 redivcl 11874 . . . . . . . . . . 11 ((𝑣 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (𝑣 / 3) ∈ ℝ)
12113expb 1121 . . . . . . . . . 10 ((𝑣 ∈ ℝ ∧ (3 ∈ ℝ ∧ 3 ≠ 0)) → (𝑣 / 3) ∈ ℝ)
137, 10, 12sylancl 587 . . . . . . . . 9 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℝ)
1413ad2antlr 728 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
15 rpcnne0 12961 . . . . . . . . . 10 (𝑣 ∈ ℝ+ → (𝑣 ∈ ℂ ∧ 𝑣 ≠ 0))
16 3cn 12262 . . . . . . . . . . 11 3 ∈ ℂ
1716, 9pm3.2i 470 . . . . . . . . . 10 (3 ∈ ℂ ∧ 3 ≠ 0)
18 divne0 11821 . . . . . . . . . 10 (((𝑣 ∈ ℂ ∧ 𝑣 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (𝑣 / 3) ≠ 0)
1915, 17, 18sylancl 587 . . . . . . . . 9 (𝑣 ∈ ℝ+ → (𝑣 / 3) ≠ 0)
2019ad2antlr 728 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
216, 14, 20redivcld 11983 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
22 reflcl 13755 . . . . . . 7 (((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
2321, 22syl 17 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
24 peano2rem 11461 . . . . . 6 ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
2523, 24syl 17 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
2625, 14remulcld 11175 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ)
27 i1ff 25643 . . . . . 6 ( ∈ dom ∫1:ℝ⟶ℝ)
2827ad2antlr 728 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → :ℝ⟶ℝ)
2928ffvelcdmda 7036 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ ℝ)
3026, 29ifcld 4513 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ ℝ)
3130fmpttd 7067 . 2 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))):ℝ⟶ℝ)
32 fzfi 13934 . . . . 5 (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ∈ Fin
33 ovex 7400 . . . . . . 7 ((𝑡 − 1) · (𝑣 / 3)) ∈ V
34 eqid 2736 . . . . . . 7 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) = (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3)))
3533, 34fnmpti 6641 . . . . . 6 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) Fn (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
36 dffn4 6758 . . . . . 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 230 . . . . 5 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))):(0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))–onto→ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3)))
38 fofi 9223 . . . . 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 693 . . . 4 ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∈ Fin
40 i1frn 25644 . . . . 5 ( ∈ dom ∫1 → ran ∈ Fin)
4140ad2antlr 728 . . . 4 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran ∈ Fin)
42 unfi 9105 . . . 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 588 . . 3 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ) ∈ Fin)
44 0zd 12536 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → 0 ∈ ℤ)
4527frnd 6676 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ran ⊆ ℝ)
46 i1f0rn 25649 . . . . . . . . . . . . . . . . . 18 ( ∈ dom ∫1 → 0 ∈ ran )
47 elex2 2813 . . . . . . . . . . . . . . . . . 18 (0 ∈ ran → ∃𝑥 𝑥 ∈ ran )
4846, 47syl 17 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → ∃𝑥 𝑥 ∈ ran )
49 n0 4293 . . . . . . . . . . . . . . . . 17 (ran ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ran )
5048, 49sylibr 234 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ran ≠ ∅)
51 fimaxre2 12101 . . . . . . . . . . . . . . . . 17 ((ran ⊆ ℝ ∧ ran ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥)
5245, 40, 51syl2anc 585 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥)
53 suprcl 12116 . . . . . . . . . . . . . . . 16 ((ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥) → sup(ran , ℝ, < ) ∈ ℝ)
5445, 50, 52, 53syl3anc 1374 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → sup(ran , ℝ, < ) ∈ ℝ)
5554ad3antlr 732 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → sup(ran , ℝ, < ) ∈ ℝ)
5655, 14, 20redivcld 11983 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (sup(ran , ℝ, < ) / (𝑣 / 3)) ∈ ℝ)
57 peano2re 11319 . . . . . . . . . . . . 13 ((sup(ran , ℝ, < ) / (𝑣 / 3)) ∈ ℝ → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ)
5856, 57syl 17 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ)
59 ceicl 13800 . . . . . . . . . . . 12 (((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
6058, 59syl 17 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
6160adantr 480 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
6221flcld 13757 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
6362adantr 480 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
64 3nn 12260 . . . . . . . . . . . . . . . . 17 3 ∈ ℕ
65 nnrp 12954 . . . . . . . . . . . . . . . . 17 (3 ∈ ℕ → 3 ∈ ℝ+)
6664, 65ax-mp 5 . . . . . . . . . . . . . . . 16 3 ∈ ℝ+
67 rpdivcl 12969 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ℝ+ ∧ 3 ∈ ℝ+) → (𝑣 / 3) ∈ ℝ+)
6866, 67mpan2 692 . . . . . . . . . . . . . . 15 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℝ+)
6968ad2antlr 728 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
701ad2antrr 727 . . . . . . . . . . . . . . . . 17 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
7170ffvelcdmda 7036 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
72 elrege0 13407 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
7371, 72sylib 218 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
7473simprd 495 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹𝑥))
756, 69, 74divge0d 13026 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹𝑥) / (𝑣 / 3)))
76 flge0nn0 13779 . . . . . . . . . . . . 13 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ 0 ≤ ((𝐹𝑥) / (𝑣 / 3))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℕ0)
7721, 75, 76syl2anc 585 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℕ0)
7877nn0ge0d 12501 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ (⌊‘((𝐹𝑥) / (𝑣 / 3))))
7978adantr 480 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → 0 ≤ (⌊‘((𝐹𝑥) / (𝑣 / 3))))
8045, 50, 523jca 1129 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → (ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥))
8180ad3antlr 732 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥))
82 ffn 6668 . . . . . . . . . . . . . . . . . 18 (:ℝ⟶ℝ → Fn ℝ)
8327, 82syl 17 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 Fn ℝ)
84 dffn3 6680 . . . . . . . . . . . . . . . . 17 ( Fn ℝ ↔ :ℝ⟶ran )
8583, 84sylib 218 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1:ℝ⟶ran )
8685ad2antlr 728 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → :ℝ⟶ran )
8786ffvelcdmda 7036 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ ran )
88 suprub 12117 . . . . . . . . . . . . . 14 (((ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥) ∧ (𝑥) ∈ ran ) → (𝑥) ≤ sup(ran , ℝ, < ))
8981, 87, 88syl2anc 585 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ≤ sup(ran , ℝ, < ))
90 letr 11240 . . . . . . . . . . . . . . 15 (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ ∧ (𝑥) ∈ ℝ ∧ sup(ran , ℝ, < ) ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < )))
9126, 29, 55, 90syl3anc 1374 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < )))
9225, 55, 69lemuldivd 13035 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) ↔ ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (sup(ran , ℝ, < ) / (𝑣 / 3))))
93 1red 11145 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
9423, 93, 56lesubaddd 11747 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (sup(ran , ℝ, < ) / (𝑣 / 3)) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
9592, 94bitrd 279 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
96 ceige 13803 . . . . . . . . . . . . . . . . 17 (((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
9758, 96syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
9860zred 12633 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℝ)
99 letr 11240 . . . . . . . . . . . . . . . . 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))))
10023, 58, 98, 99syl3anc 1374 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∧ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10197, 100mpan2d 695 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10295, 101sylbid 240 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10391, 102syld 47 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10489, 103mpan2d 695 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
105104adantrd 491 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
106105imp 406 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
10744, 61, 63, 79, 106elfzd 13469 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
108 eqid 2736 . . . . . . . . 9 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))
109 oveq1 7374 . . . . . . . . . . 11 (𝑡 = (⌊‘((𝐹𝑥) / (𝑣 / 3))) → (𝑡 − 1) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1))
110109oveq1d 7382 . . . . . . . . . 10 (𝑡 = (⌊‘((𝐹𝑥) / (𝑣 / 3))) → ((𝑡 − 1) · (𝑣 / 3)) = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))
111110rspceeqv 3587 . . . . . . . . 9 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ∧ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) → ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3)))
112107, 108, 111sylancl 587 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3)))
113 ovex 7400 . . . . . . . . 9 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ V
11434elrnmpt 5913 . . . . . . . . 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))))
115113, 114ax-mp 5 . . . . . . . 8 ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ↔ ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3)))
116112, 115sylibr 234 . . . . . . 7 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))))
117 elun1 4122 . . . . . . 7 ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
118116, 117syl 17 . . . . . 6 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
119 elun2 4123 . . . . . . . 8 ((𝑥) ∈ ran → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
12087, 119syl 17 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
121120adantr 480 . . . . . 6 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
122118, 121ifclda 4502 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
123122fmpttd 7067 . . . 4 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))):ℝ⟶(ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
124123frnd 6676 . . 3 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ⊆ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
125 ssfi 9107 . . 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)
12643, 124, 125syl2anc 585 . 2 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∈ Fin)
127 eqid 2736 . . . . 5 (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
128127mptpreima 6202 . . . 4 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}}
129 unrab 4255 . . . . 5 ({𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))} ∪ {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))}) = {𝑥 ∈ ℝ ∣ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥)))}
130 inrab 4256 . . . . . . . 8 ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) = {𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)}
131130ineq1i 4156 . . . . . . 7 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = ({𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))})
132 inrab 4256 . . . . . . 7 ({𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = {𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))}
133131, 132eqtri 2759 . . . . . 6 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = {𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))}
134 unrab 4255 . . . . . . . 8 ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) = {𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)}
135134ineq1i 4156 . . . . . . 7 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = ({𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
136 inrab 4256 . . . . . . 7 ({𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))}
137135, 136eqtri 2759 . . . . . 6 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))}
138133, 137uneq12i 4106 . . . . 5 ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})) = ({𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))} ∪ {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))})
139 eqcom 2743 . . . . . . 7 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 𝑡𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
140 fvex 6853 . . . . . . . . 9 (𝑥) ∈ V
141113, 140ifex 4517 . . . . . . . 8 if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ V
142141elsn 4582 . . . . . . 7 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 𝑡)
143 ianor 984 . . . . . . . . . . 11 (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ↔ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ ¬ (𝑥) ≠ 0))
144 nne 2936 . . . . . . . . . . . 12 (¬ (𝑥) ≠ 0 ↔ (𝑥) = 0)
145144orbi2i 913 . . . . . . . . . . 11 ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ ¬ (𝑥) ≠ 0) ↔ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0))
146143, 145bitr2i 276 . . . . . . . . . 10 ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ↔ ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0))
147146anbi1i 625 . . . . . . . . 9 (((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥)) ↔ (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (𝑥)))
148147orbi2i 913 . . . . . . . 8 (((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))) ↔ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (𝑥))))
149 eqif 4508 . . . . . . . 8 (𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ↔ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (𝑥))))
150148, 149bitr4i 278 . . . . . . 7 (((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))) ↔ 𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
151139, 142, 1503bitr4i 303 . . . . . 6 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))))
152151rabbii 3394 . . . . 5 {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} = {𝑥 ∈ ℝ ∣ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥)))}
153129, 138, 1523eqtr4ri 2770 . . . 4 {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} = ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}))
154128, 153eqtri 2759 . . 3 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}))
155 eldifi 4071 . . . . . 6 (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → 𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))))
15631frnd 6676 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ⊆ ℝ)
157156sseld 3920 . . . . . 6 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) → 𝑡 ∈ ℝ))
158155, 157syl5 34 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → 𝑡 ∈ ℝ))
159158imdistani 568 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ))
160 rabiun 37914 . . . . . . . . . 10 {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)}
161 cnvimarndm 6048 . . . . . . . . . . . . . 14 ( “ ran ) = dom
162 iunid 5003 . . . . . . . . . . . . . . . 16 𝑡 ∈ ran {𝑡} = ran
163162imaeq2i 6023 . . . . . . . . . . . . . . 15 ( 𝑡 ∈ ran {𝑡}) = ( “ ran )
164 imaiun 7200 . . . . . . . . . . . . . . 15 ( 𝑡 ∈ ran {𝑡}) = 𝑡 ∈ ran ( “ {𝑡})
165163, 164eqtr3i 2761 . . . . . . . . . . . . . 14 ( “ ran ) = 𝑡 ∈ ran ( “ {𝑡})
166161, 165eqtr3i 2761 . . . . . . . . . . . . 13 dom = 𝑡 ∈ ran ( “ {𝑡})
16727fdmd 6678 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → dom = ℝ)
168166, 167eqtr3id 2785 . . . . . . . . . . . 12 ( ∈ dom ∫1 𝑡 ∈ ran ( “ {𝑡}) = ℝ)
169168ad2antlr 728 . . . . . . . . . . 11 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran ( “ {𝑡}) = ℝ)
170 rabeq 3403 . . . . . . . . . . 11 ( 𝑡 ∈ ran ( “ {𝑡}) = ℝ → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
171169, 170syl 17 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
172160, 171eqtr3id 2785 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
173 fniniseg 7012 . . . . . . . . . . . . . . . . . 18 ( Fn ℝ → (𝑥 ∈ ( “ {𝑡}) ↔ (𝑥 ∈ ℝ ∧ (𝑥) = 𝑡)))
17427, 82, 1733syl 18 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → (𝑥 ∈ ( “ {𝑡}) ↔ (𝑥 ∈ ℝ ∧ (𝑥) = 𝑡)))
175174simplbda 499 . . . . . . . . . . . . . . . 16 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → (𝑥) = 𝑡)
176175breq2d 5097 . . . . . . . . . . . . . . 15 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ↔ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
177176rabbidva 3395 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
178 inrab2 4257 . . . . . . . . . . . . . . 15 ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡}
179 imassrn 6036 . . . . . . . . . . . . . . . . . 18 ( “ {𝑡}) ⊆ ran
180 dfdm4 5850 . . . . . . . . . . . . . . . . . . 19 dom = ran
181180, 167eqtr3id 2785 . . . . . . . . . . . . . . . . . 18 ( ∈ dom ∫1 → ran = ℝ)
182179, 181sseqtrid 3964 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → ( “ {𝑡}) ⊆ ℝ)
183 sseqin2 4163 . . . . . . . . . . . . . . . . 17 (( “ {𝑡}) ⊆ ℝ ↔ (ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}))
184182, 183sylib 218 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → (ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}))
185 rabeq 3403 . . . . . . . . . . . . . . . 16 ((ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}) → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
186184, 185syl 17 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
187178, 186eqtrid 2783 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
188177, 187eqtr4d 2774 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
189188ad3antlr 732 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
19025adantlr 716 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
19145ad2antlr 728 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran ⊆ ℝ)
192191sselda 3921 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → 𝑡 ∈ ℝ)
193192adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℝ)
19468ad3antlr 732 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
195190, 193, 194lemuldivd 13035 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡 ↔ ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (𝑡 / (𝑣 / 3))))
19623adantlr 716 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
197 1red 11145 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
19813ad3antlr 732 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
19919ad3antlr 732 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
200193, 198, 199redivcld 11983 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
201196, 197, 200lesubaddd 11747 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (𝑡 / (𝑣 / 3)) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1)))
2026adantlr 716 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
203 peano2re 11319 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 / (𝑣 / 3)) ∈ ℝ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
204200, 203syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
205 reflcl 13755 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ → (⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ)
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ)
207 peano2re 11319 . . . . . . . . . . . . . . . . . . . 20 ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ → ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ∈ ℝ)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ∈ ℝ)
209202, 208, 194ltdivmuld 13037 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ↔ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))))
21021adantlr 716 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
211 flflp1 13766 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ ((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))
212210, 204, 211syl2anc 585 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ ((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))
213198, 208remulcld 11175 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ)
214213rexrd 11195 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ*)
215 elioomnf 13397 . . . . . . . . . . . . . . . . . . . 20 (((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
216214, 215syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
217202biantrurd 532 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
218216, 217bitr4d 282 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))))
219209, 212, 2183bitr4d 311 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
220195, 201, 2193bitrd 305 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡 ↔ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
221220rabbidva 3395 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
2221feqmptd 6908 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
223222cnveqd 5830 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
224223imaeq1d 6024 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
225 eqid 2736 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ ↦ (𝐹𝑥)) = (𝑥 ∈ ℝ ↦ (𝐹𝑥))
226225mptpreima 6202 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))}
227224, 226eqtrdi 2787 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
228227ad3antrrr 731 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
229221, 228eqtr4d 2774 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
230 itg2addnc.f1 . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ MblFn)
231 mbfima 25597 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
232230, 4, 231syl2anc 585 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
233232ad3antrrr 731 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
234229, 233eqeltrd 2836 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
23545sseld 3920 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → (𝑡 ∈ ran 𝑡 ∈ ℝ))
236235ad2antlr 728 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ ran 𝑡 ∈ ℝ))
237236imdistani 568 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ))
238 i1fmbf 25642 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 ∈ MblFn)
239238, 27jca 511 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ( ∈ MblFn ∧ :ℝ⟶ℝ))
240239ad2antlr 728 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ( ∈ MblFn ∧ :ℝ⟶ℝ))
241 mbfimasn 25599 . . . . . . . . . . . . . . . 16 (( ∈ MblFn ∧ :ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
2422413expa 1119 . . . . . . . . . . . . . . 15 ((( ∈ MblFn ∧ :ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
243240, 242sylan 581 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
244237, 243syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ( “ {𝑡}) ∈ dom vol)
245 inmbl 25509 . . . . . . . . . . . . 13 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol ∧ ( “ {𝑡}) ∈ dom vol) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
246234, 244, 245syl2anc 585 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
247189, 246eqeltrd 2836 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
248247ralrimiva 3129 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
249 finiunmbl 25511 . . . . . . . . . 10 ((ran ∈ Fin ∧ ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
25041, 248, 249syl2anc 585 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
251172, 250eqeltrrd 2837 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
252 unrab 4255 . . . . . . . . . . 11 ({𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}) = {𝑥 ∈ ℝ ∣ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))}
25327feqmptd 6908 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 = (𝑥 ∈ ℝ ↦ (𝑥)))
254253cnveqd 5830 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 = (𝑥 ∈ ℝ ↦ (𝑥)))
255254imaeq1d 6024 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → ( “ (-∞(,)0)) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ (-∞(,)0)))
256 eqid 2736 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ (𝑥)) = (𝑥 ∈ ℝ ↦ (𝑥))
257256mptpreima 6202 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ↦ (𝑥)) “ (-∞(,)0)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)}
258255, 257eqtrdi 2787 . . . . . . . . . . . 12 ( ∈ dom ∫1 → ( “ (-∞(,)0)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)})
259254imaeq1d 6024 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → ( “ (0(,)+∞)) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ (0(,)+∞)))
260256mptpreima 6202 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ↦ (𝑥)) “ (0(,)+∞)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}
261259, 260eqtrdi 2787 . . . . . . . . . . . 12 ( ∈ dom ∫1 → ( “ (0(,)+∞)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)})
262258, 261uneq12d 4109 . . . . . . . . . . 11 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) = ({𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}))
26327ffvelcdmda 7036 . . . . . . . . . . . . 13 (( ∈ dom ∫1𝑥 ∈ ℝ) → (𝑥) ∈ ℝ)
264 0re 11146 . . . . . . . . . . . . . . 15 0 ∈ ℝ
265 lttri2 11228 . . . . . . . . . . . . . . 15 (((𝑥) ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥) ≠ 0 ↔ ((𝑥) < 0 ∨ 0 < (𝑥))))
266264, 265mpan2 692 . . . . . . . . . . . . . 14 ((𝑥) ∈ ℝ → ((𝑥) ≠ 0 ↔ ((𝑥) < 0 ∨ 0 < (𝑥))))
267 ibar 528 . . . . . . . . . . . . . . 15 ((𝑥) ∈ ℝ → (((𝑥) < 0 ∨ 0 < (𝑥)) ↔ ((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥)))))
268 andi 1010 . . . . . . . . . . . . . . . 16 (((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥))) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
269 0xr 11192 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
270 elioomnf 13397 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ* → ((𝑥) ∈ (-∞(,)0) ↔ ((𝑥) ∈ ℝ ∧ (𝑥) < 0)))
271 elioopnf 13396 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ* → ((𝑥) ∈ (0(,)+∞) ↔ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
272270, 271orbi12d 919 . . . . . . . . . . . . . . . . 17 (0 ∈ ℝ* → (((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥)))))
273269, 272ax-mp 5 . . . . . . . . . . . . . . . 16 (((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
274268, 273bitr4i 278 . . . . . . . . . . . . . . 15 (((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥))) ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)))
275267, 274bitrdi 287 . . . . . . . . . . . . . 14 ((𝑥) ∈ ℝ → (((𝑥) < 0 ∨ 0 < (𝑥)) ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
276266, 275bitrd 279 . . . . . . . . . . . . 13 ((𝑥) ∈ ℝ → ((𝑥) ≠ 0 ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
277263, 276syl 17 . . . . . . . . . . . 12 (( ∈ dom ∫1𝑥 ∈ ℝ) → ((𝑥) ≠ 0 ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
278277rabbidva 3395 . . . . . . . . . . 11 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} = {𝑥 ∈ ℝ ∣ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))})
279252, 262, 2783eqtr4a 2797 . . . . . . . . . 10 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) = {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0})
280 i1fima 25645 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ (-∞(,)0)) ∈ dom vol)
281 i1fima 25645 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ (0(,)+∞)) ∈ dom vol)
282 unmbl 25504 . . . . . . . . . . 11 ((( “ (-∞(,)0)) ∈ dom vol ∧ ( “ (0(,)+∞)) ∈ dom vol) → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) ∈ dom vol)
283280, 281, 282syl2anc 585 . . . . . . . . . 10 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) ∈ dom vol)
284279, 283eqeltrrd 2837 . . . . . . . . 9 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol)
285284ad2antlr 728 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol)
286 inmbl 25509 . . . . . . . 8 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
287251, 285, 286syl2anc 585 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
288287adantr 480 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
28923recnd 11173 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℂ)
290289adantlr 716 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℂ)
291 1cnd 11139 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
292 simplr 769 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℝ)
29313ad3antlr 732 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
29419ad3antlr 732 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
295292, 293, 294redivcld 11983 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
296295recnd 11173 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℂ)
297290, 291, 296subadd2d 11524 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
298 eqcom 2743 . . . . . . . . . 10 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ (𝑡 / (𝑣 / 3)) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1))
299 recn 11128 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
300299ad2antlr 728 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℂ)
30125recnd 11173 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℂ)
302301adantlr 716 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℂ)
30313recnd 11173 . . . . . . . . . . . 12 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℂ)
304303ad3antlr 732 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℂ)
305300, 302, 304, 294divmul3d 11965 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
306298, 305bitrid 283 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
307297, 306bitr3d 281 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
308307rabbidva 3395 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))})
309 imaundi 6113 . . . . . . . . . . 11 (𝐹 “ ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
310223ad4antr 733 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
311 zre 12528 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
312311adantl 481 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
31313ad3antlr 732 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ)
314312, 313remulcld 11175 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ)
315314rexrd 11195 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ*)
316 peano2z 12568 . . . . . . . . . . . . . . . . 17 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℤ)
317316zred 12633 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
318317adantl 481 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
319313, 318remulcld 11175 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
320319rexrd 11195 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ*)
321 zcn 12529 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℂ)
322321adantl 481 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℂ)
323303ad3antlr 732 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℂ)
324322, 323mulcomd 11166 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) = ((𝑣 / 3) · ((𝑡 / (𝑣 / 3)) + 1)))
32568ad3antlr 732 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ+)
326311ltp1d 12086 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) < (((𝑡 / (𝑣 / 3)) + 1) + 1))
327326adantl 481 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) < (((𝑡 / (𝑣 / 3)) + 1) + 1))
328312, 318, 325, 327ltmul2dd 13042 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · ((𝑡 / (𝑣 / 3)) + 1)) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))
329324, 328eqbrtrd 5107 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))
330 snunioo 13431 . . . . . . . . . . . . 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))))
331315, 320, 329, 330syl3anc 1374 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))
332310, 331imaeq12d 6026 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
333309, 332eqtr3id 2785 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
334225mptpreima 6202 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))}
3354ad3antrrr 731 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → 𝐹:ℝ⟶ℝ)
336335ffvelcdmda 7036 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
3373363biant1d 1481 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
338337adantr 480 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
339311adantl 481 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
340336adantr 480 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹𝑥) ∈ ℝ)
34168ad4antlr 734 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ+)
342339, 340, 341lemuldivd 13035 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ ((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3))))
343317adantl 481 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
344340, 343, 341ltdivmuld 13037 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1) ↔ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))
345344bicomd 223 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ↔ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1)))
346342, 345anbi12d 633 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
347338, 346bitr3d 281 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
348 elico2 13363 . . . . . . . . . . . . . . . 16 (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ ∧ ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ*) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
349314, 320, 348syl2anc 585 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
350349adantlr 716 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
351 eqcom 2743 . . . . . . . . . . . . . . 15 (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1))
35221adantlr 716 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
353 flbi 13775 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
354352, 353sylan 581 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
355351, 354bitrid 283 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
356347, 350, 3553bitr4d 311 . . . . . . . . . . . . 13 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
357356an32s 653 . . . . . . . . . . . 12 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
358357rabbidva 3395 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))} = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
359334, 358eqtrid 2783 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
360333, 359eqtrd 2771 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
361230ad4antr 733 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹 ∈ MblFn)
3624ad4antr 733 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹:ℝ⟶ℝ)
363 mbfimasn 25599 . . . . . . . . . . 11 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ) → (𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∈ dom vol)
364361, 362, 314, 363syl3anc 1374 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∈ dom vol)
365 mbfima 25597 . . . . . . . . . . . 12 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
366230, 4, 365syl2anc 585 . . . . . . . . . . 11 (𝜑 → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
367366ad4antr 733 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
368 unmbl 25504 . . . . . . . . . 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)
369364, 367, 368syl2anc 585 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) ∈ dom vol)
370360, 369eqeltrrd 2837 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
371 simpr 484 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
372352flcld 13757 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
373372adantr 480 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
374371, 373eqeltrd 2836 . . . . . . . . . . . . 13 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ)
375374stoic1a 1774 . . . . . . . . . . . 12 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
376375an32s 653 . . . . . . . . . . 11 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) ∧ 𝑥 ∈ ℝ) → ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
377376ralrimiva 3129 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ∀𝑥 ∈ ℝ ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
378 rabeq0 4328 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
379377, 378sylibr 234 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = ∅)
380 0mbl 25506 . . . . . . . . 9 ∅ ∈ dom vol
381379, 380eqeltrdi 2844 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
382370, 381pm2.61dan 813 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
383308, 382eqeltrrd 2837 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))} ∈ dom vol)
384 inmbl 25509 . . . . . 6 ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))} ∈ dom vol) → (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∈ dom vol)
385288, 383, 384syl2anc 585 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∈ dom vol)
386 rabiun 37914 . . . . . . . . . . 11 {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)}
387 rabeq 3403 . . . . . . . . . . . 12 ( 𝑡 ∈ ran ( “ {𝑡}) = ℝ → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
388168, 387syl 17 . . . . . . . . . . 11 ( ∈ dom ∫1 → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
389386, 388eqtr3id 2785 . . . . . . . . . 10 ( ∈ dom ∫1 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
390389ad2antlr 728 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
391176notbid 318 . . . . . . . . . . . . . . 15 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
392391rabbidva 3395 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
393 inrab2 4257 . . . . . . . . . . . . . . 15 ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡}
394 rabeq 3403 . . . . . . . . . . . . . . . 16 ((ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}) → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
395184, 394syl 17 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
396393, 395eqtrid 2783 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
397392, 396eqtr4d 2774 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
398397ad3antlr 732 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
399 imaundi 6113 . . . . . . . . . . . . . . . . 17 (𝐹 “ ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)))
40013, 19jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 ∈ ℝ+ → ((𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0))
401 redivcl 11874 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑡 ∈ ℝ ∧ (𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
4024013expb 1121 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ ℝ ∧ ((𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0)) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
403400, 402sylan2 594 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℝ ∧ 𝑣 ∈ ℝ+) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
404403ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
405404adantll 715 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
406405, 203syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
407 peano2re 11319 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
408 reflcl 13755 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
409406, 407, 4083syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
41013ad2antlr 728 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
411409, 410remulcld 11175 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ)
412411rexrd 11195 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ*)
413 pnfxr 11199 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
414413a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → +∞ ∈ ℝ*)
415 ltpnf 13071 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) < +∞)
416411, 415syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) < +∞)
417 snunioo 13431 . . . . . . . . . . . . . . . . . . 19 ((((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) < +∞) → ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) = (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞))
418412, 414, 416, 417syl3anc 1374 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) = (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞))
419418imaeq2d 6025 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
420399, 419eqtr3id 2785 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
421223imaeq1d 6024 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
422225mptpreima 6202 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)}
423421, 422eqtrdi 2787 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)})
424423ad3antrrr 731 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)})
425406, 407syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
426425adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
427 flflp1 13766 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ ∧ ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3)) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
428426, 352, 427syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3)) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
429411adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ)
430 elicopnf 13398 . . . . . . . . . . . . . . . . . . . . . 22 (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
431429, 430syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
432336biantrurd 532 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
433409adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
43468ad3antlr 732 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
435433, 336, 434lemuldivd 13035 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3))))
436431, 432, 4353bitr2d 307 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3))))
437406adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
438352, 22syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
439 1red 11145 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
440437, 438, 439ltadd1d 11743 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
441428, 436, 4403bitr4d 311 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
442295, 439, 438ltaddsubd 11750 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1)))
443441, 442bitrd 279 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ (𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1)))
444438, 24syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
445292, 444, 434ltdivmul2d 13038 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ↔ 𝑡 < (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
446444, 293remulcld 11175 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ)
447292, 446ltnled 11293 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 < (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
448443, 445, 4473bitrd 305 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
449448rabbidva 3395 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
450420, 424, 4493eqtrd 2775 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
451230ad3antrrr 731 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → 𝐹 ∈ MblFn)
452 mbfimasn 25599 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ) → (𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∈ dom vol)
453451, 335, 411, 452syl3anc 1374 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∈ dom vol)
454 mbfima 25597 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
455230, 4, 454syl2anc 585 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
456455ad3antrrr 731 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
457 unmbl 25504 . . . . . . . . . . . . . . . 16 (((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∈ dom vol ∧ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) ∈ dom vol)
458453, 456, 457syl2anc 585 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) ∈ dom vol)
459450, 458eqeltrrd 2837 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
460237, 459syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
461 inmbl 25509 . . . . . . . . . . . . 13 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol ∧ ( “ {𝑡}) ∈ dom vol) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
462460, 244, 461syl2anc 585 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
463398, 462eqeltrd 2836 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
464463ralrimiva 3129 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
465 finiunmbl 25511 . . . . . . . . . 10 ((ran ∈ Fin ∧ ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
46641, 464, 465syl2anc 585 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
467390, 466eqeltrrd 2837 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
468254imaeq1d 6024 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ {0}) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}))
469256mptpreima 6202 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}
470140elsn 4582 . . . . . . . . . . . . 13 ((𝑥) ∈ {0} ↔ (𝑥) = 0)
471470rabbii 3394 . . . . . . . . . . . 12 {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}} = {𝑥 ∈ ℝ ∣ (𝑥) = 0}
472469, 471eqtri 2759 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) = 0}
473468, 472eqtrdi 2787 . . . . . . . . . 10 ( ∈ dom ∫1 → ( “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) = 0})
474 i1fima 25645 . . . . . . . . . 10 ( ∈ dom ∫1 → ( “ {0}) ∈ dom vol)
475473, 474eqeltrrd 2837 . . . . . . . . 9 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol)
476475ad2antlr 728 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol)
477 unmbl 25504 . . . . . . . 8 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
478467, 476, 477syl2anc 585 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
479478adantr 480 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
480254imaeq1d 6024 . . . . . . . . 9 ( ∈ dom ∫1 → ( “ {𝑡}) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}))
481256mptpreima 6202 . . . . . . . . . 10 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {𝑡}}
482140elsn 4582 . . . . . . . . . . . 12 ((𝑥) ∈ {𝑡} ↔ (𝑥) = 𝑡)
483 eqcom 2743 . . . . . . . . . . . 12 ((𝑥) = 𝑡𝑡 = (𝑥))
484482, 483bitri 275 . . . . . . . . . . 11 ((𝑥) ∈ {𝑡} ↔ 𝑡 = (𝑥))
485484rabbii 3394 . . . . . . . . . 10 {𝑥 ∈ ℝ ∣ (𝑥) ∈ {𝑡}} = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}
486481, 485eqtri 2759 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}
487480, 486eqtrdi 2787 . . . . . . . 8 ( ∈ dom ∫1 → ( “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
488487ad3antlr 732 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
489488, 243eqeltrrd 2837 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)} ∈ dom vol)
490 inmbl 25509 . . . . . 6 ((({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)} ∈ dom vol) → (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) ∈ dom vol)
491479, 489, 490syl2anc 585 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) ∈ dom vol)
492 unmbl 25504 . . . . 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)
493385, 491, 492syl2anc 585 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})) ∈ dom vol)
494159, 493syl 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)
495154, 494eqeltrid 2840 . 2 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∈ dom vol)
496 mblvol 25497 . . . 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)), (𝑥))) “ {𝑡})))
497495, 496syl 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)), (𝑥))) “ {𝑡})))
498 eldifsn 4731 . . . . . 6 (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) ↔ (𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∧ 𝑡 ≠ 0))
499157anim1d 612 . . . . . 6 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ((𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∧ 𝑡 ≠ 0) → (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
500498, 499biimtrid 242 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
501500imdistani 568 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
502128a1i 11 . . . . . . . . . . 11 ( ∈ dom ∫1 → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}})
503468, 469eqtrdi 2787 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}})
504502, 503ineq12d 4161 . . . . . . . . . 10 ( ∈ dom ∫1 → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ({𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}))
505 inrab 4256 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})}
506504, 505eqtrdi 2787 . . . . . . . . 9 ( ∈ dom ∫1 → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})})
507506ad3antlr 732 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})})
508144biimpri 228 . . . . . . . . . . . . . . . . . 18 ((𝑥) = 0 → ¬ (𝑥) ≠ 0)
509508intnand 488 . . . . . . . . . . . . . . . . 17 ((𝑥) = 0 → ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0))
510509iffalsed 4477 . . . . . . . . . . . . . . . 16 ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = (𝑥))
511 eqtr 2756 . . . . . . . . . . . . . . . 16 ((if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = (𝑥) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
512510, 511mpancom 689 . . . . . . . . . . . . . . 15 ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
513512adantl 481 . . . . . . . . . . . . . 14 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
514 simpll 767 . . . . . . . . . . . . . . 15 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → 𝑡 ≠ 0)
515514necomd 2987 . . . . . . . . . . . . . 14 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → 0 ≠ 𝑡)
516513, 515eqnetrd 2999 . . . . . . . . . . . . 13 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡)
517516ex 412 . . . . . . . . . . . 12 ((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) → ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
518 orcom 871 . . . . . . . . . . . . . 14 ((¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∨ ¬ (𝑥) ∈ {0}) ↔ (¬ (𝑥) ∈ {0} ∨ ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
519 ianor 984 . . . . . . . . . . . . . 14 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ (¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∨ ¬ (𝑥) ∈ {0}))
520 imor 854 . . . . . . . . . . . . . 14 (((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}) ↔ (¬ (𝑥) ∈ {0} ∨ ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
521518, 519, 5203bitr4i 303 . . . . . . . . . . . . 13 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ ((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
522142necon3bbii 2979 . . . . . . . . . . . . . 14 (¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡)
523470, 522imbi12i 350 . . . . . . . . . . . . 13 (((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}) ↔ ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
524521, 523bitri 275 . . . . . . . . . . . 12 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
525517, 524sylibr 234 . . . . . . . . . . 11 ((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) → ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
526525ralrimiva 3129 . . . . . . . . . 10 (𝑡 ≠ 0 → ∀𝑥 ∈ ℝ ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
527 rabeq0 4328 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
528526, 527sylibr 234 . . . . . . . . 9 (𝑡 ≠ 0 → {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅)
529528ad2antll 730 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅)
530507, 529eqtrd 2771 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ∅)
531 imassrn 6036 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
532 dfdm4 5850 . . . . . . . . . 10 dom (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
533141, 127dmmpti 6642 . . . . . . . . . 10 dom (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ℝ
534532, 533eqtr3i 2761 . . . . . . . . 9 ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ℝ
535531, 534sseqtri 3970 . . . . . . . 8 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ℝ
536 reldisj 4393 . . . . . . . 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}))))
537535, 536ax-mp 5 . . . . . . 7 ((((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ∅ ↔ ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ (ℝ ∖ ( “ {0})))
538530, 537sylib 218 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ (ℝ ∖ ( “ {0})))
539 ffun 6671 . . . . . . . . . 10 (:ℝ⟶ℝ → Fun )
540 difpreima 7017 . . . . . . . . . 10 (Fun → ( “ (ran ∖ {0})) = (( “ ran ) ∖ ( “ {0})))
541539, 540syl 17 . . . . . . . . 9 (:ℝ⟶ℝ → ( “ (ran ∖ {0})) = (( “ ran ) ∖ ( “ {0})))
542 fdm 6677 . . . . . . . . . . 11 (:ℝ⟶ℝ → dom = ℝ)
543161, 542eqtrid 2783 . . . . . . . . . 10 (:ℝ⟶ℝ → ( “ ran ) = ℝ)
544543difeq1d 4065 . . . . . . . . 9 (:ℝ⟶ℝ → (( “ ran ) ∖ ( “ {0})) = (ℝ ∖ ( “ {0})))
545541, 544eqtrd 2771 . . . . . . . 8 (:ℝ⟶ℝ → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
54627, 545syl 17 . . . . . . 7 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
547546ad3antlr 732 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
548538, 547sseqtrrd 3959 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ( “ (ran ∖ {0})))
549 imassrn 6036 . . . . . . 7 ( “ (ran ∖ {0})) ⊆ ran
550549, 181sseqtrid 3964 . . . . . 6 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) ⊆ ℝ)
551550ad3antlr 732 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ( “ (ran ∖ {0})) ⊆ ℝ)
552 i1fima 25645 . . . . . . . 8 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) ∈ dom vol)
553 mblvol 25497 . . . . . . . 8 (( “ (ran ∖ {0})) ∈ dom vol → (vol‘( “ (ran ∖ {0}))) = (vol*‘( “ (ran ∖ {0}))))
554552, 553syl 17 . . . . . . 7 ( ∈ dom ∫1 → (vol‘( “ (ran ∖ {0}))) = (vol*‘( “ (ran ∖ {0}))))
555 neldifsn 4737 . . . . . . . 8 ¬ 0 ∈ (ran ∖ {0})
556 i1fima2 25646 . . . . . . . 8 (( ∈ dom ∫1 ∧ ¬ 0 ∈ (ran ∖ {0})) → (vol‘( “ (ran ∖ {0}))) ∈ ℝ)
557555, 556mpan2 692 . . . . . . 7 ( ∈ dom ∫1 → (vol‘( “ (ran ∖ {0}))) ∈ ℝ)
558554, 557eqeltrrd 2837 . . . . . 6 ( ∈ dom ∫1 → (vol*‘( “ (ran ∖ {0}))) ∈ ℝ)
559558ad3antlr 732 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (vol*‘( “ (ran ∖ {0}))) ∈ ℝ)
560 ovolsscl 25453 . . . . 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)), (𝑥))) “ {𝑡})) ∈ ℝ)
561548, 551, 559, 560syl3anc 1374 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
562501, 561syl 17 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
563497, 562eqeltrd 2836 . 2 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (vol‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
56431, 126, 495, 563i1fd 25648 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 206  wa 395  wo 848  w3a 1087   = wceq 1542  wex 1781  wcel 2114  wne 2932  wral 3051  wrex 3061  {crab 3389  Vcvv 3429  cdif 3886  cun 3887  cin 3888  wss 3889  c0 4273  ifcif 4466  {csn 4567   ciun 4933   class class class wbr 5085  cmpt 5166  ccnv 5630  dom cdm 5631  ran crn 5632  cima 5634  Fun wfun 6492   Fn wfn 6493  wf 6494  ontowfo 6496  cfv 6498  (class class class)co 7367  Fincfn 8893  supcsup 9353  cc 11036  cr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043  +∞cpnf 11176  -∞cmnf 11177  *cxr 11178   < clt 11179  cle 11180  cmin 11377  -cneg 11378   / cdiv 11807  cn 12174  3c3 12237  0cn0 12437  cz 12524  +crp 12942  (,)cioo 13298  [,)cico 13300  ...cfz 13461  cfl 13749  vol*covol 25429  volcvol 25430  MblFncmbf 25581  1citg1 25582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-inf2 9562  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-er 8643  df-map 8775  df-pm 8776  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fi 9324  df-sup 9355  df-inf 9356  df-oi 9425  df-dju 9825  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-n0 12438  df-z 12525  df-uz 12789  df-q 12899  df-rp 12943  df-xneg 13063  df-xadd 13064  df-xmul 13065  df-ioo 13302  df-ico 13304  df-icc 13305  df-fz 13462  df-fzo 13609  df-fl 13751  df-seq 13964  df-exp 14024  df-hash 14293  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198  df-clim 15450  df-sum 15649  df-rest 17385  df-topgen 17406  df-psmet 21344  df-xmet 21345  df-met 21346  df-bl 21347  df-mopn 21348  df-top 22859  df-topon 22876  df-bases 22911  df-cmp 23352  df-ovol 25431  df-vol 25432  df-mbf 25586  df-itg1 25587
This theorem is referenced by:  itg2addnclem3  37994
  Copyright terms: Public domain W3C validator