ioodvbdlimc1lem1

Description: If F has bounded derivative on ( A (,) B ) then a sequence of points in its image converges to its limsup . (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 3-Oct-2020)

	Ref	Expression
Hypotheses	ioodvbdlimc1lem1.a	$⊢ φ \to A \in ℝ$
	ioodvbdlimc1lem1.b	$⊢ φ \to B \in ℝ$
	ioodvbdlimc1lem1.altb	$⊢ φ \to A < B$
	ioodvbdlimc1lem1.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℝ$
	ioodvbdlimc1lem1.dmdv	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	ioodvbdlimc1lem1.dvbd	$⊢ φ \to \exists y \in ℝ \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq y$
	ioodvbdlimc1lem1.m	$⊢ φ \to M \in ℤ$
	ioodvbdlimc1lem1.r	$⊢ φ \to R : ℤ_{\geq M} ⟶ (A, B)$
	ioodvbdlimc1lem1.s	$⊢ S = (j \in ℤ_{\geq M} ⟼ F (R (j)))$
	ioodvbdlimc1lem1.rcnv	$⊢ φ \to R \in dom ⇝$
	ioodvbdlimc1lem1.k	$⊢ K = sup (\{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} ℝ <)$
Assertion	ioodvbdlimc1lem1	$⊢ φ \to S ⇝ lim sup (S)$

Proof

Step	Hyp	Ref	Expression
1		ioodvbdlimc1lem1.a	$⊢ φ \to A \in ℝ$
2		ioodvbdlimc1lem1.b	$⊢ φ \to B \in ℝ$
3		ioodvbdlimc1lem1.altb	$⊢ φ \to A < B$
4		ioodvbdlimc1lem1.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℝ$
5		ioodvbdlimc1lem1.dmdv	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
6		ioodvbdlimc1lem1.dvbd	$⊢ φ \to \exists y \in ℝ \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq y$
7		ioodvbdlimc1lem1.m	$⊢ φ \to M \in ℤ$
8		ioodvbdlimc1lem1.r	$⊢ φ \to R : ℤ_{\geq M} ⟶ (A, B)$
9		ioodvbdlimc1lem1.s	$⊢ S = (j \in ℤ_{\geq M} ⟼ F (R (j)))$
10		ioodvbdlimc1lem1.rcnv	$⊢ φ \to R \in dom ⇝$
11		ioodvbdlimc1lem1.k	$⊢ K = sup (\{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} ℝ <)$
12		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
13		cncff	$⊢ F : (A, B) \underset{cn}{⟶} ℝ \to F : (A, B) ⟶ ℝ$
14	4 13	syl	$⊢ φ \to F : (A, B) ⟶ ℝ$
15	14	adantr	$⊢ (φ \land j \in ℤ_{\geq M}) \to F : (A, B) ⟶ ℝ$
16	8	ffvelcdmda	$⊢ (φ \land j \in ℤ_{\geq M}) \to R (j) \in (A, B)$
17	15 16	ffvelcdmd	$⊢ (φ \land j \in ℤ_{\geq M}) \to F (R (j)) \in ℝ$
18	17 9	fmptd	$⊢ φ \to S : ℤ_{\geq M} ⟶ ℝ$
19		ssrab2	$⊢ \{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} \subseteq ℤ_{\geq M}$
20		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
21	20	adantl	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ$
22		2fveq3	$⊢ z = x \to \|F_{ℝ}^{'} (z)\| = \|F_{ℝ}^{'} (x)\|$
23	22	cbvmptv	$⊢ (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) = (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|)$
24	23	rneqi	$⊢ ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) = ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|)$
25	24	supeq1i	$⊢ sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) = sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
26		ioomidp	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to \frac{A + B}{2} \in (A, B)$
27	1 2 3 26	syl3anc	$⊢ φ \to \frac{A + B}{2} \in (A, B)$
28	27	ne0d	$⊢ φ \to (A, B) \neq \emptyset$
29		ioossre	$⊢ (A, B) \subseteq ℝ$
30	29	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
31		dvfre	$⊢ (F : (A, B) ⟶ ℝ \land (A, B) \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
32	14 30 31	syl2anc	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
33	5	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℝ)$
34	32 33	mpbid	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℝ$
35		ax-resscn	$⊢ ℝ \subseteq ℂ$
36	35	a1i	$⊢ φ \to ℝ \subseteq ℂ$
37	34 36	fssd	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℂ$
38	37	ffvelcdmda	$⊢ (φ \land x \in (A, B)) \to F_{ℝ}^{'} (x) \in ℂ$
39	38	abscld	$⊢ (φ \land x \in (A, B)) \to \|F_{ℝ}^{'} (x)\| \in ℝ$
40		eqid	$⊢ (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) = (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|)$
41		eqid	$⊢ sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <) = sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
42	28 39 6 40 41	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)\|) ℝ <))$
43	42	simpld	$⊢ φ \to sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <) \in ℝ$
44	25 43	eqeltrid	$⊢ φ \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) \in ℝ$
45	44	adantr	$⊢ (φ \land x \in ℝ^{+}) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) \in ℝ$
46		peano2re	$⊢ sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) \in ℝ \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \in ℝ$
47	45 46	syl	$⊢ (φ \land x \in ℝ^{+}) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \in ℝ$
48		0red	$⊢ φ \to 0 \in ℝ$
49		1red	$⊢ φ \to 1 \in ℝ$
50	48 49	readdcld	$⊢ φ \to 0 + 1 \in ℝ$
51	44 46	syl	$⊢ φ \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \in ℝ$
52	48	ltp1d	$⊢ φ \to 0 < 0 + 1$
53	37 27	ffvelcdmd	$⊢ φ \to F_{ℝ}^{'} (\frac{A + B}{2}) \in ℂ$
54	53	abscld	$⊢ φ \to \|F_{ℝ}^{'} (\frac{A + B}{2})\| \in ℝ$
55	53	absge0d	$⊢ φ \to 0 \leq \|F_{ℝ}^{'} (\frac{A + B}{2})\|$
56	42	simprd	$⊢ φ \to \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
57		2fveq3	$⊢ y = x \to \|F_{ℝ}^{'} (y)\| = \|F_{ℝ}^{'} (x)\|$
58	25	a1i	$⊢ y = x \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) = sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
59	57 58	breq12d	$⊢ y = x \to (\|F_{ℝ}^{'} (y)\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) \leftrightarrow \|F_{ℝ}^{'} (x)\| \leq sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <))$
60	59	cbvralvw	$⊢ \forall y \in (A, B) \|F_{ℝ}^{'} (y)\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) \leftrightarrow \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq sup (ran (x \in (A, B) ⟼ \|F_{ℝ}^{'} (x)\|) ℝ <)$
61	56 60	sylibr	$⊢ φ \to \forall y \in (A, B) \|F_{ℝ}^{'} (y)\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <)$
62		2fveq3	$⊢ y = \frac{A + B}{2} \to \|F_{ℝ}^{'} (y)\| = \|F_{ℝ}^{'} (\frac{A + B}{2})\|$
63	62	breq1d	$⊢ y = \frac{A + B}{2} \to (\|F_{ℝ}^{'} (y)\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) \leftrightarrow \|F_{ℝ}^{'} (\frac{A + B}{2})\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <))$
64	63	rspcva	$⊢ (\frac{A + B}{2} \in (A, B) \land \forall y \in (A, B) \|F_{ℝ}^{'} (y)\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <)) \to \|F_{ℝ}^{'} (\frac{A + B}{2})\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <)$
65	27 61 64	syl2anc	$⊢ φ \to \|F_{ℝ}^{'} (\frac{A + B}{2})\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <)$
66	48 54 44 55 65	letrd	$⊢ φ \to 0 \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <)$
67	48 44 49 66	leadd1dd	$⊢ φ \to 0 + 1 \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1$
68	48 50 51 52 67	ltletrd	$⊢ φ \to 0 < sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1$
69	68	gt0ne0d	$⊢ φ \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \neq 0$
70	69	adantr	$⊢ (φ \land x \in ℝ^{+}) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \neq 0$
71	21 47 70	redivcld	$⊢ (φ \land x \in ℝ^{+}) \to \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \in ℝ$
72		rpgt0	$⊢ x \in ℝ^{+} \to 0 < x$
73	72	adantl	$⊢ (φ \land x \in ℝ^{+}) \to 0 < x$
74	68	adantr	$⊢ (φ \land x \in ℝ^{+}) \to 0 < sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1$
75	21 47 73 74	divgt0d	$⊢ (φ \land x \in ℝ^{+}) \to 0 < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
76	71 75	elrpd	$⊢ (φ \land x \in ℝ^{+}) \to \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \in ℝ^{+}$
77	7	adantr	$⊢ (φ \land x \in ℝ^{+}) \to M \in ℤ$
78	10	adantr	$⊢ (φ \land x \in ℝ^{+}) \to R \in dom ⇝$
79	12	climcau	$⊢ (M \in ℤ \land R \in dom ⇝) \to \forall w \in ℝ^{+} \exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < w$
80	77 78 79	syl2anc	$⊢ (φ \land x \in ℝ^{+}) \to \forall w \in ℝ^{+} \exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < w$
81		breq2	$⊢ w = \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \to (\|R (i) - R (k)\| < w \leftrightarrow \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1})$
82	81	rexralbidv	$⊢ w = \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \to (\exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < w \leftrightarrow \exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1})$
83	82	rspcva	$⊢ (\frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \in ℝ^{+} \land \forall w \in ℝ^{+} \exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < w) \to \exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
84	76 80 83	syl2anc	$⊢ (φ \land x \in ℝ^{+}) \to \exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
85		rabn0	$⊢ \{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} \neq \emptyset \leftrightarrow \exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
86	84 85	sylibr	$⊢ (φ \land x \in ℝ^{+}) \to \{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} \neq \emptyset$
87		infssuzcl	$⊢ (\{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} \subseteq ℤ_{\geq M} \land \{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} \neq \emptyset) \to sup (\{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} ℝ <) \in \{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\}$
88	19 86 87	sylancr	$⊢ (φ \land x \in ℝ^{+}) \to sup (\{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\} ℝ <) \in \{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\}$
89	11 88	eqeltrid	$⊢ (φ \land x \in ℝ^{+}) \to K \in \{k \in ℤ_{\geq M} \| \forall i \in ℤ_{\geq k} \|R (i) - R (k)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}\}$
90	19 89	sselid	$⊢ (φ \land x \in ℝ^{+}) \to K \in ℤ_{\geq M}$
91		2fveq3	$⊢ j = i \to F (R (j)) = F (R (i))$
92		uzss	$⊢ K \in ℤ_{\geq M} \to ℤ_{\geq K} \subseteq ℤ_{\geq M}$
93	90 92	syl	$⊢ (φ \land x \in ℝ^{+}) \to ℤ_{\geq K} \subseteq ℤ_{\geq M}$
94	93	sselda	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to i \in ℤ_{\geq M}$
95	14	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to F : (A, B) ⟶ ℝ$
96	8	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to R : ℤ_{\geq M} ⟶ (A, B)$
97	96 94	ffvelcdmd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to R (i) \in (A, B)$
98	95 97	ffvelcdmd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to F (R (i)) \in ℝ$
99	9 91 94 98	fvmptd3	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to S (i) = F (R (i))$
100		2fveq3	$⊢ j = K \to F (R (j)) = F (R (K))$
101	90	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to K \in ℤ_{\geq M}$
102	96 101	ffvelcdmd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to R (K) \in (A, B)$
103	95 102	ffvelcdmd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to F (R (K)) \in ℝ$
104	9 100 101 103	fvmptd3	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to S (K) = F (R (K))$
105	99 104	oveq12d	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to S (i) - S (K) = F (R (i)) - F (R (K))$
106	105	fveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to \|S (i) - S (K)\| = \|F (R (i)) - F (R (K))\|$
107	98	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to F (R (i)) \in ℂ$
108	103	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to F (R (K)) \in ℂ$
109	107 108	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to F (R (i)) - F (R (K)) \in ℂ$
110	109	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to \|F (R (i)) - F (R (K))\| \in ℝ$
111	110	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to \|F (R (i)) - F (R (K))\| \in ℝ$
112	44	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) \in ℝ$
113	112	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) \in ℝ$
114	8	adantr	$⊢ (φ \land x \in ℝ^{+}) \to R : ℤ_{\geq M} ⟶ (A, B)$
115	114 90	ffvelcdmd	$⊢ (φ \land x \in ℝ^{+}) \to R (K) \in (A, B)$
116	29 115	sselid	$⊢ (φ \land x \in ℝ^{+}) \to R (K) \in ℝ$
117	116	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (K) \in ℝ$
118	29 97	sselid	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to R (i) \in ℝ$
119	118	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (i) \in ℝ$
120	117 119	resubcld	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (K) - R (i) \in ℝ$
121	113 120	remulcld	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (K) - R (i)) \in ℝ$
122	20	ad3antlr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to x \in ℝ$
123	107	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to F (R (i)) \in ℂ$
124	108	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to F (R (K)) \in ℂ$
125	123 124	abssubd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to \|F (R (i)) - F (R (K))\| = \|F (R (K)) - F (R (i))\|$
126	1	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to A \in ℝ$
127	2	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to B \in ℝ$
128	95	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to F : (A, B) ⟶ ℝ$
129	5	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to dom F_{ℝ}^{'} = (A, B)$
130	61	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to \forall y \in (A, B) \|F_{ℝ}^{'} (y)\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <)$
131	97	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (i) \in (A, B)$
132	118	rexrd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to R (i) \in ℝ^{*}$
133	132	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (i) \in ℝ^{*}$
134	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
135	134	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to B \in ℝ^{*}$
136	135	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to B \in ℝ^{*}$
137		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (i) < R (K)$
138	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
139	138	adantr	$⊢ (φ \land x \in ℝ^{+}) \to A \in ℝ^{*}$
140	134	adantr	$⊢ (φ \land x \in ℝ^{+}) \to B \in ℝ^{*}$
141		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land R (K) \in (A, B)) \to R (K) < B$
142	139 140 115 141	syl3anc	$⊢ (φ \land x \in ℝ^{+}) \to R (K) < B$
143	142	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (K) < B$
144	133 136 117 137 143	eliood	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (K) \in (R (i), B)$
145	126 127 128 129 113 130 131 144	dvbdfbdioolem1	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to (\|F (R (K)) - F (R (i))\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (K) - R (i)) \land \|F (R (K)) - F (R (i))\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (B - A))$
146	145	simpld	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to \|F (R (K)) - F (R (i))\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (K) - R (i))$
147	125 146	eqbrtrd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to \|F (R (i)) - F (R (K))\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (K) - R (i))$
148	113 46	syl	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \in ℝ$
149	148 120	remulcld	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to (sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1) (R (K) - R (i)) \in ℝ$
150	119 117	posdifd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to (R (i) < R (K) \leftrightarrow 0 < R (K) - R (i))$
151	137 150	mpbid	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to 0 < R (K) - R (i)$
152	120 151	elrpd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (K) - R (i) \in ℝ^{+}$
153	113	ltp1d	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) < sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1$
154	113 148 152 153	ltmul1dd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (K) - R (i)) < (sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1) (R (K) - R (i))$
155	29 102	sselid	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to R (K) \in ℝ$
156	118 155	resubcld	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to R (i) - R (K) \in ℝ$
157	156	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to R (i) - R (K) \in ℂ$
158	157	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to \|R (i) - R (K)\| \in ℝ$
159	158	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to \|R (i) - R (K)\| \in ℝ$
160	71	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \in ℝ$
161	120	leabsd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (K) - R (i) \leq \|R (K) - R (i)\|$
162	117	recnd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (K) \in ℂ$
163	118	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to R (i) \in ℂ$
164	163	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (i) \in ℂ$
165	162 164	abssubd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to \|R (K) - R (i)\| = \|R (i) - R (K)\|$
166	161 165	breqtrd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (K) - R (i) \leq \|R (i) - R (K)\|$
167		fveq2	$⊢ k = K \to ℤ_{\geq k} = ℤ_{\geq K}$
168		fveq2	$⊢ k = K \to R (k) = R (K)$
169	168	oveq2d	$⊢ k = K \to R (i) - R (k) = R (i) - R (K)$
170	169	fveq2d	$⊢ k = K \to \|R (i) - R (k)\| = \|R (i) - R (K)\|$
171	170	breq1d	$⊢ k = K \to (\|R (i) - 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})$
172	167 171	raleqbidv	$⊢ k = K \to (\forall i \in ℤ_{\geq k} \|R (i) - 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})$
173	172	elrab	$⊢ K \in \{k \in ℤ_{\geq M} \| \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} \land \forall i \in ℤ_{\geq K} \|R (i) - R (K)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1})$
174	89 173	sylib	$⊢ (φ \land x \in ℝ^{+}) \to (K \in ℤ_{\geq M} \land \forall i \in ℤ_{\geq K} \|R (i) - R (K)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1})$
175	174	simprd	$⊢ (φ \land x \in ℝ^{+}) \to \forall i \in ℤ_{\geq K} \|R (i) - R (K)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
176	175	r19.21bi	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to \|R (i) - R (K)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
177	176	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to \|R (i) - R (K)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
178	120 159 160 166 177	lelttrd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to R (K) - R (i) < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
179	51 68	elrpd	$⊢ φ \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \in ℝ^{+}$
180	179	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \in ℝ^{+}$
181	120 122 180	ltmuldiv2d	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to ((sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1) (R (K) - R (i)) < x \leftrightarrow R (K) - R (i) < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1})$
182	178 181	mpbird	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to (sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1) (R (K) - R (i)) < x$
183	121 149 122 154 182	lttrd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (K) - R (i)) < x$
184	111 121 122 147 183	lelttrd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) < R (K)) \to \|F (R (i)) - F (R (K))\| < x$
185		fveq2	$⊢ R (i) = R (K) \to F (R (i)) = F (R (K))$
186	185	oveq1d	$⊢ R (i) = R (K) \to F (R (i)) - F (R (K)) = F (R (K)) - F (R (K))$
187	108	subidd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to F (R (K)) - F (R (K)) = 0$
188	186 187	sylan9eqr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) = R (K)) \to F (R (i)) - F (R (K)) = 0$
189	188	abs00bd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) = R (K)) \to \|F (R (i)) - F (R (K))\| = 0$
190	72	ad3antlr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) = R (K)) \to 0 < x$
191	189 190	eqbrtrd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (i) = R (K)) \to \|F (R (i)) - F (R (K))\| < x$
192	191	adantlr	$⊢ ((((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land \neg R (i) < R (K)) \land R (i) = R (K)) \to \|F (R (i)) - F (R (K))\| < x$
193		simpll	$⊢ ((((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land \neg R (i) < R (K)) \land \neg R (i) = R (K)) \to ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K})$
194	155	ad2antrr	$⊢ ((((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land \neg R (i) < R (K)) \land \neg R (i) = R (K)) \to R (K) \in ℝ$
195	118	ad2antrr	$⊢ ((((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land \neg R (i) < R (K)) \land \neg R (i) = R (K)) \to R (i) \in ℝ$
196		id	$⊢ R (K) = R (i) \to R (K) = R (i)$
197	196	eqcomd	$⊢ R (K) = R (i) \to R (i) = R (K)$
198	197	necon3bi	$⊢ \neg R (i) = R (K) \to R (K) \neq R (i)$
199	198	adantl	$⊢ ((((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land \neg R (i) < R (K)) \land \neg R (i) = R (K)) \to R (K) \neq R (i)$
200		simplr	$⊢ ((((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land \neg R (i) < R (K)) \land \neg R (i) = R (K)) \to \neg R (i) < R (K)$
201	194 195 199 200	lttri5d	$⊢ ((((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land \neg R (i) < R (K)) \land \neg R (i) = R (K)) \to R (K) < R (i)$
202	110	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to \|F (R (i)) - F (R (K))\| \in ℝ$
203	112 156	remulcld	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (i) - R (K)) \in ℝ$
204	203	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (i) - R (K)) \in ℝ$
205	20	ad3antlr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to x \in ℝ$
206	1	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to A \in ℝ$
207	2	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to B \in ℝ$
208	95	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to F : (A, B) ⟶ ℝ$
209	5	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to dom F_{ℝ}^{'} = (A, B)$
210	44	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) \in ℝ$
211	61	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to \forall y \in (A, B) \|F_{ℝ}^{'} (y)\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <)$
212	102	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (K) \in (A, B)$
213	116	rexrd	$⊢ (φ \land x \in ℝ^{+}) \to R (K) \in ℝ^{*}$
214	213	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (K) \in ℝ^{*}$
215	207	rexrd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to B \in ℝ^{*}$
216	118	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (i) \in ℝ$
217		simpr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (K) < R (i)$
218	138	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to A \in ℝ^{*}$
219		iooltub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land R (i) \in (A, B)) \to R (i) < B$
220	218 135 97 219	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to R (i) < B$
221	220	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (i) < B$
222	214 215 216 217 221	eliood	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (i) \in (R (K), B)$
223	206 207 208 209 210 211 212 222	dvbdfbdioolem1	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to (\|F (R (i)) - F (R (K))\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (i) - R (K)) \land \|F (R (i)) - F (R (K))\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (B - A))$
224	223	simpld	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to \|F (R (i)) - F (R (K))\| \leq sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (i) - R (K))$
225		1red	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to 1 \in ℝ$
226	210 225	readdcld	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \in ℝ$
227	155	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (K) \in ℝ$
228	216 227	resubcld	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (i) - R (K) \in ℝ$
229	226 228	remulcld	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to (sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1) (R (i) - R (K)) \in ℝ$
230	210 46	syl	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \in ℝ$
231	227 216	posdifd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to (R (K) < R (i) \leftrightarrow 0 < R (i) - R (K))$
232	217 231	mpbid	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to 0 < R (i) - R (K)$
233	228 232	elrpd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (i) - R (K) \in ℝ^{+}$
234	210	ltp1d	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) < sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1$
235	210 230 233 234	ltmul1dd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (i) - R (K)) < (sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1) (R (i) - R (K))$
236	158	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to \|R (i) - R (K)\| \in ℝ$
237	71	ad2antrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1} \in ℝ$
238	228	leabsd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (i) - R (K) \leq \|R (i) - R (K)\|$
239	176	adantr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to \|R (i) - R (K)\| < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
240	228 236 237 238 239	lelttrd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to R (i) - R (K) < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1}$
241	179	ad3antrrr	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1 \in ℝ^{+}$
242	228 205 241	ltmuldiv2d	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to ((sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1) (R (i) - R (K)) < x \leftrightarrow R (i) - R (K) < \frac{x}{sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1})$
243	240 242	mpbird	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to (sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) + 1) (R (i) - R (K)) < x$
244	204 229 205 235 243	lttrd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to sup (ran (z \in (A, B) ⟼ \|F_{ℝ}^{'} (z)\|) ℝ <) (R (i) - R (K)) < x$
245	202 204 205 224 244	lelttrd	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land R (K) < R (i)) \to \|F (R (i)) - F (R (K))\| < x$
246	193 201 245	syl2anc	$⊢ ((((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land \neg R (i) < R (K)) \land \neg R (i) = R (K)) \to \|F (R (i)) - F (R (K))\| < x$
247	192 246	pm2.61dan	$⊢ (((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \land \neg R (i) < R (K)) \to \|F (R (i)) - F (R (K))\| < x$
248	184 247	pm2.61dan	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to \|F (R (i)) - F (R (K))\| < x$
249	106 248	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land i \in ℤ_{\geq K}) \to \|S (i) - S (K)\| < x$
250	249	ralrimiva	$⊢ (φ \land x \in ℝ^{+}) \to \forall i \in ℤ_{\geq K} \|S (i) - S (K)\| < x$
251		fveq2	$⊢ k = K \to S (k) = S (K)$
252	251	oveq2d	$⊢ k = K \to S (i) - S (k) = S (i) - S (K)$
253	252	fveq2d	$⊢ k = K \to \|S (i) - S (k)\| = \|S (i) - S (K)\|$
254	253	breq1d	$⊢ k = K \to (\|S (i) - S (k)\| < x \leftrightarrow \|S (i) - S (K)\| < x)$
255	167 254	raleqbidv	$⊢ k = K \to (\forall i \in ℤ_{\geq k} \|S (i) - S (k)\| < x \leftrightarrow \forall i \in ℤ_{\geq K} \|S (i) - S (K)\| < x)$
256	255	rspcev	$⊢ (K \in ℤ_{\geq M} \land \forall i \in ℤ_{\geq K} \|S (i) - S (K)\| < x) \to \exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|S (i) - S (k)\| < x$
257	90 250 256	syl2anc	$⊢ (φ \land x \in ℝ^{+}) \to \exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|S (i) - S (k)\| < x$
258	257	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists k \in ℤ_{\geq M} \forall i \in ℤ_{\geq k} \|S (i) - S (k)\| < x$
259	12 18 258	caurcvg	$⊢ φ \to S ⇝ lim sup (S)$

Metamath Proof Explorer

Theorem ioodvbdlimc1lem1

Proof