mbfi1fseqlem3

	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	mbfi1fseqlem3	$⊢ (φ \land A \in ℕ) \to G (A) : ℝ ⟶ ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$

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	mbfi1fseqlem2	$⊢ A \in ℕ \to G (A) = (x \in ℝ ⟼ if (x \in [- A, A], if (A J x \leq A, A J x, A), 0))$
6	5	adantl	$⊢ (φ \land A \in ℕ) \to G (A) = (x \in ℝ ⟼ if (x \in [- A, A], if (A J x \leq A, A J x, A), 0))$
7		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
8		simpr	$⊢ (m \in ℕ \land y \in ℝ) \to y \in ℝ$
9		ffvelcdm	$⊢ (F : ℝ ⟶ [0, +∞) \land y \in ℝ) \to F (y) \in [0, +∞)$
10	2 8 9	syl2an	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) \in [0, +∞)$
11	7 10	sselid	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) \in ℝ$
12		2nn	$⊢ 2 \in ℕ$
13		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
14		nnexpcl	$⊢ (2 \in ℕ \land m \in ℕ_{0}) \to 2^{m} \in ℕ$
15	12 13 14	sylancr	$⊢ m \in ℕ \to 2^{m} \in ℕ$
16	15	ad2antrl	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 2^{m} \in ℕ$
17	16	nnred	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 2^{m} \in ℝ$
18	11 17	remulcld	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) 2^{m} \in ℝ$
19		reflcl	$⊢ F (y) 2^{m} \in ℝ \to ⌊F (y) 2^{m}⌋ \in ℝ$
20	18 19	syl	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to ⌊F (y) 2^{m}⌋ \in ℝ$
21	20 16	nndivred	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ$
22	21	ralrimivva	$⊢ φ \to \forall m \in ℕ \forall y \in ℝ \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ$
23	3	fmpo	$⊢ \forall m \in ℕ \forall y \in ℝ \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ \leftrightarrow J : ℕ \times ℝ ⟶ ℝ$
24	22 23	sylib	$⊢ φ \to J : ℕ \times ℝ ⟶ ℝ$
25		fovcdm	$⊢ (J : ℕ \times ℝ ⟶ ℝ \land A \in ℕ \land x \in ℝ) \to A J x \in ℝ$
26	24 25	syl3an1	$⊢ (φ \land A \in ℕ \land x \in ℝ) \to A J x \in ℝ$
27	26	3expa	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A J x \in ℝ$
28		nnre	$⊢ A \in ℕ \to A \in ℝ$
29	28	ad2antlr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A \in ℝ$
30		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
31		nnexpcl	$⊢ (2 \in ℕ \land A \in ℕ_{0}) \to 2^{A} \in ℕ$
32	12 30 31	sylancr	$⊢ A \in ℕ \to 2^{A} \in ℕ$
33	32	ad2antlr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A} \in ℕ$
34		nnre	$⊢ 2^{A} \in ℕ \to 2^{A} \in ℝ$
35		nngt0	$⊢ 2^{A} \in ℕ \to 0 < 2^{A}$
36	34 35	jca	$⊢ 2^{A} \in ℕ \to (2^{A} \in ℝ \land 0 < 2^{A})$
37	33 36	syl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (2^{A} \in ℝ \land 0 < 2^{A})$
38		lemul1	$⊢ (A J x \in ℝ \land A \in ℝ \land (2^{A} \in ℝ \land 0 < 2^{A})) \to (A J x \leq A \leftrightarrow (A J x) 2^{A} \leq A 2^{A})$
39	27 29 37 38	syl3anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (A J x \leq A \leftrightarrow (A J x) 2^{A} \leq A 2^{A})$
40	39	biimpa	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (A J x) 2^{A} \leq A 2^{A}$
41		simpr	$⊢ (m = A \land y = x) \to y = x$
42	41	fveq2d	$⊢ (m = A \land y = x) \to F (y) = F (x)$
43		simpl	$⊢ (m = A \land y = x) \to m = A$
44	43	oveq2d	$⊢ (m = A \land y = x) \to 2^{m} = 2^{A}$
45	42 44	oveq12d	$⊢ (m = A \land y = x) \to F (y) 2^{m} = F (x) 2^{A}$
46	45	fveq2d	$⊢ (m = A \land y = x) \to ⌊F (y) 2^{m}⌋ = ⌊F (x) 2^{A}⌋$
47	46 44	oveq12d	$⊢ (m = A \land y = x) \to \frac{⌊F (y) 2^{m}⌋}{2^{m}} = \frac{⌊F (x) 2^{A}⌋}{2^{A}}$
48		ovex	$⊢ \frac{⌊F (x) 2^{A}⌋}{2^{A}} \in V$
49	47 3 48	ovmpoa	$⊢ (A \in ℕ \land x \in ℝ) \to A J x = \frac{⌊F (x) 2^{A}⌋}{2^{A}}$
50	49	ad4ant23	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to A J x = \frac{⌊F (x) 2^{A}⌋}{2^{A}}$
51	50	oveq1d	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (A J x) 2^{A} = (\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A}$
52	2	adantr	$⊢ (φ \land A \in ℕ) \to F : ℝ ⟶ [0, +∞)$
53	52	ffvelcdmda	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) \in [0, +∞)$
54		elrege0	$⊢ F (x) \in [0, +∞) \leftrightarrow (F (x) \in ℝ \land 0 \leq F (x))$
55	53 54	sylib	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (F (x) \in ℝ \land 0 \leq F (x))$
56	55	simpld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) \in ℝ$
57	33	nnred	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A} \in ℝ$
58	56 57	remulcld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) 2^{A} \in ℝ$
59	33	nnnn0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A} \in ℕ_{0}$
60	59	nn0ge0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq 2^{A}$
61		mulge0	$⊢ ((F (x) \in ℝ \land 0 \leq F (x)) \land (2^{A} \in ℝ \land 0 \leq 2^{A})) \to 0 \leq F (x) 2^{A}$
62	55 57 60 61	syl12anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq F (x) 2^{A}$
63		flge0nn0	$⊢ (F (x) 2^{A} \in ℝ \land 0 \leq F (x) 2^{A}) \to ⌊F (x) 2^{A}⌋ \in ℕ_{0}$
64	58 62 63	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A}⌋ \in ℕ_{0}$
65	64	adantr	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to ⌊F (x) 2^{A}⌋ \in ℕ_{0}$
66	65	nn0cnd	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to ⌊F (x) 2^{A}⌋ \in ℂ$
67	33	adantr	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to 2^{A} \in ℕ$
68	67	nncnd	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to 2^{A} \in ℂ$
69	67	nnne0d	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to 2^{A} \neq 0$
70	66 68 69	divcan1d	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A} = ⌊F (x) 2^{A}⌋$
71	51 70	eqtrd	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (A J x) 2^{A} = ⌊F (x) 2^{A}⌋$
72	71 65	eqeltrd	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (A J x) 2^{A} \in ℕ_{0}$
73		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
74	72 73	eleqtrdi	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (A J x) 2^{A} \in ℤ_{\geq 0}$
75		nnmulcl	$⊢ (A \in ℕ \land 2^{A} \in ℕ) \to A 2^{A} \in ℕ$
76	32 75	mpdan	$⊢ A \in ℕ \to A 2^{A} \in ℕ$
77	76	ad2antlr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A 2^{A} \in ℕ$
78	77	adantr	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to A 2^{A} \in ℕ$
79	78	nnzd	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to A 2^{A} \in ℤ$
80		elfz5	$⊢ ((A J x) 2^{A} \in ℤ_{\geq 0} \land A 2^{A} \in ℤ) \to ((A J x) 2^{A} \in (0 \dots A 2^{A}) \leftrightarrow (A J x) 2^{A} \leq A 2^{A})$
81	74 79 80	syl2anc	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to ((A J x) 2^{A} \in (0 \dots A 2^{A}) \leftrightarrow (A J x) 2^{A} \leq A 2^{A})$
82	40 81	mpbird	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (A J x) 2^{A} \in (0 \dots A 2^{A})$
83		oveq1	$⊢ m = (A J x) 2^{A} \to \frac{m}{2^{A}} = \frac{(A J x) 2^{A}}{2^{A}}$
84		eqid	$⊢ (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) = (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
85		ovex	$⊢ \frac{(A J x) 2^{A}}{2^{A}} \in V$
86	83 84 85	fvmpt	$⊢ (A J x) 2^{A} \in (0 \dots A 2^{A}) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) ((A J x) 2^{A}) = \frac{(A J x) 2^{A}}{2^{A}}$
87	82 86	syl	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) ((A J x) 2^{A}) = \frac{(A J x) 2^{A}}{2^{A}}$
88	27	adantr	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to A J x \in ℝ$
89	88	recnd	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to A J x \in ℂ$
90	89 68 69	divcan4d	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to \frac{(A J x) 2^{A}}{2^{A}} = A J x$
91	87 90	eqtrd	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) ((A J x) 2^{A}) = A J x$
92		elfznn0	$⊢ m \in (0 \dots A 2^{A}) \to m \in ℕ_{0}$
93	92	nn0red	$⊢ m \in (0 \dots A 2^{A}) \to m \in ℝ$
94	32	adantl	$⊢ (φ \land A \in ℕ) \to 2^{A} \in ℕ$
95		nndivre	$⊢ (m \in ℝ \land 2^{A} \in ℕ) \to \frac{m}{2^{A}} \in ℝ$
96	93 94 95	syl2anr	$⊢ ((φ \land A \in ℕ) \land m \in (0 \dots A 2^{A})) \to \frac{m}{2^{A}} \in ℝ$
97	96	fmpttd	$⊢ (φ \land A \in ℕ) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) : (0 \dots A 2^{A}) ⟶ ℝ$
98	97	ffnd	$⊢ (φ \land A \in ℕ) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) Fn (0 \dots A 2^{A})$
99	98	adantr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) Fn (0 \dots A 2^{A})$
100	99	adantr	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) Fn (0 \dots A 2^{A})$
101		fnfvelrn	$⊢ ((m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) Fn (0 \dots A 2^{A}) \land (A J x) 2^{A} \in (0 \dots A 2^{A})) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) ((A J x) 2^{A}) \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
102	100 82 101	syl2anc	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) ((A J x) 2^{A}) \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
103	91 102	eqeltrrd	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land A J x \leq A) \to A J x \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
104	77	nnnn0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A 2^{A} \in ℕ_{0}$
105	104 73	eleqtrdi	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A 2^{A} \in ℤ_{\geq 0}$
106		eluzfz2	$⊢ A 2^{A} \in ℤ_{\geq 0} \to A 2^{A} \in (0 \dots A 2^{A})$
107	105 106	syl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A 2^{A} \in (0 \dots A 2^{A})$
108		oveq1	$⊢ m = A 2^{A} \to \frac{m}{2^{A}} = \frac{A 2^{A}}{2^{A}}$
109		ovex	$⊢ \frac{A 2^{A}}{2^{A}} \in V$
110	108 84 109	fvmpt	$⊢ A 2^{A} \in (0 \dots A 2^{A}) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) (A 2^{A}) = \frac{A 2^{A}}{2^{A}}$
111	107 110	syl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) (A 2^{A}) = \frac{A 2^{A}}{2^{A}}$
112	29	recnd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A \in ℂ$
113	33	nncnd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A} \in ℂ$
114	33	nnne0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A} \neq 0$
115	112 113 114	divcan4d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to \frac{A 2^{A}}{2^{A}} = A$
116	111 115	eqtrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) (A 2^{A}) = A$
117		fnfvelrn	$⊢ ((m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) Fn (0 \dots A 2^{A}) \land A 2^{A} \in (0 \dots A 2^{A})) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) (A 2^{A}) \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
118	99 107 117	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) (A 2^{A}) \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
119	116 118	eqeltrrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
120	119	adantr	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land \neg A J x \leq A) \to A \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
121	103 120	ifclda	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (A J x \leq A, A J x, A) \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
122		eluzfz1	$⊢ A 2^{A} \in ℤ_{\geq 0} \to 0 \in (0 \dots A 2^{A})$
123	105 122	syl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \in (0 \dots A 2^{A})$
124		oveq1	$⊢ m = 0 \to \frac{m}{2^{A}} = \frac{0}{2^{A}}$
125		ovex	$⊢ \frac{0}{2^{A}} \in V$
126	124 84 125	fvmpt	$⊢ 0 \in (0 \dots A 2^{A}) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) (0) = \frac{0}{2^{A}}$
127	123 126	syl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) (0) = \frac{0}{2^{A}}$
128		nncn	$⊢ 2^{A} \in ℕ \to 2^{A} \in ℂ$
129		nnne0	$⊢ 2^{A} \in ℕ \to 2^{A} \neq 0$
130	128 129	div0d	$⊢ 2^{A} \in ℕ \to \frac{0}{2^{A}} = 0$
131	33 130	syl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to \frac{0}{2^{A}} = 0$
132	127 131	eqtrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) (0) = 0$
133		fnfvelrn	$⊢ ((m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) Fn (0 \dots A 2^{A}) \land 0 \in (0 \dots A 2^{A})) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) (0) \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
134	99 123 133	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}}) (0) \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
135	132 134	eqeltrrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
136	121 135	ifcld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \in ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$
137	6 136	fmpt3d	$⊢ (φ \land A \in ℕ) \to G (A) : ℝ ⟶ ran (m \in (0 \dots A 2^{A}) ⟼ \frac{m}{2^{A}})$

Metamath Proof Explorer

Theorem mbfi1fseqlem3

Proof