pntlemr

	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.o	$⊢ O = (⌊\frac{Z}{K^{J + 1}}⌋ + 1 \dots ⌊\frac{Z}{K^{J}}⌋)$
	pntlem1.v	$⊢ φ \to V \in ℝ^{+}$
	pntlem1.V	$⊢ φ \to ((K^{J} < V \land (1 + L E) V < K K^{J}) \land \forall u \in [V, (1 + L E) V] \|\frac{R (u)}{u}\| \leq E)$
	pntlem1.j	$⊢ φ \to J \in (M ..^N)$
	pntlem1.i	$⊢ I = (⌊\frac{Z}{(1 + L E) V}⌋ + 1 \dots ⌊\frac{Z}{V}⌋)$
Assertion	pntlemr	$⊢ φ \to (U - E) (\frac{L E}{8}) \log Z \leq \|I\| (U - E) (\frac{\log (\frac{Z}{V})}{\frac{Z}{V}})$

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

Metamath Proof Explorer

Theorem pntlemr

Proof