Theorem pntlemr

Description: Lemma for pntlemj . (Contributed by Mario Carneiro, 7-Jun-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 ) )
	pntlem1.o	|- O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) )
	pntlem1.v	|- ( ph -> V e. RR+ )
	pntlem1.V	|- ( ph -> ( ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
	pntlem1.j	|- ( ph -> J e. ( M ..^ N ) )
	pntlem1.i	|- I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) )
Assertion	pntlemr	|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) )

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		pntlem1.o	|- O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) )
21		pntlem1.v	|- ( ph -> V e. RR+ )
22		pntlem1.V	|- ( ph -> ( ( ( K ^ J ) < V /\ ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( V [,] ( ( 1 + ( L x. E ) ) x. V ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
23		pntlem1.j	|- ( ph -> J e. ( M ..^ N ) )
24		pntlem1.i	|- I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) )
25	1 2 3 4 5 6	pntlemd	|- ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
26	25	simp1d	|- ( ph -> L e. RR+ )
27	1 2 3 4 5 6 7 8 9 10	pntlemc	|- ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )
28	27	simp1d	|- ( ph -> E e. RR+ )
29	26 28	rpmulcld	|- ( ph -> ( L x. E ) e. RR+ )
30		4re	|- 4 e. RR
31		4pos	|- 0 < 4
32	30 31	elrpii	|- 4 e. RR+
33		rpdivcl	|- ( ( ( L x. E ) e. RR+ /\ 4 e. RR+ ) -> ( ( L x. E ) / 4 ) e. RR+ )
34	29 32 33	sylancl	|- ( ph -> ( ( L x. E ) / 4 ) e. RR+ )
35	34	rpred	|- ( ph -> ( ( L x. E ) / 4 ) e. RR )
36	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 ) ) ) ) )
37	36	simp1d	|- ( ph -> Z e. RR+ )
38	37 21	rpdivcld	|- ( ph -> ( Z / V ) e. RR+ )
39	38	rpred	|- ( ph -> ( Z / V ) e. RR )
40	35 39	remulcld	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) e. RR )
41		fzfid	|- ( ph -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) e. Fin )
42	24 41	eqeltrid	|- ( ph -> I e. Fin )
43		hashcl	|- ( I e. Fin -> ( # ` I ) e. NN0 )
44	42 43	syl	|- ( ph -> ( # ` I ) e. NN0 )
45	44	nn0red	|- ( ph -> ( # ` I ) e. RR )
46	40	recnd	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) e. CC )
47		1rp	|- 1 e. RR+
48		rpaddcl	|- ( ( 1 e. RR+ /\ ( L x. E ) e. RR+ ) -> ( 1 + ( L x. E ) ) e. RR+ )
49	47 29 48	sylancr	|- ( ph -> ( 1 + ( L x. E ) ) e. RR+ )
50	49 21	rpmulcld	|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) e. RR+ )
51	37 50	rpdivcld	|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR+ )
52	51	rpred	|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR )
53		reflcl	|- ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. RR )
54	52 53	syl	|- ( ph -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. RR )
55	54	recnd	|- ( ph -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. CC )
56		1cnd	|- ( ph -> 1 e. CC )
57	46 55 56	add32d	|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) + 1 ) = ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) )
58		peano2re	|- ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) e. RR -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) e. RR )
59	40 58	syl	|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) e. RR )
60	59 54	readdcld	|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) e. RR )
61		reflcl	|- ( ( Z / V ) e. RR -> ( |_ ` ( Z / V ) ) e. RR )
62	39 61	syl	|- ( ph -> ( |_ ` ( Z / V ) ) e. RR )
63		peano2re	|- ( ( |_ ` ( Z / V ) ) e. RR -> ( ( |_ ` ( Z / V ) ) + 1 ) e. RR )
64	62 63	syl	|- ( ph -> ( ( |_ ` ( Z / V ) ) + 1 ) e. RR )
65	29	rphalfcld	|- ( ph -> ( ( L x. E ) / 2 ) e. RR+ )
66	65 38	rpmulcld	|- ( ph -> ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) e. RR+ )
67	66	rpred	|- ( ph -> ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) e. RR )
68	67 52	readdcld	|- ( ph -> ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) e. RR )
69		rpdivcl	|- ( ( 4 e. RR+ /\ ( L x. E ) e. RR+ ) -> ( 4 / ( L x. E ) ) e. RR+ )
70	32 29 69	sylancr	|- ( ph -> ( 4 / ( L x. E ) ) e. RR+ )
71	70	rpred	|- ( ph -> ( 4 / ( L x. E ) ) e. RR )
72	37	rpsqrtcld	|- ( ph -> ( sqrt ` Z ) e. RR+ )
73	72	rpred	|- ( ph -> ( sqrt ` Z ) e. RR )
74	36	simp3d	|- ( ph -> ( ( 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 ) ) ) )
75	74	simp1d	|- ( ph -> ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) )
76	50	rpred	|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) e. RR )
77	27	simp2d	|- ( ph -> K e. RR+ )
78		elfzoelz	|- ( J e. ( M ..^ N ) -> J e. ZZ )
79	23 78	syl	|- ( ph -> J e. ZZ )
80	79	peano2zd	|- ( ph -> ( J + 1 ) e. ZZ )
81	77 80	rpexpcld	|- ( ph -> ( K ^ ( J + 1 ) ) e. RR+ )
82	81	rpred	|- ( ph -> ( K ^ ( J + 1 ) ) e. RR )
83	22	simplrd	|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( K x. ( K ^ J ) ) )
84	77	rpcnd	|- ( ph -> K e. CC )
85	77 79	rpexpcld	|- ( ph -> ( K ^ J ) e. RR+ )
86	85	rpcnd	|- ( ph -> ( K ^ J ) e. CC )
87	84 86	mulcomd	|- ( ph -> ( K x. ( K ^ J ) ) = ( ( K ^ J ) x. K ) )
88	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemg	|- ( ph -> ( M e. NN /\ N e. ( ZZ>= ` M ) /\ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) <_ ( N - M ) ) )
89	88	simp1d	|- ( ph -> M e. NN )
90		elfzouz	|- ( J e. ( M ..^ N ) -> J e. ( ZZ>= ` M ) )
91	23 90	syl	|- ( ph -> J e. ( ZZ>= ` M ) )
92		eluznn	|- ( ( M e. NN /\ J e. ( ZZ>= ` M ) ) -> J e. NN )
93	89 91 92	syl2anc	|- ( ph -> J e. NN )
94	93	nnnn0d	|- ( ph -> J e. NN0 )
95	84 94	expp1d	|- ( ph -> ( K ^ ( J + 1 ) ) = ( ( K ^ J ) x. K ) )
96	87 95	eqtr4d	|- ( ph -> ( K x. ( K ^ J ) ) = ( K ^ ( J + 1 ) ) )
97	83 96	breqtrd	|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( K ^ ( J + 1 ) ) )
98	76 82 97	ltled	|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) <_ ( K ^ ( J + 1 ) ) )
99		fzofzp1	|- ( J e. ( M ..^ N ) -> ( J + 1 ) e. ( M ... N ) )
100	23 99	syl	|- ( ph -> ( J + 1 ) e. ( M ... N ) )
101	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pntlemh	|- ( ( ph /\ ( J + 1 ) e. ( M ... N ) ) -> ( X < ( K ^ ( J + 1 ) ) /\ ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) ) )
102	100 101	mpdan	|- ( ph -> ( X < ( K ^ ( J + 1 ) ) /\ ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) ) )
103	102	simprd	|- ( ph -> ( K ^ ( J + 1 ) ) <_ ( sqrt ` Z ) )
104	76 82 73 98 103	letrd	|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) <_ ( sqrt ` Z ) )
105	76 73 72	lemul2d	|- ( ph -> ( ( ( 1 + ( L x. E ) ) x. V ) <_ ( sqrt ` Z ) <-> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) ) )
106	104 105	mpbid	|- ( ph -> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) )
107	37	rprege0d	|- ( ph -> ( Z e. RR /\ 0 <_ Z ) )
108		remsqsqrt	|- ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
109	107 108	syl	|- ( ph -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
110	106 109	breqtrd	|- ( ph -> ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ Z )
111	37	rpred	|- ( ph -> Z e. RR )
112	73 111 50	lemuldivd	|- ( ph -> ( ( ( sqrt ` Z ) x. ( ( 1 + ( L x. E ) ) x. V ) ) <_ Z <-> ( sqrt ` Z ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) )
113	110 112	mpbid	|- ( ph -> ( sqrt ` Z ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) )
114	21	rpcnd	|- ( ph -> V e. CC )
115	114	mullidd	|- ( ph -> ( 1 x. V ) = V )
116		1red	|- ( ph -> 1 e. RR )
117	49	rpred	|- ( ph -> ( 1 + ( L x. E ) ) e. RR )
118		1re	|- 1 e. RR
119		ltaddrp	|- ( ( 1 e. RR /\ ( L x. E ) e. RR+ ) -> 1 < ( 1 + ( L x. E ) ) )
120	118 29 119	sylancr	|- ( ph -> 1 < ( 1 + ( L x. E ) ) )
121	116 117 21 120	ltmul1dd	|- ( ph -> ( 1 x. V ) < ( ( 1 + ( L x. E ) ) x. V ) )
122	115 121	eqbrtrrd	|- ( ph -> V < ( ( 1 + ( L x. E ) ) x. V ) )
123	21 50 37	ltdiv2d	|- ( ph -> ( V < ( ( 1 + ( L x. E ) ) x. V ) <-> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) < ( Z / V ) ) )
124	122 123	mpbid	|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) < ( Z / V ) )
125	52 39 124	ltled	|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( Z / V ) )
126	73 52 39 113 125	letrd	|- ( ph -> ( sqrt ` Z ) <_ ( Z / V ) )
127	71 73 39 75 126	letrd	|- ( ph -> ( 4 / ( L x. E ) ) <_ ( Z / V ) )
128	71 39 39 127	leadd2dd	|- ( ph -> ( ( Z / V ) + ( 4 / ( L x. E ) ) ) <_ ( ( Z / V ) + ( Z / V ) ) )
129	38	rpcnd	|- ( ph -> ( Z / V ) e. CC )
130	129	2timesd	|- ( ph -> ( 2 x. ( Z / V ) ) = ( ( Z / V ) + ( Z / V ) ) )
131	128 130	breqtrrd	|- ( ph -> ( ( Z / V ) + ( 4 / ( L x. E ) ) ) <_ ( 2 x. ( Z / V ) ) )
132	39 71	readdcld	|- ( ph -> ( ( Z / V ) + ( 4 / ( L x. E ) ) ) e. RR )
133		2re	|- 2 e. RR
134		remulcl	|- ( ( 2 e. RR /\ ( Z / V ) e. RR ) -> ( 2 x. ( Z / V ) ) e. RR )
135	133 39 134	sylancr	|- ( ph -> ( 2 x. ( Z / V ) ) e. RR )
136	132 135 34	lemul2d	|- ( ph -> ( ( ( Z / V ) + ( 4 / ( L x. E ) ) ) <_ ( 2 x. ( Z / V ) ) <-> ( ( ( L x. E ) / 4 ) x. ( ( Z / V ) + ( 4 / ( L x. E ) ) ) ) <_ ( ( ( L x. E ) / 4 ) x. ( 2 x. ( Z / V ) ) ) ) )
137	131 136	mpbid	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( ( Z / V ) + ( 4 / ( L x. E ) ) ) ) <_ ( ( ( L x. E ) / 4 ) x. ( 2 x. ( Z / V ) ) ) )
138	34	rpcnd	|- ( ph -> ( ( L x. E ) / 4 ) e. CC )
139	70	rpcnd	|- ( ph -> ( 4 / ( L x. E ) ) e. CC )
140	138 129 139	adddid	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( ( Z / V ) + ( 4 / ( L x. E ) ) ) ) = ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( ( ( L x. E ) / 4 ) x. ( 4 / ( L x. E ) ) ) ) )
141	29	rpcnne0d	|- ( ph -> ( ( L x. E ) e. CC /\ ( L x. E ) =/= 0 ) )
142		rpcnne0	|- ( 4 e. RR+ -> ( 4 e. CC /\ 4 =/= 0 ) )
143	32 142	mp1i	|- ( ph -> ( 4 e. CC /\ 4 =/= 0 ) )
144		divcan6	|- ( ( ( ( L x. E ) e. CC /\ ( L x. E ) =/= 0 ) /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( ( ( L x. E ) / 4 ) x. ( 4 / ( L x. E ) ) ) = 1 )
145	141 143 144	syl2anc	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( 4 / ( L x. E ) ) ) = 1 )
146	145	oveq2d	|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( ( ( L x. E ) / 4 ) x. ( 4 / ( L x. E ) ) ) ) = ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) )
147	140 146	eqtrd	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( ( Z / V ) + ( 4 / ( L x. E ) ) ) ) = ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) )
148		2cnd	|- ( ph -> 2 e. CC )
149	138 148 129	mulassd	|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. 2 ) x. ( Z / V ) ) = ( ( ( L x. E ) / 4 ) x. ( 2 x. ( Z / V ) ) ) )
150	29	rpcnd	|- ( ph -> ( L x. E ) e. CC )
151		2rp	|- 2 e. RR+
152		rpcnne0	|- ( 2 e. RR+ -> ( 2 e. CC /\ 2 =/= 0 ) )
153	151 152	mp1i	|- ( ph -> ( 2 e. CC /\ 2 =/= 0 ) )
154		divdiv1	|- ( ( ( L x. E ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( L x. E ) / 2 ) / 2 ) = ( ( L x. E ) / ( 2 x. 2 ) ) )
155	150 153 153 154	syl3anc	|- ( ph -> ( ( ( L x. E ) / 2 ) / 2 ) = ( ( L x. E ) / ( 2 x. 2 ) ) )
156		2t2e4	|- ( 2 x. 2 ) = 4
157	156	oveq2i	|- ( ( L x. E ) / ( 2 x. 2 ) ) = ( ( L x. E ) / 4 )
158	155 157	eqtr2di	|- ( ph -> ( ( L x. E ) / 4 ) = ( ( ( L x. E ) / 2 ) / 2 ) )
159	158	oveq1d	|- ( ph -> ( ( ( L x. E ) / 4 ) x. 2 ) = ( ( ( ( L x. E ) / 2 ) / 2 ) x. 2 ) )
160	150	halfcld	|- ( ph -> ( ( L x. E ) / 2 ) e. CC )
161	153	simprd	|- ( ph -> 2 =/= 0 )
162	160 148 161	divcan1d	|- ( ph -> ( ( ( ( L x. E ) / 2 ) / 2 ) x. 2 ) = ( ( L x. E ) / 2 ) )
163	159 162	eqtrd	|- ( ph -> ( ( ( L x. E ) / 4 ) x. 2 ) = ( ( L x. E ) / 2 ) )
164	163	oveq1d	|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. 2 ) x. ( Z / V ) ) = ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) )
165	149 164	eqtr3d	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( 2 x. ( Z / V ) ) ) = ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) )
166	137 147 165	3brtr3d	|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) <_ ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) )
167		flle	|- ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) )
168	52 167	syl	|- ( ph -> ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) <_ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) )
169	59 54 67 52 166 168	le2addd	|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) <_ ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) )
170	65	rpred	|- ( ph -> ( ( L x. E ) / 2 ) e. RR )
171	49	rprecred	|- ( ph -> ( 1 / ( 1 + ( L x. E ) ) ) e. RR )
172	170 171	readdcld	|- ( ph -> ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) e. RR )
173	29	rpred	|- ( ph -> ( L x. E ) e. RR )
174	28	rpred	|- ( ph -> E e. RR )
175	26	rpred	|- ( ph -> L e. RR )
176		eliooord	|- ( L e. ( 0 (,) 1 ) -> ( 0 < L /\ L < 1 ) )
177	4 176	syl	|- ( ph -> ( 0 < L /\ L < 1 ) )
178	177	simprd	|- ( ph -> L < 1 )
179	175 116 28 178	ltmul1dd	|- ( ph -> ( L x. E ) < ( 1 x. E ) )
180	28	rpcnd	|- ( ph -> E e. CC )
181	180	mullidd	|- ( ph -> ( 1 x. E ) = E )
182	179 181	breqtrd	|- ( ph -> ( L x. E ) < E )
183	27	simp3d	|- ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
184	183	simp1d	|- ( ph -> E e. ( 0 (,) 1 ) )
185		eliooord	|- ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) )
186	184 185	syl	|- ( ph -> ( 0 < E /\ E < 1 ) )
187	186	simprd	|- ( ph -> E < 1 )
188	173 174 116 182 187	lttrd	|- ( ph -> ( L x. E ) < 1 )
189	173 116 116 188	ltadd2dd	|- ( ph -> ( 1 + ( L x. E ) ) < ( 1 + 1 ) )
190		df-2	|- 2 = ( 1 + 1 )
191	189 190	breqtrrdi	|- ( ph -> ( 1 + ( L x. E ) ) < 2 )
192	49	rpregt0d	|- ( ph -> ( ( 1 + ( L x. E ) ) e. RR /\ 0 < ( 1 + ( L x. E ) ) ) )
193	133	a1i	|- ( ph -> 2 e. RR )
194		2pos	|- 0 < 2
195	194	a1i	|- ( ph -> 0 < 2 )
196	29	rpregt0d	|- ( ph -> ( ( L x. E ) e. RR /\ 0 < ( L x. E ) ) )
197		ltdiv2	|- ( ( ( ( 1 + ( L x. E ) ) e. RR /\ 0 < ( 1 + ( L x. E ) ) ) /\ ( 2 e. RR /\ 0 < 2 ) /\ ( ( L x. E ) e. RR /\ 0 < ( L x. E ) ) ) -> ( ( 1 + ( L x. E ) ) < 2 <-> ( ( L x. E ) / 2 ) < ( ( L x. E ) / ( 1 + ( L x. E ) ) ) ) )
198	192 193 195 196 197	syl121anc	|- ( ph -> ( ( 1 + ( L x. E ) ) < 2 <-> ( ( L x. E ) / 2 ) < ( ( L x. E ) / ( 1 + ( L x. E ) ) ) ) )
199	191 198	mpbid	|- ( ph -> ( ( L x. E ) / 2 ) < ( ( L x. E ) / ( 1 + ( L x. E ) ) ) )
200	49	rpcnd	|- ( ph -> ( 1 + ( L x. E ) ) e. CC )
201	49	rpcnne0d	|- ( ph -> ( ( 1 + ( L x. E ) ) e. CC /\ ( 1 + ( L x. E ) ) =/= 0 ) )
202		divsubdir	|- ( ( ( 1 + ( L x. E ) ) e. CC /\ 1 e. CC /\ ( ( 1 + ( L x. E ) ) e. CC /\ ( 1 + ( L x. E ) ) =/= 0 ) ) -> ( ( ( 1 + ( L x. E ) ) - 1 ) / ( 1 + ( L x. E ) ) ) = ( ( ( 1 + ( L x. E ) ) / ( 1 + ( L x. E ) ) ) - ( 1 / ( 1 + ( L x. E ) ) ) ) )
203	200 56 201 202	syl3anc	|- ( ph -> ( ( ( 1 + ( L x. E ) ) - 1 ) / ( 1 + ( L x. E ) ) ) = ( ( ( 1 + ( L x. E ) ) / ( 1 + ( L x. E ) ) ) - ( 1 / ( 1 + ( L x. E ) ) ) ) )
204		ax-1cn	|- 1 e. CC
205		pncan2	|- ( ( 1 e. CC /\ ( L x. E ) e. CC ) -> ( ( 1 + ( L x. E ) ) - 1 ) = ( L x. E ) )
206	204 150 205	sylancr	|- ( ph -> ( ( 1 + ( L x. E ) ) - 1 ) = ( L x. E ) )
207	206	oveq1d	|- ( ph -> ( ( ( 1 + ( L x. E ) ) - 1 ) / ( 1 + ( L x. E ) ) ) = ( ( L x. E ) / ( 1 + ( L x. E ) ) ) )
208		divid	|- ( ( ( 1 + ( L x. E ) ) e. CC /\ ( 1 + ( L x. E ) ) =/= 0 ) -> ( ( 1 + ( L x. E ) ) / ( 1 + ( L x. E ) ) ) = 1 )
209	201 208	syl	|- ( ph -> ( ( 1 + ( L x. E ) ) / ( 1 + ( L x. E ) ) ) = 1 )
210	209	oveq1d	|- ( ph -> ( ( ( 1 + ( L x. E ) ) / ( 1 + ( L x. E ) ) ) - ( 1 / ( 1 + ( L x. E ) ) ) ) = ( 1 - ( 1 / ( 1 + ( L x. E ) ) ) ) )
211	203 207 210	3eqtr3d	|- ( ph -> ( ( L x. E ) / ( 1 + ( L x. E ) ) ) = ( 1 - ( 1 / ( 1 + ( L x. E ) ) ) ) )
212	199 211	breqtrd	|- ( ph -> ( ( L x. E ) / 2 ) < ( 1 - ( 1 / ( 1 + ( L x. E ) ) ) ) )
213	170 171 116	ltaddsubd	|- ( ph -> ( ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) < 1 <-> ( ( L x. E ) / 2 ) < ( 1 - ( 1 / ( 1 + ( L x. E ) ) ) ) ) )
214	212 213	mpbird	|- ( ph -> ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) < 1 )
215	172 116 38 214	ltmul1dd	|- ( ph -> ( ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) x. ( Z / V ) ) < ( 1 x. ( Z / V ) ) )
216		reccl	|- ( ( ( 1 + ( L x. E ) ) e. CC /\ ( 1 + ( L x. E ) ) =/= 0 ) -> ( 1 / ( 1 + ( L x. E ) ) ) e. CC )
217	201 216	syl	|- ( ph -> ( 1 / ( 1 + ( L x. E ) ) ) e. CC )
218	160 217 129	adddird	|- ( ph -> ( ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) x. ( Z / V ) ) = ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( ( 1 / ( 1 + ( L x. E ) ) ) x. ( Z / V ) ) ) )
219	200 114	mulcomd	|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) = ( V x. ( 1 + ( L x. E ) ) ) )
220	219	oveq2d	|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) = ( Z / ( V x. ( 1 + ( L x. E ) ) ) ) )
221	37	rpcnd	|- ( ph -> Z e. CC )
222	21	rpcnne0d	|- ( ph -> ( V e. CC /\ V =/= 0 ) )
223		divdiv1	|- ( ( Z e. CC /\ ( V e. CC /\ V =/= 0 ) /\ ( ( 1 + ( L x. E ) ) e. CC /\ ( 1 + ( L x. E ) ) =/= 0 ) ) -> ( ( Z / V ) / ( 1 + ( L x. E ) ) ) = ( Z / ( V x. ( 1 + ( L x. E ) ) ) ) )
224	221 222 201 223	syl3anc	|- ( ph -> ( ( Z / V ) / ( 1 + ( L x. E ) ) ) = ( Z / ( V x. ( 1 + ( L x. E ) ) ) ) )
225	49	rpne0d	|- ( ph -> ( 1 + ( L x. E ) ) =/= 0 )
226	129 200 225	divrec2d	|- ( ph -> ( ( Z / V ) / ( 1 + ( L x. E ) ) ) = ( ( 1 / ( 1 + ( L x. E ) ) ) x. ( Z / V ) ) )
227	220 224 226	3eqtr2d	|- ( ph -> ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) = ( ( 1 / ( 1 + ( L x. E ) ) ) x. ( Z / V ) ) )
228	227	oveq2d	|- ( ph -> ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) = ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( ( 1 / ( 1 + ( L x. E ) ) ) x. ( Z / V ) ) ) )
229	218 228	eqtr4d	|- ( ph -> ( ( ( ( L x. E ) / 2 ) + ( 1 / ( 1 + ( L x. E ) ) ) ) x. ( Z / V ) ) = ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) )
230	129	mullidd	|- ( ph -> ( 1 x. ( Z / V ) ) = ( Z / V ) )
231	215 229 230	3brtr3d	|- ( ph -> ( ( ( ( L x. E ) / 2 ) x. ( Z / V ) ) + ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) < ( Z / V ) )
232	60 68 39 169 231	lelttrd	|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) < ( Z / V ) )
233		fllep1	|- ( ( Z / V ) e. RR -> ( Z / V ) <_ ( ( |_ ` ( Z / V ) ) + 1 ) )
234	39 233	syl	|- ( ph -> ( Z / V ) <_ ( ( |_ ` ( Z / V ) ) + 1 ) )
235	60 39 64 232 234	ltletrd	|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + 1 ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) < ( ( |_ ` ( Z / V ) ) + 1 ) )
236	57 235	eqbrtrd	|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) + 1 ) < ( ( |_ ` ( Z / V ) ) + 1 ) )
237	40 54	readdcld	|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) e. RR )
238	237 62 116	ltadd1d	|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) < ( |_ ` ( Z / V ) ) <-> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) + 1 ) < ( ( |_ ` ( Z / V ) ) + 1 ) ) )
239	236 238	mpbird	|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) < ( |_ ` ( Z / V ) ) )
240	40 54 62	ltaddsubd	|- ( ph -> ( ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) + ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) < ( |_ ` ( Z / V ) ) <-> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) < ( ( |_ ` ( Z / V ) ) - ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) ) )
241	239 240	mpbid	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) < ( ( |_ ` ( Z / V ) ) - ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) )
242	39	flcld	|- ( ph -> ( |_ ` ( Z / V ) ) e. ZZ )
243		fzval3	|- ( ( |_ ` ( Z / V ) ) e. ZZ -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) )
244	242 243	syl	|- ( ph -> ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ... ( |_ ` ( Z / V ) ) ) = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) )
245	24 244	eqtrid	|- ( ph -> I = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) )
246	245	fveq2d	|- ( ph -> ( # ` I ) = ( # ` ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) ) )
247		flword2	|- ( ( ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) e. RR /\ ( Z / V ) e. RR /\ ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) <_ ( Z / V ) ) -> ( |_ ` ( Z / V ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) )
248	52 39 125 247	syl3anc	|- ( ph -> ( |_ ` ( Z / V ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) )
249		eluzp1p1	|- ( ( |_ ` ( Z / V ) ) e. ( ZZ>= ` ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) -> ( ( |_ ` ( Z / V ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) )
250	248 249	syl	|- ( ph -> ( ( |_ ` ( Z / V ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) )
251		hashfzo	|- ( ( ( |_ ` ( Z / V ) ) + 1 ) e. ( ZZ>= ` ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) -> ( # ` ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) ) = ( ( ( |_ ` ( Z / V ) ) + 1 ) - ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) )
252	250 251	syl	|- ( ph -> ( # ` ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ..^ ( ( |_ ` ( Z / V ) ) + 1 ) ) ) = ( ( ( |_ ` ( Z / V ) ) + 1 ) - ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) )
253	62	recnd	|- ( ph -> ( |_ ` ( Z / V ) ) e. CC )
254	253 55 56	pnpcan2d	|- ( ph -> ( ( ( |_ ` ( Z / V ) ) + 1 ) - ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) + 1 ) ) = ( ( |_ ` ( Z / V ) ) - ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) )
255	246 252 254	3eqtrd	|- ( ph -> ( # ` I ) = ( ( |_ ` ( Z / V ) ) - ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. V ) ) ) ) )
256	241 255	breqtrrd	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) < ( # ` I ) )
257	40 45 256	ltled	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) <_ ( # ` I ) )
258	35 45 38	lemuldivd	|- ( ph -> ( ( ( ( L x. E ) / 4 ) x. ( Z / V ) ) <_ ( # ` I ) <-> ( ( L x. E ) / 4 ) <_ ( ( # ` I ) / ( Z / V ) ) ) )
259	257 258	mpbid	|- ( ph -> ( ( L x. E ) / 4 ) <_ ( ( # ` I ) / ( Z / V ) ) )
260	21	rpred	|- ( ph -> V e. RR )
261	76 82 73 97 103	ltletrd	|- ( ph -> ( ( 1 + ( L x. E ) ) x. V ) < ( sqrt ` Z ) )
262	260 76 73 122 261	lttrd	|- ( ph -> V < ( sqrt ` Z ) )
263	260 73 262	ltled	|- ( ph -> V <_ ( sqrt ` Z ) )
264	21	rprege0d	|- ( ph -> ( V e. RR /\ 0 <_ V ) )
265	72	rprege0d	|- ( ph -> ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) )
266		le2sq	|- ( ( ( V e. RR /\ 0 <_ V ) /\ ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) ) -> ( V <_ ( sqrt ` Z ) <-> ( V ^ 2 ) <_ ( ( sqrt ` Z ) ^ 2 ) ) )
267	264 265 266	syl2anc	|- ( ph -> ( V <_ ( sqrt ` Z ) <-> ( V ^ 2 ) <_ ( ( sqrt ` Z ) ^ 2 ) ) )
268	263 267	mpbid	|- ( ph -> ( V ^ 2 ) <_ ( ( sqrt ` Z ) ^ 2 ) )
269		resqrtth	|- ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) ^ 2 ) = Z )
270	107 269	syl	|- ( ph -> ( ( sqrt ` Z ) ^ 2 ) = Z )
271	268 270	breqtrd	|- ( ph -> ( V ^ 2 ) <_ Z )
272		2z	|- 2 e. ZZ
273		rpexpcl	|- ( ( V e. RR+ /\ 2 e. ZZ ) -> ( V ^ 2 ) e. RR+ )
274	21 272 273	sylancl	|- ( ph -> ( V ^ 2 ) e. RR+ )
275	274	rpred	|- ( ph -> ( V ^ 2 ) e. RR )
276	275 111 37	lemul2d	|- ( ph -> ( ( V ^ 2 ) <_ Z <-> ( Z x. ( V ^ 2 ) ) <_ ( Z x. Z ) ) )
277	271 276	mpbid	|- ( ph -> ( Z x. ( V ^ 2 ) ) <_ ( Z x. Z ) )
278	221	sqvald	|- ( ph -> ( Z ^ 2 ) = ( Z x. Z ) )
279	277 278	breqtrrd	|- ( ph -> ( Z x. ( V ^ 2 ) ) <_ ( Z ^ 2 ) )
280	111	resqcld	|- ( ph -> ( Z ^ 2 ) e. RR )
281	111 280 274	lemuldivd	|- ( ph -> ( ( Z x. ( V ^ 2 ) ) <_ ( Z ^ 2 ) <-> Z <_ ( ( Z ^ 2 ) / ( V ^ 2 ) ) ) )
282	279 281	mpbid	|- ( ph -> Z <_ ( ( Z ^ 2 ) / ( V ^ 2 ) ) )
283	21	rpne0d	|- ( ph -> V =/= 0 )
284	221 114 283	sqdivd	|- ( ph -> ( ( Z / V ) ^ 2 ) = ( ( Z ^ 2 ) / ( V ^ 2 ) ) )
285	282 284	breqtrrd	|- ( ph -> Z <_ ( ( Z / V ) ^ 2 ) )
286		rpexpcl	|- ( ( ( Z / V ) e. RR+ /\ 2 e. ZZ ) -> ( ( Z / V ) ^ 2 ) e. RR+ )
287	38 272 286	sylancl	|- ( ph -> ( ( Z / V ) ^ 2 ) e. RR+ )
288	37 287	logled	|- ( ph -> ( Z <_ ( ( Z / V ) ^ 2 ) <-> ( log ` Z ) <_ ( log ` ( ( Z / V ) ^ 2 ) ) ) )
289	285 288	mpbid	|- ( ph -> ( log ` Z ) <_ ( log ` ( ( Z / V ) ^ 2 ) ) )
290		relogexp	|- ( ( ( Z / V ) e. RR+ /\ 2 e. ZZ ) -> ( log ` ( ( Z / V ) ^ 2 ) ) = ( 2 x. ( log ` ( Z / V ) ) ) )
291	38 272 290	sylancl	|- ( ph -> ( log ` ( ( Z / V ) ^ 2 ) ) = ( 2 x. ( log ` ( Z / V ) ) ) )
292	289 291	breqtrd	|- ( ph -> ( log ` Z ) <_ ( 2 x. ( log ` ( Z / V ) ) ) )
293	37	relogcld	|- ( ph -> ( log ` Z ) e. RR )
294	38	relogcld	|- ( ph -> ( log ` ( Z / V ) ) e. RR )
295		ledivmul	|- ( ( ( log ` Z ) e. RR /\ ( log ` ( Z / V ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( log ` Z ) / 2 ) <_ ( log ` ( Z / V ) ) <-> ( log ` Z ) <_ ( 2 x. ( log ` ( Z / V ) ) ) ) )
296	293 294 193 195 295	syl112anc	|- ( ph -> ( ( ( log ` Z ) / 2 ) <_ ( log ` ( Z / V ) ) <-> ( log ` Z ) <_ ( 2 x. ( log ` ( Z / V ) ) ) ) )
297	292 296	mpbird	|- ( ph -> ( ( log ` Z ) / 2 ) <_ ( log ` ( Z / V ) ) )
298	34	rprege0d	|- ( ph -> ( ( ( L x. E ) / 4 ) e. RR /\ 0 <_ ( ( L x. E ) / 4 ) ) )
299	45 38	rerpdivcld	|- ( ph -> ( ( # ` I ) / ( Z / V ) ) e. RR )
300	36	simp2d	|- ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) )
301	300	simp1d	|- ( ph -> 1 < Z )
302	111 301	rplogcld	|- ( ph -> ( log ` Z ) e. RR+ )
303	302	rphalfcld	|- ( ph -> ( ( log ` Z ) / 2 ) e. RR+ )
304	303	rprege0d	|- ( ph -> ( ( ( log ` Z ) / 2 ) e. RR /\ 0 <_ ( ( log ` Z ) / 2 ) ) )
305		lemul12a	|- ( ( ( ( ( ( L x. E ) / 4 ) e. RR /\ 0 <_ ( ( L x. E ) / 4 ) ) /\ ( ( # ` I ) / ( Z / V ) ) e. RR ) /\ ( ( ( ( log ` Z ) / 2 ) e. RR /\ 0 <_ ( ( log ` Z ) / 2 ) ) /\ ( log ` ( Z / V ) ) e. RR ) ) -> ( ( ( ( L x. E ) / 4 ) <_ ( ( # ` I ) / ( Z / V ) ) /\ ( ( log ` Z ) / 2 ) <_ ( log ` ( Z / V ) ) ) -> ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) <_ ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) ) )
306	298 299 304 294 305	syl22anc	|- ( ph -> ( ( ( ( L x. E ) / 4 ) <_ ( ( # ` I ) / ( Z / V ) ) /\ ( ( log ` Z ) / 2 ) <_ ( log ` ( Z / V ) ) ) -> ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) <_ ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) ) )
307	259 297 306	mp2and	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) <_ ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) )
308	302	rpcnd	|- ( ph -> ( log ` Z ) e. CC )
309		8nn	|- 8 e. NN
310		nnrp	|- ( 8 e. NN -> 8 e. RR+ )
311	309 310	ax-mp	|- 8 e. RR+
312		rpcnne0	|- ( 8 e. RR+ -> ( 8 e. CC /\ 8 =/= 0 ) )
313	311 312	mp1i	|- ( ph -> ( 8 e. CC /\ 8 =/= 0 ) )
314		div23	|- ( ( ( L x. E ) e. CC /\ ( log ` Z ) e. CC /\ ( 8 e. CC /\ 8 =/= 0 ) ) -> ( ( ( L x. E ) x. ( log ` Z ) ) / 8 ) = ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) )
315	150 308 313 314	syl3anc	|- ( ph -> ( ( ( L x. E ) x. ( log ` Z ) ) / 8 ) = ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) )
316		divmuldiv	|- ( ( ( ( L x. E ) e. CC /\ ( log ` Z ) e. CC ) /\ ( ( 4 e. CC /\ 4 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) ) -> ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) = ( ( ( L x. E ) x. ( log ` Z ) ) / ( 4 x. 2 ) ) )
317	150 308 143 153 316	syl22anc	|- ( ph -> ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) = ( ( ( L x. E ) x. ( log ` Z ) ) / ( 4 x. 2 ) ) )
318		4t2e8	|- ( 4 x. 2 ) = 8
319	318	oveq2i	|- ( ( ( L x. E ) x. ( log ` Z ) ) / ( 4 x. 2 ) ) = ( ( ( L x. E ) x. ( log ` Z ) ) / 8 )
320	317 319	eqtr2di	|- ( ph -> ( ( ( L x. E ) x. ( log ` Z ) ) / 8 ) = ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) )
321	315 320	eqtr3d	|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) = ( ( ( L x. E ) / 4 ) x. ( ( log ` Z ) / 2 ) ) )
322	45	recnd	|- ( ph -> ( # ` I ) e. CC )
323	294	recnd	|- ( ph -> ( log ` ( Z / V ) ) e. CC )
324	38	rpcnne0d	|- ( ph -> ( ( Z / V ) e. CC /\ ( Z / V ) =/= 0 ) )
325		divass	|- ( ( ( # ` I ) e. CC /\ ( log ` ( Z / V ) ) e. CC /\ ( ( Z / V ) e. CC /\ ( Z / V ) =/= 0 ) ) -> ( ( ( # ` I ) x. ( log ` ( Z / V ) ) ) / ( Z / V ) ) = ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) )
326		div23	|- ( ( ( # ` I ) e. CC /\ ( log ` ( Z / V ) ) e. CC /\ ( ( Z / V ) e. CC /\ ( Z / V ) =/= 0 ) ) -> ( ( ( # ` I ) x. ( log ` ( Z / V ) ) ) / ( Z / V ) ) = ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) )
327	325 326	eqtr3d	|- ( ( ( # ` I ) e. CC /\ ( log ` ( Z / V ) ) e. CC /\ ( ( Z / V ) e. CC /\ ( Z / V ) =/= 0 ) ) -> ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) )
328	322 323 324 327	syl3anc	|- ( ph -> ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) = ( ( ( # ` I ) / ( Z / V ) ) x. ( log ` ( Z / V ) ) ) )
329	307 321 328	3brtr4d	|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) <_ ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) )
330		rpdivcl	|- ( ( ( L x. E ) e. RR+ /\ 8 e. RR+ ) -> ( ( L x. E ) / 8 ) e. RR+ )
331	29 311 330	sylancl	|- ( ph -> ( ( L x. E ) / 8 ) e. RR+ )
332	331 302	rpmulcld	|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) e. RR+ )
333	332	rpred	|- ( ph -> ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) e. RR )
334	294 38	rerpdivcld	|- ( ph -> ( ( log ` ( Z / V ) ) / ( Z / V ) ) e. RR )
335	45 334	remulcld	|- ( ph -> ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) e. RR )
336	183	simp3d	|- ( ph -> ( U - E ) e. RR+ )
337	333 335 336	lemul2d	|- ( ph -> ( ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) <_ ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) <-> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ ( ( U - E ) x. ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) ) )
338	329 337	mpbid	|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ ( ( U - E ) x. ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) )
339	336	rpcnd	|- ( ph -> ( U - E ) e. CC )
340	334	recnd	|- ( ph -> ( ( log ` ( Z / V ) ) / ( Z / V ) ) e. CC )
341	339 322 340	mul12d	|- ( ph -> ( ( U - E ) x. ( ( # ` I ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) = ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) )
342	338 341	breqtrd	|- ( ph -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ ( ( # ` I ) x. ( ( U - E ) x. ( ( log ` ( Z / V ) ) / ( Z / V ) ) ) ) )