pntlemo

Description: Lemma for pnt . Combine all the estimates to establish a smaller eventual bound on R ( Z ) / Z . (Contributed by Mario Carneiro, 14-Apr-2016)

	Ref	Expression
Hypotheses	pntlem1.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
	pntlem1.a	$⊢ φ \to A \in ℝ^{+}$
	pntlem1.b	$⊢ φ \to B \in ℝ^{+}$
	pntlem1.l	$⊢ φ \to L \in (0, 1)$
	pntlem1.d	$⊢ D = A + 1$
	pntlem1.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
	pntlem1.u	$⊢ φ \to U \in ℝ^{+}$
	pntlem1.u2	$⊢ φ \to U \leq A$
	pntlem1.e	$⊢ E = \frac{U}{D}$
	pntlem1.k	$⊢ K = e^{\frac{B}{E}}$
	pntlem1.y	$⊢ φ \to (Y \in ℝ^{+} \land 1 \leq Y)$
	pntlem1.x	$⊢ φ \to (X \in ℝ^{+} \land Y < X)$
	pntlem1.c	$⊢ φ \to C \in ℝ^{+}$
	pntlem1.w	$⊢ W = {(Y + (\frac{4}{L E}))}^{2} + {X K^{2}}^{4} + e^{(\frac{32 B}{(U - E) L E^{2}}) (U \cdot 3 + C)}$
	pntlem1.z	$⊢ φ \to Z \in [W, +∞)$
	pntlem1.m	$⊢ M = ⌊\frac{\log X}{\log K}⌋ + 1$
	pntlem1.n	$⊢ N = ⌊\frac{\frac{\log Z}{\log K}}{2}⌋$
	pntlem1.U	$⊢ φ \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
	pntlem1.K	$⊢ φ \to \forall y \in (X, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < K y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
	pntlem1.C	$⊢ φ \to \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{i = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{i})\| \log i}{z} \leq C$
Assertion	pntlemo	$⊢ φ \to \|\frac{R (Z)}{Z}\| \leq U - F U^{3}$

Proof

Step	Hyp	Ref	Expression
1		pntlem1.r	$⊢ R = (a \in ℝ^{+} ⟼ ψ (a) - a)$
2		pntlem1.a	$⊢ φ \to A \in ℝ^{+}$
3		pntlem1.b	$⊢ φ \to B \in ℝ^{+}$
4		pntlem1.l	$⊢ φ \to L \in (0, 1)$
5		pntlem1.d	$⊢ D = A + 1$
6		pntlem1.f	$⊢ F = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}})$
7		pntlem1.u	$⊢ φ \to U \in ℝ^{+}$
8		pntlem1.u2	$⊢ φ \to U \leq A$
9		pntlem1.e	$⊢ E = \frac{U}{D}$
10		pntlem1.k	$⊢ K = e^{\frac{B}{E}}$
11		pntlem1.y	$⊢ φ \to (Y \in ℝ^{+} \land 1 \leq Y)$
12		pntlem1.x	$⊢ φ \to (X \in ℝ^{+} \land Y < X)$
13		pntlem1.c	$⊢ φ \to C \in ℝ^{+}$
14		pntlem1.w	$⊢ W = {(Y + (\frac{4}{L E}))}^{2} + {X K^{2}}^{4} + e^{(\frac{32 B}{(U - E) L E^{2}}) (U \cdot 3 + C)}$
15		pntlem1.z	$⊢ φ \to Z \in [W, +∞)$
16		pntlem1.m	$⊢ M = ⌊\frac{\log X}{\log K}⌋ + 1$
17		pntlem1.n	$⊢ N = ⌊\frac{\frac{\log Z}{\log K}}{2}⌋$
18		pntlem1.U	$⊢ φ \to \forall z \in [Y, +∞) \|\frac{R (z)}{z}\| \leq U$
19		pntlem1.K	$⊢ φ \to \forall y \in (X, +∞) \exists z \in ℝ^{+} ((y < z \land (1 + L E) z < K y) \land \forall u \in [z, (1 + L E) z] \|\frac{R (u)}{u}\| \leq E)$
20		pntlem1.C	$⊢ φ \to \forall z \in (1, +∞) \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{i = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{i})\| \log i}{z} \leq C$
21	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pntlemb	$⊢ φ \to (Z \in ℝ^{+} \land (1 < Z \land e \leq \sqrt{Z} \land \sqrt{Z} \leq \frac{Z}{Y}) \land (\frac{4}{L E} \leq \sqrt{Z} \land (\frac{\log X}{\log K}) + 2 \leq \frac{\frac{\log Z}{\log K}}{4} \land U \cdot 3 + C \leq (U - E) (\frac{L E^{2}}{32 B}) \log Z))$
22	21	simp1d	$⊢ φ \to Z \in ℝ^{+}$
23	1	pntrf	$⊢ R : ℝ^{+} ⟶ ℝ$
24	23	ffvelrni	$⊢ Z \in ℝ^{+} \to R (Z) \in ℝ$
25	22 24	syl	$⊢ φ \to R (Z) \in ℝ$
26	25 22	rerpdivcld	$⊢ φ \to \frac{R (Z)}{Z} \in ℝ$
27	26	recnd	$⊢ φ \to \frac{R (Z)}{Z} \in ℂ$
28	27	abscld	$⊢ φ \to \|\frac{R (Z)}{Z}\| \in ℝ$
29	22	relogcld	$⊢ φ \to \log Z \in ℝ$
30	28 29	remulcld	$⊢ φ \to \|\frac{R (Z)}{Z}\| \log Z \in ℝ$
31	7	rpred	$⊢ φ \to U \in ℝ$
32		3re	$⊢ 3 \in ℝ$
33	32	a1i	$⊢ φ \to 3 \in ℝ$
34	29 33	readdcld	$⊢ φ \to \log Z + 3 \in ℝ$
35	31 34	remulcld	$⊢ φ \to U (\log Z + 3) \in ℝ$
36		2re	$⊢ 2 \in ℝ$
37	36	a1i	$⊢ φ \to 2 \in ℝ$
38	1 2 3 4 5 6 7 8 9 10	pntlemc	$⊢ φ \to (E \in ℝ^{+} \land K \in ℝ^{+} \land (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+}))$
39	38	simp3d	$⊢ φ \to (E \in (0, 1) \land 1 < K \land U - E \in ℝ^{+})$
40	39	simp3d	$⊢ φ \to U - E \in ℝ^{+}$
41	40	rpred	$⊢ φ \to U - E \in ℝ$
42	1 2 3 4 5 6	pntlemd	$⊢ φ \to (L \in ℝ^{+} \land D \in ℝ^{+} \land F \in ℝ^{+})$
43	42	simp1d	$⊢ φ \to L \in ℝ^{+}$
44	38	simp1d	$⊢ φ \to E \in ℝ^{+}$
45		2z	$⊢ 2 \in ℤ$
46		rpexpcl	$⊢ (E \in ℝ^{+} \land 2 \in ℤ) \to E^{2} \in ℝ^{+}$
47	44 45 46	sylancl	$⊢ φ \to E^{2} \in ℝ^{+}$
48	43 47	rpmulcld	$⊢ φ \to L E^{2} \in ℝ^{+}$
49		3nn0	$⊢ 3 \in ℕ_{0}$
50		2nn	$⊢ 2 \in ℕ$
51	49 50	decnncl	$⊢ 32 \in ℕ$
52		nnrp	$⊢ 32 \in ℕ \to 32 \in ℝ^{+}$
53	51 52	ax-mp	$⊢ 32 \in ℝ^{+}$
54		rpmulcl	$⊢ (32 \in ℝ^{+} \land B \in ℝ^{+}) \to 32 B \in ℝ^{+}$
55	53 3 54	sylancr	$⊢ φ \to 32 B \in ℝ^{+}$
56	48 55	rpdivcld	$⊢ φ \to \frac{L E^{2}}{32 B} \in ℝ^{+}$
57	56	rpred	$⊢ φ \to \frac{L E^{2}}{32 B} \in ℝ$
58	41 57	remulcld	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) \in ℝ$
59	58 29	remulcld	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) \log Z \in ℝ$
60	37 59	remulcld	$⊢ φ \to 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \in ℝ$
61	35 60	resubcld	$⊢ φ \to U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \in ℝ$
62	13	rpred	$⊢ φ \to C \in ℝ$
63	61 62	readdcld	$⊢ φ \to U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z + C \in ℝ$
64	7	rpcnd	$⊢ φ \to U \in ℂ$
65	58	recnd	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) \in ℂ$
66	29	recnd	$⊢ φ \to \log Z \in ℂ$
67	64 65 66	subdird	$⊢ φ \to (U - (U - E) (\frac{L E^{2}}{32 B})) \log Z = U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z$
68	43	rpcnd	$⊢ φ \to L \in ℂ$
69	47	rpcnd	$⊢ φ \to E^{2} \in ℂ$
70	55	rpcnne0d	$⊢ φ \to (32 B \in ℂ \land 32 B \neq 0)$
71		div23	$⊢ (L \in ℂ \land E^{2} \in ℂ \land (32 B \in ℂ \land 32 B \neq 0)) \to \frac{L E^{2}}{32 B} = (\frac{L}{32 B}) E^{2}$
72	68 69 70 71	syl3anc	$⊢ φ \to \frac{L E^{2}}{32 B} = (\frac{L}{32 B}) E^{2}$
73	9	oveq1i	$⊢ E^{2} = {(\frac{U}{D})}^{2}$
74	42	simp2d	$⊢ φ \to D \in ℝ^{+}$
75	74	rpcnd	$⊢ φ \to D \in ℂ$
76	74	rpne0d	$⊢ φ \to D \neq 0$
77	64 75 76	sqdivd	$⊢ φ \to {(\frac{U}{D})}^{2} = \frac{U^{2}}{D^{2}}$
78	73 77	syl5eq	$⊢ φ \to E^{2} = \frac{U^{2}}{D^{2}}$
79	78	oveq2d	$⊢ φ \to (\frac{L}{32 B}) E^{2} = (\frac{L}{32 B}) (\frac{U^{2}}{D^{2}})$
80	43 55	rpdivcld	$⊢ φ \to \frac{L}{32 B} \in ℝ^{+}$
81	80	rpcnd	$⊢ φ \to \frac{L}{32 B} \in ℂ$
82	64	sqcld	$⊢ φ \to U^{2} \in ℂ$
83		rpexpcl	$⊢ (D \in ℝ^{+} \land 2 \in ℤ) \to D^{2} \in ℝ^{+}$
84	74 45 83	sylancl	$⊢ φ \to D^{2} \in ℝ^{+}$
85	84	rpcnne0d	$⊢ φ \to (D^{2} \in ℂ \land D^{2} \neq 0)$
86		divass	$⊢ (\frac{L}{32 B} \in ℂ \land U^{2} \in ℂ \land (D^{2} \in ℂ \land D^{2} \neq 0)) \to \frac{(\frac{L}{32 B}) U^{2}}{D^{2}} = (\frac{L}{32 B}) (\frac{U^{2}}{D^{2}})$
87		div23	$⊢ (\frac{L}{32 B} \in ℂ \land U^{2} \in ℂ \land (D^{2} \in ℂ \land D^{2} \neq 0)) \to \frac{(\frac{L}{32 B}) U^{2}}{D^{2}} = (\frac{\frac{L}{32 B}}{D^{2}}) U^{2}$
88	86 87	eqtr3d	$⊢ (\frac{L}{32 B} \in ℂ \land U^{2} \in ℂ \land (D^{2} \in ℂ \land D^{2} \neq 0)) \to (\frac{L}{32 B}) (\frac{U^{2}}{D^{2}}) = (\frac{\frac{L}{32 B}}{D^{2}}) U^{2}$
89	81 82 85 88	syl3anc	$⊢ φ \to (\frac{L}{32 B}) (\frac{U^{2}}{D^{2}}) = (\frac{\frac{L}{32 B}}{D^{2}}) U^{2}$
90	72 79 89	3eqtrd	$⊢ φ \to \frac{L E^{2}}{32 B} = (\frac{\frac{L}{32 B}}{D^{2}}) U^{2}$
91	90	oveq2d	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) = (U - E) (\frac{\frac{L}{32 B}}{D^{2}}) U^{2}$
92		df-3	$⊢ 3 = 2 + 1$
93	92	oveq2i	$⊢ U^{3} = U^{2 + 1}$
94		2nn0	$⊢ 2 \in ℕ_{0}$
95		expp1	$⊢ (U \in ℂ \land 2 \in ℕ_{0}) \to U^{2 + 1} = U^{2} U$
96	64 94 95	sylancl	$⊢ φ \to U^{2 + 1} = U^{2} U$
97	93 96	syl5eq	$⊢ φ \to U^{3} = U^{2} U$
98	82 64	mulcomd	$⊢ φ \to U^{2} U = U U^{2}$
99	97 98	eqtrd	$⊢ φ \to U^{3} = U U^{2}$
100	99	oveq2d	$⊢ φ \to F U^{3} = F U U^{2}$
101	42	simp3d	$⊢ φ \to F \in ℝ^{+}$
102	101	rpcnd	$⊢ φ \to F \in ℂ$
103	102 64 82	mulassd	$⊢ φ \to F U U^{2} = F U U^{2}$
104		1cnd	$⊢ φ \to 1 \in ℂ$
105	74	rpreccld	$⊢ φ \to \frac{1}{D} \in ℝ^{+}$
106	105	rpcnd	$⊢ φ \to \frac{1}{D} \in ℂ$
107	104 106 64	subdird	$⊢ φ \to (1 - (\frac{1}{D})) U = 1 U - (\frac{1}{D}) U$
108	64	mulid2d	$⊢ φ \to 1 U = U$
109	64 75 76	divrec2d	$⊢ φ \to \frac{U}{D} = (\frac{1}{D}) U$
110	9 109	eqtr2id	$⊢ φ \to (\frac{1}{D}) U = E$
111	108 110	oveq12d	$⊢ φ \to 1 U - (\frac{1}{D}) U = U - E$
112	107 111	eqtr2d	$⊢ φ \to U - E = (1 - (\frac{1}{D})) U$
113	112	oveq1d	$⊢ φ \to (U - E) (\frac{\frac{L}{32 B}}{D^{2}}) = (1 - (\frac{1}{D})) U (\frac{\frac{L}{32 B}}{D^{2}})$
114	6	oveq1i	$⊢ F U = (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}}) U$
115	104 106	subcld	$⊢ φ \to 1 - (\frac{1}{D}) \in ℂ$
116	80 84	rpdivcld	$⊢ φ \to \frac{\frac{L}{32 B}}{D^{2}} \in ℝ^{+}$
117	116	rpcnd	$⊢ φ \to \frac{\frac{L}{32 B}}{D^{2}} \in ℂ$
118	115 117 64	mul32d	$⊢ φ \to (1 - (\frac{1}{D})) (\frac{\frac{L}{32 B}}{D^{2}}) U = (1 - (\frac{1}{D})) U (\frac{\frac{L}{32 B}}{D^{2}})$
119	114 118	syl5eq	$⊢ φ \to F U = (1 - (\frac{1}{D})) U (\frac{\frac{L}{32 B}}{D^{2}})$
120	113 119	eqtr4d	$⊢ φ \to (U - E) (\frac{\frac{L}{32 B}}{D^{2}}) = F U$
121	120	oveq1d	$⊢ φ \to (U - E) (\frac{\frac{L}{32 B}}{D^{2}}) U^{2} = F U U^{2}$
122	40	rpcnd	$⊢ φ \to U - E \in ℂ$
123	122 117 82	mulassd	$⊢ φ \to (U - E) (\frac{\frac{L}{32 B}}{D^{2}}) U^{2} = (U - E) (\frac{\frac{L}{32 B}}{D^{2}}) U^{2}$
124	121 123	eqtr3d	$⊢ φ \to F U U^{2} = (U - E) (\frac{\frac{L}{32 B}}{D^{2}}) U^{2}$
125	100 103 124	3eqtr2d	$⊢ φ \to F U^{3} = (U - E) (\frac{\frac{L}{32 B}}{D^{2}}) U^{2}$
126	91 125	eqtr4d	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) = F U^{3}$
127	126	oveq2d	$⊢ φ \to U - (U - E) (\frac{L E^{2}}{32 B}) = U - F U^{3}$
128	127	oveq1d	$⊢ φ \to (U - (U - E) (\frac{L E^{2}}{32 B})) \log Z = (U - F U^{3}) \log Z$
129	67 128	eqtr3d	$⊢ φ \to U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z = (U - F U^{3}) \log Z$
130	31 29	remulcld	$⊢ φ \to U \log Z \in ℝ$
131	130 59	resubcld	$⊢ φ \to U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z \in ℝ$
132	129 131	eqeltrrd	$⊢ φ \to (U - F U^{3}) \log Z \in ℝ$
133	22	rpred	$⊢ φ \to Z \in ℝ$
134	21	simp2d	$⊢ φ \to (1 < Z \land e \leq \sqrt{Z} \land \sqrt{Z} \leq \frac{Z}{Y})$
135	134	simp1d	$⊢ φ \to 1 < Z$
136	133 135	rplogcld	$⊢ φ \to \log Z \in ℝ^{+}$
137	37 136	rerpdivcld	$⊢ φ \to \frac{2}{\log Z} \in ℝ$
138		fzfid	$⊢ φ \to (1 \dots ⌊\frac{Z}{Y}⌋) \in Fin$
139	22	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to Z \in ℝ^{+}$
140		elfznn	$⊢ n \in (1 \dots ⌊\frac{Z}{Y}⌋) \to n \in ℕ$
141	140	adantl	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to n \in ℕ$
142	141	nnrpd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to n \in ℝ^{+}$
143	139 142	rpdivcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{Z}{n} \in ℝ^{+}$
144	23	ffvelrni	$⊢ \frac{Z}{n} \in ℝ^{+} \to R (\frac{Z}{n}) \in ℝ$
145	143 144	syl	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to R (\frac{Z}{n}) \in ℝ$
146	145 139	rerpdivcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{R (\frac{Z}{n})}{Z} \in ℝ$
147	146	recnd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{R (\frac{Z}{n})}{Z} \in ℂ$
148	147	abscld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|\frac{R (\frac{Z}{n})}{Z}\| \in ℝ$
149	142	relogcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \log n \in ℝ$
150	148 149	remulcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|\frac{R (\frac{Z}{n})}{Z}\| \log n \in ℝ$
151	138 150	fsumrecl	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \in ℝ$
152	137 151	remulcld	$⊢ φ \to (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \in ℝ$
153	152 62	readdcld	$⊢ φ \to (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n + C \in ℝ$
154	25	recnd	$⊢ φ \to R (Z) \in ℂ$
155	154	abscld	$⊢ φ \to \|R (Z)\| \in ℝ$
156	155	recnd	$⊢ φ \to \|R (Z)\| \in ℂ$
157	156 66	mulcld	$⊢ φ \to \|R (Z)\| \log Z \in ℂ$
158	137	recnd	$⊢ φ \to \frac{2}{\log Z} \in ℂ$
159	145	recnd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to R (\frac{Z}{n}) \in ℂ$
160	159	abscld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|R (\frac{Z}{n})\| \in ℝ$
161	160 149	remulcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|R (\frac{Z}{n})\| \log n \in ℝ$
162	138 161	fsumrecl	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n \in ℝ$
163	162	recnd	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n \in ℂ$
164	158 163	mulcld	$⊢ φ \to (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n \in ℂ$
165	22	rpcnd	$⊢ φ \to Z \in ℂ$
166	22	rpne0d	$⊢ φ \to Z \neq 0$
167	157 164 165 166	divsubdird	$⊢ φ \to \frac{\|R (Z)\| \log Z - (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z} = (\frac{\|R (Z)\| \log Z}{Z}) - (\frac{(\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z})$
168	156 66 165 166	div23d	$⊢ φ \to \frac{\|R (Z)\| \log Z}{Z} = (\frac{\|R (Z)\|}{Z}) \log Z$
169	154 165 166	absdivd	$⊢ φ \to \|\frac{R (Z)}{Z}\| = \frac{\|R (Z)\|}{\|Z\|}$
170	22	rprege0d	$⊢ φ \to (Z \in ℝ \land 0 \leq Z)$
171		absid	$⊢ (Z \in ℝ \land 0 \leq Z) \to \|Z\| = Z$
172	170 171	syl	$⊢ φ \to \|Z\| = Z$
173	172	oveq2d	$⊢ φ \to \frac{\|R (Z)\|}{\|Z\|} = \frac{\|R (Z)\|}{Z}$
174	169 173	eqtrd	$⊢ φ \to \|\frac{R (Z)}{Z}\| = \frac{\|R (Z)\|}{Z}$
175	174	oveq1d	$⊢ φ \to \|\frac{R (Z)}{Z}\| \log Z = (\frac{\|R (Z)\|}{Z}) \log Z$
176	168 175	eqtr4d	$⊢ φ \to \frac{\|R (Z)\| \log Z}{Z} = \|\frac{R (Z)}{Z}\| \log Z$
177	158 163 165 166	divassd	$⊢ φ \to \frac{(\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z} = (\frac{2}{\log Z}) (\frac{\sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z})$
178	165	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to Z \in ℂ$
179	166	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to Z \neq 0$
180	159 178 179	absdivd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|\frac{R (\frac{Z}{n})}{Z}\| = \frac{\|R (\frac{Z}{n})\|}{\|Z\|}$
181	172	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|Z\| = Z$
182	181	oveq2d	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{\|R (\frac{Z}{n})\|}{\|Z\|} = \frac{\|R (\frac{Z}{n})\|}{Z}$
183	180 182	eqtrd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|\frac{R (\frac{Z}{n})}{Z}\| = \frac{\|R (\frac{Z}{n})\|}{Z}$
184	183	oveq1d	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|\frac{R (\frac{Z}{n})}{Z}\| \log n = (\frac{\|R (\frac{Z}{n})\|}{Z}) \log n$
185	160	recnd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|R (\frac{Z}{n})\| \in ℂ$
186	149	recnd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \log n \in ℂ$
187	22	rpcnne0d	$⊢ φ \to (Z \in ℂ \land Z \neq 0)$
188	187	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to (Z \in ℂ \land Z \neq 0)$
189		div23	$⊢ (\|R (\frac{Z}{n})\| \in ℂ \land \log n \in ℂ \land (Z \in ℂ \land Z \neq 0)) \to \frac{\|R (\frac{Z}{n})\| \log n}{Z} = (\frac{\|R (\frac{Z}{n})\|}{Z}) \log n$
190	185 186 188 189	syl3anc	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{\|R (\frac{Z}{n})\| \log n}{Z} = (\frac{\|R (\frac{Z}{n})\|}{Z}) \log n$
191	184 190	eqtr4d	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|\frac{R (\frac{Z}{n})}{Z}\| \log n = \frac{\|R (\frac{Z}{n})\| \log n}{Z}$
192	191	sumeq2dv	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n = \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{\|R (\frac{Z}{n})\| \log n}{Z})$
193	161	recnd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|R (\frac{Z}{n})\| \log n \in ℂ$
194	138 165 193 166	fsumdivc	$⊢ φ \to \frac{\sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z} = \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{\|R (\frac{Z}{n})\| \log n}{Z})$
195	192 194	eqtr4d	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n = \frac{\sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z}$
196	195	oveq2d	$⊢ φ \to (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n = (\frac{2}{\log Z}) (\frac{\sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z})$
197	177 196	eqtr4d	$⊢ φ \to \frac{(\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z} = (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
198	176 197	oveq12d	$⊢ φ \to (\frac{\|R (Z)\| \log Z}{Z}) - (\frac{(\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z}) = \|\frac{R (Z)}{Z}\| \log Z - (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
199	167 198	eqtrd	$⊢ φ \to \frac{\|R (Z)\| \log Z - (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z} = \|\frac{R (Z)}{Z}\| \log Z - (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
200		2fveq3	$⊢ z = Z \to \|R (z)\| = \|R (Z)\|$
201		fveq2	$⊢ z = Z \to \log z = \log Z$
202	200 201	oveq12d	$⊢ z = Z \to \|R (z)\| \log z = \|R (Z)\| \log Z$
203	201	oveq2d	$⊢ z = Z \to \frac{2}{\log z} = \frac{2}{\log Z}$
204		oveq2	$⊢ i = n \to \frac{z}{i} = \frac{z}{n}$
205	204	fveq2d	$⊢ i = n \to R (\frac{z}{i}) = R (\frac{z}{n})$
206	205	fveq2d	$⊢ i = n \to \|R (\frac{z}{i})\| = \|R (\frac{z}{n})\|$
207		fveq2	$⊢ i = n \to \log i = \log n$
208	206 207	oveq12d	$⊢ i = n \to \|R (\frac{z}{i})\| \log i = \|R (\frac{z}{n})\| \log n$
209	208	cbvsumv	$⊢ \sum_{i = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{i})\| \log i = \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n$
210		fvoveq1	$⊢ z = Z \to ⌊\frac{z}{Y}⌋ = ⌊\frac{Z}{Y}⌋$
211	210	oveq2d	$⊢ z = Z \to (1 \dots ⌊\frac{z}{Y}⌋) = (1 \dots ⌊\frac{Z}{Y}⌋)$
212		simpl	$⊢ (z = Z \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to z = Z$
213	212	fvoveq1d	$⊢ (z = Z \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to R (\frac{z}{n}) = R (\frac{Z}{n})$
214	213	fveq2d	$⊢ (z = Z \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|R (\frac{z}{n})\| = \|R (\frac{Z}{n})\|$
215	214	oveq1d	$⊢ (z = Z \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|R (\frac{z}{n})\| \log n = \|R (\frac{Z}{n})\| \log n$
216	211 215	sumeq12rdv	$⊢ z = Z \to \sum_{n = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{n})\| \log n = \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n$
217	209 216	syl5eq	$⊢ z = Z \to \sum_{i = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{i})\| \log i = \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n$
218	203 217	oveq12d	$⊢ z = Z \to (\frac{2}{\log z}) \sum_{i = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{i})\| \log i = (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n$
219	202 218	oveq12d	$⊢ z = Z \to \|R (z)\| \log z - (\frac{2}{\log z}) \sum_{i = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{i})\| \log i = \|R (Z)\| \log Z - (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n$
220		id	$⊢ z = Z \to z = Z$
221	219 220	oveq12d	$⊢ z = Z \to \frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{i = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{i})\| \log i}{z} = \frac{\|R (Z)\| \log Z - (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z}$
222	221	breq1d	$⊢ z = Z \to (\frac{\|R (z)\| \log z - (\frac{2}{\log z}) \sum_{i = 1}^{⌊\frac{z}{Y}⌋} \|R (\frac{z}{i})\| \log i}{z} \leq C \leftrightarrow \frac{\|R (Z)\| \log Z - (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z} \leq C)$
223		1re	$⊢ 1 \in ℝ$
224		rexr	$⊢ 1 \in ℝ \to 1 \in ℝ^{*}$
225		elioopnf	$⊢ 1 \in ℝ^{*} \to (Z \in (1, +∞) \leftrightarrow (Z \in ℝ \land 1 < Z))$
226	223 224 225	mp2b	$⊢ Z \in (1, +∞) \leftrightarrow (Z \in ℝ \land 1 < Z)$
227	133 135 226	sylanbrc	$⊢ φ \to Z \in (1, +∞)$
228	222 20 227	rspcdva	$⊢ φ \to \frac{\|R (Z)\| \log Z - (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|R (\frac{Z}{n})\| \log n}{Z} \leq C$
229	199 228	eqbrtrrd	$⊢ φ \to \|\frac{R (Z)}{Z}\| \log Z - (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \leq C$
230	30 152 62	lesubadd2d	$⊢ φ \to (\|\frac{R (Z)}{Z}\| \log Z - (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \leq C \leftrightarrow \|\frac{R (Z)}{Z}\| \log Z \leq (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n + C)$
231	229 230	mpbid	$⊢ φ \to \|\frac{R (Z)}{Z}\| \log Z \leq (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n + C$
232		2cnd	$⊢ φ \to 2 \in ℂ$
233	148	recnd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|\frac{R (\frac{Z}{n})}{Z}\| \in ℂ$
234	233 186	mulcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \|\frac{R (\frac{Z}{n})}{Z}\| \log n \in ℂ$
235	138 234	fsumcl	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \in ℂ$
236	136	rpne0d	$⊢ φ \to \log Z \neq 0$
237	232 235 66 236	div23d	$⊢ φ \to \frac{2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n}{\log Z} = (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
238	29	resqcld	$⊢ φ \to {\log Z}^{2} \in ℝ$
239	57 238	remulcld	$⊢ φ \to (\frac{L E^{2}}{32 B}) {\log Z}^{2} \in ℝ$
240	41 239	remulcld	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \in ℝ$
241		remulcl	$⊢ (2 \in ℝ \land (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \in ℝ) \to 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \in ℝ$
242	36 240 241	sylancr	$⊢ φ \to 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \in ℝ$
243	35 29	remulcld	$⊢ φ \to U (\log Z + 3) \log Z \in ℝ$
244		remulcl	$⊢ (2 \in ℝ \land \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \in ℝ) \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \in ℝ$
245	36 151 244	sylancr	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \in ℝ$
246	31	adantr	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to U \in ℝ$
247	246 141	nndivred	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{U}{n} \in ℝ$
248	247 148	resubcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to (\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\| \in ℝ$
249	248 149	remulcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
250	138 249	fsumrecl	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
251	37 250	remulcld	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ$
252	243 245	resubcld	$⊢ φ \to U (\log Z + 3) \log Z - 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \in ℝ$
253	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	pntlemf	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
254		2pos	$⊢ 0 < 2$
255	254	a1i	$⊢ φ \to 0 < 2$
256		lemul2	$⊢ ((U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \in ℝ \land \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \in ℝ \land (2 \in ℝ \land 0 < 2)) \to ((U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leftrightarrow 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
257	240 250 37 255 256	syl112anc	$⊢ φ \to ((U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leftrightarrow 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n)$
258	253 257	mpbid	$⊢ φ \to 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n$
259	247	recnd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to \frac{U}{n} \in ℂ$
260	259 233 186	subdird	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n = (\frac{U}{n}) \log n - \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
261	260	sumeq2dv	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n = \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) \log n - \|\frac{R (\frac{Z}{n})}{Z}\| \log n)$
262	247 149	remulcld	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to (\frac{U}{n}) \log n \in ℝ$
263	262	recnd	$⊢ (φ \land n \in (1 \dots ⌊\frac{Z}{Y}⌋)) \to (\frac{U}{n}) \log n \in ℂ$
264	138 263 234	fsumsub	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) \log n - \|\frac{R (\frac{Z}{n})}{Z}\| \log n) = \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n - \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
265	261 264	eqtrd	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n = \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n - \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
266	265	oveq2d	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n = 2 (\sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n - \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n)$
267	138 262	fsumrecl	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n \in ℝ$
268	267	recnd	$⊢ φ \to \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n \in ℂ$
269	232 268 235	subdid	$⊢ φ \to 2 (\sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n - \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n) = 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n - 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
270	266 269	eqtrd	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n = 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n - 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
271		remulcl	$⊢ (2 \in ℝ \land \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n \in ℝ) \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n \in ℝ$
272	36 267 271	sylancr	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n \in ℝ$
273	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	pntlemk	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n \leq U (\log Z + 3) \log Z$
274	272 243 245 273	lesub1dd	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} (\frac{U}{n}) \log n - 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \leq U (\log Z + 3) \log Z - 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
275	270 274	eqbrtrd	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} ((\frac{U}{n}) - \|\frac{R (\frac{Z}{n})}{Z}\|) \log n \leq U (\log Z + 3) \log Z - 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
276	242 251 252 258 275	letrd	$⊢ φ \to 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} \leq U (\log Z + 3) \log Z - 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n$
277	242 243 245 276	lesubd	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \leq U (\log Z + 3) \log Z - 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2}$
278	35	recnd	$⊢ φ \to U (\log Z + 3) \in ℂ$
279	60	recnd	$⊢ φ \to 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \in ℂ$
280	278 279 66	subdird	$⊢ φ \to (U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z) \log Z = U (\log Z + 3) \log Z - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \log Z$
281	59	recnd	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) \log Z \in ℂ$
282	232 281 66	mulassd	$⊢ φ \to 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \log Z = 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \log Z$
283	65 66 66	mulassd	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) \log Z \log Z = (U - E) (\frac{L E^{2}}{32 B}) \log Z \log Z$
284	66	sqvald	$⊢ φ \to {\log Z}^{2} = \log Z \log Z$
285	284	oveq2d	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} = (U - E) (\frac{L E^{2}}{32 B}) \log Z \log Z$
286	56	rpcnd	$⊢ φ \to \frac{L E^{2}}{32 B} \in ℂ$
287	238	recnd	$⊢ φ \to {\log Z}^{2} \in ℂ$
288	122 286 287	mulassd	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2} = (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2}$
289	283 285 288	3eqtr2d	$⊢ φ \to (U - E) (\frac{L E^{2}}{32 B}) \log Z \log Z = (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2}$
290	289	oveq2d	$⊢ φ \to 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \log Z = 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2}$
291	282 290	eqtrd	$⊢ φ \to 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \log Z = 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2}$
292	291	oveq2d	$⊢ φ \to U (\log Z + 3) \log Z - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \log Z = U (\log Z + 3) \log Z - 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2}$
293	280 292	eqtrd	$⊢ φ \to (U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z) \log Z = U (\log Z + 3) \log Z - 2 (U - E) (\frac{L E^{2}}{32 B}) {\log Z}^{2}$
294	277 293	breqtrrd	$⊢ φ \to 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \leq (U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z) \log Z$
295	245 61 136	ledivmul2d	$⊢ φ \to (\frac{2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n}{\log Z} \leq U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \leftrightarrow 2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \leq (U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z) \log Z)$
296	294 295	mpbird	$⊢ φ \to \frac{2 \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n}{\log Z} \leq U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z$
297	237 296	eqbrtrrd	$⊢ φ \to (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n \leq U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z$
298	152 61 62 297	leadd1dd	$⊢ φ \to (\frac{2}{\log Z}) \sum_{n = 1}^{⌊\frac{Z}{Y}⌋} \|\frac{R (\frac{Z}{n})}{Z}\| \log n + C \leq U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z + C$
299	30 153 63 231 298	letrd	$⊢ φ \to \|\frac{R (Z)}{Z}\| \log Z \leq U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z + C$
300		remulcl	$⊢ (U \in ℝ \land 3 \in ℝ) \to U \cdot 3 \in ℝ$
301	31 32 300	sylancl	$⊢ φ \to U \cdot 3 \in ℝ$
302	301 62	readdcld	$⊢ φ \to U \cdot 3 + C \in ℝ$
303	21	simp3d	$⊢ φ \to (\frac{4}{L E} \leq \sqrt{Z} \land (\frac{\log X}{\log K}) + 2 \leq \frac{\frac{\log Z}{\log K}}{4} \land U \cdot 3 + C \leq (U - E) (\frac{L E^{2}}{32 B}) \log Z)$
304	303	simp3d	$⊢ φ \to U \cdot 3 + C \leq (U - E) (\frac{L E^{2}}{32 B}) \log Z$
305	302 59 130 304	leadd2dd	$⊢ φ \to U \log Z + U \cdot 3 + C \leq U \log Z + (U - E) (\frac{L E^{2}}{32 B}) \log Z$
306	33	recnd	$⊢ φ \to 3 \in ℂ$
307	64 66 306	adddid	$⊢ φ \to U (\log Z + 3) = U \log Z + U \cdot 3$
308	307	oveq1d	$⊢ φ \to U (\log Z + 3) + C = U \log Z + U \cdot 3 + C$
309	130	recnd	$⊢ φ \to U \log Z \in ℂ$
310	64 306	mulcld	$⊢ φ \to U \cdot 3 \in ℂ$
311	13	rpcnd	$⊢ φ \to C \in ℂ$
312	309 310 311	addassd	$⊢ φ \to U \log Z + U \cdot 3 + C = U \log Z + U \cdot 3 + C$
313	308 312	eqtrd	$⊢ φ \to U (\log Z + 3) + C = U \log Z + U \cdot 3 + C$
314	281	2timesd	$⊢ φ \to 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z = (U - E) (\frac{L E^{2}}{32 B}) \log Z + (U - E) (\frac{L E^{2}}{32 B}) \log Z$
315	314	oveq2d	$⊢ φ \to U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z + 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z = (U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z) + (U - E) (\frac{L E^{2}}{32 B}) \log Z + (U - E) (\frac{L E^{2}}{32 B}) \log Z$
316	309 281 281	nppcan3d	$⊢ φ \to (U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z) + (U - E) (\frac{L E^{2}}{32 B}) \log Z + (U - E) (\frac{L E^{2}}{32 B}) \log Z = U \log Z + (U - E) (\frac{L E^{2}}{32 B}) \log Z$
317	315 316	eqtrd	$⊢ φ \to U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z + 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z = U \log Z + (U - E) (\frac{L E^{2}}{32 B}) \log Z$
318	305 313 317	3brtr4d	$⊢ φ \to U (\log Z + 3) + C \leq U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z + 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z$
319	35 62	readdcld	$⊢ φ \to U (\log Z + 3) + C \in ℝ$
320	319 60 131	lesubaddd	$⊢ φ \to (U (\log Z + 3) + C - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \leq U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z \leftrightarrow U (\log Z + 3) + C \leq U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z + 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z)$
321	318 320	mpbird	$⊢ φ \to U (\log Z + 3) + C - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z \leq U \log Z - (U - E) (\frac{L E^{2}}{32 B}) \log Z$
322	278 311 279	addsubd	$⊢ φ \to U (\log Z + 3) + C - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z = U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z + C$
323	321 322 129	3brtr3d	$⊢ φ \to U (\log Z + 3) - 2 (U - E) (\frac{L E^{2}}{32 B}) \log Z + C \leq (U - F U^{3}) \log Z$
324	30 63 132 299 323	letrd	$⊢ φ \to \|\frac{R (Z)}{Z}\| \log Z \leq (U - F U^{3}) \log Z$
325		3z	$⊢ 3 \in ℤ$
326		rpexpcl	$⊢ (U \in ℝ^{+} \land 3 \in ℤ) \to U^{3} \in ℝ^{+}$
327	7 325 326	sylancl	$⊢ φ \to U^{3} \in ℝ^{+}$
328	101 327	rpmulcld	$⊢ φ \to F U^{3} \in ℝ^{+}$
329	328	rpred	$⊢ φ \to F U^{3} \in ℝ$
330	31 329	resubcld	$⊢ φ \to U - F U^{3} \in ℝ$
331	28 330 136	lemul1d	$⊢ φ \to (\|\frac{R (Z)}{Z}\| \leq U - F U^{3} \leftrightarrow \|\frac{R (Z)}{Z}\| \log Z \leq (U - F U^{3}) \log Z)$
332	324 331	mpbird	$⊢ φ \to \|\frac{R (Z)}{Z}\| \leq U - F U^{3}$

Metamath Proof Explorer

Theorem pntlemo

Proof