itg2addnclem2

Description: Lemma for itg2addnc . The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017)

	Ref	Expression
Hypotheses	itg2addnc.f1	$⊢ φ \to F \in MblFn$
	itg2addnc.f2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
Assertion	itg2addnclem2	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) \in dom \int^{1}$

Proof

Step	Hyp	Ref	Expression
1		itg2addnc.f1	$⊢ φ \to F \in MblFn$
2		itg2addnc.f2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
3		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
4		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F : ℝ ⟶ ℝ$
5	2 3 4	sylancl	$⊢ φ \to F : ℝ ⟶ ℝ$
6	5	ad2antrr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to F : ℝ ⟶ ℝ$
7	6	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to F (x) \in ℝ$
8		rpre	$⊢ v \in ℝ^{+} \to v \in ℝ$
9		3re	$⊢ 3 \in ℝ$
10		3ne0	$⊢ 3 \neq 0$
11	9 10	pm3.2i	$⊢ (3 \in ℝ \land 3 \neq 0)$
12		redivcl	$⊢ (v \in ℝ \land 3 \in ℝ \land 3 \neq 0) \to \frac{v}{3} \in ℝ$
13	12	3expb	$⊢ (v \in ℝ \land (3 \in ℝ \land 3 \neq 0)) \to \frac{v}{3} \in ℝ$
14	8 11 13	sylancl	$⊢ v \in ℝ^{+} \to \frac{v}{3} \in ℝ$
15	14	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to \frac{v}{3} \in ℝ$
16		rpcnne0	$⊢ v \in ℝ^{+} \to (v \in ℂ \land v \neq 0)$
17		3cn	$⊢ 3 \in ℂ$
18	17 10	pm3.2i	$⊢ (3 \in ℂ \land 3 \neq 0)$
19		divne0	$⊢ ((v \in ℂ \land v \neq 0) \land (3 \in ℂ \land 3 \neq 0)) \to \frac{v}{3} \neq 0$
20	16 18 19	sylancl	$⊢ v \in ℝ^{+} \to \frac{v}{3} \neq 0$
21	20	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to \frac{v}{3} \neq 0$
22	7 15 21	redivcld	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to \frac{F (x)}{\frac{v}{3}} \in ℝ$
23		reflcl	$⊢ \frac{F (x)}{\frac{v}{3}} \in ℝ \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℝ$
24	22 23	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℝ$
25		peano2rem	$⊢ ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℝ \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \in ℝ$
26	24 25	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \in ℝ$
27	26 15	remulcld	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in ℝ$
28		i1ff	$⊢ h \in dom \int^{1} \to h : ℝ ⟶ ℝ$
29	28	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to h : ℝ ⟶ ℝ$
30	29	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to h (x) \in ℝ$
31	27 30	ifcld	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in ℝ$
32	31	fmpttd	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) : ℝ ⟶ ℝ$
33		fzfi	$⊢ (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) \in Fin$
34		ovex	$⊢ (t - 1) (\frac{v}{3}) \in V$
35		eqid	$⊢ (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) = (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3}))$
36	34 35	fnmpti	$⊢ (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) Fn (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋)$
37		dffn4	$⊢ (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) Fn (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) \leftrightarrow (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) : (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) \underset{onto}{⟶} ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3}))$
38	36 37	mpbi	$⊢ (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) : (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) \underset{onto}{⟶} ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3}))$
39		fofi	$⊢ ((0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) \in Fin \land (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) : (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) \underset{onto}{⟶} ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3}))) \to ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \in Fin$
40	33 38 39	mp2an	$⊢ ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \in Fin$
41		i1frn	$⊢ h \in dom \int^{1} \to ran h \in Fin$
42	41	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ran h \in Fin$
43		unfi	$⊢ (ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \in Fin \land ran h \in Fin) \to ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h \in Fin$
44	40 42 43	sylancr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h \in Fin$
45		0zd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \land ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)) \to 0 \in ℤ$
46	28	frnd	$⊢ h \in dom \int^{1} \to ran h \subseteq ℝ$
47		i1f0rn	$⊢ h \in dom \int^{1} \to 0 \in ran h$
48		elex2	$⊢ 0 \in ran h \to \exists x x \in ran h$
49	47 48	syl	$⊢ h \in dom \int^{1} \to \exists x x \in ran h$
50		n0	$⊢ ran h \neq \emptyset \leftrightarrow \exists x x \in ran h$
51	49 50	sylibr	$⊢ h \in dom \int^{1} \to ran h \neq \emptyset$
52		fimaxre2	$⊢ (ran h \subseteq ℝ \land ran h \in Fin) \to \exists x \in ℝ \forall y \in ran h y \leq x$
53	46 41 52	syl2anc	$⊢ h \in dom \int^{1} \to \exists x \in ℝ \forall y \in ran h y \leq x$
54		suprcl	$⊢ (ran h \subseteq ℝ \land ran h \neq \emptyset \land \exists x \in ℝ \forall y \in ran h y \leq x) \to sup (ran h ℝ <) \in ℝ$
55	46 51 53 54	syl3anc	$⊢ h \in dom \int^{1} \to sup (ran h ℝ <) \in ℝ$
56	55	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to sup (ran h ℝ <) \in ℝ$
57	56 15 21	redivcld	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to \frac{sup (ran h ℝ <)}{\frac{v}{3}} \in ℝ$
58		peano2re	$⊢ \frac{sup (ran h ℝ <)}{\frac{v}{3}} \in ℝ \to (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \in ℝ$
59	57 58	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \in ℝ$
60		ceicl	$⊢ (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \in ℝ \to - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋ \in ℤ$
61	59 60	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋ \in ℤ$
62	61	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \land ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)) \to - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋ \in ℤ$
63	22	flcld	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℤ$
64	63	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \land ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℤ$
65		3nn	$⊢ 3 \in ℕ$
66		nnrp	$⊢ 3 \in ℕ \to 3 \in ℝ^{+}$
67	65 66	ax-mp	$⊢ 3 \in ℝ^{+}$
68		rpdivcl	$⊢ (v \in ℝ^{+} \land 3 \in ℝ^{+}) \to \frac{v}{3} \in ℝ^{+}$
69	67 68	mpan2	$⊢ v \in ℝ^{+} \to \frac{v}{3} \in ℝ^{+}$
70	69	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to \frac{v}{3} \in ℝ^{+}$
71	2	ad2antrr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to F : ℝ ⟶ [0, +∞)$
72	71	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to F (x) \in [0, +∞)$
73		elrege0	$⊢ F (x) \in [0, +∞) \leftrightarrow (F (x) \in ℝ \land 0 \leq F (x))$
74	72 73	sylib	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (F (x) \in ℝ \land 0 \leq F (x))$
75	74	simprd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to 0 \leq F (x)$
76	7 70 75	divge0d	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to 0 \leq \frac{F (x)}{\frac{v}{3}}$
77		flge0nn0	$⊢ (\frac{F (x)}{\frac{v}{3}} \in ℝ \land 0 \leq \frac{F (x)}{\frac{v}{3}}) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℕ_{0}$
78	22 76 77	syl2anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℕ_{0}$
79	78	nn0ge0d	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to 0 \leq ⌊\frac{F (x)}{\frac{v}{3}}⌋$
80	79	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \land ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)) \to 0 \leq ⌊\frac{F (x)}{\frac{v}{3}}⌋$
81	46 51 53	3jca	$⊢ h \in dom \int^{1} \to (ran h \subseteq ℝ \land ran h \neq \emptyset \land \exists x \in ℝ \forall y \in ran h y \leq x)$
82	81	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (ran h \subseteq ℝ \land ran h \neq \emptyset \land \exists x \in ℝ \forall y \in ran h y \leq x)$
83		ffn	$⊢ h : ℝ ⟶ ℝ \to h Fn ℝ$
84	28 83	syl	$⊢ h \in dom \int^{1} \to h Fn ℝ$
85		dffn3	$⊢ h Fn ℝ \leftrightarrow h : ℝ ⟶ ran h$
86	84 85	sylib	$⊢ h \in dom \int^{1} \to h : ℝ ⟶ ran h$
87	86	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to h : ℝ ⟶ ran h$
88	87	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to h (x) \in ran h$
89		suprub	$⊢ ((ran h \subseteq ℝ \land ran h \neq \emptyset \land \exists x \in ℝ \forall y \in ran h y \leq x) \land h (x) \in ran h) \to h (x) \leq sup (ran h ℝ <)$
90	82 88 89	syl2anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to h (x) \leq sup (ran h ℝ <)$
91		letr	$⊢ ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in ℝ \land h (x) \in ℝ \land sup (ran h ℝ <) \in ℝ) \to (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \leq sup (ran h ℝ <)) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq sup (ran h ℝ <))$
92	27 30 56 91	syl3anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \leq sup (ran h ℝ <)) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq sup (ran h ℝ <))$
93	26 56 70	lemuldivd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq sup (ran h ℝ <) \leftrightarrow ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \leq \frac{sup (ran h ℝ <)}{\frac{v}{3}})$
94		1red	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to 1 \in ℝ$
95	24 94 57	lesubaddd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \leq \frac{sup (ran h ℝ <)}{\frac{v}{3}} \leftrightarrow ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)$
96	93 95	bitrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq sup (ran h ℝ <) \leftrightarrow ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)$
97		ceige	$⊢ (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \in ℝ \to (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋$
98	59 97	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋$
99	61	zred	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋ \in ℝ$
100		letr	$⊢ (⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℝ \land (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \in ℝ \land - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋ \in ℝ) \to ((⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \land (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋)$
101	24 59 99 100	syl3anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ((⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \land (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋)$
102	98 101	mpan2d	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋)$
103	96 102	sylbid	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq sup (ran h ℝ <) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋)$
104	92 103	syld	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \leq sup (ran h ℝ <)) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋)$
105	90 104	mpan2d	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋)$
106	105	adantrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋)$
107	106	imp	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \land ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋$
108	45 62 64 80 107	elfzd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \land ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋)$
109		eqid	$⊢ (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})$
110		oveq1	$⊢ t = ⌊\frac{F (x)}{\frac{v}{3}}⌋ \to t - 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1$
111	110	oveq1d	$⊢ t = ⌊\frac{F (x)}{\frac{v}{3}}⌋ \to (t - 1) (\frac{v}{3}) = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})$
112	111	rspceeqv	$⊢ (⌊\frac{F (x)}{\frac{v}{3}}⌋ \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) \land (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})) \to \exists t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) = (t - 1) (\frac{v}{3})$
113	108 109 112	sylancl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \land ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)) \to \exists t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) = (t - 1) (\frac{v}{3})$
114		ovex	$⊢ (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in V$
115	35	elrnmpt	$⊢ (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in V \to ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \leftrightarrow \exists t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) = (t - 1) (\frac{v}{3}))$
116	114 115	ax-mp	$⊢ (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \leftrightarrow \exists t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) = (t - 1) (\frac{v}{3})$
117	113 116	sylibr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \land ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3}))$
118		elun1	$⊢ (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in (ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h)$
119	117 118	syl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \land ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in (ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h)$
120		elun2	$⊢ h (x) \in ran h \to h (x) \in (ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h)$
121	88 120	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to h (x) \in (ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h)$
122	121	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \land \neg ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)) \to h (x) \in (ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h)$
123	119 122	ifclda	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in (ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h)$
124	123	fmpttd	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) : ℝ ⟶ ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h$
125	124	frnd	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) \subseteq ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h$
126		ssfi	$⊢ (ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h \in Fin \land ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) \subseteq ran (t \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) ⟼ (t - 1) (\frac{v}{3})) \cup ran h) \to ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) \in Fin$
127	44 125 126	syl2anc	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) \in Fin$
128		eqid	$⊢ (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) = (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))$
129	128	mptpreima	$⊢ {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] = \{x \in ℝ \| if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\}\}$
130		unrab	$⊢ \{x \in ℝ \| (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}))\} \cup \{x \in ℝ \| ((\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \land t = h (x))\} = \{x \in ℝ \| ((((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})) \lor ((\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \land t = h (x)))\}$
131		inrab	$⊢ \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\} = \{x \in ℝ \| ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)\}$
132	131	ineq1i	$⊢ (\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\} = \{x \in ℝ \| ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)\} \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\}$
133		inrab	$⊢ \{x \in ℝ \| ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)\} \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\} = \{x \in ℝ \| (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}))\}$
134	132 133	eqtri	$⊢ (\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\} = \{x \in ℝ \| (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}))\}$
135		unrab	$⊢ \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\} = \{x \in ℝ \| (\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0)\}$
136	135	ineq1i	$⊢ (\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\} = \{x \in ℝ \| (\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0)\} \cap \{x \in ℝ \| t = h (x)\}$
137		inrab	$⊢ \{x \in ℝ \| (\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0)\} \cap \{x \in ℝ \| t = h (x)\} = \{x \in ℝ \| ((\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \land t = h (x))\}$
138	136 137	eqtri	$⊢ (\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\} = \{x \in ℝ \| ((\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \land t = h (x))\}$
139	134 138	uneq12i	$⊢ ((\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\}) \cup ((\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\}) = \{x \in ℝ \| (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}))\} \cup \{x \in ℝ \| ((\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \land t = h (x))\}$
140		eqcom	$⊢ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) = t \leftrightarrow t = if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))$
141		fvex	$⊢ h (x) \in V$
142	114 141	ifex	$⊢ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in V$
143	142	elsn	$⊢ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \leftrightarrow if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) = t$
144		ianor	$⊢ \neg ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \leftrightarrow (\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor \neg h (x) \neq 0)$
145		nne	$⊢ \neg h (x) \neq 0 \leftrightarrow h (x) = 0$
146	145	orbi2i	$⊢ (\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor \neg h (x) \neq 0) \leftrightarrow (\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0)$
147	144 146	bitr2i	$⊢ (\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \leftrightarrow \neg ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)$
148	147	anbi1i	$⊢ ((\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \land t = h (x)) \leftrightarrow (\neg ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = h (x))$
149	148	orbi2i	$⊢ ((((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})) \lor ((\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \land t = h (x))) \leftrightarrow ((((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})) \lor (\neg ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = h (x)))$
150		eqif	$⊢ t = if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \leftrightarrow ((((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})) \lor (\neg ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = h (x)))$
151	149 150	bitr4i	$⊢ ((((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})) \lor ((\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \land t = h (x))) \leftrightarrow t = if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))$
152	140 143 151	3bitr4i	$⊢ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \leftrightarrow ((((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})) \lor ((\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \land t = h (x)))$
153	152	rabbii	$⊢ \{x \in ℝ \| if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\}\} = \{x \in ℝ \| ((((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0) \land t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})) \lor ((\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \lor h (x) = 0) \land t = h (x)))\}$
154	130 139 153	3eqtr4ri	$⊢ \{x \in ℝ \| if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\}\} = ((\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\}) \cup ((\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\})$
155	129 154	eqtri	$⊢ {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] = ((\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\}) \cup ((\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\})$
156		eldifi	$⊢ t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\}) \to t \in ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))$
157	32	frnd	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) \subseteq ℝ$
158	157	sseld	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (t \in ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) \to t \in ℝ)$
159	156 158	syl5	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\}) \to t \in ℝ)$
160	159	imdistani	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\})) \to (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ)$
161		rabiun	$⊢ \{x \in ⋃_{t \in ran h} h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = ⋃_{t \in ran h} \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\}$
162		cnvimarndm	$⊢ h^{-1} [ran h] = dom h$
163		iunid	$⊢ ⋃_{t \in ran h} \{t\} = ran h$
164	163	imaeq2i	$⊢ h^{-1} [⋃_{t \in ran h} \{t\}] = h^{-1} [ran h]$
165		imaiun	$⊢ h^{-1} [⋃_{t \in ran h} \{t\}] = ⋃_{t \in ran h} h^{-1} [\{t\}]$
166	164 165	eqtr3i	$⊢ h^{-1} [ran h] = ⋃_{t \in ran h} h^{-1} [\{t\}]$
167	162 166	eqtr3i	$⊢ dom h = ⋃_{t \in ran h} h^{-1} [\{t\}]$
168	28	fdmd	$⊢ h \in dom \int^{1} \to dom h = ℝ$
169	167 168	eqtr3id	$⊢ h \in dom \int^{1} \to ⋃_{t \in ran h} h^{-1} [\{t\}] = ℝ$
170	169	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ⋃_{t \in ran h} h^{-1} [\{t\}] = ℝ$
171		rabeq	$⊢ ⋃_{t \in ran h} h^{-1} [\{t\}] = ℝ \to \{x \in ⋃_{t \in ran h} h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\}$
172	170 171	syl	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \{x \in ⋃_{t \in ran h} h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\}$
173	161 172	eqtr3id	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ⋃_{t \in ran h} \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\}$
174		fniniseg	$⊢ h Fn ℝ \to (x \in h^{-1} [\{t\}] \leftrightarrow (x \in ℝ \land h (x) = t))$
175	28 83 174	3syl	$⊢ h \in dom \int^{1} \to (x \in h^{-1} [\{t\}] \leftrightarrow (x \in ℝ \land h (x) = t))$
176	175	simplbda	$⊢ (h \in dom \int^{1} \land x \in h^{-1} [\{t\}]) \to h (x) = t$
177	176	breq2d	$⊢ (h \in dom \int^{1} \land x \in h^{-1} [\{t\}]) \to ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \leftrightarrow (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t)$
178	177	rabbidva	$⊢ h \in dom \int^{1} \to \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
179		inrab2	$⊢ \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}] = \{x \in (ℝ \cap h^{-1} [\{t\}]) \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
180		imassrn	$⊢ h^{-1} [\{t\}] \subseteq ran h^{-1}$
181		dfdm4	$⊢ dom h = ran h^{-1}$
182	181 168	eqtr3id	$⊢ h \in dom \int^{1} \to ran h^{-1} = ℝ$
183	180 182	sseqtrid	$⊢ h \in dom \int^{1} \to h^{-1} [\{t\}] \subseteq ℝ$
184		sseqin2	$⊢ h^{-1} [\{t\}] \subseteq ℝ \leftrightarrow ℝ \cap h^{-1} [\{t\}] = h^{-1} [\{t\}]$
185	183 184	sylib	$⊢ h \in dom \int^{1} \to ℝ \cap h^{-1} [\{t\}] = h^{-1} [\{t\}]$
186		rabeq	$⊢ ℝ \cap h^{-1} [\{t\}] = h^{-1} [\{t\}] \to \{x \in (ℝ \cap h^{-1} [\{t\}]) \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} = \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
187	185 186	syl	$⊢ h \in dom \int^{1} \to \{x \in (ℝ \cap h^{-1} [\{t\}]) \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} = \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
188	179 187	syl5eq	$⊢ h \in dom \int^{1} \to \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}] = \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
189	178 188	eqtr4d	$⊢ h \in dom \int^{1} \to \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}]$
190	189	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}]$
191	26	adantlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \in ℝ$
192	46	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ran h \subseteq ℝ$
193	192	sselda	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to t \in ℝ$
194	193	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to t \in ℝ$
195	69	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to \frac{v}{3} \in ℝ^{+}$
196	191 194 195	lemuldivd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t \leftrightarrow ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \leq \frac{t}{\frac{v}{3}})$
197	24	adantlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℝ$
198		1red	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to 1 \in ℝ$
199	14	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to \frac{v}{3} \in ℝ$
200	20	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to \frac{v}{3} \neq 0$
201	194 199 200	redivcld	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to \frac{t}{\frac{v}{3}} \in ℝ$
202	197 198 201	lesubaddd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \leq \frac{t}{\frac{v}{3}} \leftrightarrow ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq (\frac{t}{\frac{v}{3}}) + 1)$
203	7	adantlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to F (x) \in ℝ$
204		peano2re	$⊢ \frac{t}{\frac{v}{3}} \in ℝ \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
205	201 204	syl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
206		reflcl	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℝ \to ⌊(\frac{t}{\frac{v}{3}}) + 1⌋ \in ℝ$
207	205 206	syl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to ⌊(\frac{t}{\frac{v}{3}}) + 1⌋ \in ℝ$
208		peano2re	$⊢ ⌊(\frac{t}{\frac{v}{3}}) + 1⌋ \in ℝ \to ⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1 \in ℝ$
209	207 208	syl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to ⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1 \in ℝ$
210	203 209 195	ltdivmuld	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to (\frac{F (x)}{\frac{v}{3}} < ⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1 \leftrightarrow F (x) < (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))$
211	22	adantlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to \frac{F (x)}{\frac{v}{3}} \in ℝ$
212		flflp1	$⊢ (\frac{F (x)}{\frac{v}{3}} \in ℝ \land (\frac{t}{\frac{v}{3}}) + 1 \in ℝ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq (\frac{t}{\frac{v}{3}}) + 1 \leftrightarrow \frac{F (x)}{\frac{v}{3}} < ⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1)$
213	211 205 212	syl2anc	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq (\frac{t}{\frac{v}{3}}) + 1 \leftrightarrow \frac{F (x)}{\frac{v}{3}} < ⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1)$
214	199 209	remulcld	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1) \in ℝ$
215	214	rexrd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1) \in ℝ^{*}$
216		elioomnf	$⊢ (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1) \in ℝ^{*} \to (F (x) \in (−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1)) \leftrightarrow (F (x) \in ℝ \land F (x) < (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1)))$
217	215 216	syl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to (F (x) \in (−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1)) \leftrightarrow (F (x) \in ℝ \land F (x) < (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1)))$
218	203	biantrurd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to (F (x) < (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1) \leftrightarrow (F (x) \in ℝ \land F (x) < (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1)))$
219	217 218	bitr4d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to (F (x) \in (−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1)) \leftrightarrow F (x) < (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))$
220	210 213 219	3bitr4d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq (\frac{t}{\frac{v}{3}}) + 1 \leftrightarrow F (x) \in (−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1)))$
221	196 202 220	3bitrd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t \leftrightarrow F (x) \in (−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1)))$
222	221	rabbidva	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} = \{x \in ℝ \| F (x) \in (−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))\}$
223	2	feqmptd	$⊢ φ \to F = (x \in ℝ ⟼ F (x))$
224	223	cnveqd	$⊢ φ \to F^{-1} = {(x \in ℝ ⟼ F (x))}^{-1}$
225	224	imaeq1d	$⊢ φ \to F^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))] = {(x \in ℝ ⟼ F (x))}^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))]$
226		eqid	$⊢ (x \in ℝ ⟼ F (x)) = (x \in ℝ ⟼ F (x))$
227	226	mptpreima	$⊢ {(x \in ℝ ⟼ F (x))}^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))] = \{x \in ℝ \| F (x) \in (−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))\}$
228	225 227	eqtrdi	$⊢ φ \to F^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))] = \{x \in ℝ \| F (x) \in (−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))\}$
229	228	ad3antrrr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to F^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))] = \{x \in ℝ \| F (x) \in (−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))\}$
230	222 229	eqtr4d	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} = F^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))]$
231		mbfima	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ) \to F^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))] \in dom vol$
232	1 5 231	syl2anc	$⊢ φ \to F^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))] \in dom vol$
233	232	ad3antrrr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to F^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))] \in dom vol$
234	230 233	eqeltrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \in dom vol$
235	46	sseld	$⊢ h \in dom \int^{1} \to (t \in ran h \to t \in ℝ)$
236	235	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (t \in ran h \to t \in ℝ)$
237	236	imdistani	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ)$
238		i1fmbf	$⊢ h \in dom \int^{1} \to h \in MblFn$
239	238 28	jca	$⊢ h \in dom \int^{1} \to (h \in MblFn \land h : ℝ ⟶ ℝ)$
240	239	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (h \in MblFn \land h : ℝ ⟶ ℝ)$
241		mbfimasn	$⊢ (h \in MblFn \land h : ℝ ⟶ ℝ \land t \in ℝ) \to h^{-1} [\{t\}] \in dom vol$
242	241	3expa	$⊢ ((h \in MblFn \land h : ℝ ⟶ ℝ) \land t \in ℝ) \to h^{-1} [\{t\}] \in dom vol$
243	240 242	sylan	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to h^{-1} [\{t\}] \in dom vol$
244	237 243	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to h^{-1} [\{t\}] \in dom vol$
245		inmbl	$⊢ (\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \in dom vol \land h^{-1} [\{t\}] \in dom vol) \to \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}] \in dom vol$
246	234 244 245	syl2anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}] \in dom vol$
247	190 246	eqeltrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol$
248	247	ralrimiva	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \forall t \in ran h \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol$
249		finiunmbl	$⊢ (ran h \in Fin \land \forall t \in ran h \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol) \to ⋃_{t \in ran h} \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol$
250	42 248 249	syl2anc	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ⋃_{t \in ran h} \{x \in h^{-1} [\{t\}] \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol$
251	173 250	eqeltrrd	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol$
252		unrab	$⊢ \{x \in ℝ \| h (x) \in (−∞, 0)\} \cup \{x \in ℝ \| h (x) \in (0, +∞)\} = \{x \in ℝ \| (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞))\}$
253	28	feqmptd	$⊢ h \in dom \int^{1} \to h = (x \in ℝ ⟼ h (x))$
254	253	cnveqd	$⊢ h \in dom \int^{1} \to h^{-1} = {(x \in ℝ ⟼ h (x))}^{-1}$
255	254	imaeq1d	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] = {(x \in ℝ ⟼ h (x))}^{-1} [(−∞, 0)]$
256		eqid	$⊢ (x \in ℝ ⟼ h (x)) = (x \in ℝ ⟼ h (x))$
257	256	mptpreima	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [(−∞, 0)] = \{x \in ℝ \| h (x) \in (−∞, 0)\}$
258	255 257	eqtrdi	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] = \{x \in ℝ \| h (x) \in (−∞, 0)\}$
259	254	imaeq1d	$⊢ h \in dom \int^{1} \to h^{-1} [(0, +∞)] = {(x \in ℝ ⟼ h (x))}^{-1} [(0, +∞)]$
260	256	mptpreima	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [(0, +∞)] = \{x \in ℝ \| h (x) \in (0, +∞)\}$
261	259 260	eqtrdi	$⊢ h \in dom \int^{1} \to h^{-1} [(0, +∞)] = \{x \in ℝ \| h (x) \in (0, +∞)\}$
262	258 261	uneq12d	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] \cup h^{-1} [(0, +∞)] = \{x \in ℝ \| h (x) \in (−∞, 0)\} \cup \{x \in ℝ \| h (x) \in (0, +∞)\}$
263	28	ffvelrnda	$⊢ (h \in dom \int^{1} \land x \in ℝ) \to h (x) \in ℝ$
264		0re	$⊢ 0 \in ℝ$
265		lttri2	$⊢ (h (x) \in ℝ \land 0 \in ℝ) \to (h (x) \neq 0 \leftrightarrow (h (x) < 0 \lor 0 < h (x)))$
266	264 265	mpan2	$⊢ h (x) \in ℝ \to (h (x) \neq 0 \leftrightarrow (h (x) < 0 \lor 0 < h (x)))$
267		ibar	$⊢ h (x) \in ℝ \to ((h (x) < 0 \lor 0 < h (x)) \leftrightarrow (h (x) \in ℝ \land (h (x) < 0 \lor 0 < h (x))))$
268		andi	$⊢ (h (x) \in ℝ \land (h (x) < 0 \lor 0 < h (x))) \leftrightarrow ((h (x) \in ℝ \land h (x) < 0) \lor (h (x) \in ℝ \land 0 < h (x)))$
269		0xr	$⊢ 0 \in ℝ^{*}$
270		elioomnf	$⊢ 0 \in ℝ^{*} \to (h (x) \in (−∞, 0) \leftrightarrow (h (x) \in ℝ \land h (x) < 0))$
271		elioopnf	$⊢ 0 \in ℝ^{*} \to (h (x) \in (0, +∞) \leftrightarrow (h (x) \in ℝ \land 0 < h (x)))$
272	270 271	orbi12d	$⊢ 0 \in ℝ^{*} \to ((h (x) \in (−∞, 0) \lor h (x) \in (0, +∞)) \leftrightarrow ((h (x) \in ℝ \land h (x) < 0) \lor (h (x) \in ℝ \land 0 < h (x))))$
273	269 272	ax-mp	$⊢ (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞)) \leftrightarrow ((h (x) \in ℝ \land h (x) < 0) \lor (h (x) \in ℝ \land 0 < h (x)))$
274	268 273	bitr4i	$⊢ (h (x) \in ℝ \land (h (x) < 0 \lor 0 < h (x))) \leftrightarrow (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞))$
275	267 274	bitrdi	$⊢ h (x) \in ℝ \to ((h (x) < 0 \lor 0 < h (x)) \leftrightarrow (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞)))$
276	266 275	bitrd	$⊢ h (x) \in ℝ \to (h (x) \neq 0 \leftrightarrow (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞)))$
277	263 276	syl	$⊢ (h \in dom \int^{1} \land x \in ℝ) \to (h (x) \neq 0 \leftrightarrow (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞)))$
278	277	rabbidva	$⊢ h \in dom \int^{1} \to \{x \in ℝ \| h (x) \neq 0\} = \{x \in ℝ \| (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞))\}$
279	252 262 278	3eqtr4a	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] \cup h^{-1} [(0, +∞)] = \{x \in ℝ \| h (x) \neq 0\}$
280		i1fima	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] \in dom vol$
281		i1fima	$⊢ h \in dom \int^{1} \to h^{-1} [(0, +∞)] \in dom vol$
282		unmbl	$⊢ (h^{-1} [(−∞, 0)] \in dom vol \land h^{-1} [(0, +∞)] \in dom vol) \to h^{-1} [(−∞, 0)] \cup h^{-1} [(0, +∞)] \in dom vol$
283	280 281 282	syl2anc	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] \cup h^{-1} [(0, +∞)] \in dom vol$
284	279 283	eqeltrrd	$⊢ h \in dom \int^{1} \to \{x \in ℝ \| h (x) \neq 0\} \in dom vol$
285	284	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \{x \in ℝ \| h (x) \neq 0\} \in dom vol$
286		inmbl	$⊢ (\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol \land \{x \in ℝ \| h (x) \neq 0\} \in dom vol) \to \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\} \in dom vol$
287	251 285 286	syl2anc	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\} \in dom vol$
288	287	adantr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\} \in dom vol$
289	24	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℂ$
290	289	adantlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℂ$
291		1cnd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to 1 \in ℂ$
292		simplr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to t \in ℝ$
293	14	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{v}{3} \in ℝ$
294	20	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{v}{3} \neq 0$
295	292 293 294	redivcld	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{t}{\frac{v}{3}} \in ℝ$
296	295	recnd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{t}{\frac{v}{3}} \in ℂ$
297	290 291 296	subadd2d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 = \frac{t}{\frac{v}{3}} \leftrightarrow (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋)$
298		eqcom	$⊢ ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 = \frac{t}{\frac{v}{3}} \leftrightarrow \frac{t}{\frac{v}{3}} = ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1$
299		recn	$⊢ t \in ℝ \to t \in ℂ$
300	299	ad2antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to t \in ℂ$
301	26	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \in ℂ$
302	301	adantlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \in ℂ$
303	14	recnd	$⊢ v \in ℝ^{+} \to \frac{v}{3} \in ℂ$
304	303	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{v}{3} \in ℂ$
305	300 302 304 294	divmul3d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (\frac{t}{\frac{v}{3}} = ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \leftrightarrow t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}))$
306	298 305	syl5bb	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 = \frac{t}{\frac{v}{3}} \leftrightarrow t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}))$
307	297 306	bitr3d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ((\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leftrightarrow t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}))$
308	307	rabbidva	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \{x \in ℝ \| (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋\} = \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\}$
309		imaundi	$⊢ F^{-1} [\{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\} \cup (((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] = F^{-1} [\{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\}] \cup F^{-1} [(((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))]$
310	224	ad4antr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F^{-1} = {(x \in ℝ ⟼ F (x))}^{-1}$
311		zre	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℤ \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
312	311	adantl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
313	14	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \frac{v}{3} \in ℝ$
314	312 313	remulcld	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \in ℝ$
315	314	rexrd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \in ℝ^{*}$
316		peano2z	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℤ \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℤ$
317	316	zred	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℤ \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ$
318	317	adantl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ$
319	313 318	remulcld	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1) \in ℝ$
320	319	rexrd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1) \in ℝ^{*}$
321		zcn	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℤ \to (\frac{t}{\frac{v}{3}}) + 1 \in ℂ$
322	321	adantl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (\frac{t}{\frac{v}{3}}) + 1 \in ℂ$
323	303	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \frac{v}{3} \in ℂ$
324	322 323	mulcomd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) = (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1)$
325	69	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \frac{v}{3} \in ℝ^{+}$
326	311	ltp1d	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℤ \to (\frac{t}{\frac{v}{3}}) + 1 < (\frac{t}{\frac{v}{3}}) + 1 + 1$
327	326	adantl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (\frac{t}{\frac{v}{3}}) + 1 < (\frac{t}{\frac{v}{3}}) + 1 + 1$
328	312 318 325 327	ltmul2dd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)$
329	324 328	eqbrtrd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)$
330		snunioo	$⊢ (((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \in ℝ^{} \land (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1) \in ℝ^{} \land ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) \to \{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\} \cup (((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) = [((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))$
331	315 320 329 330	syl3anc	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\} \cup (((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) = [((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))$
332	310 331	imaeq12d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F^{-1} [\{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\} \cup (((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] = {(x \in ℝ ⟼ F (x))}^{-1} [[((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))]$
333	309 332	eqtr3id	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F^{-1} [\{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\}] \cup F^{-1} [(((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] = {(x \in ℝ ⟼ F (x))}^{-1} [[((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))]$
334	226	mptpreima	$⊢ {(x \in ℝ ⟼ F (x))}^{-1} [[((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] = \{x \in ℝ \| F (x) \in [((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))\}$
335	5	ad3antrrr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F : ℝ ⟶ ℝ$
336	335	ffvelrnda	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to F (x) \in ℝ$
337	336	3biant1d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ((((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \leq F (x) \land F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) \leftrightarrow (F (x) \in ℝ \land ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \leq F (x) \land F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)))$
338	337	adantr	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to ((((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \leq F (x) \land F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) \leftrightarrow (F (x) \in ℝ \land ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \leq F (x) \land F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)))$
339	311	adantl	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
340	336	adantr	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F (x) \in ℝ$
341	69	ad4antlr	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \frac{v}{3} \in ℝ^{+}$
342	339 340 341	lemuldivd	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \leq F (x) \leftrightarrow (\frac{t}{\frac{v}{3}}) + 1 \leq \frac{F (x)}{\frac{v}{3}})$
343	317	adantl	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ$
344	340 343 341	ltdivmuld	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (\frac{F (x)}{\frac{v}{3}} < (\frac{t}{\frac{v}{3}}) + 1 + 1 \leftrightarrow F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))$
345	344	bicomd	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1) \leftrightarrow \frac{F (x)}{\frac{v}{3}} < (\frac{t}{\frac{v}{3}}) + 1 + 1)$
346	342 345	anbi12d	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to ((((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \leq F (x) \land F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) \leftrightarrow ((\frac{t}{\frac{v}{3}}) + 1 \leq \frac{F (x)}{\frac{v}{3}} \land \frac{F (x)}{\frac{v}{3}} < (\frac{t}{\frac{v}{3}}) + 1 + 1))$
347	338 346	bitr3d	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to ((F (x) \in ℝ \land ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \leq F (x) \land F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) \leftrightarrow ((\frac{t}{\frac{v}{3}}) + 1 \leq \frac{F (x)}{\frac{v}{3}} \land \frac{F (x)}{\frac{v}{3}} < (\frac{t}{\frac{v}{3}}) + 1 + 1))$
348		elico2	$⊢ (((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \in ℝ \land (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1) \in ℝ^{*}) \to (F (x) \in [((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) \leftrightarrow (F (x) \in ℝ \land ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \leq F (x) \land F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)))$
349	314 320 348	syl2anc	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (F (x) \in [((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) \leftrightarrow (F (x) \in ℝ \land ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \leq F (x) \land F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)))$
350	349	adantlr	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (F (x) \in [((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) \leftrightarrow (F (x) \in ℝ \land ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \leq F (x) \land F (x) < (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)))$
351		eqcom	$⊢ (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leftrightarrow ⌊\frac{F (x)}{\frac{v}{3}}⌋ = (\frac{t}{\frac{v}{3}}) + 1$
352	22	adantlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{F (x)}{\frac{v}{3}} \in ℝ$
353		flbi	$⊢ (\frac{F (x)}{\frac{v}{3}} \in ℝ \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ = (\frac{t}{\frac{v}{3}}) + 1 \leftrightarrow ((\frac{t}{\frac{v}{3}}) + 1 \leq \frac{F (x)}{\frac{v}{3}} \land \frac{F (x)}{\frac{v}{3}} < (\frac{t}{\frac{v}{3}}) + 1 + 1))$
354	352 353	sylan	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ = (\frac{t}{\frac{v}{3}}) + 1 \leftrightarrow ((\frac{t}{\frac{v}{3}}) + 1 \leq \frac{F (x)}{\frac{v}{3}} \land \frac{F (x)}{\frac{v}{3}} < (\frac{t}{\frac{v}{3}}) + 1 + 1))$
355	351 354	syl5bb	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to ((\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leftrightarrow ((\frac{t}{\frac{v}{3}}) + 1 \leq \frac{F (x)}{\frac{v}{3}} \land \frac{F (x)}{\frac{v}{3}} < (\frac{t}{\frac{v}{3}}) + 1 + 1))$
356	347 350 355	3bitr4d	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to (F (x) \in [((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) \leftrightarrow (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋)$
357	356	an32s	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \land x \in ℝ) \to (F (x) \in [((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1)) \leftrightarrow (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋)$
358	357	rabbidva	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \{x \in ℝ \| F (x) \in [((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))\} = \{x \in ℝ \| (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋\}$
359	334 358	syl5eq	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to {(x \in ℝ ⟼ F (x))}^{-1} [[((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] = \{x \in ℝ \| (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋\}$
360	333 359	eqtrd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F^{-1} [\{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\}] \cup F^{-1} [(((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] = \{x \in ℝ \| (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋\}$
361	1	ad4antr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F \in MblFn$
362	5	ad4antr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F : ℝ ⟶ ℝ$
363		mbfimasn	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ \land ((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}) \in ℝ) \to F^{-1} [\{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\}] \in dom vol$
364	361 362 314 363	syl3anc	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F^{-1} [\{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\}] \in dom vol$
365		mbfima	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ) \to F^{-1} [(((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] \in dom vol$
366	1 5 365	syl2anc	$⊢ φ \to F^{-1} [(((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] \in dom vol$
367	366	ad4antr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F^{-1} [(((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] \in dom vol$
368		unmbl	$⊢ (F^{-1} [\{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\}] \in dom vol \land F^{-1} [(((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] \in dom vol) \to F^{-1} [\{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\}] \cup F^{-1} [(((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] \in dom vol$
369	364 367 368	syl2anc	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F^{-1} [\{((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3})\}] \cup F^{-1} [(((\frac{t}{\frac{v}{3}}) + 1) (\frac{v}{3}), (\frac{v}{3}) ((\frac{t}{\frac{v}{3}}) + 1 + 1))] \in dom vol$
370	360 369	eqeltrrd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \{x \in ℝ \| (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋\} \in dom vol$
371		simpr	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋) \to (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋$
372	352	flcld	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℤ$
373	372	adantr	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℤ$
374	371 373	eqeltrd	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋) \to (\frac{t}{\frac{v}{3}}) + 1 \in ℤ$
375	374	stoic1a	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \land \neg (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \neg (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋$
376	375	an32s	$⊢ (((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land \neg (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \land x \in ℝ) \to \neg (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋$
377	376	ralrimiva	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land \neg (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \forall x \in ℝ \neg (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋$
378		rabeq0	$⊢ \{x \in ℝ \| (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋\} = \emptyset \leftrightarrow \forall x \in ℝ \neg (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋$
379	377 378	sylibr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land \neg (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \{x \in ℝ \| (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋\} = \emptyset$
380		0mbl	$⊢ \emptyset \in dom vol$
381	379 380	eqeltrdi	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land \neg (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to \{x \in ℝ \| (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋\} \in dom vol$
382	370 381	pm2.61dan	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \{x \in ℝ \| (\frac{t}{\frac{v}{3}}) + 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋\} \in dom vol$
383	308 382	eqeltrrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\} \in dom vol$
384		inmbl	$⊢ (\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\} \in dom vol \land \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\} \in dom vol) \to (\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\} \in dom vol$
385	288 383 384	syl2anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to (\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\} \in dom vol$
386		rabiun	$⊢ \{x \in ⋃_{t \in ran h} h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = ⋃_{t \in ran h} \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\}$
387		rabeq	$⊢ ⋃_{t \in ran h} h^{-1} [\{t\}] = ℝ \to \{x \in ⋃_{t \in ran h} h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\}$
388	169 387	syl	$⊢ h \in dom \int^{1} \to \{x \in ⋃_{t \in ran h} h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\}$
389	386 388	eqtr3id	$⊢ h \in dom \int^{1} \to ⋃_{t \in ran h} \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\}$
390	389	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ⋃_{t \in ran h} \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\}$
391	177	notbid	$⊢ (h \in dom \int^{1} \land x \in h^{-1} [\{t\}]) \to (\neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \leftrightarrow \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t)$
392	391	rabbidva	$⊢ h \in dom \int^{1} \to \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
393		inrab2	$⊢ \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}] = \{x \in (ℝ \cap h^{-1} [\{t\}]) \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
394		rabeq	$⊢ ℝ \cap h^{-1} [\{t\}] = h^{-1} [\{t\}] \to \{x \in (ℝ \cap h^{-1} [\{t\}]) \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} = \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
395	185 394	syl	$⊢ h \in dom \int^{1} \to \{x \in (ℝ \cap h^{-1} [\{t\}]) \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} = \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
396	393 395	syl5eq	$⊢ h \in dom \int^{1} \to \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}] = \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
397	392 396	eqtr4d	$⊢ h \in dom \int^{1} \to \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}]$
398	397	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} = \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}]$
399		imaundi	$⊢ F^{-1} [\{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\} \cup (⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] = F^{-1} [\{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\}] \cup F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)]$
400	14 20	jca	$⊢ v \in ℝ^{+} \to (\frac{v}{3} \in ℝ \land \frac{v}{3} \neq 0)$
401		redivcl	$⊢ (t \in ℝ \land \frac{v}{3} \in ℝ \land \frac{v}{3} \neq 0) \to \frac{t}{\frac{v}{3}} \in ℝ$
402	401	3expb	$⊢ (t \in ℝ \land (\frac{v}{3} \in ℝ \land \frac{v}{3} \neq 0)) \to \frac{t}{\frac{v}{3}} \in ℝ$
403	400 402	sylan2	$⊢ (t \in ℝ \land v \in ℝ^{+}) \to \frac{t}{\frac{v}{3}} \in ℝ$
404	403	ancoms	$⊢ (v \in ℝ^{+} \land t \in ℝ) \to \frac{t}{\frac{v}{3}} \in ℝ$
405	404	adantll	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \frac{t}{\frac{v}{3}} \in ℝ$
406	405 204	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
407		peano2re	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℝ \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ$
408		reflcl	$⊢ (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ \in ℝ$
409	406 407 408	3syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ \in ℝ$
410	14	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \frac{v}{3} \in ℝ$
411	409 410	remulcld	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \in ℝ$
412	411	rexrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \in ℝ^{*}$
413		pnfxr	$⊢ +∞ \in ℝ^{*}$
414	413	a1i	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to +∞ \in ℝ^{*}$
415		ltpnf	$⊢ ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \in ℝ \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) < +∞$
416	411 415	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) < +∞$
417		snunioo	$⊢ (⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \in ℝ^{} \land +∞ \in ℝ^{} \land ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) < +∞) \to \{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\} \cup (⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞) = [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)$
418	412 414 416 417	syl3anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\} \cup (⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞) = [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)$
419	418	imaeq2d	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F^{-1} [\{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\} \cup (⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] = F^{-1} [[⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)]$
420	399 419	eqtr3id	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F^{-1} [\{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\}] \cup F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] = F^{-1} [[⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)]$
421	224	imaeq1d	$⊢ φ \to F^{-1} [[⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] = {(x \in ℝ ⟼ F (x))}^{-1} [[⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)]$
422	226	mptpreima	$⊢ {(x \in ℝ ⟼ F (x))}^{-1} [[⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] = \{x \in ℝ \| F (x) \in [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)\}$
423	421 422	eqtrdi	$⊢ φ \to F^{-1} [[⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] = \{x \in ℝ \| F (x) \in [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)\}$
424	423	ad3antrrr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F^{-1} [[⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] = \{x \in ℝ \| F (x) \in [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)\}$
425	406 407	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ$
426	425	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ$
427		flflp1	$⊢ ((\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ \land \frac{F (x)}{\frac{v}{3}} \in ℝ) \to (⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ \leq \frac{F (x)}{\frac{v}{3}} \leftrightarrow (\frac{t}{\frac{v}{3}}) + 1 + 1 < ⌊\frac{F (x)}{\frac{v}{3}}⌋ + 1)$
428	426 352 427	syl2anc	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ \leq \frac{F (x)}{\frac{v}{3}} \leftrightarrow (\frac{t}{\frac{v}{3}}) + 1 + 1 < ⌊\frac{F (x)}{\frac{v}{3}}⌋ + 1)$
429	411	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \in ℝ$
430		elicopnf	$⊢ ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \in ℝ \to (F (x) \in [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞) \leftrightarrow (F (x) \in ℝ \land ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \leq F (x)))$
431	429 430	syl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (F (x) \in [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞) \leftrightarrow (F (x) \in ℝ \land ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \leq F (x)))$
432	336	biantrurd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \leq F (x) \leftrightarrow (F (x) \in ℝ \land ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \leq F (x)))$
433	409	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ \in ℝ$
434	69	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{v}{3} \in ℝ^{+}$
435	433 336 434	lemuldivd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \leq F (x) \leftrightarrow ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ \leq \frac{F (x)}{\frac{v}{3}})$
436	431 432 435	3bitr2d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (F (x) \in [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞) \leftrightarrow ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ \leq \frac{F (x)}{\frac{v}{3}})$
437	406	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
438	352 23	syl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℝ$
439		1red	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to 1 \in ℝ$
440	437 438 439	ltadd1d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ((\frac{t}{\frac{v}{3}}) + 1 < ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leftrightarrow (\frac{t}{\frac{v}{3}}) + 1 + 1 < ⌊\frac{F (x)}{\frac{v}{3}}⌋ + 1)$
441	428 436 440	3bitr4d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (F (x) \in [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞) \leftrightarrow (\frac{t}{\frac{v}{3}}) + 1 < ⌊\frac{F (x)}{\frac{v}{3}}⌋)$
442	295 439 438	ltaddsubd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ((\frac{t}{\frac{v}{3}}) + 1 < ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leftrightarrow \frac{t}{\frac{v}{3}} < ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1)$
443	441 442	bitrd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (F (x) \in [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞) \leftrightarrow \frac{t}{\frac{v}{3}} < ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1)$
444	438 25	syl	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \in ℝ$
445	292 444 434	ltdivmul2d	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (\frac{t}{\frac{v}{3}} < ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \leftrightarrow t < (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}))$
446	444 293	remulcld	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in ℝ$
447	292 446	ltnled	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (t < (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leftrightarrow \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t)$
448	443 445 447	3bitrd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (F (x) \in [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞) \leftrightarrow \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t)$
449	448	rabbidva	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \{x \in ℝ \| F (x) \in [⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)\} = \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
450	420 424 449	3eqtrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F^{-1} [\{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\}] \cup F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] = \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\}$
451	1	ad3antrrr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F \in MblFn$
452		mbfimasn	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ \land ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \in ℝ) \to F^{-1} [\{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\}] \in dom vol$
453	451 335 411 452	syl3anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F^{-1} [\{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\}] \in dom vol$
454		mbfima	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ) \to F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] \in dom vol$
455	1 5 454	syl2anc	$⊢ φ \to F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] \in dom vol$
456	455	ad3antrrr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] \in dom vol$
457		unmbl	$⊢ (F^{-1} [\{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\}] \in dom vol \land F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] \in dom vol) \to F^{-1} [\{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\}] \cup F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] \in dom vol$
458	453 456 457	syl2anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F^{-1} [\{⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3})\}] \cup F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] \in dom vol$
459	450 458	eqeltrrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \in dom vol$
460	237 459	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \in dom vol$
461		inmbl	$⊢ (\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \in dom vol \land h^{-1} [\{t\}] \in dom vol) \to \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}] \in dom vol$
462	460 244 461	syl2anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq t\} \cap h^{-1} [\{t\}] \in dom vol$
463	398 462	eqeltrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol$
464	463	ralrimiva	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \forall t \in ran h \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol$
465		finiunmbl	$⊢ (ran h \in Fin \land \forall t \in ran h \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol) \to ⋃_{t \in ran h} \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol$
466	42 464 465	syl2anc	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ⋃_{t \in ran h} \{x \in h^{-1} [\{t\}] \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol$
467	390 466	eqeltrrd	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol$
468	254	imaeq1d	$⊢ h \in dom \int^{1} \to h^{-1} [\{0\}] = {(x \in ℝ ⟼ h (x))}^{-1} [\{0\}]$
469	256	mptpreima	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [\{0\}] = \{x \in ℝ \| h (x) \in \{0\}\}$
470	141	elsn	$⊢ h (x) \in \{0\} \leftrightarrow h (x) = 0$
471	470	rabbii	$⊢ \{x \in ℝ \| h (x) \in \{0\}\} = \{x \in ℝ \| h (x) = 0\}$
472	469 471	eqtri	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [\{0\}] = \{x \in ℝ \| h (x) = 0\}$
473	468 472	eqtrdi	$⊢ h \in dom \int^{1} \to h^{-1} [\{0\}] = \{x \in ℝ \| h (x) = 0\}$
474		i1fima	$⊢ h \in dom \int^{1} \to h^{-1} [\{0\}] \in dom vol$
475	473 474	eqeltrrd	$⊢ h \in dom \int^{1} \to \{x \in ℝ \| h (x) = 0\} \in dom vol$
476	475	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \{x \in ℝ \| h (x) = 0\} \in dom vol$
477		unmbl	$⊢ (\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \in dom vol \land \{x \in ℝ \| h (x) = 0\} \in dom vol) \to \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\} \in dom vol$
478	467 476 477	syl2anc	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\} \in dom vol$
479	478	adantr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\} \in dom vol$
480	254	imaeq1d	$⊢ h \in dom \int^{1} \to h^{-1} [\{t\}] = {(x \in ℝ ⟼ h (x))}^{-1} [\{t\}]$
481	256	mptpreima	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [\{t\}] = \{x \in ℝ \| h (x) \in \{t\}\}$
482	141	elsn	$⊢ h (x) \in \{t\} \leftrightarrow h (x) = t$
483		eqcom	$⊢ h (x) = t \leftrightarrow t = h (x)$
484	482 483	bitri	$⊢ h (x) \in \{t\} \leftrightarrow t = h (x)$
485	484	rabbii	$⊢ \{x \in ℝ \| h (x) \in \{t\}\} = \{x \in ℝ \| t = h (x)\}$
486	481 485	eqtri	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [\{t\}] = \{x \in ℝ \| t = h (x)\}$
487	480 486	eqtrdi	$⊢ h \in dom \int^{1} \to h^{-1} [\{t\}] = \{x \in ℝ \| t = h (x)\}$
488	487	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to h^{-1} [\{t\}] = \{x \in ℝ \| t = h (x)\}$
489	488 243	eqeltrrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \{x \in ℝ \| t = h (x)\} \in dom vol$
490		inmbl	$⊢ (\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\} \in dom vol \land \{x \in ℝ \| t = h (x)\} \in dom vol) \to (\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\} \in dom vol$
491	479 489 490	syl2anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to (\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\} \in dom vol$
492		unmbl	$⊢ ((\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\} \in dom vol \land (\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\} \in dom vol) \to ((\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\}) \cup ((\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\}) \in dom vol$
493	385 491 492	syl2anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to ((\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\}) \cup ((\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\}) \in dom vol$
494	160 493	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\})) \to ((\{x \in ℝ \| (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cap \{x \in ℝ \| h (x) \neq 0\}) \cap \{x \in ℝ \| t = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})\}) \cup ((\{x \in ℝ \| \neg (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x)\} \cup \{x \in ℝ \| h (x) = 0\}) \cap \{x \in ℝ \| t = h (x)\}) \in dom vol$
495	155 494	eqeltrid	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\})) \to {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \in dom vol$
496		mblvol	$⊢ {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \in dom vol \to vol ({(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}]) = {vol}^{*} ({(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}])$
497	495 496	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\})) \to vol ({(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}]) = {vol}^{*} ({(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}])$
498		eldifsn	$⊢ t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\}) \leftrightarrow (t \in ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) \land t \neq 0)$
499	158	anim1d	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ((t \in ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) \land t \neq 0) \to (t \in ℝ \land t \neq 0))$
500	498 499	syl5bi	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\}) \to (t \in ℝ \land t \neq 0))$
501	500	imdistani	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\})) \to (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0))$
502	129	a1i	$⊢ h \in dom \int^{1} \to {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] = \{x \in ℝ \| if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\}\}$
503	468 469	eqtrdi	$⊢ h \in dom \int^{1} \to h^{-1} [\{0\}] = \{x \in ℝ \| h (x) \in \{0\}\}$
504	502 503	ineq12d	$⊢ h \in dom \int^{1} \to {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \cap h^{-1} [\{0\}] = \{x \in ℝ \| if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\}\} \cap \{x \in ℝ \| h (x) \in \{0\}\}$
505		inrab	$⊢ \{x \in ℝ \| if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\}\} \cap \{x \in ℝ \| h (x) \in \{0\}\} = \{x \in ℝ \| (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\})\}$
506	504 505	eqtrdi	$⊢ h \in dom \int^{1} \to {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \cap h^{-1} [\{0\}] = \{x \in ℝ \| (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\})\}$
507	506	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0)) \to {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \cap h^{-1} [\{0\}] = \{x \in ℝ \| (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\})\}$
508	145	biimpri	$⊢ h (x) = 0 \to \neg h (x) \neq 0$
509	508	intnand	$⊢ h (x) = 0 \to \neg ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)$
510	509	iffalsed	$⊢ h (x) = 0 \to if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) = h (x)$
511		eqtr	$⊢ (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) = h (x) \land h (x) = 0) \to if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) = 0$
512	510 511	mpancom	$⊢ h (x) = 0 \to if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) = 0$
513	512	adantl	$⊢ ((t \neq 0 \land x \in ℝ) \land h (x) = 0) \to if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) = 0$
514		simpll	$⊢ ((t \neq 0 \land x \in ℝ) \land h (x) = 0) \to t \neq 0$
515	514	necomd	$⊢ ((t \neq 0 \land x \in ℝ) \land h (x) = 0) \to 0 \neq t$
516	513 515	eqnetrd	$⊢ ((t \neq 0 \land x \in ℝ) \land h (x) = 0) \to if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \neq t$
517	516	ex	$⊢ (t \neq 0 \land x \in ℝ) \to (h (x) = 0 \to if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \neq t)$
518		orcom	$⊢ (\neg if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \lor \neg h (x) \in \{0\}) \leftrightarrow (\neg h (x) \in \{0\} \lor \neg if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\})$
519		ianor	$⊢ \neg (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\}) \leftrightarrow (\neg if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \lor \neg h (x) \in \{0\})$
520		imor	$⊢ (h (x) \in \{0\} \to \neg if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\}) \leftrightarrow (\neg h (x) \in \{0\} \lor \neg if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\})$
521	518 519 520	3bitr4i	$⊢ \neg (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\}) \leftrightarrow (h (x) \in \{0\} \to \neg if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\})$
522	143	necon3bbii	$⊢ \neg if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \leftrightarrow if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \neq t$
523	470 522	imbi12i	$⊢ (h (x) \in \{0\} \to \neg if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\}) \leftrightarrow (h (x) = 0 \to if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \neq t)$
524	521 523	bitri	$⊢ \neg (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\}) \leftrightarrow (h (x) = 0 \to if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \neq t)$
525	517 524	sylibr	$⊢ (t \neq 0 \land x \in ℝ) \to \neg (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\})$
526	525	ralrimiva	$⊢ t \neq 0 \to \forall x \in ℝ \neg (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\})$
527		rabeq0	$⊢ \{x \in ℝ \| (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\})\} = \emptyset \leftrightarrow \forall x \in ℝ \neg (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\})$
528	526 527	sylibr	$⊢ t \neq 0 \to \{x \in ℝ \| (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\})\} = \emptyset$
529	528	ad2antll	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0)) \to \{x \in ℝ \| (if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)) \in \{t\} \land h (x) \in \{0\})\} = \emptyset$
530	507 529	eqtrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0)) \to {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \cap h^{-1} [\{0\}] = \emptyset$
531		imassrn	$⊢ {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \subseteq ran {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1}$
532		dfdm4	$⊢ dom (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) = ran {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1}$
533	142 128	dmmpti	$⊢ dom (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) = ℝ$
534	532 533	eqtr3i	$⊢ ran {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} = ℝ$
535	531 534	sseqtri	$⊢ {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \subseteq ℝ$
536		reldisj	$⊢ {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \subseteq ℝ \to ({(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \cap h^{-1} [\{0\}] = \emptyset \leftrightarrow {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \subseteq ℝ ∖ h^{-1} [\{0\}])$
537	535 536	ax-mp	$⊢ {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \cap h^{-1} [\{0\}] = \emptyset \leftrightarrow {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \subseteq ℝ ∖ h^{-1} [\{0\}]$
538	530 537	sylib	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0)) \to {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \subseteq ℝ ∖ h^{-1} [\{0\}]$
539		ffun	$⊢ h : ℝ ⟶ ℝ \to Fun h$
540		difpreima	$⊢ Fun h \to h^{-1} [ran h ∖ \{0\}] = h^{-1} [ran h] ∖ h^{-1} [\{0\}]$
541	539 540	syl	$⊢ h : ℝ ⟶ ℝ \to h^{-1} [ran h ∖ \{0\}] = h^{-1} [ran h] ∖ h^{-1} [\{0\}]$
542		fdm	$⊢ h : ℝ ⟶ ℝ \to dom h = ℝ$
543	162 542	syl5eq	$⊢ h : ℝ ⟶ ℝ \to h^{-1} [ran h] = ℝ$
544	543	difeq1d	$⊢ h : ℝ ⟶ ℝ \to h^{-1} [ran h] ∖ h^{-1} [\{0\}] = ℝ ∖ h^{-1} [\{0\}]$
545	541 544	eqtrd	$⊢ h : ℝ ⟶ ℝ \to h^{-1} [ran h ∖ \{0\}] = ℝ ∖ h^{-1} [\{0\}]$
546	28 545	syl	$⊢ h \in dom \int^{1} \to h^{-1} [ran h ∖ \{0\}] = ℝ ∖ h^{-1} [\{0\}]$
547	546	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0)) \to h^{-1} [ran h ∖ \{0\}] = ℝ ∖ h^{-1} [\{0\}]$
548	538 547	sseqtrrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0)) \to {(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \subseteq h^{-1} [ran h ∖ \{0\}]$
549		imassrn	$⊢ h^{-1} [ran h ∖ \{0\}] \subseteq ran h^{-1}$
550	549 182	sseqtrid	$⊢ h \in dom \int^{1} \to h^{-1} [ran h ∖ \{0\}] \subseteq ℝ$
551	550	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0)) \to h^{-1} [ran h ∖ \{0\}] \subseteq ℝ$
552		i1fima	$⊢ h \in dom \int^{1} \to h^{-1} [ran h ∖ \{0\}] \in dom vol$
553		mblvol	$⊢ h^{-1} [ran h ∖ \{0\}] \in dom vol \to vol (h^{-1} [ran h ∖ \{0\}]) = {vol}^{*} (h^{-1} [ran h ∖ \{0\}])$
554	552 553	syl	$⊢ h \in dom \int^{1} \to vol (h^{-1} [ran h ∖ \{0\}]) = {vol}^{*} (h^{-1} [ran h ∖ \{0\}])$
555		neldifsn	$⊢ \neg 0 \in (ran h ∖ \{0\})$
556		i1fima2	$⊢ (h \in dom \int^{1} \land \neg 0 \in (ran h ∖ \{0\})) \to vol (h^{-1} [ran h ∖ \{0\}]) \in ℝ$
557	555 556	mpan2	$⊢ h \in dom \int^{1} \to vol (h^{-1} [ran h ∖ \{0\}]) \in ℝ$
558	554 557	eqeltrrd	$⊢ h \in dom \int^{1} \to {vol}^{*} (h^{-1} [ran h ∖ \{0\}]) \in ℝ$
559	558	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0)) \to {vol}^{*} (h^{-1} [ran h ∖ \{0\}]) \in ℝ$
560		ovolsscl	$⊢ ({(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}] \subseteq h^{-1} [ran h ∖ \{0\}] \land h^{-1} [ran h ∖ \{0\}] \subseteq ℝ \land {vol}^{} (h^{-1} [ran h ∖ \{0\}]) \in ℝ) \to {vol}^{} ({(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}]) \in ℝ$
561	548 551 559 560	syl3anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0)) \to {vol}^{*} ({(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}]) \in ℝ$
562	501 561	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\})) \to {vol}^{*} ({(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}]) \in ℝ$
563	497 562	eqeltrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in (ran (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) ∖ \{0\})) \to vol ({(x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x)))}^{-1} [\{t\}]) \in ℝ$
564	32 127 495 563	i1fd	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (x \in ℝ ⟼ if (((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0), (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}), h (x))) \in dom \int^{1}$

Metamath Proof Explorer

Theorem itg2addnclem2

Proof