mbfi1fseqlem1

	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}})$
Assertion	mbfi1fseqlem1	$⊢ φ \to J : ℕ \times ℝ ⟶ [0, +∞)$

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		simpr	$⊢ (m \in ℕ \land y \in ℝ) \to y \in ℝ$
5		ffvelcdm	$⊢ (F : ℝ ⟶ [0, +∞) \land y \in ℝ) \to F (y) \in [0, +∞)$
6	2 4 5	syl2an	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) \in [0, +∞)$
7		elrege0	$⊢ F (y) \in [0, +∞) \leftrightarrow (F (y) \in ℝ \land 0 \leq F (y))$
8	6 7	sylib	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to (F (y) \in ℝ \land 0 \leq F (y))$
9	8	simpld	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) \in ℝ$
10		2nn	$⊢ 2 \in ℕ$
11		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
12		nnexpcl	$⊢ (2 \in ℕ \land m \in ℕ_{0}) \to 2^{m} \in ℕ$
13	10 11 12	sylancr	$⊢ m \in ℕ \to 2^{m} \in ℕ$
14	13	ad2antrl	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 2^{m} \in ℕ$
15	14	nnred	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 2^{m} \in ℝ$
16	9 15	remulcld	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) 2^{m} \in ℝ$
17		reflcl	$⊢ F (y) 2^{m} \in ℝ \to ⌊F (y) 2^{m}⌋ \in ℝ$
18	16 17	syl	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to ⌊F (y) 2^{m}⌋ \in ℝ$
19	18 14	nndivred	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ$
20	14	nnnn0d	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 2^{m} \in ℕ_{0}$
21	20	nn0ge0d	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 0 \leq 2^{m}$
22		mulge0	$⊢ ((F (y) \in ℝ \land 0 \leq F (y)) \land (2^{m} \in ℝ \land 0 \leq 2^{m})) \to 0 \leq F (y) 2^{m}$
23	8 15 21 22	syl12anc	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 0 \leq F (y) 2^{m}$
24		flge0nn0	$⊢ (F (y) 2^{m} \in ℝ \land 0 \leq F (y) 2^{m}) \to ⌊F (y) 2^{m}⌋ \in ℕ_{0}$
25	16 23 24	syl2anc	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to ⌊F (y) 2^{m}⌋ \in ℕ_{0}$
26	25	nn0ge0d	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 0 \leq ⌊F (y) 2^{m}⌋$
27	14	nngt0d	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 0 < 2^{m}$
28		divge0	$⊢ ((⌊F (y) 2^{m}⌋ \in ℝ \land 0 \leq ⌊F (y) 2^{m}⌋) \land (2^{m} \in ℝ \land 0 < 2^{m})) \to 0 \leq \frac{⌊F (y) 2^{m}⌋}{2^{m}}$
29	18 26 15 27 28	syl22anc	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 0 \leq \frac{⌊F (y) 2^{m}⌋}{2^{m}}$
30		elrege0	$⊢ \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in [0, +∞) \leftrightarrow (\frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ \land 0 \leq \frac{⌊F (y) 2^{m}⌋}{2^{m}})$
31	19 29 30	sylanbrc	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in [0, +∞)$
32	31	ralrimivva	$⊢ φ \to \forall m \in ℕ \forall y \in ℝ \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in [0, +∞)$
33	3	fmpo	$⊢ \forall m \in ℕ \forall y \in ℝ \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in [0, +∞) \leftrightarrow J : ℕ \times ℝ ⟶ [0, +∞)$
34	32 33	sylib	$⊢ φ \to J : ℕ \times ℝ ⟶ [0, +∞)$

Metamath Proof Explorer

Theorem mbfi1fseqlem1

Proof