chebbnd1lem2

Description: Lemma for chebbnd1 : Show that log ( N ) / N does not change too much between N and M = |_ ( N / 2 ) . (Contributed by Mario Carneiro, 22-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		chebbnd1lem2.1	$⊢ M = ⌊\frac{N}{2}⌋$
2		2rp	$⊢ 2 \in ℝ^{+}$
3		4nn	$⊢ 4 \in ℕ$
4		4z	$⊢ 4 \in ℤ$
5	4	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \in ℤ$
6		rehalfcl	$⊢ N \in ℝ \to \frac{N}{2} \in ℝ$
7	6	adantr	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{N}{2} \in ℝ$
8	7	flcld	$⊢ (N \in ℝ \land 8 \leq N) \to ⌊\frac{N}{2}⌋ \in ℤ$
9	1 8	eqeltrid	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℤ$
10		4t2e8	$⊢ 4 \cdot 2 = 8$
11		simpr	$⊢ (N \in ℝ \land 8 \leq N) \to 8 \leq N$
12	10 11	eqbrtrid	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \cdot 2 \leq N$
13		4re	$⊢ 4 \in ℝ$
14	13	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \in ℝ$
15		simpl	$⊢ (N \in ℝ \land 8 \leq N) \to N \in ℝ$
16		2re	$⊢ 2 \in ℝ$
17	16	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \in ℝ$
18		2pos	$⊢ 0 < 2$
19	18	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 0 < 2$
20		lemuldiv	$⊢ (4 \in ℝ \land N \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (4 \cdot 2 \leq N \leftrightarrow 4 \leq \frac{N}{2})$
21	14 15 17 19 20	syl112anc	$⊢ (N \in ℝ \land 8 \leq N) \to (4 \cdot 2 \leq N \leftrightarrow 4 \leq \frac{N}{2})$
22	12 21	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \leq \frac{N}{2}$
23		flge	$⊢ (\frac{N}{2} \in ℝ \land 4 \in ℤ) \to (4 \leq \frac{N}{2} \leftrightarrow 4 \leq ⌊\frac{N}{2}⌋)$
24	7 4 23	sylancl	$⊢ (N \in ℝ \land 8 \leq N) \to (4 \leq \frac{N}{2} \leftrightarrow 4 \leq ⌊\frac{N}{2}⌋)$
25	22 24	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \leq ⌊\frac{N}{2}⌋$
26	25 1	breqtrrdi	$⊢ (N \in ℝ \land 8 \leq N) \to 4 \leq M$
27		eluz2	$⊢ M \in ℤ_{\geq 4} \leftrightarrow (4 \in ℤ \land M \in ℤ \land 4 \leq M)$
28	5 9 26 27	syl3anbrc	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℤ_{\geq 4}$
29		eluznn	$⊢ (4 \in ℕ \land M \in ℤ_{\geq 4}) \to M \in ℕ$
30	3 28 29	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℕ$
31	30	nnrpd	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℝ^{+}$
32		rpmulcl	$⊢ (2 \in ℝ^{+} \land M \in ℝ^{+}) \to 2 \cdot M \in ℝ^{+}$
33	2 31 32	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \cdot M \in ℝ^{+}$
34	33	relogcld	$⊢ (N \in ℝ \land 8 \leq N) \to \log 2 \cdot M \in ℝ$
35	34 33	rerpdivcld	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log 2 \cdot M}{2 \cdot M} \in ℝ$
36		0red	$⊢ (N \in ℝ \land 8 \leq N) \to 0 \in ℝ$
37		8re	$⊢ 8 \in ℝ$
38	37	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 8 \in ℝ$
39		8pos	$⊢ 0 < 8$
40	39	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 0 < 8$
41	36 38 15 40 11	ltletrd	$⊢ (N \in ℝ \land 8 \leq N) \to 0 < N$
42	15 41	elrpd	$⊢ (N \in ℝ \land 8 \leq N) \to N \in ℝ^{+}$
43	42	rphalfcld	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{N}{2} \in ℝ^{+}$
44	43	relogcld	$⊢ (N \in ℝ \land 8 \leq N) \to \log (\frac{N}{2}) \in ℝ$
45	44 43	rerpdivcld	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log (\frac{N}{2})}{\frac{N}{2}} \in ℝ$
46	42	relogcld	$⊢ (N \in ℝ \land 8 \leq N) \to \log N \in ℝ$
47	46 42	rerpdivcld	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log N}{N} \in ℝ$
48		remulcl	$⊢ (2 \in ℝ \land \frac{\log N}{N} \in ℝ) \to 2 (\frac{\log N}{N}) \in ℝ$
49	16 47 48	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to 2 (\frac{\log N}{N}) \in ℝ$
50	9	zred	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℝ$
51		peano2re	$⊢ M \in ℝ \to M + 1 \in ℝ$
52	50 51	syl	$⊢ (N \in ℝ \land 8 \leq N) \to M + 1 \in ℝ$
53		remulcl	$⊢ (2 \in ℝ \land M \in ℝ) \to 2 \cdot M \in ℝ$
54	16 50 53	sylancr	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \cdot M \in ℝ$
55		flltp1	$⊢ \frac{N}{2} \in ℝ \to \frac{N}{2} < ⌊\frac{N}{2}⌋ + 1$
56	7 55	syl	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{N}{2} < ⌊\frac{N}{2}⌋ + 1$
57	1	oveq1i	$⊢ M + 1 = ⌊\frac{N}{2}⌋ + 1$
58	56 57	breqtrrdi	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{N}{2} < M + 1$
59		1red	$⊢ (N \in ℝ \land 8 \leq N) \to 1 \in ℝ$
60	30	nnge1d	$⊢ (N \in ℝ \land 8 \leq N) \to 1 \leq M$
61	59 50 50 60	leadd2dd	$⊢ (N \in ℝ \land 8 \leq N) \to M + 1 \leq M + M$
62	50	recnd	$⊢ (N \in ℝ \land 8 \leq N) \to M \in ℂ$
63	62	2timesd	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \cdot M = M + M$
64	61 63	breqtrrd	$⊢ (N \in ℝ \land 8 \leq N) \to M + 1 \leq 2 \cdot M$
65	7 52 54 58 64	ltletrd	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{N}{2} < 2 \cdot M$
66		ere	$⊢ e \in ℝ$
67	66	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to e \in ℝ$
68		egt2lt3	$⊢ (2 < e \land e < 3)$
69	68	simpri	$⊢ e < 3$
70		3lt4	$⊢ 3 < 4$
71		3re	$⊢ 3 \in ℝ$
72	66 71 13	lttri	$⊢ (e < 3 \land 3 < 4) \to e < 4$
73	69 70 72	mp2an	$⊢ e < 4$
74	73	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to e < 4$
75	67 14 7 74 22	ltletrd	$⊢ (N \in ℝ \land 8 \leq N) \to e < \frac{N}{2}$
76	67 7 75	ltled	$⊢ (N \in ℝ \land 8 \leq N) \to e \leq \frac{N}{2}$
77	67 7 54 75 65	lttrd	$⊢ (N \in ℝ \land 8 \leq N) \to e < 2 \cdot M$
78	67 54 77	ltled	$⊢ (N \in ℝ \land 8 \leq N) \to e \leq 2 \cdot M$
79		logdivlt	$⊢ ((\frac{N}{2} \in ℝ \land e \leq \frac{N}{2}) \land (2 \cdot M \in ℝ \land e \leq 2 \cdot M)) \to (\frac{N}{2} < 2 \cdot M \leftrightarrow \frac{\log 2 \cdot M}{2 \cdot M} < \frac{\log (\frac{N}{2})}{\frac{N}{2}})$
80	7 76 54 78 79	syl22anc	$⊢ (N \in ℝ \land 8 \leq N) \to (\frac{N}{2} < 2 \cdot M \leftrightarrow \frac{\log 2 \cdot M}{2 \cdot M} < \frac{\log (\frac{N}{2})}{\frac{N}{2}})$
81	65 80	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log 2 \cdot M}{2 \cdot M} < \frac{\log (\frac{N}{2})}{\frac{N}{2}}$
82		rphalflt	$⊢ N \in ℝ^{+} \to \frac{N}{2} < N$
83	42 82	syl	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{N}{2} < N$
84		logltb	$⊢ (\frac{N}{2} \in ℝ^{+} \land N \in ℝ^{+}) \to (\frac{N}{2} < N \leftrightarrow \log (\frac{N}{2}) < \log N)$
85	43 42 84	syl2anc	$⊢ (N \in ℝ \land 8 \leq N) \to (\frac{N}{2} < N \leftrightarrow \log (\frac{N}{2}) < \log N)$
86	83 85	mpbid	$⊢ (N \in ℝ \land 8 \leq N) \to \log (\frac{N}{2}) < \log N$
87	44 46 43 86	ltdiv1dd	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log (\frac{N}{2})}{\frac{N}{2}} < \frac{\log N}{\frac{N}{2}}$
88	46	recnd	$⊢ (N \in ℝ \land 8 \leq N) \to \log N \in ℂ$
89	15	recnd	$⊢ (N \in ℝ \land 8 \leq N) \to N \in ℂ$
90	17	recnd	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \in ℂ$
91	42	rpne0d	$⊢ (N \in ℝ \land 8 \leq N) \to N \neq 0$
92		2ne0	$⊢ 2 \neq 0$
93	92	a1i	$⊢ (N \in ℝ \land 8 \leq N) \to 2 \neq 0$
94	88 89 90 91 93	divdiv2d	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log N}{\frac{N}{2}} = \frac{\log N \cdot 2}{N}$
95	88 90	mulcomd	$⊢ (N \in ℝ \land 8 \leq N) \to \log N \cdot 2 = 2 \log N$
96	95	oveq1d	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log N \cdot 2}{N} = \frac{2 \log N}{N}$
97	90 88 89 91	divassd	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{2 \log N}{N} = 2 (\frac{\log N}{N})$
98	94 96 97	3eqtrd	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log N}{\frac{N}{2}} = 2 (\frac{\log N}{N})$
99	87 98	breqtrd	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log (\frac{N}{2})}{\frac{N}{2}} < 2 (\frac{\log N}{N})$
100	35 45 49 81 99	lttrd	$⊢ (N \in ℝ \land 8 \leq N) \to \frac{\log 2 \cdot M}{2 \cdot M} < 2 (\frac{\log N}{N})$

Metamath Proof Explorer

Theorem chebbnd1lem2

Proof