chebbnd1lem3

Description: Lemma for chebbnd1 : get a lower bound on ppi ( N ) / ( N / log ( N ) ) that is independent of N . (Contributed by Mario Carneiro, 21-Sep-2014)

		Ref	Expression
	Hypothesis	chebbnd1lem2.1	$⊢ M = ⌊\frac{N}{2}⌋$
	Assertion	chebbnd1lem3	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log 2 - (\frac{1}{2 e})}{2} < \underline{π} (N) (\frac{\log N}{N})$

Proof

Step	Hyp	Ref	Expression
1		chebbnd1lem2.1	$⊢ M = ⌊\frac{N}{2}⌋$
2		2rp	$⊢ 2 \in ℝ^{+}$
3		relogcl	$⊢ 2 \in ℝ^{+} \to \log 2 \in ℝ$
4	2 3	ax-mp	$⊢ \log 2 \in ℝ$
5		1re	$⊢ 1 \in ℝ$
6		2re	$⊢ 2 \in ℝ$
7		ere	$⊢ e \in ℝ$
8	6 7	remulcli	$⊢ 2 e \in ℝ$
9		2pos	$⊢ 0 < 2$
10		epos	$⊢ 0 < e$
11	6 7 9 10	mulgt0ii	$⊢ 0 < 2 e$
12	8 11	gt0ne0ii	$⊢ 2 e \neq 0$
13	5 8 12	redivcli	$⊢ \frac{1}{2 e} \in ℝ$
14	4 13	resubcli	$⊢ \log 2 - (\frac{1}{2 e}) \in ℝ$
15		2ne0	$⊢ 2 \neq 0$
16	14 6 15	redivcli	$⊢ \frac{\log 2 - (\frac{1}{2 e})}{2} \in ℝ$
17	16	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log 2 - (\frac{1}{2 e})}{2} \in ℝ$
18	6	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \in ℝ$
19		8re	$⊢ 8 \in ℝ$
20	19	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 8 \in ℝ$
21		simpl	$⊢ (N \in ℝ \land 8 \leq N) \to N \in ℝ$
22		2lt8	$⊢ 2 < 8$
23	6 19 22	ltleii	$⊢ 2 \leq 8$
24	23	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \leq 8$
25		simpr	$⊢ (N \in ℝ \land 8 \leq N) \to 8 \leq N$
26	18 20 21 24 25	letrd	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \leq N$
27		ppinncl	$⊢ (N \in ℝ \land 2 \leq N) \to \underline{π} (N) \in ℕ$
28	26 27	syldan	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (N) \in ℕ$
29	28	nnred	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (N) \in ℝ$
30		rehalfcl	$⊢ N \in ℝ \to \frac{N}{2} \in ℝ$
31	30	adantr	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{N}{2} \in ℝ$
32	31	flcld	$⊢ (N \in ℝ \land 8 \leq N) \to ⌊\frac{N}{2}⌋ \in ℤ$
33	1 32	eqeltrid	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℤ$
34	33	zred	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℝ$
35		remulcl	$⊢ (2 \in ℝ \land M \in ℝ) \to 2 \cdot M \in ℝ$
36	6 34 35	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \cdot M \in ℝ$
37	5	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 1 \in ℝ$
38		1lt2	$⊢ 1 < 2$
39	38	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 1 < 2$
40		2t1e2	$⊢ 2 \cdot 1 = 2$
41		4nn	$⊢ 4 \in ℕ$
42		4z	$⊢ 4 \in ℤ$
43	42	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \in ℤ$
44		4t2e8	$⊢ 4 \cdot 2 = 8$
45	44 25	eqbrtrid	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \cdot 2 \leq N$
46		4re	$⊢ 4 \in ℝ$
47	46	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \in ℝ$
48	9	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 0 < 2$
49		lemuldiv	$⊢ (4 \in ℝ \land N \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (4 \cdot 2 \leq N \leftrightarrow 4 \leq \frac{N}{2})$
50	47 21 18 48 49	syl112anc	$⊢ (N \in ℝ \land 8 \leq N) \to (4 \cdot 2 \leq N \leftrightarrow 4 \leq \frac{N}{2})$
51	45 50	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \leq \frac{N}{2}$
52		flge	$⊢ (\frac{N}{2} \in ℝ \land 4 \in ℤ) \to (4 \leq \frac{N}{2} \leftrightarrow 4 \leq ⌊\frac{N}{2}⌋)$
53	31 42 52	sylancl	$⊢ (N \in ℝ \land 8 \leq N) \to (4 \leq \frac{N}{2} \leftrightarrow 4 \leq ⌊\frac{N}{2}⌋)$
54	51 53	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \leq ⌊\frac{N}{2}⌋$
55	54 1	breqtrrdi	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \leq M$
56		eluz2	$⊢ M \in ℤ_{\geq 4} \leftrightarrow (4 \in ℤ \land M \in ℤ \land 4 \leq M)$
57	43 33 55 56	syl3anbrc	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℤ_{\geq 4}$
58		eluznn	$⊢ (4 \in ℕ \land M \in ℤ_{\geq 4}) \to M \in ℕ$
59	41 57 58	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℕ$
60	59	nnge1d	$⊢ (N \in ℝ \land 8 \leq N) \to 1 \leq M$
61		lemul2	$⊢ (1 \in ℝ \land M \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (1 \leq M \leftrightarrow 2 \cdot 1 \leq 2 \cdot M)$
62	37 34 18 48 61	syl112anc	$⊢ (N \in ℝ \land 8 \leq N) \to (1 \leq M \leftrightarrow 2 \cdot 1 \leq 2 \cdot M)$
63	60 62	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \cdot 1 \leq 2 \cdot M$
64	40 63	eqbrtrrid	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \leq 2 \cdot M$
65	37 18 36 39 64	ltletrd	$⊢ (N \in ℝ \land 8 \leq N) \to 1 < 2 \cdot M$
66	36 65	rplogcld	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 \cdot M \in ℝ^{+}$
67	66	rpred	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 \cdot M \in ℝ$
68		2nn	$⊢ 2 \in ℕ$
69		nnmulcl	$⊢ (2 \in ℕ \land M \in ℕ) \to 2 \cdot M \in ℕ$
70	68 59 69	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \cdot M \in ℕ$
71	67 70	nndivred	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log 2 \cdot M}{2 \cdot M} \in ℝ$
72	29 71	remulcld	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) \in ℝ$
73		rehalfcl	$⊢ \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) \in ℝ \to \frac{\underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M})}{2} \in ℝ$
74	72 73	syl	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M})}{2} \in ℝ$
75		0red	$⊢ (N \in ℝ \land 8 \leq N) \to 0 \in ℝ$
76		8pos	$⊢ 0 < 8$
77	76	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 0 < 8$
78	75 20 21 77 25	ltletrd	$⊢ (N \in ℝ \land 8 \leq N) \to 0 < N$
79	21 78	elrpd	$⊢ (N \in ℝ \land 8 \leq N) \to N \in ℝ^{+}$
80	79	relogcld	$⊢ (N \in ℝ \land 8 \leq N) \to \log N \in ℝ$
81	80 79	rerpdivcld	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log N}{N} \in ℝ$
82	29 81	remulcld	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (N) (\frac{\log N}{N}) \in ℝ$
83	14	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 - (\frac{1}{2 e}) \in ℝ$
84		ppinncl	$⊢ (2 \cdot M \in ℝ \land 2 \leq 2 \cdot M) \to \underline{π} (2 \cdot M) \in ℕ$
85	36 64 84	syl2anc	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (2 \cdot M) \in ℕ$
86	85	nnred	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (2 \cdot M) \in ℝ$
87	86 71	remulcld	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (2 \cdot M) (\frac{\log 2 \cdot M}{2 \cdot M}) \in ℝ$
88		remulcl	$⊢ (\log 2 - (\frac{1}{2 e}) \in ℝ \land 2 \cdot M \in ℝ) \to (\log 2 - (\frac{1}{2 e})) 2 \cdot M \in ℝ$
89	14 36 88	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to (\log 2 - (\frac{1}{2 e})) 2 \cdot M \in ℝ$
90		4pos	$⊢ 0 < 4$
91	46 90	elrpii	$⊢ 4 \in ℝ^{+}$
92		rpexpcl	$⊢ (4 \in ℝ^{+} \land M \in ℤ) \to 4^{M} \in ℝ^{+}$
93	91 33 92	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to 4^{M} \in ℝ^{+}$
94	59	nnrpd	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℝ^{+}$
95	93 94	rpdivcld	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{4^{M}}{M} \in ℝ^{+}$
96	95	relogcld	$⊢ (N \in ℝ \land 8 \leq N) \to \log (\frac{4^{M}}{M}) \in ℝ$
97	86 67	remulcld	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (2 \cdot M) \log 2 \cdot M \in ℝ$
98	94	relogcld	$⊢ (N \in ℝ \land 8 \leq N) \to \log M \in ℝ$
99		epr	$⊢ e \in ℝ^{+}$
100		rerpdivcl	$⊢ (M \in ℝ \land e \in ℝ^{+}) \to \frac{M}{e} \in ℝ$
101	34 99 100	sylancl	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{M}{e} \in ℝ$
102	93	relogcld	$⊢ (N \in ℝ \land 8 \leq N) \to \log 4^{M} \in ℝ$
103	7	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to e \in ℝ$
104		egt2lt3	$⊢ (2 < e \land e < 3)$
105	104	simpri	$⊢ e < 3$
106		3lt4	$⊢ 3 < 4$
107		3re	$⊢ 3 \in ℝ$
108	7 107 46	lttri	$⊢ (e < 3 \land 3 < 4) \to e < 4$
109	105 106 108	mp2an	$⊢ e < 4$
110	109	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to e < 4$
111	103 47 34 110 55	ltletrd	$⊢ (N \in ℝ \land 8 \leq N) \to e < M$
112	103 34 111	ltled	$⊢ (N \in ℝ \land 8 \leq N) \to e \leq M$
113	7	leidi	$⊢ e \leq e$
114		logdivlt	$⊢ ((e \in ℝ \land e \leq e) \land (M \in ℝ \land e \leq M)) \to (e < M \leftrightarrow \frac{\log M}{M} < \frac{\log e}{e})$
115	7 113 114	mpanl12	$⊢ (M \in ℝ \land e \leq M) \to (e < M \leftrightarrow \frac{\log M}{M} < \frac{\log e}{e})$
116	34 112 115	syl2anc	$⊢ (N \in ℝ \land 8 \leq N) \to (e < M \leftrightarrow \frac{\log M}{M} < \frac{\log e}{e})$
117	111 116	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log M}{M} < \frac{\log e}{e}$
118		loge	$⊢ \log e = 1$
119	118	oveq1i	$⊢ \frac{\log e}{e} = \frac{1}{e}$
120	117 119	breqtrdi	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log M}{M} < \frac{1}{e}$
121	7 10	pm3.2i	$⊢ (e \in ℝ \land 0 < e)$
122	121	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to (e \in ℝ \land 0 < e)$
123	59	nngt0d	$⊢ (N \in ℝ \land 8 \leq N) \to 0 < M$
124	34 123	jca	$⊢ (N \in ℝ \land 8 \leq N) \to (M \in ℝ \land 0 < M)$
125		lt2mul2div	$⊢ ((\log M \in ℝ \land (e \in ℝ \land 0 < e)) \land (1 \in ℝ \land (M \in ℝ \land 0 < M))) \to (\log M e < 1 \cdot M \leftrightarrow \frac{\log M}{M} < \frac{1}{e})$
126	98 122 37 124 125	syl22anc	$⊢ (N \in ℝ \land 8 \leq N) \to (\log M e < 1 \cdot M \leftrightarrow \frac{\log M}{M} < \frac{1}{e})$
127	120 126	mpbird	$⊢ (N \in ℝ \land 8 \leq N) \to \log M e < 1 \cdot M$
128	34	recnd	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℂ$
129	128	mulid2d	$⊢ (N \in ℝ \land 8 \leq N) \to 1 \cdot M = M$
130	127 129	breqtrd	$⊢ (N \in ℝ \land 8 \leq N) \to \log M e < M$
131		ltmuldiv	$⊢ (\log M \in ℝ \land M \in ℝ \land (e \in ℝ \land 0 < e)) \to (\log M e < M \leftrightarrow \log M < \frac{M}{e})$
132	98 34 122 131	syl3anc	$⊢ (N \in ℝ \land 8 \leq N) \to (\log M e < M \leftrightarrow \log M < \frac{M}{e})$
133	130 132	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to \log M < \frac{M}{e}$
134	98 101 102 133	ltsub2dd	$⊢ (N \in ℝ \land 8 \leq N) \to \log 4^{M} - (\frac{M}{e}) < \log 4^{M} - \log M$
135	4	recni	$⊢ \log 2 \in ℂ$
136	135	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 \in ℂ$
137	13	recni	$⊢ \frac{1}{2 e} \in ℂ$
138	137	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{1}{2 e} \in ℂ$
139	70	nnrpd	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \cdot M \in ℝ^{+}$
140	139	rpcnd	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \cdot M \in ℂ$
141	136 138 140	subdird	$⊢ (N \in ℝ \land 8 \leq N) \to (\log 2 - (\frac{1}{2 e})) 2 \cdot M = \log 2 2 \cdot M - (\frac{1}{2 e}) 2 \cdot M$
142	136 140	mulcomd	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 2 \cdot M = 2 \cdot M \log 2$
143		2z	$⊢ 2 \in ℤ$
144		zmulcl	$⊢ (2 \in ℤ \land M \in ℤ) \to 2 \cdot M \in ℤ$
145	143 33 144	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \cdot M \in ℤ$
146		relogexp	$⊢ (2 \in ℝ^{+} \land 2 \cdot M \in ℤ) \to \log 2^{2 \cdot M} = 2 \cdot M \log 2$
147	2 145 146	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2^{2 \cdot M} = 2 \cdot M \log 2$
148		2cnd	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \in ℂ$
149	59	nnnn0d	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℕ_{0}$
150		2nn0	$⊢ 2 \in ℕ_{0}$
151	150	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \in ℕ_{0}$
152	148 149 151	expmuld	$⊢ (N \in ℝ \land 8 \leq N) \to 2^{2 \cdot M} = {(2^{2})}^{M}$
153		sq2	$⊢ 2^{2} = 4$
154	153	oveq1i	$⊢ {(2^{2})}^{M} = 4^{M}$
155	152 154	eqtrdi	$⊢ (N \in ℝ \land 8 \leq N) \to 2^{2 \cdot M} = 4^{M}$
156	155	fveq2d	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2^{2 \cdot M} = \log 4^{M}$
157	142 147 156	3eqtr2d	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 2 \cdot M = \log 4^{M}$
158	8	recni	$⊢ 2 e \in ℂ$
159	158	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 2 e \in ℂ$
160	12	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 2 e \neq 0$
161	140 159 160	divrec2d	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{2 \cdot M}{2 e} = (\frac{1}{2 e}) 2 \cdot M$
162	7	recni	$⊢ e \in ℂ$
163	162	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to e \in ℂ$
164	7 10	gt0ne0ii	$⊢ e \neq 0$
165	164	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to e \neq 0$
166	15	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \neq 0$
167	128 163 148 165 166	divcan5d	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{2 \cdot M}{2 e} = \frac{M}{e}$
168	161 167	eqtr3d	$⊢ (N \in ℝ \land 8 \leq N) \to (\frac{1}{2 e}) 2 \cdot M = \frac{M}{e}$
169	157 168	oveq12d	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 2 \cdot M - (\frac{1}{2 e}) 2 \cdot M = \log 4^{M} - (\frac{M}{e})$
170	141 169	eqtrd	$⊢ (N \in ℝ \land 8 \leq N) \to (\log 2 - (\frac{1}{2 e})) 2 \cdot M = \log 4^{M} - (\frac{M}{e})$
171	93 94	relogdivd	$⊢ (N \in ℝ \land 8 \leq N) \to \log (\frac{4^{M}}{M}) = \log 4^{M} - \log M$
172	134 170 171	3brtr4d	$⊢ (N \in ℝ \land 8 \leq N) \to (\log 2 - (\frac{1}{2 e})) 2 \cdot M < \log (\frac{4^{M}}{M})$
173		eqid	$⊢ if (2 \cdot M \leq (\binom{2 \cdot M}{M}), 2 \cdot M, (\binom{2 \cdot M}{M})) = if (2 \cdot M \leq (\binom{2 \cdot M}{M}), 2 \cdot M, (\binom{2 \cdot M}{M}))$
174	173	chebbnd1lem1	$⊢ M \in ℤ_{\geq 4} \to \log (\frac{4^{M}}{M}) < \underline{π} (2 \cdot M) \log 2 \cdot M$
175	57 174	syl	$⊢ (N \in ℝ \land 8 \leq N) \to \log (\frac{4^{M}}{M}) < \underline{π} (2 \cdot M) \log 2 \cdot M$
176	89 96 97 172 175	lttrd	$⊢ (N \in ℝ \land 8 \leq N) \to (\log 2 - (\frac{1}{2 e})) 2 \cdot M < \underline{π} (2 \cdot M) \log 2 \cdot M$
177	83 97 139	ltmuldivd	$⊢ (N \in ℝ \land 8 \leq N) \to ((\log 2 - (\frac{1}{2 e})) 2 \cdot M < \underline{π} (2 \cdot M) \log 2 \cdot M \leftrightarrow \log 2 - (\frac{1}{2 e}) < \frac{\underline{π} (2 \cdot M) \log 2 \cdot M}{2 \cdot M})$
178	176 177	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 - (\frac{1}{2 e}) < \frac{\underline{π} (2 \cdot M) \log 2 \cdot M}{2 \cdot M}$
179	86	recnd	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (2 \cdot M) \in ℂ$
180	66	rpcnd	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 \cdot M \in ℂ$
181	139	rpcnne0d	$⊢ (N \in ℝ \land 8 \leq N) \to (2 \cdot M \in ℂ \land 2 \cdot M \neq 0)$
182		divass	$⊢ (\underline{π} (2 \cdot M) \in ℂ \land \log 2 \cdot M \in ℂ \land (2 \cdot M \in ℂ \land 2 \cdot M \neq 0)) \to \frac{\underline{π} (2 \cdot M) \log 2 \cdot M}{2 \cdot M} = \underline{π} (2 \cdot M) (\frac{\log 2 \cdot M}{2 \cdot M})$
183	179 180 181 182	syl3anc	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\underline{π} (2 \cdot M) \log 2 \cdot M}{2 \cdot M} = \underline{π} (2 \cdot M) (\frac{\log 2 \cdot M}{2 \cdot M})$
184	178 183	breqtrd	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 - (\frac{1}{2 e}) < \underline{π} (2 \cdot M) (\frac{\log 2 \cdot M}{2 \cdot M})$
185		flle	$⊢ \frac{N}{2} \in ℝ \to ⌊\frac{N}{2}⌋ \leq \frac{N}{2}$
186	31 185	syl	$⊢ (N \in ℝ \land 8 \leq N) \to ⌊\frac{N}{2}⌋ \leq \frac{N}{2}$
187	1 186	eqbrtrid	$⊢ (N \in ℝ \land 8 \leq N) \to M \leq \frac{N}{2}$
188		lemuldiv2	$⊢ (M \in ℝ \land N \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 \cdot M \leq N \leftrightarrow M \leq \frac{N}{2})$
189	34 21 18 48 188	syl112anc	$⊢ (N \in ℝ \land 8 \leq N) \to (2 \cdot M \leq N \leftrightarrow M \leq \frac{N}{2})$
190	187 189	mpbird	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \cdot M \leq N$
191		ppiwordi	$⊢ (2 \cdot M \in ℝ \land N \in ℝ \land 2 \cdot M \leq N) \to \underline{π} (2 \cdot M) \leq \underline{π} (N)$
192	36 21 190 191	syl3anc	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (2 \cdot M) \leq \underline{π} (N)$
193	66 139	rpdivcld	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log 2 \cdot M}{2 \cdot M} \in ℝ^{+}$
194	86 29 193	lemul1d	$⊢ (N \in ℝ \land 8 \leq N) \to (\underline{π} (2 \cdot M) \leq \underline{π} (N) \leftrightarrow \underline{π} (2 \cdot M) (\frac{\log 2 \cdot M}{2 \cdot M}) \leq \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}))$
195	192 194	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (2 \cdot M) (\frac{\log 2 \cdot M}{2 \cdot M}) \leq \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M})$
196	83 87 72 184 195	ltletrd	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 - (\frac{1}{2 e}) < \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M})$
197		ltdiv1	$⊢ (\log 2 - (\frac{1}{2 e}) \in ℝ \land \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\log 2 - (\frac{1}{2 e}) < \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) \leftrightarrow \frac{\log 2 - (\frac{1}{2 e})}{2} < \frac{\underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M})}{2})$
198	83 72 18 48 197	syl112anc	$⊢ (N \in ℝ \land 8 \leq N) \to (\log 2 - (\frac{1}{2 e}) < \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) \leftrightarrow \frac{\log 2 - (\frac{1}{2 e})}{2} < \frac{\underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M})}{2})$
199	196 198	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log 2 - (\frac{1}{2 e})}{2} < \frac{\underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M})}{2}$
200	1	chebbnd1lem2	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log 2 \cdot M}{2 \cdot M} < 2 (\frac{\log N}{N})$
201		remulcl	$⊢ (2 \in ℝ \land \frac{\log N}{N} \in ℝ) \to 2 (\frac{\log N}{N}) \in ℝ$
202	6 81 201	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to 2 (\frac{\log N}{N}) \in ℝ$
203	28	nngt0d	$⊢ (N \in ℝ \land 8 \leq N) \to 0 < \underline{π} (N)$
204		ltmul2	$⊢ (\frac{\log 2 \cdot M}{2 \cdot M} \in ℝ \land 2 (\frac{\log N}{N}) \in ℝ \land (\underline{π} (N) \in ℝ \land 0 < \underline{π} (N))) \to (\frac{\log 2 \cdot M}{2 \cdot M} < 2 (\frac{\log N}{N}) \leftrightarrow \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) < \underline{π} (N) 2 (\frac{\log N}{N}))$
205	71 202 29 203 204	syl112anc	$⊢ (N \in ℝ \land 8 \leq N) \to (\frac{\log 2 \cdot M}{2 \cdot M} < 2 (\frac{\log N}{N}) \leftrightarrow \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) < \underline{π} (N) 2 (\frac{\log N}{N}))$
206	200 205	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) < \underline{π} (N) 2 (\frac{\log N}{N})$
207	29	recnd	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (N) \in ℂ$
208	81	recnd	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log N}{N} \in ℂ$
209	207 148 208	mul12d	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (N) 2 (\frac{\log N}{N}) = 2 \underline{π} (N) (\frac{\log N}{N})$
210	206 209	breqtrd	$⊢ (N \in ℝ \land 8 \leq N) \to \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) < 2 \underline{π} (N) (\frac{\log N}{N})$
211		ltdivmul	$⊢ (\underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) \in ℝ \land \underline{π} (N) (\frac{\log N}{N}) \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{\underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M})}{2} < \underline{π} (N) (\frac{\log N}{N}) \leftrightarrow \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) < 2 \underline{π} (N) (\frac{\log N}{N}))$
212	72 82 18 48 211	syl112anc	$⊢ (N \in ℝ \land 8 \leq N) \to (\frac{\underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M})}{2} < \underline{π} (N) (\frac{\log N}{N}) \leftrightarrow \underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M}) < 2 \underline{π} (N) (\frac{\log N}{N}))$
213	210 212	mpbird	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\underline{π} (N) (\frac{\log 2 \cdot M}{2 \cdot M})}{2} < \underline{π} (N) (\frac{\log N}{N})$
214	17 74 82 199 213	lttrd	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log 2 - (\frac{1}{2 e})}{2} < \underline{π} (N) (\frac{\log N}{N})$

Metamath Proof Explorer

Theorem chebbnd1lem3

Proof