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 \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, +∞)$
Assertion	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))$

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

Metamath Proof Explorer

Theorem pntlemb

Proof