pntlemk

Description: Lemma for pnt . Evaluate the naive part of the estimate. (Contributed by Mario Carneiro, 14-Apr-2016)

	Ref	Expression
Hypotheses	pntlem1.r	\|- R = ( a e. RR+ \|-> ( ( psi ` a ) - a ) )
	pntlem1.a	\|- ( ph -> A e. RR+ )
	pntlem1.b	\|- ( ph -> B e. RR+ )
	pntlem1.l	\|- ( ph -> L e. ( 0 (,) 1 ) )
	pntlem1.d	\|- D = ( A + 1 )
	pntlem1.f	\|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
	pntlem1.u	\|- ( ph -> U e. RR+ )
	pntlem1.u2	\|- ( ph -> U <_ A )
	pntlem1.e	\|- E = ( U / D )
	pntlem1.k	\|- K = ( exp ` ( B / E ) )
	pntlem1.y	\|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
	pntlem1.x	\|- ( ph -> ( X e. RR+ /\ Y < X ) )
	pntlem1.c	\|- ( ph -> C e. RR+ )
	pntlem1.w	\|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
	pntlem1.z	\|- ( ph -> Z e. ( W [,) +oo ) )
	pntlem1.m	\|- M = ( ( \|_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
	pntlem1.n	\|- N = ( \|_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
	pntlem1.U	\|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
	pntlem1.K	\|- ( ph -> A. y e. ( X (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
Assertion	pntlemk	\|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) <_ ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		pntlem1.r	\|- R = ( a e. RR+ \|-> ( ( psi ` a ) - a ) )
2		pntlem1.a	\|- ( ph -> A e. RR+ )
3		pntlem1.b	\|- ( ph -> B e. RR+ )
4		pntlem1.l	\|- ( ph -> L e. ( 0 (,) 1 ) )
5		pntlem1.d	\|- D = ( A + 1 )
6		pntlem1.f	\|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
7		pntlem1.u	\|- ( ph -> U e. RR+ )
8		pntlem1.u2	\|- ( ph -> U <_ A )
9		pntlem1.e	\|- E = ( U / D )
10		pntlem1.k	\|- K = ( exp ` ( B / E ) )
11		pntlem1.y	\|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
12		pntlem1.x	\|- ( ph -> ( X e. RR+ /\ Y < X ) )
13		pntlem1.c	\|- ( ph -> C e. RR+ )
14		pntlem1.w	\|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
15		pntlem1.z	\|- ( ph -> Z e. ( W [,) +oo ) )
16		pntlem1.m	\|- M = ( ( \|_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
17		pntlem1.n	\|- N = ( \|_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
18		pntlem1.U	\|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
19		pntlem1.K	\|- ( ph -> A. y e. ( X (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
20		2re	\|- 2 e. RR
21		fzfid	\|- ( ph -> ( 1 ... ( \|_ ` ( Z / Y ) ) ) e. Fin )
22		elfznn	\|- ( n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) -> n e. NN )
23	22	adantl	\|- ( ( ph /\ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ) -> n e. NN )
24	23	nnrpd	\|- ( ( ph /\ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ) -> n e. RR+ )
25	24	relogcld	\|- ( ( ph /\ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ) -> ( log ` n ) e. RR )
26	25 23	nndivred	\|- ( ( ph /\ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ) -> ( ( log ` n ) / n ) e. RR )
27	21 26	fsumrecl	\|- ( ph -> sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. RR )
28		remulcl	\|- ( ( 2 e. RR /\ sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. RR ) -> ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) e. RR )
29	20 27 28	sylancr	\|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) e. RR )
30	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	pntlemb	\|- ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )
31	30	simp1d	\|- ( ph -> Z e. RR+ )
32	31	relogcld	\|- ( ph -> ( log ` Z ) e. RR )
33		peano2re	\|- ( ( log ` Z ) e. RR -> ( ( log ` Z ) + 1 ) e. RR )
34	32 33	syl	\|- ( ph -> ( ( log ` Z ) + 1 ) e. RR )
35	34	resqcld	\|- ( ph -> ( ( ( log ` Z ) + 1 ) ^ 2 ) e. RR )
36		3re	\|- 3 e. RR
37		readdcl	\|- ( ( ( log ` Z ) e. RR /\ 3 e. RR ) -> ( ( log ` Z ) + 3 ) e. RR )
38	32 36 37	sylancl	\|- ( ph -> ( ( log ` Z ) + 3 ) e. RR )
39	38 32	remulcld	\|- ( ph -> ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) e. RR )
40	31	rpred	\|- ( ph -> Z e. RR )
41	11	simpld	\|- ( ph -> Y e. RR+ )
42	40 41	rerpdivcld	\|- ( ph -> ( Z / Y ) e. RR )
43		1red	\|- ( ph -> 1 e. RR )
44	31	rpsqrtcld	\|- ( ph -> ( sqrt ` Z ) e. RR+ )
45	44	rpred	\|- ( ph -> ( sqrt ` Z ) e. RR )
46		ere	\|- _e e. RR
47	46	a1i	\|- ( ph -> _e e. RR )
48		1re	\|- 1 e. RR
49		1lt2	\|- 1 < 2
50		egt2lt3	\|- ( 2 < _e /\ _e < 3 )
51	50	simpli	\|- 2 < _e
52	48 20 46	lttri	\|- ( ( 1 < 2 /\ 2 < _e ) -> 1 < _e )
53	49 51 52	mp2an	\|- 1 < _e
54	48 46 53	ltleii	\|- 1 <_ _e
55	54	a1i	\|- ( ph -> 1 <_ _e )
56	30	simp2d	\|- ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) )
57	56	simp2d	\|- ( ph -> _e <_ ( sqrt ` Z ) )
58	43 47 45 55 57	letrd	\|- ( ph -> 1 <_ ( sqrt ` Z ) )
59	56	simp3d	\|- ( ph -> ( sqrt ` Z ) <_ ( Z / Y ) )
60	43 45 42 58 59	letrd	\|- ( ph -> 1 <_ ( Z / Y ) )
61		flge1nn	\|- ( ( ( Z / Y ) e. RR /\ 1 <_ ( Z / Y ) ) -> ( \|_ ` ( Z / Y ) ) e. NN )
62	42 60 61	syl2anc	\|- ( ph -> ( \|_ ` ( Z / Y ) ) e. NN )
63	62	nnrpd	\|- ( ph -> ( \|_ ` ( Z / Y ) ) e. RR+ )
64	63	relogcld	\|- ( ph -> ( log ` ( \|_ ` ( Z / Y ) ) ) e. RR )
65	64 43	readdcld	\|- ( ph -> ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) e. RR )
66	65	resqcld	\|- ( ph -> ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) e. RR )
67		logdivbnd	\|- ( ( \|_ ` ( Z / Y ) ) e. NN -> sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) )
68	62 67	syl	\|- ( ph -> sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) )
69	20	a1i	\|- ( ph -> 2 e. RR )
70		2pos	\|- 0 < 2
71	70	a1i	\|- ( ph -> 0 < 2 )
72		lemuldiv2	\|- ( ( sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. RR /\ ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <-> sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) ) )
73	27 66 69 71 72	syl112anc	\|- ( ph -> ( ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <-> sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) / 2 ) ) )
74	68 73	mpbird	\|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) )
75		reflcl	\|- ( ( Z / Y ) e. RR -> ( \|_ ` ( Z / Y ) ) e. RR )
76	42 75	syl	\|- ( ph -> ( \|_ ` ( Z / Y ) ) e. RR )
77		flle	\|- ( ( Z / Y ) e. RR -> ( \|_ ` ( Z / Y ) ) <_ ( Z / Y ) )
78	42 77	syl	\|- ( ph -> ( \|_ ` ( Z / Y ) ) <_ ( Z / Y ) )
79	11	simprd	\|- ( ph -> 1 <_ Y )
80		1rp	\|- 1 e. RR+
81	80	a1i	\|- ( ph -> 1 e. RR+ )
82	81 41 31	lediv2d	\|- ( ph -> ( 1 <_ Y <-> ( Z / Y ) <_ ( Z / 1 ) ) )
83	79 82	mpbid	\|- ( ph -> ( Z / Y ) <_ ( Z / 1 ) )
84	40	recnd	\|- ( ph -> Z e. CC )
85	84	div1d	\|- ( ph -> ( Z / 1 ) = Z )
86	83 85	breqtrd	\|- ( ph -> ( Z / Y ) <_ Z )
87	76 42 40 78 86	letrd	\|- ( ph -> ( \|_ ` ( Z / Y ) ) <_ Z )
88	63 31	logled	\|- ( ph -> ( ( \|_ ` ( Z / Y ) ) <_ Z <-> ( log ` ( \|_ ` ( Z / Y ) ) ) <_ ( log ` Z ) ) )
89	87 88	mpbid	\|- ( ph -> ( log ` ( \|_ ` ( Z / Y ) ) ) <_ ( log ` Z ) )
90	64 32 43 89	leadd1dd	\|- ( ph -> ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) <_ ( ( log ` Z ) + 1 ) )
91		0red	\|- ( ph -> 0 e. RR )
92		log1	\|- ( log ` 1 ) = 0
93	62	nnge1d	\|- ( ph -> 1 <_ ( \|_ ` ( Z / Y ) ) )
94		logleb	\|- ( ( 1 e. RR+ /\ ( \|_ ` ( Z / Y ) ) e. RR+ ) -> ( 1 <_ ( \|_ ` ( Z / Y ) ) <-> ( log ` 1 ) <_ ( log ` ( \|_ ` ( Z / Y ) ) ) ) )
95	80 63 94	sylancr	\|- ( ph -> ( 1 <_ ( \|_ ` ( Z / Y ) ) <-> ( log ` 1 ) <_ ( log ` ( \|_ ` ( Z / Y ) ) ) ) )
96	93 95	mpbid	\|- ( ph -> ( log ` 1 ) <_ ( log ` ( \|_ ` ( Z / Y ) ) ) )
97	92 96	eqbrtrrid	\|- ( ph -> 0 <_ ( log ` ( \|_ ` ( Z / Y ) ) ) )
98	64	lep1d	\|- ( ph -> ( log ` ( \|_ ` ( Z / Y ) ) ) <_ ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) )
99	91 64 65 97 98	letrd	\|- ( ph -> 0 <_ ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) )
100	91 65 34 99 90	letrd	\|- ( ph -> 0 <_ ( ( log ` Z ) + 1 ) )
101	65 34 99 100	le2sqd	\|- ( ph -> ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) <_ ( ( log ` Z ) + 1 ) <-> ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <_ ( ( ( log ` Z ) + 1 ) ^ 2 ) ) )
102	90 101	mpbid	\|- ( ph -> ( ( ( log ` ( \|_ ` ( Z / Y ) ) ) + 1 ) ^ 2 ) <_ ( ( ( log ` Z ) + 1 ) ^ 2 ) )
103	29 66 35 74 102	letrd	\|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` Z ) + 1 ) ^ 2 ) )
104	32	resqcld	\|- ( ph -> ( ( log ` Z ) ^ 2 ) e. RR )
105	69 32	remulcld	\|- ( ph -> ( 2 x. ( log ` Z ) ) e. RR )
106	104 105	readdcld	\|- ( ph -> ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) e. RR )
107		loge	\|- ( log ` _e ) = 1
108	44	rpge0d	\|- ( ph -> 0 <_ ( sqrt ` Z ) )
109	45 45 108 58	lemulge12d	\|- ( ph -> ( sqrt ` Z ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) )
110	31	rprege0d	\|- ( ph -> ( Z e. RR /\ 0 <_ Z ) )
111		remsqsqrt	\|- ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
112	110 111	syl	\|- ( ph -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
113	109 112	breqtrd	\|- ( ph -> ( sqrt ` Z ) <_ Z )
114	47 45 40 57 113	letrd	\|- ( ph -> _e <_ Z )
115		epr	\|- _e e. RR+
116		logleb	\|- ( ( _e e. RR+ /\ Z e. RR+ ) -> ( _e <_ Z <-> ( log ` _e ) <_ ( log ` Z ) ) )
117	115 31 116	sylancr	\|- ( ph -> ( _e <_ Z <-> ( log ` _e ) <_ ( log ` Z ) ) )
118	114 117	mpbid	\|- ( ph -> ( log ` _e ) <_ ( log ` Z ) )
119	107 118	eqbrtrrid	\|- ( ph -> 1 <_ ( log ` Z ) )
120	43 32 106 119	leadd2dd	\|- ( ph -> ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + 1 ) <_ ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + ( log ` Z ) ) )
121	32	recnd	\|- ( ph -> ( log ` Z ) e. CC )
122		binom21	\|- ( ( log ` Z ) e. CC -> ( ( ( log ` Z ) + 1 ) ^ 2 ) = ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + 1 ) )
123	121 122	syl	\|- ( ph -> ( ( ( log ` Z ) + 1 ) ^ 2 ) = ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + 1 ) )
124	121	sqvald	\|- ( ph -> ( ( log ` Z ) ^ 2 ) = ( ( log ` Z ) x. ( log ` Z ) ) )
125		df-3	\|- 3 = ( 2 + 1 )
126	125	oveq1i	\|- ( 3 x. ( log ` Z ) ) = ( ( 2 + 1 ) x. ( log ` Z ) )
127		2cnd	\|- ( ph -> 2 e. CC )
128		1cnd	\|- ( ph -> 1 e. CC )
129	127 128 121	adddird	\|- ( ph -> ( ( 2 + 1 ) x. ( log ` Z ) ) = ( ( 2 x. ( log ` Z ) ) + ( 1 x. ( log ` Z ) ) ) )
130	126 129	eqtrid	\|- ( ph -> ( 3 x. ( log ` Z ) ) = ( ( 2 x. ( log ` Z ) ) + ( 1 x. ( log ` Z ) ) ) )
131	121	mullidd	\|- ( ph -> ( 1 x. ( log ` Z ) ) = ( log ` Z ) )
132	131	oveq2d	\|- ( ph -> ( ( 2 x. ( log ` Z ) ) + ( 1 x. ( log ` Z ) ) ) = ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) )
133	130 132	eqtr2d	\|- ( ph -> ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) = ( 3 x. ( log ` Z ) ) )
134	124 133	oveq12d	\|- ( ph -> ( ( ( log ` Z ) ^ 2 ) + ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) ) = ( ( ( log ` Z ) x. ( log ` Z ) ) + ( 3 x. ( log ` Z ) ) ) )
135	121	sqcld	\|- ( ph -> ( ( log ` Z ) ^ 2 ) e. CC )
136		2cn	\|- 2 e. CC
137		mulcl	\|- ( ( 2 e. CC /\ ( log ` Z ) e. CC ) -> ( 2 x. ( log ` Z ) ) e. CC )
138	136 121 137	sylancr	\|- ( ph -> ( 2 x. ( log ` Z ) ) e. CC )
139	135 138 121	addassd	\|- ( ph -> ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + ( log ` Z ) ) = ( ( ( log ` Z ) ^ 2 ) + ( ( 2 x. ( log ` Z ) ) + ( log ` Z ) ) ) )
140		3cn	\|- 3 e. CC
141	140	a1i	\|- ( ph -> 3 e. CC )
142	121 141 121	adddird	\|- ( ph -> ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) = ( ( ( log ` Z ) x. ( log ` Z ) ) + ( 3 x. ( log ` Z ) ) ) )
143	134 139 142	3eqtr4rd	\|- ( ph -> ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) = ( ( ( ( log ` Z ) ^ 2 ) + ( 2 x. ( log ` Z ) ) ) + ( log ` Z ) ) )
144	120 123 143	3brtr4d	\|- ( ph -> ( ( ( log ` Z ) + 1 ) ^ 2 ) <_ ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) )
145	29 35 39 103 144	letrd	\|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) )
146	29 39 7	lemul2d	\|- ( ph -> ( ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) <-> ( U x. ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) <_ ( U x. ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) ) )
147	145 146	mpbid	\|- ( ph -> ( U x. ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) <_ ( U x. ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) )
148	7	rpred	\|- ( ph -> U e. RR )
149	148	adantr	\|- ( ( ph /\ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ) -> U e. RR )
150	149	recnd	\|- ( ( ph /\ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ) -> U e. CC )
151	25	recnd	\|- ( ( ph /\ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ) -> ( log ` n ) e. CC )
152	24	rpcnne0d	\|- ( ( ph /\ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ) -> ( n e. CC /\ n =/= 0 ) )
153		div23	\|- ( ( U e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U x. ( log ` n ) ) / n ) = ( ( U / n ) x. ( log ` n ) ) )
154		divass	\|- ( ( U e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U x. ( log ` n ) ) / n ) = ( U x. ( ( log ` n ) / n ) ) )
155	153 154	eqtr3d	\|- ( ( U e. CC /\ ( log ` n ) e. CC /\ ( n e. CC /\ n =/= 0 ) ) -> ( ( U / n ) x. ( log ` n ) ) = ( U x. ( ( log ` n ) / n ) ) )
156	150 151 152 155	syl3anc	\|- ( ( ph /\ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ) -> ( ( U / n ) x. ( log ` n ) ) = ( U x. ( ( log ` n ) / n ) ) )
157	156	sumeq2dv	\|- ( ph -> sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) = sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( U x. ( ( log ` n ) / n ) ) )
158	148	recnd	\|- ( ph -> U e. CC )
159	26	recnd	\|- ( ( ph /\ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ) -> ( ( log ` n ) / n ) e. CC )
160	21 158 159	fsummulc2	\|- ( ph -> ( U x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) = sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( U x. ( ( log ` n ) / n ) ) )
161	157 160	eqtr4d	\|- ( ph -> sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) = ( U x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) )
162	161	oveq2d	\|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) = ( 2 x. ( U x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) )
163	27	recnd	\|- ( ph -> sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) e. CC )
164	127 158 163	mul12d	\|- ( ph -> ( 2 x. ( U x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) = ( U x. ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) )
165	162 164	eqtrd	\|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) = ( U x. ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( log ` n ) / n ) ) ) )
166	38	recnd	\|- ( ph -> ( ( log ` Z ) + 3 ) e. CC )
167	158 166 121	mulassd	\|- ( ph -> ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) = ( U x. ( ( ( log ` Z ) + 3 ) x. ( log ` Z ) ) ) )
168	147 165 167	3brtr4d	\|- ( ph -> ( 2 x. sum_ n e. ( 1 ... ( \|_ ` ( Z / Y ) ) ) ( ( U / n ) x. ( log ` n ) ) ) <_ ( ( U x. ( ( log ` Z ) + 3 ) ) x. ( log ` Z ) ) )

Metamath Proof Explorer

Theorem pntlemk

Proof