ioodvbdlimc2lem

Description: Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 3-Oct-2020)

	Ref	Expression
Hypotheses	ioodvbdlimc2lem.a	$⊢ φ \to A \in ℝ$
	ioodvbdlimc2lem.b	$⊢ φ \to B \in ℝ$
	ioodvbdlimc2lem.altb	$⊢ φ \to A < B$
	ioodvbdlimc2lem.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
	ioodvbdlimc2lem.dmdv	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	ioodvbdlimc2lem.dvbd	$⊢ φ \to \exists y \in ℝ \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq y$
	ioodvbdlimc2lem.y	$⊢ Y = sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
	ioodvbdlimc2lem.m	$⊢ M = ⌊\frac{1}{B - A}⌋ + 1$
	ioodvbdlimc2lem.s	$⊢ S = (j \in ℤ_{\geq M} ⟼ F (B - (\frac{1}{j})))$
	ioodvbdlimc2lem.r	$⊢ R = (j \in ℤ_{\geq M} ⟼ B - (\frac{1}{j}))$
	ioodvbdlimc2lem.n	$⊢ N = if (M \leq ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, M)$
	ioodvbdlimc2lem.ch	$⊢ χ \leftrightarrow (((((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \land z \in (A, B)) \land \|z - B\| < \frac{1}{j})$
Assertion	ioodvbdlimc2lem	$⊢ φ \to lim sup (S) \in (F {lim}_{ℂ} B)$

Proof

Step	Hyp	Ref	Expression
1		ioodvbdlimc2lem.a	$⊢ φ \to A \in ℝ$
2		ioodvbdlimc2lem.b	$⊢ φ \to B \in ℝ$
3		ioodvbdlimc2lem.altb	$⊢ φ \to A < B$
4		ioodvbdlimc2lem.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
5		ioodvbdlimc2lem.dmdv	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
6		ioodvbdlimc2lem.dvbd	$⊢ φ \to \exists y \in ℝ \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq y$
7		ioodvbdlimc2lem.y	$⊢ Y = sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
8		ioodvbdlimc2lem.m	$⊢ M = ⌊\frac{1}{B - A}⌋ + 1$
9		ioodvbdlimc2lem.s	$⊢ S = (j \in ℤ_{\geq M} ⟼ F (B - (\frac{1}{j})))$
10		ioodvbdlimc2lem.r	$⊢ R = (j \in ℤ_{\geq M} ⟼ B - (\frac{1}{j}))$
11		ioodvbdlimc2lem.n	$⊢ N = if (M \leq ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, M)$
12		ioodvbdlimc2lem.ch	$⊢ χ \leftrightarrow (((((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \land z \in (A, B)) \land \|z - B\| < \frac{1}{j})$
13		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
14		zssre	$⊢ ℤ \subseteq ℝ$
15	13 14	sstri	$⊢ ℤ_{\geq M} \subseteq ℝ$
16	15	a1i	$⊢ φ \to ℤ_{\geq M} \subseteq ℝ$
17	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
18	1 2	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
19	3 18	mpbid	$⊢ φ \to 0 < B - A$
20	19	gt0ne0d	$⊢ φ \to B - A \neq 0$
21	17 20	rereccld	$⊢ φ \to \frac{1}{B - A} \in ℝ$
22		0red	$⊢ φ \to 0 \in ℝ$
23	17 19	recgt0d	$⊢ φ \to 0 < \frac{1}{B - A}$
24	22 21 23	ltled	$⊢ φ \to 0 \leq \frac{1}{B - A}$
25		flge0nn0	$⊢ (\frac{1}{B - A} \in ℝ \land 0 \leq \frac{1}{B - A}) \to ⌊\frac{1}{B - A}⌋ \in ℕ_{0}$
26	21 24 25	syl2anc	$⊢ φ \to ⌊\frac{1}{B - A}⌋ \in ℕ_{0}$
27		peano2nn0	$⊢ ⌊\frac{1}{B - A}⌋ \in ℕ_{0} \to ⌊\frac{1}{B - A}⌋ + 1 \in ℕ_{0}$
28	26 27	syl	$⊢ φ \to ⌊\frac{1}{B - A}⌋ + 1 \in ℕ_{0}$
29	8 28	eqeltrid	$⊢ φ \to M \in ℕ_{0}$
30	29	nn0zd	$⊢ φ \to M \in ℤ$
31		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
32	31	uzsup	$⊢ M \in ℤ \to sup (ℤ_{\geq M} ℝ^{*} <) = +∞$
33	30 32	syl	$⊢ φ \to sup (ℤ_{\geq M} ℝ^{*} <) = +∞$
34	4	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to F : (A, B) ⟶ ℝ$
35	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
36	35	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to A \in ℝ^{*}$
37	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
38	37	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to B \in ℝ^{*}$
39	2	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to B \in ℝ$
40		eluzelre	$⊢ j \in ℤ_{\geq M} \to j \in ℝ$
41	40	adantl	$⊢ (φ \land j \in ℤ_{\geq M}) \to j \in ℝ$
42		0red	$⊢ (φ \land j \in ℤ_{\geq M}) \to 0 \in ℝ$
43		0red	$⊢ j \in ℤ_{\geq M} \to 0 \in ℝ$
44		1red	$⊢ j \in ℤ_{\geq M} \to 1 \in ℝ$
45	43 44	readdcld	$⊢ j \in ℤ_{\geq M} \to 0 + 1 \in ℝ$
46	45	adantl	$⊢ (φ \land j \in ℤ_{\geq M}) \to 0 + 1 \in ℝ$
47	43	ltp1d	$⊢ j \in ℤ_{\geq M} \to 0 < 0 + 1$
48	47	adantl	$⊢ (φ \land j \in ℤ_{\geq M}) \to 0 < 0 + 1$
49		eluzel2	$⊢ j \in ℤ_{\geq M} \to M \in ℤ$
50	49	zred	$⊢ j \in ℤ_{\geq M} \to M \in ℝ$
51	50	adantl	$⊢ (φ \land j \in ℤ_{\geq M}) \to M \in ℝ$
52	21	flcld	$⊢ φ \to ⌊\frac{1}{B - A}⌋ \in ℤ$
53	52	zred	$⊢ φ \to ⌊\frac{1}{B - A}⌋ \in ℝ$
54		1red	$⊢ φ \to 1 \in ℝ$
55	26	nn0ge0d	$⊢ φ \to 0 \leq ⌊\frac{1}{B - A}⌋$
56	22 53 54 55	leadd1dd	$⊢ φ \to 0 + 1 \leq ⌊\frac{1}{B - A}⌋ + 1$
57	56 8	breqtrrdi	$⊢ φ \to 0 + 1 \leq M$
58	57	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to 0 + 1 \leq M$
59		eluzle	$⊢ j \in ℤ_{\geq M} \to M \leq j$
60	59	adantl	$⊢ (φ \land j \in ℤ_{\geq M}) \to M \leq j$
61	46 51 41 58 60	letrd	$⊢ (φ \land j \in ℤ_{\geq M}) \to 0 + 1 \leq j$
62	42 46 41 48 61	ltletrd	$⊢ (φ \land j \in ℤ_{\geq M}) \to 0 < j$
63	62	gt0ne0d	$⊢ (φ \land j \in ℤ_{\geq M}) \to j \neq 0$
64	41 63	rereccld	$⊢ (φ \land j \in ℤ_{\geq M}) \to \frac{1}{j} \in ℝ$
65	39 64	resubcld	$⊢ (φ \land j \in ℤ_{\geq M}) \to B - (\frac{1}{j}) \in ℝ$
66	1	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to A \in ℝ$
67	29	nn0red	$⊢ φ \to M \in ℝ$
68	22 54	readdcld	$⊢ φ \to 0 + 1 \in ℝ$
69	53 54	readdcld	$⊢ φ \to ⌊\frac{1}{B - A}⌋ + 1 \in ℝ$
70	22	ltp1d	$⊢ φ \to 0 < 0 + 1$
71	22 68 69 70 56	ltletrd	$⊢ φ \to 0 < ⌊\frac{1}{B - A}⌋ + 1$
72	71 8	breqtrrdi	$⊢ φ \to 0 < M$
73	72	gt0ne0d	$⊢ φ \to M \neq 0$
74	67 73	rereccld	$⊢ φ \to \frac{1}{M} \in ℝ$
75	74	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to \frac{1}{M} \in ℝ$
76	39 75	resubcld	$⊢ (φ \land j \in ℤ_{\geq M}) \to B - (\frac{1}{M}) \in ℝ$
77	8	eqcomi	$⊢ ⌊\frac{1}{B - A}⌋ + 1 = M$
78	77	oveq2i	$⊢ \frac{1}{⌊\frac{1}{B - A}⌋ + 1} = \frac{1}{M}$
79	78 74	eqeltrid	$⊢ φ \to \frac{1}{⌊\frac{1}{B - A}⌋ + 1} \in ℝ$
80	21 23	elrpd	$⊢ φ \to \frac{1}{B - A} \in ℝ^{+}$
81	69 71	elrpd	$⊢ φ \to ⌊\frac{1}{B - A}⌋ + 1 \in ℝ^{+}$
82		1rp	$⊢ 1 \in ℝ^{+}$
83	82	a1i	$⊢ φ \to 1 \in ℝ^{+}$
84		fllelt	$⊢ \frac{1}{B - A} \in ℝ \to (⌊\frac{1}{B - A}⌋ \leq \frac{1}{B - A} \land \frac{1}{B - A} < ⌊\frac{1}{B - A}⌋ + 1)$
85	21 84	syl	$⊢ φ \to (⌊\frac{1}{B - A}⌋ \leq \frac{1}{B - A} \land \frac{1}{B - A} < ⌊\frac{1}{B - A}⌋ + 1)$
86	85	simprd	$⊢ φ \to \frac{1}{B - A} < ⌊\frac{1}{B - A}⌋ + 1$
87	80 81 83 86	ltdiv2dd	$⊢ φ \to \frac{1}{⌊\frac{1}{B - A}⌋ + 1} < \frac{1}{\frac{1}{B - A}}$
88	17	recnd	$⊢ φ \to B - A \in ℂ$
89	88 20	recrecd	$⊢ φ \to \frac{1}{\frac{1}{B - A}} = B - A$
90	87 89	breqtrd	$⊢ φ \to \frac{1}{⌊\frac{1}{B - A}⌋ + 1} < B - A$
91	79 17 2 90	ltsub2dd	$⊢ φ \to B - (B - A) < B - (\frac{1}{⌊\frac{1}{B - A}⌋ + 1})$
92	2	recnd	$⊢ φ \to B \in ℂ$
93	1	recnd	$⊢ φ \to A \in ℂ$
94	92 93	nncand	$⊢ φ \to B - (B - A) = A$
95	78	oveq2i	$⊢ B - (\frac{1}{⌊\frac{1}{B - A}⌋ + 1}) = B - (\frac{1}{M})$
96	95	a1i	$⊢ φ \to B - (\frac{1}{⌊\frac{1}{B - A}⌋ + 1}) = B - (\frac{1}{M})$
97	91 94 96	3brtr3d	$⊢ φ \to A < B - (\frac{1}{M})$
98	97	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to A < B - (\frac{1}{M})$
99	67 72	elrpd	$⊢ φ \to M \in ℝ^{+}$
100	99	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to M \in ℝ^{+}$
101	41 62	elrpd	$⊢ (φ \land j \in ℤ_{\geq M}) \to j \in ℝ^{+}$
102		1red	$⊢ (φ \land j \in ℤ_{\geq M}) \to 1 \in ℝ$
103		0le1	$⊢ 0 \leq 1$
104	103	a1i	$⊢ (φ \land j \in ℤ_{\geq M}) \to 0 \leq 1$
105	100 101 102 104 60	lediv2ad	$⊢ (φ \land j \in ℤ_{\geq M}) \to \frac{1}{j} \leq \frac{1}{M}$
106	64 75 39 105	lesub2dd	$⊢ (φ \land j \in ℤ_{\geq M}) \to B - (\frac{1}{M}) \leq B - (\frac{1}{j})$
107	66 76 65 98 106	ltletrd	$⊢ (φ \land j \in ℤ_{\geq M}) \to A < B - (\frac{1}{j})$
108	101	rpreccld	$⊢ (φ \land j \in ℤ_{\geq M}) \to \frac{1}{j} \in ℝ^{+}$
109	39 108	ltsubrpd	$⊢ (φ \land j \in ℤ_{\geq M}) \to B - (\frac{1}{j}) < B$
110	36 38 65 107 109	eliood	$⊢ (φ \land j \in ℤ_{\geq M}) \to B - (\frac{1}{j}) \in (A, B)$
111	34 110	ffvelcdmd	$⊢ (φ \land j \in ℤ_{\geq M}) \to F (B - (\frac{1}{j})) \in ℝ$
112	111 9	fmptd	$⊢ φ \to S : ℤ_{\geq M} ⟶ ℝ$
113	1 2 3 4 5 6	dvbdfbdioo	$⊢ φ \to \exists b \in ℝ \forall x \in (A, B) \|F (x)\| \leq b$
114	67	adantr	$⊢ (φ \land \forall x \in (A, B) \|F (x)\| \leq b) \to M \in ℝ$
115		simpr	$⊢ (φ \land j \in ℤ_{\geq M}) \to j \in ℤ_{\geq M}$
116	9	fvmpt2	$⊢ (j \in ℤ_{\geq M} \land F (B - (\frac{1}{j})) \in ℝ) \to S (j) = F (B - (\frac{1}{j}))$
117	115 111 116	syl2anc	$⊢ (φ \land j \in ℤ_{\geq M}) \to S (j) = F (B - (\frac{1}{j}))$
118	117	fveq2d	$⊢ (φ \land j \in ℤ_{\geq M}) \to \|S (j)\| = \|F (B - (\frac{1}{j}))\|$
119	118	adantlr	$⊢ ((φ \land \forall x \in (A, B) \|F (x)\| \leq b) \land j \in ℤ_{\geq M}) \to \|S (j)\| = \|F (B - (\frac{1}{j}))\|$
120		simplr	$⊢ ((φ \land \forall x \in (A, B) \|F (x)\| \leq b) \land j \in ℤ_{\geq M}) \to \forall x \in (A, B) \|F (x)\| \leq b$
121	110	adantlr	$⊢ ((φ \land \forall x \in (A, B) \|F (x)\| \leq b) \land j \in ℤ_{\geq M}) \to B - (\frac{1}{j}) \in (A, B)$
122		2fveq3	$⊢ x = B - (\frac{1}{j}) \to \|F (x)\| = \|F (B - (\frac{1}{j}))\|$
123	122	breq1d	$⊢ x = B - (\frac{1}{j}) \to (\|F (x)\| \leq b \leftrightarrow \|F (B - (\frac{1}{j}))\| \leq b)$
124	123	rspccva	$⊢ (\forall x \in (A, B) \|F (x)\| \leq b \land B - (\frac{1}{j}) \in (A, B)) \to \|F (B - (\frac{1}{j}))\| \leq b$
125	120 121 124	syl2anc	$⊢ ((φ \land \forall x \in (A, B) \|F (x)\| \leq b) \land j \in ℤ_{\geq M}) \to \|F (B - (\frac{1}{j}))\| \leq b$
126	119 125	eqbrtrd	$⊢ ((φ \land \forall x \in (A, B) \|F (x)\| \leq b) \land j \in ℤ_{\geq M}) \to \|S (j)\| \leq b$
127	126	a1d	$⊢ ((φ \land \forall x \in (A, B) \|F (x)\| \leq b) \land j \in ℤ_{\geq M}) \to (M \leq j \to \|S (j)\| \leq b)$
128	127	ralrimiva	$⊢ (φ \land \forall x \in (A, B) \|F (x)\| \leq b) \to \forall j \in ℤ_{\geq M} (M \leq j \to \|S (j)\| \leq b)$
129		breq1	$⊢ k = M \to (k \leq j \leftrightarrow M \leq j)$
130	129	imbi1d	$⊢ k = M \to ((k \leq j \to \|S (j)\| \leq b) \leftrightarrow (M \leq j \to \|S (j)\| \leq b))$
131	130	ralbidv	$⊢ k = M \to (\forall j \in ℤ_{\geq M} (k \leq j \to \|S (j)\| \leq b) \leftrightarrow \forall j \in ℤ_{\geq M} (M \leq j \to \|S (j)\| \leq b))$
132	131	rspcev	$⊢ (M \in ℝ \land \forall j \in ℤ_{\geq M} (M \leq j \to \|S (j)\| \leq b)) \to \exists k \in ℝ \forall j \in ℤ_{\geq M} (k \leq j \to \|S (j)\| \leq b)$
133	114 128 132	syl2anc	$⊢ (φ \land \forall x \in (A, B) \|F (x)\| \leq b) \to \exists k \in ℝ \forall j \in ℤ_{\geq M} (k \leq j \to \|S (j)\| \leq b)$
134	133	ex	$⊢ φ \to (\forall x \in (A, B) \|F (x)\| \leq b \to \exists k \in ℝ \forall j \in ℤ_{\geq M} (k \leq j \to \|S (j)\| \leq b))$
135	134	reximdv	$⊢ φ \to (\exists b \in ℝ \forall x \in (A, B) \|F (x)\| \leq b \to \exists b \in ℝ \exists k \in ℝ \forall j \in ℤ_{\geq M} (k \leq j \to \|S (j)\| \leq b))$
136	113 135	mpd	$⊢ φ \to \exists b \in ℝ \exists k \in ℝ \forall j \in ℤ_{\geq M} (k \leq j \to \|S (j)\| \leq b)$
137	16 33 112 136	limsupre	$⊢ φ \to lim sup (S) \in ℝ$
138	137	recnd	$⊢ φ \to lim sup (S) \in ℂ$
139		eluzelre	$⊢ j \in ℤ_{\geq N} \to j \in ℝ$
140	139	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to j \in ℝ$
141		0red	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to 0 \in ℝ$
142	52	peano2zd	$⊢ φ \to ⌊\frac{1}{B - A}⌋ + 1 \in ℤ$
143	8 142	eqeltrid	$⊢ φ \to M \in ℤ$
144	143	adantr	$⊢ (φ \land x \in ℝ^{+}) \to M \in ℤ$
145	144	zred	$⊢ (φ \land x \in ℝ^{+}) \to M \in ℝ$
146	145	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to M \in ℝ$
147	72	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to 0 < M$
148		ioomidp	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to \frac{A + B}{2} \in (A, B)$
149	1 2 3 148	syl3anc	$⊢ φ \to \frac{A + B}{2} \in (A, B)$
150		ne0i	$⊢ \frac{A + B}{2} \in (A, B) \to (A, B) \neq \emptyset$
151	149 150	syl	$⊢ φ \to (A, B) \neq \emptyset$
152		ioossre	$⊢ (A, B) \subseteq ℝ$
153	152	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
154		dvfre	$⊢ (F : (A, B) ⟶ ℝ \land (A, B) \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
155	4 153 154	syl2anc	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
156	5	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℝ)$
157	155 156	mpbid	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℝ$
158	157	ffvelcdmda	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℝ$
159	158	recnd	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℂ$
160	159	abscld	$⊢ (φ \land x \in (A, B)) \to \|F_{ℝ}^{'} (x)\| \in ℝ$
161		eqid	$⊢ (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) = (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|)$
162		eqid	$⊢ sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <) = sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
163	151 160 6 161 162	suprnmpt	$⊢ φ \to (sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <) \in ℝ \land \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <))$
164	163	simpld	$⊢ φ \to sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <) \in ℝ$
165	7 164	eqeltrid	$⊢ φ \to Y \in ℝ$
166	165	adantr	$⊢ (φ \land x \in ℝ^{+}) \to Y \in ℝ$
167		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
168	167	rehalfcld	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ$
169	168	adantl	$⊢ (φ \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ$
170	167	recnd	$⊢ x \in ℝ^{+} \to x \in ℂ$
171	170	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℂ$
172		2cnd	$⊢ (φ \land x \in ℝ^{+}) \to 2 \in ℂ$
173		rpne0	$⊢ x \in ℝ^{+} \to x \neq 0$
174	173	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \neq 0$
175		2ne0	$⊢ 2 \neq 0$
176	175	a1i	$⊢ (φ \land x \in ℝ^{+}) \to 2 \neq 0$
177	171 172 174 176	divne0d	$⊢ (φ \land x \in ℝ^{+}) \to \frac{x}{2} \neq 0$
178	166 169 177	redivcld	$⊢ (φ \land x \in ℝ^{+}) \to \frac{Y}{\frac{x}{2}} \in ℝ$
179	178	flcld	$⊢ (φ \land x \in ℝ^{+}) \to ⌊\frac{Y}{\frac{x}{2}}⌋ \in ℤ$
180	179	peano2zd	$⊢ (φ \land x \in ℝ^{+}) \to ⌊\frac{Y}{\frac{x}{2}}⌋ + 1 \in ℤ$
181	180 144	ifcld	$⊢ (φ \land x \in ℝ^{+}) \to if (M \leq ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, M) \in ℤ$
182	11 181	eqeltrid	$⊢ (φ \land x \in ℝ^{+}) \to N \in ℤ$
183	182	zred	$⊢ (φ \land x \in ℝ^{+}) \to N \in ℝ$
184	183	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to N \in ℝ$
185	180	zred	$⊢ (φ \land x \in ℝ^{+}) \to ⌊\frac{Y}{\frac{x}{2}}⌋ + 1 \in ℝ$
186		max1	$⊢ (M \in ℝ \land ⌊\frac{Y}{\frac{x}{2}}⌋ + 1 \in ℝ) \to M \leq if (M \leq ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, M)$
187	145 185 186	syl2anc	$⊢ (φ \land x \in ℝ^{+}) \to M \leq if (M \leq ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, M)$
188	187 11	breqtrrdi	$⊢ (φ \land x \in ℝ^{+}) \to M \leq N$
189	188	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to M \leq N$
190		eluzle	$⊢ j \in ℤ_{\geq N} \to N \leq j$
191	190	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to N \leq j$
192	146 184 140 189 191	letrd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to M \leq j$
193	141 146 140 147 192	ltletrd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to 0 < j$
194	193	gt0ne0d	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to j \neq 0$
195	140 194	rereccld	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to \frac{1}{j} \in ℝ$
196	140 193	recgt0d	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to 0 < \frac{1}{j}$
197	195 196	elrpd	$⊢ ((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \to \frac{1}{j} \in ℝ^{+}$
198	197	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \to \frac{1}{j} \in ℝ^{+}$
199	12	biimpi	$⊢ χ \to (((((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \land z \in (A, B)) \land \|z - B\| < \frac{1}{j})$
200		simp-5l	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \land z \in (A, B)) \land \|z - B\| < \frac{1}{j}) \to φ$
201	199 200	syl	$⊢ χ \to φ$
202	201 4	syl	$⊢ χ \to F : (A, B) ⟶ ℝ$
203	199	simplrd	$⊢ χ \to z \in (A, B)$
204	202 203	ffvelcdmd	$⊢ χ \to F (z) \in ℝ$
205	204	recnd	$⊢ χ \to F (z) \in ℂ$
206	201 112	syl	$⊢ χ \to S : ℤ_{\geq M} ⟶ ℝ$
207		simp-5r	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \land z \in (A, B)) \land \|z - B\| < \frac{1}{j}) \to x \in ℝ^{+}$
208	199 207	syl	$⊢ χ \to x \in ℝ^{+}$
209		eluz2	$⊢ N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N)$
210	144 182 188 209	syl3anbrc	$⊢ (φ \land x \in ℝ^{+}) \to N \in ℤ_{\geq M}$
211	201 208 210	syl2anc	$⊢ χ \to N \in ℤ_{\geq M}$
212		uzss	$⊢ N \in ℤ_{\geq M} \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
213	211 212	syl	$⊢ χ \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
214		simp-4r	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \land z \in (A, B)) \land \|z - B\| < \frac{1}{j}) \to j \in ℤ_{\geq N}$
215	199 214	syl	$⊢ χ \to j \in ℤ_{\geq N}$
216	213 215	sseldd	$⊢ χ \to j \in ℤ_{\geq M}$
217	206 216	ffvelcdmd	$⊢ χ \to S (j) \in ℝ$
218	217	recnd	$⊢ χ \to S (j) \in ℂ$
219	201 138	syl	$⊢ χ \to lim sup (S) \in ℂ$
220	205 218 219	npncand	$⊢ χ \to (F (z) - S (j)) + S (j) - lim sup (S) = F (z) - lim sup (S)$
221	220	eqcomd	$⊢ χ \to F (z) - lim sup (S) = (F (z) - S (j)) + S (j) - lim sup (S)$
222	221	fveq2d	$⊢ χ \to \|F (z) - lim sup (S)\| = \|(F (z) - S (j)) + S (j) - lim sup (S)\|$
223	204 217	resubcld	$⊢ χ \to F (z) - S (j) \in ℝ$
224	201 137	syl	$⊢ χ \to lim sup (S) \in ℝ$
225	217 224	resubcld	$⊢ χ \to S (j) - lim sup (S) \in ℝ$
226	223 225	readdcld	$⊢ χ \to (F (z) - S (j)) + S (j) - lim sup (S) \in ℝ$
227	226	recnd	$⊢ χ \to (F (z) - S (j)) + S (j) - lim sup (S) \in ℂ$
228	227	abscld	$⊢ χ \to \|(F (z) - S (j)) + S (j) - lim sup (S)\| \in ℝ$
229	223	recnd	$⊢ χ \to F (z) - S (j) \in ℂ$
230	229	abscld	$⊢ χ \to \|F (z) - S (j)\| \in ℝ$
231	225	recnd	$⊢ χ \to S (j) - lim sup (S) \in ℂ$
232	231	abscld	$⊢ χ \to \|S (j) - lim sup (S)\| \in ℝ$
233	230 232	readdcld	$⊢ χ \to \|F (z) - S (j)\| + \|S (j) - lim sup (S)\| \in ℝ$
234	208	rpred	$⊢ χ \to x \in ℝ$
235	229 231	abstrid	$⊢ χ \to \|(F (z) - S (j)) + S (j) - lim sup (S)\| \leq \|F (z) - S (j)\| + \|S (j) - lim sup (S)\|$
236	234	rehalfcld	$⊢ χ \to \frac{x}{2} \in ℝ$
237	201 216 117	syl2anc	$⊢ χ \to S (j) = F (B - (\frac{1}{j}))$
238	237	oveq2d	$⊢ χ \to F (z) - S (j) = F (z) - F (B - (\frac{1}{j}))$
239	238	fveq2d	$⊢ χ \to \|F (z) - S (j)\| = \|F (z) - F (B - (\frac{1}{j}))\|$
240	239 230	eqeltrrd	$⊢ χ \to \|F (z) - F (B - (\frac{1}{j}))\| \in ℝ$
241	201 165	syl	$⊢ χ \to Y \in ℝ$
242	152 203	sselid	$⊢ χ \to z \in ℝ$
243	201 216 65	syl2anc	$⊢ χ \to B - (\frac{1}{j}) \in ℝ$
244	242 243	resubcld	$⊢ χ \to z - (B - (\frac{1}{j})) \in ℝ$
245	241 244	remulcld	$⊢ χ \to Y (z - (B - (\frac{1}{j}))) \in ℝ$
246	201 1	syl	$⊢ χ \to A \in ℝ$
247	201 2	syl	$⊢ χ \to B \in ℝ$
248	201 5	syl	$⊢ χ \to dom F_{ℝ}^{'} = (A, B)$
249	163	simprd	$⊢ φ \to \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
250	7	breq2i	$⊢ \|F_{ℝ}^{'} (x)\| \leq Y \leftrightarrow \|F_{ℝ}^{'} (x)\| \leq sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
251	250	ralbii	$⊢ \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq Y \leftrightarrow \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
252	249 251	sylibr	$⊢ φ \to \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq Y$
253	201 252	syl	$⊢ χ \to \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq Y$
254		2fveq3	$⊢ w = x \to \|F_{ℝ}^{'} (w)\| = \|F_{ℝ}^{'} (x)\|$
255	254	breq1d	$⊢ w = x \to (\|F_{ℝ}^{'} (w)\| \leq Y \leftrightarrow \|F_{ℝ}^{'} (x)\| \leq Y)$
256	255	cbvralvw	$⊢ \forall w \in (A, B) \|F_{ℝ}^{'} (w)\| \leq Y \leftrightarrow \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq Y$
257	253 256	sylibr	$⊢ χ \to \forall w \in (A, B) \|F_{ℝ}^{'} (w)\| \leq Y$
258	201 216 110	syl2anc	$⊢ χ \to B - (\frac{1}{j}) \in (A, B)$
259	243	rexrd	$⊢ χ \to B - (\frac{1}{j}) \in ℝ^{*}$
260	201 37	syl	$⊢ χ \to B \in ℝ^{*}$
261	15 216	sselid	$⊢ χ \to j \in ℝ$
262	201 216 63	syl2anc	$⊢ χ \to j \neq 0$
263	261 262	rereccld	$⊢ χ \to \frac{1}{j} \in ℝ$
264	247 242	resubcld	$⊢ χ \to B - z \in ℝ$
265	242 247	resubcld	$⊢ χ \to z - B \in ℝ$
266	265	recnd	$⊢ χ \to z - B \in ℂ$
267	266	abscld	$⊢ χ \to \|z - B\| \in ℝ$
268	264	leabsd	$⊢ χ \to B - z \leq \|B - z\|$
269	201 92	syl	$⊢ χ \to B \in ℂ$
270	242	recnd	$⊢ χ \to z \in ℂ$
271	269 270	abssubd	$⊢ χ \to \|B - z\| = \|z - B\|$
272	268 271	breqtrd	$⊢ χ \to B - z \leq \|z - B\|$
273	199	simprd	$⊢ χ \to \|z - B\| < \frac{1}{j}$
274	264 267 263 272 273	lelttrd	$⊢ χ \to B - z < \frac{1}{j}$
275	247 242 263 274	ltsub23d	$⊢ χ \to B - (\frac{1}{j}) < z$
276	201 35	syl	$⊢ χ \to A \in ℝ^{*}$
277		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land z \in (A, B)) \to z < B$
278	276 260 203 277	syl3anc	$⊢ χ \to z < B$
279	259 260 242 275 278	eliood	$⊢ χ \to z \in (B - (\frac{1}{j}), B)$
280	246 247 202 248 241 257 258 279	dvbdfbdioolem1	$⊢ χ \to (\|F (z) - F (B - (\frac{1}{j}))\| \leq Y (z - (B - (\frac{1}{j}))) \land \|F (z) - F (B - (\frac{1}{j}))\| \leq Y (B - A))$
281	280	simpld	$⊢ χ \to \|F (z) - F (B - (\frac{1}{j}))\| \leq Y (z - (B - (\frac{1}{j})))$
282	201 216 64	syl2anc	$⊢ χ \to \frac{1}{j} \in ℝ$
283	241 282	remulcld	$⊢ χ \to Y (\frac{1}{j}) \in ℝ$
284	157 149	ffvelcdmd	$⊢ φ \to F_{ℝ}^{'} (\frac{A + B}{2}) \in ℝ$
285	284	recnd	$⊢ φ \to F_{ℝ}^{'} (\frac{A + B}{2}) \in ℂ$
286	285	abscld	$⊢ φ \to \|F_{ℝ}^{'} (\frac{A + B}{2})\| \in ℝ$
287	285	absge0d	$⊢ φ \to 0 \leq \|F_{ℝ}^{'} (\frac{A + B}{2})\|$
288		2fveq3	$⊢ x = \frac{A + B}{2} \to \|F_{ℝ}^{'} (x)\| = \|F_{ℝ}^{'} (\frac{A + B}{2})\|$
289	7	eqcomi	$⊢ sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <) = Y$
290	289	a1i	$⊢ x = \frac{A + B}{2} \to sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <) = Y$
291	288 290	breq12d	$⊢ x = \frac{A + B}{2} \to (\|F_{ℝ}^{'} (x)\| \leq sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <) \leftrightarrow \|F_{ℝ}^{'} (\frac{A + B}{2})\| \leq Y)$
292	291	rspcva	$⊢ (\frac{A + B}{2} \in (A, B) \land \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)) \to \|F_{ℝ}^{'} (\frac{A + B}{2})\| \leq Y$
293	149 249 292	syl2anc	$⊢ φ \to \|F_{ℝ}^{'} (\frac{A + B}{2})\| \leq Y$
294	22 286 165 287 293	letrd	$⊢ φ \to 0 \leq Y$
295	201 294	syl	$⊢ χ \to 0 \leq Y$
296	282	recnd	$⊢ χ \to \frac{1}{j} \in ℂ$
297		sub31	$⊢ (z \in ℂ \land B \in ℂ \land \frac{1}{j} \in ℂ) \to z - (B - (\frac{1}{j})) = (\frac{1}{j}) - (B - z)$
298	270 269 296 297	syl3anc	$⊢ χ \to z - (B - (\frac{1}{j})) = (\frac{1}{j}) - (B - z)$
299	242 247	posdifd	$⊢ χ \to (z < B \leftrightarrow 0 < B - z)$
300	278 299	mpbid	$⊢ χ \to 0 < B - z$
301	264 300	elrpd	$⊢ χ \to B - z \in ℝ^{+}$
302	282 301	ltsubrpd	$⊢ χ \to (\frac{1}{j}) - (B - z) < \frac{1}{j}$
303	298 302	eqbrtrd	$⊢ χ \to z - (B - (\frac{1}{j})) < \frac{1}{j}$
304	244 282 303	ltled	$⊢ χ \to z - (B - (\frac{1}{j})) \leq \frac{1}{j}$
305	244 282 241 295 304	lemul2ad	$⊢ χ \to Y (z - (B - (\frac{1}{j}))) \leq Y (\frac{1}{j})$
306	283	adantr	$⊢ (χ \land Y = 0) \to Y (\frac{1}{j}) \in ℝ$
307	236	adantr	$⊢ (χ \land Y = 0) \to \frac{x}{2} \in ℝ$
308		oveq1	$⊢ Y = 0 \to Y (\frac{1}{j}) = 0 \cdot (\frac{1}{j})$
309	296	mul02d	$⊢ χ \to 0 \cdot (\frac{1}{j}) = 0$
310	308 309	sylan9eqr	$⊢ (χ \land Y = 0) \to Y (\frac{1}{j}) = 0$
311	208	rphalfcld	$⊢ χ \to \frac{x}{2} \in ℝ^{+}$
312	311	rpgt0d	$⊢ χ \to 0 < \frac{x}{2}$
313	312	adantr	$⊢ (χ \land Y = 0) \to 0 < \frac{x}{2}$
314	310 313	eqbrtrd	$⊢ (χ \land Y = 0) \to Y (\frac{1}{j}) < \frac{x}{2}$
315	306 307 314	ltled	$⊢ (χ \land Y = 0) \to Y (\frac{1}{j}) \leq \frac{x}{2}$
316	241	adantr	$⊢ (χ \land \neg Y = 0) \to Y \in ℝ$
317	295	adantr	$⊢ (χ \land \neg Y = 0) \to 0 \leq Y$
318		neqne	$⊢ \neg Y = 0 \to Y \neq 0$
319	318	adantl	$⊢ (χ \land \neg Y = 0) \to Y \neq 0$
320	316 317 319	ne0gt0d	$⊢ (χ \land \neg Y = 0) \to 0 < Y$
321	283	adantr	$⊢ (χ \land 0 < Y) \to Y (\frac{1}{j}) \in ℝ$
322	15 211	sselid	$⊢ χ \to N \in ℝ$
323		0red	$⊢ χ \to 0 \in ℝ$
324	201 208 145	syl2anc	$⊢ χ \to M \in ℝ$
325	201 72	syl	$⊢ χ \to 0 < M$
326	201 208 188	syl2anc	$⊢ χ \to M \leq N$
327	323 324 322 325 326	ltletrd	$⊢ χ \to 0 < N$
328	327	gt0ne0d	$⊢ χ \to N \neq 0$
329	322 328	rereccld	$⊢ χ \to \frac{1}{N} \in ℝ$
330	241 329	remulcld	$⊢ χ \to Y (\frac{1}{N}) \in ℝ$
331	330	adantr	$⊢ (χ \land 0 < Y) \to Y (\frac{1}{N}) \in ℝ$
332	236	adantr	$⊢ (χ \land 0 < Y) \to \frac{x}{2} \in ℝ$
333	282	adantr	$⊢ (χ \land 0 < Y) \to \frac{1}{j} \in ℝ$
334	329	adantr	$⊢ (χ \land 0 < Y) \to \frac{1}{N} \in ℝ$
335	241	adantr	$⊢ (χ \land 0 < Y) \to Y \in ℝ$
336	295	adantr	$⊢ (χ \land 0 < Y) \to 0 \leq Y$
337	322 327	elrpd	$⊢ χ \to N \in ℝ^{+}$
338	201 216 101	syl2anc	$⊢ χ \to j \in ℝ^{+}$
339		1red	$⊢ χ \to 1 \in ℝ$
340	103	a1i	$⊢ χ \to 0 \leq 1$
341	215 190	syl	$⊢ χ \to N \leq j$
342	337 338 339 340 341	lediv2ad	$⊢ χ \to \frac{1}{j} \leq \frac{1}{N}$
343	342	adantr	$⊢ (χ \land 0 < Y) \to \frac{1}{j} \leq \frac{1}{N}$
344	333 334 335 336 343	lemul2ad	$⊢ (χ \land 0 < Y) \to Y (\frac{1}{j}) \leq Y (\frac{1}{N})$
345	234	recnd	$⊢ χ \to x \in ℂ$
346		2cnd	$⊢ χ \to 2 \in ℂ$
347	208	rpne0d	$⊢ χ \to x \neq 0$
348	175	a1i	$⊢ χ \to 2 \neq 0$
349	345 346 347 348	divne0d	$⊢ χ \to \frac{x}{2} \neq 0$
350	241 236 349	redivcld	$⊢ χ \to \frac{Y}{\frac{x}{2}} \in ℝ$
351	350	adantr	$⊢ (χ \land 0 < Y) \to \frac{Y}{\frac{x}{2}} \in ℝ$
352		simpr	$⊢ (χ \land 0 < Y) \to 0 < Y$
353	312	adantr	$⊢ (χ \land 0 < Y) \to 0 < \frac{x}{2}$
354	335 332 352 353	divgt0d	$⊢ (χ \land 0 < Y) \to 0 < \frac{Y}{\frac{x}{2}}$
355	351 354	elrpd	$⊢ (χ \land 0 < Y) \to \frac{Y}{\frac{x}{2}} \in ℝ^{+}$
356	355	rprecred	$⊢ (χ \land 0 < Y) \to \frac{1}{\frac{Y}{\frac{x}{2}}} \in ℝ$
357	337	adantr	$⊢ (χ \land 0 < Y) \to N \in ℝ^{+}$
358		1red	$⊢ (χ \land 0 < Y) \to 1 \in ℝ$
359	103	a1i	$⊢ (χ \land 0 < Y) \to 0 \leq 1$
360	350	flcld	$⊢ χ \to ⌊\frac{Y}{\frac{x}{2}}⌋ \in ℤ$
361	360	peano2zd	$⊢ χ \to ⌊\frac{Y}{\frac{x}{2}}⌋ + 1 \in ℤ$
362	361	zred	$⊢ χ \to ⌊\frac{Y}{\frac{x}{2}}⌋ + 1 \in ℝ$
363	201 143	syl	$⊢ χ \to M \in ℤ$
364	361 363	ifcld	$⊢ χ \to if (M \leq ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, M) \in ℤ$
365	11 364	eqeltrid	$⊢ χ \to N \in ℤ$
366	365	zred	$⊢ χ \to N \in ℝ$
367		flltp1	$⊢ \frac{Y}{\frac{x}{2}} \in ℝ \to \frac{Y}{\frac{x}{2}} < ⌊\frac{Y}{\frac{x}{2}}⌋ + 1$
368	350 367	syl	$⊢ χ \to \frac{Y}{\frac{x}{2}} < ⌊\frac{Y}{\frac{x}{2}}⌋ + 1$
369	201 67	syl	$⊢ χ \to M \in ℝ$
370		max2	$⊢ (M \in ℝ \land ⌊\frac{Y}{\frac{x}{2}}⌋ + 1 \in ℝ) \to ⌊\frac{Y}{\frac{x}{2}}⌋ + 1 \leq if (M \leq ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, M)$
371	369 362 370	syl2anc	$⊢ χ \to ⌊\frac{Y}{\frac{x}{2}}⌋ + 1 \leq if (M \leq ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, M)$
372	371 11	breqtrrdi	$⊢ χ \to ⌊\frac{Y}{\frac{x}{2}}⌋ + 1 \leq N$
373	350 362 366 368 372	ltletrd	$⊢ χ \to \frac{Y}{\frac{x}{2}} < N$
374	350 322 373	ltled	$⊢ χ \to \frac{Y}{\frac{x}{2}} \leq N$
375	374	adantr	$⊢ (χ \land 0 < Y) \to \frac{Y}{\frac{x}{2}} \leq N$
376	355 357 358 359 375	lediv2ad	$⊢ (χ \land 0 < Y) \to \frac{1}{N} \leq \frac{1}{\frac{Y}{\frac{x}{2}}}$
377	334 356 335 336 376	lemul2ad	$⊢ (χ \land 0 < Y) \to Y (\frac{1}{N}) \leq Y (\frac{1}{\frac{Y}{\frac{x}{2}}})$
378	335	recnd	$⊢ (χ \land 0 < Y) \to Y \in ℂ$
379	351	recnd	$⊢ (χ \land 0 < Y) \to \frac{Y}{\frac{x}{2}} \in ℂ$
380	354	gt0ne0d	$⊢ (χ \land 0 < Y) \to \frac{Y}{\frac{x}{2}} \neq 0$
381	378 379 380	divrecd	$⊢ (χ \land 0 < Y) \to \frac{Y}{\frac{Y}{\frac{x}{2}}} = Y (\frac{1}{\frac{Y}{\frac{x}{2}}})$
382	332	recnd	$⊢ (χ \land 0 < Y) \to \frac{x}{2} \in ℂ$
383	352	gt0ne0d	$⊢ (χ \land 0 < Y) \to Y \neq 0$
384	349	adantr	$⊢ (χ \land 0 < Y) \to \frac{x}{2} \neq 0$
385	378 382 383 384	ddcand	$⊢ (χ \land 0 < Y) \to \frac{Y}{\frac{Y}{\frac{x}{2}}} = \frac{x}{2}$
386	381 385	eqtr3d	$⊢ (χ \land 0 < Y) \to Y (\frac{1}{\frac{Y}{\frac{x}{2}}}) = \frac{x}{2}$
387	377 386	breqtrd	$⊢ (χ \land 0 < Y) \to Y (\frac{1}{N}) \leq \frac{x}{2}$
388	321 331 332 344 387	letrd	$⊢ (χ \land 0 < Y) \to Y (\frac{1}{j}) \leq \frac{x}{2}$
389	320 388	syldan	$⊢ (χ \land \neg Y = 0) \to Y (\frac{1}{j}) \leq \frac{x}{2}$
390	315 389	pm2.61dan	$⊢ χ \to Y (\frac{1}{j}) \leq \frac{x}{2}$
391	245 283 236 305 390	letrd	$⊢ χ \to Y (z - (B - (\frac{1}{j}))) \leq \frac{x}{2}$
392	240 245 236 281 391	letrd	$⊢ χ \to \|F (z) - F (B - (\frac{1}{j}))\| \leq \frac{x}{2}$
393	239 392	eqbrtrd	$⊢ χ \to \|F (z) - S (j)\| \leq \frac{x}{2}$
394		simpllr	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \land z \in (A, B)) \land \|z - B\| < \frac{1}{j}) \to \|S (j) - lim sup (S)\| < \frac{x}{2}$
395	199 394	syl	$⊢ χ \to \|S (j) - lim sup (S)\| < \frac{x}{2}$
396	230 232 236 236 393 395	leltaddd	$⊢ χ \to \|F (z) - S (j)\| + \|S (j) - lim sup (S)\| < (\frac{x}{2}) + (\frac{x}{2})$
397	345	2halvesd	$⊢ χ \to (\frac{x}{2}) + (\frac{x}{2}) = x$
398	396 397	breqtrd	$⊢ χ \to \|F (z) - S (j)\| + \|S (j) - lim sup (S)\| < x$
399	228 233 234 235 398	lelttrd	$⊢ χ \to \|(F (z) - S (j)) + S (j) - lim sup (S)\| < x$
400	222 399	eqbrtrd	$⊢ χ \to \|F (z) - lim sup (S)\| < x$
401	12 400	sylbir	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \land z \in (A, B)) \land \|z - B\| < \frac{1}{j}) \to \|F (z) - lim sup (S)\| < x$
402	401	adantrl	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \land z \in (A, B)) \land (z \neq B \land \|z - B\| < \frac{1}{j})) \to \|F (z) - lim sup (S)\| < x$
403	402	ex	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \land z \in (A, B)) \to ((z \neq B \land \|z - B\| < \frac{1}{j}) \to \|F (z) - lim sup (S)\| < x)$
404	403	ralrimiva	$⊢ (((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \to \forall z \in (A, B) ((z \neq B \land \|z - B\| < \frac{1}{j}) \to \|F (z) - lim sup (S)\| < x)$
405		brimralrspcev	$⊢ (\frac{1}{j} \in ℝ^{+} \land \forall z \in (A, B) ((z \neq B \land \|z - B\| < \frac{1}{j}) \to \|F (z) - lim sup (S)\| < x)) \to \exists y \in ℝ^{+} \forall z \in (A, B) ((z \neq B \land \|z - B\| < y) \to \|F (z) - lim sup (S)\| < x)$
406	198 404 405	syl2anc	$⊢ (((φ \land x \in ℝ^{+}) \land j \in ℤ_{\geq N}) \land \|S (j) - lim sup (S)\| < \frac{x}{2}) \to \exists y \in ℝ^{+} \forall z \in (A, B) ((z \neq B \land \|z - B\| < y) \to \|F (z) - lim sup (S)\| < x)$
407		simpr	$⊢ ((φ \land x \in ℝ^{+}) \land b \leq N) \to b \leq N$
408	407	iftrued	$⊢ ((φ \land x \in ℝ^{+}) \land b \leq N) \to if (b \leq N, N, b) = N$
409		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
410	182 409	syl	$⊢ (φ \land x \in ℝ^{+}) \to N \in ℤ_{\geq N}$
411	410	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land b \leq N) \to N \in ℤ_{\geq N}$
412	408 411	eqeltrd	$⊢ ((φ \land x \in ℝ^{+}) \land b \leq N) \to if (b \leq N, N, b) \in ℤ_{\geq N}$
413	412	adantlr	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land b \leq N) \to if (b \leq N, N, b) \in ℤ_{\geq N}$
414		iffalse	$⊢ \neg b \leq N \to if (b \leq N, N, b) = b$
415	414	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to if (b \leq N, N, b) = b$
416	182	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to N \in ℤ$
417		simplr	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to b \in ℤ$
418	416	zred	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to N \in ℝ$
419	417	zred	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to b \in ℝ$
420		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to \neg b \leq N$
421	418 419	ltnled	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to (N < b \leftrightarrow \neg b \leq N)$
422	420 421	mpbird	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to N < b$
423	418 419 422	ltled	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to N \leq b$
424		eluz2	$⊢ b \in ℤ_{\geq N} \leftrightarrow (N \in ℤ \land b \in ℤ \land N \leq b)$
425	416 417 423 424	syl3anbrc	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to b \in ℤ_{\geq N}$
426	415 425	eqeltrd	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \neg b \leq N) \to if (b \leq N, N, b) \in ℤ_{\geq N}$
427	413 426	pm2.61dan	$⊢ ((φ \land x \in ℝ^{+}) \land b \in ℤ) \to if (b \leq N, N, b) \in ℤ_{\geq N}$
428	427	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2})) \to if (b \leq N, N, b) \in ℤ_{\geq N}$
429		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2})) \to \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2})$
430		simpr	$⊢ ((φ \land x \in ℝ^{+}) \land b \in ℤ) \to b \in ℤ$
431	182	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land b \in ℤ) \to N \in ℤ$
432	431 430	ifcld	$⊢ ((φ \land x \in ℝ^{+}) \land b \in ℤ) \to if (b \leq N, N, b) \in ℤ$
433	430	zred	$⊢ ((φ \land x \in ℝ^{+}) \land b \in ℤ) \to b \in ℝ$
434	431	zred	$⊢ ((φ \land x \in ℝ^{+}) \land b \in ℤ) \to N \in ℝ$
435		max1	$⊢ (b \in ℝ \land N \in ℝ) \to b \leq if (b \leq N, N, b)$
436	433 434 435	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land b \in ℤ) \to b \leq if (b \leq N, N, b)$
437		eluz2	$⊢ if (b \leq N, N, b) \in ℤ_{\geq b} \leftrightarrow (b \in ℤ \land if (b \leq N, N, b) \in ℤ \land b \leq if (b \leq N, N, b))$
438	430 432 436 437	syl3anbrc	$⊢ ((φ \land x \in ℝ^{+}) \land b \in ℤ) \to if (b \leq N, N, b) \in ℤ_{\geq b}$
439	438	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2})) \to if (b \leq N, N, b) \in ℤ_{\geq b}$
440		fveq2	$⊢ c = if (b \leq N, N, b) \to S (c) = S (if (b \leq N, N, b))$
441	440	eleq1d	$⊢ c = if (b \leq N, N, b) \to (S (c) \in ℂ \leftrightarrow S (if (b \leq N, N, b)) \in ℂ)$
442	440	fvoveq1d	$⊢ c = if (b \leq N, N, b) \to \|S (c) - lim sup (S)\| = \|S (if (b \leq N, N, b)) - lim sup (S)\|$
443	442	breq1d	$⊢ c = if (b \leq N, N, b) \to (\|S (c) - lim sup (S)\| < \frac{x}{2} \leftrightarrow \|S (if (b \leq N, N, b)) - lim sup (S)\| < \frac{x}{2})$
444	441 443	anbi12d	$⊢ c = if (b \leq N, N, b) \to ((S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2}) \leftrightarrow (S (if (b \leq N, N, b)) \in ℂ \land \|S (if (b \leq N, N, b)) - lim sup (S)\| < \frac{x}{2}))$
445	444	rspccva	$⊢ (\forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2}) \land if (b \leq N, N, b) \in ℤ_{\geq b}) \to (S (if (b \leq N, N, b)) \in ℂ \land \|S (if (b \leq N, N, b)) - lim sup (S)\| < \frac{x}{2})$
446	429 439 445	syl2anc	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2})) \to (S (if (b \leq N, N, b)) \in ℂ \land \|S (if (b \leq N, N, b)) - lim sup (S)\| < \frac{x}{2})$
447	446	simprd	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2})) \to \|S (if (b \leq N, N, b)) - lim sup (S)\| < \frac{x}{2}$
448		fveq2	$⊢ j = if (b \leq N, N, b) \to S (j) = S (if (b \leq N, N, b))$
449	448	fvoveq1d	$⊢ j = if (b \leq N, N, b) \to \|S (j) - lim sup (S)\| = \|S (if (b \leq N, N, b)) - lim sup (S)\|$
450	449	breq1d	$⊢ j = if (b \leq N, N, b) \to (\|S (j) - lim sup (S)\| < \frac{x}{2} \leftrightarrow \|S (if (b \leq N, N, b)) - lim sup (S)\| < \frac{x}{2})$
451	450	rspcev	$⊢ (if (b \leq N, N, b) \in ℤ_{\geq N} \land \|S (if (b \leq N, N, b)) - lim sup (S)\| < \frac{x}{2}) \to \exists j \in ℤ_{\geq N} \|S (j) - lim sup (S)\| < \frac{x}{2}$
452	428 447 451	syl2anc	$⊢ (((φ \land x \in ℝ^{+}) \land b \in ℤ) \land \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2})) \to \exists j \in ℤ_{\geq N} \|S (j) - lim sup (S)\| < \frac{x}{2}$
453		ax-resscn	$⊢ ℝ \subseteq ℂ$
454	453	a1i	$⊢ φ \to ℝ \subseteq ℂ$
455	4 454	fssd	$⊢ φ \to F : (A, B) ⟶ ℂ$
456		dvcn	$⊢ ((ℝ \subseteq ℂ \land F : (A, B) ⟶ ℂ \land (A, B) \subseteq ℝ) \land dom F_{ℝ}^{'} = (A, B)) \to F : (A, B) \underset{cn}{⟶} ℂ$
457	454 455 153 5 456	syl31anc	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
458		cncfcdm	$⊢ (ℝ \subseteq ℂ \land F : (A, B) \underset{cn}{⟶} ℂ) \to (F : (A, B) \underset{cn}{⟶} ℝ \leftrightarrow F : (A, B) ⟶ ℝ)$
459	454 457 458	syl2anc	$⊢ φ \to (F : (A, B) \underset{cn}{⟶} ℝ \leftrightarrow F : (A, B) ⟶ ℝ)$
460	4 459	mpbird	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℝ$
461	110 10	fmptd	$⊢ φ \to R : ℤ_{\geq M} ⟶ (A, B)$
462		eqid	$⊢ (j \in ℤ_{\geq M} ⟼ F (R (j))) = (j \in ℤ_{\geq M} ⟼ F (R (j)))$
463		climrel	$⊢ Rel ⇝$
464	463	a1i	$⊢ φ \to Rel ⇝$
465		fvex	$⊢ ℤ_{\geq M} \in V$
466	465	mptex	$⊢ (j \in ℤ_{\geq M} ⟼ B) \in V$
467	466	a1i	$⊢ φ \to (j \in ℤ_{\geq M} ⟼ B) \in V$
468		eqidd	$⊢ (φ \land m \in ℤ_{\geq M}) \to (j \in ℤ_{\geq M} ⟼ B) = (j \in ℤ_{\geq M} ⟼ B)$
469		eqidd	$⊢ ((φ \land m \in ℤ_{\geq M}) \land j = m) \to B = B$
470		simpr	$⊢ (φ \land m \in ℤ_{\geq M}) \to m \in ℤ_{\geq M}$
471	2	adantr	$⊢ (φ \land m \in ℤ_{\geq M}) \to B \in ℝ$
472	468 469 470 471	fvmptd	$⊢ (φ \land m \in ℤ_{\geq M}) \to (j \in ℤ_{\geq M} ⟼ B) (m) = B$
473	31 30 467 92 472	climconst	$⊢ φ \to (j \in ℤ_{\geq M} ⟼ B) ⇝ B$
474	465	mptex	$⊢ (j \in ℤ_{\geq M} ⟼ B - (\frac{1}{j})) \in V$
475	10 474	eqeltri	$⊢ R \in V$
476	475	a1i	$⊢ φ \to R \in V$
477		1cnd	$⊢ φ \to 1 \in ℂ$
478		elnnnn0b	$⊢ M \in ℕ \leftrightarrow (M \in ℕ_{0} \land 0 < M)$
479	29 72 478	sylanbrc	$⊢ φ \to M \in ℕ$
480		divcnvg	$⊢ (1 \in ℂ \land M \in ℕ) \to (j \in ℤ_{\geq M} ⟼ \frac{1}{j}) ⇝ 0$
481	477 479 480	syl2anc	$⊢ φ \to (j \in ℤ_{\geq M} ⟼ \frac{1}{j}) ⇝ 0$
482		eqidd	$⊢ (φ \land i \in ℤ_{\geq M}) \to (j \in ℤ_{\geq M} ⟼ B) = (j \in ℤ_{\geq M} ⟼ B)$
483		eqidd	$⊢ ((φ \land i \in ℤ_{\geq M}) \land j = i) \to B = B$
484		simpr	$⊢ (φ \land i \in ℤ_{\geq M}) \to i \in ℤ_{\geq M}$
485	2	adantr	$⊢ (φ \land i \in ℤ_{\geq M}) \to B \in ℝ$
486	482 483 484 485	fvmptd	$⊢ (φ \land i \in ℤ_{\geq M}) \to (j \in ℤ_{\geq M} ⟼ B) (i) = B$
487	486 485	eqeltrd	$⊢ (φ \land i \in ℤ_{\geq M}) \to (j \in ℤ_{\geq M} ⟼ B) (i) \in ℝ$
488	487	recnd	$⊢ (φ \land i \in ℤ_{\geq M}) \to (j \in ℤ_{\geq M} ⟼ B) (i) \in ℂ$
489		eqidd	$⊢ (φ \land i \in ℤ_{\geq M}) \to (j \in ℤ_{\geq M} ⟼ \frac{1}{j}) = (j \in ℤ_{\geq M} ⟼ \frac{1}{j})$
490		oveq2	$⊢ j = i \to \frac{1}{j} = \frac{1}{i}$
491	490	adantl	$⊢ ((φ \land i \in ℤ_{\geq M}) \land j = i) \to \frac{1}{j} = \frac{1}{i}$
492	15 484	sselid	$⊢ (φ \land i \in ℤ_{\geq M}) \to i \in ℝ$
493		0red	$⊢ (φ \land i \in ℤ_{\geq M}) \to 0 \in ℝ$
494	67	adantr	$⊢ (φ \land i \in ℤ_{\geq M}) \to M \in ℝ$
495	72	adantr	$⊢ (φ \land i \in ℤ_{\geq M}) \to 0 < M$
496		eluzle	$⊢ i \in ℤ_{\geq M} \to M \leq i$
497	496	adantl	$⊢ (φ \land i \in ℤ_{\geq M}) \to M \leq i$
498	493 494 492 495 497	ltletrd	$⊢ (φ \land i \in ℤ_{\geq M}) \to 0 < i$
499	498	gt0ne0d	$⊢ (φ \land i \in ℤ_{\geq M}) \to i \neq 0$
500	492 499	rereccld	$⊢ (φ \land i \in ℤ_{\geq M}) \to \frac{1}{i} \in ℝ$
501	489 491 484 500	fvmptd	$⊢ (φ \land i \in ℤ_{\geq M}) \to (j \in ℤ_{\geq M} ⟼ \frac{1}{j}) (i) = \frac{1}{i}$
502	492	recnd	$⊢ (φ \land i \in ℤ_{\geq M}) \to i \in ℂ$
503	502 499	reccld	$⊢ (φ \land i \in ℤ_{\geq M}) \to \frac{1}{i} \in ℂ$
504	501 503	eqeltrd	$⊢ (φ \land i \in ℤ_{\geq M}) \to (j \in ℤ_{\geq M} ⟼ \frac{1}{j}) (i) \in ℂ$
505	490	oveq2d	$⊢ j = i \to B - (\frac{1}{j}) = B - (\frac{1}{i})$
506		ovex	$⊢ B - (\frac{1}{i}) \in V$
507	505 10 506	fvmpt	$⊢ i \in ℤ_{\geq M} \to R (i) = B - (\frac{1}{i})$
508	507	adantl	$⊢ (φ \land i \in ℤ_{\geq M}) \to R (i) = B - (\frac{1}{i})$
509	486 501	oveq12d	$⊢ (φ \land i \in ℤ_{\geq M}) \to (j \in ℤ_{\geq M} ⟼ B) (i) - (j \in ℤ_{\geq M} ⟼ \frac{1}{j}) (i) = B - (\frac{1}{i})$
510	508 509	eqtr4d	$⊢ (φ \land i \in ℤ_{\geq M}) \to R (i) = (j \in ℤ_{\geq M} ⟼ B) (i) - (j \in ℤ_{\geq M} ⟼ \frac{1}{j}) (i)$
511	31 30 473 476 481 488 504 510	climsub	$⊢ φ \to R ⇝ (B - 0)$
512	92	subid1d	$⊢ φ \to B - 0 = B$
513	511 512	breqtrd	$⊢ φ \to R ⇝ B$
514		releldm	$⊢ (Rel ⇝ \land R ⇝ B) \to R \in dom ⇝$
515	464 513 514	syl2anc	$⊢ φ \to R \in dom ⇝$
516		fveq2	$⊢ l = k \to ℤ_{\geq l} = ℤ_{\geq k}$
517		fveq2	$⊢ l = k \to R (l) = R (k)$
518	517	oveq2d	$⊢ l = k \to R (h) - R (l) = R (h) - R (k)$
519	518	fveq2d	$⊢ l = k \to \|R (h) - R (l)\| = \|R (h) - R (k)\|$
520	519	breq1d	$⊢ l = k \to (\|R (h) - R (l)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \leftrightarrow \|R (h) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1})$
521	516 520	raleqbidv	$⊢ l = k \to (\forall h \in ℤ_{\geq l} \|R (h) - R (l)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \leftrightarrow \forall h \in ℤ_{\geq k} \|R (h) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1})$
522	521	cbvrabv	$⊢ \{l \in ℤ_{\geq M} \| \forall h \in ℤ_{\geq l} \|R (h) - R (l)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} = \{k \in ℤ_{\geq M} \| \forall h \in ℤ_{\geq k} \|R (h) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\}$
523		fveq2	$⊢ h = i \to R (h) = R (i)$
524	523	fvoveq1d	$⊢ h = i \to \|R (h) - R (k)\| = \|R (i) - R (k)\|$
525	524	breq1d	$⊢ h = i \to (\|R (h) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \leftrightarrow \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1})$
526	525	cbvralvw	$⊢ \forall h \in ℤ_{\geq k} \|R (h) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \leftrightarrow \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
527	526	rgenw	$⊢ \forall k \in ℤ_{\geq M} (\forall h \in ℤ_{\geq k} \|R (h) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \leftrightarrow \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1})$
528		rabbi	$⊢ \forall k \in ℤ_{\geq M} (\forall h \in ℤ_{\geq k} \|R (h) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \leftrightarrow \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}) \leftrightarrow \{k \in ℤ_{\geq M} \| \forall h \in ℤ_{\geq k} \|R (h) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} = \{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\}$
529	527 528	mpbi	$⊢ \{k \in ℤ_{\geq M} \| \forall h \in ℤ_{\geq k} \|R (h) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} = \{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\}$
530	522 529	eqtri	$⊢ \{l \in ℤ_{\geq M} \| \forall h \in ℤ_{\geq l} \|R (h) - R (l)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} = \{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\}$
531	530	infeq1i	$⊢ inf (\{l \in ℤ_{\geq M} \| \forall h \in ℤ_{\geq l} \|R (h) - R (l)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} ℝ <) = inf (\{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} ℝ <)$
532	1 2 3 460 5 6 30 461 462 515 531	ioodvbdlimc1lem1	$⊢ φ \to (j \in ℤ_{\geq M} ⟼ F (R (j))) ⇝ lim sup ((j \in ℤ_{\geq M} ⟼ F (R (j))))$
533	10	fvmpt2	$⊢ (j \in ℤ_{\geq M} \land B - (\frac{1}{j}) \in ℝ) \to R (j) = B - (\frac{1}{j})$
534	115 65 533	syl2anc	$⊢ (φ \land j \in ℤ_{\geq M}) \to R (j) = B - (\frac{1}{j})$
535	534	eqcomd	$⊢ (φ \land j \in ℤ_{\geq M}) \to B - (\frac{1}{j}) = R (j)$
536	535	fveq2d	$⊢ (φ \land j \in ℤ_{\geq M}) \to F (B - (\frac{1}{j})) = F (R (j))$
537	536	mpteq2dva	$⊢ φ \to (j \in ℤ_{\geq M} ⟼ F (B - (\frac{1}{j}))) = (j \in ℤ_{\geq M} ⟼ F (R (j)))$
538	9 537	eqtrid	$⊢ φ \to S = (j \in ℤ_{\geq M} ⟼ F (R (j)))$
539	538	fveq2d	$⊢ φ \to lim sup (S) = lim sup ((j \in ℤ_{\geq M} ⟼ F (R (j))))$
540	532 538 539	3brtr4d	$⊢ φ \to S ⇝ lim sup (S)$
541	465	mptex	$⊢ (j \in ℤ_{\geq M} ⟼ F (B - (\frac{1}{j}))) \in V$
542	9 541	eqeltri	$⊢ S \in V$
543	542	a1i	$⊢ φ \to S \in V$
544		eqidd	$⊢ (φ \land c \in ℤ) \to S (c) = S (c)$
545	543 544	clim	$⊢ φ \to (S ⇝ lim sup (S) \leftrightarrow (lim sup (S) \in ℂ \land \forall a \in ℝ^{+} \exists b \in ℤ \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < a)))$
546	540 545	mpbid	$⊢ φ \to (lim sup (S) \in ℂ \land \forall a \in ℝ^{+} \exists b \in ℤ \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < a))$
547	546	simprd	$⊢ φ \to \forall a \in ℝ^{+} \exists b \in ℤ \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < a)$
548	547	adantr	$⊢ (φ \land x \in ℝ^{+}) \to \forall a \in ℝ^{+} \exists b \in ℤ \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < a)$
549		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
550	549	rphalfcld	$⊢ (φ \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ^{+}$
551		breq2	$⊢ a = \frac{x}{2} \to (\|S (c) - lim sup (S)\| < a \leftrightarrow \|S (c) - lim sup (S)\| < \frac{x}{2})$
552	551	anbi2d	$⊢ a = \frac{x}{2} \to ((S (c) \in ℂ \land \|S (c) - lim sup (S)\| < a) \leftrightarrow (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2}))$
553	552	rexralbidv	$⊢ a = \frac{x}{2} \to (\exists b \in ℤ \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < a) \leftrightarrow \exists b \in ℤ \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2}))$
554	553	rspccva	$⊢ (\forall a \in ℝ^{+} \exists b \in ℤ \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < a) \land \frac{x}{2} \in ℝ^{+}) \to \exists b \in ℤ \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2})$
555	548 550 554	syl2anc	$⊢ (φ \land x \in ℝ^{+}) \to \exists b \in ℤ \forall c \in ℤ_{\geq b} (S (c) \in ℂ \land \|S (c) - lim sup (S)\| < \frac{x}{2})$
556	452 555	r19.29a	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in ℤ_{\geq N} \|S (j) - lim sup (S)\| < \frac{x}{2}$
557	406 556	r19.29a	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in (A, B) ((z \neq B \land \|z - B\| < y) \to \|F (z) - lim sup (S)\| < x)$
558	557	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in (A, B) ((z \neq B \land \|z - B\| < y) \to \|F (z) - lim sup (S)\| < x)$
559		ioosscn	$⊢ (A, B) \subseteq ℂ$
560	559	a1i	$⊢ φ \to (A, B) \subseteq ℂ$
561	455 560 92	ellimc3	$⊢ φ \to (lim sup (S) \in (F {lim}_{ℂ} B) \leftrightarrow (lim sup (S) \in ℂ \land \forall x \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in (A, B) ((z \neq B \land \|z - B\| < y) \to \|F (z) - lim sup (S)\| < x)))$
562	138 558 561	mpbir2and	$⊢ φ \to lim sup (S) \in (F {lim}_{ℂ} B)$

Metamath Proof Explorer

Theorem ioodvbdlimc2lem

Proof