pntpbnd1

	Ref	Expression
Hypotheses	pntpbnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	pntpbnd1.e	$⊢ φ \to E \in (0, 1)$
	pntpbnd1.x	$⊢ X = e^{\frac{2}{E}}$
	pntpbnd1.y	$⊢ φ \to Y \in (X, +∞)$
	pntpbnd1.1	$⊢ φ \to A \in ℝ^{+}$
	pntpbnd1.2	$⊢ φ \to \forall i \in ℕ \forall j \in ℤ \|\sum_{y = i}^{j} (\frac{R (y)}{y (y + 1)})\| \leq A$
	pntpbnd1.c	$⊢ C = A + 2$
	pntpbnd1.k	$⊢ φ \to K \in [e^{\frac{C}{E}}, +∞)$
	pntpbnd1.3	$⊢ φ \to \neg \exists y \in ℕ ((Y < y \land y \leq K Y) \land \|\frac{R (y)}{y}\| \leq E)$
Assertion	pntpbnd1	$⊢ φ \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} \|\frac{R (n)}{n (n + 1)}\| \leq A$

Proof

Step	Hyp	Ref	Expression
1		pntpbnd.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		pntpbnd1.e	$⊢ φ \to E \in (0, 1)$
3		pntpbnd1.x	$⊢ X = e^{\frac{2}{E}}$
4		pntpbnd1.y	$⊢ φ \to Y \in (X, +∞)$
5		pntpbnd1.1	$⊢ φ \to A \in ℝ^{+}$
6		pntpbnd1.2	$⊢ φ \to \forall i \in ℕ \forall j \in ℤ \|\sum_{y = i}^{j} (\frac{R (y)}{y (y + 1)})\| \leq A$
7		pntpbnd1.c	$⊢ C = A + 2$
8		pntpbnd1.k	$⊢ φ \to K \in [e^{\frac{C}{E}}, +∞)$
9		pntpbnd1.3	$⊢ φ \to \neg \exists y \in ℕ ((Y < y \land y \leq K Y) \land \|\frac{R (y)}{y}\| \leq E)$
10		fzfid	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \to (⌊Y⌋ + 1 \dots ⌊K Y⌋) \in Fin$
11		ioossre	$⊢ (X, +∞) \subseteq ℝ$
12	11 4	sselid	$⊢ φ \to Y \in ℝ$
13		0red	$⊢ φ \to 0 \in ℝ$
14		2re	$⊢ 2 \in ℝ$
15		ioossre	$⊢ (0, 1) \subseteq ℝ$
16	15 2	sselid	$⊢ φ \to E \in ℝ$
17		eliooord	$⊢ E \in (0, 1) \to (0 < E \land E < 1)$
18	2 17	syl	$⊢ φ \to (0 < E \land E < 1)$
19	18	simpld	$⊢ φ \to 0 < E$
20	16 19	elrpd	$⊢ φ \to E \in ℝ^{+}$
21		rerpdivcl	$⊢ (2 \in ℝ \land E \in ℝ^{+}) \to \frac{2}{E} \in ℝ$
22	14 20 21	sylancr	$⊢ φ \to \frac{2}{E} \in ℝ$
23	22	reefcld	$⊢ φ \to e^{\frac{2}{E}} \in ℝ$
24	3 23	eqeltrid	$⊢ φ \to X \in ℝ$
25		efgt0	$⊢ \frac{2}{E} \in ℝ \to 0 < e^{\frac{2}{E}}$
26	22 25	syl	$⊢ φ \to 0 < e^{\frac{2}{E}}$
27	26 3	breqtrrdi	$⊢ φ \to 0 < X$
28		eliooord	$⊢ Y \in (X, +∞) \to (X < Y \land Y < +∞)$
29	4 28	syl	$⊢ φ \to (X < Y \land Y < +∞)$
30	29	simpld	$⊢ φ \to X < Y$
31	13 24 12 27 30	lttrd	$⊢ φ \to 0 < Y$
32	13 12 31	ltled	$⊢ φ \to 0 \leq Y$
33		flge0nn0	$⊢ (Y \in ℝ \land 0 \leq Y) \to ⌊Y⌋ \in ℕ_{0}$
34	12 32 33	syl2anc	$⊢ φ \to ⌊Y⌋ \in ℕ_{0}$
35		nn0p1nn	$⊢ ⌊Y⌋ \in ℕ_{0} \to ⌊Y⌋ + 1 \in ℕ$
36	34 35	syl	$⊢ φ \to ⌊Y⌋ + 1 \in ℕ$
37		elfzuz	$⊢ n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) \to n \in ℤ_{\geq (⌊Y⌋ + 1)}$
38		eluznn	$⊢ (⌊Y⌋ + 1 \in ℕ \land n \in ℤ_{\geq (⌊Y⌋ + 1)}) \to n \in ℕ$
39	36 37 38	syl2an	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n \in ℕ$
40	39	nnrpd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n \in ℝ^{+}$
41	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
42	41	ffvelrni	$⊢ n \in ℝ^{+} \to R (n) \in ℝ$
43	40 42	syl	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to R (n) \in ℝ$
44	39	peano2nnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n + 1 \in ℕ$
45	39 44	nnmulcld	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n (n + 1) \in ℕ$
46	43 45	nndivred	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{R (n)}{n (n + 1)} \in ℝ$
47	46	adantlr	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{R (n)}{n (n + 1)} \in ℝ$
48	10 47	fsumrecl	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)}) \in ℝ$
49	43	adantlr	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to R (n) \in ℝ$
50		fveq2	$⊢ i = n \to R (i) = R (n)$
51	50	breq2d	$⊢ i = n \to (0 \leq R (i) \leftrightarrow 0 \leq R (n))$
52	51	rspccva	$⊢ (\forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to 0 \leq R (n)$
53	52	adantll	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to 0 \leq R (n)$
54	45	adantlr	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n (n + 1) \in ℕ$
55	54	nnred	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n (n + 1) \in ℝ$
56	54	nngt0d	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to 0 < n (n + 1)$
57		divge0	$⊢ ((R (n) \in ℝ \land 0 \leq R (n)) \land (n (n + 1) \in ℝ \land 0 < n (n + 1))) \to 0 \leq \frac{R (n)}{n (n + 1)}$
58	49 53 55 56 57	syl22anc	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to 0 \leq \frac{R (n)}{n (n + 1)}$
59	10 47 58	fsumge0	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \to 0 \leq \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})$
60	48 59	absidd	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \to \|\sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})\| = \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})$
61	47 58	absidd	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \|\frac{R (n)}{n (n + 1)}\| = \frac{R (n)}{n (n + 1)}$
62	61	sumeq2dv	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} \|\frac{R (n)}{n (n + 1)}\| = \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})$
63	60 62	eqtr4d	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i)) \to \|\sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})\| = \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} \|\frac{R (n)}{n (n + 1)}\|$
64		fzfid	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \to (⌊Y⌋ + 1 \dots ⌊K Y⌋) \in Fin$
65	46	adantlr	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{R (n)}{n (n + 1)} \in ℝ$
66	65	recnd	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{R (n)}{n (n + 1)} \in ℂ$
67	64 66	fsumneg	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (- \frac{R (n)}{n (n + 1)}) = - \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})$
68	43	adantlr	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to R (n) \in ℝ$
69	68	renegcld	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to - R (n) \in ℝ$
70	50	breq1d	$⊢ i = n \to (R (i) \leq 0 \leftrightarrow R (n) \leq 0)$
71	70	rspccva	$⊢ (\forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0 \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to R (n) \leq 0$
72	71	adantll	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to R (n) \leq 0$
73	68	le0neg1d	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (R (n) \leq 0 \leftrightarrow 0 \leq - R (n))$
74	72 73	mpbid	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to 0 \leq - R (n)$
75	45	adantlr	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n (n + 1) \in ℕ$
76	75	nnred	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n (n + 1) \in ℝ$
77	75	nngt0d	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to 0 < n (n + 1)$
78		divge0	$⊢ ((- R (n) \in ℝ \land 0 \leq - R (n)) \land (n (n + 1) \in ℝ \land 0 < n (n + 1))) \to 0 \leq \frac{- R (n)}{n (n + 1)}$
79	69 74 76 77 78	syl22anc	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to 0 \leq \frac{- R (n)}{n (n + 1)}$
80	43	recnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to R (n) \in ℂ$
81	45	nncnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n (n + 1) \in ℂ$
82	45	nnne0d	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n (n + 1) \neq 0$
83	80 81 82	divnegd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to - \frac{R (n)}{n (n + 1)} = \frac{- R (n)}{n (n + 1)}$
84	83	adantlr	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to - \frac{R (n)}{n (n + 1)} = \frac{- R (n)}{n (n + 1)}$
85	79 84	breqtrrd	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to 0 \leq - \frac{R (n)}{n (n + 1)}$
86	65	le0neg1d	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\frac{R (n)}{n (n + 1)} \leq 0 \leftrightarrow 0 \leq - \frac{R (n)}{n (n + 1)})$
87	85 86	mpbird	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{R (n)}{n (n + 1)} \leq 0$
88	65 87	absnidd	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \|\frac{R (n)}{n (n + 1)}\| = - \frac{R (n)}{n (n + 1)}$
89	88	sumeq2dv	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} \|\frac{R (n)}{n (n + 1)}\| = \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (- \frac{R (n)}{n (n + 1)})$
90	64 65	fsumrecl	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)}) \in ℝ$
91	65	renegcld	$⊢ ((φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to - \frac{R (n)}{n (n + 1)} \in ℝ$
92	64 91 85	fsumge0	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \to 0 \leq \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (- \frac{R (n)}{n (n + 1)})$
93	92 67	breqtrd	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \to 0 \leq - \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})$
94	90	le0neg1d	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \to (\sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)}) \leq 0 \leftrightarrow 0 \leq - \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)}))$
95	93 94	mpbird	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)}) \leq 0$
96	90 95	absnidd	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \to \|\sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})\| = - \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})$
97	67 89 96	3eqtr4rd	$⊢ (φ \land \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0) \to \|\sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})\| = \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} \|\frac{R (n)}{n (n + 1)}\|$
98		2rp	$⊢ 2 \in ℝ^{+}$
99		rpaddcl	$⊢ (A \in ℝ^{+} \land 2 \in ℝ^{+}) \to A + 2 \in ℝ^{+}$
100	5 98 99	sylancl	$⊢ φ \to A + 2 \in ℝ^{+}$
101	7 100	eqeltrid	$⊢ φ \to C \in ℝ^{+}$
102	101 20	rpdivcld	$⊢ φ \to \frac{C}{E} \in ℝ^{+}$
103	102	rpred	$⊢ φ \to \frac{C}{E} \in ℝ$
104	103	reefcld	$⊢ φ \to e^{\frac{C}{E}} \in ℝ$
105		pnfxr	$⊢ +∞ \in ℝ^{*}$
106		icossre	$⊢ (e^{\frac{C}{E}} \in ℝ \land +∞ \in ℝ^{*}) \to [e^{\frac{C}{E}}, +∞) \subseteq ℝ$
107	104 105 106	sylancl	$⊢ φ \to [e^{\frac{C}{E}}, +∞) \subseteq ℝ$
108	107 8	sseldd	$⊢ φ \to K \in ℝ$
109	108 12	remulcld	$⊢ φ \to K Y \in ℝ$
110	12	recnd	$⊢ φ \to Y \in ℂ$
111	110	mulid2d	$⊢ φ \to 1 Y = Y$
112		1red	$⊢ φ \to 1 \in ℝ$
113		efgt1	$⊢ \frac{C}{E} \in ℝ^{+} \to 1 < e^{\frac{C}{E}}$
114	102 113	syl	$⊢ φ \to 1 < e^{\frac{C}{E}}$
115		elicopnf	$⊢ e^{\frac{C}{E}} \in ℝ \to (K \in [e^{\frac{C}{E}}, +∞) \leftrightarrow (K \in ℝ \land e^{\frac{C}{E}} \leq K))$
116	104 115	syl	$⊢ φ \to (K \in [e^{\frac{C}{E}}, +∞) \leftrightarrow (K \in ℝ \land e^{\frac{C}{E}} \leq K))$
117	116	simplbda	$⊢ (φ \land K \in [e^{\frac{C}{E}}, +∞)) \to e^{\frac{C}{E}} \leq K$
118	8 117	mpdan	$⊢ φ \to e^{\frac{C}{E}} \leq K$
119	112 104 108 114 118	ltletrd	$⊢ φ \to 1 < K$
120		ltmul1	$⊢ (1 \in ℝ \land K \in ℝ \land (Y \in ℝ \land 0 < Y)) \to (1 < K \leftrightarrow 1 Y < K Y)$
121	112 108 12 31 120	syl112anc	$⊢ φ \to (1 < K \leftrightarrow 1 Y < K Y)$
122	119 121	mpbid	$⊢ φ \to 1 Y < K Y$
123	111 122	eqbrtrrd	$⊢ φ \to Y < K Y$
124	12 109 123	ltled	$⊢ φ \to Y \leq K Y$
125		flword2	$⊢ (Y \in ℝ \land K Y \in ℝ \land Y \leq K Y) \to ⌊K Y⌋ \in ℤ_{\geq ⌊Y⌋}$
126	12 109 124 125	syl3anc	$⊢ φ \to ⌊K Y⌋ \in ℤ_{\geq ⌊Y⌋}$
127	109	flcld	$⊢ φ \to ⌊K Y⌋ \in ℤ$
128		uzid	$⊢ ⌊K Y⌋ \in ℤ \to ⌊K Y⌋ \in ℤ_{\geq ⌊K Y⌋}$
129	127 128	syl	$⊢ φ \to ⌊K Y⌋ \in ℤ_{\geq ⌊K Y⌋}$
130		elfzuzb	$⊢ ⌊K Y⌋ \in (⌊Y⌋ \dots ⌊K Y⌋) \leftrightarrow (⌊K Y⌋ \in ℤ_{\geq ⌊Y⌋} \land ⌊K Y⌋ \in ℤ_{\geq ⌊K Y⌋})$
131	126 129 130	sylanbrc	$⊢ φ \to ⌊K Y⌋ \in (⌊Y⌋ \dots ⌊K Y⌋)$
132		oveq2	$⊢ x = ⌊Y⌋ \to (⌊Y⌋ + 1 \dots x) = (⌊Y⌋ + 1 \dots ⌊Y⌋)$
133	132	raleqdv	$⊢ x = ⌊Y⌋ \to (\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \leftrightarrow \forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) 0 \leq R (i))$
134	132	raleqdv	$⊢ x = ⌊Y⌋ \to (\forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0 \leftrightarrow \forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) R (i) \leq 0)$
135	133 134	orbi12d	$⊢ x = ⌊Y⌋ \to ((\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0) \leftrightarrow (\forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) R (i) \leq 0))$
136	135	imbi2d	$⊢ x = ⌊Y⌋ \to ((φ \to (\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0)) \leftrightarrow (φ \to (\forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) R (i) \leq 0)))$
137		oveq2	$⊢ x = m \to (⌊Y⌋ + 1 \dots x) = (⌊Y⌋ + 1 \dots m)$
138	137	raleqdv	$⊢ x = m \to (\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \leftrightarrow \forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i))$
139	137	raleqdv	$⊢ x = m \to (\forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0 \leftrightarrow \forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0)$
140	138 139	orbi12d	$⊢ x = m \to ((\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0) \leftrightarrow (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0))$
141	140	imbi2d	$⊢ x = m \to ((φ \to (\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0)) \leftrightarrow (φ \to (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0)))$
142		oveq2	$⊢ x = m + 1 \to (⌊Y⌋ + 1 \dots x) = (⌊Y⌋ + 1 \dots m + 1)$
143	142	raleqdv	$⊢ x = m + 1 \to (\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \leftrightarrow \forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i))$
144	142	raleqdv	$⊢ x = m + 1 \to (\forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0 \leftrightarrow \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0)$
145	143 144	orbi12d	$⊢ x = m + 1 \to ((\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0) \leftrightarrow (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0))$
146	145	imbi2d	$⊢ x = m + 1 \to ((φ \to (\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0)) \leftrightarrow (φ \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0)))$
147		oveq2	$⊢ x = ⌊K Y⌋ \to (⌊Y⌋ + 1 \dots x) = (⌊Y⌋ + 1 \dots ⌊K Y⌋)$
148	147	raleqdv	$⊢ x = ⌊K Y⌋ \to (\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \leftrightarrow \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i))$
149	147	raleqdv	$⊢ x = ⌊K Y⌋ \to (\forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0 \leftrightarrow \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0)$
150	148 149	orbi12d	$⊢ x = ⌊K Y⌋ \to ((\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0) \leftrightarrow (\forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0))$
151	150	imbi2d	$⊢ x = ⌊K Y⌋ \to ((φ \to (\forall i \in (⌊Y⌋ + 1 \dots x) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots x) R (i) \leq 0)) \leftrightarrow (φ \to (\forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0)))$
152		elfzle3	$⊢ i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) \to ⌊Y⌋ + 1 \leq ⌊Y⌋$
153		elfzel2	$⊢ i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) \to ⌊Y⌋ \in ℤ$
154	153	zred	$⊢ i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) \to ⌊Y⌋ \in ℝ$
155	154	ltp1d	$⊢ i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) \to ⌊Y⌋ < ⌊Y⌋ + 1$
156		peano2re	$⊢ ⌊Y⌋ \in ℝ \to ⌊Y⌋ + 1 \in ℝ$
157	154 156	syl	$⊢ i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) \to ⌊Y⌋ + 1 \in ℝ$
158	154 157	ltnled	$⊢ i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) \to (⌊Y⌋ < ⌊Y⌋ + 1 \leftrightarrow \neg ⌊Y⌋ + 1 \leq ⌊Y⌋)$
159	155 158	mpbid	$⊢ i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) \to \neg ⌊Y⌋ + 1 \leq ⌊Y⌋$
160	152 159	pm2.21dd	$⊢ i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) \to R (i) \leq 0$
161	160	rgen	$⊢ \forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) R (i) \leq 0$
162	161	olci	$⊢ (\forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) R (i) \leq 0)$
163	162	2a1i	$⊢ ⌊K Y⌋ \in ℤ_{\geq ⌊Y⌋} \to (φ \to (\forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots ⌊Y⌋) R (i) \leq 0))$
164		elfzofz	$⊢ m \in (⌊Y⌋ ..^⌊K Y⌋) \to m \in (⌊Y⌋ \dots ⌊K Y⌋)$
165		elfzp12	$⊢ ⌊K Y⌋ \in ℤ_{\geq ⌊Y⌋} \to (m \in (⌊Y⌋ \dots ⌊K Y⌋) \leftrightarrow (m = ⌊Y⌋ \lor m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)))$
166	126 165	syl	$⊢ φ \to (m \in (⌊Y⌋ \dots ⌊K Y⌋) \leftrightarrow (m = ⌊Y⌋ \lor m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)))$
167	164 166	syl5ib	$⊢ φ \to (m \in (⌊Y⌋ ..^⌊K Y⌋) \to (m = ⌊Y⌋ \lor m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)))$
168	167	imp	$⊢ (φ \land m \in (⌊Y⌋ ..^⌊K Y⌋)) \to (m = ⌊Y⌋ \lor m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋))$
169	36	nnrpd	$⊢ φ \to ⌊Y⌋ + 1 \in ℝ^{+}$
170	41	ffvelrni	$⊢ ⌊Y⌋ + 1 \in ℝ^{+} \to R (⌊Y⌋ + 1) \in ℝ$
171	169 170	syl	$⊢ φ \to R (⌊Y⌋ + 1) \in ℝ$
172	13 171	letrid	$⊢ φ \to (0 \leq R (⌊Y⌋ + 1) \lor R (⌊Y⌋ + 1) \leq 0)$
173	172	adantr	$⊢ (φ \land m = ⌊Y⌋) \to (0 \leq R (⌊Y⌋ + 1) \lor R (⌊Y⌋ + 1) \leq 0)$
174		oveq1	$⊢ m = ⌊Y⌋ \to m + 1 = ⌊Y⌋ + 1$
175	174	oveq2d	$⊢ m = ⌊Y⌋ \to (⌊Y⌋ + 1 \dots m + 1) = (⌊Y⌋ + 1 \dots ⌊Y⌋ + 1)$
176	12	flcld	$⊢ φ \to ⌊Y⌋ \in ℤ$
177	176	peano2zd	$⊢ φ \to ⌊Y⌋ + 1 \in ℤ$
178		fzsn	$⊢ ⌊Y⌋ + 1 \in ℤ \to (⌊Y⌋ + 1 \dots ⌊Y⌋ + 1) = \{⌊Y⌋ + 1\}$
179	177 178	syl	$⊢ φ \to (⌊Y⌋ + 1 \dots ⌊Y⌋ + 1) = \{⌊Y⌋ + 1\}$
180	175 179	sylan9eqr	$⊢ (φ \land m = ⌊Y⌋) \to (⌊Y⌋ + 1 \dots m + 1) = \{⌊Y⌋ + 1\}$
181	180	raleqdv	$⊢ (φ \land m = ⌊Y⌋) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \leftrightarrow \forall i \in \{⌊Y⌋ + 1\} 0 \leq R (i))$
182		ovex	$⊢ ⌊Y⌋ + 1 \in V$
183		fveq2	$⊢ i = ⌊Y⌋ + 1 \to R (i) = R (⌊Y⌋ + 1)$
184	183	breq2d	$⊢ i = ⌊Y⌋ + 1 \to (0 \leq R (i) \leftrightarrow 0 \leq R (⌊Y⌋ + 1))$
185	182 184	ralsn	$⊢ \forall i \in \{⌊Y⌋ + 1\} 0 \leq R (i) \leftrightarrow 0 \leq R (⌊Y⌋ + 1)$
186	181 185	bitrdi	$⊢ (φ \land m = ⌊Y⌋) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \leftrightarrow 0 \leq R (⌊Y⌋ + 1))$
187	180	raleqdv	$⊢ (φ \land m = ⌊Y⌋) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0 \leftrightarrow \forall i \in \{⌊Y⌋ + 1\} R (i) \leq 0)$
188	183	breq1d	$⊢ i = ⌊Y⌋ + 1 \to (R (i) \leq 0 \leftrightarrow R (⌊Y⌋ + 1) \leq 0)$
189	182 188	ralsn	$⊢ \forall i \in \{⌊Y⌋ + 1\} R (i) \leq 0 \leftrightarrow R (⌊Y⌋ + 1) \leq 0$
190	187 189	bitrdi	$⊢ (φ \land m = ⌊Y⌋) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0 \leftrightarrow R (⌊Y⌋ + 1) \leq 0)$
191	186 190	orbi12d	$⊢ (φ \land m = ⌊Y⌋) \to ((\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0) \leftrightarrow (0 \leq R (⌊Y⌋ + 1) \lor R (⌊Y⌋ + 1) \leq 0))$
192	173 191	mpbird	$⊢ (φ \land m = ⌊Y⌋) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0)$
193	192	a1d	$⊢ (φ \land m = ⌊Y⌋) \to ((\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0))$
194		elfzuz	$⊢ m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) \to m \in ℤ_{\geq (⌊Y⌋ + 1)}$
195	194	adantl	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to m \in ℤ_{\geq (⌊Y⌋ + 1)}$
196		eluzfz2	$⊢ m \in ℤ_{\geq (⌊Y⌋ + 1)} \to m \in (⌊Y⌋ + 1 \dots m)$
197	195 196	syl	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to m \in (⌊Y⌋ + 1 \dots m)$
198		fveq2	$⊢ i = m \to R (i) = R (m)$
199	198	breq2d	$⊢ i = m \to (0 \leq R (i) \leftrightarrow 0 \leq R (m))$
200	199	rspcv	$⊢ m \in (⌊Y⌋ + 1 \dots m) \to (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \to 0 \leq R (m))$
201	197 200	syl	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \to 0 \leq R (m))$
202	9	adantr	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \neg \exists y \in ℕ ((Y < y \land y \leq K Y) \land \|\frac{R (y)}{y}\| \leq E)$
203		eluznn	$⊢ (⌊Y⌋ + 1 \in ℕ \land m \in ℤ_{\geq (⌊Y⌋ + 1)}) \to m \in ℕ$
204	36 194 203	syl2an	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to m \in ℕ$
205	204	adantr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land \|R (m)\| \leq \|R (m + 1) - R (m)\|) \to m \in ℕ$
206		elfzle1	$⊢ m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) \to ⌊Y⌋ + 1 \leq m$
207	206	adantl	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to ⌊Y⌋ + 1 \leq m$
208		elfzelz	$⊢ m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) \to m \in ℤ$
209		zltp1le	$⊢ (⌊Y⌋ \in ℤ \land m \in ℤ) \to (⌊Y⌋ < m \leftrightarrow ⌊Y⌋ + 1 \leq m)$
210	176 208 209	syl2an	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (⌊Y⌋ < m \leftrightarrow ⌊Y⌋ + 1 \leq m)$
211	207 210	mpbird	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to ⌊Y⌋ < m$
212		fllt	$⊢ (Y \in ℝ \land m \in ℤ) \to (Y < m \leftrightarrow ⌊Y⌋ < m)$
213	12 208 212	syl2an	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (Y < m \leftrightarrow ⌊Y⌋ < m)$
214	211 213	mpbird	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to Y < m$
215		elfzle2	$⊢ m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) \to m \leq ⌊K Y⌋$
216	215	adantl	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to m \leq ⌊K Y⌋$
217		flge	$⊢ (K Y \in ℝ \land m \in ℤ) \to (m \leq K Y \leftrightarrow m \leq ⌊K Y⌋)$
218	109 208 217	syl2an	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (m \leq K Y \leftrightarrow m \leq ⌊K Y⌋)$
219	216 218	mpbird	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to m \leq K Y$
220	214 219	jca	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (Y < m \land m \leq K Y)$
221	220	adantr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land \|R (m)\| \leq \|R (m + 1) - R (m)\|) \to (Y < m \land m \leq K Y)$
222	2	ad2antrr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land \|R (m)\| \leq \|R (m + 1) - R (m)\|) \to E \in (0, 1)$
223	4	ad2antrr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land \|R (m)\| \leq \|R (m + 1) - R (m)\|) \to Y \in (X, +∞)$
224		simpr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land \|R (m)\| \leq \|R (m + 1) - R (m)\|) \to \|R (m)\| \leq \|R (m + 1) - R (m)\|$
225	1 222 3 223 205 221 224	pntpbnd1a	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land \|R (m)\| \leq \|R (m + 1) - R (m)\|) \to \|\frac{R (m)}{m}\| \leq E$
226		breq2	$⊢ y = m \to (Y < y \leftrightarrow Y < m)$
227		breq1	$⊢ y = m \to (y \leq K Y \leftrightarrow m \leq K Y)$
228	226 227	anbi12d	$⊢ y = m \to ((Y < y \land y \leq K Y) \leftrightarrow (Y < m \land m \leq K Y))$
229		fveq2	$⊢ y = m \to R (y) = R (m)$
230		id	$⊢ y = m \to y = m$
231	229 230	oveq12d	$⊢ y = m \to \frac{R (y)}{y} = \frac{R (m)}{m}$
232	231	fveq2d	$⊢ y = m \to \|\frac{R (y)}{y}\| = \|\frac{R (m)}{m}\|$
233	232	breq1d	$⊢ y = m \to (\|\frac{R (y)}{y}\| \leq E \leftrightarrow \|\frac{R (m)}{m}\| \leq E)$
234	228 233	anbi12d	$⊢ y = m \to (((Y < y \land y \leq K Y) \land \|\frac{R (y)}{y}\| \leq E) \leftrightarrow ((Y < m \land m \leq K Y) \land \|\frac{R (m)}{m}\| \leq E))$
235	234	rspcev	$⊢ (m \in ℕ \land ((Y < m \land m \leq K Y) \land \|\frac{R (m)}{m}\| \leq E)) \to \exists y \in ℕ ((Y < y \land y \leq K Y) \land \|\frac{R (y)}{y}\| \leq E)$
236	205 221 225 235	syl12anc	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land \|R (m)\| \leq \|R (m + 1) - R (m)\|) \to \exists y \in ℕ ((Y < y \land y \leq K Y) \land \|\frac{R (y)}{y}\| \leq E)$
237	202 236	mtand	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \neg \|R (m)\| \leq \|R (m + 1) - R (m)\|$
238	237	adantr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land 0 \leq R (m)) \to \neg \|R (m)\| \leq \|R (m + 1) - R (m)\|$
239	204	nnrpd	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to m \in ℝ^{+}$
240	41	ffvelrni	$⊢ m \in ℝ^{+} \to R (m) \in ℝ$
241	239 240	syl	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to R (m) \in ℝ$
242	241	adantr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to R (m) \in ℝ$
243	242	recnd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to R (m) \in ℂ$
244	243	subid1d	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to R (m) - 0 = R (m)$
245	204	peano2nnd	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to m + 1 \in ℕ$
246	245	nnrpd	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to m + 1 \in ℝ^{+}$
247	41	ffvelrni	$⊢ m + 1 \in ℝ^{+} \to R (m + 1) \in ℝ$
248	246 247	syl	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to R (m + 1) \in ℝ$
249	248	adantr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to R (m + 1) \in ℝ$
250		0red	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to 0 \in ℝ$
251		0re	$⊢ 0 \in ℝ$
252		letric	$⊢ (0 \in ℝ \land R (m + 1) \in ℝ) \to (0 \leq R (m + 1) \lor R (m + 1) \leq 0)$
253	251 248 252	sylancr	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (0 \leq R (m + 1) \lor R (m + 1) \leq 0)$
254	253	ord	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\neg 0 \leq R (m + 1) \to R (m + 1) \leq 0)$
255	254	imp	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land \neg 0 \leq R (m + 1)) \to R (m + 1) \leq 0$
256	255	adantrl	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to R (m + 1) \leq 0$
257	249 250 242 256	lesub2dd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to R (m) - 0 \leq R (m) - R (m + 1)$
258	244 257	eqbrtrrd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to R (m) \leq R (m) - R (m + 1)$
259		simprl	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to 0 \leq R (m)$
260	242 259	absidd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to \|R (m)\| = R (m)$
261	249 250 242 256 259	letrd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to R (m + 1) \leq R (m)$
262	249 242 261	abssuble0d	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to \|R (m + 1) - R (m)\| = R (m) - R (m + 1)$
263	258 260 262	3brtr4d	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (0 \leq R (m) \land \neg 0 \leq R (m + 1))) \to \|R (m)\| \leq \|R (m + 1) - R (m)\|$
264	263	expr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land 0 \leq R (m)) \to (\neg 0 \leq R (m + 1) \to \|R (m)\| \leq \|R (m + 1) - R (m)\|)$
265	238 264	mt3d	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land 0 \leq R (m)) \to 0 \leq R (m + 1)$
266	265	ex	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (0 \leq R (m) \to 0 \leq R (m + 1))$
267	201 266	syld	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \to 0 \leq R (m + 1))$
268		ovex	$⊢ m + 1 \in V$
269		fveq2	$⊢ i = m + 1 \to R (i) = R (m + 1)$
270	269	breq2d	$⊢ i = m + 1 \to (0 \leq R (i) \leftrightarrow 0 \leq R (m + 1))$
271	268 270	ralsn	$⊢ \forall i \in \{m + 1\} 0 \leq R (i) \leftrightarrow 0 \leq R (m + 1)$
272	267 271	syl6ibr	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \to \forall i \in \{m + 1\} 0 \leq R (i))$
273	272	ancld	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \to (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \land \forall i \in \{m + 1\} 0 \leq R (i)))$
274		fzsuc	$⊢ m \in ℤ_{\geq (⌊Y⌋ + 1)} \to (⌊Y⌋ + 1 \dots m + 1) = (⌊Y⌋ + 1 \dots m) \cup \{m + 1\}$
275	195 274	syl	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (⌊Y⌋ + 1 \dots m + 1) = (⌊Y⌋ + 1 \dots m) \cup \{m + 1\}$
276	275	raleqdv	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \leftrightarrow \forall i \in ((⌊Y⌋ + 1 \dots m) \cup \{m + 1\}) 0 \leq R (i))$
277		ralunb	$⊢ \forall i \in ((⌊Y⌋ + 1 \dots m) \cup \{m + 1\}) 0 \leq R (i) \leftrightarrow (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \land \forall i \in \{m + 1\} 0 \leq R (i))$
278	276 277	bitrdi	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \leftrightarrow (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \land \forall i \in \{m + 1\} 0 \leq R (i)))$
279	273 278	sylibrd	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \to \forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i))$
280	198	breq1d	$⊢ i = m \to (R (i) \leq 0 \leftrightarrow R (m) \leq 0)$
281	280	rspcv	$⊢ m \in (⌊Y⌋ + 1 \dots m) \to (\forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0 \to R (m) \leq 0)$
282	197 281	syl	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0 \to R (m) \leq 0)$
283	237	adantr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land R (m) \leq 0) \to \neg \|R (m)\| \leq \|R (m + 1) - R (m)\|$
284	254	con1d	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\neg R (m + 1) \leq 0 \to 0 \leq R (m + 1))$
285	284	imp	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land \neg R (m + 1) \leq 0) \to 0 \leq R (m + 1)$
286	285	adantrl	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to 0 \leq R (m + 1)$
287	241	adantr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to R (m) \in ℝ$
288	287	renegcld	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to - R (m) \in ℝ$
289	248	adantr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to R (m + 1) \in ℝ$
290	288 289	addge02d	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to (0 \leq R (m + 1) \leftrightarrow - R (m) \leq R (m + 1) + (- R (m)))$
291	286 290	mpbid	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to - R (m) \leq R (m + 1) + (- R (m))$
292	289	recnd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to R (m + 1) \in ℂ$
293	287	recnd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to R (m) \in ℂ$
294	292 293	negsubd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to R (m + 1) + (- R (m)) = R (m + 1) - R (m)$
295	291 294	breqtrd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to - R (m) \leq R (m + 1) - R (m)$
296		simprl	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to R (m) \leq 0$
297	287 296	absnidd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to \|R (m)\| = - R (m)$
298		0red	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to 0 \in ℝ$
299	287 298 289 296 286	letrd	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to R (m) \leq R (m + 1)$
300	287 289 299	abssubge0d	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to \|R (m + 1) - R (m)\| = R (m + 1) - R (m)$
301	295 297 300	3brtr4d	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land (R (m) \leq 0 \land \neg R (m + 1) \leq 0)) \to \|R (m)\| \leq \|R (m + 1) - R (m)\|$
302	301	expr	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land R (m) \leq 0) \to (\neg R (m + 1) \leq 0 \to \|R (m)\| \leq \|R (m + 1) - R (m)\|)$
303	283 302	mt3d	$⊢ ((φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \land R (m) \leq 0) \to R (m + 1) \leq 0$
304	303	ex	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (R (m) \leq 0 \to R (m + 1) \leq 0)$
305	282 304	syld	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0 \to R (m + 1) \leq 0)$
306	269	breq1d	$⊢ i = m + 1 \to (R (i) \leq 0 \leftrightarrow R (m + 1) \leq 0)$
307	268 306	ralsn	$⊢ \forall i \in \{m + 1\} R (i) \leq 0 \leftrightarrow R (m + 1) \leq 0$
308	305 307	syl6ibr	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0 \to \forall i \in \{m + 1\} R (i) \leq 0)$
309	308	ancld	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0 \to (\forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0 \land \forall i \in \{m + 1\} R (i) \leq 0))$
310	275	raleqdv	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0 \leftrightarrow \forall i \in ((⌊Y⌋ + 1 \dots m) \cup \{m + 1\}) R (i) \leq 0)$
311		ralunb	$⊢ \forall i \in ((⌊Y⌋ + 1 \dots m) \cup \{m + 1\}) R (i) \leq 0 \leftrightarrow (\forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0 \land \forall i \in \{m + 1\} R (i) \leq 0)$
312	310 311	bitrdi	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0 \leftrightarrow (\forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0 \land \forall i \in \{m + 1\} R (i) \leq 0))$
313	309 312	sylibrd	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0 \to \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0)$
314	279 313	orim12d	$⊢ (φ \land m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to ((\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0))$
315	193 314	jaodan	$⊢ (φ \land (m = ⌊Y⌋ \lor m \in (⌊Y⌋ + 1 \dots ⌊K Y⌋))) \to ((\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0))$
316	168 315	syldan	$⊢ (φ \land m \in (⌊Y⌋ ..^⌊K Y⌋)) \to ((\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0))$
317	316	expcom	$⊢ m \in (⌊Y⌋ ..^⌊K Y⌋) \to (φ \to ((\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0) \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0)))$
318	317	a2d	$⊢ m \in (⌊Y⌋ ..^⌊K Y⌋) \to ((φ \to (\forall i \in (⌊Y⌋ + 1 \dots m) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m) R (i) \leq 0)) \to (φ \to (\forall i \in (⌊Y⌋ + 1 \dots m + 1) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots m + 1) R (i) \leq 0)))$
319	136 141 146 151 163 318	fzind2	$⊢ ⌊K Y⌋ \in (⌊Y⌋ \dots ⌊K Y⌋) \to (φ \to (\forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0))$
320	131 319	mpcom	$⊢ φ \to (\forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) 0 \leq R (i) \lor \forall i \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) R (i) \leq 0)$
321	63 97 320	mpjaodan	$⊢ φ \to \|\sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})\| = \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} \|\frac{R (n)}{n (n + 1)}\|$
322		fveq2	$⊢ y = n \to R (y) = R (n)$
323		id	$⊢ y = n \to y = n$
324		oveq1	$⊢ y = n \to y + 1 = n + 1$
325	323 324	oveq12d	$⊢ y = n \to y (y + 1) = n (n + 1)$
326	322 325	oveq12d	$⊢ y = n \to \frac{R (y)}{y (y + 1)} = \frac{R (n)}{n (n + 1)}$
327	326	cbvsumv	$⊢ \sum_{y = i}^{j} (\frac{R (y)}{y (y + 1)}) = \sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)})$
328		oveq1	$⊢ i = ⌊Y⌋ + 1 \to (i \dots j) = (⌊Y⌋ + 1 \dots j)$
329	328	sumeq1d	$⊢ i = ⌊Y⌋ + 1 \to \sum_{n = i}^{j} (\frac{R (n)}{n (n + 1)}) = \sum_{n = ⌊Y⌋ + 1}^{j} (\frac{R (n)}{n (n + 1)})$
330	327 329	syl5eq	$⊢ i = ⌊Y⌋ + 1 \to \sum_{y = i}^{j} (\frac{R (y)}{y (y + 1)}) = \sum_{n = ⌊Y⌋ + 1}^{j} (\frac{R (n)}{n (n + 1)})$
331	330	fveq2d	$⊢ i = ⌊Y⌋ + 1 \to \|\sum_{y = i}^{j} (\frac{R (y)}{y (y + 1)})\| = \|\sum_{n = ⌊Y⌋ + 1}^{j} (\frac{R (n)}{n (n + 1)})\|$
332	331	breq1d	$⊢ i = ⌊Y⌋ + 1 \to (\|\sum_{y = i}^{j} (\frac{R (y)}{y (y + 1)})\| \leq A \leftrightarrow \|\sum_{n = ⌊Y⌋ + 1}^{j} (\frac{R (n)}{n (n + 1)})\| \leq A)$
333		oveq2	$⊢ j = ⌊K Y⌋ \to (⌊Y⌋ + 1 \dots j) = (⌊Y⌋ + 1 \dots ⌊K Y⌋)$
334	333	sumeq1d	$⊢ j = ⌊K Y⌋ \to \sum_{n = ⌊Y⌋ + 1}^{j} (\frac{R (n)}{n (n + 1)}) = \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})$
335	334	fveq2d	$⊢ j = ⌊K Y⌋ \to \|\sum_{n = ⌊Y⌋ + 1}^{j} (\frac{R (n)}{n (n + 1)})\| = \|\sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})\|$
336	335	breq1d	$⊢ j = ⌊K Y⌋ \to (\|\sum_{n = ⌊Y⌋ + 1}^{j} (\frac{R (n)}{n (n + 1)})\| \leq A \leftrightarrow \|\sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})\| \leq A)$
337	332 336	rspc2va	$⊢ ((⌊Y⌋ + 1 \in ℕ \land ⌊K Y⌋ \in ℤ) \land \forall i \in ℕ \forall j \in ℤ \|\sum_{y = i}^{j} (\frac{R (y)}{y (y + 1)})\| \leq A) \to \|\sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})\| \leq A$
338	36 127 6 337	syl21anc	$⊢ φ \to \|\sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{R (n)}{n (n + 1)})\| \leq A$
339	321 338	eqbrtrrd	$⊢ φ \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} \|\frac{R (n)}{n (n + 1)}\| \leq A$

Metamath Proof Explorer

Theorem pntpbnd1

Proof