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		3nn	$⊢ 3 \in ℕ$
46		nnrp	$⊢ 3 \in ℕ \to 3 \in ℝ^{+}$
47	45 46	ax-mp	$⊢ 3 \in ℝ^{+}$
48		rpdivcl	$⊢ (v \in ℝ^{+} \land 3 \in ℝ^{+}) \to \frac{v}{3} \in ℝ^{+}$
49	47 48	mpan2	$⊢ v \in ℝ^{+} \to \frac{v}{3} \in ℝ^{+}$
50	49	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to \frac{v}{3} \in ℝ^{+}$
51	2	ad2antrr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to F : ℝ ⟶ [0, +∞)$
52	51	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to F (x) \in [0, +∞)$
53		elrege0	$⊢ F (x) \in [0, +∞) \leftrightarrow (F (x) \in ℝ \land 0 \leq F (x))$
54	52 53	sylib	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (F (x) \in ℝ \land 0 \leq F (x))$
55	54	simprd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to 0 \leq F (x)$
56	7 50 55	divge0d	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to 0 \leq \frac{F (x)}{\frac{v}{3}}$
57		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}$
58	22 56 57	syl2anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℕ_{0}$
59	58	nn0ge0d	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to 0 \leq ⌊\frac{F (x)}{\frac{v}{3}}⌋$
60	59	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}}⌋$
61	28	frnd	$⊢ h \in dom \int^{1} \to ran h \subseteq ℝ$
62		i1f0rn	$⊢ h \in dom \int^{1} \to 0 \in ran h$
63		elex2	$⊢ 0 \in ran h \to \exists x x \in ran h$
64	62 63	syl	$⊢ h \in dom \int^{1} \to \exists x x \in ran h$
65		n0	$⊢ ran h \neq \emptyset \leftrightarrow \exists x x \in ran h$
66	64 65	sylibr	$⊢ h \in dom \int^{1} \to ran h \neq \emptyset$
67		fimaxre2	$⊢ (ran h \subseteq ℝ \land ran h \in Fin) \to \exists x \in ℝ \forall y \in ran h y \leq x$
68	61 41 67	syl2anc	$⊢ h \in dom \int^{1} \to \exists x \in ℝ \forall y \in ran h y \leq x$
69	61 66 68	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)$
70	69	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)$
71		ffn	$⊢ h : ℝ ⟶ ℝ \to h Fn ℝ$
72	28 71	syl	$⊢ h \in dom \int^{1} \to h Fn ℝ$
73		dffn3	$⊢ h Fn ℝ \leftrightarrow h : ℝ ⟶ ran h$
74	72 73	sylib	$⊢ h \in dom \int^{1} \to h : ℝ ⟶ ran h$
75	74	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to h : ℝ ⟶ ran h$
76	75	ffvelrnda	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to h (x) \in ran h$
77		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 ℝ <)$
78	70 76 77	syl2anc	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to h (x) \leq sup (ran h ℝ <)$
79		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 ℝ$
80	61 66 68 79	syl3anc	$⊢ h \in dom \int^{1} \to sup (ran h ℝ <) \in ℝ$
81	80	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to sup (ran h ℝ <) \in ℝ$
82		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 ℝ <))$
83	27 30 81 82	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 ℝ <))$
84	26 81 50	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}})$
85		1red	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to 1 \in ℝ$
86	81 15 21	redivcld	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to \frac{sup (ran h ℝ <)}{\frac{v}{3}} \in ℝ$
87	24 85 86	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)$
88	84 87	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)$
89		peano2re	$⊢ \frac{sup (ran h ℝ <)}{\frac{v}{3}} \in ℝ \to (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \in ℝ$
90	86 89	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \in ℝ$
91		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)⌋$
92	90 91	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)⌋$
93		ceicl	$⊢ (\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1 \in ℝ \to - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋ \in ℤ$
94	90 93	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋ \in ℤ$
95	94	zred	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋ \in ℝ$
96		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)⌋)$
97	24 90 95 96	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)⌋)$
98	92 97	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)⌋)$
99	88 98	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)⌋)$
100	83 99	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)⌋)$
101	78 100	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)⌋)$
102	101	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)⌋)$
103	102	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)⌋$
104	22	flcld	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℤ$
105	104	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 ℤ$
106		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 ℤ$
107	94	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 ℤ$
108		elfz	$⊢ (⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℤ \land 0 \in ℤ \land - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋ \in ℤ) \to (⌊\frac{F (x)}{\frac{v}{3}}⌋ \in (0 \dots - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋) \leftrightarrow (0 \leq ⌊\frac{F (x)}{\frac{v}{3}}⌋ \land ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋))$
109	105 106 107 108	syl3anc	$⊢ ((((φ \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)⌋) \leftrightarrow (0 \leq ⌊\frac{F (x)}{\frac{v}{3}}⌋ \land ⌊\frac{F (x)}{\frac{v}{3}}⌋ \leq - ⌊- ((\frac{sup (ran h ℝ <)}{\frac{v}{3}}) + 1)⌋))$
110	60 103 109	mpbir2and	$⊢ ((((φ \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)⌋)$
111		eqid	$⊢ (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})$
112		oveq1	$⊢ t = ⌊\frac{F (x)}{\frac{v}{3}}⌋ \to t - 1 = ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1$
113	112	oveq1d	$⊢ t = ⌊\frac{F (x)}{\frac{v}{3}}⌋ \to (t - 1) (\frac{v}{3}) = (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3})$
114	113	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})$
115	110 111 114	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})$
116		ovex	$⊢ (⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \in V$
117	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}))$
118	116 117	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})$
119	115 118	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}))$
120		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)$
121	119 120	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)$
122		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)$
123	76 122	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)$
124	123	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)$
125	121 124	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)$
126	125	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$
127	126	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$
128		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$
129	44 127 128	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$
130		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)))$
131	130	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\}\}$
132		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)))\}$
133		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)\}$
134	133	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})\}$
135		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}))\}$
136	134 135	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}))\}$
137		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)\}$
138	137	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)\}$
139		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))\}$
140	138 139	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))\}$
141	136 140	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))\}$
142		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))$
143		fvex	$⊢ h (x) \in V$
144	116 143	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$
145	144	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$
146		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)$
147		nne	$⊢ \neg h (x) \neq 0 \leftrightarrow h (x) = 0$
148	147	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)$
149	146 148	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)$
150	149	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))$
151	150	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)))$
152		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)))$
153	151 152	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))$
154	142 145 153	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)))$
155	154	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)))\}$
156	132 141 155	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)\})$
157	131 156	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)\})$
158		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)))$
159	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 ℝ$
160	159	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 ℝ)$
161	158 160	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 ℝ)$
162	161	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 ℝ)$
163		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)\}$
164		cnvimarndm	$⊢ h^{-1} [ran h] = dom h$
165		iunid	$⊢ ⋃_{t \in ran h} \{t\} = ran h$
166	165	imaeq2i	$⊢ h^{-1} [⋃_{t \in ran h} \{t\}] = h^{-1} [ran h]$
167		imaiun	$⊢ h^{-1} [⋃_{t \in ran h} \{t\}] = ⋃_{t \in ran h} h^{-1} [\{t\}]$
168	166 167	eqtr3i	$⊢ h^{-1} [ran h] = ⋃_{t \in ran h} h^{-1} [\{t\}]$
169	164 168	eqtr3i	$⊢ dom h = ⋃_{t \in ran h} h^{-1} [\{t\}]$
170	28	fdmd	$⊢ h \in dom \int^{1} \to dom h = ℝ$
171	169 170	syl5eqr	$⊢ h \in dom \int^{1} \to ⋃_{t \in ran h} h^{-1} [\{t\}] = ℝ$
172	171	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ⋃_{t \in ran h} h^{-1} [\{t\}] = ℝ$
173		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)\}$
174	172 173	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)\}$
175	163 174	syl5eqr	$⊢ ((φ \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)\}$
176		fniniseg	$⊢ h Fn ℝ \to (x \in h^{-1} [\{t\}] \leftrightarrow (x \in ℝ \land h (x) = t))$
177	28 71 176	3syl	$⊢ h \in dom \int^{1} \to (x \in h^{-1} [\{t\}] \leftrightarrow (x \in ℝ \land h (x) = t))$
178	177	simplbda	$⊢ (h \in dom \int^{1} \land x \in h^{-1} [\{t\}]) \to h (x) = t$
179	178	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)$
180	179	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\}$
181		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\}$
182		imassrn	$⊢ h^{-1} [\{t\}] \subseteq ran h^{-1}$
183		dfdm4	$⊢ dom h = ran h^{-1}$
184	183 170	syl5eqr	$⊢ h \in dom \int^{1} \to ran h^{-1} = ℝ$
185	182 184	sseqtrid	$⊢ h \in dom \int^{1} \to h^{-1} [\{t\}] \subseteq ℝ$
186		sseqin2	$⊢ h^{-1} [\{t\}] \subseteq ℝ \leftrightarrow ℝ \cap h^{-1} [\{t\}] = h^{-1} [\{t\}]$
187	185 186	sylib	$⊢ h \in dom \int^{1} \to ℝ \cap h^{-1} [\{t\}] = h^{-1} [\{t\}]$
188		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\}$
189	187 188	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\}$
190	181 189	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\}$
191	180 190	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\}]$
192	191	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\}]$
193	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 ℝ$
194	61	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to ran h \subseteq ℝ$
195	194	sselda	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to t \in ℝ$
196	195	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to t \in ℝ$
197	49	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to \frac{v}{3} \in ℝ^{+}$
198	193 196 197	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}})$
199	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 ℝ$
200		1red	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to 1 \in ℝ$
201	14	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to \frac{v}{3} \in ℝ$
202	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$
203	196 201 202	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 ℝ$
204	199 200 203	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)$
205	7	adantlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \land x \in ℝ) \to F (x) \in ℝ$
206		peano2re	$⊢ \frac{t}{\frac{v}{3}} \in ℝ \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
207	203 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		reflcl	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℝ \to ⌊(\frac{t}{\frac{v}{3}}) + 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⌋ \in ℝ$
210		peano2re	$⊢ ⌊(\frac{t}{\frac{v}{3}}) + 1⌋ \in ℝ \to ⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1 \in ℝ$
211	209 210	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 ℝ$
212	205 211 197	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))$
213	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 ℝ$
214		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)$
215	213 207 214	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)$
216	201 211	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 ℝ$
217	216	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 ℝ^{*}$
218		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)))$
219	217 218	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)))$
220	205	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)))$
221	219 220	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))$
222	212 215 221	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)))$
223	198 204 222	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)))$
224	223	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))\}$
225	2	feqmptd	$⊢ φ \to F = (x \in ℝ ⟼ F (x))$
226	225	cnveqd	$⊢ φ \to F^{-1} = {(x \in ℝ ⟼ F (x))}^{-1}$
227	226	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))]$
228		eqid	$⊢ (x \in ℝ ⟼ F (x)) = (x \in ℝ ⟼ F (x))$
229	228	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))\}$
230	227 229	syl6eq	$⊢ φ \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))\}$
231	230	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))\}$
232	224 231	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))]$
233		mbfima	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ) \to F^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))] \in dom vol$
234	1 5 233	syl2anc	$⊢ φ \to F^{-1} [(−∞, (\frac{v}{3}) (⌊(\frac{t}{\frac{v}{3}}) + 1⌋ + 1))] \in dom vol$
235	234	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$
236	232 235	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$
237	61	sseld	$⊢ h \in dom \int^{1} \to (t \in ran h \to t \in ℝ)$
238	237	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (t \in ran h \to t \in ℝ)$
239	238	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 ℝ)$
240		i1fmbf	$⊢ h \in dom \int^{1} \to h \in MblFn$
241	240 28	jca	$⊢ h \in dom \int^{1} \to (h \in MblFn \land h : ℝ ⟶ ℝ)$
242	241	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to (h \in MblFn \land h : ℝ ⟶ ℝ)$
243		mbfimasn	$⊢ (h \in MblFn \land h : ℝ ⟶ ℝ \land t \in ℝ) \to h^{-1} [\{t\}] \in dom vol$
244	243	3expa	$⊢ ((h \in MblFn \land h : ℝ ⟶ ℝ) \land t \in ℝ) \to h^{-1} [\{t\}] \in dom vol$
245	242 244	sylan	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to h^{-1} [\{t\}] \in dom vol$
246	239 245	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ran h) \to h^{-1} [\{t\}] \in dom vol$
247		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$
248	236 246 247	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$
249	192 248	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$
250	249	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$
251		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$
252	42 250 251	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$
253	175 252	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$
254		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, +∞))\}$
255	28	feqmptd	$⊢ h \in dom \int^{1} \to h = (x \in ℝ ⟼ h (x))$
256	255	cnveqd	$⊢ h \in dom \int^{1} \to h^{-1} = {(x \in ℝ ⟼ h (x))}^{-1}$
257	256	imaeq1d	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] = {(x \in ℝ ⟼ h (x))}^{-1} [(−∞, 0)]$
258		eqid	$⊢ (x \in ℝ ⟼ h (x)) = (x \in ℝ ⟼ h (x))$
259	258	mptpreima	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [(−∞, 0)] = \{x \in ℝ \| h (x) \in (−∞, 0)\}$
260	257 259	syl6eq	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] = \{x \in ℝ \| h (x) \in (−∞, 0)\}$
261	256	imaeq1d	$⊢ h \in dom \int^{1} \to h^{-1} [(0, +∞)] = {(x \in ℝ ⟼ h (x))}^{-1} [(0, +∞)]$
262	258	mptpreima	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [(0, +∞)] = \{x \in ℝ \| h (x) \in (0, +∞)\}$
263	261 262	syl6eq	$⊢ h \in dom \int^{1} \to h^{-1} [(0, +∞)] = \{x \in ℝ \| h (x) \in (0, +∞)\}$
264	260 263	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, +∞)\}$
265	28	ffvelrnda	$⊢ (h \in dom \int^{1} \land x \in ℝ) \to h (x) \in ℝ$
266		0re	$⊢ 0 \in ℝ$
267		lttri2	$⊢ (h (x) \in ℝ \land 0 \in ℝ) \to (h (x) \neq 0 \leftrightarrow (h (x) < 0 \lor 0 < h (x)))$
268	266 267	mpan2	$⊢ h (x) \in ℝ \to (h (x) \neq 0 \leftrightarrow (h (x) < 0 \lor 0 < h (x)))$
269		ibar	$⊢ h (x) \in ℝ \to ((h (x) < 0 \lor 0 < h (x)) \leftrightarrow (h (x) \in ℝ \land (h (x) < 0 \lor 0 < h (x))))$
270		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)))$
271		0xr	$⊢ 0 \in ℝ^{*}$
272		elioomnf	$⊢ 0 \in ℝ^{*} \to (h (x) \in (−∞, 0) \leftrightarrow (h (x) \in ℝ \land h (x) < 0))$
273		elioopnf	$⊢ 0 \in ℝ^{*} \to (h (x) \in (0, +∞) \leftrightarrow (h (x) \in ℝ \land 0 < h (x)))$
274	272 273	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))))$
275	271 274	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)))$
276	270 275	bitr4i	$⊢ (h (x) \in ℝ \land (h (x) < 0 \lor 0 < h (x))) \leftrightarrow (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞))$
277	269 276	syl6bb	$⊢ h (x) \in ℝ \to ((h (x) < 0 \lor 0 < h (x)) \leftrightarrow (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞)))$
278	268 277	bitrd	$⊢ h (x) \in ℝ \to (h (x) \neq 0 \leftrightarrow (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞)))$
279	265 278	syl	$⊢ (h \in dom \int^{1} \land x \in ℝ) \to (h (x) \neq 0 \leftrightarrow (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞)))$
280	279	rabbidva	$⊢ h \in dom \int^{1} \to \{x \in ℝ \| h (x) \neq 0\} = \{x \in ℝ \| (h (x) \in (−∞, 0) \lor h (x) \in (0, +∞))\}$
281	254 264 280	3eqtr4a	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] \cup h^{-1} [(0, +∞)] = \{x \in ℝ \| h (x) \neq 0\}$
282		i1fima	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] \in dom vol$
283		i1fima	$⊢ h \in dom \int^{1} \to h^{-1} [(0, +∞)] \in dom vol$
284		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$
285	282 283 284	syl2anc	$⊢ h \in dom \int^{1} \to h^{-1} [(−∞, 0)] \cup h^{-1} [(0, +∞)] \in dom vol$
286	281 285	eqeltrrd	$⊢ h \in dom \int^{1} \to \{x \in ℝ \| h (x) \neq 0\} \in dom vol$
287	286	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \{x \in ℝ \| h (x) \neq 0\} \in dom vol$
288		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$
289	253 287 288	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$
290	289	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$
291	24	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℂ$
292	291	adantlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℂ$
293		1cnd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to 1 \in ℂ$
294		simplr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to t \in ℝ$
295	14	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{v}{3} \in ℝ$
296	20	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{v}{3} \neq 0$
297	294 295 296	redivcld	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{t}{\frac{v}{3}} \in ℝ$
298	297	recnd	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{t}{\frac{v}{3}} \in ℂ$
299	292 293 298	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}}⌋)$
300		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$
301		recn	$⊢ t \in ℝ \to t \in ℂ$
302	301	ad2antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to t \in ℂ$
303	26	recnd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1 \in ℂ$
304	303	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 ℂ$
305	14	recnd	$⊢ v \in ℝ^{+} \to \frac{v}{3} \in ℂ$
306	305	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{v}{3} \in ℂ$
307	302 304 306 296	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}))$
308	300 307	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}))$
309	299 308	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}))$
310	309	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})\}$
311		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))]$
312	226	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}$
313		zre	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℤ \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
314	313	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 ℝ$
315	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 ℝ$
316	314 315	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 ℝ$
317	316	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 ℝ^{*}$
318		peano2z	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℤ \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℤ$
319	318	zred	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℤ \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ$
320	319	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 ℝ$
321	315 320	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 ℝ$
322	321	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 ℝ^{*}$
323		zcn	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℤ \to (\frac{t}{\frac{v}{3}}) + 1 \in ℂ$
324	323	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 ℂ$
325	305	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	324 325	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)$
327	49	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 ℝ^{+}$
328	313	ltp1d	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℤ \to (\frac{t}{\frac{v}{3}}) + 1 < (\frac{t}{\frac{v}{3}}) + 1 + 1$
329	328	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$
330	314 320 327 329	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)$
331	326 330	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)$
332		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))$
333	317 322 331 332	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))$
334	312 333	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))]$
335	311 334	syl5eqr	$⊢ ((((φ \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))]$
336	228	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))\}$
337	5	ad3antrrr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F : ℝ ⟶ ℝ$
338	337	ffvelrnda	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to F (x) \in ℝ$
339	338	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)))$
340	339	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)))$
341	313	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 ℝ$
342	338	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 ℝ$
343	49	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 ℝ^{+}$
344	341 342 343	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}})$
345	319	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 ℝ$
346	342 345 343	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))$
347	346	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)$
348	344 347	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))$
349	340 348	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))$
350		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)))$
351	316 322 350	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)))$
352	351	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)))$
353		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$
354	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 ℝ$
355		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))$
356	354 355	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))$
357	353 356	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))$
358	349 352 357	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}}⌋)$
359	358	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}}⌋)$
360	359	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}}⌋\}$
361	336 360	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}}⌋\}$
362	335 361	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}}⌋\}$
363	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$
364	5	ad4antr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land (\frac{t}{\frac{v}{3}}) + 1 \in ℤ) \to F : ℝ ⟶ ℝ$
365		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$
366	363 364 316 365	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$
367		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$
368	1 5 367	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$
369	368	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$
370		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$
371	366 369 370	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$
372	362 371	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$
373		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}}⌋$
374	354	flcld	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to ⌊\frac{F (x)}{\frac{v}{3}}⌋ \in ℤ$
375	374	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 ℤ$
376	373 375	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 ℤ$
377	376	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}}⌋$
378	377	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}}⌋$
379	378	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}}⌋$
380		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}}⌋$
381	379 380	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$
382		0mbl	$⊢ \emptyset \in dom vol$
383	381 382	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$
384	372 383	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$
385	310 384	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$
386		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$
387	290 385 386	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$
388		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)\}$
389		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)\}$
390	171 389	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)\}$
391	388 390	syl5eqr	$⊢ 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)\}$
392	391	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)\}$
393	179	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)$
394	393	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\}$
395		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\}$
396		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\}$
397	187 396	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\}$
398	395 397	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\}$
399	394 398	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\}]$
400	399	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\}]$
401		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}), +∞)]$
402	14 20	jca	$⊢ v \in ℝ^{+} \to (\frac{v}{3} \in ℝ \land \frac{v}{3} \neq 0)$
403		redivcl	$⊢ (t \in ℝ \land \frac{v}{3} \in ℝ \land \frac{v}{3} \neq 0) \to \frac{t}{\frac{v}{3}} \in ℝ$
404	403	3expb	$⊢ (t \in ℝ \land (\frac{v}{3} \in ℝ \land \frac{v}{3} \neq 0)) \to \frac{t}{\frac{v}{3}} \in ℝ$
405	402 404	sylan2	$⊢ (t \in ℝ \land v \in ℝ^{+}) \to \frac{t}{\frac{v}{3}} \in ℝ$
406	405	ancoms	$⊢ (v \in ℝ^{+} \land t \in ℝ) \to \frac{t}{\frac{v}{3}} \in ℝ$
407	406	adantll	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \frac{t}{\frac{v}{3}} \in ℝ$
408	407 206	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
409		peano2re	$⊢ (\frac{t}{\frac{v}{3}}) + 1 \in ℝ \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ$
410		reflcl	$⊢ (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ \in ℝ$
411	408 409 410	3syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ \in ℝ$
412	14	ad2antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \frac{v}{3} \in ℝ$
413	411 412	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 ℝ$
414	413	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 ℝ^{*}$
415		pnfxr	$⊢ +∞ \in ℝ^{*}$
416	415	a1i	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to +∞ \in ℝ^{*}$
417		ltpnf	$⊢ ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) \in ℝ \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) < +∞$
418	413 417	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to ⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}) < +∞$
419		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}), +∞)$
420	414 416 418 419	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}), +∞)$
421	420	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}), +∞)]$
422	401 421	syl5eqr	$⊢ (((φ \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}), +∞)]$
423	226	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}), +∞)]$
424	228	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}), +∞)\}$
425	423 424	syl6eq	$⊢ φ \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}), +∞)\}$
426	425	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}), +∞)\}$
427	408 409	syl	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to (\frac{t}{\frac{v}{3}}) + 1 + 1 \in ℝ$
428	427	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 ℝ$
429		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)$
430	428 354 429	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)$
431	413	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 ℝ$
432		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)))$
433	431 432	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)))$
434	338	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)))$
435	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⌋ \in ℝ$
436	49	ad3antlr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to \frac{v}{3} \in ℝ^{+}$
437	435 338 436	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}})$
438	433 434 437	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}})$
439	408	adantr	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to (\frac{t}{\frac{v}{3}}) + 1 \in ℝ$
440	354 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 ℝ$
441		1red	$⊢ ((((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \land x \in ℝ) \to 1 \in ℝ$
442	439 440 441	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)$
443	430 438 442	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}}⌋)$
444	297 441 440	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)$
445	443 444	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)$
446	440 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 ℝ$
447	294 446 436	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}))$
448	446 295	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 ℝ$
449	294 448	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)$
450	445 447 449	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)$
451	450	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\}$
452	422 426 451	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\}$
453	1	ad3antrrr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to F \in MblFn$
454		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$
455	453 337 413 454	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$
456		mbfima	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ) \to F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] \in dom vol$
457	1 5 456	syl2anc	$⊢ φ \to F^{-1} [(⌊(\frac{t}{\frac{v}{3}}) + 1 + 1⌋ (\frac{v}{3}), +∞)] \in dom vol$
458	457	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$
459		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$
460	455 458 459	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$
461	452 460	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$
462	239 461	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$
463		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$
464	462 246 463	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$
465	400 464	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$
466	465	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$
467		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$
468	42 466 467	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$
469	392 468	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$
470	256	imaeq1d	$⊢ h \in dom \int^{1} \to h^{-1} [\{0\}] = {(x \in ℝ ⟼ h (x))}^{-1} [\{0\}]$
471	258	mptpreima	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [\{0\}] = \{x \in ℝ \| h (x) \in \{0\}\}$
472	143	elsn	$⊢ h (x) \in \{0\} \leftrightarrow h (x) = 0$
473	472	rabbii	$⊢ \{x \in ℝ \| h (x) \in \{0\}\} = \{x \in ℝ \| h (x) = 0\}$
474	471 473	eqtri	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [\{0\}] = \{x \in ℝ \| h (x) = 0\}$
475	470 474	syl6eq	$⊢ h \in dom \int^{1} \to h^{-1} [\{0\}] = \{x \in ℝ \| h (x) = 0\}$
476		i1fima	$⊢ h \in dom \int^{1} \to h^{-1} [\{0\}] \in dom vol$
477	475 476	eqeltrrd	$⊢ h \in dom \int^{1} \to \{x \in ℝ \| h (x) = 0\} \in dom vol$
478	477	ad2antlr	$⊢ ((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \to \{x \in ℝ \| h (x) = 0\} \in dom vol$
479		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$
480	469 478 479	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$
481	480	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$
482	256	imaeq1d	$⊢ h \in dom \int^{1} \to h^{-1} [\{t\}] = {(x \in ℝ ⟼ h (x))}^{-1} [\{t\}]$
483	258	mptpreima	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [\{t\}] = \{x \in ℝ \| h (x) \in \{t\}\}$
484	143	elsn	$⊢ h (x) \in \{t\} \leftrightarrow h (x) = t$
485		eqcom	$⊢ h (x) = t \leftrightarrow t = h (x)$
486	484 485	bitri	$⊢ h (x) \in \{t\} \leftrightarrow t = h (x)$
487	486	rabbii	$⊢ \{x \in ℝ \| h (x) \in \{t\}\} = \{x \in ℝ \| t = h (x)\}$
488	483 487	eqtri	$⊢ {(x \in ℝ ⟼ h (x))}^{-1} [\{t\}] = \{x \in ℝ \| t = h (x)\}$
489	482 488	syl6eq	$⊢ h \in dom \int^{1} \to h^{-1} [\{t\}] = \{x \in ℝ \| t = h (x)\}$
490	489	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to h^{-1} [\{t\}] = \{x \in ℝ \| t = h (x)\}$
491	490 245	eqeltrrd	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land t \in ℝ) \to \{x \in ℝ \| t = h (x)\} \in dom vol$
492		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$
493	481 491 492	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$
494		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$
495	387 493 494	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$
496	162 495	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$
497	157 496	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$
498		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\}])$
499	497 498	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\}])$
500		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)$
501	160	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))$
502	500 501	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))$
503	502	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))$
504	131	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\}\}$
505	470 471	syl6eq	$⊢ h \in dom \int^{1} \to h^{-1} [\{0\}] = \{x \in ℝ \| h (x) \in \{0\}\}$
506	504 505	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\}\}$
507		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\})\}$
508	506 507	syl6eq	$⊢ 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\})\}$
509	508	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\})\}$
510	147	biimpri	$⊢ h (x) = 0 \to \neg h (x) \neq 0$
511	510	intnand	$⊢ h (x) = 0 \to \neg ((⌊\frac{F (x)}{\frac{v}{3}}⌋ - 1) (\frac{v}{3}) \leq h (x) \land h (x) \neq 0)$
512	511	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)$
513		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$
514	512 513	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$
515	514	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$
516		simpll	$⊢ ((t \neq 0 \land x \in ℝ) \land h (x) = 0) \to t \neq 0$
517	516	necomd	$⊢ ((t \neq 0 \land x \in ℝ) \land h (x) = 0) \to 0 \neq t$
518	515 517	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$
519	518	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)$
520		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\})$
521		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\})$
522		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\})$
523	520 521 522	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\})$
524	145	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$
525	472 524	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)$
526	523 525	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)$
527	519 526	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\})$
528	527	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\})$
529		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\})$
530	528 529	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$
531	530	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$
532	509 531	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$
533		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}$
534		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}$
535	144 130	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))) = ℝ$
536	534 535	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} = ℝ$
537	533 536	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 ℝ$
538		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\}])$
539	537 538	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\}]$
540	532 539	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\}]$
541		ffun	$⊢ h : ℝ ⟶ ℝ \to Fun h$
542		difpreima	$⊢ Fun h \to h^{-1} [ran h ∖ \{0\}] = h^{-1} [ran h] ∖ h^{-1} [\{0\}]$
543	541 542	syl	$⊢ h : ℝ ⟶ ℝ \to h^{-1} [ran h ∖ \{0\}] = h^{-1} [ran h] ∖ h^{-1} [\{0\}]$
544		fdm	$⊢ h : ℝ ⟶ ℝ \to dom h = ℝ$
545	164 544	syl5eq	$⊢ h : ℝ ⟶ ℝ \to h^{-1} [ran h] = ℝ$
546	545	difeq1d	$⊢ h : ℝ ⟶ ℝ \to h^{-1} [ran h] ∖ h^{-1} [\{0\}] = ℝ ∖ h^{-1} [\{0\}]$
547	543 546	eqtrd	$⊢ h : ℝ ⟶ ℝ \to h^{-1} [ran h ∖ \{0\}] = ℝ ∖ h^{-1} [\{0\}]$
548	28 547	syl	$⊢ h \in dom \int^{1} \to h^{-1} [ran h ∖ \{0\}] = ℝ ∖ h^{-1} [\{0\}]$
549	548	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\}]$
550	540 549	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\}]$
551		imassrn	$⊢ h^{-1} [ran h ∖ \{0\}] \subseteq ran h^{-1}$
552	551 184	sseqtrid	$⊢ h \in dom \int^{1} \to h^{-1} [ran h ∖ \{0\}] \subseteq ℝ$
553	552	ad3antlr	$⊢ (((φ \land h \in dom \int^{1}) \land v \in ℝ^{+}) \land (t \in ℝ \land t \neq 0)) \to h^{-1} [ran h ∖ \{0\}] \subseteq ℝ$
554		i1fima	$⊢ h \in dom \int^{1} \to h^{-1} [ran h ∖ \{0\}] \in dom vol$
555		mblvol	$⊢ h^{-1} [ran h ∖ \{0\}] \in dom vol \to vol (h^{-1} [ran h ∖ \{0\}]) = {vol}^{*} (h^{-1} [ran h ∖ \{0\}])$
556	554 555	syl	$⊢ h \in dom \int^{1} \to vol (h^{-1} [ran h ∖ \{0\}]) = {vol}^{*} (h^{-1} [ran h ∖ \{0\}])$
557		neldifsn	$⊢ \neg 0 \in (ran h ∖ \{0\})$
558		i1fima2	$⊢ (h \in dom \int^{1} \land \neg 0 \in (ran h ∖ \{0\})) \to vol (h^{-1} [ran h ∖ \{0\}]) \in ℝ$
559	557 558	mpan2	$⊢ h \in dom \int^{1} \to vol (h^{-1} [ran h ∖ \{0\}]) \in ℝ$
560	556 559	eqeltrrd	$⊢ h \in dom \int^{1} \to {vol}^{*} (h^{-1} [ran h ∖ \{0\}]) \in ℝ$
561	560	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 ℝ$
562		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 ℝ$
563	550 553 561 562	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 ℝ$
564	503 563	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 ℝ$
565	499 564	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 ℝ$
566	32 129 497 565	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