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 37732
Description: Lemma for itg2addnc 37734. 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 13358 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ
3 fss 6672 . . . . . . . . . . 11 ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
41, 2, 3sylancl 586 . . . . . . . . . 10 (𝜑𝐹:ℝ⟶ℝ)
54ad2antrr 726 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝐹:ℝ⟶ℝ)
65ffvelcdmda 7023 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
7 rpre 12901 . . . . . . . . . 10 (𝑣 ∈ ℝ+𝑣 ∈ ℝ)
8 3re 12212 . . . . . . . . . . 11 3 ∈ ℝ
9 3ne0 12238 . . . . . . . . . . 11 3 ≠ 0
108, 9pm3.2i 470 . . . . . . . . . 10 (3 ∈ ℝ ∧ 3 ≠ 0)
11 redivcl 11847 . . . . . . . . . . 11 ((𝑣 ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (𝑣 / 3) ∈ ℝ)
12113expb 1120 . . . . . . . . . 10 ((𝑣 ∈ ℝ ∧ (3 ∈ ℝ ∧ 3 ≠ 0)) → (𝑣 / 3) ∈ ℝ)
137, 10, 12sylancl 586 . . . . . . . . 9 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℝ)
1413ad2antlr 727 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
15 rpcnne0 12911 . . . . . . . . . 10 (𝑣 ∈ ℝ+ → (𝑣 ∈ ℂ ∧ 𝑣 ≠ 0))
16 3cn 12213 . . . . . . . . . . 11 3 ∈ ℂ
1716, 9pm3.2i 470 . . . . . . . . . 10 (3 ∈ ℂ ∧ 3 ≠ 0)
18 divne0 11795 . . . . . . . . . 10 (((𝑣 ∈ ℂ ∧ 𝑣 ≠ 0) ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (𝑣 / 3) ≠ 0)
1915, 17, 18sylancl 586 . . . . . . . . 9 (𝑣 ∈ ℝ+ → (𝑣 / 3) ≠ 0)
2019ad2antlr 727 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
216, 14, 20redivcld 11956 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
22 reflcl 13702 . . . . . . 7 (((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
2321, 22syl 17 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
24 peano2rem 11435 . . . . . 6 ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
2523, 24syl 17 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
2625, 14remulcld 11149 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ)
27 i1ff 25605 . . . . . 6 ( ∈ dom ∫1:ℝ⟶ℝ)
2827ad2antlr 727 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → :ℝ⟶ℝ)
2928ffvelcdmda 7023 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ ℝ)
3026, 29ifcld 4521 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ ℝ)
3130fmpttd 7054 . 2 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))):ℝ⟶ℝ)
32 fzfi 13881 . . . . 5 (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ∈ Fin
33 ovex 7385 . . . . . . 7 ((𝑡 − 1) · (𝑣 / 3)) ∈ V
34 eqid 2733 . . . . . . 7 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) = (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3)))
3533, 34fnmpti 6629 . . . . . 6 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) Fn (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
36 dffn4 6746 . . . . . 6 ((𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) Fn (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↔ (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))):(0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))–onto→ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))))
3735, 36mpbi 230 . . . . 5 (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))):(0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))–onto→ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3)))
38 fofi 9204 . . . . 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 692 . . . 4 ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∈ Fin
40 i1frn 25606 . . . . 5 ( ∈ dom ∫1 → ran ∈ Fin)
4140ad2antlr 727 . . . 4 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran ∈ Fin)
42 unfi 9087 . . . 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 587 . . 3 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ) ∈ Fin)
44 0zd 12487 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → 0 ∈ ℤ)
4527frnd 6664 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ran ⊆ ℝ)
46 i1f0rn 25611 . . . . . . . . . . . . . . . . . 18 ( ∈ dom ∫1 → 0 ∈ ran )
47 elex2 2810 . . . . . . . . . . . . . . . . . 18 (0 ∈ ran → ∃𝑥 𝑥 ∈ ran )
4846, 47syl 17 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → ∃𝑥 𝑥 ∈ ran )
49 n0 4302 . . . . . . . . . . . . . . . . 17 (ran ≠ ∅ ↔ ∃𝑥 𝑥 ∈ ran )
5048, 49sylibr 234 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ran ≠ ∅)
51 fimaxre2 12074 . . . . . . . . . . . . . . . . 17 ((ran ⊆ ℝ ∧ ran ∈ Fin) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥)
5245, 40, 51syl2anc 584 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥)
53 suprcl 12089 . . . . . . . . . . . . . . . 16 ((ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥) → sup(ran , ℝ, < ) ∈ ℝ)
5445, 50, 52, 53syl3anc 1373 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → sup(ran , ℝ, < ) ∈ ℝ)
5554ad3antlr 731 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → sup(ran , ℝ, < ) ∈ ℝ)
5655, 14, 20redivcld 11956 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (sup(ran , ℝ, < ) / (𝑣 / 3)) ∈ ℝ)
57 peano2re 11293 . . . . . . . . . . . . 13 ((sup(ran , ℝ, < ) / (𝑣 / 3)) ∈ ℝ → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ)
5856, 57syl 17 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ)
59 ceicl 13747 . . . . . . . . . . . 12 (((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
6058, 59syl 17 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
6160adantr 480 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℤ)
6221flcld 13704 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
6362adantr 480 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
64 3nn 12211 . . . . . . . . . . . . . . . . 17 3 ∈ ℕ
65 nnrp 12904 . . . . . . . . . . . . . . . . 17 (3 ∈ ℕ → 3 ∈ ℝ+)
6664, 65ax-mp 5 . . . . . . . . . . . . . . . 16 3 ∈ ℝ+
67 rpdivcl 12919 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ℝ+ ∧ 3 ∈ ℝ+) → (𝑣 / 3) ∈ ℝ+)
6866, 67mpan2 691 . . . . . . . . . . . . . . 15 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℝ+)
6968ad2antlr 727 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
701ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝐹:ℝ⟶(0[,)+∞))
7170ffvelcdmda 7023 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ (0[,)+∞))
72 elrege0 13356 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) ∈ (0[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
7371, 72sylib 218 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ℝ ∧ 0 ≤ (𝐹𝑥)))
7473simprd 495 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹𝑥))
756, 69, 74divge0d 12976 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ ((𝐹𝑥) / (𝑣 / 3)))
76 flge0nn0 13726 . . . . . . . . . . . . 13 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ 0 ≤ ((𝐹𝑥) / (𝑣 / 3))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℕ0)
7721, 75, 76syl2anc 584 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℕ0)
7877nn0ge0d 12452 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 0 ≤ (⌊‘((𝐹𝑥) / (𝑣 / 3))))
7978adantr 480 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → 0 ≤ (⌊‘((𝐹𝑥) / (𝑣 / 3))))
8045, 50, 523jca 1128 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → (ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥))
8180ad3antlr 731 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥))
82 ffn 6656 . . . . . . . . . . . . . . . . . 18 (:ℝ⟶ℝ → Fn ℝ)
8327, 82syl 17 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 Fn ℝ)
84 dffn3 6668 . . . . . . . . . . . . . . . . 17 ( Fn ℝ ↔ :ℝ⟶ran )
8583, 84sylib 218 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1:ℝ⟶ran )
8685ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → :ℝ⟶ran )
8786ffvelcdmda 7023 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ ran )
88 suprub 12090 . . . . . . . . . . . . . 14 (((ran ⊆ ℝ ∧ ran ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran 𝑦𝑥) ∧ (𝑥) ∈ ran ) → (𝑥) ≤ sup(ran , ℝ, < ))
8981, 87, 88syl2anc 584 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ≤ sup(ran , ℝ, < ))
90 letr 11214 . . . . . . . . . . . . . . 15 (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ ∧ (𝑥) ∈ ℝ ∧ sup(ran , ℝ, < ) ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < )))
9126, 29, 55, 90syl3anc 1373 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < )))
9225, 55, 69lemuldivd 12985 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) ↔ ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (sup(ran , ℝ, < ) / (𝑣 / 3))))
93 1red 11120 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
9423, 93, 56lesubaddd 11721 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (sup(ran , ℝ, < ) / (𝑣 / 3)) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
9592, 94bitrd 279 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
96 ceige 13750 . . . . . . . . . . . . . . . . 17 (((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∈ ℝ → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
9758, 96syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
9860zred 12583 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)) ∈ ℝ)
99 letr 11214 . . . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ∧ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10197, 100mpan2d 694 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10295, 101sylbid 240 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ sup(ran , ℝ, < ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10391, 102syld 47 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≤ sup(ran , ℝ, < )) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
10489, 103mpan2d 694 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
105104adantrd 491 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
106105imp 406 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ -(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))
10744, 61, 63, 79, 106elfzd 13417 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))))
108 eqid 2733 . . . . . . . . 9 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))
109 oveq1 7359 . . . . . . . . . . 11 (𝑡 = (⌊‘((𝐹𝑥) / (𝑣 / 3))) → (𝑡 − 1) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1))
110109oveq1d 7367 . . . . . . . . . 10 (𝑡 = (⌊‘((𝐹𝑥) / (𝑣 / 3))) → ((𝑡 − 1) · (𝑣 / 3)) = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))
111110rspceeqv 3596 . . . . . . . . 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 586 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3)))
113 ovex 7385 . . . . . . . . 9 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ V
11434elrnmpt 5902 . . . . . . . . 9 ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ V → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ↔ ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3))))
115113, 114ax-mp 5 . . . . . . . 8 ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ↔ ∃𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1)))(((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) = ((𝑡 − 1) · (𝑣 / 3)))
116112, 115sylibr 234 . . . . . . 7 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))))
117 elun1 4131 . . . . . . 7 ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
118116, 117syl 17 . . . . . 6 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
119 elun2 4132 . . . . . . . 8 ((𝑥) ∈ ran → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
12087, 119syl 17 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
121120adantr 480 . . . . . 6 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) ∧ ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)) → (𝑥) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
122118, 121ifclda 4510 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
123122fmpttd 7054 . . . 4 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))):ℝ⟶(ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
124123frnd 6664 . . 3 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ⊆ (ran (𝑡 ∈ (0...-(⌊‘-((sup(ran , ℝ, < ) / (𝑣 / 3)) + 1))) ↦ ((𝑡 − 1) · (𝑣 / 3))) ∪ ran ))
125 ssfi 9089 . . 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 584 . 2 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∈ Fin)
127 eqid 2733 . . . . 5 (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
128127mptpreima 6190 . . . 4 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}}
129 unrab 4264 . . . . 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 4265 . . . . . . . 8 ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) = {𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)}
131130ineq1i 4165 . . . . . . 7 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = ({𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))})
132 inrab 4265 . . . . . . 7 ({𝑥 ∈ ℝ ∣ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = {𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))}
133131, 132eqtri 2756 . . . . . 6 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) = {𝑥 ∈ ℝ ∣ (((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)))}
134 unrab 4264 . . . . . . . 8 ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) = {𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)}
135134ineq1i 4165 . . . . . . 7 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = ({𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
136 inrab 4265 . . . . . . 7 ({𝑥 ∈ ℝ ∣ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0)} ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))}
137135, 136eqtri 2756 . . . . . 6 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) = {𝑥 ∈ ℝ ∣ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))}
138133, 137uneq12i 4115 . . . . 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 2740 . . . . . . 7 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 𝑡𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
140 fvex 6841 . . . . . . . . 9 (𝑥) ∈ V
141113, 140ifex 4525 . . . . . . . 8 if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ V
142141elsn 4590 . . . . . . 7 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 𝑡)
143 ianor 983 . . . . . . . . . . 11 (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ↔ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ ¬ (𝑥) ≠ 0))
144 nne 2933 . . . . . . . . . . . 12 (¬ (𝑥) ≠ 0 ↔ (𝑥) = 0)
145144orbi2i 912 . . . . . . . . . . 11 ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ ¬ (𝑥) ≠ 0) ↔ (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0))
146143, 145bitr2i 276 . . . . . . . . . 10 ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ↔ ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0))
147146anbi1i 624 . . . . . . . . 9 (((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥)) ↔ (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (𝑥)))
148147orbi2i 912 . . . . . . . 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 4516 . . . . . . . 8 (𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ↔ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ (¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (𝑥))))
150148, 149bitr4i 278 . . . . . . 7 (((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))) ↔ 𝑡 = if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
151139, 142, 1503bitr4i 303 . . . . . 6 (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥))))
152151rabbii 3401 . . . . 5 {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} = {𝑥 ∈ ℝ ∣ ((((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0) ∧ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))) ∨ ((¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∨ (𝑥) = 0) ∧ 𝑡 = (𝑥)))}
153129, 138, 1523eqtr4ri 2767 . . . 4 {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} = ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}))
154128, 153eqtri 2756 . . 3 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}))
155 eldifi 4080 . . . . . 6 (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → 𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))))
15631frnd 6664 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ⊆ ℝ)
157156sseld 3929 . . . . . 6 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) → 𝑡 ∈ ℝ))
158155, 157syl5 34 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → 𝑡 ∈ ℝ))
159158imdistani 568 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ))
160 rabiun 37653 . . . . . . . . . 10 {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)}
161 cnvimarndm 6036 . . . . . . . . . . . . . 14 ( “ ran ) = dom
162 iunid 5011 . . . . . . . . . . . . . . . 16 𝑡 ∈ ran {𝑡} = ran
163162imaeq2i 6011 . . . . . . . . . . . . . . 15 ( 𝑡 ∈ ran {𝑡}) = ( “ ran )
164 imaiun 7185 . . . . . . . . . . . . . . 15 ( 𝑡 ∈ ran {𝑡}) = 𝑡 ∈ ran ( “ {𝑡})
165163, 164eqtr3i 2758 . . . . . . . . . . . . . 14 ( “ ran ) = 𝑡 ∈ ran ( “ {𝑡})
166161, 165eqtr3i 2758 . . . . . . . . . . . . 13 dom = 𝑡 ∈ ran ( “ {𝑡})
16727fdmd 6666 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → dom = ℝ)
168166, 167eqtr3id 2782 . . . . . . . . . . . 12 ( ∈ dom ∫1 𝑡 ∈ ran ( “ {𝑡}) = ℝ)
169168ad2antlr 727 . . . . . . . . . . 11 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran ( “ {𝑡}) = ℝ)
170 rabeq 3410 . . . . . . . . . . 11 ( 𝑡 ∈ ran ( “ {𝑡}) = ℝ → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
171169, 170syl 17 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
172160, 171eqtr3id 2782 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
173 fniniseg 6999 . . . . . . . . . . . . . . . . . 18 ( Fn ℝ → (𝑥 ∈ ( “ {𝑡}) ↔ (𝑥 ∈ ℝ ∧ (𝑥) = 𝑡)))
17427, 82, 1733syl 18 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → (𝑥 ∈ ( “ {𝑡}) ↔ (𝑥 ∈ ℝ ∧ (𝑥) = 𝑡)))
175174simplbda 499 . . . . . . . . . . . . . . . 16 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → (𝑥) = 𝑡)
176175breq2d 5105 . . . . . . . . . . . . . . 15 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ↔ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
177176rabbidva 3402 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
178 inrab2 4266 . . . . . . . . . . . . . . 15 ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡}
179 imassrn 6024 . . . . . . . . . . . . . . . . . 18 ( “ {𝑡}) ⊆ ran
180 dfdm4 5839 . . . . . . . . . . . . . . . . . . 19 dom = ran
181180, 167eqtr3id 2782 . . . . . . . . . . . . . . . . . 18 ( ∈ dom ∫1 → ran = ℝ)
182179, 181sseqtrid 3973 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 → ( “ {𝑡}) ⊆ ℝ)
183 sseqin2 4172 . . . . . . . . . . . . . . . . 17 (( “ {𝑡}) ⊆ ℝ ↔ (ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}))
184182, 183sylib 218 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → (ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}))
185 rabeq 3410 . . . . . . . . . . . . . . . 16 ((ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}) → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
186184, 185syl 17 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
187178, 186eqtrid 2780 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
188177, 187eqtr4d 2771 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
189188ad3antlr 731 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
19025adantlr 715 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
19145ad2antlr 727 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ran ⊆ ℝ)
192191sselda 3930 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → 𝑡 ∈ ℝ)
193192adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℝ)
19468ad3antlr 731 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
195190, 193, 194lemuldivd 12985 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡 ↔ ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (𝑡 / (𝑣 / 3))))
19623adantlr 715 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
197 1red 11120 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
19813ad3antlr 731 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
19919ad3antlr 731 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
200193, 198, 199redivcld 11956 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
201196, 197, 200lesubaddd 11721 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ≤ (𝑡 / (𝑣 / 3)) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1)))
2026adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
203 peano2re 11293 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 / (𝑣 / 3)) ∈ ℝ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
204200, 203syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
205 reflcl 13702 . . . . . . . . . . . . . . . . . . . . 21 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ → (⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ)
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ)
207 peano2re 11293 . . . . . . . . . . . . . . . . . . . 20 ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) ∈ ℝ → ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ∈ ℝ)
208206, 207syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ∈ ℝ)
209202, 208, 194ltdivmuld 12987 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → (((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1) ↔ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))))
21021adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
211 flflp1 13713 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ ((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))
212210, 204, 211syl2anc 584 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ ((𝐹𝑥) / (𝑣 / 3)) < ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))
213198, 208remulcld 11149 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ)
214213rexrd 11169 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ*)
215 elioomnf 13346 . . . . . . . . . . . . . . . . . . . 20 (((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ∈ ℝ* → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
216214, 215syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
217202biantrurd 532 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)) ↔ ((𝐹𝑥) ∈ ℝ ∧ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
218216, 217bitr4d 282 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))) ↔ (𝐹𝑥) < ((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1))))
219209, 212, 2183bitr4d 311 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) ≤ ((𝑡 / (𝑣 / 3)) + 1) ↔ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
220195, 201, 2193bitrd 305 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) ∧ 𝑥 ∈ ℝ) → ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡 ↔ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
221220rabbidva 3402 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
2221feqmptd 6896 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
223222cnveqd 5819 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
224223imaeq1d 6012 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
225 eqid 2733 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ ↦ (𝐹𝑥)) = (𝑥 ∈ ℝ ↦ (𝐹𝑥))
226225mptpreima 6190 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))}
227224, 226eqtrdi 2784 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
228227ad3antrrr 730 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))})
229221, 228eqtr4d 2771 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))))
230 itg2addnc.f1 . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ MblFn)
231 mbfima 25559 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
232230, 4, 231syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
233232ad3antrrr 730 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (𝐹 “ (-∞(,)((𝑣 / 3) · ((⌊‘((𝑡 / (𝑣 / 3)) + 1)) + 1)))) ∈ dom vol)
234229, 233eqeltrd 2833 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
23545sseld 3929 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → (𝑡 ∈ ran 𝑡 ∈ ℝ))
236235ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ ran 𝑡 ∈ ℝ))
237236imdistani 568 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ))
238 i1fmbf 25604 . . . . . . . . . . . . . . . . 17 ( ∈ dom ∫1 ∈ MblFn)
239238, 27jca 511 . . . . . . . . . . . . . . . 16 ( ∈ dom ∫1 → ( ∈ MblFn ∧ :ℝ⟶ℝ))
240239ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ( ∈ MblFn ∧ :ℝ⟶ℝ))
241 mbfimasn 25561 . . . . . . . . . . . . . . . 16 (( ∈ MblFn ∧ :ℝ⟶ℝ ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
2422413expa 1118 . . . . . . . . . . . . . . 15 ((( ∈ MblFn ∧ :ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
243240, 242sylan 580 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) ∈ dom vol)
244237, 243syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ( “ {𝑡}) ∈ dom vol)
245 inmbl 25471 . . . . . . . . . . . . 13 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol ∧ ( “ {𝑡}) ∈ dom vol) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
246234, 244, 245syl2anc 584 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
247189, 246eqeltrd 2833 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
248247ralrimiva 3125 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
249 finiunmbl 25473 . . . . . . . . . 10 ((ran ∈ Fin ∧ ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
25041, 248, 249syl2anc 584 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
251172, 250eqeltrrd 2834 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
252 unrab 4264 . . . . . . . . . . 11 ({𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}) = {𝑥 ∈ ℝ ∣ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))}
25327feqmptd 6896 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 = (𝑥 ∈ ℝ ↦ (𝑥)))
254253cnveqd 5819 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 = (𝑥 ∈ ℝ ↦ (𝑥)))
255254imaeq1d 6012 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → ( “ (-∞(,)0)) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ (-∞(,)0)))
256 eqid 2733 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ ↦ (𝑥)) = (𝑥 ∈ ℝ ↦ (𝑥))
257256mptpreima 6190 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ↦ (𝑥)) “ (-∞(,)0)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)}
258255, 257eqtrdi 2784 . . . . . . . . . . . 12 ( ∈ dom ∫1 → ( “ (-∞(,)0)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)})
259254imaeq1d 6012 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → ( “ (0(,)+∞)) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ (0(,)+∞)))
260256mptpreima 6190 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ↦ (𝑥)) “ (0(,)+∞)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}
261259, 260eqtrdi 2784 . . . . . . . . . . . 12 ( ∈ dom ∫1 → ( “ (0(,)+∞)) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)})
262258, 261uneq12d 4118 . . . . . . . . . . 11 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) = ({𝑥 ∈ ℝ ∣ (𝑥) ∈ (-∞(,)0)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) ∈ (0(,)+∞)}))
26327ffvelcdmda 7023 . . . . . . . . . . . . 13 (( ∈ dom ∫1𝑥 ∈ ℝ) → (𝑥) ∈ ℝ)
264 0re 11121 . . . . . . . . . . . . . . 15 0 ∈ ℝ
265 lttri2 11202 . . . . . . . . . . . . . . 15 (((𝑥) ∈ ℝ ∧ 0 ∈ ℝ) → ((𝑥) ≠ 0 ↔ ((𝑥) < 0 ∨ 0 < (𝑥))))
266264, 265mpan2 691 . . . . . . . . . . . . . 14 ((𝑥) ∈ ℝ → ((𝑥) ≠ 0 ↔ ((𝑥) < 0 ∨ 0 < (𝑥))))
267 ibar 528 . . . . . . . . . . . . . . 15 ((𝑥) ∈ ℝ → (((𝑥) < 0 ∨ 0 < (𝑥)) ↔ ((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥)))))
268 andi 1009 . . . . . . . . . . . . . . . 16 (((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥))) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
269 0xr 11166 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ*
270 elioomnf 13346 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ* → ((𝑥) ∈ (-∞(,)0) ↔ ((𝑥) ∈ ℝ ∧ (𝑥) < 0)))
271 elioopnf 13345 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ* → ((𝑥) ∈ (0(,)+∞) ↔ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
272270, 271orbi12d 918 . . . . . . . . . . . . . . . . 17 (0 ∈ ℝ* → (((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥)))))
273269, 272ax-mp 5 . . . . . . . . . . . . . . . 16 (((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)) ↔ (((𝑥) ∈ ℝ ∧ (𝑥) < 0) ∨ ((𝑥) ∈ ℝ ∧ 0 < (𝑥))))
274268, 273bitr4i 278 . . . . . . . . . . . . . . 15 (((𝑥) ∈ ℝ ∧ ((𝑥) < 0 ∨ 0 < (𝑥))) ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞)))
275267, 274bitrdi 287 . . . . . . . . . . . . . 14 ((𝑥) ∈ ℝ → (((𝑥) < 0 ∨ 0 < (𝑥)) ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
276266, 275bitrd 279 . . . . . . . . . . . . 13 ((𝑥) ∈ ℝ → ((𝑥) ≠ 0 ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
277263, 276syl 17 . . . . . . . . . . . 12 (( ∈ dom ∫1𝑥 ∈ ℝ) → ((𝑥) ≠ 0 ↔ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))))
278277rabbidva 3402 . . . . . . . . . . 11 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} = {𝑥 ∈ ℝ ∣ ((𝑥) ∈ (-∞(,)0) ∨ (𝑥) ∈ (0(,)+∞))})
279252, 262, 2783eqtr4a 2794 . . . . . . . . . 10 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) = {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0})
280 i1fima 25607 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ (-∞(,)0)) ∈ dom vol)
281 i1fima 25607 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ (0(,)+∞)) ∈ dom vol)
282 unmbl 25466 . . . . . . . . . . 11 ((( “ (-∞(,)0)) ∈ dom vol ∧ ( “ (0(,)+∞)) ∈ dom vol) → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) ∈ dom vol)
283280, 281, 282syl2anc 584 . . . . . . . . . 10 ( ∈ dom ∫1 → (( “ (-∞(,)0)) ∪ ( “ (0(,)+∞))) ∈ dom vol)
284279, 283eqeltrrd 2834 . . . . . . . . 9 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol)
285284ad2antlr 727 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol)
286 inmbl 25471 . . . . . . . 8 (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0} ∈ dom vol) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
287251, 285, 286syl2anc 584 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
288287adantr 480 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol)
28923recnd 11147 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℂ)
290289adantlr 715 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℂ)
291 1cnd 11114 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℂ)
292 simplr 768 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℝ)
29313ad3antlr 731 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
29419ad3antlr 731 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ≠ 0)
295292, 293, 294redivcld 11956 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
296295recnd 11147 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℂ)
297290, 291, 296subadd2d 11498 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
298 eqcom 2740 . . . . . . . . . 10 (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ (𝑡 / (𝑣 / 3)) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1))
299 recn 11103 . . . . . . . . . . . 12 (𝑡 ∈ ℝ → 𝑡 ∈ ℂ)
300299ad2antlr 727 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 𝑡 ∈ ℂ)
30125recnd 11147 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℂ)
302301adantlr 715 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℂ)
30313recnd 11147 . . . . . . . . . . . 12 (𝑣 ∈ ℝ+ → (𝑣 / 3) ∈ ℂ)
304303ad3antlr 731 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℂ)
305300, 302, 304, 294divmul3d 11938 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) = ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
306298, 305bitrid 283 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) = (𝑡 / (𝑣 / 3)) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
307297, 306bitr3d 281 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
308307rabbidva 3402 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))})
309 imaundi 6101 . . . . . . . . . . 11 (𝐹 “ ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
310223ad4antr 732 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹𝑥)))
311 zre 12479 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
312311adantl 481 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
31313ad3antlr 731 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ)
314312, 313remulcld 11149 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ)
315314rexrd 11169 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ*)
316 peano2z 12519 . . . . . . . . . . . . . . . . 17 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℤ)
317316zred 12583 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
318317adantl 481 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
319313, 318remulcld 11149 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
320319rexrd 11169 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ*)
321 zcn 12480 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℂ)
322321adantl 481 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℂ)
323303ad3antlr 731 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℂ)
324322, 323mulcomd 11140 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) = ((𝑣 / 3) · ((𝑡 / (𝑣 / 3)) + 1)))
32568ad3antlr 731 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ+)
326311ltp1d 12059 . . . . . . . . . . . . . . . 16 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ → ((𝑡 / (𝑣 / 3)) + 1) < (((𝑡 / (𝑣 / 3)) + 1) + 1))
327326adantl 481 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) < (((𝑡 / (𝑣 / 3)) + 1) + 1))
328312, 318, 325, 327ltmul2dd 12992 . . . . . . . . . . . . . 14 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑣 / 3) · ((𝑡 / (𝑣 / 3)) + 1)) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))
329324, 328eqbrtrd 5115 . . . . . . . . . . . . 13 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))
330 snunioo 13380 . . . . . . . . . . . . 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 1373 . . . . . . . . . . . 12 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))
332310, 331imaeq12d 6014 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ ({(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))} ∪ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
333309, 332eqtr3id 2782 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
334225mptpreima 6190 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))}
3354ad3antrrr 730 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → 𝐹:ℝ⟶ℝ)
336335ffvelcdmda 7023 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹𝑥) ∈ ℝ)
3373363biant1d 1480 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
338337adantr 480 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
339311adantl 481 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
340336adantr 480 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹𝑥) ∈ ℝ)
34168ad4antlr 733 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝑣 / 3) ∈ ℝ+)
342339, 340, 341lemuldivd 12985 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ ((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3))))
343317adantl 481 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
344340, 343, 341ltdivmuld 12987 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1) ↔ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))
345344bicomd 223 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)) ↔ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1)))
346342, 345anbi12d 632 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
347338, 346bitr3d 281 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
348 elico2 13312 . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
350349adantlr 715 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝐹𝑥) ∈ ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ≤ (𝐹𝑥) ∧ (𝐹𝑥) < ((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))))
351 eqcom 2740 . . . . . . . . . . . . . . 15 (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1))
35221adantlr 715 . . . . . . . . . . . . . . . 16 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ)
353 flbi 13722 . . . . . . . . . . . . . . . 16 ((((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
354352, 353sylan 580 . . . . . . . . . . . . . . 15 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) = ((𝑡 / (𝑣 / 3)) + 1) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
355351, 354bitrid 283 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (((𝑡 / (𝑣 / 3)) + 1) ≤ ((𝐹𝑥) / (𝑣 / 3)) ∧ ((𝐹𝑥) / (𝑣 / 3)) < (((𝑡 / (𝑣 / 3)) + 1) + 1))))
356347, 350, 3553bitr4d 311 . . . . . . . . . . . . 13 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
357356an32s 652 . . . . . . . . . . . 12 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))) ↔ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
358357rabbidva 3402 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))} = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
359334, 358eqtrid 2780 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))[,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
360333, 359eqtrd 2768 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) = {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))})
361230ad4antr 732 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹 ∈ MblFn)
3624ad4antr 732 . . . . . . . . . . 11 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → 𝐹:ℝ⟶ℝ)
363 mbfimasn 25561 . . . . . . . . . . 11 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧ (((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3)) ∈ ℝ) → (𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∈ dom vol)
364361, 362, 314, 363syl3anc 1373 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∈ dom vol)
365 mbfima 25559 . . . . . . . . . . . 12 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
366230, 4, 365syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
367366ad4antr 732 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1)))) ∈ dom vol)
368 unmbl 25466 . . . . . . . . . 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 584 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ((𝐹 “ {(((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))}) ∪ (𝐹 “ ((((𝑡 / (𝑣 / 3)) + 1) · (𝑣 / 3))(,)((𝑣 / 3) · (((𝑡 / (𝑣 / 3)) + 1) + 1))))) ∈ dom vol)
370360, 369eqeltrrd 2834 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
371 simpr 484 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
372352flcld 13704 . . . . . . . . . . . . . . 15 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
373372adantr 480 . . . . . . . . . . . . . 14 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℤ)
374371, 373eqeltrd 2833 . . . . . . . . . . . . 13 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ)
375374stoic1a 1773 . . . . . . . . . . . 12 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
376375an32s 652 . . . . . . . . . . 11 ((((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) ∧ 𝑥 ∈ ℝ) → ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
377376ralrimiva 3125 . . . . . . . . . 10 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → ∀𝑥 ∈ ℝ ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
378 rabeq0 4337 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3))))
379377, 378sylibr 234 . . . . . . . . 9 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} = ∅)
380 0mbl 25468 . . . . . . . . 9 ∅ ∈ dom vol
381379, 380eqeltrdi 2841 . . . . . . . 8 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ ¬ ((𝑡 / (𝑣 / 3)) + 1) ∈ ℤ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
382370, 381pm2.61dan 812 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ((𝑡 / (𝑣 / 3)) + 1) = (⌊‘((𝐹𝑥) / (𝑣 / 3)))} ∈ dom vol)
383308, 382eqeltrrd 2834 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))} ∈ dom vol)
384 inmbl 25471 . . . . . 6 ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))} ∈ dom vol) → (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∈ dom vol)
385288, 383, 384syl2anc 584 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∈ dom vol)
386 rabiun 37653 . . . . . . . . . . 11 {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)}
387 rabeq 3410 . . . . . . . . . . . 12 ( 𝑡 ∈ ran ( “ {𝑡}) = ℝ → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
388168, 387syl 17 . . . . . . . . . . 11 ( ∈ dom ∫1 → {𝑥 𝑡 ∈ ran ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
389386, 388eqtr3id 2782 . . . . . . . . . 10 ( ∈ dom ∫1 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
390389ad2antlr 727 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)})
391176notbid 318 . . . . . . . . . . . . . . 15 (( ∈ dom ∫1𝑥 ∈ ( “ {𝑡})) → (¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
392391rabbidva 3402 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
393 inrab2 4266 . . . . . . . . . . . . . . 15 ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡}
394 rabeq 3410 . . . . . . . . . . . . . . . 16 ((ℝ ∩ ( “ {𝑡})) = ( “ {𝑡}) → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
395184, 394syl 17 . . . . . . . . . . . . . . 15 ( ∈ dom ∫1 → {𝑥 ∈ (ℝ ∩ ( “ {𝑡})) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
396393, 395eqtrid 2780 . . . . . . . . . . . . . 14 ( ∈ dom ∫1 → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) = {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
397392, 396eqtr4d 2771 . . . . . . . . . . . . 13 ( ∈ dom ∫1 → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
398397ad3antlr 731 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} = ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})))
399 imaundi 6101 . . . . . . . . . . . . . . . . 17 (𝐹 “ ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)))
40013, 19jca 511 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑣 ∈ ℝ+ → ((𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0))
401 redivcl 11847 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑡 ∈ ℝ ∧ (𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
4024013expb 1120 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 ∈ ℝ ∧ ((𝑣 / 3) ∈ ℝ ∧ (𝑣 / 3) ≠ 0)) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
403400, 402sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑡 ∈ ℝ ∧ 𝑣 ∈ ℝ+) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
404403ancoms 458 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑣 ∈ ℝ+𝑡 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
405404adantll 714 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝑡 / (𝑣 / 3)) ∈ ℝ)
406405, 203syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
407 peano2re 11293 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
408 reflcl 13702 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
409406, 407, 4083syl 18 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
41013ad2antlr 727 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝑣 / 3) ∈ ℝ)
411409, 410remulcld 11149 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ)
412411rexrd 11169 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ*)
413 pnfxr 11173 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
414413a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → +∞ ∈ ℝ*)
415 ltpnf 13021 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) < +∞)
416411, 415syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) < +∞)
417 snunioo 13380 . . . . . . . . . . . . . . . . . . 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 1373 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) = (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞))
419418imaeq2d 6013 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ ({((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))} ∪ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
420399, 419eqtr3id 2782 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
421223imaeq1d 6012 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)))
422225mptpreima 6190 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ↦ (𝐹𝑥)) “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)}
423421, 422eqtrdi 2784 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)})
424423ad3antrrr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)) = {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)})
425406, 407syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
426425adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ)
427 flflp1 13713 . . . . . . . . . . . . . . . . . . . . 21 (((((𝑡 / (𝑣 / 3)) + 1) + 1) ∈ ℝ ∧ ((𝐹𝑥) / (𝑣 / 3)) ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3)) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
428426, 352, 427syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3)) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
429411adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ)
430 elicopnf 13347 . . . . . . . . . . . . . . . . . . . . . 22 (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
431429, 430syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
432336biantrurd 532 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ ((𝐹𝑥) ∈ ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥))))
433409adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ∈ ℝ)
43468ad3antlr 731 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑣 / 3) ∈ ℝ+)
435433, 336, 434lemuldivd 12985 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ≤ (𝐹𝑥) ↔ (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3))))
436431, 432, 4353bitr2d 307 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ (⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) ≤ ((𝐹𝑥) / (𝑣 / 3))))
437406adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) + 1) ∈ ℝ)
438352, 22syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (⌊‘((𝐹𝑥) / (𝑣 / 3))) ∈ ℝ)
439 1red 11120 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → 1 ∈ ℝ)
440437, 438, 439ltadd1d 11717 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (((𝑡 / (𝑣 / 3)) + 1) + 1) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) + 1)))
441428, 436, 4403bitr4d 311 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3)))))
442295, 439, 438ltaddsubd 11724 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((𝑡 / (𝑣 / 3)) + 1) < (⌊‘((𝐹𝑥) / (𝑣 / 3))) ↔ (𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1)))
443441, 442bitrd 279 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ (𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1)))
444438, 24syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ∈ ℝ)
445292, 444, 434ltdivmul2d 12988 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝑡 / (𝑣 / 3)) < ((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) ↔ 𝑡 < (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))))
446444, 293remulcld 11149 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ∈ ℝ)
447292, 446ltnled 11267 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝑡 < (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
448443, 445, 4473bitrd 305 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → ((𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞) ↔ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡))
449448rabbidva 3402 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ (𝐹𝑥) ∈ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))[,)+∞)} = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
450420, 424, 4493eqtrd 2772 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) = {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡})
451230ad3antrrr 730 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → 𝐹 ∈ MblFn)
452 mbfimasn 25561 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ ∧ ((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3)) ∈ ℝ) → (𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∈ dom vol)
453451, 335, 411, 452syl3anc 1373 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∈ dom vol)
454 mbfima 25559 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
455230, 4, 454syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
456455ad3antrrr 730 . . . . . . . . . . . . . . . 16 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞)) ∈ dom vol)
457 unmbl 25466 . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . . 15 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((𝐹 “ {((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))}) ∪ (𝐹 “ (((⌊‘(((𝑡 / (𝑣 / 3)) + 1) + 1)) · (𝑣 / 3))(,)+∞))) ∈ dom vol)
459450, 458eqeltrrd 2834 . . . . . . . . . . . . . 14 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
460237, 459syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol)
461 inmbl 25471 . . . . . . . . . . . . 13 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∈ dom vol ∧ ( “ {𝑡}) ∈ dom vol) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
462460, 244, 461syl2anc 584 . . . . . . . . . . . 12 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ 𝑡} ∩ ( “ {𝑡})) ∈ dom vol)
463398, 462eqeltrd 2833 . . . . . . . . . . 11 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ran ) → {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
464463ralrimiva 3125 . . . . . . . . . 10 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
465 finiunmbl 25473 . . . . . . . . . 10 ((ran ∈ Fin ∧ ∀𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
46641, 464, 465syl2anc 584 . . . . . . . . 9 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → 𝑡 ∈ ran {𝑥 ∈ ( “ {𝑡}) ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
467390, 466eqeltrrd 2834 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol)
468254imaeq1d 6012 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ {0}) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}))
469256mptpreima 6190 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}
470140elsn 4590 . . . . . . . . . . . . 13 ((𝑥) ∈ {0} ↔ (𝑥) = 0)
471470rabbii 3401 . . . . . . . . . . . 12 {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}} = {𝑥 ∈ ℝ ∣ (𝑥) = 0}
472469, 471eqtri 2756 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) = 0}
473468, 472eqtrdi 2784 . . . . . . . . . 10 ( ∈ dom ∫1 → ( “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) = 0})
474 i1fima 25607 . . . . . . . . . 10 ( ∈ dom ∫1 → ( “ {0}) ∈ dom vol)
475473, 474eqeltrrd 2834 . . . . . . . . 9 ( ∈ dom ∫1 → {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol)
476475ad2antlr 727 . . . . . . . 8 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol)
477 unmbl 25466 . . . . . . . 8 (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ (𝑥) = 0} ∈ dom vol) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
478467, 476, 477syl2anc 584 . . . . . . 7 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
479478adantr 480 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol)
480254imaeq1d 6012 . . . . . . . . 9 ( ∈ dom ∫1 → ( “ {𝑡}) = ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}))
481256mptpreima 6190 . . . . . . . . . 10 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {𝑡}}
482140elsn 4590 . . . . . . . . . . . 12 ((𝑥) ∈ {𝑡} ↔ (𝑥) = 𝑡)
483 eqcom 2740 . . . . . . . . . . . 12 ((𝑥) = 𝑡𝑡 = (𝑥))
484482, 483bitri 275 . . . . . . . . . . 11 ((𝑥) ∈ {𝑡} ↔ 𝑡 = (𝑥))
485484rabbii 3401 . . . . . . . . . 10 {𝑥 ∈ ℝ ∣ (𝑥) ∈ {𝑡}} = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}
486481, 485eqtri 2756 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ (𝑥)) “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}
487480, 486eqtrdi 2784 . . . . . . . 8 ( ∈ dom ∫1 → ( “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
488487ad3antlr 731 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ( “ {𝑡}) = {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})
489488, 243eqeltrrd 2834 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)} ∈ dom vol)
490 inmbl 25471 . . . . . 6 ((({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∈ dom vol ∧ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)} ∈ dom vol) → (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) ∈ dom vol)
491479, 489, 490syl2anc 584 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)}) ∈ dom vol)
492 unmbl 25466 . . . . 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 584 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ ℝ) → ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})) ∈ dom vol)
494159, 493syl 17 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → ((({𝑥 ∈ ℝ ∣ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ≠ 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3))}) ∪ (({𝑥 ∈ ℝ ∣ ¬ (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥)} ∪ {𝑥 ∈ ℝ ∣ (𝑥) = 0}) ∩ {𝑥 ∈ ℝ ∣ 𝑡 = (𝑥)})) ∈ dom vol)
495154, 494eqeltrid 2837 . 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 25459 . . . 4 (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∈ dom vol → (vol‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) = (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})))
497495, 496syl 17 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (vol‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) = (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})))
498 eldifsn 4737 . . . . . 6 (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) ↔ (𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∧ 𝑡 ≠ 0))
499157anim1d 611 . . . . . 6 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → ((𝑡 ∈ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∧ 𝑡 ≠ 0) → (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
500498, 499biimtrid 242 . . . . 5 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0}) → (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
501500imdistani 568 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)))
502128a1i 11 . . . . . . . . . . 11 ( ∈ dom ∫1 → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) = {𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}})
503468, 469eqtrdi 2784 . . . . . . . . . . 11 ( ∈ dom ∫1 → ( “ {0}) = {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}})
504502, 503ineq12d 4170 . . . . . . . . . 10 ( ∈ dom ∫1 → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ({𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}))
505 inrab 4265 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}} ∩ {𝑥 ∈ ℝ ∣ (𝑥) ∈ {0}}) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})}
506504, 505eqtrdi 2784 . . . . . . . . 9 ( ∈ dom ∫1 → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})})
507506ad3antlr 731 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})})
508144biimpri 228 . . . . . . . . . . . . . . . . . 18 ((𝑥) = 0 → ¬ (𝑥) ≠ 0)
509508intnand 488 . . . . . . . . . . . . . . . . 17 ((𝑥) = 0 → ¬ ((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0))
510509iffalsed 4485 . . . . . . . . . . . . . . . 16 ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = (𝑥))
511 eqtr 2753 . . . . . . . . . . . . . . . 16 ((if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = (𝑥) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
512510, 511mpancom 688 . . . . . . . . . . . . . . 15 ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
513512adantl 481 . . . . . . . . . . . . . 14 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) = 0)
514 simpll 766 . . . . . . . . . . . . . . 15 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → 𝑡 ≠ 0)
515514necomd 2984 . . . . . . . . . . . . . 14 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → 0 ≠ 𝑡)
516513, 515eqnetrd 2996 . . . . . . . . . . . . 13 (((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) ∧ (𝑥) = 0) → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡)
517516ex 412 . . . . . . . . . . . 12 ((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) → ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
518 orcom 870 . . . . . . . . . . . . . 14 ((¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∨ ¬ (𝑥) ∈ {0}) ↔ (¬ (𝑥) ∈ {0} ∨ ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
519 ianor 983 . . . . . . . . . . . . . 14 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ (¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∨ ¬ (𝑥) ∈ {0}))
520 imor 853 . . . . . . . . . . . . . 14 (((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}) ↔ (¬ (𝑥) ∈ {0} ∨ ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
521518, 519, 5203bitr4i 303 . . . . . . . . . . . . 13 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ ((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}))
522142necon3bbii 2976 . . . . . . . . . . . . . 14 (¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ↔ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡)
523470, 522imbi12i 350 . . . . . . . . . . . . 13 (((𝑥) ∈ {0} → ¬ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡}) ↔ ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
524521, 523bitri 275 . . . . . . . . . . . 12 (¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}) ↔ ((𝑥) = 0 → if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ≠ 𝑡))
525517, 524sylibr 234 . . . . . . . . . . 11 ((𝑡 ≠ 0 ∧ 𝑥 ∈ ℝ) → ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
526525ralrimiva 3125 . . . . . . . . . 10 (𝑡 ≠ 0 → ∀𝑥 ∈ ℝ ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
527 rabeq0 4337 . . . . . . . . . 10 ({𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅ ↔ ∀𝑥 ∈ ℝ ¬ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0}))
528526, 527sylibr 234 . . . . . . . . 9 (𝑡 ≠ 0 → {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅)
529528ad2antll 729 . . . . . . . 8 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → {𝑥 ∈ ℝ ∣ (if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)) ∈ {𝑡} ∧ (𝑥) ∈ {0})} = ∅)
530507, 529eqtrd 2768 . . . . . . 7 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ∅)
531 imassrn 6024 . . . . . . . . 9 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
532 dfdm4 5839 . . . . . . . . . 10 dom (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥)))
533141, 127dmmpti 6630 . . . . . . . . . 10 dom (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ℝ
534532, 533eqtr3i 2758 . . . . . . . . 9 ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) = ℝ
535531, 534sseqtri 3979 . . . . . . . 8 ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ℝ
536 reldisj 4402 . . . . . . . 8 (((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ℝ → ((((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ∅ ↔ ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ (ℝ ∖ ( “ {0}))))
537535, 536ax-mp 5 . . . . . . 7 ((((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ∩ ( “ {0})) = ∅ ↔ ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ (ℝ ∖ ( “ {0})))
538530, 537sylib 218 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ (ℝ ∖ ( “ {0})))
539 ffun 6659 . . . . . . . . . 10 (:ℝ⟶ℝ → Fun )
540 difpreima 7004 . . . . . . . . . 10 (Fun → ( “ (ran ∖ {0})) = (( “ ran ) ∖ ( “ {0})))
541539, 540syl 17 . . . . . . . . 9 (:ℝ⟶ℝ → ( “ (ran ∖ {0})) = (( “ ran ) ∖ ( “ {0})))
542 fdm 6665 . . . . . . . . . . 11 (:ℝ⟶ℝ → dom = ℝ)
543161, 542eqtrid 2780 . . . . . . . . . 10 (:ℝ⟶ℝ → ( “ ran ) = ℝ)
544543difeq1d 4074 . . . . . . . . 9 (:ℝ⟶ℝ → (( “ ran ) ∖ ( “ {0})) = (ℝ ∖ ( “ {0})))
545541, 544eqtrd 2768 . . . . . . . 8 (:ℝ⟶ℝ → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
54627, 545syl 17 . . . . . . 7 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
547546ad3antlr 731 . . . . . 6 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ( “ (ran ∖ {0})) = (ℝ ∖ ( “ {0})))
548538, 547sseqtrrd 3968 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡}) ⊆ ( “ (ran ∖ {0})))
549 imassrn 6024 . . . . . . 7 ( “ (ran ∖ {0})) ⊆ ran
550549, 181sseqtrid 3973 . . . . . 6 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) ⊆ ℝ)
551550ad3antlr 731 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → ( “ (ran ∖ {0})) ⊆ ℝ)
552 i1fima 25607 . . . . . . . 8 ( ∈ dom ∫1 → ( “ (ran ∖ {0})) ∈ dom vol)
553 mblvol 25459 . . . . . . . 8 (( “ (ran ∖ {0})) ∈ dom vol → (vol‘( “ (ran ∖ {0}))) = (vol*‘( “ (ran ∖ {0}))))
554552, 553syl 17 . . . . . . 7 ( ∈ dom ∫1 → (vol‘( “ (ran ∖ {0}))) = (vol*‘( “ (ran ∖ {0}))))
555 neldifsn 4743 . . . . . . . 8 ¬ 0 ∈ (ran ∖ {0})
556 i1fima2 25608 . . . . . . . 8 (( ∈ dom ∫1 ∧ ¬ 0 ∈ (ran ∖ {0})) → (vol‘( “ (ran ∖ {0}))) ∈ ℝ)
557555, 556mpan2 691 . . . . . . 7 ( ∈ dom ∫1 → (vol‘( “ (ran ∖ {0}))) ∈ ℝ)
558554, 557eqeltrrd 2834 . . . . . 6 ( ∈ dom ∫1 → (vol*‘( “ (ran ∖ {0}))) ∈ ℝ)
559558ad3antlr 731 . . . . 5 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (vol*‘( “ (ran ∖ {0}))) ∈ ℝ)
560 ovolsscl 25415 . . . . 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 1373 . . . 4 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ (𝑡 ∈ ℝ ∧ 𝑡 ≠ 0)) → (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
562501, 561syl 17 . . 3 ((((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) ∧ 𝑡 ∈ (ran (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∖ {0})) → (vol*‘((𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) “ {𝑡})) ∈ ℝ)
563497, 562eqeltrd 2833 . 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 25610 1 (((𝜑 ∈ dom ∫1) ∧ 𝑣 ∈ ℝ+) → (𝑥 ∈ ℝ ↦ if(((((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)) ≤ (𝑥) ∧ (𝑥) ≠ 0), (((⌊‘((𝐹𝑥) / (𝑣 / 3))) − 1) · (𝑣 / 3)), (𝑥))) ∈ dom ∫1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1541  wex 1780  wcel 2113  wne 2929  wral 3048  wrex 3057  {crab 3396  Vcvv 3437  cdif 3895  cun 3896  cin 3897  wss 3898  c0 4282  ifcif 4474  {csn 4575   ciun 4941   class class class wbr 5093  cmpt 5174  ccnv 5618  dom cdm 5619  ran crn 5620  cima 5622  Fun wfun 6480   Fn wfn 6481  wf 6482  ontowfo 6484  cfv 6486  (class class class)co 7352  Fincfn 8875  supcsup 9331  cc 11011  cr 11012  0cc0 11013  1c1 11014   + caddc 11016   · cmul 11018  +∞cpnf 11150  -∞cmnf 11151  *cxr 11152   < clt 11153  cle 11154  cmin 11351  -cneg 11352   / cdiv 11781  cn 12132  3c3 12188  0cn0 12388  cz 12475  +crp 12892  (,)cioo 13247  [,)cico 13249  ...cfz 13409  cfl 13696  vol*covol 25391  volcvol 25392  MblFncmbf 25543  1citg1 25544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-inf2 9538  ax-cnex 11069  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089  ax-pre-mulgt0 11090  ax-pre-sup 11091
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-int 4898  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-isom 6495  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-of 7616  df-om 7803  df-1st 7927  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-1o 8391  df-2o 8392  df-er 8628  df-map 8758  df-pm 8759  df-en 8876  df-dom 8877  df-sdom 8878  df-fin 8879  df-fi 9302  df-sup 9333  df-inf 9334  df-oi 9403  df-dju 9801  df-card 9839  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-sub 11353  df-neg 11354  df-div 11782  df-nn 12133  df-2 12195  df-3 12196  df-n0 12389  df-z 12476  df-uz 12739  df-q 12849  df-rp 12893  df-xneg 13013  df-xadd 13014  df-xmul 13015  df-ioo 13251  df-ico 13253  df-icc 13254  df-fz 13410  df-fzo 13557  df-fl 13698  df-seq 13911  df-exp 13971  df-hash 14240  df-cj 15008  df-re 15009  df-im 15010  df-sqrt 15144  df-abs 15145  df-clim 15397  df-sum 15596  df-rest 17328  df-topgen 17349  df-psmet 21285  df-xmet 21286  df-met 21287  df-bl 21288  df-mopn 21289  df-top 22810  df-topon 22827  df-bases 22862  df-cmp 23303  df-ovol 25393  df-vol 25394  df-mbf 25548  df-itg1 25549
This theorem is referenced by:  itg2addnclem3  37733
  Copyright terms: Public domain W3C validator