mbfi1fseqlem4

Description: Lemma for mbfi1fseq . This lemma is not as interesting as it is long - it is simply checking that G is in fact a sequence of simple functions, by verifying that its range is in ( 0 ... n 2 ^ n ) / ( 2 ^ n ) (which is to say, the numbers from 0 to n in increments of 1 / ( 2 ^ n ) ), and also that the preimage of each point k is measurable, because it is equal to ( -u n , n ) i^i (`' F " ( k [,) k + 1 / ( 2 ^ n ) ) ) for k < n and ( -u n , n ) i^i ( ``' F " ( k [,) +oo ) ) for k = n ` . (Contributed by Mario Carneiro, 16-Aug-2014)

	Ref	Expression
Hypotheses	mbfi1fseq.1	$⊢ φ \to F \in MblFn$
	mbfi1fseq.2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	mbfi1fseq.3	$⊢ J = (m \in ℕ, y \in ℝ ⟼ \frac{⌊F (y) 2^{m}⌋}{2^{m}})$
	mbfi1fseq.4	$⊢ G = (m \in ℕ ⟼ (x \in ℝ ⟼ if (x \in [- m, m], if (m J x \leq m, m J x, m), 0)))$
Assertion	mbfi1fseqlem4	$⊢ φ \to G : ℕ ⟶ dom \int^{1}$

Proof

Step	Hyp	Ref	Expression
1		mbfi1fseq.1	$⊢ φ \to F \in MblFn$
2		mbfi1fseq.2	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
3		mbfi1fseq.3	$⊢ J = (m \in ℕ, y \in ℝ ⟼ \frac{⌊F (y) 2^{m}⌋}{2^{m}})$
4		mbfi1fseq.4	$⊢ G = (m \in ℕ ⟼ (x \in ℝ ⟼ if (x \in [- m, m], if (m J x \leq m, m J x, m), 0)))$
5		reex	$⊢ ℝ \in V$
6	5	mptex	$⊢ (x \in ℝ ⟼ if (x \in [- m, m], if (m J x \leq m, m J x, m), 0)) \in V$
7	6 4	fnmpti	$⊢ G Fn ℕ$
8	7	a1i	$⊢ φ \to G Fn ℕ$
9	1 2 3 4	mbfi1fseqlem3	$⊢ (φ \land n \in ℕ) \to G (n) : ℝ ⟶ ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}})$
10		elfznn0	$⊢ m \in (0 \dots n 2^{n}) \to m \in ℕ_{0}$
11	10	nn0red	$⊢ m \in (0 \dots n 2^{n}) \to m \in ℝ$
12		2nn	$⊢ 2 \in ℕ$
13		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
14		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
15	12 13 14	sylancr	$⊢ n \in ℕ \to 2^{n} \in ℕ$
16	15	adantl	$⊢ (φ \land n \in ℕ) \to 2^{n} \in ℕ$
17		nndivre	$⊢ (m \in ℝ \land 2^{n} \in ℕ) \to \frac{m}{2^{n}} \in ℝ$
18	11 16 17	syl2anr	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n 2^{n})) \to \frac{m}{2^{n}} \in ℝ$
19	18	fmpttd	$⊢ (φ \land n \in ℕ) \to (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) : (0 \dots n 2^{n}) ⟶ ℝ$
20	19	frnd	$⊢ (φ \land n \in ℕ) \to ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) \subseteq ℝ$
21	9 20	fssd	$⊢ (φ \land n \in ℕ) \to G (n) : ℝ ⟶ ℝ$
22		fzfid	$⊢ (φ \land n \in ℕ) \to (0 \dots n 2^{n}) \in Fin$
23	19	ffnd	$⊢ (φ \land n \in ℕ) \to (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) Fn (0 \dots n 2^{n})$
24		dffn4	$⊢ (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) Fn (0 \dots n 2^{n}) \leftrightarrow (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) : (0 \dots n 2^{n}) \underset{onto}{⟶} ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}})$
25	23 24	sylib	$⊢ (φ \land n \in ℕ) \to (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) : (0 \dots n 2^{n}) \underset{onto}{⟶} ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}})$
26		fofi	$⊢ ((0 \dots n 2^{n}) \in Fin \land (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) : (0 \dots n 2^{n}) \underset{onto}{⟶} ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}})) \to ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) \in Fin$
27	22 25 26	syl2anc	$⊢ (φ \land n \in ℕ) \to ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) \in Fin$
28	9	frnd	$⊢ (φ \land n \in ℕ) \to ran G (n) \subseteq ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}})$
29	27 28	ssfid	$⊢ (φ \land n \in ℕ) \to ran G (n) \in Fin$
30	1 2 3 4	mbfi1fseqlem2	$⊢ n \in ℕ \to G (n) = (x \in ℝ ⟼ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0))$
31	30	fveq1d	$⊢ n \in ℕ \to G (n) (x) = (x \in ℝ ⟼ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)) (x)$
32	31	ad2antlr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to G (n) (x) = (x \in ℝ ⟼ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)) (x)$
33		simpr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to x \in ℝ$
34		ovex	$⊢ n J x \in V$
35		vex	$⊢ n \in V$
36	34 35	ifex	$⊢ if (n J x \leq n, n J x, n) \in V$
37		c0ex	$⊢ 0 \in V$
38	36 37	ifex	$⊢ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \in V$
39		eqid	$⊢ (x \in ℝ ⟼ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)) = (x \in ℝ ⟼ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0))$
40	39	fvmpt2	$⊢ (x \in ℝ \land if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \in V) \to (x \in ℝ ⟼ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)) (x) = if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)$
41	33 38 40	sylancl	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (x \in ℝ ⟼ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)) (x) = if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)$
42	32 41	eqtrd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to G (n) (x) = if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)$
43	42	adantlr	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to G (n) (x) = if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)$
44	43	eqeq1d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (G (n) (x) = k \leftrightarrow if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = k)$
45		eldifsni	$⊢ k \in (ran G (n) ∖ \{0\}) \to k \neq 0$
46	45	ad2antlr	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to k \neq 0$
47		neeq1	$⊢ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = k \to (if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \neq 0 \leftrightarrow k \neq 0)$
48	46 47	syl5ibrcom	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = k \to if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \neq 0)$
49		iffalse	$⊢ \neg x \in [- n, n] \to if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = 0$
50	49	necon1ai	$⊢ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \neq 0 \to x \in [- n, n]$
51	48 50	syl6	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = k \to x \in [- n, n])$
52	51	pm4.71rd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = k \leftrightarrow (x \in [- n, n] \land if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = k))$
53		iftrue	$⊢ x \in [- n, n] \to if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = if (n J x \leq n, n J x, n)$
54	53	eqeq1d	$⊢ x \in [- n, n] \to (if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = k \leftrightarrow if (n J x \leq n, n J x, n) = k)$
55		simpllr	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to n \in ℕ$
56	55	nnred	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to n \in ℝ$
57	56	adantr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to n \in ℝ$
58		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
59		simpr	$⊢ (m \in ℕ \land y \in ℝ) \to y \in ℝ$
60		ffvelcdm	$⊢ (F : ℝ ⟶ [0, +∞) \land y \in ℝ) \to F (y) \in [0, +∞)$
61	2 59 60	syl2an	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) \in [0, +∞)$
62	58 61	sselid	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) \in ℝ$
63		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
64		nnexpcl	$⊢ (2 \in ℕ \land m \in ℕ_{0}) \to 2^{m} \in ℕ$
65	12 63 64	sylancr	$⊢ m \in ℕ \to 2^{m} \in ℕ$
66	65	ad2antrl	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 2^{m} \in ℕ$
67	66	nnred	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 2^{m} \in ℝ$
68	62 67	remulcld	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) 2^{m} \in ℝ$
69		reflcl	$⊢ F (y) 2^{m} \in ℝ \to ⌊F (y) 2^{m}⌋ \in ℝ$
70	68 69	syl	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to ⌊F (y) 2^{m}⌋ \in ℝ$
71	70 66	nndivred	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ$
72	71	ralrimivva	$⊢ φ \to \forall m \in ℕ \forall y \in ℝ \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ$
73	3	fmpo	$⊢ \forall m \in ℕ \forall y \in ℝ \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ \leftrightarrow J : ℕ \times ℝ ⟶ ℝ$
74	72 73	sylib	$⊢ φ \to J : ℕ \times ℝ ⟶ ℝ$
75		fovcdm	$⊢ (J : ℕ \times ℝ ⟶ ℝ \land n \in ℕ \land x \in ℝ) \to n J x \in ℝ$
76	74 75	syl3an1	$⊢ (φ \land n \in ℕ \land x \in ℝ) \to n J x \in ℝ$
77	76	3expa	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to n J x \in ℝ$
78	77	adantlr	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to n J x \in ℝ$
79	78	adantr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to n J x \in ℝ$
80		lemin	$⊢ (n \in ℝ \land n J x \in ℝ \land n \in ℝ) \to (n \leq if (n J x \leq n, n J x, n) \leftrightarrow (n \leq n J x \land n \leq n))$
81	57 79 57 80	syl3anc	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to (n \leq if (n J x \leq n, n J x, n) \leftrightarrow (n \leq n J x \land n \leq n))$
82	79 57	ifcld	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to if (n J x \leq n, n J x, n) \in ℝ$
83	82 57	letri3d	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to (if (n J x \leq n, n J x, n) = n \leftrightarrow (if (n J x \leq n, n J x, n) \leq n \land n \leq if (n J x \leq n, n J x, n)))$
84		simpr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to k = n$
85	84	eqeq2d	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to (if (n J x \leq n, n J x, n) = k \leftrightarrow if (n J x \leq n, n J x, n) = n)$
86		min2	$⊢ (n J x \in ℝ \land n \in ℝ) \to if (n J x \leq n, n J x, n) \leq n$
87	79 57 86	syl2anc	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to if (n J x \leq n, n J x, n) \leq n$
88	87	biantrurd	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to (n \leq if (n J x \leq n, n J x, n) \leftrightarrow (if (n J x \leq n, n J x, n) \leq n \land n \leq if (n J x \leq n, n J x, n)))$
89	83 85 88	3bitr4d	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to (if (n J x \leq n, n J x, n) = k \leftrightarrow n \leq if (n J x \leq n, n J x, n))$
90	57	leidd	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to n \leq n$
91	90	biantrud	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to (n \leq n J x \leftrightarrow (n \leq n J x \land n \leq n))$
92	81 89 91	3bitr4d	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to (if (n J x \leq n, n J x, n) = k \leftrightarrow n \leq n J x)$
93		breq1	$⊢ k = n \to (k \leq F (x) \leftrightarrow n \leq F (x))$
94	2	adantr	$⊢ (φ \land n \in ℕ) \to F : ℝ ⟶ [0, +∞)$
95	94	ffvelcdmda	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (x) \in [0, +∞)$
96		elrege0	$⊢ F (x) \in [0, +∞) \leftrightarrow (F (x) \in ℝ \land 0 \leq F (x))$
97	95 96	sylib	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (F (x) \in ℝ \land 0 \leq F (x))$
98	97	simpld	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (x) \in ℝ$
99	98	adantlr	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to F (x) \in ℝ$
100	55 15	syl	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to 2^{n} \in ℕ$
101	100	nnred	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to 2^{n} \in ℝ$
102	99 101	remulcld	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to F (x) 2^{n} \in ℝ$
103		reflcl	$⊢ F (x) 2^{n} \in ℝ \to ⌊F (x) 2^{n}⌋ \in ℝ$
104	102 103	syl	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to ⌊F (x) 2^{n}⌋ \in ℝ$
105	100	nngt0d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to 0 < 2^{n}$
106		lemuldiv	$⊢ (n \in ℝ \land ⌊F (x) 2^{n}⌋ \in ℝ \land (2^{n} \in ℝ \land 0 < 2^{n})) \to (n 2^{n} \leq ⌊F (x) 2^{n}⌋ \leftrightarrow n \leq \frac{⌊F (x) 2^{n}⌋}{2^{n}})$
107	56 104 101 105 106	syl112anc	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (n 2^{n} \leq ⌊F (x) 2^{n}⌋ \leftrightarrow n \leq \frac{⌊F (x) 2^{n}⌋}{2^{n}})$
108		lemul1	$⊢ (n \in ℝ \land F (x) \in ℝ \land (2^{n} \in ℝ \land 0 < 2^{n})) \to (n \leq F (x) \leftrightarrow n 2^{n} \leq F (x) 2^{n})$
109	56 99 101 105 108	syl112anc	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (n \leq F (x) \leftrightarrow n 2^{n} \leq F (x) 2^{n})$
110		nnmulcl	$⊢ (n \in ℕ \land 2^{n} \in ℕ) \to n 2^{n} \in ℕ$
111	55 15 110	syl2anc2	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to n 2^{n} \in ℕ$
112	111	nnzd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to n 2^{n} \in ℤ$
113		flge	$⊢ (F (x) 2^{n} \in ℝ \land n 2^{n} \in ℤ) \to (n 2^{n} \leq F (x) 2^{n} \leftrightarrow n 2^{n} \leq ⌊F (x) 2^{n}⌋)$
114	102 112 113	syl2anc	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (n 2^{n} \leq F (x) 2^{n} \leftrightarrow n 2^{n} \leq ⌊F (x) 2^{n}⌋)$
115	109 114	bitrd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (n \leq F (x) \leftrightarrow n 2^{n} \leq ⌊F (x) 2^{n}⌋)$
116		simpr	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to x \in ℝ$
117		simpr	$⊢ (m = n \land y = x) \to y = x$
118	117	fveq2d	$⊢ (m = n \land y = x) \to F (y) = F (x)$
119		simpl	$⊢ (m = n \land y = x) \to m = n$
120	119	oveq2d	$⊢ (m = n \land y = x) \to 2^{m} = 2^{n}$
121	118 120	oveq12d	$⊢ (m = n \land y = x) \to F (y) 2^{m} = F (x) 2^{n}$
122	121	fveq2d	$⊢ (m = n \land y = x) \to ⌊F (y) 2^{m}⌋ = ⌊F (x) 2^{n}⌋$
123	122 120	oveq12d	$⊢ (m = n \land y = x) \to \frac{⌊F (y) 2^{m}⌋}{2^{m}} = \frac{⌊F (x) 2^{n}⌋}{2^{n}}$
124		ovex	$⊢ \frac{⌊F (x) 2^{n}⌋}{2^{n}} \in V$
125	123 3 124	ovmpoa	$⊢ (n \in ℕ \land x \in ℝ) \to n J x = \frac{⌊F (x) 2^{n}⌋}{2^{n}}$
126	55 116 125	syl2anc	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to n J x = \frac{⌊F (x) 2^{n}⌋}{2^{n}}$
127	126	breq2d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (n \leq n J x \leftrightarrow n \leq \frac{⌊F (x) 2^{n}⌋}{2^{n}})$
128	107 115 127	3bitr4d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (n \leq F (x) \leftrightarrow n \leq n J x)$
129	93 128	sylan9bbr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to (k \leq F (x) \leftrightarrow n \leq n J x)$
130	116	adantr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to x \in ℝ$
131		iftrue	$⊢ k = n \to if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) = ℝ$
132	131	adantl	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) = ℝ$
133	130 132	eleqtrrd	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))])$
134	133	biantrurd	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to (k \leq F (x) \leftrightarrow (x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \land k \leq F (x)))$
135	92 129 134	3bitr2d	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k = n) \to (if (n J x \leq n, n J x, n) = k \leftrightarrow (x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \land k \leq F (x)))$
136	28	ssdifssd	$⊢ (φ \land n \in ℕ) \to ran G (n) ∖ \{0\} \subseteq ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}})$
137	136	sselda	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to k \in ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}})$
138		eqid	$⊢ (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) = (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}})$
139	138	rnmpt	$⊢ ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) = \{k \| \exists m \in (0 \dots n 2^{n}) k = \frac{m}{2^{n}}\}$
140	139	eqabri	$⊢ k \in ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) \leftrightarrow \exists m \in (0 \dots n 2^{n}) k = \frac{m}{2^{n}}$
141		elfzelz	$⊢ m \in (0 \dots n 2^{n}) \to m \in ℤ$
142	141	adantl	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n 2^{n})) \to m \in ℤ$
143	142	zcnd	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n 2^{n})) \to m \in ℂ$
144	15	ad2antlr	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n 2^{n})) \to 2^{n} \in ℕ$
145	144	nncnd	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n 2^{n})) \to 2^{n} \in ℂ$
146	144	nnne0d	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n 2^{n})) \to 2^{n} \neq 0$
147	143 145 146	divcan1d	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n 2^{n})) \to (\frac{m}{2^{n}}) 2^{n} = m$
148	147 142	eqeltrd	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n 2^{n})) \to (\frac{m}{2^{n}}) 2^{n} \in ℤ$
149		oveq1	$⊢ k = \frac{m}{2^{n}} \to k 2^{n} = (\frac{m}{2^{n}}) 2^{n}$
150	149	eleq1d	$⊢ k = \frac{m}{2^{n}} \to (k 2^{n} \in ℤ \leftrightarrow (\frac{m}{2^{n}}) 2^{n} \in ℤ)$
151	148 150	syl5ibrcom	$⊢ ((φ \land n \in ℕ) \land m \in (0 \dots n 2^{n})) \to (k = \frac{m}{2^{n}} \to k 2^{n} \in ℤ)$
152	151	rexlimdva	$⊢ (φ \land n \in ℕ) \to (\exists m \in (0 \dots n 2^{n}) k = \frac{m}{2^{n}} \to k 2^{n} \in ℤ)$
153	140 152	biimtrid	$⊢ (φ \land n \in ℕ) \to (k \in ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}}) \to k 2^{n} \in ℤ)$
154	153	imp	$⊢ ((φ \land n \in ℕ) \land k \in ran (m \in (0 \dots n 2^{n}) ⟼ \frac{m}{2^{n}})) \to k 2^{n} \in ℤ$
155	137 154	syldan	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to k 2^{n} \in ℤ$
156	155	adantr	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to k 2^{n} \in ℤ$
157		flbi	$⊢ (F (x) 2^{n} \in ℝ \land k 2^{n} \in ℤ) \to (⌊F (x) 2^{n}⌋ = k 2^{n} \leftrightarrow (k 2^{n} \leq F (x) 2^{n} \land F (x) 2^{n} < k 2^{n} + 1))$
158	102 156 157	syl2anc	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (⌊F (x) 2^{n}⌋ = k 2^{n} \leftrightarrow (k 2^{n} \leq F (x) 2^{n} \land F (x) 2^{n} < k 2^{n} + 1))$
159	158	adantr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to (⌊F (x) 2^{n}⌋ = k 2^{n} \leftrightarrow (k 2^{n} \leq F (x) 2^{n} \land F (x) 2^{n} < k 2^{n} + 1))$
160		neeq1	$⊢ if (n J x \leq n, n J x, n) = k \to (if (n J x \leq n, n J x, n) \neq n \leftrightarrow k \neq n)$
161	160	biimparc	$⊢ (k \neq n \land if (n J x \leq n, n J x, n) = k) \to if (n J x \leq n, n J x, n) \neq n$
162		iffalse	$⊢ \neg n J x \leq n \to if (n J x \leq n, n J x, n) = n$
163	162	necon1ai	$⊢ if (n J x \leq n, n J x, n) \neq n \to n J x \leq n$
164	161 163	syl	$⊢ (k \neq n \land if (n J x \leq n, n J x, n) = k) \to n J x \leq n$
165	164	iftrued	$⊢ (k \neq n \land if (n J x \leq n, n J x, n) = k) \to if (n J x \leq n, n J x, n) = n J x$
166		simpr	$⊢ (k \neq n \land if (n J x \leq n, n J x, n) = k) \to if (n J x \leq n, n J x, n) = k$
167	165 166	eqtr3d	$⊢ (k \neq n \land if (n J x \leq n, n J x, n) = k) \to n J x = k$
168	167 164	eqbrtrrd	$⊢ (k \neq n \land if (n J x \leq n, n J x, n) = k) \to k \leq n$
169	168 167	jca	$⊢ (k \neq n \land if (n J x \leq n, n J x, n) = k) \to (k \leq n \land n J x = k)$
170	169	ex	$⊢ k \neq n \to (if (n J x \leq n, n J x, n) = k \to (k \leq n \land n J x = k))$
171		breq1	$⊢ n J x = k \to (n J x \leq n \leftrightarrow k \leq n)$
172	171	biimparc	$⊢ (k \leq n \land n J x = k) \to n J x \leq n$
173	172	iftrued	$⊢ (k \leq n \land n J x = k) \to if (n J x \leq n, n J x, n) = n J x$
174		simpr	$⊢ (k \leq n \land n J x = k) \to n J x = k$
175	173 174	eqtrd	$⊢ (k \leq n \land n J x = k) \to if (n J x \leq n, n J x, n) = k$
176	170 175	impbid1	$⊢ k \neq n \to (if (n J x \leq n, n J x, n) = k \leftrightarrow (k \leq n \land n J x = k))$
177	176	adantl	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to (if (n J x \leq n, n J x, n) = k \leftrightarrow (k \leq n \land n J x = k))$
178		eldifi	$⊢ k \in (ran G (n) ∖ \{0\}) \to k \in ran G (n)$
179		nnre	$⊢ n \in ℕ \to n \in ℝ$
180	179	ad2antlr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to n \in ℝ$
181	77 180 86	syl2anc	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to if (n J x \leq n, n J x, n) \leq n$
182	13	ad2antlr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to n \in ℕ_{0}$
183	182	nn0ge0d	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to 0 \leq n$
184		breq1	$⊢ if (n J x \leq n, n J x, n) = if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \to (if (n J x \leq n, n J x, n) \leq n \leftrightarrow if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \leq n)$
185		breq1	$⊢ 0 = if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \to (0 \leq n \leftrightarrow if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \leq n)$
186	184 185	ifboth	$⊢ (if (n J x \leq n, n J x, n) \leq n \land 0 \leq n) \to if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \leq n$
187	181 183 186	syl2anc	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \leq n$
188	42 187	eqbrtrd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to G (n) (x) \leq n$
189	188	ralrimiva	$⊢ (φ \land n \in ℕ) \to \forall x \in ℝ G (n) (x) \leq n$
190	9	ffnd	$⊢ (φ \land n \in ℕ) \to G (n) Fn ℝ$
191		breq1	$⊢ k = G (n) (x) \to (k \leq n \leftrightarrow G (n) (x) \leq n)$
192	191	ralrn	$⊢ G (n) Fn ℝ \to (\forall k \in ran G (n) k \leq n \leftrightarrow \forall x \in ℝ G (n) (x) \leq n)$
193	190 192	syl	$⊢ (φ \land n \in ℕ) \to (\forall k \in ran G (n) k \leq n \leftrightarrow \forall x \in ℝ G (n) (x) \leq n)$
194	189 193	mpbird	$⊢ (φ \land n \in ℕ) \to \forall k \in ran G (n) k \leq n$
195	194	r19.21bi	$⊢ ((φ \land n \in ℕ) \land k \in ran G (n)) \to k \leq n$
196	178 195	sylan2	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to k \leq n$
197	196	ad2antrr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to k \leq n$
198	197	biantrurd	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to (n J x = k \leftrightarrow (k \leq n \land n J x = k))$
199	126	eqeq1d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (n J x = k \leftrightarrow \frac{⌊F (x) 2^{n}⌋}{2^{n}} = k)$
200	104	recnd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to ⌊F (x) 2^{n}⌋ \in ℂ$
201	28 20	sstrd	$⊢ (φ \land n \in ℕ) \to ran G (n) \subseteq ℝ$
202	201	ssdifssd	$⊢ (φ \land n \in ℕ) \to ran G (n) ∖ \{0\} \subseteq ℝ$
203	202	sselda	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to k \in ℝ$
204	203	adantr	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to k \in ℝ$
205	204	recnd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to k \in ℂ$
206	100	nncnd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to 2^{n} \in ℂ$
207	100	nnne0d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to 2^{n} \neq 0$
208	200 205 206 207	divmul3d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (\frac{⌊F (x) 2^{n}⌋}{2^{n}} = k \leftrightarrow ⌊F (x) 2^{n}⌋ = k 2^{n})$
209	199 208	bitrd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (n J x = k \leftrightarrow ⌊F (x) 2^{n}⌋ = k 2^{n})$
210	209	adantr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to (n J x = k \leftrightarrow ⌊F (x) 2^{n}⌋ = k 2^{n})$
211	177 198 210	3bitr2d	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to (if (n J x \leq n, n J x, n) = k \leftrightarrow ⌊F (x) 2^{n}⌋ = k 2^{n})$
212		ifnefalse	$⊢ k \neq n \to if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) = F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]$
213	212	eleq2d	$⊢ k \neq n \to (x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \leftrightarrow x \in F^{-1} [(−∞, k + (\frac{1}{2^{n}}))])$
214	100	nnrecred	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to \frac{1}{2^{n}} \in ℝ$
215	204 214	readdcld	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to k + (\frac{1}{2^{n}}) \in ℝ$
216	215	rexrd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to k + (\frac{1}{2^{n}}) \in ℝ^{*}$
217		elioomnf	$⊢ k + (\frac{1}{2^{n}}) \in ℝ^{*} \to (F (x) \in (−∞, k + (\frac{1}{2^{n}})) \leftrightarrow (F (x) \in ℝ \land F (x) < k + (\frac{1}{2^{n}})))$
218	216 217	syl	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (F (x) \in (−∞, k + (\frac{1}{2^{n}})) \leftrightarrow (F (x) \in ℝ \land F (x) < k + (\frac{1}{2^{n}})))$
219	94	ad2antrr	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to F : ℝ ⟶ [0, +∞)$
220	219	ffnd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to F Fn ℝ$
221		elpreima	$⊢ F Fn ℝ \to (x \in F^{-1} [(−∞, k + (\frac{1}{2^{n}}))] \leftrightarrow (x \in ℝ \land F (x) \in (−∞, k + (\frac{1}{2^{n}}))))$
222	220 221	syl	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (x \in F^{-1} [(−∞, k + (\frac{1}{2^{n}}))] \leftrightarrow (x \in ℝ \land F (x) \in (−∞, k + (\frac{1}{2^{n}}))))$
223	116 222	mpbirand	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (x \in F^{-1} [(−∞, k + (\frac{1}{2^{n}}))] \leftrightarrow F (x) \in (−∞, k + (\frac{1}{2^{n}})))$
224	99	biantrurd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (F (x) < k + (\frac{1}{2^{n}}) \leftrightarrow (F (x) \in ℝ \land F (x) < k + (\frac{1}{2^{n}})))$
225	218 223 224	3bitr4d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (x \in F^{-1} [(−∞, k + (\frac{1}{2^{n}}))] \leftrightarrow F (x) < k + (\frac{1}{2^{n}}))$
226		ltmul1	$⊢ (F (x) \in ℝ \land k + (\frac{1}{2^{n}}) \in ℝ \land (2^{n} \in ℝ \land 0 < 2^{n})) \to (F (x) < k + (\frac{1}{2^{n}}) \leftrightarrow F (x) 2^{n} < (k + (\frac{1}{2^{n}})) 2^{n})$
227	99 215 101 105 226	syl112anc	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (F (x) < k + (\frac{1}{2^{n}}) \leftrightarrow F (x) 2^{n} < (k + (\frac{1}{2^{n}})) 2^{n})$
228	214	recnd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to \frac{1}{2^{n}} \in ℂ$
229	206 207	recid2d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (\frac{1}{2^{n}}) 2^{n} = 1$
230	229	oveq2d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to k 2^{n} + (\frac{1}{2^{n}}) 2^{n} = k 2^{n} + 1$
231	205 206 228 230	joinlmuladdmuld	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (k + (\frac{1}{2^{n}})) 2^{n} = k 2^{n} + 1$
232	231	breq2d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (F (x) 2^{n} < (k + (\frac{1}{2^{n}})) 2^{n} \leftrightarrow F (x) 2^{n} < k 2^{n} + 1)$
233	225 227 232	3bitrd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (x \in F^{-1} [(−∞, k + (\frac{1}{2^{n}}))] \leftrightarrow F (x) 2^{n} < k 2^{n} + 1)$
234	213 233	sylan9bbr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to (x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \leftrightarrow F (x) 2^{n} < k 2^{n} + 1)$
235		lemul1	$⊢ (k \in ℝ \land F (x) \in ℝ \land (2^{n} \in ℝ \land 0 < 2^{n})) \to (k \leq F (x) \leftrightarrow k 2^{n} \leq F (x) 2^{n})$
236	204 99 101 105 235	syl112anc	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (k \leq F (x) \leftrightarrow k 2^{n} \leq F (x) 2^{n})$
237	236	adantr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to (k \leq F (x) \leftrightarrow k 2^{n} \leq F (x) 2^{n})$
238	234 237	anbi12d	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to ((x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \land k \leq F (x)) \leftrightarrow (F (x) 2^{n} < k 2^{n} + 1 \land k 2^{n} \leq F (x) 2^{n}))$
239	238	biancomd	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to ((x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \land k \leq F (x)) \leftrightarrow (k 2^{n} \leq F (x) 2^{n} \land F (x) 2^{n} < k 2^{n} + 1))$
240	159 211 239	3bitr4d	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land k \neq n) \to (if (n J x \leq n, n J x, n) = k \leftrightarrow (x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \land k \leq F (x)))$
241	135 240	pm2.61dane	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (if (n J x \leq n, n J x, n) = k \leftrightarrow (x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \land k \leq F (x)))$
242		eldif	$⊢ x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)]) \leftrightarrow (x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \land \neg x \in F^{-1} [(−∞, k)])$
243	204	rexrd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to k \in ℝ^{*}$
244		elioomnf	$⊢ k \in ℝ^{*} \to (F (x) \in (−∞, k) \leftrightarrow (F (x) \in ℝ \land F (x) < k))$
245	243 244	syl	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (F (x) \in (−∞, k) \leftrightarrow (F (x) \in ℝ \land F (x) < k))$
246		elpreima	$⊢ F Fn ℝ \to (x \in F^{-1} [(−∞, k)] \leftrightarrow (x \in ℝ \land F (x) \in (−∞, k)))$
247	220 246	syl	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (x \in F^{-1} [(−∞, k)] \leftrightarrow (x \in ℝ \land F (x) \in (−∞, k)))$
248	116 247	mpbirand	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (x \in F^{-1} [(−∞, k)] \leftrightarrow F (x) \in (−∞, k))$
249	99	biantrurd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (F (x) < k \leftrightarrow (F (x) \in ℝ \land F (x) < k))$
250	245 248 249	3bitr4d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (x \in F^{-1} [(−∞, k)] \leftrightarrow F (x) < k)$
251	250	notbid	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (\neg x \in F^{-1} [(−∞, k)] \leftrightarrow \neg F (x) < k)$
252	204 99	lenltd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (k \leq F (x) \leftrightarrow \neg F (x) < k)$
253	251 252	bitr4d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (\neg x \in F^{-1} [(−∞, k)] \leftrightarrow k \leq F (x))$
254	253	anbi2d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to ((x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \land \neg x \in F^{-1} [(−∞, k)]) \leftrightarrow (x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \land k \leq F (x)))$
255	242 254	bitrid	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)]) \leftrightarrow (x \in if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \land k \leq F (x)))$
256	241 255	bitr4d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (if (n J x \leq n, n J x, n) = k \leftrightarrow x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)]))$
257	54 256	sylan9bbr	$⊢ ((((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \land x \in [- n, n]) \to (if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = k \leftrightarrow x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)]))$
258	257	pm5.32da	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to ((x \in [- n, n] \land if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = k) \leftrightarrow (x \in [- n, n] \land x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)])))$
259	44 52 258	3bitrd	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (G (n) (x) = k \leftrightarrow (x \in [- n, n] \land x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)])))$
260	259	pm5.32da	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to ((x \in ℝ \land G (n) (x) = k) \leftrightarrow (x \in ℝ \land (x \in [- n, n] \land x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)]))))$
261	21	adantr	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to G (n) : ℝ ⟶ ℝ$
262	261	ffnd	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to G (n) Fn ℝ$
263		fniniseg	$⊢ G (n) Fn ℝ \to (x \in {G (n)}^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land G (n) (x) = k))$
264	262 263	syl	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to (x \in {G (n)}^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land G (n) (x) = k))$
265		elin	$⊢ x \in ([- n, n] \cap (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)])) \leftrightarrow (x \in [- n, n] \land x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)]))$
266	179	ad2antlr	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to n \in ℝ$
267	266	renegcld	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to - n \in ℝ$
268		iccmbl	$⊢ (- n \in ℝ \land n \in ℝ) \to [- n, n] \in dom vol$
269	267 266 268	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to [- n, n] \in dom vol$
270		mblss	$⊢ [- n, n] \in dom vol \to [- n, n] \subseteq ℝ$
271	269 270	syl	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to [- n, n] \subseteq ℝ$
272	271	sseld	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to (x \in [- n, n] \to x \in ℝ)$
273	272	adantrd	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to ((x \in [- n, n] \land x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)])) \to x \in ℝ)$
274	273	pm4.71rd	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to ((x \in [- n, n] \land x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)])) \leftrightarrow (x \in ℝ \land (x \in [- n, n] \land x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)]))))$
275	265 274	bitrid	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to (x \in ([- n, n] \cap (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)])) \leftrightarrow (x \in ℝ \land (x \in [- n, n] \land x \in (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)]))))$
276	260 264 275	3bitr4d	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to (x \in {G (n)}^{-1} [\{k\}] \leftrightarrow x \in ([- n, n] \cap (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)])))$
277	276	eqrdv	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to {G (n)}^{-1} [\{k\}] = [- n, n] \cap (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)])$
278		rembl	$⊢ ℝ \in dom vol$
279		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F : ℝ ⟶ ℝ$
280	2 58 279	sylancl	$⊢ φ \to F : ℝ ⟶ ℝ$
281		mbfima	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ) \to F^{-1} [(−∞, k + (\frac{1}{2^{n}}))] \in dom vol$
282	1 280 281	syl2anc	$⊢ φ \to F^{-1} [(−∞, k + (\frac{1}{2^{n}}))] \in dom vol$
283		ifcl	$⊢ (ℝ \in dom vol \land F^{-1} [(−∞, k + (\frac{1}{2^{n}}))] \in dom vol) \to if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \in dom vol$
284	278 282 283	sylancr	$⊢ φ \to if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \in dom vol$
285		mbfima	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ) \to F^{-1} [(−∞, k)] \in dom vol$
286	1 280 285	syl2anc	$⊢ φ \to F^{-1} [(−∞, k)] \in dom vol$
287		difmbl	$⊢ (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) \in dom vol \land F^{-1} [(−∞, k)] \in dom vol) \to if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)] \in dom vol$
288	284 286 287	syl2anc	$⊢ φ \to if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)] \in dom vol$
289	288	ad2antrr	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)] \in dom vol$
290		inmbl	$⊢ ([- n, n] \in dom vol \land if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)] \in dom vol) \to [- n, n] \cap (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)]) \in dom vol$
291	269 289 290	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to [- n, n] \cap (if (k = n, ℝ, F^{-1} [(−∞, k + (\frac{1}{2^{n}}))]) ∖ F^{-1} [(−∞, k)]) \in dom vol$
292	277 291	eqeltrd	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to {G (n)}^{-1} [\{k\}] \in dom vol$
293		mblvol	$⊢ {G (n)}^{-1} [\{k\}] \in dom vol \to vol ({G (n)}^{-1} [\{k\}]) = {vol}^{*} ({G (n)}^{-1} [\{k\}])$
294	292 293	syl	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to vol ({G (n)}^{-1} [\{k\}]) = {vol}^{*} ({G (n)}^{-1} [\{k\}])$
295	190	adantr	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to G (n) Fn ℝ$
296	295 263	syl	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to (x \in {G (n)}^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land G (n) (x) = k))$
297	77 180	ifcld	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to if (n J x \leq n, n J x, n) \in ℝ$
298		0re	$⊢ 0 \in ℝ$
299		ifcl	$⊢ (if (n J x \leq n, n J x, n) \in ℝ \land 0 \in ℝ) \to if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \in ℝ$
300	297 298 299	sylancl	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \in ℝ$
301	39	fvmpt2	$⊢ (x \in ℝ \land if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) \in ℝ) \to (x \in ℝ ⟼ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)) (x) = if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)$
302	33 300 301	syl2anc	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to (x \in ℝ ⟼ if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)) (x) = if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)$
303	32 302	eqtrd	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to G (n) (x) = if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)$
304	303	adantlr	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to G (n) (x) = if (x \in [- n, n], if (n J x \leq n, n J x, n), 0)$
305	304	eqeq1d	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (G (n) (x) = k \leftrightarrow if (x \in [- n, n], if (n J x \leq n, n J x, n), 0) = k)$
306	305 51	sylbid	$⊢ (((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \land x \in ℝ) \to (G (n) (x) = k \to x \in [- n, n])$
307	306	expimpd	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to ((x \in ℝ \land G (n) (x) = k) \to x \in [- n, n])$
308	296 307	sylbid	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to (x \in {G (n)}^{-1} [\{k\}] \to x \in [- n, n])$
309	308	ssrdv	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to {G (n)}^{-1} [\{k\}] \subseteq [- n, n]$
310		iccssre	$⊢ (- n \in ℝ \land n \in ℝ) \to [- n, n] \subseteq ℝ$
311	267 266 310	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to [- n, n] \subseteq ℝ$
312		mblvol	$⊢ [- n, n] \in dom vol \to vol ([- n, n]) = {vol}^{*} ([- n, n])$
313	269 312	syl	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to vol ([- n, n]) = {vol}^{*} ([- n, n])$
314		iccvolcl	$⊢ (- n \in ℝ \land n \in ℝ) \to vol ([- n, n]) \in ℝ$
315	267 266 314	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to vol ([- n, n]) \in ℝ$
316	313 315	eqeltrrd	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to {vol}^{*} ([- n, n]) \in ℝ$
317		ovolsscl	$⊢ ({G (n)}^{-1} [\{k\}] \subseteq [- n, n] \land [- n, n] \subseteq ℝ \land {vol}^{} ([- n, n]) \in ℝ) \to {vol}^{} ({G (n)}^{-1} [\{k\}]) \in ℝ$
318	309 311 316 317	syl3anc	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to {vol}^{*} ({G (n)}^{-1} [\{k\}]) \in ℝ$
319	294 318	eqeltrd	$⊢ ((φ \land n \in ℕ) \land k \in (ran G (n) ∖ \{0\})) \to vol ({G (n)}^{-1} [\{k\}]) \in ℝ$
320	21 29 292 319	i1fd	$⊢ (φ \land n \in ℕ) \to G (n) \in dom \int^{1}$
321	320	ralrimiva	$⊢ φ \to \forall n \in ℕ G (n) \in dom \int^{1}$
322		ffnfv	$⊢ G : ℕ ⟶ dom \int^{1} \leftrightarrow (G Fn ℕ \land \forall n \in ℕ G (n) \in dom \int^{1})$
323	8 321 322	sylanbrc	$⊢ φ \to G : ℕ ⟶ dom \int^{1}$

Metamath Proof Explorer

Theorem mbfi1fseqlem4

Proof