mbfi1fseqlem6

Description: Lemma for mbfi1fseq . Verify that G converges pointwise to F , and wrap up the existential quantifier. (Contributed by Mario Carneiro, 16-Aug-2014) (Revised by Mario Carneiro, 23-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	mbfi1fseqlem6	$⊢ φ \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ F (x))$

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	1 2 3 4	mbfi1fseqlem4	$⊢ φ \to G : ℕ ⟶ dom \int^{1}$
6	1 2 3 4	mbfi1fseqlem5	$⊢ (φ \land n \in ℕ) \to (0_{𝑝} \leq_{f} G (n) \land G (n) \leq_{f} G (n + 1))$
7	6	ralrimiva	$⊢ φ \to \forall n \in ℕ (0_{𝑝} \leq_{f} G (n) \land G (n) \leq_{f} G (n + 1))$
8		simpr	$⊢ (φ \land x \in ℝ) \to x \in ℝ$
9	8	recnd	$⊢ (φ \land x \in ℝ) \to x \in ℂ$
10	9	abscld	$⊢ (φ \land x \in ℝ) \to \|x\| \in ℝ$
11	2	ffvelrnda	$⊢ (φ \land x \in ℝ) \to F (x) \in [0, +∞)$
12		elrege0	$⊢ F (x) \in [0, +∞) \leftrightarrow (F (x) \in ℝ \land 0 \leq F (x))$
13	11 12	sylib	$⊢ (φ \land x \in ℝ) \to (F (x) \in ℝ \land 0 \leq F (x))$
14	13	simpld	$⊢ (φ \land x \in ℝ) \to F (x) \in ℝ$
15	10 14	readdcld	$⊢ (φ \land x \in ℝ) \to \|x\| + F (x) \in ℝ$
16		arch	$⊢ \|x\| + F (x) \in ℝ \to \exists k \in ℕ \|x\| + F (x) < k$
17	15 16	syl	$⊢ (φ \land x \in ℝ) \to \exists k \in ℕ \|x\| + F (x) < k$
18		eqid	$⊢ ℤ_{\geq k} = ℤ_{\geq k}$
19		nnz	$⊢ k \in ℕ \to k \in ℤ$
20	19	ad2antrl	$⊢ ((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \to k \in ℤ$
21		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
22		1zzd	$⊢ (φ \land x \in ℝ) \to 1 \in ℤ$
23		halfcn	$⊢ \frac{1}{2} \in ℂ$
24	23	a1i	$⊢ (φ \land x \in ℝ) \to \frac{1}{2} \in ℂ$
25		halfre	$⊢ \frac{1}{2} \in ℝ$
26		halfge0	$⊢ 0 \leq \frac{1}{2}$
27		absid	$⊢ (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2}) \to \|\frac{1}{2}\| = \frac{1}{2}$
28	25 26 27	mp2an	$⊢ \|\frac{1}{2}\| = \frac{1}{2}$
29		halflt1	$⊢ \frac{1}{2} < 1$
30	28 29	eqbrtri	$⊢ \|\frac{1}{2}\| < 1$
31	30	a1i	$⊢ (φ \land x \in ℝ) \to \|\frac{1}{2}\| < 1$
32	24 31	expcnv	$⊢ (φ \land x \in ℝ) \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) ⇝ 0$
33	14	recnd	$⊢ (φ \land x \in ℝ) \to F (x) \in ℂ$
34		nnex	$⊢ ℕ \in V$
35	34	mptex	$⊢ (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) \in V$
36	35	a1i	$⊢ (φ \land x \in ℝ) \to (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) \in V$
37		nnnn0	$⊢ j \in ℕ \to j \in ℕ_{0}$
38	37	adantl	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to j \in ℕ_{0}$
39		oveq2	$⊢ n = j \to {(\frac{1}{2})}^{n} = {(\frac{1}{2})}^{j}$
40		eqid	$⊢ (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) = (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n})$
41		ovex	$⊢ {(\frac{1}{2})}^{j} \in V$
42	39 40 41	fvmpt	$⊢ j \in ℕ_{0} \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (j) = {(\frac{1}{2})}^{j}$
43	38 42	syl	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (j) = {(\frac{1}{2})}^{j}$
44		expcl	$⊢ (\frac{1}{2} \in ℂ \land j \in ℕ_{0}) \to {(\frac{1}{2})}^{j} \in ℂ$
45	23 38 44	sylancr	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to {(\frac{1}{2})}^{j} \in ℂ$
46	43 45	eqeltrd	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (j) \in ℂ$
47	39	oveq2d	$⊢ n = j \to F (x) - {(\frac{1}{2})}^{n} = F (x) - {(\frac{1}{2})}^{j}$
48		eqid	$⊢ (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) = (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n})$
49		ovex	$⊢ F (x) - {(\frac{1}{2})}^{j} \in V$
50	47 48 49	fvmpt	$⊢ j \in ℕ \to (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) (j) = F (x) - {(\frac{1}{2})}^{j}$
51	50	adantl	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) (j) = F (x) - {(\frac{1}{2})}^{j}$
52	43	oveq2d	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to F (x) - (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (j) = F (x) - {(\frac{1}{2})}^{j}$
53	51 52	eqtr4d	$⊢ ((φ \land x \in ℝ) \land j \in ℕ) \to (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) (j) = F (x) - (n \in ℕ_{0} ⟼ {(\frac{1}{2})}^{n}) (j)$
54	21 22 32 33 36 46 53	climsubc2	$⊢ (φ \land x \in ℝ) \to (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) ⇝ (F (x) - 0)$
55	33	subid1d	$⊢ (φ \land x \in ℝ) \to F (x) - 0 = F (x)$
56	54 55	breqtrd	$⊢ (φ \land x \in ℝ) \to (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) ⇝ F (x)$
57	56	adantr	$⊢ ((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \to (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) ⇝ F (x)$
58	34	mptex	$⊢ (n \in ℕ ⟼ G (n) (x)) \in V$
59	58	a1i	$⊢ ((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \to (n \in ℕ ⟼ G (n) (x)) \in V$
60		simprl	$⊢ ((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \to k \in ℕ$
61		eluznn	$⊢ (k \in ℕ \land j \in ℤ_{\geq k}) \to j \in ℕ$
62	60 61	sylan	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to j \in ℕ$
63	62 50	syl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) (j) = F (x) - {(\frac{1}{2})}^{j}$
64	14	ad2antrr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) \in ℝ$
65	62 37	syl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to j \in ℕ_{0}$
66		reexpcl	$⊢ (\frac{1}{2} \in ℝ \land j \in ℕ_{0}) \to {(\frac{1}{2})}^{j} \in ℝ$
67	25 65 66	sylancr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to {(\frac{1}{2})}^{j} \in ℝ$
68	64 67	resubcld	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) - {(\frac{1}{2})}^{j} \in ℝ$
69	63 68	eqeltrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) (j) \in ℝ$
70		fveq2	$⊢ n = j \to G (n) = G (j)$
71	70	fveq1d	$⊢ n = j \to G (n) (x) = G (j) (x)$
72		eqid	$⊢ (n \in ℕ ⟼ G (n) (x)) = (n \in ℕ ⟼ G (n) (x))$
73		fvex	$⊢ G (j) (x) \in V$
74	71 72 73	fvmpt	$⊢ j \in ℕ \to (n \in ℕ ⟼ G (n) (x)) (j) = G (j) (x)$
75	62 74	syl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (n \in ℕ ⟼ G (n) (x)) (j) = G (j) (x)$
76	5	ad3antrrr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to G : ℕ ⟶ dom \int^{1}$
77	76 62	ffvelrnd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to G (j) \in dom \int^{1}$
78		i1ff	$⊢ G (j) \in dom \int^{1} \to G (j) : ℝ ⟶ ℝ$
79	77 78	syl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to G (j) : ℝ ⟶ ℝ$
80	8	ad2antrr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to x \in ℝ$
81	79 80	ffvelrnd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to G (j) (x) \in ℝ$
82	75 81	eqeltrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (n \in ℕ ⟼ G (n) (x)) (j) \in ℝ$
83	33	ad2antrr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) \in ℂ$
84		2nn	$⊢ 2 \in ℕ$
85		nnexpcl	$⊢ (2 \in ℕ \land j \in ℕ_{0}) \to 2^{j} \in ℕ$
86	84 65 85	sylancr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 2^{j} \in ℕ$
87	86	nnred	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 2^{j} \in ℝ$
88	87	recnd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 2^{j} \in ℂ$
89	86	nnne0d	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 2^{j} \neq 0$
90	83 88 89	divcan4d	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \frac{F (x) 2^{j}}{2^{j}} = F (x)$
91	90	eqcomd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) = \frac{F (x) 2^{j}}{2^{j}}$
92		2cnd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 2 \in ℂ$
93		2ne0	$⊢ 2 \neq 0$
94	93	a1i	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 2 \neq 0$
95		eluzelz	$⊢ j \in ℤ_{\geq k} \to j \in ℤ$
96	95	adantl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to j \in ℤ$
97	92 94 96	exprecd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to {(\frac{1}{2})}^{j} = \frac{1}{2^{j}}$
98	91 97	oveq12d	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) - {(\frac{1}{2})}^{j} = (\frac{F (x) 2^{j}}{2^{j}}) - (\frac{1}{2^{j}})$
99	64 87	remulcld	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) 2^{j} \in ℝ$
100	99	recnd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) 2^{j} \in ℂ$
101		1cnd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 1 \in ℂ$
102	100 101 88 89	divsubdird	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \frac{F (x) 2^{j} - 1}{2^{j}} = (\frac{F (x) 2^{j}}{2^{j}}) - (\frac{1}{2^{j}})$
103	98 102	eqtr4d	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) - {(\frac{1}{2})}^{j} = \frac{F (x) 2^{j} - 1}{2^{j}}$
104		fllep1	$⊢ F (x) 2^{j} \in ℝ \to F (x) 2^{j} \leq ⌊F (x) 2^{j}⌋ + 1$
105	99 104	syl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) 2^{j} \leq ⌊F (x) 2^{j}⌋ + 1$
106		1red	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 1 \in ℝ$
107		reflcl	$⊢ F (x) 2^{j} \in ℝ \to ⌊F (x) 2^{j}⌋ \in ℝ$
108	99 107	syl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to ⌊F (x) 2^{j}⌋ \in ℝ$
109	99 106 108	lesubaddd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (F (x) 2^{j} - 1 \leq ⌊F (x) 2^{j}⌋ \leftrightarrow F (x) 2^{j} \leq ⌊F (x) 2^{j}⌋ + 1)$
110	105 109	mpbird	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) 2^{j} - 1 \leq ⌊F (x) 2^{j}⌋$
111		peano2rem	$⊢ F (x) 2^{j} \in ℝ \to F (x) 2^{j} - 1 \in ℝ$
112	99 111	syl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) 2^{j} - 1 \in ℝ$
113	86	nngt0d	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 0 < 2^{j}$
114		lediv1	$⊢ (F (x) 2^{j} - 1 \in ℝ \land ⌊F (x) 2^{j}⌋ \in ℝ \land (2^{j} \in ℝ \land 0 < 2^{j})) \to (F (x) 2^{j} - 1 \leq ⌊F (x) 2^{j}⌋ \leftrightarrow \frac{F (x) 2^{j} - 1}{2^{j}} \leq \frac{⌊F (x) 2^{j}⌋}{2^{j}})$
115	112 108 87 113 114	syl112anc	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (F (x) 2^{j} - 1 \leq ⌊F (x) 2^{j}⌋ \leftrightarrow \frac{F (x) 2^{j} - 1}{2^{j}} \leq \frac{⌊F (x) 2^{j}⌋}{2^{j}})$
116	110 115	mpbid	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \frac{F (x) 2^{j} - 1}{2^{j}} \leq \frac{⌊F (x) 2^{j}⌋}{2^{j}}$
117	103 116	eqbrtrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) - {(\frac{1}{2})}^{j} \leq \frac{⌊F (x) 2^{j}⌋}{2^{j}}$
118	1 2 3 4	mbfi1fseqlem2	$⊢ j \in ℕ \to G (j) = (x \in ℝ ⟼ if (x \in [- j, j], if (j J x \leq j, j J x, j), 0))$
119	62 118	syl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to G (j) = (x \in ℝ ⟼ if (x \in [- j, j], if (j J x \leq j, j J x, j), 0))$
120	119	fveq1d	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to G (j) (x) = (x \in ℝ ⟼ if (x \in [- j, j], if (j J x \leq j, j J x, j), 0)) (x)$
121		ovex	$⊢ j J x \in V$
122		vex	$⊢ j \in V$
123	121 122	ifex	$⊢ if (j J x \leq j, j J x, j) \in V$
124		c0ex	$⊢ 0 \in V$
125	123 124	ifex	$⊢ if (x \in [- j, j], if (j J x \leq j, j J x, j), 0) \in V$
126		eqid	$⊢ (x \in ℝ ⟼ if (x \in [- j, j], if (j J x \leq j, j J x, j), 0)) = (x \in ℝ ⟼ if (x \in [- j, j], if (j J x \leq j, j J x, j), 0))$
127	126	fvmpt2	$⊢ (x \in ℝ \land if (x \in [- j, j], if (j J x \leq j, j J x, j), 0) \in V) \to (x \in ℝ ⟼ if (x \in [- j, j], if (j J x \leq j, j J x, j), 0)) (x) = if (x \in [- j, j], if (j J x \leq j, j J x, j), 0)$
128	80 125 127	sylancl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (x \in ℝ ⟼ if (x \in [- j, j], if (j J x \leq j, j J x, j), 0)) (x) = if (x \in [- j, j], if (j J x \leq j, j J x, j), 0)$
129	75 120 128	3eqtrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (n \in ℕ ⟼ G (n) (x)) (j) = if (x \in [- j, j], if (j J x \leq j, j J x, j), 0)$
130	10	ad2antrr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \|x\| \in ℝ$
131	15	ad2antrr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \|x\| + F (x) \in ℝ$
132	62	nnred	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to j \in ℝ$
133	11	ad2antrr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) \in [0, +∞)$
134	133 12	sylib	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (F (x) \in ℝ \land 0 \leq F (x))$
135	134	simprd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 0 \leq F (x)$
136	130 64	addge01d	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (0 \leq F (x) \leftrightarrow \|x\| \leq \|x\| + F (x))$
137	135 136	mpbid	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \|x\| \leq \|x\| + F (x)$
138	60	adantr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to k \in ℕ$
139	138	nnred	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to k \in ℝ$
140		simplrr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \|x\| + F (x) < k$
141	131 139 140	ltled	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \|x\| + F (x) \leq k$
142		eluzle	$⊢ j \in ℤ_{\geq k} \to k \leq j$
143	142	adantl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to k \leq j$
144	131 139 132 141 143	letrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \|x\| + F (x) \leq j$
145	130 131 132 137 144	letrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \|x\| \leq j$
146	80 132	absled	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (\|x\| \leq j \leftrightarrow (- j \leq x \land x \leq j))$
147	145 146	mpbid	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (- j \leq x \land x \leq j)$
148	147	simpld	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to - j \leq x$
149	147	simprd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to x \leq j$
150	132	renegcld	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to - j \in ℝ$
151		elicc2	$⊢ (- j \in ℝ \land j \in ℝ) \to (x \in [- j, j] \leftrightarrow (x \in ℝ \land - j \leq x \land x \leq j))$
152	150 132 151	syl2anc	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (x \in [- j, j] \leftrightarrow (x \in ℝ \land - j \leq x \land x \leq j))$
153	80 148 149 152	mpbir3and	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to x \in [- j, j]$
154	153	iftrued	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to if (x \in [- j, j], if (j J x \leq j, j J x, j), 0) = if (j J x \leq j, j J x, j)$
155		simpr	$⊢ (m = j \land y = x) \to y = x$
156	155	fveq2d	$⊢ (m = j \land y = x) \to F (y) = F (x)$
157		simpl	$⊢ (m = j \land y = x) \to m = j$
158	157	oveq2d	$⊢ (m = j \land y = x) \to 2^{m} = 2^{j}$
159	156 158	oveq12d	$⊢ (m = j \land y = x) \to F (y) 2^{m} = F (x) 2^{j}$
160	159	fveq2d	$⊢ (m = j \land y = x) \to ⌊F (y) 2^{m}⌋ = ⌊F (x) 2^{j}⌋$
161	160 158	oveq12d	$⊢ (m = j \land y = x) \to \frac{⌊F (y) 2^{m}⌋}{2^{m}} = \frac{⌊F (x) 2^{j}⌋}{2^{j}}$
162		ovex	$⊢ \frac{⌊F (x) 2^{j}⌋}{2^{j}} \in V$
163	161 3 162	ovmpoa	$⊢ (j \in ℕ \land x \in ℝ) \to j J x = \frac{⌊F (x) 2^{j}⌋}{2^{j}}$
164	62 80 163	syl2anc	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to j J x = \frac{⌊F (x) 2^{j}⌋}{2^{j}}$
165	108 86	nndivred	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \frac{⌊F (x) 2^{j}⌋}{2^{j}} \in ℝ$
166		flle	$⊢ F (x) 2^{j} \in ℝ \to ⌊F (x) 2^{j}⌋ \leq F (x) 2^{j}$
167	99 166	syl	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to ⌊F (x) 2^{j}⌋ \leq F (x) 2^{j}$
168		ledivmul2	$⊢ (⌊F (x) 2^{j}⌋ \in ℝ \land F (x) \in ℝ \land (2^{j} \in ℝ \land 0 < 2^{j})) \to (\frac{⌊F (x) 2^{j}⌋}{2^{j}} \leq F (x) \leftrightarrow ⌊F (x) 2^{j}⌋ \leq F (x) 2^{j})$
169	108 64 87 113 168	syl112anc	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (\frac{⌊F (x) 2^{j}⌋}{2^{j}} \leq F (x) \leftrightarrow ⌊F (x) 2^{j}⌋ \leq F (x) 2^{j})$
170	167 169	mpbird	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \frac{⌊F (x) 2^{j}⌋}{2^{j}} \leq F (x)$
171	9	ad2antrr	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to x \in ℂ$
172	171	absge0d	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to 0 \leq \|x\|$
173	64 130	addge02d	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (0 \leq \|x\| \leftrightarrow F (x) \leq \|x\| + F (x))$
174	172 173	mpbid	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) \leq \|x\| + F (x)$
175	64 131 132 174 144	letrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to F (x) \leq j$
176	165 64 132 170 175	letrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to \frac{⌊F (x) 2^{j}⌋}{2^{j}} \leq j$
177	164 176	eqbrtrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to j J x \leq j$
178	177	iftrued	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to if (j J x \leq j, j J x, j) = j J x$
179	178 164	eqtrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to if (j J x \leq j, j J x, j) = \frac{⌊F (x) 2^{j}⌋}{2^{j}}$
180	129 154 179	3eqtrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (n \in ℕ ⟼ G (n) (x)) (j) = \frac{⌊F (x) 2^{j}⌋}{2^{j}}$
181	117 63 180	3brtr4d	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (n \in ℕ ⟼ F (x) - {(\frac{1}{2})}^{n}) (j) \leq (n \in ℕ ⟼ G (n) (x)) (j)$
182	180 170	eqbrtrd	$⊢ (((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \land j \in ℤ_{\geq k}) \to (n \in ℕ ⟼ G (n) (x)) (j) \leq F (x)$
183	18 20 57 59 69 82 181 182	climsqz	$⊢ ((φ \land x \in ℝ) \land (k \in ℕ \land \|x\| + F (x) < k)) \to (n \in ℕ ⟼ G (n) (x)) ⇝ F (x)$
184	17 183	rexlimddv	$⊢ (φ \land x \in ℝ) \to (n \in ℕ ⟼ G (n) (x)) ⇝ F (x)$
185	184	ralrimiva	$⊢ φ \to \forall x \in ℝ (n \in ℕ ⟼ G (n) (x)) ⇝ F (x)$
186	34	mptex	$⊢ (m \in ℕ ⟼ (x \in ℝ ⟼ if (x \in [- m, m], if (m J x \leq m, m J x, m), 0))) \in V$
187	4 186	eqeltri	$⊢ G \in V$
188		feq1	$⊢ g = G \to (g : ℕ ⟶ dom \int^{1} \leftrightarrow G : ℕ ⟶ dom \int^{1})$
189		fveq1	$⊢ g = G \to g (n) = G (n)$
190	189	breq2d	$⊢ g = G \to (0_{𝑝} \leq_{f} g (n) \leftrightarrow 0_{𝑝} \leq_{f} G (n))$
191		fveq1	$⊢ g = G \to g (n + 1) = G (n + 1)$
192	189 191	breq12d	$⊢ g = G \to (g (n) \leq_{f} g (n + 1) \leftrightarrow G (n) \leq_{f} G (n + 1))$
193	190 192	anbi12d	$⊢ g = G \to ((0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \leftrightarrow (0_{𝑝} \leq_{f} G (n) \land G (n) \leq_{f} G (n + 1)))$
194	193	ralbidv	$⊢ g = G \to (\forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \leftrightarrow \forall n \in ℕ (0_{𝑝} \leq_{f} G (n) \land G (n) \leq_{f} G (n + 1)))$
195	189	fveq1d	$⊢ g = G \to g (n) (x) = G (n) (x)$
196	195	mpteq2dv	$⊢ g = G \to (n \in ℕ ⟼ g (n) (x)) = (n \in ℕ ⟼ G (n) (x))$
197	196	breq1d	$⊢ g = G \to ((n \in ℕ ⟼ g (n) (x)) ⇝ F (x) \leftrightarrow (n \in ℕ ⟼ G (n) (x)) ⇝ F (x))$
198	197	ralbidv	$⊢ g = G \to (\forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ F (x) \leftrightarrow \forall x \in ℝ (n \in ℕ ⟼ G (n) (x)) ⇝ F (x))$
199	188 194 198	3anbi123d	$⊢ g = G \to ((g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ F (x)) \leftrightarrow (G : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} G (n) \land G (n) \leq_{f} G (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ G (n) (x)) ⇝ F (x)))$
200	187 199	spcev	$⊢ (G : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} G (n) \land G (n) \leq_{f} G (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ G (n) (x)) ⇝ F (x)) \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ F (x))$
201	5 7 185 200	syl3anc	$⊢ φ \to \exists g (g : ℕ ⟶ dom \int^{1} \land \forall n \in ℕ (0_{𝑝} \leq_{f} g (n) \land g (n) \leq_{f} g (n + 1)) \land \forall x \in ℝ (n \in ℕ ⟼ g (n) (x)) ⇝ F (x))$

Metamath Proof Explorer

Theorem mbfi1fseqlem6

Proof