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 38301
Description: Lemma for itg2addnc 38303. 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 13484 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ
3 fss 6724 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
41, 2, 3sylancl 597 . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
54ad2antrr 738 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝐹:ℝ⟶ℝ)
65ffvelcdmda 7081 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
7 rpre 13026 . . . . . . . . . 10 (𝑣 ∈ ℝ+𝑣 ∈ ℝ)
8 3re 12322 . . . . . . . . . . 11 3 ∈ ℝ
9 3ne0 12351 . . . . . . . . . . 11 3 ≠ 0
108, 9pm3.2i 475 . . . . . . . . . 10 (3 ∈ ℝ ∧ 3 ≠ 0)
11 redivcl 11935 . . . . . . . . . . 11 ((𝑣 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (𝑣 / 3) ∈ ℝ)
12113expb 1138 . . . . . . . . . 10 ((𝑣 ∈ ℝ ∧ (3 ∈ ℝ ∧ 3 ≠ 0)) → (𝑣 / 3) ∈ ℝ)
137, 10, 12sylancl 597 . . . . . . . . 9 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℝ)
1413ad2antlr 739 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
15 rpcnne0 13036 . . . . . . . . . 10 (𝑣 ∈ ℝ+ → (𝑣 ∈ ℂ ∧ 𝑣 ≠ 0))
16 3cn 12323 . . . . . . . . . . 11 3 ∈ ℂ
1716, 9pm3.2i 475 . . . . . . . . . 10 (3 ∈ ℂ ∧ 3 ≠ 0)
18 divne0 11885 . . . . . . . . . 10 (((𝑣 ∈ ℂ ∧ 𝑣 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (𝑣 / 3) ≠ 0)
1915, 17, 18sylancl 597 . . . . . . . . 9 (𝑣 ∈ ℝ+ → (𝑣 / 3) ≠ 0)
2019ad2antlr 739 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
216, 14, 20redivcld 12044 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
22 reflcl 13831 . . . . . . 7 (((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
2321, 22syl 18 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
24 peano2rem 11526 . . . . . 6 ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
2523, 24syl 18 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
2625, 14remulcld 11240 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ)
27 i1ff 25816 . . . . . 6 ( ∈ dom ∫1:ℝ⟶ℝ)
2827ad2antlr 739 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → :ℝ⟶ℝ)
2928ffvelcdmda 7081 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ ℝ)
3026, 29ifcld 4535 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ ℝ)
3130fmpttd 7112 . 2 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))):ℝ⟶ℝ)
32 fzfi 14010 . . . . 5 (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ∈ Fin
33 ovex 7445 . . . . . . 7 ((𝑡 − 1) · (𝑣 / 3)) ∈ V
34 eqid 2763 . . . . . . 7 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) = (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3)))
3533, 34fnmpti 6680 . . . . . 6 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) Fn (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
36 dffn4 6800 . . . . . 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 233 . . . . 5 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))):(0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))–onto→ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3)))
38 fofi 9274 . . . . 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 704 . . . 4 ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∈ Fin
40 i1frn 25817 . . . . 5 ( ∈ dom ∫1 → ran ∈ Fin)
4140ad2antlr 739 . . . 4 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran ∈ Fin)
42 unfi 9156 . . . 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 598 . . 3 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ) ∈ Fin)
44 0zd 12604 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → 0 ∈ ℤ)
4527frnd 6716 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ran ⊆ ℝ)
46 i1f0rn 25822 . . . . . . . . . . . . . . . . . 18 ( ∈ dom ∫1 → 0 ∈ ran )
47 elex2 2840 . . . . . . . . . . . . . . . . . 18 (0 ∈ ran → ∃𝑥 𝑥 ∈ ran )
4846, 47syl 18 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → ∃𝑥 𝑥 ∈ ran )
49 n0 4308 . . . . . . . . . . . . . . . . 17 (ran ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ran )
5048, 49sylibr 237 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ran ≠ ∅)
51 fimaxre2 12161 . . . . . . . . . . . . . . . . 17 ((ran ⊆ ℝ ∧ ran ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥)
5245, 40, 51syl2anc 595 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥)
53 suprcl 12176 . . . . . . . . . . . . . . . 16 ((ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥) → sup(ran , ℝ, < ) ∈ ℝ)
5445, 50, 52, 53syl3anc 1398 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → sup(ran , ℝ, < ) ∈ ℝ)
5554ad3antlr 743 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → sup(ran , ℝ, < ) ∈ ℝ)
5655, 14, 20redivcld 12044 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (sup(ran , ℝ, < ) / (𝑣 / 3)) ∈ ℝ)
57 peano2re 11384 . . . . . . . . . . . . 13 ((sup(ran , ℝ, < ) / (𝑣 / 3)) ∈ ℝ → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ)
5856, 57syl 18 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ)
59 ceicl 13876 . . . . . . . . . . . 12 (((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
6058, 59syl 18 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
6160adantr 485 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
6221flcld 13833 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
6362adantr 485 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
64 3nn 12321 . . . . . . . . . . . . . . . . 17 3 ∈ ℕ
65 nnrp 13029 . . . . . . . . . . . . . . . . 17 (3 ∈ ℕ → 3 ∈ ℝ+)
6664, 65ax-mp 5 . . . . . . . . . . . . . . . 16 3 ∈ ℝ+
67 rpdivcl 13044 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ℝ+ ∧ 3 ∈ ℝ+) → (𝑣 / 3) ∈ ℝ+)
6866, 67mpan2 703 . . . . . . . . . . . . . . 15 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℝ+)
6968ad2antlr 739 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
701ad2antrr 738 . . . . . . . . . . . . . . . . 17 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
7170ffvelcdmda 7081 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
72 elrege0 13482 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
7371, 72sylib 221 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
7473simprd 500 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹𝑥))
756, 69, 74divge0d 13101 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹𝑥) / (𝑣 / 3)))
76 flge0nn0 13855 . . . . . . . . . . . . 13 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ 0 ≤ ((𝐹𝑥) / (𝑣 / 3))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℕ0)
7721, 75, 76syl2anc 595 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℕ0)
7877nn0ge0d 12569 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ (⌊‘((𝐹𝑥) / (𝑣 / 3))))
7978adantr 485 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → 0 ≤ (⌊‘((𝐹𝑥) / (𝑣 / 3))))
8045, 50, 523jca 1146 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → (ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥))
8180ad3antlr 743 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥))
82 ffn 6707 . . . . . . . . . . . . . . . . . 18 (:ℝ⟶ℝ → Fn ℝ)
8327, 82syl 18 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 Fn ℝ)
84 dffn3 6720 . . . . . . . . . . . . . . . . 17 ( Fn ℝ ↔ :ℝ⟶ran )
8583, 84sylib 221 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1:ℝ⟶ran )
8685ad2antlr 739 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → :ℝ⟶ran )
8786ffvelcdmda 7081 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ ran )
88 suprub 12177 . . . . . . . . . . . . . 14 (((ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥) ∧ (𝑥) ∈ ran ) → (𝑥) ≤ sup(ran , ℝ, < ))
8981, 87, 88syl2anc 595 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ≤ sup(ran , ℝ, < ))
90 letr 11305 . . . . . . . . . . . . . . 15 (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ ∧ (𝑥) ∈ ℝ ∧ sup(ran , ℝ, < ) ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < )))
9126, 29, 55, 90syl3anc 1398 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < )))
9225, 55, 69lemuldivd 13110 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) ↔ ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (sup(ran , ℝ, < ) / (𝑣 / 3))))
93 1red 11210 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
9423, 93, 56lesubaddd 11812 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (sup(ran , ℝ, < ) / (𝑣 / 3)) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
9592, 94bitrd 282 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
96 ceige 13879 . . . . . . . . . . . . . . . . 17 (((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
9758, 96syl 18 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
9860zred 12701 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℝ)
99 letr 11305 . . . . . . . . . . . . . . . . 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 1398 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∧ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10197, 100mpan2d 706 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10295, 101sylbid 243 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10391, 102syld 48 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10489, 103mpan2d 706 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
105104adantrd 496 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
106105imp 411 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
10744, 61, 63, 79, 106elfzd 13544 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
108 eqid 2763 . . . . . . . . 9 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))
109 oveq1 7419 . . . . . . . . . . 11 (𝑡 = (⌊‘((𝐹𝑥) / (𝑣 / 3))) → (𝑡 − 1) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1))
110109oveq1d 7427 . . . . . . . . . 10 (𝑡 = (⌊‘((𝐹𝑥) / (𝑣 / 3))) → ((𝑡 − 1) · (𝑣 / 3)) = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))
111110rspceeqv 3605 . . . . . . . . 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 597 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3)))
113 ovex 7445 . . . . . . . . 9 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ V
11434elrnmpt 5950 . . . . . . . . 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 237 . . . . . . 7 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))))
117 elun1 4136 . . . . . . 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 18 . . . . . 6 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
119 elun2 4137 . . . . . . . 8 ((𝑥) ∈ ran → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
12087, 119syl 18 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
121120adantr 485 . . . . . 6 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
122118, 121ifclda 4524 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
123122fmpttd 7112 . . . 4 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))):ℝ⟶(ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
124123frnd 6716 . . 3 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ⊆ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
125 ssfi 9158 . . 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 595 . 2 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∈ Fin)
127 eqid 2763 . . . . 5 (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
128127mptpreima 6241 . . . 4 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}}
129 unrab 4269 . . . . 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 4270 . . . . . . . 8 ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) = {𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)}
131130ineq1i 4170 . . . . . . 7 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = ({𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))})
132 inrab 4270 . . . . . . 7 ({𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = {𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))}
133131, 132eqtri 2786 . . . . . 6 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = {𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))}
134 unrab 4269 . . . . . . . 8 ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) = {𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)}
135134ineq1i 4170 . . . . . . 7 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = ({𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
136 inrab 4270 . . . . . . 7 ({𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))}
137135, 136eqtri 2786 . . . . . 6 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))}
138133, 137uneq12i 4121 . . . . 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 2770 . . . . . . 7 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 𝑡𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
140 fvex 6896 . . . . . . . . 9 (𝑥) ∈ V
141113, 140ifex 4539 . . . . . . . 8 if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ V
142141elsn 4605 . . . . . . 7 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 𝑡)
143 ianor 997 . . . . . . . . . . 11 (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ↔ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ ¬ (𝑥) ≠ 0))
144 nne 2962 . . . . . . . . . . . 12 (¬ (𝑥) ≠ 0 ↔ (𝑥) = 0)
145144orbi2i 925 . . . . . . . . . . 11 ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ ¬ (𝑥) ≠ 0) ↔ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0))
146143, 145bitr2i 279 . . . . . . . . . 10 ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ↔ ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0))
147146anbi1i 635 . . . . . . . . 9 (((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥)) ↔ (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (𝑥)))
148147orbi2i 925 . . . . . . . 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 4530 . . . . . . . 8 (𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ↔ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (𝑥))))
150148, 149bitr4i 281 . . . . . . 7 (((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))) ↔ 𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
151139, 142, 1503bitr4i 306 . . . . . 6 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))))
152151rabbii 3421 . . . . 5 {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} = {𝑥 ∈ ℝ ∣ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥)))}
153129, 138, 1523eqtr4ri 2797 . . . 4 {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} = ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}))
154128, 153eqtri 2786 . . 3 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}))
155 eldifi 4086 . . . . . 6 (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → 𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))))
15631frnd 6716 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ⊆ ℝ)
157156sseld 3937 . . . . . 6 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) → 𝑡 ∈ ℝ))
158155, 157syl5 35 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → 𝑡 ∈ ℝ))
159158imdistani 578 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ))
160 rabiun 38222 . . . . . . . . . 10 {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)}
161 cnvimarndm 6087 . . . . . . . . . . . . . 14 ( “ ran ) = dom
162 iunid 5026 . . . . . . . . . . . . . . . 16 𝑡 ∈ ran {𝑡} = ran
163162imaeq2i 6062 . . . . . . . . . . . . . . 15 ( 𝑡 ∈ ran {𝑡}) = ( “ ran )
164 imaiun 7245 . . . . . . . . . . . . . . 15 ( 𝑡 ∈ ran {𝑡}) = 𝑡 ∈ ran ( “ {𝑡})
165163, 164eqtr3i 2788 . . . . . . . . . . . . . 14 ( “ ran ) = 𝑡 ∈ ran ( “ {𝑡})
166161, 165eqtr3i 2788 . . . . . . . . . . . . 13 dom = 𝑡 ∈ ran ( “ {𝑡})
16727fdmd 6718 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → dom = ℝ)
168166, 167eqtr3id 2812 . . . . . . . . . . . 12 ( ∈ dom ∫1 𝑡 ∈ ran ( “ {𝑡}) = ℝ)
169168ad2antlr 739 . . . . . . . . . . 11 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran ( “ {𝑡}) = ℝ)
170 rabeq 3430 . . . . . . . . . . 11 ( 𝑡 ∈ ran ( “ {𝑡}) = ℝ → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
171169, 170syl 18 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
172160, 171eqtr3id 2812 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
173 fniniseg 7057 . . . . . . . . . . . . . . . . . 18 ( Fn ℝ → (𝑥 ∈ ( “ {𝑡}) ↔ (𝑥 ∈ ℝ ∧ (𝑥) = 𝑡)))
17427, 82, 1733syl 19 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → (𝑥 ∈ ( “ {𝑡}) ↔ (𝑥 ∈ ℝ ∧ (𝑥) = 𝑡)))
175174simplbda 504 . . . . . . . . . . . . . . . 16 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → (𝑥) = 𝑡)
176175breq2d 5122 . . . . . . . . . . . . . . 15 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ↔ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
177176rabbidva 3422 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
178 inrab2 4271 . . . . . . . . . . . . . . 15 ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡}
179 imassrn 6075 . . . . . . . . . . . . . . . . . 18 ( “ {𝑡}) ⊆ ran
180 dfdm4 5887 . . . . . . . . . . . . . . . . . . 19 dom = ran
181180, 167eqtr3id 2812 . . . . . . . . . . . . . . . . . 18 ( ∈ dom ∫1 → ran = ℝ)
182179, 181sseqtrid 3980 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → ( “ {𝑡}) ⊆ ℝ)
183 sseqin2 4177 . . . . . . . . . . . . . . . . 17 (( “ {𝑡}) ⊆ ℝ ↔ (ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}))
184182, 183sylib 221 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → (ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}))
185 rabeq 3430 . . . . . . . . . . . . . . . 16 ((ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}) → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
186184, 185syl 18 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
187178, 186eqtrid 2810 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
188177, 187eqtr4d 2801 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
189188ad3antlr 743 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
19025adantlr 727 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
19145ad2antlr 739 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran ⊆ ℝ)
192191sselda 3938 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → 𝑡 ∈ ℝ)
193192adantr 485 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℝ)
19468ad3antlr 743 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
195190, 193, 194lemuldivd 13110 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡 ↔ ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (𝑡 / (𝑣 / 3))))
19623adantlr 727 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
197 1red 11210 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
19813ad3antlr 743 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
19919ad3antlr 743 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
200193, 198, 199redivcld 12044 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
201196, 197, 200lesubaddd 11812 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (𝑡 / (𝑣 / 3)) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1)))
2026adantlr 727 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
203 peano2re 11384 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 / (𝑣 / 3)) ∈ ℝ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
204200, 203syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
205 reflcl 13831 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ → (⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ)
206204, 205syl 18 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ)
207 peano2re 11384 . . . . . . . . . . . . . . . . . . . 20 ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ → ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ∈ ℝ)
208206, 207syl 18 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ∈ ℝ)
209202, 208, 194ltdivmuld 13112 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ↔ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))))
21021adantlr 727 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
211 flflp1 13842 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ ((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))
212210, 204, 211syl2anc 595 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ ((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))
213198, 208remulcld 11240 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ)
214213rexrd 11260 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ*)
215 elioomnf 13472 . . . . . . . . . . . . . . . . . . . 20 (((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
216214, 215syl 18 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
217202biantrurd 541 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
218216, 217bitr4d 285 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))))
219209, 212, 2183bitr4d 314 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
220195, 201, 2193bitrd 308 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡 ↔ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
221220rabbidva 3422 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
2221feqmptd 6951 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
223222cnveqd 5863 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
224223imaeq1d 6063 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
225 eqid 2763 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ ↦ (𝐹𝑥)) = (𝑥 ∈ ℝ ↦ (𝐹𝑥))
226225mptpreima 6241 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))}
227224, 226eqtrdi 2814 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
228227ad3antrrr 742 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
229221, 228eqtr4d 2801 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
230 itg2addnc.f1 . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ MblFn)
231 mbfima 25770 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
232230, 4, 231syl2anc 595 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
233232ad3antrrr 742 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
234229, 233eqeltrd 2863 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
23545sseld 3937 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → (𝑡 ∈ ran 𝑡 ∈ ℝ))
236235ad2antlr 739 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ ran 𝑡 ∈ ℝ))
237236imdistani 578 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ))
238 i1fmbf 25815 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 ∈ MblFn)
239238, 27jca 520 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ( ∈ MblFn ∧ :ℝ⟶ℝ))
240239ad2antlr 739 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ( ∈ MblFn ∧ :ℝ⟶ℝ))
241 mbfimasn 25772 . . . . . . . . . . . . . . . 16 (( ∈ MblFn ∧ :ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
2422413expa 1136 . . . . . . . . . . . . . . 15 ((( ∈ MblFn ∧ :ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
243240, 242sylan 591 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
244237, 243syl 18 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ( “ {𝑡}) ∈ dom vol)
245 inmbl 25682 . . . . . . . . . . . . 13 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol ∧ ( “ {𝑡}) ∈ dom vol) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
246234, 244, 245syl2anc 595 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
247189, 246eqeltrd 2863 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
248247ralrimiva 3157 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
249 finiunmbl 25684 . . . . . . . . . 10 ((ran ∈ Fin ∧ ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
25041, 248, 249syl2anc 595 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
251172, 250eqeltrrd 2864 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
252 unrab 4269 . . . . . . . . . . 11 ({𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}) = {𝑥 ∈ ℝ ∣ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))}
25327feqmptd 6951 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 = (𝑥 ∈ ℝ ↦ (𝑥)))
254253cnveqd 5863 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 = (𝑥 ∈ ℝ ↦ (𝑥)))
255254imaeq1d 6063 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → ( “ (-∞(,)0)) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ (-∞(,)0)))
256 eqid 2763 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ (𝑥)) = (𝑥 ∈ ℝ ↦ (𝑥))
257256mptpreima 6241 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ↦ (𝑥)) “ (-∞(,)0)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)}
258255, 257eqtrdi 2814 . . . . . . . . . . . 12 ( ∈ dom ∫1 → ( “ (-∞(,)0)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)})
259254imaeq1d 6063 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → ( “ (0(,)+∞)) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ (0(,)+∞)))
260256mptpreima 6241 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ↦ (𝑥)) “ (0(,)+∞)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}
261259, 260eqtrdi 2814 . . . . . . . . . . . 12 ( ∈ dom ∫1 → ( “ (0(,)+∞)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)})
262258, 261uneq12d 4124 . . . . . . . . . . 11 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) = ({𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}))
26327ffvelcdmda 7081 . . . . . . . . . . . . 13 (( ∈ dom ∫1𝑥 ∈ ℝ) → (𝑥) ∈ ℝ)
264 0re 11211 . . . . . . . . . . . . . . 15 0 ∈ ℝ
265 lttri2 11293 . . . . . . . . . . . . . . 15 (((𝑥) ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥) ≠ 0 ↔ ((𝑥) < 0 ∨ 0 < (𝑥))))
266264, 265mpan2 703 . . . . . . . . . . . . . 14 ((𝑥) ∈ ℝ → ((𝑥) ≠ 0 ↔ ((𝑥) < 0 ∨ 0 < (𝑥))))
267 ibar 537 . . . . . . . . . . . . . . 15 ((𝑥) ∈ ℝ → (((𝑥) < 0 ∨ 0 < (𝑥)) ↔ ((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥)))))
268 andi 1025 . . . . . . . . . . . . . . . 16 (((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥))) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
269 0xr 11257 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
270 elioomnf 13472 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ* → ((𝑥) ∈ (-∞(,)0) ↔ ((𝑥) ∈ ℝ ∧ (𝑥) < 0)))
271 elioopnf 13471 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ* → ((𝑥) ∈ (0(,)+∞) ↔ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
272270, 271orbi12d 931 . . . . . . . . . . . . . . . . 17 (0 ∈ ℝ* → (((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥)))))
273269, 272ax-mp 5 . . . . . . . . . . . . . . . 16 (((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
274268, 273bitr4i 281 . . . . . . . . . . . . . . 15 (((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥))) ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)))
275267, 274bitrdi 290 . . . . . . . . . . . . . 14 ((𝑥) ∈ ℝ → (((𝑥) < 0 ∨ 0 < (𝑥)) ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
276266, 275bitrd 282 . . . . . . . . . . . . 13 ((𝑥) ∈ ℝ → ((𝑥) ≠ 0 ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
277263, 276syl 18 . . . . . . . . . . . 12 (( ∈ dom ∫1𝑥 ∈ ℝ) → ((𝑥) ≠ 0 ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
278277rabbidva 3422 . . . . . . . . . . 11 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} = {𝑥 ∈ ℝ ∣ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))})
279252, 262, 2783eqtr4a 2824 . . . . . . . . . 10 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) = {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0})
280 i1fima 25818 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ (-∞(,)0)) ∈ dom vol)
281 i1fima 25818 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ (0(,)+∞)) ∈ dom vol)
282 unmbl 25677 . . . . . . . . . . 11 ((( “ (-∞(,)0)) ∈ dom vol ∧ ( “ (0(,)+∞)) ∈ dom vol) → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) ∈ dom vol)
283280, 281, 282syl2anc 595 . . . . . . . . . 10 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) ∈ dom vol)
284279, 283eqeltrrd 2864 . . . . . . . . 9 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol)
285284ad2antlr 739 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol)
286 inmbl 25682 . . . . . . . 8 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
287251, 285, 286syl2anc 595 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
288287adantr 485 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
28923recnd 11238 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℂ)
290289adantlr 727 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℂ)
291 1cnd 11203 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
292 simplr 780 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℝ)
29313ad3antlr 743 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
29419ad3antlr 743 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
295292, 293, 294redivcld 12044 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
296295recnd 11238 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℂ)
297290, 291, 296subadd2d 11589 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
298 eqcom 2770 . . . . . . . . . 10 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ (𝑡 / (𝑣 / 3)) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1))
299 recn 11191 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
300299ad2antlr 739 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℂ)
30125recnd 11238 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℂ)
302301adantlr 727 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℂ)
30313recnd 11238 . . . . . . . . . . . 12 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℂ)
304303ad3antlr 743 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℂ)
305300, 302, 304, 294divmul3d 12026 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
306298, 305bitrid 286 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
307297, 306bitr3d 284 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
308307rabbidva 3422 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))})
309 imaundi 6149 . . . . . . . . . . 11 (𝐹 “ ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
310223ad4antr 744 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
311 zre 12596 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
312311adantl 486 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
31313ad3antlr 743 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ)
314312, 313remulcld 11240 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ)
315314rexrd 11260 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ*)
316 peano2z 12636 . . . . . . . . . . . . . . . . 17 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℤ)
317316zred 12701 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
318317adantl 486 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
319313, 318remulcld 11240 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
320319rexrd 11260 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ*)
321 zcn 12597 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℂ)
322321adantl 486 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℂ)
323303ad3antlr 743 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℂ)
324322, 323mulcomd 11231 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) = ((𝑣 / 3) · ((𝑡 / (𝑣 / 3)) + 1)))
32568ad3antlr 743 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ+)
326311ltp1d 12146 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) < (((𝑡 / (𝑣 / 3)) + 1) + 1))
327326adantl 486 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) < (((𝑡 / (𝑣 / 3)) + 1) + 1))
328312, 318, 325, 327ltmul2dd 13117 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · ((𝑡 / (𝑣 / 3)) + 1)) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))
329324, 328eqbrtrd 5134 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))
330 snunioo 13506 . . . . . . . . . . . . 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 1398 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))
332310, 331imaeq12d 6065 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
333309, 332eqtr3id 2812 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
334225mptpreima 6241 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))}
3354ad3antrrr 742 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → 𝐹:ℝ⟶ℝ)
336335ffvelcdmda 7081 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
3373363biant1d 1509 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
338337adantr 485 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
339311adantl 486 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
340336adantr 485 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹𝑥) ∈ ℝ)
34168ad4antlr 745 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ+)
342339, 340, 341lemuldivd 13110 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ ((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3))))
343317adantl 486 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
344340, 343, 341ltdivmuld 13112 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1) ↔ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))
345344bicomd 226 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ↔ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1)))
346342, 345anbi12d 643 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
347338, 346bitr3d 284 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
348 elico2 13438 . . . . . . . . . . . . . . . 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 595 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
350349adantlr 727 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
351 eqcom 2770 . . . . . . . . . . . . . . 15 (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1))
35221adantlr 727 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
353 flbi 13851 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
354352, 353sylan 591 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
355351, 354bitrid 286 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
356347, 350, 3553bitr4d 314 . . . . . . . . . . . . 13 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
357356an32s 664 . . . . . . . . . . . 12 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
358357rabbidva 3422 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))} = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
359334, 358eqtrid 2810 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
360333, 359eqtrd 2798 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
361230ad4antr 744 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹 ∈ MblFn)
3624ad4antr 744 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹:ℝ⟶ℝ)
363 mbfimasn 25772 . . . . . . . . . . 11 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ) → (𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∈ dom vol)
364361, 362, 314, 363syl3anc 1398 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∈ dom vol)
365 mbfima 25770 . . . . . . . . . . . 12 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
366230, 4, 365syl2anc 595 . . . . . . . . . . 11 (𝜑 → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
367366ad4antr 744 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
368 unmbl 25677 . . . . . . . . . 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 595 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) ∈ dom vol)
370360, 369eqeltrrd 2864 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
371 simpr 489 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
372352flcld 13833 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
373372adantr 485 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
374371, 373eqeltrd 2863 . . . . . . . . . . . . 13 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ)
375374stoic1a 1802 . . . . . . . . . . . 12 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
376375an32s 664 . . . . . . . . . . 11 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) ∧ 𝑥 ∈ ℝ) → ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
377376ralrimiva 3157 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ∀𝑥 ∈ ℝ ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
378 rabeq0 4346 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
379377, 378sylibr 237 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = ∅)
380 0mbl 25679 . . . . . . . . 9 ∅ ∈ dom vol
381379, 380eqeltrdi 2871 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
382370, 381pm2.61dan 824 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
383308, 382eqeltrrd 2864 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))} ∈ dom vol)
384 inmbl 25682 . . . . . 6 ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))} ∈ dom vol) → (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∈ dom vol)
385288, 383, 384syl2anc 595 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∈ dom vol)
386 rabiun 38222 . . . . . . . . . . 11 {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)}
387 rabeq 3430 . . . . . . . . . . . 12 ( 𝑡 ∈ ran ( “ {𝑡}) = ℝ → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
388168, 387syl 18 . . . . . . . . . . 11 ( ∈ dom ∫1 → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
389386, 388eqtr3id 2812 . . . . . . . . . 10 ( ∈ dom ∫1 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
390389ad2antlr 739 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
391176notbid 321 . . . . . . . . . . . . . . 15 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
392391rabbidva 3422 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
393 inrab2 4271 . . . . . . . . . . . . . . 15 ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡}
394 rabeq 3430 . . . . . . . . . . . . . . . 16 ((ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}) → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
395184, 394syl 18 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
396393, 395eqtrid 2810 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
397392, 396eqtr4d 2801 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
398397ad3antlr 743 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
399 imaundi 6149 . . . . . . . . . . . . . . . . 17 (𝐹 “ ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)))
40013, 19jca 520 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 ∈ ℝ+ → ((𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0))
401 redivcl 11935 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑡 ∈ ℝ ∧ (𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
4024013expb 1138 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ ℝ ∧ ((𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0)) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
403400, 402sylan2 604 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℝ ∧ 𝑣 ∈ ℝ+) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
404403ancoms 463 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
405404adantll 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
406405, 203syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
407 peano2re 11384 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
408 reflcl 13831 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
409406, 407, 4083syl 19 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
41013ad2antlr 739 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
411409, 410remulcld 11240 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ)
412411rexrd 11260 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ*)
413 pnfxr 11264 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
414413a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → +∞ ∈ ℝ*)
415 ltpnf 13146 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) < +∞)
416411, 415syl 18 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) < +∞)
417 snunioo 13506 . . . . . . . . . . . . . . . . . . 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 1398 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) = (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞))
419418imaeq2d 6064 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
420399, 419eqtr3id 2812 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
421223imaeq1d 6063 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
422225mptpreima 6241 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)}
423421, 422eqtrdi 2814 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)})
424423ad3antrrr 742 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)})
425406, 407syl 18 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
426425adantr 485 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
427 flflp1 13842 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ ∧ ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3)) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
428426, 352, 427syl2anc 595 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3)) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
429411adantr 485 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ)
430 elicopnf 13473 . . . . . . . . . . . . . . . . . . . . . 22 (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
431429, 430syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
432336biantrurd 541 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
433409adantr 485 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
43468ad3antlr 743 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
435433, 336, 434lemuldivd 13110 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3))))
436431, 432, 4353bitr2d 310 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3))))
437406adantr 485 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
438352, 22syl 18 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
439 1red 11210 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
440437, 438, 439ltadd1d 11808 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
441428, 436, 4403bitr4d 314 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
442295, 439, 438ltaddsubd 11815 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1)))
443441, 442bitrd 282 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ (𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1)))
444438, 24syl 18 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
445292, 444, 434ltdivmul2d 13113 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ↔ 𝑡 < (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
446444, 293remulcld 11240 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ)
447292, 446ltnled 11358 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 < (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
448443, 445, 4473bitrd 308 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
449448rabbidva 3422 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
450420, 424, 4493eqtrd 2802 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
451230ad3antrrr 742 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → 𝐹 ∈ MblFn)
452 mbfimasn 25772 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ) → (𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∈ dom vol)
453451, 335, 411, 452syl3anc 1398 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∈ dom vol)
454 mbfima 25770 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
455230, 4, 454syl2anc 595 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
456455ad3antrrr 742 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
457 unmbl 25677 . . . . . . . . . . . . . . . 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 595 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) ∈ dom vol)
459450, 458eqeltrrd 2864 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
460237, 459syl 18 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
461 inmbl 25682 . . . . . . . . . . . . 13 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol ∧ ( “ {𝑡}) ∈ dom vol) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
462460, 244, 461syl2anc 595 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
463398, 462eqeltrd 2863 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
464463ralrimiva 3157 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
465 finiunmbl 25684 . . . . . . . . . 10 ((ran ∈ Fin ∧ ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
46641, 464, 465syl2anc 595 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
467390, 466eqeltrrd 2864 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
468254imaeq1d 6063 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ {0}) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}))
469256mptpreima 6241 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}
470140elsn 4605 . . . . . . . . . . . . 13 ((𝑥) ∈ {0} ↔ (𝑥) = 0)
471470rabbii 3421 . . . . . . . . . . . 12 {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}} = {𝑥 ∈ ℝ ∣ (𝑥) = 0}
472469, 471eqtri 2786 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) = 0}
473468, 472eqtrdi 2814 . . . . . . . . . 10 ( ∈ dom ∫1 → ( “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) = 0})
474 i1fima 25818 . . . . . . . . . 10 ( ∈ dom ∫1 → ( “ {0}) ∈ dom vol)
475473, 474eqeltrrd 2864 . . . . . . . . 9 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol)
476475ad2antlr 739 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol)
477 unmbl 25677 . . . . . . . 8 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
478467, 476, 477syl2anc 595 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
479478adantr 485 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
480254imaeq1d 6063 . . . . . . . . 9 ( ∈ dom ∫1 → ( “ {𝑡}) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}))
481256mptpreima 6241 . . . . . . . . . 10 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {𝑡}}
482140elsn 4605 . . . . . . . . . . . 12 ((𝑥) ∈ {𝑡} ↔ (𝑥) = 𝑡)
483 eqcom 2770 . . . . . . . . . . . 12 ((𝑥) = 𝑡𝑡 = (𝑥))
484482, 483bitri 278 . . . . . . . . . . 11 ((𝑥) ∈ {𝑡} ↔ 𝑡 = (𝑥))
485484rabbii 3421 . . . . . . . . . 10 {𝑥 ∈ ℝ ∣ (𝑥) ∈ {𝑡}} = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}
486481, 485eqtri 2786 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}
487480, 486eqtrdi 2814 . . . . . . . 8 ( ∈ dom ∫1 → ( “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
488487ad3antlr 743 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
489488, 243eqeltrrd 2864 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)} ∈ dom vol)
490 inmbl 25682 . . . . . 6 ((({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)} ∈ dom vol) → (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) ∈ dom vol)
491479, 489, 490syl2anc 595 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) ∈ dom vol)
492 unmbl 25677 . . . . 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 595 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})) ∈ dom vol)
494159, 493syl 18 . . 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 2867 . 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 25670 . . . 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 18 . . 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 4754 . . . . . 6 (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) ↔ (𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∧ 𝑡 ≠ 0))
499157anim1d 622 . . . . . 6 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ((𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∧ 𝑡 ≠ 0) → (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
500498, 499biimtrid 245 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
501500imdistani 578 . . . 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 2814 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}})
504502, 503ineq12d 4175 . . . . . . . . . 10 ( ∈ dom ∫1 → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ({𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}))
505 inrab 4270 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})}
506504, 505eqtrdi 2814 . . . . . . . . 9 ( ∈ dom ∫1 → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})})
507506ad3antlr 743 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})})
508144biimpri 231 . . . . . . . . . . . . . . . . . 18 ((𝑥) = 0 → ¬ (𝑥) ≠ 0)
509508intnand 493 . . . . . . . . . . . . . . . . 17 ((𝑥) = 0 → ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0))
510509iffalsed 4499 . . . . . . . . . . . . . . . 16 ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = (𝑥))
511 eqtr 2783 . . . . . . . . . . . . . . . 16 ((if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = (𝑥) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
512510, 511mpancom 700 . . . . . . . . . . . . . . 15 ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
513512adantl 486 . . . . . . . . . . . . . 14 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
514 simpll 778 . . . . . . . . . . . . . . 15 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → 𝑡 ≠ 0)
515514necomd 3013 . . . . . . . . . . . . . 14 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → 0 ≠ 𝑡)
516513, 515eqnetrd 3025 . . . . . . . . . . . . 13 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡)
517516ex 417 . . . . . . . . . . . 12 ((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) → ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
518 orcom 883 . . . . . . . . . . . . . 14 ((¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∨ ¬ (𝑥) ∈ {0}) ↔ (¬ (𝑥) ∈ {0} ∨ ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
519 ianor 997 . . . . . . . . . . . . . 14 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ (¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∨ ¬ (𝑥) ∈ {0}))
520 imor 866 . . . . . . . . . . . . . 14 (((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}) ↔ (¬ (𝑥) ∈ {0} ∨ ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
521518, 519, 5203bitr4i 306 . . . . . . . . . . . . 13 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ ((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
522142necon3bbii 3005 . . . . . . . . . . . . . 14 (¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡)
523470, 522imbi12i 353 . . . . . . . . . . . . 13 (((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}) ↔ ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
524521, 523bitri 278 . . . . . . . . . . . 12 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
525517, 524sylibr 237 . . . . . . . . . . 11 ((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) → ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
526525ralrimiva 3157 . . . . . . . . . 10 (𝑡 ≠ 0 → ∀𝑥 ∈ ℝ ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
527 rabeq0 4346 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
528526, 527sylibr 237 . . . . . . . . 9 (𝑡 ≠ 0 → {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅)
529528ad2antll 741 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅)
530507, 529eqtrd 2798 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ∅)
531 imassrn 6075 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
532 dfdm4 5887 . . . . . . . . . 10 dom (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
533141, 127dmmpti 6681 . . . . . . . . . 10 dom (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ℝ
534532, 533eqtr3i 2788 . . . . . . . . 9 ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ℝ
535531, 534sseqtri 3986 . . . . . . . 8 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ℝ
536 reldisj 4414 . . . . . . . 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 221 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ (ℝ ∖ ( “ {0})))
539 ffun 6710 . . . . . . . . . 10 (:ℝ⟶ℝ → Fun )
540 difpreima 7062 . . . . . . . . . 10 (Fun → ( “ (ran ∖ {0})) = (( “ ran ) ∖ ( “ {0})))
541539, 540syl 18 . . . . . . . . 9 (:ℝ⟶ℝ → ( “ (ran ∖ {0})) = (( “ ran ) ∖ ( “ {0})))
542 fdm 6717 . . . . . . . . . . 11 (:ℝ⟶ℝ → dom = ℝ)
543161, 542eqtrid 2810 . . . . . . . . . 10 (:ℝ⟶ℝ → ( “ ran ) = ℝ)
544543difeq1d 4081 . . . . . . . . 9 (:ℝ⟶ℝ → (( “ ran ) ∖ ( “ {0})) = (ℝ ∖ ( “ {0})))
545541, 544eqtrd 2798 . . . . . . . 8 (:ℝ⟶ℝ → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
54627, 545syl 18 . . . . . . 7 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
547546ad3antlr 743 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
548538, 547sseqtrrd 3975 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ( “ (ran ∖ {0})))
549 imassrn 6075 . . . . . . 7 ( “ (ran ∖ {0})) ⊆ ran
550549, 181sseqtrid 3980 . . . . . 6 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) ⊆ ℝ)
551550ad3antlr 743 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ( “ (ran ∖ {0})) ⊆ ℝ)
552 i1fima 25818 . . . . . . . 8 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) ∈ dom vol)
553 mblvol 25670 . . . . . . . 8 (( “ (ran ∖ {0})) ∈ dom vol → (vol‘( “ (ran ∖ {0}))) = (vol*‘( “ (ran ∖ {0}))))
554552, 553syl 18 . . . . . . 7 ( ∈ dom ∫1 → (vol‘( “ (ran ∖ {0}))) = (vol*‘( “ (ran ∖ {0}))))
555 neldifsn 4761 . . . . . . . 8 ¬ 0 ∈ (ran ∖ {0})
556 i1fima2 25819 . . . . . . . 8 (( ∈ dom ∫1 ∧ ¬ 0 ∈ (ran ∖ {0})) → (vol‘( “ (ran ∖ {0}))) ∈ ℝ)
557555, 556mpan2 703 . . . . . . 7 ( ∈ dom ∫1 → (vol‘( “ (ran ∖ {0}))) ∈ ℝ)
558554, 557eqeltrrd 2864 . . . . . 6 ( ∈ dom ∫1 → (vol*‘( “ (ran ∖ {0}))) ∈ ℝ)
559558ad3antlr 743 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (vol*‘( “ (ran ∖ {0}))) ∈ ℝ)
560 ovolsscl 25626 . . . . 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 1398 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
562501, 561syl 18 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
563497, 562eqeltrd 2863 . 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 25821 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 209  wa 400  wo 860  w3a 1103   = wceq 1570  wex 1809  wcel 2143  wne 2958  wral 3079  wrex 3089  {crab 3416  Vcvv 3455  cdif 3903  cun 3904  cin 3905  wss 3906  c0 4287  ifcif 4488  {csn 4590   ciun 4957   class class class wbr 5110  cmpt 5193  ccnv 5662  dom cdm 5663  ran crn 5664  cima 5666  Fun wfun 6532   Fn wfn 6533  wf 6534  ontowfo 6536  cfv 6538  (class class class)co 7412  Fincfn 8944  supcsup 9401  cc 11099  cr 11100  0cc0 11101  1c1 11102   + caddc 11104   · cmul 11106  +∞cpnf 11241  -∞cmnf 11242  *cxr 11243   < clt 11244  cle 11245  cmin 11442  -cneg 11443   / cdiv 11872  cn 12234  3c3 12297  0cn0 12505  cz 12592  +crp 13017  (,)cioo 13373  [,)cico 13375  ...cfz 13536  cfl 13825  vol*covol 25602  volcvol 25603  MblFncmbf 25754  1citg1 25755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-inf2 9611  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178  ax-pre-sup 11179
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-int 4914  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7676  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-1o 8454  df-2o 8455  df-er 8695  df-map 8827  df-pm 8828  df-en 8945  df-dom 8946  df-sdom 8947  df-fin 8948  df-fi 9372  df-sup 9403  df-inf 9404  df-oi 9473  df-dju 9888  df-card 9926  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-div 11873  df-nn 12235  df-2 12304  df-3 12305  df-n0 12506  df-z 12593  df-uz 12864  df-q 12974  df-rp 13018  df-xneg 13138  df-xadd 13139  df-xmul 13140  df-ioo 13377  df-ico 13379  df-icc 13380  df-fz 13537  df-fzo 13685  df-fl 13827  df-seq 14040  df-exp 14100  df-hash 14369  df-cj 15152  df-re 15153  df-im 15154  df-sqrt 15288  df-abs 15289  df-clim 15541  df-sum 15740  df-rest 17476  df-topgen 17497  df-psmet 21495  df-xmet 21496  df-met 21497  df-bl 21498  df-mopn 21499  df-top 23032  df-topon 23049  df-bases 23084  df-cmp 23525  df-ovol 25604  df-vol 25605  df-mbf 25759  df-itg1 25760
This theorem is referenced by:  itg2addnclem3  38302
  Copyright terms: Public domain W3C validator