mbfi1fseqlem5

Description: Lemma for mbfi1fseq . Verify that G describes an increasing sequence of positive functions. (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	mbfi1fseqlem5	$⊢ (φ \land A \in ℕ) \to (0_{𝑝} \leq_{f} G (A) \land G (A) \leq_{f} G (A + 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	2	adantr	$⊢ (φ \land A \in ℕ) \to F : ℝ ⟶ [0, +∞)$
6	5	ffvelcdmda	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) \in [0, +∞)$
7		elrege0	$⊢ F (x) \in [0, +∞) \leftrightarrow (F (x) \in ℝ \land 0 \leq F (x))$
8	6 7	sylib	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (F (x) \in ℝ \land 0 \leq F (x))$
9	8	simpld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) \in ℝ$
10		2nn	$⊢ 2 \in ℕ$
11		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
12		nnexpcl	$⊢ (2 \in ℕ \land A \in ℕ_{0}) \to 2^{A} \in ℕ$
13	10 11 12	sylancr	$⊢ A \in ℕ \to 2^{A} \in ℕ$
14	13	ad2antlr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A} \in ℕ$
15	14	nnred	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A} \in ℝ$
16	9 15	remulcld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) 2^{A} \in ℝ$
17	14	nnnn0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A} \in ℕ_{0}$
18	17	nn0ge0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq 2^{A}$
19		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}$
20	8 15 18 19	syl12anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq F (x) 2^{A}$
21		flge0nn0	$⊢ (F (x) 2^{A} \in ℝ \land 0 \leq F (x) 2^{A}) \to ⌊F (x) 2^{A}⌋ \in ℕ_{0}$
22	16 20 21	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A}⌋ \in ℕ_{0}$
23	22	nn0red	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A}⌋ \in ℝ$
24	22	nn0ge0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq ⌊F (x) 2^{A}⌋$
25	14	nngt0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 < 2^{A}$
26		divge0	$⊢ ((⌊F (x) 2^{A}⌋ \in ℝ \land 0 \leq ⌊F (x) 2^{A}⌋) \land (2^{A} \in ℝ \land 0 < 2^{A})) \to 0 \leq \frac{⌊F (x) 2^{A}⌋}{2^{A}}$
27	23 24 15 25 26	syl22anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq \frac{⌊F (x) 2^{A}⌋}{2^{A}}$
28		simpr	$⊢ (m = A \land y = x) \to y = x$
29	28	fveq2d	$⊢ (m = A \land y = x) \to F (y) = F (x)$
30		simpl	$⊢ (m = A \land y = x) \to m = A$
31	30	oveq2d	$⊢ (m = A \land y = x) \to 2^{m} = 2^{A}$
32	29 31	oveq12d	$⊢ (m = A \land y = x) \to F (y) 2^{m} = F (x) 2^{A}$
33	32	fveq2d	$⊢ (m = A \land y = x) \to ⌊F (y) 2^{m}⌋ = ⌊F (x) 2^{A}⌋$
34	33 31	oveq12d	$⊢ (m = A \land y = x) \to \frac{⌊F (y) 2^{m}⌋}{2^{m}} = \frac{⌊F (x) 2^{A}⌋}{2^{A}}$
35		ovex	$⊢ \frac{⌊F (x) 2^{A}⌋}{2^{A}} \in V$
36	34 3 35	ovmpoa	$⊢ (A \in ℕ \land x \in ℝ) \to A J x = \frac{⌊F (x) 2^{A}⌋}{2^{A}}$
37	36	adantll	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A J x = \frac{⌊F (x) 2^{A}⌋}{2^{A}}$
38	27 37	breqtrrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq A J x$
39	11	nn0ge0d	$⊢ A \in ℕ \to 0 \leq A$
40	39	ad2antlr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq A$
41		breq2	$⊢ A J x = if (A J x \leq A, A J x, A) \to (0 \leq A J x \leftrightarrow 0 \leq if (A J x \leq A, A J x, A))$
42		breq2	$⊢ A = if (A J x \leq A, A J x, A) \to (0 \leq A \leftrightarrow 0 \leq if (A J x \leq A, A J x, A))$
43	41 42	ifboth	$⊢ (0 \leq A J x \land 0 \leq A) \to 0 \leq if (A J x \leq A, A J x, A)$
44	38 40 43	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq if (A J x \leq A, A J x, A)$
45		0le0	$⊢ 0 \leq 0$
46		breq2	$⊢ if (A J x \leq A, A J x, A) = if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \to (0 \leq if (A J x \leq A, A J x, A) \leftrightarrow 0 \leq if (x \in [- A, A], if (A J x \leq A, A J x, A), 0))$
47		breq2	$⊢ 0 = if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (x \in [- A, A], if (A J x \leq A, A J x, A), 0))$
48	46 47	ifboth	$⊢ (0 \leq if (A J x \leq A, A J x, A) \land 0 \leq 0) \to 0 \leq if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)$
49	44 45 48	sylancl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)$
50	49	ralrimiva	$⊢ (φ \land A \in ℕ) \to \forall x \in ℝ 0 \leq if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)$
51		0re	$⊢ 0 \in ℝ$
52		fnconstg	$⊢ 0 \in ℝ \to (ℂ \times \{0\}) Fn ℂ$
53	51 52	ax-mp	$⊢ (ℂ \times \{0\}) Fn ℂ$
54		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
55	54	fneq1i	$⊢ 0_{𝑝} Fn ℂ \leftrightarrow (ℂ \times \{0\}) Fn ℂ$
56	53 55	mpbir	$⊢ 0_{𝑝} Fn ℂ$
57	56	a1i	$⊢ (φ \land A \in ℕ) \to 0_{𝑝} Fn ℂ$
58	1 2 3 4	mbfi1fseqlem4	$⊢ φ \to G : ℕ ⟶ dom \int^{1}$
59	58	ffvelcdmda	$⊢ (φ \land A \in ℕ) \to G (A) \in dom \int^{1}$
60		i1ff	$⊢ G (A) \in dom \int^{1} \to G (A) : ℝ ⟶ ℝ$
61		ffn	$⊢ G (A) : ℝ ⟶ ℝ \to G (A) Fn ℝ$
62	59 60 61	3syl	$⊢ (φ \land A \in ℕ) \to G (A) Fn ℝ$
63		cnex	$⊢ ℂ \in V$
64	63	a1i	$⊢ (φ \land A \in ℕ) \to ℂ \in V$
65		reex	$⊢ ℝ \in V$
66	65	a1i	$⊢ (φ \land A \in ℕ) \to ℝ \in V$
67		ax-resscn	$⊢ ℝ \subseteq ℂ$
68		sseqin2	$⊢ ℝ \subseteq ℂ \leftrightarrow ℂ \cap ℝ = ℝ$
69	67 68	mpbi	$⊢ ℂ \cap ℝ = ℝ$
70		0pval	$⊢ x \in ℂ \to 0_{𝑝} (x) = 0$
71	70	adantl	$⊢ ((φ \land A \in ℕ) \land x \in ℂ) \to 0_{𝑝} (x) = 0$
72	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))$
73	72	fveq1d	$⊢ A \in ℕ \to G (A) (x) = (x \in ℝ ⟼ if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)) (x)$
74	73	ad2antlr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to G (A) (x) = (x \in ℝ ⟼ if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)) (x)$
75		simpr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to x \in ℝ$
76		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
77		simpr	$⊢ (m \in ℕ \land y \in ℝ) \to y \in ℝ$
78		ffvelcdm	$⊢ (F : ℝ ⟶ [0, +∞) \land y \in ℝ) \to F (y) \in [0, +∞)$
79	2 77 78	syl2an	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) \in [0, +∞)$
80	76 79	sselid	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) \in ℝ$
81		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
82		nnexpcl	$⊢ (2 \in ℕ \land m \in ℕ_{0}) \to 2^{m} \in ℕ$
83	10 81 82	sylancr	$⊢ m \in ℕ \to 2^{m} \in ℕ$
84	83	ad2antrl	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 2^{m} \in ℕ$
85	84	nnred	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to 2^{m} \in ℝ$
86	80 85	remulcld	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to F (y) 2^{m} \in ℝ$
87		reflcl	$⊢ F (y) 2^{m} \in ℝ \to ⌊F (y) 2^{m}⌋ \in ℝ$
88	86 87	syl	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to ⌊F (y) 2^{m}⌋ \in ℝ$
89	88 84	nndivred	$⊢ (φ \land (m \in ℕ \land y \in ℝ)) \to \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ$
90	89	ralrimivva	$⊢ φ \to \forall m \in ℕ \forall y \in ℝ \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ$
91	3	fmpo	$⊢ \forall m \in ℕ \forall y \in ℝ \frac{⌊F (y) 2^{m}⌋}{2^{m}} \in ℝ \leftrightarrow J : ℕ \times ℝ ⟶ ℝ$
92	90 91	sylib	$⊢ φ \to J : ℕ \times ℝ ⟶ ℝ$
93		fovcdm	$⊢ (J : ℕ \times ℝ ⟶ ℝ \land A \in ℕ \land x \in ℝ) \to A J x \in ℝ$
94	92 93	syl3an1	$⊢ (φ \land A \in ℕ \land x \in ℝ) \to A J x \in ℝ$
95	94	3expa	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A J x \in ℝ$
96		nnre	$⊢ A \in ℕ \to A \in ℝ$
97	96	ad2antlr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A \in ℝ$
98	95 97	ifcld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (A J x \leq A, A J x, A) \in ℝ$
99		ifcl	$⊢ (if (A J x \leq A, A J x, A) \in ℝ \land 0 \in ℝ) \to if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \in ℝ$
100	98 51 99	sylancl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \in ℝ$
101		eqid	$⊢ (x \in ℝ ⟼ if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)) = (x \in ℝ ⟼ if (x \in [- A, A], if (A J x \leq A, A J x, A), 0))$
102	101	fvmpt2	$⊢ (x \in ℝ \land if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \in ℝ) \to (x \in ℝ ⟼ if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)) (x) = if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)$
103	75 100 102	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (x \in ℝ ⟼ if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)) (x) = if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)$
104	74 103	eqtrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to G (A) (x) = if (x \in [- A, A], if (A J x \leq A, A J x, A), 0)$
105	57 62 64 66 69 71 104	ofrfval	$⊢ (φ \land A \in ℕ) \to (0_{𝑝} \leq_{f} G (A) \leftrightarrow \forall x \in ℝ 0 \leq if (x \in [- A, A], if (A J x \leq A, A J x, A), 0))$
106	50 105	mpbird	$⊢ (φ \land A \in ℕ) \to 0_{𝑝} \leq_{f} G (A)$
107	1 2 3	mbfi1fseqlem1	$⊢ φ \to J : ℕ \times ℝ ⟶ [0, +∞)$
108	107	ad2antrr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to J : ℕ \times ℝ ⟶ [0, +∞)$
109		peano2nn	$⊢ A \in ℕ \to A + 1 \in ℕ$
110	109	ad2antlr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A + 1 \in ℕ$
111	108 110 75	fovcdmd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (A + 1) J x \in [0, +∞)$
112		elrege0	$⊢ (A + 1) J x \in [0, +∞) \leftrightarrow ((A + 1) J x \in ℝ \land 0 \leq (A + 1) J x)$
113	111 112	sylib	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ((A + 1) J x \in ℝ \land 0 \leq (A + 1) J x)$
114	113	simpld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (A + 1) J x \in ℝ$
115		min1	$⊢ (A J x \in ℝ \land A \in ℝ) \to if (A J x \leq A, A J x, A) \leq A J x$
116	95 97 115	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (A J x \leq A, A J x, A) \leq A J x$
117		2cn	$⊢ 2 \in ℂ$
118	11	ad2antlr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A \in ℕ_{0}$
119		expp1	$⊢ (2 \in ℂ \land A \in ℕ_{0}) \to 2^{A + 1} = 2^{A} \cdot 2$
120	117 118 119	sylancr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A + 1} = 2^{A} \cdot 2$
121	120	oveq2d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A + 1} = (\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A} \cdot 2$
122	37 95	eqeltrrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to \frac{⌊F (x) 2^{A}⌋}{2^{A}} \in ℝ$
123	122	recnd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to \frac{⌊F (x) 2^{A}⌋}{2^{A}} \in ℂ$
124	15	recnd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A} \in ℂ$
125		2cnd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2 \in ℂ$
126	123 124 125	mulassd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A} \cdot 2 = (\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A} \cdot 2$
127	23	recnd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A}⌋ \in ℂ$
128	14	nnne0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A} \neq 0$
129	127 124 128	divcan1d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A} = ⌊F (x) 2^{A}⌋$
130	129	oveq1d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A} \cdot 2 = ⌊F (x) 2^{A}⌋ \cdot 2$
131	121 126 130	3eqtr2d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A + 1} = ⌊F (x) 2^{A}⌋ \cdot 2$
132		flle	$⊢ F (x) 2^{A} \in ℝ \to ⌊F (x) 2^{A}⌋ \leq F (x) 2^{A}$
133	16 132	syl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A}⌋ \leq F (x) 2^{A}$
134		2re	$⊢ 2 \in ℝ$
135		2pos	$⊢ 0 < 2$
136	134 135	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
137	136	a1i	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (2 \in ℝ \land 0 < 2)$
138		lemul1	$⊢ (⌊F (x) 2^{A}⌋ \in ℝ \land F (x) 2^{A} \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (⌊F (x) 2^{A}⌋ \leq F (x) 2^{A} \leftrightarrow ⌊F (x) 2^{A}⌋ \cdot 2 \leq F (x) 2^{A} \cdot 2)$
139	23 16 137 138	syl3anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (⌊F (x) 2^{A}⌋ \leq F (x) 2^{A} \leftrightarrow ⌊F (x) 2^{A}⌋ \cdot 2 \leq F (x) 2^{A} \cdot 2)$
140	133 139	mpbid	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A}⌋ \cdot 2 \leq F (x) 2^{A} \cdot 2$
141	120	oveq2d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) 2^{A + 1} = F (x) 2^{A} \cdot 2$
142	9	recnd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) \in ℂ$
143	142 124 125	mulassd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) 2^{A} \cdot 2 = F (x) 2^{A} \cdot 2$
144	141 143	eqtr4d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) 2^{A + 1} = F (x) 2^{A} \cdot 2$
145	140 144	breqtrrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A}⌋ \cdot 2 \leq F (x) 2^{A + 1}$
146	110	nnnn0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A + 1 \in ℕ_{0}$
147		nnexpcl	$⊢ (2 \in ℕ \land A + 1 \in ℕ_{0}) \to 2^{A + 1} \in ℕ$
148	10 146 147	sylancr	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A + 1} \in ℕ$
149	148	nnred	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 2^{A + 1} \in ℝ$
150	9 149	remulcld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to F (x) 2^{A + 1} \in ℝ$
151	16	flcld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A}⌋ \in ℤ$
152		2z	$⊢ 2 \in ℤ$
153		zmulcl	$⊢ (⌊F (x) 2^{A}⌋ \in ℤ \land 2 \in ℤ) \to ⌊F (x) 2^{A}⌋ \cdot 2 \in ℤ$
154	151 152 153	sylancl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A}⌋ \cdot 2 \in ℤ$
155		flge	$⊢ (F (x) 2^{A + 1} \in ℝ \land ⌊F (x) 2^{A}⌋ \cdot 2 \in ℤ) \to (⌊F (x) 2^{A}⌋ \cdot 2 \leq F (x) 2^{A + 1} \leftrightarrow ⌊F (x) 2^{A}⌋ \cdot 2 \leq ⌊F (x) 2^{A + 1}⌋)$
156	150 154 155	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (⌊F (x) 2^{A}⌋ \cdot 2 \leq F (x) 2^{A + 1} \leftrightarrow ⌊F (x) 2^{A}⌋ \cdot 2 \leq ⌊F (x) 2^{A + 1}⌋)$
157	145 156	mpbid	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A}⌋ \cdot 2 \leq ⌊F (x) 2^{A + 1}⌋$
158	131 157	eqbrtrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A + 1} \leq ⌊F (x) 2^{A + 1}⌋$
159		reflcl	$⊢ F (x) 2^{A + 1} \in ℝ \to ⌊F (x) 2^{A + 1}⌋ \in ℝ$
160	150 159	syl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ⌊F (x) 2^{A + 1}⌋ \in ℝ$
161	148	nngt0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 < 2^{A + 1}$
162		lemuldiv	$⊢ (\frac{⌊F (x) 2^{A}⌋}{2^{A}} \in ℝ \land ⌊F (x) 2^{A + 1}⌋ \in ℝ \land (2^{A + 1} \in ℝ \land 0 < 2^{A + 1})) \to ((\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A + 1} \leq ⌊F (x) 2^{A + 1}⌋ \leftrightarrow \frac{⌊F (x) 2^{A}⌋}{2^{A}} \leq \frac{⌊F (x) 2^{A + 1}⌋}{2^{A + 1}})$
163	122 160 149 161 162	syl112anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to ((\frac{⌊F (x) 2^{A}⌋}{2^{A}}) 2^{A + 1} \leq ⌊F (x) 2^{A + 1}⌋ \leftrightarrow \frac{⌊F (x) 2^{A}⌋}{2^{A}} \leq \frac{⌊F (x) 2^{A + 1}⌋}{2^{A + 1}})$
164	158 163	mpbid	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to \frac{⌊F (x) 2^{A}⌋}{2^{A}} \leq \frac{⌊F (x) 2^{A + 1}⌋}{2^{A + 1}}$
165		simpr	$⊢ (m = A + 1 \land y = x) \to y = x$
166	165	fveq2d	$⊢ (m = A + 1 \land y = x) \to F (y) = F (x)$
167		simpl	$⊢ (m = A + 1 \land y = x) \to m = A + 1$
168	167	oveq2d	$⊢ (m = A + 1 \land y = x) \to 2^{m} = 2^{A + 1}$
169	166 168	oveq12d	$⊢ (m = A + 1 \land y = x) \to F (y) 2^{m} = F (x) 2^{A + 1}$
170	169	fveq2d	$⊢ (m = A + 1 \land y = x) \to ⌊F (y) 2^{m}⌋ = ⌊F (x) 2^{A + 1}⌋$
171	170 168	oveq12d	$⊢ (m = A + 1 \land y = x) \to \frac{⌊F (y) 2^{m}⌋}{2^{m}} = \frac{⌊F (x) 2^{A + 1}⌋}{2^{A + 1}}$
172		ovex	$⊢ \frac{⌊F (x) 2^{A + 1}⌋}{2^{A + 1}} \in V$
173	171 3 172	ovmpoa	$⊢ (A + 1 \in ℕ \land x \in ℝ) \to (A + 1) J x = \frac{⌊F (x) 2^{A + 1}⌋}{2^{A + 1}}$
174	110 75 173	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (A + 1) J x = \frac{⌊F (x) 2^{A + 1}⌋}{2^{A + 1}}$
175	164 37 174	3brtr4d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A J x \leq (A + 1) J x$
176	98 95 114 116 175	letrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (A J x \leq A, A J x, A) \leq (A + 1) J x$
177	110	nnred	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A + 1 \in ℝ$
178		min2	$⊢ (A J x \in ℝ \land A \in ℝ) \to if (A J x \leq A, A J x, A) \leq A$
179	95 97 178	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (A J x \leq A, A J x, A) \leq A$
180	97	lep1d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to A \leq A + 1$
181	98 97 177 179 180	letrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (A J x \leq A, A J x, A) \leq A + 1$
182		breq2	$⊢ (A + 1) J x = if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1) \to (if (A J x \leq A, A J x, A) \leq (A + 1) J x \leftrightarrow if (A J x \leq A, A J x, A) \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1))$
183		breq2	$⊢ A + 1 = if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1) \to (if (A J x \leq A, A J x, A) \leq A + 1 \leftrightarrow if (A J x \leq A, A J x, A) \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1))$
184	182 183	ifboth	$⊢ (if (A J x \leq A, A J x, A) \leq (A + 1) J x \land if (A J x \leq A, A J x, A) \leq A + 1) \to if (A J x \leq A, A J x, A) \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1)$
185	176 181 184	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (A J x \leq A, A J x, A) \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1)$
186	185	adantr	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land x \in [- A, A]) \to if (A J x \leq A, A J x, A) \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1)$
187		iftrue	$⊢ x \in [- A, A] \to if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) = if (A J x \leq A, A J x, A)$
188	187	adantl	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land x \in [- A, A]) \to if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) = if (A J x \leq A, A J x, A)$
189	177	renegcld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to - (A + 1) \in ℝ$
190	97 177	lenegd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (A \leq A + 1 \leftrightarrow - (A + 1) \leq - A)$
191	180 190	mpbid	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to - (A + 1) \leq - A$
192		iccss	$⊢ ((- (A + 1) \in ℝ \land A + 1 \in ℝ) \land (- (A + 1) \leq - A \land A \leq A + 1)) \to [- A, A] \subseteq [- (A + 1), A + 1]$
193	189 177 191 180 192	syl22anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to [- A, A] \subseteq [- (A + 1), A + 1]$
194	193	sselda	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land x \in [- A, A]) \to x \in [- (A + 1), A + 1]$
195	194	iftrued	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land x \in [- A, A]) \to if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0) = if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1)$
196	186 188 195	3brtr4d	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land x \in [- A, A]) \to if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \leq if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)$
197		iffalse	$⊢ \neg x \in [- A, A] \to if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) = 0$
198	197	adantl	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land \neg x \in [- A, A]) \to if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) = 0$
199	113	simprd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq (A + 1) J x$
200	146	nn0ge0d	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq A + 1$
201		breq2	$⊢ (A + 1) J x = if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1) \to (0 \leq (A + 1) J x \leftrightarrow 0 \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1))$
202		breq2	$⊢ A + 1 = if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1) \to (0 \leq A + 1 \leftrightarrow 0 \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1))$
203	201 202	ifboth	$⊢ (0 \leq (A + 1) J x \land 0 \leq A + 1) \to 0 \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1)$
204	199 200 203	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1)$
205		breq2	$⊢ if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1) = if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0) \to (0 \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1) \leftrightarrow 0 \leq if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0))$
206		breq2	$⊢ 0 = if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0))$
207	205 206	ifboth	$⊢ (0 \leq if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1) \land 0 \leq 0) \to 0 \leq if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)$
208	204 45 207	sylancl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to 0 \leq if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)$
209	208	adantr	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land \neg x \in [- A, A]) \to 0 \leq if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)$
210	198 209	eqbrtrd	$⊢ (((φ \land A \in ℕ) \land x \in ℝ) \land \neg x \in [- A, A]) \to if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \leq if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)$
211	196 210	pm2.61dan	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \leq if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)$
212	211	ralrimiva	$⊢ (φ \land A \in ℕ) \to \forall x \in ℝ if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \leq if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)$
213		ffvelcdm	$⊢ (G : ℕ ⟶ dom \int^{1} \land A + 1 \in ℕ) \to G (A + 1) \in dom \int^{1}$
214	58 109 213	syl2an	$⊢ (φ \land A \in ℕ) \to G (A + 1) \in dom \int^{1}$
215		i1ff	$⊢ G (A + 1) \in dom \int^{1} \to G (A + 1) : ℝ ⟶ ℝ$
216		ffn	$⊢ G (A + 1) : ℝ ⟶ ℝ \to G (A + 1) Fn ℝ$
217	214 215 216	3syl	$⊢ (φ \land A \in ℕ) \to G (A + 1) Fn ℝ$
218		inidm	$⊢ ℝ \cap ℝ = ℝ$
219	1 2 3 4	mbfi1fseqlem2	$⊢ A + 1 \in ℕ \to G (A + 1) = (x \in ℝ ⟼ if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0))$
220	219	fveq1d	$⊢ A + 1 \in ℕ \to G (A + 1) (x) = (x \in ℝ ⟼ if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)) (x)$
221	110 220	syl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to G (A + 1) (x) = (x \in ℝ ⟼ if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)) (x)$
222	114 177	ifcld	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1) \in ℝ$
223		ifcl	$⊢ (if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1) \in ℝ \land 0 \in ℝ) \to if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0) \in ℝ$
224	222 51 223	sylancl	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0) \in ℝ$
225		eqid	$⊢ (x \in ℝ ⟼ if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)) = (x \in ℝ ⟼ if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0))$
226	225	fvmpt2	$⊢ (x \in ℝ \land if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0) \in ℝ) \to (x \in ℝ ⟼ if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)) (x) = if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)$
227	75 224 226	syl2anc	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to (x \in ℝ ⟼ if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)) (x) = if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)$
228	221 227	eqtrd	$⊢ ((φ \land A \in ℕ) \land x \in ℝ) \to G (A + 1) (x) = if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0)$
229	62 217 66 66 218 104 228	ofrfval	$⊢ (φ \land A \in ℕ) \to (G (A) \leq_{f} G (A + 1) \leftrightarrow \forall x \in ℝ if (x \in [- A, A], if (A J x \leq A, A J x, A), 0) \leq if (x \in [- (A + 1), A + 1], if ((A + 1) J x \leq A + 1, (A + 1) J x, A + 1), 0))$
230	212 229	mpbird	$⊢ (φ \land A \in ℕ) \to G (A) \leq_{f} G (A + 1)$
231	106 230	jca	$⊢ (φ \land A \in ℕ) \to (0_{𝑝} \leq_{f} G (A) \land G (A) \leq_{f} G (A + 1))$

Metamath Proof Explorer

Theorem mbfi1fseqlem5

Proof