Theorem pntlemb

Description: Lemma for pnt . Unpack all the lower bounds contained in W , in the form they will be used. For comparison with Equation 10.6.27 of Shapiro, p. 434, Z is x. (Contributed by Mario Carneiro, 13-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 ) )
Assertion	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 ) ) ) ) )

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	1 2 3 4 5 6 7 8 9 10 11 12 13 14	pntlema	|- ( ph -> W e. RR+ )
17	16	rpred	|- ( ph -> W e. RR )
18		pnfxr	|- +oo e. RR*
19		elico2	|- ( ( W e. RR /\ +oo e. RR* ) -> ( Z e. ( W [,) +oo ) <-> ( Z e. RR /\ W <_ Z /\ Z < +oo ) ) )
20	17 18 19	sylancl	|- ( ph -> ( Z e. ( W [,) +oo ) <-> ( Z e. RR /\ W <_ Z /\ Z < +oo ) ) )
21	15 20	mpbid	|- ( ph -> ( Z e. RR /\ W <_ Z /\ Z < +oo ) )
22	21	simp1d	|- ( ph -> Z e. RR )
23	21	simp2d	|- ( ph -> W <_ Z )
24	22 16 23	rpgecld	|- ( ph -> Z e. RR+ )
25		1re	|- 1 e. RR
26	25	a1i	|- ( ph -> 1 e. RR )
27		ere	|- _e e. RR
28	27	a1i	|- ( ph -> _e e. RR )
29	24	rpsqrtcld	|- ( ph -> ( sqrt ` Z ) e. RR+ )
30	29	rpred	|- ( ph -> ( sqrt ` Z ) e. RR )
31		1lt2	|- 1 < 2
32		egt2lt3	|- ( 2 < _e /\ _e < 3 )
33	32	simpli	|- 2 < _e
34		2re	|- 2 e. RR
35	25 34 27	lttri	|- ( ( 1 < 2 /\ 2 < _e ) -> 1 < _e )
36	31 33 35	mp2an	|- 1 < _e
37	36	a1i	|- ( ph -> 1 < _e )
38		4re	|- 4 e. RR
39	38	a1i	|- ( ph -> 4 e. RR )
40	32	simpri	|- _e < 3
41		3lt4	|- 3 < 4
42		3re	|- 3 e. RR
43	27 42 38	lttri	|- ( ( _e < 3 /\ 3 < 4 ) -> _e < 4 )
44	40 41 43	mp2an	|- _e < 4
45	44	a1i	|- ( ph -> _e < 4 )
46		4nn	|- 4 e. NN
47		nnrp	|- ( 4 e. NN -> 4 e. RR+ )
48	46 47	ax-mp	|- 4 e. RR+
49	1 2 3 4 5 6	pntlemd	|- ( ph -> ( L e. RR+ /\ D e. RR+ /\ F e. RR+ ) )
50	49	simp1d	|- ( ph -> L e. RR+ )
51	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+ ) ) )
52	51	simp1d	|- ( ph -> E e. RR+ )
53	50 52	rpmulcld	|- ( ph -> ( L x. E ) e. RR+ )
54		rpdivcl	|- ( ( 4 e. RR+ /\ ( L x. E ) e. RR+ ) -> ( 4 / ( L x. E ) ) e. RR+ )
55	48 53 54	sylancr	|- ( ph -> ( 4 / ( L x. E ) ) e. RR+ )
56	55	rpred	|- ( ph -> ( 4 / ( L x. E ) ) e. RR )
57	53	rpred	|- ( ph -> ( L x. E ) e. RR )
58	52	rpred	|- ( ph -> E e. RR )
59	50	rpred	|- ( ph -> L e. RR )
60		eliooord	|- ( L e. ( 0 (,) 1 ) -> ( 0 < L /\ L < 1 ) )
61	4 60	syl	|- ( ph -> ( 0 < L /\ L < 1 ) )
62	61	simprd	|- ( ph -> L < 1 )
63	59 26 52 62	ltmul1dd	|- ( ph -> ( L x. E ) < ( 1 x. E ) )
64	52	rpcnd	|- ( ph -> E e. CC )
65	64	mulid2d	|- ( ph -> ( 1 x. E ) = E )
66	63 65	breqtrd	|- ( ph -> ( L x. E ) < E )
67	51	simp3d	|- ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
68	67	simp1d	|- ( ph -> E e. ( 0 (,) 1 ) )
69		eliooord	|- ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) )
70	68 69	syl	|- ( ph -> ( 0 < E /\ E < 1 ) )
71	70	simprd	|- ( ph -> E < 1 )
72	57 58 26 66 71	lttrd	|- ( ph -> ( L x. E ) < 1 )
73		4pos	|- 0 < 4
74	39 73	jctir	|- ( ph -> ( 4 e. RR /\ 0 < 4 ) )
75		ltmul2	|- ( ( ( L x. E ) e. RR /\ 1 e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( L x. E ) < 1 <-> ( 4 x. ( L x. E ) ) < ( 4 x. 1 ) ) )
76	57 26 74 75	syl3anc	|- ( ph -> ( ( L x. E ) < 1 <-> ( 4 x. ( L x. E ) ) < ( 4 x. 1 ) ) )
77	72 76	mpbid	|- ( ph -> ( 4 x. ( L x. E ) ) < ( 4 x. 1 ) )
78		4cn	|- 4 e. CC
79	78	mulid1i	|- ( 4 x. 1 ) = 4
80	77 79	breqtrdi	|- ( ph -> ( 4 x. ( L x. E ) ) < 4 )
81	39 39 53	ltmuldivd	|- ( ph -> ( ( 4 x. ( L x. E ) ) < 4 <-> 4 < ( 4 / ( L x. E ) ) ) )
82	80 81	mpbid	|- ( ph -> 4 < ( 4 / ( L x. E ) ) )
83	11	simpld	|- ( ph -> Y e. RR+ )
84	83 55	rpaddcld	|- ( ph -> ( Y + ( 4 / ( L x. E ) ) ) e. RR+ )
85	84	rpred	|- ( ph -> ( Y + ( 4 / ( L x. E ) ) ) e. RR )
86	56 83	ltaddrp2d	|- ( ph -> ( 4 / ( L x. E ) ) < ( Y + ( 4 / ( L x. E ) ) ) )
87	85	resqcld	|- ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) e. RR )
88	12	simpld	|- ( ph -> X e. RR+ )
89	51	simp2d	|- ( ph -> K e. RR+ )
90		2z	|- 2 e. ZZ
91		rpexpcl	|- ( ( K e. RR+ /\ 2 e. ZZ ) -> ( K ^ 2 ) e. RR+ )
92	89 90 91	sylancl	|- ( ph -> ( K ^ 2 ) e. RR+ )
93	88 92	rpmulcld	|- ( ph -> ( X x. ( K ^ 2 ) ) e. RR+ )
94		4z	|- 4 e. ZZ
95		rpexpcl	|- ( ( ( X x. ( K ^ 2 ) ) e. RR+ /\ 4 e. ZZ ) -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) e. RR+ )
96	93 94 95	sylancl	|- ( ph -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) e. RR+ )
97		3nn0	|- 3 e. NN0
98		2nn	|- 2 e. NN
99	97 98	decnncl	|- ; 3 2 e. NN
100		nnrp	|- ( ; 3 2 e. NN -> ; 3 2 e. RR+ )
101	99 100	ax-mp	|- ; 3 2 e. RR+
102		rpmulcl	|- ( ( ; 3 2 e. RR+ /\ B e. RR+ ) -> ( ; 3 2 x. B ) e. RR+ )
103	101 3 102	sylancr	|- ( ph -> ( ; 3 2 x. B ) e. RR+ )
104	67	simp3d	|- ( ph -> ( U - E ) e. RR+ )
105		rpexpcl	|- ( ( E e. RR+ /\ 2 e. ZZ ) -> ( E ^ 2 ) e. RR+ )
106	52 90 105	sylancl	|- ( ph -> ( E ^ 2 ) e. RR+ )
107	50 106	rpmulcld	|- ( ph -> ( L x. ( E ^ 2 ) ) e. RR+ )
108	104 107	rpmulcld	|- ( ph -> ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) e. RR+ )
109	103 108	rpdivcld	|- ( ph -> ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) e. RR+ )
110		3rp	|- 3 e. RR+
111		rpmulcl	|- ( ( U e. RR+ /\ 3 e. RR+ ) -> ( U x. 3 ) e. RR+ )
112	7 110 111	sylancl	|- ( ph -> ( U x. 3 ) e. RR+ )
113	112 13	rpaddcld	|- ( ph -> ( ( U x. 3 ) + C ) e. RR+ )
114	109 113	rpmulcld	|- ( ph -> ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) e. RR+ )
115	114	rpred	|- ( ph -> ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) e. RR )
116	115	rpefcld	|- ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) e. RR+ )
117	96 116	rpaddcld	|- ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) e. RR+ )
118	87 117	ltaddrpd	|- ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < ( ( ( 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 ) ) ) ) ) )
119	118 14	breqtrrdi	|- ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < W )
120	87 17 22 119 23	ltletrd	|- ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < Z )
121	24	rprege0d	|- ( ph -> ( Z e. RR /\ 0 <_ Z ) )
122		resqrtth	|- ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) ^ 2 ) = Z )
123	121 122	syl	|- ( ph -> ( ( sqrt ` Z ) ^ 2 ) = Z )
124	120 123	breqtrrd	|- ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) )
125	84	rprege0d	|- ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) e. RR /\ 0 <_ ( Y + ( 4 / ( L x. E ) ) ) ) )
126	29	rprege0d	|- ( ph -> ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) )
127		lt2sq	|- ( ( ( ( Y + ( 4 / ( L x. E ) ) ) e. RR /\ 0 <_ ( Y + ( 4 / ( L x. E ) ) ) ) /\ ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) ) -> ( ( Y + ( 4 / ( L x. E ) ) ) < ( sqrt ` Z ) <-> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) ) )
128	125 126 127	syl2anc	|- ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) < ( sqrt ` Z ) <-> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) ) )
129	124 128	mpbird	|- ( ph -> ( Y + ( 4 / ( L x. E ) ) ) < ( sqrt ` Z ) )
130	56 85 30 86 129	lttrd	|- ( ph -> ( 4 / ( L x. E ) ) < ( sqrt ` Z ) )
131	39 56 30 82 130	lttrd	|- ( ph -> 4 < ( sqrt ` Z ) )
132	28 39 30 45 131	lttrd	|- ( ph -> _e < ( sqrt ` Z ) )
133	26 28 30 37 132	lttrd	|- ( ph -> 1 < ( sqrt ` Z ) )
134		0le1	|- 0 <_ 1
135	134	a1i	|- ( ph -> 0 <_ 1 )
136		lt2sq	|- ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( ( sqrt ` Z ) e. RR /\ 0 <_ ( sqrt ` Z ) ) ) -> ( 1 < ( sqrt ` Z ) <-> ( 1 ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) ) )
137	26 135 126 136	syl21anc	|- ( ph -> ( 1 < ( sqrt ` Z ) <-> ( 1 ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) ) )
138	133 137	mpbid	|- ( ph -> ( 1 ^ 2 ) < ( ( sqrt ` Z ) ^ 2 ) )
139		sq1	|- ( 1 ^ 2 ) = 1
140	139	a1i	|- ( ph -> ( 1 ^ 2 ) = 1 )
141	138 140 123	3brtr3d	|- ( ph -> 1 < Z )
142	28 30 132	ltled	|- ( ph -> _e <_ ( sqrt ` Z ) )
143	22 83	rerpdivcld	|- ( ph -> ( Z / Y ) e. RR )
144	83	rpred	|- ( ph -> Y e. RR )
145	144 55	ltaddrpd	|- ( ph -> Y < ( Y + ( 4 / ( L x. E ) ) ) )
146	144 85 30 145 129	lttrd	|- ( ph -> Y < ( sqrt ` Z ) )
147	144 30 29 146	ltmul2dd	|- ( ph -> ( ( sqrt ` Z ) x. Y ) < ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) )
148		remsqsqrt	|- ( ( Z e. RR /\ 0 <_ Z ) -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
149	121 148	syl	|- ( ph -> ( ( sqrt ` Z ) x. ( sqrt ` Z ) ) = Z )
150	147 149	breqtrd	|- ( ph -> ( ( sqrt ` Z ) x. Y ) < Z )
151	30 22 83	ltmuldivd	|- ( ph -> ( ( ( sqrt ` Z ) x. Y ) < Z <-> ( sqrt ` Z ) < ( Z / Y ) ) )
152	150 151	mpbid	|- ( ph -> ( sqrt ` Z ) < ( Z / Y ) )
153	30 143 152	ltled	|- ( ph -> ( sqrt ` Z ) <_ ( Z / Y ) )
154	141 142 153	3jca	|- ( ph -> ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) )
155	56 30 130	ltled	|- ( ph -> ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) )
156	88	relogcld	|- ( ph -> ( log ` X ) e. RR )
157	89	rpred	|- ( ph -> K e. RR )
158	67	simp2d	|- ( ph -> 1 < K )
159	157 158	rplogcld	|- ( ph -> ( log ` K ) e. RR+ )
160	156 159	rerpdivcld	|- ( ph -> ( ( log ` X ) / ( log ` K ) ) e. RR )
161		readdcl	|- ( ( ( ( log ` X ) / ( log ` K ) ) e. RR /\ 2 e. RR ) -> ( ( ( log ` X ) / ( log ` K ) ) + 2 ) e. RR )
162	160 34 161	sylancl	|- ( ph -> ( ( ( log ` X ) / ( log ` K ) ) + 2 ) e. RR )
163	24	relogcld	|- ( ph -> ( log ` Z ) e. RR )
164	163 159	rerpdivcld	|- ( ph -> ( ( log ` Z ) / ( log ` K ) ) e. RR )
165		nndivre	|- ( ( ( ( log ` Z ) / ( log ` K ) ) e. RR /\ 4 e. NN ) -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR )
166	164 46 165	sylancl	|- ( ph -> ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) e. RR )
167	93	relogcld	|- ( ph -> ( log ` ( X x. ( K ^ 2 ) ) ) e. RR )
168		nndivre	|- ( ( ( log ` Z ) e. RR /\ 4 e. NN ) -> ( ( log ` Z ) / 4 ) e. RR )
169	163 46 168	sylancl	|- ( ph -> ( ( log ` Z ) / 4 ) e. RR )
170		relogexp	|- ( ( ( X x. ( K ^ 2 ) ) e. RR+ /\ 4 e. ZZ ) -> ( log ` ( ( X x. ( K ^ 2 ) ) ^ 4 ) ) = ( 4 x. ( log ` ( X x. ( K ^ 2 ) ) ) ) )
171	93 94 170	sylancl	|- ( ph -> ( log ` ( ( X x. ( K ^ 2 ) ) ^ 4 ) ) = ( 4 x. ( log ` ( X x. ( K ^ 2 ) ) ) ) )
172	96	rpred	|- ( ph -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) e. RR )
173	117	rpred	|- ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) e. RR )
174	172 116	ltaddrpd	|- ( ph -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) < ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
175		rpexpcl	|- ( ( ( Y + ( 4 / ( L x. E ) ) ) e. RR+ /\ 2 e. ZZ ) -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) e. RR+ )
176	84 90 175	sylancl	|- ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) e. RR+ )
177	173 176	ltaddrpd	|- ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) < ( ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) + ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) ) )
178	87	recnd	|- ( ph -> ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) e. CC )
179	117	rpcnd	|- ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) e. CC )
180	178 179	addcomd	|- ( ph -> ( ( ( 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 ) ) ) ) ) = ( ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) + ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) ) )
181	14 180	eqtrid	|- ( ph -> W = ( ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) + ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) ) )
182	177 181	breqtrrd	|- ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) < W )
183	173 17 22 182 23	ltletrd	|- ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) < Z )
184	172 173 22 174 183	lttrd	|- ( ph -> ( ( X x. ( K ^ 2 ) ) ^ 4 ) < Z )
185		logltb	|- ( ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) e. RR+ /\ Z e. RR+ ) -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) < Z <-> ( log ` ( ( X x. ( K ^ 2 ) ) ^ 4 ) ) < ( log ` Z ) ) )
186	96 24 185	syl2anc	|- ( ph -> ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) < Z <-> ( log ` ( ( X x. ( K ^ 2 ) ) ^ 4 ) ) < ( log ` Z ) ) )
187	184 186	mpbid	|- ( ph -> ( log ` ( ( X x. ( K ^ 2 ) ) ^ 4 ) ) < ( log ` Z ) )
188	171 187	eqbrtrrd	|- ( ph -> ( 4 x. ( log ` ( X x. ( K ^ 2 ) ) ) ) < ( log ` Z ) )
189		ltmuldiv2	|- ( ( ( log ` ( X x. ( K ^ 2 ) ) ) e. RR /\ ( log ` Z ) e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( 4 x. ( log ` ( X x. ( K ^ 2 ) ) ) ) < ( log ` Z ) <-> ( log ` ( X x. ( K ^ 2 ) ) ) < ( ( log ` Z ) / 4 ) ) )
190	167 163 74 189	syl3anc	|- ( ph -> ( ( 4 x. ( log ` ( X x. ( K ^ 2 ) ) ) ) < ( log ` Z ) <-> ( log ` ( X x. ( K ^ 2 ) ) ) < ( ( log ` Z ) / 4 ) ) )
191	188 190	mpbid	|- ( ph -> ( log ` ( X x. ( K ^ 2 ) ) ) < ( ( log ` Z ) / 4 ) )
192	167 169 159 191	ltdiv1dd	|- ( ph -> ( ( log ` ( X x. ( K ^ 2 ) ) ) / ( log ` K ) ) < ( ( ( log ` Z ) / 4 ) / ( log ` K ) ) )
193	88 92	relogmuld	|- ( ph -> ( log ` ( X x. ( K ^ 2 ) ) ) = ( ( log ` X ) + ( log ` ( K ^ 2 ) ) ) )
194		relogexp	|- ( ( K e. RR+ /\ 2 e. ZZ ) -> ( log ` ( K ^ 2 ) ) = ( 2 x. ( log ` K ) ) )
195	89 90 194	sylancl	|- ( ph -> ( log ` ( K ^ 2 ) ) = ( 2 x. ( log ` K ) ) )
196	195	oveq2d	|- ( ph -> ( ( log ` X ) + ( log ` ( K ^ 2 ) ) ) = ( ( log ` X ) + ( 2 x. ( log ` K ) ) ) )
197	193 196	eqtrd	|- ( ph -> ( log ` ( X x. ( K ^ 2 ) ) ) = ( ( log ` X ) + ( 2 x. ( log ` K ) ) ) )
198	197	oveq1d	|- ( ph -> ( ( log ` ( X x. ( K ^ 2 ) ) ) / ( log ` K ) ) = ( ( ( log ` X ) + ( 2 x. ( log ` K ) ) ) / ( log ` K ) ) )
199	156	recnd	|- ( ph -> ( log ` X ) e. CC )
200		2cnd	|- ( ph -> 2 e. CC )
201	159	rpcnd	|- ( ph -> ( log ` K ) e. CC )
202	200 201	mulcld	|- ( ph -> ( 2 x. ( log ` K ) ) e. CC )
203	159	rpcnne0d	|- ( ph -> ( ( log ` K ) e. CC /\ ( log ` K ) =/= 0 ) )
204		divdir	|- ( ( ( log ` X ) e. CC /\ ( 2 x. ( log ` K ) ) e. CC /\ ( ( log ` K ) e. CC /\ ( log ` K ) =/= 0 ) ) -> ( ( ( log ` X ) + ( 2 x. ( log ` K ) ) ) / ( log ` K ) ) = ( ( ( log ` X ) / ( log ` K ) ) + ( ( 2 x. ( log ` K ) ) / ( log ` K ) ) ) )
205	199 202 203 204	syl3anc	|- ( ph -> ( ( ( log ` X ) + ( 2 x. ( log ` K ) ) ) / ( log ` K ) ) = ( ( ( log ` X ) / ( log ` K ) ) + ( ( 2 x. ( log ` K ) ) / ( log ` K ) ) ) )
206	203	simprd	|- ( ph -> ( log ` K ) =/= 0 )
207	200 201 206	divcan4d	|- ( ph -> ( ( 2 x. ( log ` K ) ) / ( log ` K ) ) = 2 )
208	207	oveq2d	|- ( ph -> ( ( ( log ` X ) / ( log ` K ) ) + ( ( 2 x. ( log ` K ) ) / ( log ` K ) ) ) = ( ( ( log ` X ) / ( log ` K ) ) + 2 ) )
209	198 205 208	3eqtrd	|- ( ph -> ( ( log ` ( X x. ( K ^ 2 ) ) ) / ( log ` K ) ) = ( ( ( log ` X ) / ( log ` K ) ) + 2 ) )
210	163	recnd	|- ( ph -> ( log ` Z ) e. CC )
211		rpcnne0	|- ( 4 e. RR+ -> ( 4 e. CC /\ 4 =/= 0 ) )
212	48 211	mp1i	|- ( ph -> ( 4 e. CC /\ 4 =/= 0 ) )
213		divdiv32	|- ( ( ( log ` Z ) e. CC /\ ( 4 e. CC /\ 4 =/= 0 ) /\ ( ( log ` K ) e. CC /\ ( log ` K ) =/= 0 ) ) -> ( ( ( log ` Z ) / 4 ) / ( log ` K ) ) = ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
214	210 212 203 213	syl3anc	|- ( ph -> ( ( ( log ` Z ) / 4 ) / ( log ` K ) ) = ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
215	192 209 214	3brtr3d	|- ( ph -> ( ( ( log ` X ) / ( log ` K ) ) + 2 ) < ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
216	162 166 215	ltled	|- ( ph -> ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) )
217	113	rpred	|- ( ph -> ( ( U x. 3 ) + C ) e. RR )
218	108 103	rpdivcld	|- ( ph -> ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) e. RR+ )
219	218	rpred	|- ( ph -> ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) e. RR )
220	219 163	remulcld	|- ( ph -> ( ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) e. RR )
221	113	rpcnd	|- ( ph -> ( ( U x. 3 ) + C ) e. CC )
222	108	rpcnne0d	|- ( ph -> ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) e. CC /\ ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) =/= 0 ) )
223	103	rpcnne0d	|- ( ph -> ( ( ; 3 2 x. B ) e. CC /\ ( ; 3 2 x. B ) =/= 0 ) )
224		divdiv2	|- ( ( ( ( U x. 3 ) + C ) e. CC /\ ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) e. CC /\ ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) =/= 0 ) /\ ( ( ; 3 2 x. B ) e. CC /\ ( ; 3 2 x. B ) =/= 0 ) ) -> ( ( ( U x. 3 ) + C ) / ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) ) = ( ( ( ( U x. 3 ) + C ) x. ( ; 3 2 x. B ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) )
225	221 222 223 224	syl3anc	|- ( ph -> ( ( ( U x. 3 ) + C ) / ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) ) = ( ( ( ( U x. 3 ) + C ) x. ( ; 3 2 x. B ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) )
226	103	rpcnd	|- ( ph -> ( ; 3 2 x. B ) e. CC )
227	221 226	mulcomd	|- ( ph -> ( ( ( U x. 3 ) + C ) x. ( ; 3 2 x. B ) ) = ( ( ; 3 2 x. B ) x. ( ( U x. 3 ) + C ) ) )
228	227	oveq1d	|- ( ph -> ( ( ( ( U x. 3 ) + C ) x. ( ; 3 2 x. B ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) = ( ( ( ; 3 2 x. B ) x. ( ( U x. 3 ) + C ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) )
229		div23	|- ( ( ( ; 3 2 x. B ) e. CC /\ ( ( U x. 3 ) + C ) e. CC /\ ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) e. CC /\ ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) =/= 0 ) ) -> ( ( ( ; 3 2 x. B ) x. ( ( U x. 3 ) + C ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) = ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) )
230	226 221 222 229	syl3anc	|- ( ph -> ( ( ( ; 3 2 x. B ) x. ( ( U x. 3 ) + C ) ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) = ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) )
231	225 228 230	3eqtrd	|- ( ph -> ( ( ( U x. 3 ) + C ) / ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) ) = ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) )
232	115	reefcld	|- ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) e. RR )
233	232 96	ltaddrp2d	|- ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) < ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
234	232 173 22 233 183	lttrd	|- ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) < Z )
235	24	reeflogd	|- ( ph -> ( exp ` ( log ` Z ) ) = Z )
236	234 235	breqtrrd	|- ( ph -> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) < ( exp ` ( log ` Z ) ) )
237		eflt	|- ( ( ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) e. RR /\ ( log ` Z ) e. RR ) -> ( ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) < ( log ` Z ) <-> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) < ( exp ` ( log ` Z ) ) ) )
238	115 163 237	syl2anc	|- ( ph -> ( ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) < ( log ` Z ) <-> ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) < ( exp ` ( log ` Z ) ) ) )
239	236 238	mpbird	|- ( ph -> ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) < ( log ` Z ) )
240	231 239	eqbrtrd	|- ( ph -> ( ( ( U x. 3 ) + C ) / ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) ) < ( log ` Z ) )
241	217 163 218	ltdivmuld	|- ( ph -> ( ( ( ( U x. 3 ) + C ) / ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) ) < ( log ` Z ) <-> ( ( U x. 3 ) + C ) < ( ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) ) )
242	240 241	mpbid	|- ( ph -> ( ( U x. 3 ) + C ) < ( ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) )
243	217 220 242	ltled	|- ( ph -> ( ( U x. 3 ) + C ) <_ ( ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) )
244	104	rpcnd	|- ( ph -> ( U - E ) e. CC )
245	107	rpcnd	|- ( ph -> ( L x. ( E ^ 2 ) ) e. CC )
246		divass	|- ( ( ( U - E ) e. CC /\ ( L x. ( E ^ 2 ) ) e. CC /\ ( ( ; 3 2 x. B ) e. CC /\ ( ; 3 2 x. B ) =/= 0 ) ) -> ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) = ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) )
247	244 245 223 246	syl3anc	|- ( ph -> ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) = ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) )
248	247	oveq1d	|- ( ph -> ( ( ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) / ( ; 3 2 x. B ) ) x. ( log ` Z ) ) = ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) )
249	243 248	breqtrd	|- ( ph -> ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) )
250	155 216 249	3jca	|- ( 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 ) ) ) )
251	24 154 250	3jca	|- ( 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 ) ) ) ) )