pntpbnd2

	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	pntpbnd2	$⊢ \neg φ$

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		2div2e1	$⊢ \frac{2}{2} = 1$
11		2re	$⊢ 2 \in ℝ$
12	11	a1i	$⊢ φ \to 2 \in ℝ$
13		ioossre	$⊢ (0, 1) \subseteq ℝ$
14	13 2	sselid	$⊢ φ \to E \in ℝ$
15		eliooord	$⊢ E \in (0, 1) \to (0 < E \land E < 1)$
16	2 15	syl	$⊢ φ \to (0 < E \land E < 1)$
17	16	simpld	$⊢ φ \to 0 < E$
18	14 17	elrpd	$⊢ φ \to E \in ℝ^{+}$
19		2rp	$⊢ 2 \in ℝ^{+}$
20	19	a1i	$⊢ φ \to 2 \in ℝ^{+}$
21	7	oveq1i	$⊢ C - A = A + 2 - A$
22	5	rpcnd	$⊢ φ \to A \in ℂ$
23		2cn	$⊢ 2 \in ℂ$
24		pncan2	$⊢ (A \in ℂ \land 2 \in ℂ) \to A + 2 - A = 2$
25	22 23 24	sylancl	$⊢ φ \to A + 2 - A = 2$
26	21 25	eqtrid	$⊢ φ \to C - A = 2$
27	26	oveq1d	$⊢ φ \to \frac{C - A}{E} = \frac{2}{E}$
28		rpaddcl	$⊢ (A \in ℝ^{+} \land 2 \in ℝ^{+}) \to A + 2 \in ℝ^{+}$
29	5 19 28	sylancl	$⊢ φ \to A + 2 \in ℝ^{+}$
30	7 29	eqeltrid	$⊢ φ \to C \in ℝ^{+}$
31	30	rpcnd	$⊢ φ \to C \in ℂ$
32	14	recnd	$⊢ φ \to E \in ℂ$
33	18	rpne0d	$⊢ φ \to E \neq 0$
34	31 22 32 33	divsubdird	$⊢ φ \to \frac{C - A}{E} = (\frac{C}{E}) - (\frac{A}{E})$
35	27 34	eqtr3d	$⊢ φ \to \frac{2}{E} = (\frac{C}{E}) - (\frac{A}{E})$
36	30 18	rpdivcld	$⊢ φ \to \frac{C}{E} \in ℝ^{+}$
37	36	rpred	$⊢ φ \to \frac{C}{E} \in ℝ$
38	5	rpred	$⊢ φ \to A \in ℝ$
39	38 18	rerpdivcld	$⊢ φ \to \frac{A}{E} \in ℝ$
40		resubcl	$⊢ (\frac{C}{E} \in ℝ \land 2 \in ℝ) \to (\frac{C}{E}) - 2 \in ℝ$
41	37 11 40	sylancl	$⊢ φ \to (\frac{C}{E}) - 2 \in ℝ$
42	37	reefcld	$⊢ φ \to e^{\frac{C}{E}} \in ℝ$
43		elicopnf	$⊢ e^{\frac{C}{E}} \in ℝ \to (K \in [e^{\frac{C}{E}}, +∞) \leftrightarrow (K \in ℝ \land e^{\frac{C}{E}} \leq K))$
44	42 43	syl	$⊢ φ \to (K \in [e^{\frac{C}{E}}, +∞) \leftrightarrow (K \in ℝ \land e^{\frac{C}{E}} \leq K))$
45	8 44	mpbid	$⊢ φ \to (K \in ℝ \land e^{\frac{C}{E}} \leq K)$
46	45	simpld	$⊢ φ \to K \in ℝ$
47		0red	$⊢ φ \to 0 \in ℝ$
48		1re	$⊢ 1 \in ℝ$
49	48	a1i	$⊢ φ \to 1 \in ℝ$
50		0lt1	$⊢ 0 < 1$
51	50	a1i	$⊢ φ \to 0 < 1$
52		efgt1	$⊢ \frac{C}{E} \in ℝ^{+} \to 1 < e^{\frac{C}{E}}$
53	36 52	syl	$⊢ φ \to 1 < e^{\frac{C}{E}}$
54	45	simprd	$⊢ φ \to e^{\frac{C}{E}} \leq K$
55	49 42 46 53 54	ltletrd	$⊢ φ \to 1 < K$
56	47 49 46 51 55	lttrd	$⊢ φ \to 0 < K$
57	46 56	elrpd	$⊢ φ \to K \in ℝ^{+}$
58	57	relogcld	$⊢ φ \to \log K \in ℝ$
59		resubcl	$⊢ (\log K \in ℝ \land 2 \in ℝ) \to \log K - 2 \in ℝ$
60	58 11 59	sylancl	$⊢ φ \to \log K - 2 \in ℝ$
61	57	reeflogd	$⊢ φ \to e^{\log K} = K$
62	54 61	breqtrrd	$⊢ φ \to e^{\frac{C}{E}} \leq e^{\log K}$
63		efle	$⊢ (\frac{C}{E} \in ℝ \land \log K \in ℝ) \to (\frac{C}{E} \leq \log K \leftrightarrow e^{\frac{C}{E}} \leq e^{\log K})$
64	37 58 63	syl2anc	$⊢ φ \to (\frac{C}{E} \leq \log K \leftrightarrow e^{\frac{C}{E}} \leq e^{\log K})$
65	62 64	mpbird	$⊢ φ \to \frac{C}{E} \leq \log K$
66	37 58 12 65	lesub1dd	$⊢ φ \to (\frac{C}{E}) - 2 \leq \log K - 2$
67		fzfid	$⊢ φ \to (⌊Y⌋ + 1 \dots ⌊K Y⌋) \in Fin$
68		ioossre	$⊢ (X, +∞) \subseteq ℝ$
69	68 4	sselid	$⊢ φ \to Y \in ℝ$
70		rerpdivcl	$⊢ (2 \in ℝ \land E \in ℝ^{+}) \to \frac{2}{E} \in ℝ$
71	11 18 70	sylancr	$⊢ φ \to \frac{2}{E} \in ℝ$
72	71	reefcld	$⊢ φ \to e^{\frac{2}{E}} \in ℝ$
73	3 72	eqeltrid	$⊢ φ \to X \in ℝ$
74		efgt0	$⊢ \frac{2}{E} \in ℝ \to 0 < e^{\frac{2}{E}}$
75	71 74	syl	$⊢ φ \to 0 < e^{\frac{2}{E}}$
76	75 3	breqtrrdi	$⊢ φ \to 0 < X$
77	73	rexrd	$⊢ φ \to X \in ℝ^{*}$
78		elioopnf	$⊢ X \in ℝ^{*} \to (Y \in (X, +∞) \leftrightarrow (Y \in ℝ \land X < Y))$
79	77 78	syl	$⊢ φ \to (Y \in (X, +∞) \leftrightarrow (Y \in ℝ \land X < Y))$
80	4 79	mpbid	$⊢ φ \to (Y \in ℝ \land X < Y)$
81	80	simprd	$⊢ φ \to X < Y$
82	47 73 69 76 81	lttrd	$⊢ φ \to 0 < Y$
83	47 69 82	ltled	$⊢ φ \to 0 \leq Y$
84		flge0nn0	$⊢ (Y \in ℝ \land 0 \leq Y) \to ⌊Y⌋ \in ℕ_{0}$
85	69 83 84	syl2anc	$⊢ φ \to ⌊Y⌋ \in ℕ_{0}$
86		nn0p1nn	$⊢ ⌊Y⌋ \in ℕ_{0} \to ⌊Y⌋ + 1 \in ℕ$
87	85 86	syl	$⊢ φ \to ⌊Y⌋ + 1 \in ℕ$
88		elfzuz	$⊢ n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) \to n \in ℤ_{\geq (⌊Y⌋ + 1)}$
89		eluznn	$⊢ (⌊Y⌋ + 1 \in ℕ \land n \in ℤ_{\geq (⌊Y⌋ + 1)}) \to n \in ℕ$
90	87 88 89	syl2an	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n \in ℕ$
91	90	peano2nnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n + 1 \in ℕ$
92	91	nnrecred	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{1}{n + 1} \in ℝ$
93	67 92	fsumrecl	$⊢ φ \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}) \in ℝ$
94	58	recnd	$⊢ φ \to \log K \in ℂ$
95		2cnd	$⊢ φ \to 2 \in ℂ$
96	69 82	elrpd	$⊢ φ \to Y \in ℝ^{+}$
97	96	relogcld	$⊢ φ \to \log Y \in ℝ$
98	97	recnd	$⊢ φ \to \log Y \in ℂ$
99	94 95 98	pnpcan2d	$⊢ φ \to \log K + \log Y - (2 + \log Y) = \log K - 2$
100	57 96	relogmuld	$⊢ φ \to \log K Y = \log K + \log Y$
101	58 97	readdcld	$⊢ φ \to \log K + \log Y \in ℝ$
102	100 101	eqeltrd	$⊢ φ \to \log K Y \in ℝ$
103		fzfid	$⊢ φ \to (0 \dots ⌊Y⌋) \in Fin$
104		elfznn0	$⊢ n \in (0 \dots ⌊Y⌋) \to n \in ℕ_{0}$
105	104	adantl	$⊢ (φ \land n \in (0 \dots ⌊Y⌋)) \to n \in ℕ_{0}$
106		nn0p1nn	$⊢ n \in ℕ_{0} \to n + 1 \in ℕ$
107	105 106	syl	$⊢ (φ \land n \in (0 \dots ⌊Y⌋)) \to n + 1 \in ℕ$
108	107	nnrecred	$⊢ (φ \land n \in (0 \dots ⌊Y⌋)) \to \frac{1}{n + 1} \in ℝ$
109	103 108	fsumrecl	$⊢ φ \to \sum_{n = 0}^{⌊Y⌋} (\frac{1}{n + 1}) \in ℝ$
110	109 93	readdcld	$⊢ φ \to \sum_{n = 0}^{⌊Y⌋} (\frac{1}{n + 1}) + \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}) \in ℝ$
111		readdcl	$⊢ (2 \in ℝ \land \log Y \in ℝ) \to 2 + \log Y \in ℝ$
112	11 97 111	sylancr	$⊢ φ \to 2 + \log Y \in ℝ$
113	112 93	readdcld	$⊢ φ \to 2 + \log Y + \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}) \in ℝ$
114	46 69	remulcld	$⊢ φ \to K Y \in ℝ$
115	69	recnd	$⊢ φ \to Y \in ℂ$
116	115	mulid2d	$⊢ φ \to 1 Y = Y$
117	49 46 55	ltled	$⊢ φ \to 1 \leq K$
118		lemul1	$⊢ (1 \in ℝ \land K \in ℝ \land (Y \in ℝ \land 0 < Y)) \to (1 \leq K \leftrightarrow 1 Y \leq K Y)$
119	49 46 69 82 118	syl112anc	$⊢ φ \to (1 \leq K \leftrightarrow 1 Y \leq K Y)$
120	117 119	mpbid	$⊢ φ \to 1 Y \leq K Y$
121	116 120	eqbrtrrd	$⊢ φ \to Y \leq K Y$
122	47 69 114 83 121	letrd	$⊢ φ \to 0 \leq K Y$
123		flge0nn0	$⊢ (K Y \in ℝ \land 0 \leq K Y) \to ⌊K Y⌋ \in ℕ_{0}$
124	114 122 123	syl2anc	$⊢ φ \to ⌊K Y⌋ \in ℕ_{0}$
125		nn0p1nn	$⊢ ⌊K Y⌋ \in ℕ_{0} \to ⌊K Y⌋ + 1 \in ℕ$
126	124 125	syl	$⊢ φ \to ⌊K Y⌋ + 1 \in ℕ$
127	126	nnrpd	$⊢ φ \to ⌊K Y⌋ + 1 \in ℝ^{+}$
128	127	relogcld	$⊢ φ \to \log (⌊K Y⌋ + 1) \in ℝ$
129		1zzd	$⊢ φ \to 1 \in ℤ$
130	114	flcld	$⊢ φ \to ⌊K Y⌋ \in ℤ$
131	130	peano2zd	$⊢ φ \to ⌊K Y⌋ + 1 \in ℤ$
132		elfznn	$⊢ k \in (1 \dots ⌊K Y⌋ + 1) \to k \in ℕ$
133	132	adantl	$⊢ (φ \land k \in (1 \dots ⌊K Y⌋ + 1)) \to k \in ℕ$
134		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
135	134	recnd	$⊢ k \in ℕ \to \frac{1}{k} \in ℂ$
136	133 135	syl	$⊢ (φ \land k \in (1 \dots ⌊K Y⌋ + 1)) \to \frac{1}{k} \in ℂ$
137		oveq2	$⊢ k = n + 1 \to \frac{1}{k} = \frac{1}{n + 1}$
138	129 129 131 136 137	fsumshftm	$⊢ φ \to \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) = \sum_{n = 1 - 1}^{⌊K Y⌋ + 1 - 1} (\frac{1}{n + 1})$
139		1m1e0	$⊢ 1 - 1 = 0$
140	139	a1i	$⊢ φ \to 1 - 1 = 0$
141	130	zcnd	$⊢ φ \to ⌊K Y⌋ \in ℂ$
142		ax-1cn	$⊢ 1 \in ℂ$
143		pncan	$⊢ (⌊K Y⌋ \in ℂ \land 1 \in ℂ) \to ⌊K Y⌋ + 1 - 1 = ⌊K Y⌋$
144	141 142 143	sylancl	$⊢ φ \to ⌊K Y⌋ + 1 - 1 = ⌊K Y⌋$
145	140 144	oveq12d	$⊢ φ \to (1 - 1 \dots ⌊K Y⌋ + 1 - 1) = (0 \dots ⌊K Y⌋)$
146	145	sumeq1d	$⊢ φ \to \sum_{n = 1 - 1}^{⌊K Y⌋ + 1 - 1} (\frac{1}{n + 1}) = \sum_{n = 0}^{⌊K Y⌋} (\frac{1}{n + 1})$
147		reflcl	$⊢ Y \in ℝ \to ⌊Y⌋ \in ℝ$
148	69 147	syl	$⊢ φ \to ⌊Y⌋ \in ℝ$
149	148	ltp1d	$⊢ φ \to ⌊Y⌋ < ⌊Y⌋ + 1$
150		fzdisj	$⊢ ⌊Y⌋ < ⌊Y⌋ + 1 \to (0 \dots ⌊Y⌋) \cap (⌊Y⌋ + 1 \dots ⌊K Y⌋) = \emptyset$
151	149 150	syl	$⊢ φ \to (0 \dots ⌊Y⌋) \cap (⌊Y⌋ + 1 \dots ⌊K Y⌋) = \emptyset$
152		flwordi	$⊢ (Y \in ℝ \land K Y \in ℝ \land Y \leq K Y) \to ⌊Y⌋ \leq ⌊K Y⌋$
153	69 114 121 152	syl3anc	$⊢ φ \to ⌊Y⌋ \leq ⌊K Y⌋$
154		elfz2nn0	$⊢ ⌊Y⌋ \in (0 \dots ⌊K Y⌋) \leftrightarrow (⌊Y⌋ \in ℕ_{0} \land ⌊K Y⌋ \in ℕ_{0} \land ⌊Y⌋ \leq ⌊K Y⌋)$
155	85 124 153 154	syl3anbrc	$⊢ φ \to ⌊Y⌋ \in (0 \dots ⌊K Y⌋)$
156		fzsplit	$⊢ ⌊Y⌋ \in (0 \dots ⌊K Y⌋) \to (0 \dots ⌊K Y⌋) = (0 \dots ⌊Y⌋) \cup (⌊Y⌋ + 1 \dots ⌊K Y⌋)$
157	155 156	syl	$⊢ φ \to (0 \dots ⌊K Y⌋) = (0 \dots ⌊Y⌋) \cup (⌊Y⌋ + 1 \dots ⌊K Y⌋)$
158		fzfid	$⊢ φ \to (0 \dots ⌊K Y⌋) \in Fin$
159		elfznn0	$⊢ n \in (0 \dots ⌊K Y⌋) \to n \in ℕ_{0}$
160	159	adantl	$⊢ (φ \land n \in (0 \dots ⌊K Y⌋)) \to n \in ℕ_{0}$
161	160 106	syl	$⊢ (φ \land n \in (0 \dots ⌊K Y⌋)) \to n + 1 \in ℕ$
162	161	nnrecred	$⊢ (φ \land n \in (0 \dots ⌊K Y⌋)) \to \frac{1}{n + 1} \in ℝ$
163	162	recnd	$⊢ (φ \land n \in (0 \dots ⌊K Y⌋)) \to \frac{1}{n + 1} \in ℂ$
164	151 157 158 163	fsumsplit	$⊢ φ \to \sum_{n = 0}^{⌊K Y⌋} (\frac{1}{n + 1}) = \sum_{n = 0}^{⌊Y⌋} (\frac{1}{n + 1}) + \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1})$
165	138 146 164	3eqtrd	$⊢ φ \to \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) = \sum_{n = 0}^{⌊Y⌋} (\frac{1}{n + 1}) + \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1})$
166	165 110	eqeltrd	$⊢ φ \to \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) \in ℝ$
167		fllep1	$⊢ K Y \in ℝ \to K Y \leq ⌊K Y⌋ + 1$
168	114 167	syl	$⊢ φ \to K Y \leq ⌊K Y⌋ + 1$
169	57 96	rpmulcld	$⊢ φ \to K Y \in ℝ^{+}$
170	169 127	logled	$⊢ φ \to (K Y \leq ⌊K Y⌋ + 1 \leftrightarrow \log K Y \leq \log (⌊K Y⌋ + 1))$
171	168 170	mpbid	$⊢ φ \to \log K Y \leq \log (⌊K Y⌋ + 1)$
172		emre	$⊢ γ \in ℝ$
173	172	a1i	$⊢ φ \to γ \in ℝ$
174	166 128	resubcld	$⊢ φ \to \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1) \in ℝ$
175		0re	$⊢ 0 \in ℝ$
176		emgt0	$⊢ 0 < γ$
177	175 172 176	ltleii	$⊢ 0 \leq γ$
178	177	a1i	$⊢ φ \to 0 \leq γ$
179		harmonicbnd	$⊢ ⌊K Y⌋ + 1 \in ℕ \to \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1) \in [γ, 1]$
180	126 179	syl	$⊢ φ \to \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1) \in [γ, 1]$
181	172 48	elicc2i	$⊢ \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1) \in [γ, 1] \leftrightarrow (\sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1) \in ℝ \land γ \leq \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1) \land \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1) \leq 1)$
182	181	simp2bi	$⊢ \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1) \in [γ, 1] \to γ \leq \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1)$
183	180 182	syl	$⊢ φ \to γ \leq \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1)$
184	47 173 174 178 183	letrd	$⊢ φ \to 0 \leq \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1)$
185	166 128	subge0d	$⊢ φ \to (0 \leq \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}) - \log (⌊K Y⌋ + 1) \leftrightarrow \log (⌊K Y⌋ + 1) \leq \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k}))$
186	184 185	mpbid	$⊢ φ \to \log (⌊K Y⌋ + 1) \leq \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k})$
187	102 128 166 171 186	letrd	$⊢ φ \to \log K Y \leq \sum_{k = 1}^{⌊K Y⌋ + 1} (\frac{1}{k})$
188	187 165	breqtrd	$⊢ φ \to \log K Y \leq \sum_{n = 0}^{⌊Y⌋} (\frac{1}{n + 1}) + \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1})$
189	69	flcld	$⊢ φ \to ⌊Y⌋ \in ℤ$
190	189	peano2zd	$⊢ φ \to ⌊Y⌋ + 1 \in ℤ$
191		elfznn	$⊢ k \in (1 \dots ⌊Y⌋ + 1) \to k \in ℕ$
192	191	adantl	$⊢ (φ \land k \in (1 \dots ⌊Y⌋ + 1)) \to k \in ℕ$
193	192 135	syl	$⊢ (φ \land k \in (1 \dots ⌊Y⌋ + 1)) \to \frac{1}{k} \in ℂ$
194	129 129 190 193 137	fsumshftm	$⊢ φ \to \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) = \sum_{n = 1 - 1}^{⌊Y⌋ + 1 - 1} (\frac{1}{n + 1})$
195	148	recnd	$⊢ φ \to ⌊Y⌋ \in ℂ$
196		pncan	$⊢ (⌊Y⌋ \in ℂ \land 1 \in ℂ) \to ⌊Y⌋ + 1 - 1 = ⌊Y⌋$
197	195 142 196	sylancl	$⊢ φ \to ⌊Y⌋ + 1 - 1 = ⌊Y⌋$
198	140 197	oveq12d	$⊢ φ \to (1 - 1 \dots ⌊Y⌋ + 1 - 1) = (0 \dots ⌊Y⌋)$
199	198	sumeq1d	$⊢ φ \to \sum_{n = 1 - 1}^{⌊Y⌋ + 1 - 1} (\frac{1}{n + 1}) = \sum_{n = 0}^{⌊Y⌋} (\frac{1}{n + 1})$
200	194 199	eqtrd	$⊢ φ \to \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) = \sum_{n = 0}^{⌊Y⌋} (\frac{1}{n + 1})$
201	200 109	eqeltrd	$⊢ φ \to \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) \in ℝ$
202	87	nnrpd	$⊢ φ \to ⌊Y⌋ + 1 \in ℝ^{+}$
203	202	relogcld	$⊢ φ \to \log (⌊Y⌋ + 1) \in ℝ$
204		readdcl	$⊢ (1 \in ℝ \land \log (⌊Y⌋ + 1) \in ℝ) \to 1 + \log (⌊Y⌋ + 1) \in ℝ$
205	48 203 204	sylancr	$⊢ φ \to 1 + \log (⌊Y⌋ + 1) \in ℝ$
206		harmonicbnd	$⊢ ⌊Y⌋ + 1 \in ℕ \to \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) - \log (⌊Y⌋ + 1) \in [γ, 1]$
207	87 206	syl	$⊢ φ \to \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) - \log (⌊Y⌋ + 1) \in [γ, 1]$
208	172 48	elicc2i	$⊢ \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) - \log (⌊Y⌋ + 1) \in [γ, 1] \leftrightarrow (\sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) - \log (⌊Y⌋ + 1) \in ℝ \land γ \leq \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) - \log (⌊Y⌋ + 1) \land \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) - \log (⌊Y⌋ + 1) \leq 1)$
209	208	simp3bi	$⊢ \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) - \log (⌊Y⌋ + 1) \in [γ, 1] \to \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) - \log (⌊Y⌋ + 1) \leq 1$
210	207 209	syl	$⊢ φ \to \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) - \log (⌊Y⌋ + 1) \leq 1$
211	201 203 49	lesubaddd	$⊢ φ \to (\sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) - \log (⌊Y⌋ + 1) \leq 1 \leftrightarrow \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) \leq 1 + \log (⌊Y⌋ + 1))$
212	210 211	mpbid	$⊢ φ \to \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) \leq 1 + \log (⌊Y⌋ + 1)$
213		readdcl	$⊢ (1 \in ℝ \land \log Y \in ℝ) \to 1 + \log Y \in ℝ$
214	48 97 213	sylancr	$⊢ φ \to 1 + \log Y \in ℝ$
215		peano2re	$⊢ ⌊Y⌋ \in ℝ \to ⌊Y⌋ + 1 \in ℝ$
216	148 215	syl	$⊢ φ \to ⌊Y⌋ + 1 \in ℝ$
217	12 69	remulcld	$⊢ φ \to 2 Y \in ℝ$
218		epr	$⊢ e \in ℝ^{+}$
219		rpmulcl	$⊢ (e \in ℝ^{+} \land Y \in ℝ^{+}) \to e Y \in ℝ^{+}$
220	218 96 219	sylancr	$⊢ φ \to e Y \in ℝ^{+}$
221	220	rpred	$⊢ φ \to e Y \in ℝ$
222		flle	$⊢ Y \in ℝ \to ⌊Y⌋ \leq Y$
223	69 222	syl	$⊢ φ \to ⌊Y⌋ \leq Y$
224	20 18	rpdivcld	$⊢ φ \to \frac{2}{E} \in ℝ^{+}$
225		efgt1	$⊢ \frac{2}{E} \in ℝ^{+} \to 1 < e^{\frac{2}{E}}$
226	224 225	syl	$⊢ φ \to 1 < e^{\frac{2}{E}}$
227	226 3	breqtrrdi	$⊢ φ \to 1 < X$
228	49 73 69 227 81	lttrd	$⊢ φ \to 1 < Y$
229	49 69 228	ltled	$⊢ φ \to 1 \leq Y$
230	148 49 69 69 223 229	le2addd	$⊢ φ \to ⌊Y⌋ + 1 \leq Y + Y$
231	115	2timesd	$⊢ φ \to 2 Y = Y + Y$
232	230 231	breqtrrd	$⊢ φ \to ⌊Y⌋ + 1 \leq 2 Y$
233		ere	$⊢ e \in ℝ$
234		egt2lt3	$⊢ (2 < e \land e < 3)$
235	234	simpli	$⊢ 2 < e$
236	11 233 235	ltleii	$⊢ 2 \leq e$
237	236	a1i	$⊢ φ \to 2 \leq e$
238	233	a1i	$⊢ φ \to e \in ℝ$
239		lemul1	$⊢ (2 \in ℝ \land e \in ℝ \land (Y \in ℝ \land 0 < Y)) \to (2 \leq e \leftrightarrow 2 Y \leq e Y)$
240	12 238 69 82 239	syl112anc	$⊢ φ \to (2 \leq e \leftrightarrow 2 Y \leq e Y)$
241	237 240	mpbid	$⊢ φ \to 2 Y \leq e Y$
242	216 217 221 232 241	letrd	$⊢ φ \to ⌊Y⌋ + 1 \leq e Y$
243	202 220	logled	$⊢ φ \to (⌊Y⌋ + 1 \leq e Y \leftrightarrow \log (⌊Y⌋ + 1) \leq \log e Y)$
244	242 243	mpbid	$⊢ φ \to \log (⌊Y⌋ + 1) \leq \log e Y$
245		relogmul	$⊢ (e \in ℝ^{+} \land Y \in ℝ^{+}) \to \log e Y = \log e + \log Y$
246	218 96 245	sylancr	$⊢ φ \to \log e Y = \log e + \log Y$
247		loge	$⊢ \log e = 1$
248	247	oveq1i	$⊢ \log e + \log Y = 1 + \log Y$
249	246 248	eqtrdi	$⊢ φ \to \log e Y = 1 + \log Y$
250	244 249	breqtrd	$⊢ φ \to \log (⌊Y⌋ + 1) \leq 1 + \log Y$
251	203 214 49 250	leadd2dd	$⊢ φ \to 1 + \log (⌊Y⌋ + 1) \leq 1 + 1 + \log Y$
252		df-2	$⊢ 2 = 1 + 1$
253	252	oveq1i	$⊢ 2 + \log Y = 1 + 1 + \log Y$
254	142	a1i	$⊢ φ \to 1 \in ℂ$
255	254 254 98	addassd	$⊢ φ \to 1 + 1 + \log Y = 1 + 1 + \log Y$
256	253 255	eqtrid	$⊢ φ \to 2 + \log Y = 1 + 1 + \log Y$
257	251 256	breqtrrd	$⊢ φ \to 1 + \log (⌊Y⌋ + 1) \leq 2 + \log Y$
258	201 205 112 212 257	letrd	$⊢ φ \to \sum_{k = 1}^{⌊Y⌋ + 1} (\frac{1}{k}) \leq 2 + \log Y$
259	200 258	eqbrtrrd	$⊢ φ \to \sum_{n = 0}^{⌊Y⌋} (\frac{1}{n + 1}) \leq 2 + \log Y$
260	109 112 93 259	leadd1dd	$⊢ φ \to \sum_{n = 0}^{⌊Y⌋} (\frac{1}{n + 1}) + \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}) \leq 2 + \log Y + \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1})$
261	102 110 113 188 260	letrd	$⊢ φ \to \log K Y \leq 2 + \log Y + \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1})$
262	100 261	eqbrtrrd	$⊢ φ \to \log K + \log Y \leq 2 + \log Y + \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1})$
263	101 112 93	lesubadd2d	$⊢ φ \to (\log K + \log Y - (2 + \log Y) \leq \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}) \leftrightarrow \log K + \log Y \leq 2 + \log Y + \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}))$
264	262 263	mpbird	$⊢ φ \to \log K + \log Y - (2 + \log Y) \leq \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1})$
265	99 264	eqbrtrrd	$⊢ φ \to \log K - 2 \leq \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1})$
266	92	recnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{1}{n + 1} \in ℂ$
267	67 32 266	fsummulc2	$⊢ φ \to E \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}) = \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} E (\frac{1}{n + 1})$
268	14	adantr	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to E \in ℝ$
269	268	recnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to E \in ℂ$
270	91	nncnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n + 1 \in ℂ$
271	91	nnne0d	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n + 1 \neq 0$
272	269 270 271	divrecd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{E}{n + 1} = E (\frac{1}{n + 1})$
273	268 91	nndivred	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{E}{n + 1} \in ℝ$
274	272 273	eqeltrrd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to E (\frac{1}{n + 1}) \in ℝ$
275	67 274	fsumrecl	$⊢ φ \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} E (\frac{1}{n + 1}) \in ℝ$
276	90	nnrpd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n \in ℝ^{+}$
277	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
278	277	ffvelrni	$⊢ n \in ℝ^{+} \to R (n) \in ℝ$
279	276 278	syl	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to R (n) \in ℝ$
280	90 91	nnmulcld	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n (n + 1) \in ℕ$
281	279 280	nndivred	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{R (n)}{n (n + 1)} \in ℝ$
282	281	recnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{R (n)}{n (n + 1)} \in ℂ$
283	282	abscld	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \|\frac{R (n)}{n (n + 1)}\| \in ℝ$
284	67 283	fsumrecl	$⊢ φ \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} \|\frac{R (n)}{n (n + 1)}\| \in ℝ$
285	279 90	nndivred	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{R (n)}{n} \in ℝ$
286	285	recnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{R (n)}{n} \in ℂ$
287	286	abscld	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \|\frac{R (n)}{n}\| \in ℝ$
288	91	nnrpd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n + 1 \in ℝ^{+}$
289	9	adantr	$⊢ (φ \land n \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)$
290		elfzle1	$⊢ n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) \to ⌊Y⌋ + 1 \leq n$
291	290	adantl	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to ⌊Y⌋ + 1 \leq n$
292	69	adantr	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to Y \in ℝ$
293	292	flcld	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to ⌊Y⌋ \in ℤ$
294	90	nnzd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n \in ℤ$
295		zltp1le	$⊢ (⌊Y⌋ \in ℤ \land n \in ℤ) \to (⌊Y⌋ < n \leftrightarrow ⌊Y⌋ + 1 \leq n)$
296	293 294 295	syl2anc	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (⌊Y⌋ < n \leftrightarrow ⌊Y⌋ + 1 \leq n)$
297	291 296	mpbird	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to ⌊Y⌋ < n$
298		fllt	$⊢ (Y \in ℝ \land n \in ℤ) \to (Y < n \leftrightarrow ⌊Y⌋ < n)$
299	292 294 298	syl2anc	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (Y < n \leftrightarrow ⌊Y⌋ < n)$
300	297 299	mpbird	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to Y < n$
301		elfzle2	$⊢ n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋) \to n \leq ⌊K Y⌋$
302	301	adantl	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n \leq ⌊K Y⌋$
303	114	adantr	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to K Y \in ℝ$
304		flge	$⊢ (K Y \in ℝ \land n \in ℤ) \to (n \leq K Y \leftrightarrow n \leq ⌊K Y⌋)$
305	303 294 304	syl2anc	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (n \leq K Y \leftrightarrow n \leq ⌊K Y⌋)$
306	302 305	mpbird	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n \leq K Y$
307		breq2	$⊢ y = n \to (Y < y \leftrightarrow Y < n)$
308		breq1	$⊢ y = n \to (y \leq K Y \leftrightarrow n \leq K Y)$
309	307 308	anbi12d	$⊢ y = n \to ((Y < y \land y \leq K Y) \leftrightarrow (Y < n \land n \leq K Y))$
310		fveq2	$⊢ y = n \to R (y) = R (n)$
311		id	$⊢ y = n \to y = n$
312	310 311	oveq12d	$⊢ y = n \to \frac{R (y)}{y} = \frac{R (n)}{n}$
313	312	fveq2d	$⊢ y = n \to \|\frac{R (y)}{y}\| = \|\frac{R (n)}{n}\|$
314	313	breq1d	$⊢ y = n \to (\|\frac{R (y)}{y}\| \leq E \leftrightarrow \|\frac{R (n)}{n}\| \leq E)$
315	309 314	anbi12d	$⊢ y = n \to (((Y < y \land y \leq K Y) \land \|\frac{R (y)}{y}\| \leq E) \leftrightarrow ((Y < n \land n \leq K Y) \land \|\frac{R (n)}{n}\| \leq E))$
316	315	rspcev	$⊢ (n \in ℕ \land ((Y < n \land n \leq K Y) \land \|\frac{R (n)}{n}\| \leq E)) \to \exists y \in ℕ ((Y < y \land y \leq K Y) \land \|\frac{R (y)}{y}\| \leq E)$
317	316	expr	$⊢ (n \in ℕ \land (Y < n \land n \leq K Y)) \to (\|\frac{R (n)}{n}\| \leq E \to \exists y \in ℕ ((Y < y \land y \leq K Y) \land \|\frac{R (y)}{y}\| \leq E))$
318	90 300 306 317	syl12anc	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\|\frac{R (n)}{n}\| \leq E \to \exists y \in ℕ ((Y < y \land y \leq K Y) \land \|\frac{R (y)}{y}\| \leq E))$
319	289 318	mtod	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \neg \|\frac{R (n)}{n}\| \leq E$
320	287 268	letrid	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\|\frac{R (n)}{n}\| \leq E \lor E \leq \|\frac{R (n)}{n}\|)$
321	320	ord	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (\neg \|\frac{R (n)}{n}\| \leq E \to E \leq \|\frac{R (n)}{n}\|)$
322	319 321	mpd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to E \leq \|\frac{R (n)}{n}\|$
323	268 287 288 322	lediv1dd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{E}{n + 1} \leq \frac{\|\frac{R (n)}{n}\|}{n + 1}$
324	286 270 271	absdivd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \|\frac{\frac{R (n)}{n}}{n + 1}\| = \frac{\|\frac{R (n)}{n}\|}{\|n + 1\|}$
325	279	recnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to R (n) \in ℂ$
326	90	nncnd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n \in ℂ$
327	90	nnne0d	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to n \neq 0$
328	325 326 270 327 271	divdiv1d	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{\frac{R (n)}{n}}{n + 1} = \frac{R (n)}{n (n + 1)}$
329	328	fveq2d	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \|\frac{\frac{R (n)}{n}}{n + 1}\| = \|\frac{R (n)}{n (n + 1)}\|$
330	288	rprege0d	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to (n + 1 \in ℝ \land 0 \leq n + 1)$
331		absid	$⊢ (n + 1 \in ℝ \land 0 \leq n + 1) \to \|n + 1\| = n + 1$
332	330 331	syl	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \|n + 1\| = n + 1$
333	332	oveq2d	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{\|\frac{R (n)}{n}\|}{\|n + 1\|} = \frac{\|\frac{R (n)}{n}\|}{n + 1}$
334	324 329 333	3eqtr3rd	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to \frac{\|\frac{R (n)}{n}\|}{n + 1} = \|\frac{R (n)}{n (n + 1)}\|$
335	323 272 334	3brtr3d	$⊢ (φ \land n \in (⌊Y⌋ + 1 \dots ⌊K Y⌋)) \to E (\frac{1}{n + 1}) \leq \|\frac{R (n)}{n (n + 1)}\|$
336	67 274 283 335	fsumle	$⊢ φ \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} E (\frac{1}{n + 1}) \leq \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} \|\frac{R (n)}{n (n + 1)}\|$
337	1 2 3 4 5 6 7 8 9	pntpbnd1	$⊢ φ \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} \|\frac{R (n)}{n (n + 1)}\| \leq A$
338	275 284 38 336 337	letrd	$⊢ φ \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} E (\frac{1}{n + 1}) \leq A$
339	267 338	eqbrtrd	$⊢ φ \to E \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}) \leq A$
340	93 38 18	lemuldiv2d	$⊢ φ \to (E \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}) \leq A \leftrightarrow \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}) \leq \frac{A}{E})$
341	339 340	mpbid	$⊢ φ \to \sum_{n = ⌊Y⌋ + 1}^{⌊K Y⌋} (\frac{1}{n + 1}) \leq \frac{A}{E}$
342	60 93 39 265 341	letrd	$⊢ φ \to \log K - 2 \leq \frac{A}{E}$
343	41 60 39 66 342	letrd	$⊢ φ \to (\frac{C}{E}) - 2 \leq \frac{A}{E}$
344	37 12 39 343	subled	$⊢ φ \to (\frac{C}{E}) - (\frac{A}{E}) \leq 2$
345	35 344	eqbrtrd	$⊢ φ \to \frac{2}{E} \leq 2$
346	12 18 20 345	lediv23d	$⊢ φ \to \frac{2}{2} \leq E$
347	10 346	eqbrtrrid	$⊢ φ \to 1 \leq E$
348	16	simprd	$⊢ φ \to E < 1$
349		ltnle	$⊢ (E \in ℝ \land 1 \in ℝ) \to (E < 1 \leftrightarrow \neg 1 \leq E)$
350	14 48 349	sylancl	$⊢ φ \to (E < 1 \leftrightarrow \neg 1 \leq E)$
351	348 350	mpbid	$⊢ φ \to \neg 1 \leq E$
352	347 351	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem pntpbnd2

Proof