ioodvbdlimc1lem2

Description: Limit at the lower 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	ioodvbdlimc1lem2.a	$⊢ φ \to A \in ℝ$
	ioodvbdlimc1lem2.b	$⊢ φ \to B \in ℝ$
	ioodvbdlimc1lem2.altb	$⊢ φ \to A < B$
	ioodvbdlimc1lem2.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
	ioodvbdlimc1lem2.dmdv	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	ioodvbdlimc1lem2.dvbd	$⊢ φ \to \exists y \in ℝ \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq y$
	ioodvbdlimc1lem2.y	$⊢ Y = sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
	ioodvbdlimc1lem2.m	$⊢ M = ⌊\frac{1}{B - A}⌋ + 1$
	ioodvbdlimc1lem2.s	$⊢ S = (j \in ℤ_{\geq M} ⟼ F (A + (\frac{1}{j})))$
	ioodvbdlimc1lem2.r	$⊢ R = (j \in ℤ_{\geq M} ⟼ A + (\frac{1}{j}))$
	ioodvbdlimc1lem2.n	$⊢ N = if (M \leq ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, ⌊\frac{Y}{\frac{x}{2}}⌋ + 1, M)$
	ioodvbdlimc1lem2.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 - A\| < \frac{1}{j})$
Assertion	ioodvbdlimc1lem2	$⊢ φ \to lim sup (S) \in (F {lim}_{ℂ} A)$

Proof

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

Metamath Proof Explorer

Theorem ioodvbdlimc1lem2

Proof